Copyright | (C) 2020 Ryan Scott |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Richard Eisenberg (rae@cs.brynmawr.edu) |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | GHC2021 |
Exports promoted and singled versions of the definitions in Data.Proxy.
Synopsis
- type family Sing :: k -> Type
- data SProxy :: Proxy t -> Type where
- type family AsProxyTypeOf (a :: a) (a :: proxy a) :: a where ...
- sAsProxyTypeOf :: forall (t :: a) (t :: proxy a). Sing t -> Sing t -> Sing (Apply (Apply AsProxyTypeOfSym0 t) t :: a) :: Type
- type family ProxySym0 where ...
- data AsProxyTypeOfSym0 :: (~>) a ((~>) (proxy a) a)
- data AsProxyTypeOfSym1 (a6989586621680381772 :: a) :: (~>) (proxy a) a
- type family AsProxyTypeOfSym2 (a6989586621680381772 :: a) (a6989586621680381773 :: proxy a) :: a where ...
The Proxy
singleton
type family Sing :: k -> Type Source #
The singleton kind-indexed type family.
Instances
data SProxy :: Proxy t -> Type where Source #
Instances
TestCoercion (SProxy :: Proxy t -> Type) Source # | |
Defined in Data.Proxy.Singletons | |
TestEquality (SProxy :: Proxy t -> Type) Source # | |
Defined in Data.Proxy.Singletons | |
Show (SProxy z) Source # | |
type family AsProxyTypeOf (a :: a) (a :: proxy a) :: a where ... Source #
AsProxyTypeOf a_6989586621680381765 a_6989586621680381767 = Apply (Apply ConstSym0 a_6989586621680381765) a_6989586621680381767 |
sAsProxyTypeOf :: forall (t :: a) (t :: proxy a). Sing t -> Sing t -> Sing (Apply (Apply AsProxyTypeOfSym0 t) t :: a) :: Type Source #
Defunctionalization symbols
data AsProxyTypeOfSym0 :: (~>) a ((~>) (proxy a) a) Source #
Instances
SingI (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type) Source # | |
Defined in Data.Proxy.Singletons | |
SuppressUnusedWarnings (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type) Source # | |
Defined in Data.Proxy.Singletons suppressUnusedWarnings :: () Source # | |
type Apply (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type) (a6989586621680381772 :: a) Source # | |
Defined in Data.Proxy.Singletons type Apply (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type) (a6989586621680381772 :: a) = AsProxyTypeOfSym1 a6989586621680381772 :: TyFun (proxy a) a -> Type |
data AsProxyTypeOfSym1 (a6989586621680381772 :: a) :: (~>) (proxy a) a Source #
Instances
SingI1 (AsProxyTypeOfSym1 :: a -> TyFun (proxy a) a -> Type) Source # | |
Defined in Data.Proxy.Singletons | |
SingI d => SingI (AsProxyTypeOfSym1 d :: TyFun (proxy a) a -> Type) Source # | |
Defined in Data.Proxy.Singletons sing :: Sing (AsProxyTypeOfSym1 d) Source # | |
SuppressUnusedWarnings (AsProxyTypeOfSym1 a6989586621680381772 :: TyFun (proxy a) a -> Type) Source # | |
Defined in Data.Proxy.Singletons suppressUnusedWarnings :: () Source # | |
type Apply (AsProxyTypeOfSym1 a6989586621680381772 :: TyFun (proxy a) a -> Type) (a6989586621680381773 :: proxy a) Source # | |
Defined in Data.Proxy.Singletons type Apply (AsProxyTypeOfSym1 a6989586621680381772 :: TyFun (proxy a) a -> Type) (a6989586621680381773 :: proxy a) = AsProxyTypeOf a6989586621680381772 a6989586621680381773 |
type family AsProxyTypeOfSym2 (a6989586621680381772 :: a) (a6989586621680381773 :: proxy a) :: a where ... Source #
AsProxyTypeOfSym2 a6989586621680381772 a6989586621680381773 = AsProxyTypeOf a6989586621680381772 a6989586621680381773 |