{-# LANGUAGE MagicHash, RankNTypes, PolyKinds, GADTs, DataKinds,
FlexibleContexts, FlexibleInstances,
TypeFamilies, TypeOperators, TypeFamilyDependencies,
UndecidableInstances, ConstraintKinds,
ScopedTypeVariables, TypeApplications, AllowAmbiguousTypes,
PatternSynonyms, ViewPatterns, StandaloneKindSignatures #-}
module Data.Singletons.Internal (
module Data.Singletons.Internal
, Proxy(..)
) where
import Data.Kind (Type)
import Unsafe.Coerce
import Data.Proxy ( Proxy(..) )
import GHC.Exts ( Proxy#, Constraint )
type KindOf :: k -> Type
type KindOf (a :: k) = k
type SameKind :: k -> k -> Constraint
type SameKind a b = ()
type Sing :: k -> Type
type family Sing
class SingI a where
sing :: Sing a
{-# COMPLETE Sing #-}
pattern Sing :: forall k (a :: k). () => SingI a => Sing a
pattern $bSing :: Sing a
$mSing :: forall r k (a :: k). Sing a -> (SingI a => r) -> (Void# -> r) -> r
Sing <- (singInstance -> SingInstance)
where Sing = Sing a
forall k (a :: k). SingI a => Sing a
sing
type SingKind :: Type -> Constraint
class SingKind k where
type Demote k = (r :: Type) | r -> k
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
type SomeSing :: Type -> Type
data SomeSing k where
SomeSing :: Sing (a :: k) -> SomeSing k
{-# COMPLETE FromSing #-}
pattern FromSing :: SingKind k => forall (a :: k). Sing a -> Demote k
pattern $bFromSing :: Sing a -> Demote k
$mFromSing :: forall r k.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> (Void# -> r) -> r
FromSing sng <- ((\demotedVal -> withSomeSing demotedVal SomeSing) -> SomeSing sng)
where FromSing Sing a
sng = Sing a -> Demote k
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a
sng
type WrappedSing :: k -> Type
newtype WrappedSing a where
WrapSing :: forall k (a :: k). { WrappedSing a -> Sing a
unwrapSing :: Sing a } -> WrappedSing a
type SWrappedSing :: forall k (a :: k). WrappedSing a -> Type
newtype SWrappedSing ws where
SWrapSing :: forall k (a :: k) (ws :: WrappedSing a).
{ SWrappedSing ws -> Sing a
sUnwrapSing :: Sing a } -> SWrappedSing ws
type instance Sing = SWrappedSing
type UnwrapSing :: WrappedSing a -> Sing a
type family UnwrapSing ws where
UnwrapSing ('WrapSing s) = s
instance SingKind (WrappedSing a) where
type Demote (WrappedSing a) = WrappedSing a
fromSing :: Sing a -> Demote (WrappedSing a)
fromSing (SWrapSing s) = Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing Sing a
s
toSing :: Demote (WrappedSing a) -> SomeSing (WrappedSing a)
toSing (WrapSing s) = Sing Any -> SomeSing (WrappedSing a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing Any -> SomeSing (WrappedSing a))
-> Sing Any -> SomeSing (WrappedSing a)
forall a b. (a -> b) -> a -> b
$ Sing a -> SWrappedSing Any
forall k (a :: k) (ws :: WrappedSing a). Sing a -> SWrappedSing ws
SWrapSing Sing a
s
instance forall a (s :: Sing a). SingI a => SingI ('WrapSing s) where
sing :: Sing ('WrapSing s)
sing = Sing a -> SWrappedSing ('WrapSing s)
forall k (a :: k) (ws :: WrappedSing a). Sing a -> SWrappedSing ws
SWrapSing Sing a
forall k (a :: k). SingI a => Sing a
sing
type SingInstance :: k -> Type
data SingInstance a where
SingInstance :: SingI a => SingInstance a
type DI :: k -> Type
newtype DI a = Don'tInstantiate (SingI a => SingInstance a)
singInstance :: forall k (a :: k). Sing a -> SingInstance a
singInstance :: Sing a -> SingInstance a
singInstance Sing a
s = (SingI a => SingInstance a) -> SingInstance a
with_sing_i SingI a => SingInstance a
forall k (a :: k). SingI a => SingInstance a
SingInstance
where
with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
with_sing_i SingI a => SingInstance a
si = DI a -> Sing a -> SingInstance a
forall a b. a -> b
unsafeCoerce ((SingI a => SingInstance a) -> DI a
forall k (a :: k). (SingI a => SingInstance a) -> DI a
Don'tInstantiate SingI a => SingInstance a
si) Sing a
s
type TyFun :: Type -> Type -> Type
data TyFun a b
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type Apply :: (k1 ~> k2) -> k1 -> k2
type family Apply f x
type (@@) :: (k1 ~> k2) -> k1 -> k2
type a @@ b = Apply a b
infixl 9 @@
type TyCon :: (k1 -> k2) -> unmatchable_fun
data family TyCon
type ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun)
type family ApplyTyCon where
ApplyTyCon @k1 @(k2 -> k3) @unmatchable_fun = ApplyTyConAux2
ApplyTyCon @k1 @k2 @k2 = ApplyTyConAux1
type instance Apply (TyCon f) x = ApplyTyCon f @@ x
type ApplyTyConAux1 :: (k1 -> k2) -> (k1 ~> k2)
data ApplyTyConAux1 f z
type ApplyTyConAux2 :: (k1 -> k2 -> k3) -> (k1 ~> unmatchable_fun)
data ApplyTyConAux2 f z
type instance Apply (ApplyTyConAux1 f) x = f x
type instance Apply (ApplyTyConAux2 f) x = TyCon (f x)
type TyCon1 :: (k1 -> k2) -> (k1 ~> k2)
type TyCon1 = TyCon
type TyCon2 :: (k1 -> k2 -> k3) -> (k1 ~> k2 ~> k3)
type TyCon2 = TyCon
type TyCon3 :: (k1 -> k2 -> k3 -> k4) -> (k1 ~> k2 ~> k3 ~> k4)
type TyCon3 = TyCon
type TyCon4 :: (k1 -> k2 -> k3 -> k4 -> k5) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5)
type TyCon4 = TyCon
type TyCon5 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6)
-> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6)
type TyCon5 = TyCon
type TyCon6 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7)
-> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7)
type TyCon6 = TyCon
type TyCon7 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8)
-> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8)
type TyCon7 = TyCon
type TyCon8 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
-> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9)
type TyCon8 = TyCon
type SLambda :: (k1 ~> k2) -> Type
newtype SLambda f =
SLambda { SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
applySing :: forall t. Sing t -> Sing (f @@ t) }
type instance Sing = SLambda
(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
@@ :: Sing f -> Sing t -> Sing (f @@ t)
(@@) = Sing f -> Sing t -> Sing (f @@ t)
forall k1 k2 (f :: k1 ~> k2).
SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
applySing
instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
type Demote (k1 ~> k2) = Demote k1 -> Demote k2
fromSing :: Sing a -> Demote (k1 ~> k2)
fromSing Sing a
sFun Demote k1
x = Demote k1 -> (forall (a :: k1). Sing a -> Demote k2) -> Demote k2
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
x (Sing (Apply a a) -> Demote k2
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (Sing (Apply a a) -> Demote k2)
-> (Sing a -> Sing (Apply a a)) -> Sing a -> Demote k2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SLambda a -> forall (t :: k1). Sing t -> Sing (a @@ t)
forall k1 k2 (f :: k1 ~> k2).
SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
applySing SLambda a
Sing a
sFun)
toSing :: Demote (k1 ~> k2) -> SomeSing (k1 ~> k2)
toSing Demote (k1 ~> k2)
f = Sing Any -> SomeSing (k1 ~> k2)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing Any
forall (f :: k1 ~> k2). Sing f
slam
where
slam :: forall (f :: k1 ~> k2). Sing f
slam :: Sing f
slam = SingFunction1 f -> Sing f
forall a1 b (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 @f SingFunction1 f
lam
where
lam :: forall (t :: k1). Sing t -> Sing (f @@ t)
lam :: Sing t -> Sing (f @@ t)
lam Sing t
x = Demote k2
-> (forall (a :: k2). Sing a -> Sing (f @@ t)) -> Sing (f @@ t)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (Demote (k1 ~> k2)
Demote k1 -> Demote k2
f (Sing t -> Demote k1
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
x)) (\(r :: Sing res) -> Sing a -> Sing (f @@ t)
forall a b. a -> b
unsafeCoerce Sing a
r)
type SingFunction1 :: (a1 ~> b) -> Type
type SingFunction1 f = forall t. Sing t -> Sing (f @@ t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 :: SingFunction1 f -> Sing f
singFun1 SingFunction1 f
f = SingFunction1 f -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda SingFunction1 f
f
type SingFunction2 :: (a1 ~> a2 ~> b) -> Type
type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f @@ t1 @@ t2)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 :: SingFunction2 f -> Sing f
singFun2 SingFunction2 f
f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\Sing t
x -> SingFunction1 (f @@ t) -> Sing (f @@ t)
forall a1 b (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (Sing t -> Sing t -> Sing ((f @@ t) @@ t)
SingFunction2 f
f Sing t
x))
type SingFunction3 :: (a1 ~> a2 ~> a3 ~> b) -> Type
type SingFunction3 f = forall t1 t2 t3.
Sing t1 -> Sing t2 -> Sing t3
-> Sing (f @@ t1 @@ t2 @@ t3)
singFun3 :: forall f. SingFunction3 f -> Sing f
singFun3 :: SingFunction3 f -> Sing f
singFun3 SingFunction3 f
f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\Sing t
x -> SingFunction2 (f @@ t) -> Sing (f @@ t)
forall a1 a2 b (f :: a1 ~> (a2 ~> b)). SingFunction2 f -> Sing f
singFun2 (Sing t -> Sing t1 -> Sing t2 -> Sing (((f @@ t) @@ t1) @@ t2)
SingFunction3 f
f Sing t
x))
type SingFunction4 :: (a1 ~> a2 ~> a3 ~> a4 ~> b) -> Type
type SingFunction4 f = forall t1 t2 t3 t4.
Sing t1 -> Sing t2 -> Sing t3 -> Sing t4
-> Sing (f @@ t1 @@ t2 @@ t3 @@ t4)
singFun4 :: forall f. SingFunction4 f -> Sing f
singFun4 :: SingFunction4 f -> Sing f
singFun4 SingFunction4 f
f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\Sing t
x -> SingFunction3 (f @@ t) -> Sing (f @@ t)
forall a1 a2 a3 b (f :: a1 ~> (a2 ~> (a3 ~> b))).
SingFunction3 f -> Sing f
singFun3 (Sing t
-> Sing t1
-> Sing t2
-> Sing t3
-> Sing ((((f @@ t) @@ t1) @@ t2) @@ t3)
SingFunction4 f
f Sing t
x))
type SingFunction5 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> b) -> Type
type SingFunction5 f = forall t1 t2 t3 t4 t5.
Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5
-> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5)
singFun5 :: forall f. SingFunction5 f -> Sing f
singFun5 :: SingFunction5 f -> Sing f
singFun5 SingFunction5 f
f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\Sing t
x -> SingFunction4 (f @@ t) -> Sing (f @@ t)
forall a1 a2 a3 a4 b (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
SingFunction4 f -> Sing f
singFun4 (Sing t
-> Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing (((((f @@ t) @@ t1) @@ t2) @@ t3) @@ t4)
SingFunction5 f
f Sing t
x))
type SingFunction6 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> b) -> Type
type SingFunction6 f = forall t1 t2 t3 t4 t5 t6.
Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6
-> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6)
singFun6 :: forall f. SingFunction6 f -> Sing f
singFun6 :: SingFunction6 f -> Sing f
singFun6 SingFunction6 f
f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\Sing t
x -> SingFunction5 (f @@ t) -> Sing (f @@ t)
forall a1 a2 a3 a4 a5 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
SingFunction5 f -> Sing f
singFun5 (Sing t
-> Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing ((((((f @@ t) @@ t1) @@ t2) @@ t3) @@ t4) @@ t5)
SingFunction6 f
f Sing t
x))
type SingFunction7 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> b) -> Type
type SingFunction7 f = forall t1 t2 t3 t4 t5 t6 t7.
Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7
-> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6 @@ t7)
singFun7 :: forall f. SingFunction7 f -> Sing f
singFun7 :: SingFunction7 f -> Sing f
singFun7 SingFunction7 f
f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\Sing t
x -> SingFunction6 (f @@ t) -> Sing (f @@ t)
forall a1 a2 a3 a4 a5 a6 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
SingFunction6 f -> Sing f
singFun6 (Sing t
-> Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing t6
-> Sing (((((((f @@ t) @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6)
SingFunction7 f
f Sing t
x))
type SingFunction8 :: (a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> a8 ~> b) -> Type
type SingFunction8 f = forall t1 t2 t3 t4 t5 t6 t7 t8.
Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing t8
-> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6 @@ t7 @@ t8)
singFun8 :: forall f. SingFunction8 f -> Sing f
singFun8 :: SingFunction8 f -> Sing f
singFun8 SingFunction8 f
f = (forall (t :: a1). Sing t -> Sing (f @@ t)) -> SLambda f
forall k1 k2 (f :: k1 ~> k2).
(forall (t :: k1). Sing t -> Sing (f @@ t)) -> SLambda f
SLambda (\Sing t
x -> SingFunction7 (f @@ t) -> Sing (f @@ t)
forall a1 a2 a3 a4 a5 a6 a7 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))).
SingFunction7 f -> Sing f
singFun7 (Sing t
-> Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing t6
-> Sing t7
-> Sing
((((((((f @@ t) @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7)
SingFunction8 f
f Sing t
x))
unSingFun1 :: forall f. Sing f -> SingFunction1 f
unSingFun1 :: Sing f -> SingFunction1 f
unSingFun1 Sing f
sf = SLambda f -> SingFunction1 f
forall k1 k2 (f :: k1 ~> k2).
SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
applySing SLambda f
Sing f
sf
unSingFun2 :: forall f. Sing f -> SingFunction2 f
unSingFun2 :: Sing f -> SingFunction2 f
unSingFun2 Sing f
sf Sing t1
x = Sing (Apply f t1) -> SingFunction1 (Apply f t1)
forall a1 b (f :: a1 ~> b). Sing f -> SingFunction1 f
unSingFun1 (Sing f
sf Sing f -> Sing t1 -> Sing (Apply f t1)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t1
x)
unSingFun3 :: forall f. Sing f -> SingFunction3 f
unSingFun3 :: Sing f -> SingFunction3 f
unSingFun3 Sing f
sf Sing t1
x = Sing (Apply f t1) -> SingFunction2 (Apply f t1)
forall a1 a2 b (f :: a1 ~> (a2 ~> b)). Sing f -> SingFunction2 f
unSingFun2 (Sing f
sf Sing f -> Sing t1 -> Sing (Apply f t1)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t1
x)
unSingFun4 :: forall f. Sing f -> SingFunction4 f
unSingFun4 :: Sing f -> SingFunction4 f
unSingFun4 Sing f
sf Sing t1
x = Sing (Apply f t1) -> SingFunction3 (Apply f t1)
forall a1 a2 a3 b (f :: a1 ~> (a2 ~> (a3 ~> b))).
Sing f -> SingFunction3 f
unSingFun3 (Sing f
sf Sing f -> Sing t1 -> Sing (Apply f t1)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t1
x)
unSingFun5 :: forall f. Sing f -> SingFunction5 f
unSingFun5 :: Sing f -> SingFunction5 f
unSingFun5 Sing f
sf Sing t1
x = Sing (Apply f t1) -> SingFunction4 (Apply f t1)
forall a1 a2 a3 a4 b (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
Sing f -> SingFunction4 f
unSingFun4 (Sing f
sf Sing f -> Sing t1 -> Sing (Apply f t1)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t1
x)
unSingFun6 :: forall f. Sing f -> SingFunction6 f
unSingFun6 :: Sing f -> SingFunction6 f
unSingFun6 Sing f
sf Sing t1
x = Sing (Apply f t1) -> SingFunction5 (Apply f t1)
forall a1 a2 a3 a4 a5 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
Sing f -> SingFunction5 f
unSingFun5 (Sing f
sf Sing f -> Sing t1 -> Sing (Apply f t1)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t1
x)
unSingFun7 :: forall f. Sing f -> SingFunction7 f
unSingFun7 :: Sing f -> SingFunction7 f
unSingFun7 Sing f
sf Sing t1
x = Sing (Apply f t1) -> SingFunction6 (Apply f t1)
forall a1 a2 a3 a4 a5 a6 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
Sing f -> SingFunction6 f
unSingFun6 (Sing f
sf Sing f -> Sing t1 -> Sing (Apply f t1)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t1
x)
unSingFun8 :: forall f. Sing f -> SingFunction8 f
unSingFun8 :: Sing f -> SingFunction8 f
unSingFun8 Sing f
sf Sing t1
x = Sing (Apply f t1) -> SingFunction7 (Apply f t1)
forall a1 a2 a3 a4 a5 a6 a7 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))).
Sing f -> SingFunction7 f
unSingFun7 (Sing f
sf Sing f -> Sing t1 -> Sing (Apply f t1)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing t1
x)
{-# COMPLETE SLambda2 #-}
pattern SLambda2 :: forall f. SingFunction2 f -> Sing f
pattern $bSLambda2 :: SingFunction2 f -> Sing f
$mSLambda2 :: forall r a1 a2 b (f :: a1 ~> (a2 ~> b)).
Sing f -> (SingFunction2 f -> r) -> (Void# -> r) -> r
SLambda2 {Sing f
-> forall (t1 :: a1) (t2 :: a2).
Sing t1 -> Sing t2 -> Sing ((f @@ t1) @@ t2)
applySing2} <- (unSingFun2 -> applySing2)
where SLambda2 SingFunction2 f
lam2 = SingFunction2 f -> Sing f
forall a1 a2 b (f :: a1 ~> (a2 ~> b)). SingFunction2 f -> Sing f
singFun2 SingFunction2 f
lam2
{-# COMPLETE SLambda3 #-}
pattern SLambda3 :: forall f. SingFunction3 f -> Sing f
pattern $bSLambda3 :: SingFunction3 f -> Sing f
$mSLambda3 :: forall r a1 a2 a3 b (f :: a1 ~> (a2 ~> (a3 ~> b))).
Sing f -> (SingFunction3 f -> r) -> (Void# -> r) -> r
SLambda3 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3).
Sing t1 -> Sing t2 -> Sing t3 -> Sing (((f @@ t1) @@ t2) @@ t3)
applySing3} <- (unSingFun3 -> applySing3)
where SLambda3 SingFunction3 f
lam3 = SingFunction3 f -> Sing f
forall a1 a2 a3 b (f :: a1 ~> (a2 ~> (a3 ~> b))).
SingFunction3 f -> Sing f
singFun3 SingFunction3 f
lam3
{-# COMPLETE SLambda4 #-}
pattern SLambda4 :: forall f. SingFunction4 f -> Sing f
pattern $bSLambda4 :: SingFunction4 f -> Sing f
$mSLambda4 :: forall r a1 a2 a3 a4 b (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
Sing f -> (SingFunction4 f -> r) -> (Void# -> r) -> r
SLambda4 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing ((((f @@ t1) @@ t2) @@ t3) @@ t4)
applySing4} <- (unSingFun4 -> applySing4)
where SLambda4 SingFunction4 f
lam4 = SingFunction4 f -> Sing f
forall a1 a2 a3 a4 b (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))).
SingFunction4 f -> Sing f
singFun4 SingFunction4 f
lam4
{-# COMPLETE SLambda5 #-}
pattern SLambda5 :: forall f. SingFunction5 f -> Sing f
pattern $bSLambda5 :: SingFunction5 f -> Sing f
$mSLambda5 :: forall r a1 a2 a3 a4 a5 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
Sing f -> (SingFunction5 f -> r) -> (Void# -> r) -> r
SLambda5 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing (((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5)
applySing5} <- (unSingFun5 -> applySing5)
where SLambda5 SingFunction5 f
lam5 = SingFunction5 f -> Sing f
forall a1 a2 a3 a4 a5 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))).
SingFunction5 f -> Sing f
singFun5 SingFunction5 f
lam5
{-# COMPLETE SLambda6 #-}
pattern SLambda6 :: forall f. SingFunction6 f -> Sing f
pattern $bSLambda6 :: SingFunction6 f -> Sing f
$mSLambda6 :: forall r a1 a2 a3 a4 a5 a6 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
Sing f -> (SingFunction6 f -> r) -> (Void# -> r) -> r
SLambda6 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5)
(t6 :: a6).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing t6
-> Sing ((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6)
applySing6} <- (unSingFun6 -> applySing6)
where SLambda6 SingFunction6 f
lam6 = SingFunction6 f -> Sing f
forall a1 a2 a3 a4 a5 a6 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))).
SingFunction6 f -> Sing f
singFun6 SingFunction6 f
lam6
{-# COMPLETE SLambda7 #-}
pattern SLambda7 :: forall f. SingFunction7 f -> Sing f
pattern $bSLambda7 :: SingFunction7 f -> Sing f
$mSLambda7 :: forall r a1 a2 a3 a4 a5 a6 a7 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))).
Sing f -> (SingFunction7 f -> r) -> (Void# -> r) -> r
SLambda7 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5)
(t6 :: a6) (t7 :: a7).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing t6
-> Sing t7
-> Sing (((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7)
applySing7} <- (unSingFun7 -> applySing7)
where SLambda7 SingFunction7 f
lam7 = SingFunction7 f -> Sing f
forall a1 a2 a3 a4 a5 a6 a7 b
(f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))).
SingFunction7 f -> Sing f
singFun7 SingFunction7 f
lam7
{-# COMPLETE SLambda8 #-}
pattern SLambda8 :: forall f. SingFunction8 f -> Sing f
pattern $bSLambda8 :: SingFunction8 f -> Sing f
$mSLambda8 :: forall r a1 a2 a3 a4 a5 a6 a7 a8 b
(f :: a1
~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))).
Sing f -> (SingFunction8 f -> r) -> (Void# -> r) -> r
SLambda8 {Sing f
-> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5)
(t6 :: a6) (t7 :: a7) (t8 :: a8).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing t6
-> Sing t7
-> Sing t8
-> Sing
((((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7) @@ t8)
applySing8} <- (unSingFun8 -> applySing8)
where SLambda8 SingFunction8 f
lam8 = SingFunction8 f -> Sing f
forall a1 a2 a3 a4 a5 a6 a7 a8 b
(f :: a1
~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))).
SingFunction8 f -> Sing f
singFun8 SingFunction8 f
lam8
withSingI :: Sing n -> (SingI n => r) -> r
withSingI :: Sing n -> (SingI n => r) -> r
withSingI Sing n
sn SingI n => r
r =
case Sing n -> SingInstance n
forall k (a :: k). Sing a -> SingInstance a
singInstance Sing n
sn of
SingInstance n
SingInstance -> r
SingI n => r
r
withSomeSing :: forall k r
. SingKind k
=> Demote k
-> (forall (a :: k). Sing a -> r)
-> r
withSomeSing :: Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k
x forall (a :: k). Sing a -> r
f =
case Demote k -> SomeSing k
forall k. SingKind k => Demote k -> SomeSing k
toSing Demote k
x of
SomeSing Sing a
x' -> Sing a -> r
forall (a :: k). Sing a -> r
f Sing a
x'
withSing :: SingI a => (Sing a -> b) -> b
withSing :: (Sing a -> b) -> b
withSing Sing a -> b
f = Sing a -> b
f Sing a
forall k (a :: k). SingI a => Sing a
sing
singThat :: forall k (a :: k). (SingKind k, SingI a)
=> (Demote k -> Bool) -> Maybe (Sing a)
singThat :: (Demote k -> Bool) -> Maybe (Sing a)
singThat Demote k -> Bool
p = (Sing a -> Maybe (Sing a)) -> Maybe (Sing a)
forall k (a :: k) b. SingI a => (Sing a -> b) -> b
withSing ((Sing a -> Maybe (Sing a)) -> Maybe (Sing a))
-> (Sing a -> Maybe (Sing a)) -> Maybe (Sing a)
forall a b. (a -> b) -> a -> b
$ \Sing a
x -> if Demote k -> Bool
p (Sing a -> Demote k
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a
x) then Sing a -> Maybe (Sing a)
forall a. a -> Maybe a
Just Sing a
x else Maybe (Sing a)
forall a. Maybe a
Nothing
singByProxy :: SingI a => proxy a -> Sing a
singByProxy :: proxy a -> Sing a
singByProxy proxy a
_ = Sing a
forall k (a :: k). SingI a => Sing a
sing
singByProxy# :: SingI a => Proxy# a -> Sing a
singByProxy# :: Proxy# a -> Sing a
singByProxy# Proxy# a
_ = Sing a
forall k (a :: k). SingI a => Sing a
sing
demote :: forall a. (SingKind (KindOf a), SingI a) => Demote (KindOf a)
demote :: Demote (KindOf a)
demote = Sing a -> Demote (KindOf a)
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (SingI a => Sing a
forall k (a :: k). SingI a => Sing a
sing @a)