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 (a6989586621680080240 :: a) :: (~>) (proxy a) a
- type family AsProxyTypeOfSym2 (a6989586621680080240 :: a) (a6989586621680080241 :: proxy a) :: a where ...
The Proxy
singleton
type family Sing :: k -> Type #
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 testCoercion :: forall (a :: k) (b :: k). SProxy a -> SProxy b -> Maybe (Coercion a b) | |
TestEquality (SProxy :: Proxy t -> Type) Source # | |
Defined in Data.Proxy.Singletons testEquality :: forall (a :: k) (b :: k). SProxy a -> SProxy b -> Maybe (a :~: b) | |
Show (SProxy z) Source # | |
type family AsProxyTypeOf (a :: a) (a :: proxy a) :: a where ... Source #
AsProxyTypeOf a_6989586621680080233 a_6989586621680080235 = Apply (Apply ConstSym0 a_6989586621680080233) a_6989586621680080235 |
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 :: () # | |
type Apply (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type) (a6989586621680080240 :: a) Source # | |
Defined in Data.Proxy.Singletons type Apply (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type) (a6989586621680080240 :: a) = AsProxyTypeOfSym1 a6989586621680080240 :: TyFun (proxy a) a -> Type |
data AsProxyTypeOfSym1 (a6989586621680080240 :: a) :: (~>) (proxy a) a Source #
Instances
SingI1 (AsProxyTypeOfSym1 :: a -> TyFun (proxy a) a -> Type) Source # | |
Defined in Data.Proxy.Singletons liftSing :: forall (x :: k1). Sing x -> Sing (AsProxyTypeOfSym1 x) # | |
SingI d => SingI (AsProxyTypeOfSym1 d :: TyFun (proxy a) a -> Type) Source # | |
Defined in Data.Proxy.Singletons sing :: Sing (AsProxyTypeOfSym1 d) # | |
SuppressUnusedWarnings (AsProxyTypeOfSym1 a6989586621680080240 :: TyFun (proxy a) a -> Type) Source # | |
Defined in Data.Proxy.Singletons suppressUnusedWarnings :: () # | |
type Apply (AsProxyTypeOfSym1 a6989586621680080240 :: TyFun (proxy a) a -> Type) (a6989586621680080241 :: proxy a) Source # | |
Defined in Data.Proxy.Singletons type Apply (AsProxyTypeOfSym1 a6989586621680080240 :: TyFun (proxy a) a -> Type) (a6989586621680080241 :: proxy a) = AsProxyTypeOf a6989586621680080240 a6989586621680080241 |
type family AsProxyTypeOfSym2 (a6989586621680080240 :: a) (a6989586621680080241 :: proxy a) :: a where ... Source #
AsProxyTypeOfSym2 a6989586621680080240 a6989586621680080241 = AsProxyTypeOf a6989586621680080240 a6989586621680080241 |