singletons-base-3.4: tests/compile-and-dump/Singletons/T150.golden
Singletons/T150.hs:(0,0)-(0,0): Splicing declarations
withOptions defaultOptions {genSingKindInsts = False}
$ singletons
$ lift
[d| headVec :: Vec (Succ n) a -> a
headVec (VCons x _) = x
tailVec :: Vec (Succ n) a -> Vec n a
tailVec (VCons _ xs) = xs
(!) :: Vec n a -> Fin n -> a
VCons x _ ! FZ = x
VCons _ xs ! FS n = xs ! n
VNil ! n = case n of {}
mapVec :: (a -> b) -> Vec n a -> Vec n b
mapVec _ VNil = VNil
mapVec f (VCons x xs) = VCons (f x) (mapVec f xs)
symmetry :: Equal a b -> Equal b a
symmetry Reflexive = Reflexive
transitivity :: Equal a b -> Equal b c -> Equal a c
transitivity Reflexive Reflexive = Reflexive
data Fin :: Nat -> Type
where
FZ :: Fin (Succ n)
FS :: Fin n -> Fin (Succ n)
data Foo :: Type -> Type
where
MkFoo1 :: Foo Bool
MkFoo2 :: Foo Ordering
data Vec :: Nat -> Type -> Type
where
VNil :: Vec Zero a
VCons :: a -> Vec n a -> Vec (Succ n) a
data Equal :: Type -> Type -> Type where Reflexive :: Equal a a
data HList :: [Type] -> Type
where
HNil :: HList '[]
HCons :: x -> HList xs -> HList (x : xs)
data Obj :: Type where Obj :: a -> Obj |]
======>
data Fin :: Nat -> Type
where
FZ :: Fin ('Succ n)
FS :: (Fin n) -> Fin ('Succ n)
data Foo :: Type -> Type
where
MkFoo1 :: Foo Bool
MkFoo2 :: Foo Ordering
data Vec :: Nat -> Type -> Type
where
VNil :: Vec 'Zero a
VCons :: a -> (Vec n a) -> Vec ('Succ n) a
headVec :: Vec ('Succ n) a -> a
headVec (VCons x _) = x
tailVec :: Vec ('Succ n) a -> Vec n a
tailVec (VCons _ xs) = xs
(!) :: Vec n a -> Fin n -> a
(!) (VCons x _) FZ = x
(!) (VCons _ xs) (FS n) = (xs ! n)
(!) VNil n = case n of {}
mapVec :: (a -> b) -> Vec n a -> Vec n b
mapVec _ VNil = VNil
mapVec f (VCons x xs) = VCons (f x) (mapVec f xs)
data Equal :: Type -> Type -> Type where Reflexive :: Equal a a
symmetry :: Equal a b -> Equal b a
symmetry Reflexive = Reflexive
transitivity :: Equal a b -> Equal b c -> Equal a c
transitivity Reflexive Reflexive = Reflexive
data HList :: [Type] -> Type
where
HNil :: HList '[]
HCons :: x -> (HList xs) -> HList ('(:) x xs)
data Obj :: Type where Obj :: a -> Obj
type FZSym0 :: Fin ('Succ n)
type family FZSym0 @n :: Fin ('Succ n) where
FZSym0 = FZ
type FSSym0 :: (~>) (Fin n) (Fin ('Succ n))
data FSSym0 :: (~>) (Fin n) (Fin ('Succ n))
where
FSSym0KindInference :: SameKind (Apply FSSym0 arg) (FSSym1 arg) =>
FSSym0 a0123456789876543210
type instance Apply FSSym0 a0123456789876543210 = FS a0123456789876543210
instance SuppressUnusedWarnings FSSym0 where
suppressUnusedWarnings = snd ((,) FSSym0KindInference ())
type FSSym1 :: Fin n -> Fin ('Succ n)
type family FSSym1 @n (a0123456789876543210 :: Fin n) :: Fin ('Succ n) where
FSSym1 a0123456789876543210 = FS a0123456789876543210
type MkFoo1Sym0 :: Foo Bool
type family MkFoo1Sym0 :: Foo Bool where
MkFoo1Sym0 = MkFoo1
type MkFoo2Sym0 :: Foo Ordering
type family MkFoo2Sym0 :: Foo Ordering where
MkFoo2Sym0 = MkFoo2
type VNilSym0 :: Vec 'Zero a
type family VNilSym0 @a :: Vec 'Zero a where
VNilSym0 = VNil
type VConsSym0 :: (~>) a ((~>) (Vec n a) (Vec ('Succ n) a))
data VConsSym0 :: (~>) a ((~>) (Vec n a) (Vec ('Succ n) a))
where
VConsSym0KindInference :: SameKind (Apply VConsSym0 arg) (VConsSym1 arg) =>
VConsSym0 a0123456789876543210
type instance Apply VConsSym0 a0123456789876543210 = VConsSym1 a0123456789876543210
instance SuppressUnusedWarnings VConsSym0 where
suppressUnusedWarnings = snd ((,) VConsSym0KindInference ())
type VConsSym1 :: a -> (~>) (Vec n a) (Vec ('Succ n) a)
data VConsSym1 (a0123456789876543210 :: a) :: (~>) (Vec n a) (Vec ('Succ n) a)
where
VConsSym1KindInference :: SameKind (Apply (VConsSym1 a0123456789876543210) arg) (VConsSym2 a0123456789876543210 arg) =>
VConsSym1 a0123456789876543210 a0123456789876543210
type instance Apply (VConsSym1 a0123456789876543210) a0123456789876543210 = VCons a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (VConsSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) VConsSym1KindInference ())
type VConsSym2 :: a -> Vec n a -> Vec ('Succ n) a
type family VConsSym2 @a @n (a0123456789876543210 :: a) (a0123456789876543210 :: Vec n a) :: Vec ('Succ n) a where
VConsSym2 a0123456789876543210 a0123456789876543210 = VCons a0123456789876543210 a0123456789876543210
type ReflexiveSym0 :: Equal a a
type family ReflexiveSym0 @a :: Equal a a where
ReflexiveSym0 = Reflexive
type HNilSym0 :: HList '[]
type family HNilSym0 :: HList '[] where
HNilSym0 = HNil
type HConsSym0 :: (~>) x ((~>) (HList xs) (HList ('(:) x xs)))
data HConsSym0 :: (~>) x ((~>) (HList xs) (HList ('(:) x xs)))
where
HConsSym0KindInference :: SameKind (Apply HConsSym0 arg) (HConsSym1 arg) =>
HConsSym0 a0123456789876543210
type instance Apply HConsSym0 a0123456789876543210 = HConsSym1 a0123456789876543210
instance SuppressUnusedWarnings HConsSym0 where
suppressUnusedWarnings = snd ((,) HConsSym0KindInference ())
type HConsSym1 :: x -> (~>) (HList xs) (HList ('(:) x xs))
data HConsSym1 (a0123456789876543210 :: x) :: (~>) (HList xs) (HList ('(:) x xs))
where
HConsSym1KindInference :: SameKind (Apply (HConsSym1 a0123456789876543210) arg) (HConsSym2 a0123456789876543210 arg) =>
HConsSym1 a0123456789876543210 a0123456789876543210
type instance Apply (HConsSym1 a0123456789876543210) a0123456789876543210 = HCons a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (HConsSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) HConsSym1KindInference ())
type HConsSym2 :: x -> HList xs -> HList ('(:) x xs)
type family HConsSym2 @x @xs (a0123456789876543210 :: x) (a0123456789876543210 :: HList xs) :: HList ('(:) x xs) where
HConsSym2 a0123456789876543210 a0123456789876543210 = HCons a0123456789876543210 a0123456789876543210
type ObjSym0 :: (~>) a Obj
data ObjSym0 :: (~>) a Obj
where
ObjSym0KindInference :: SameKind (Apply ObjSym0 arg) (ObjSym1 arg) =>
ObjSym0 a0123456789876543210
type instance Apply ObjSym0 a0123456789876543210 = Obj a0123456789876543210
instance SuppressUnusedWarnings ObjSym0 where
suppressUnusedWarnings = snd ((,) ObjSym0KindInference ())
type ObjSym1 :: a -> Obj
type family ObjSym1 @a (a0123456789876543210 :: a) :: Obj where
ObjSym1 a0123456789876543210 = Obj a0123456789876543210
type family Case_0123456789876543210 n0123456789876543210 t where
type TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c))
data TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c))
where
TransitivitySym0KindInference :: SameKind (Apply TransitivitySym0 arg) (TransitivitySym1 arg) =>
TransitivitySym0 a0123456789876543210
type instance Apply TransitivitySym0 a0123456789876543210 = TransitivitySym1 a0123456789876543210
instance SuppressUnusedWarnings TransitivitySym0 where
suppressUnusedWarnings = snd ((,) TransitivitySym0KindInference ())
type TransitivitySym1 :: Equal a b -> (~>) (Equal b c) (Equal a c)
data TransitivitySym1 (a0123456789876543210 :: Equal a b) :: (~>) (Equal b c) (Equal a c)
where
TransitivitySym1KindInference :: SameKind (Apply (TransitivitySym1 a0123456789876543210) arg) (TransitivitySym2 a0123456789876543210 arg) =>
TransitivitySym1 a0123456789876543210 a0123456789876543210
type instance Apply (TransitivitySym1 a0123456789876543210) a0123456789876543210 = Transitivity a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (TransitivitySym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) TransitivitySym1KindInference ())
type TransitivitySym2 :: Equal a b -> Equal b c -> Equal a c
type family TransitivitySym2 @a @b @c (a0123456789876543210 :: Equal a b) (a0123456789876543210 :: Equal b c) :: Equal a c where
TransitivitySym2 a0123456789876543210 a0123456789876543210 = Transitivity a0123456789876543210 a0123456789876543210
type SymmetrySym0 :: (~>) (Equal a b) (Equal b a)
data SymmetrySym0 :: (~>) (Equal a b) (Equal b a)
where
SymmetrySym0KindInference :: SameKind (Apply SymmetrySym0 arg) (SymmetrySym1 arg) =>
SymmetrySym0 a0123456789876543210
type instance Apply SymmetrySym0 a0123456789876543210 = Symmetry a0123456789876543210
instance SuppressUnusedWarnings SymmetrySym0 where
suppressUnusedWarnings = snd ((,) SymmetrySym0KindInference ())
type SymmetrySym1 :: Equal a b -> Equal b a
type family SymmetrySym1 @a @b (a0123456789876543210 :: Equal a b) :: Equal b a where
SymmetrySym1 a0123456789876543210 = Symmetry a0123456789876543210
type MapVecSym0 :: (~>) ((~>) a b) ((~>) (Vec n a) (Vec n b))
data MapVecSym0 :: (~>) ((~>) a b) ((~>) (Vec n a) (Vec n b))
where
MapVecSym0KindInference :: SameKind (Apply MapVecSym0 arg) (MapVecSym1 arg) =>
MapVecSym0 a0123456789876543210
type instance Apply MapVecSym0 a0123456789876543210 = MapVecSym1 a0123456789876543210
instance SuppressUnusedWarnings MapVecSym0 where
suppressUnusedWarnings = snd ((,) MapVecSym0KindInference ())
type MapVecSym1 :: (~>) a b -> (~>) (Vec n a) (Vec n b)
data MapVecSym1 (a0123456789876543210 :: (~>) a b) :: (~>) (Vec n a) (Vec n b)
where
MapVecSym1KindInference :: SameKind (Apply (MapVecSym1 a0123456789876543210) arg) (MapVecSym2 a0123456789876543210 arg) =>
MapVecSym1 a0123456789876543210 a0123456789876543210
type instance Apply (MapVecSym1 a0123456789876543210) a0123456789876543210 = MapVec a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (MapVecSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) MapVecSym1KindInference ())
type MapVecSym2 :: (~>) a b -> Vec n a -> Vec n b
type family MapVecSym2 @a @b @n (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Vec n a) :: Vec n b where
MapVecSym2 a0123456789876543210 a0123456789876543210 = MapVec a0123456789876543210 a0123456789876543210
type (!@#@$) :: (~>) (Vec n a) ((~>) (Fin n) a)
data (!@#@$) :: (~>) (Vec n a) ((~>) (Fin n) a)
where
(:!@#@$###) :: SameKind (Apply (!@#@$) arg) ((!@#@$$) arg) =>
(!@#@$) a0123456789876543210
type instance Apply (!@#@$) a0123456789876543210 = (!@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (!@#@$) where
suppressUnusedWarnings = snd ((,) (:!@#@$###) ())
type (!@#@$$) :: Vec n a -> (~>) (Fin n) a
data (!@#@$$) (a0123456789876543210 :: Vec n a) :: (~>) (Fin n) a
where
(:!@#@$$###) :: SameKind (Apply ((!@#@$$) a0123456789876543210) arg) ((!@#@$$$) a0123456789876543210 arg) =>
(!@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply ((!@#@$$) a0123456789876543210) a0123456789876543210 = (!) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((!@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd ((,) (:!@#@$$###) ())
type (!@#@$$$) :: Vec n a -> Fin n -> a
type family (!@#@$$$) @n @a (a0123456789876543210 :: Vec n a) (a0123456789876543210 :: Fin n) :: a where
(!@#@$$$) a0123456789876543210 a0123456789876543210 = (!) a0123456789876543210 a0123456789876543210
type TailVecSym0 :: (~>) (Vec ('Succ n) a) (Vec n a)
data TailVecSym0 :: (~>) (Vec ('Succ n) a) (Vec n a)
where
TailVecSym0KindInference :: SameKind (Apply TailVecSym0 arg) (TailVecSym1 arg) =>
TailVecSym0 a0123456789876543210
type instance Apply TailVecSym0 a0123456789876543210 = TailVec a0123456789876543210
instance SuppressUnusedWarnings TailVecSym0 where
suppressUnusedWarnings = snd ((,) TailVecSym0KindInference ())
type TailVecSym1 :: Vec ('Succ n) a -> Vec n a
type family TailVecSym1 @n @a (a0123456789876543210 :: Vec ('Succ n) a) :: Vec n a where
TailVecSym1 a0123456789876543210 = TailVec a0123456789876543210
type HeadVecSym0 :: (~>) (Vec ('Succ n) a) a
data HeadVecSym0 :: (~>) (Vec ('Succ n) a) a
where
HeadVecSym0KindInference :: SameKind (Apply HeadVecSym0 arg) (HeadVecSym1 arg) =>
HeadVecSym0 a0123456789876543210
type instance Apply HeadVecSym0 a0123456789876543210 = HeadVec a0123456789876543210
instance SuppressUnusedWarnings HeadVecSym0 where
suppressUnusedWarnings = snd ((,) HeadVecSym0KindInference ())
type HeadVecSym1 :: Vec ('Succ n) a -> a
type family HeadVecSym1 @n @a (a0123456789876543210 :: Vec ('Succ n) a) :: a where
HeadVecSym1 a0123456789876543210 = HeadVec a0123456789876543210
type Transitivity :: Equal a b -> Equal b c -> Equal a c
type family Transitivity @a @b @c (a :: Equal a b) (a :: Equal b c) :: Equal a c where
Transitivity Reflexive Reflexive = ReflexiveSym0
type Symmetry :: Equal a b -> Equal b a
type family Symmetry @a @b (a :: Equal a b) :: Equal b a where
Symmetry Reflexive = ReflexiveSym0
type MapVec :: (~>) a b -> Vec n a -> Vec n b
type family MapVec @a @b @n (a :: (~>) a b) (a :: Vec n a) :: Vec n b where
MapVec _ VNil = VNilSym0
MapVec f (VCons x xs) = Apply (Apply VConsSym0 (Apply f x)) (Apply (Apply MapVecSym0 f) xs)
type (!) :: Vec n a -> Fin n -> a
type family (!) @n @a (a :: Vec n a) (a :: Fin n) :: a where
(!) (VCons x _) FZ = x
(!) (VCons _ xs) (FS n) = Apply (Apply (!@#@$) xs) n
(!) VNil n = Case_0123456789876543210 n n
type TailVec :: Vec ('Succ n) a -> Vec n a
type family TailVec @n @a (a :: Vec ('Succ n) a) :: Vec n a where
TailVec (VCons _ xs) = xs
type HeadVec :: Vec ('Succ n) a -> a
type family HeadVec @n @a (a :: Vec ('Succ n) a) :: a where
HeadVec (VCons x _) = x
sTransitivity ::
(forall (t :: Equal a b) (t :: Equal b c).
Sing t
-> Sing t
-> Sing (Apply (Apply TransitivitySym0 t) t :: Equal a c) :: Type)
sSymmetry ::
(forall (t :: Equal a b).
Sing t -> Sing (Apply SymmetrySym0 t :: Equal b a) :: Type)
sMapVec ::
(forall (t :: (~>) a b) (t :: Vec n a).
Sing t
-> Sing t
-> Sing (Apply (Apply MapVecSym0 t) t :: Vec n b) :: Type)
(%!) ::
(forall (t :: Vec n a) (t :: Fin n).
Sing t -> Sing t -> Sing (Apply (Apply (!@#@$) t) t :: a) :: Type)
sTailVec ::
(forall (t :: Vec ('Succ n) a).
Sing t -> Sing (Apply TailVecSym0 t :: Vec n a) :: Type)
sHeadVec ::
(forall (t :: Vec ('Succ n) a).
Sing t -> Sing (Apply HeadVecSym0 t :: a) :: Type)
sTransitivity SReflexive SReflexive = SReflexive
sSymmetry SReflexive = SReflexive
sMapVec _ SVNil = SVNil
sMapVec (sF :: Sing f) (SVCons (sX :: Sing x) (sXs :: Sing xs))
= applySing
(applySing (singFun2 @VConsSym0 SVCons) (applySing sF sX))
(applySing (applySing (singFun2 @MapVecSym0 sMapVec) sF) sXs)
(%!) (SVCons (sX :: Sing x) _) SFZ = sX
(%!) (SVCons _ (sXs :: Sing xs)) (SFS (sN :: Sing n))
= applySing (applySing (singFun2 @(!@#@$) (%!)) sXs) sN
(%!) SVNil (sN :: Sing n)
= id @(Sing (Case_0123456789876543210 n n)) (case sN of {})
sTailVec (SVCons _ (sXs :: Sing xs)) = sXs
sHeadVec (SVCons (sX :: Sing x) _) = sX
instance SingI (TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c))) where
sing = singFun2 @TransitivitySym0 sTransitivity
instance SingI d =>
SingI (TransitivitySym1 (d :: Equal a b) :: (~>) (Equal b c) (Equal a c)) where
sing
= singFun1
@(TransitivitySym1 (d :: Equal a b)) (sTransitivity (sing @d))
instance SingI1 (TransitivitySym1 :: Equal a b
-> (~>) (Equal b c) (Equal a c)) where
liftSing (s :: Sing (d :: Equal a b))
= singFun1 @(TransitivitySym1 (d :: Equal a b)) (sTransitivity s)
instance SingI (SymmetrySym0 :: (~>) (Equal a b) (Equal b a)) where
sing = singFun1 @SymmetrySym0 sSymmetry
instance SingI (MapVecSym0 :: (~>) ((~>) a b) ((~>) (Vec n a) (Vec n b))) where
sing = singFun2 @MapVecSym0 sMapVec
instance SingI d =>
SingI (MapVecSym1 (d :: (~>) a b) :: (~>) (Vec n a) (Vec n b)) where
sing = singFun1 @(MapVecSym1 (d :: (~>) a b)) (sMapVec (sing @d))
instance SingI1 (MapVecSym1 :: (~>) a b
-> (~>) (Vec n a) (Vec n b)) where
liftSing (s :: Sing (d :: (~>) a b))
= singFun1 @(MapVecSym1 (d :: (~>) a b)) (sMapVec s)
instance SingI ((!@#@$) :: (~>) (Vec n a) ((~>) (Fin n) a)) where
sing = singFun2 @(!@#@$) (%!)
instance SingI d =>
SingI ((!@#@$$) (d :: Vec n a) :: (~>) (Fin n) a) where
sing = singFun1 @((!@#@$$) (d :: Vec n a)) ((%!) (sing @d))
instance SingI1 ((!@#@$$) :: Vec n a -> (~>) (Fin n) a) where
liftSing (s :: Sing (d :: Vec n a))
= singFun1 @((!@#@$$) (d :: Vec n a)) ((%!) s)
instance SingI (TailVecSym0 :: (~>) (Vec ('Succ n) a) (Vec n a)) where
sing = singFun1 @TailVecSym0 sTailVec
instance SingI (HeadVecSym0 :: (~>) (Vec ('Succ n) a) a) where
sing = singFun1 @HeadVecSym0 sHeadVec
data SFin :: forall (a :: Nat). Fin a -> Type
where
SFZ :: forall n. SFin (FZ :: Fin ('Succ n))
SFS :: forall n (n :: Fin n).
(Sing n) -> SFin (FS n :: Fin ('Succ n))
type instance Sing @(Fin a) = SFin
data SFoo :: forall (a :: Type). Foo a -> Type
where
SMkFoo1 :: SFoo (MkFoo1 :: Foo Bool)
SMkFoo2 :: SFoo (MkFoo2 :: Foo Ordering)
type instance Sing @(Foo a) = SFoo
data SVec :: forall (a :: Nat) (a :: Type). Vec a a -> Type
where
SVNil :: forall a. SVec (VNil :: Vec 'Zero a)
SVCons :: forall a n (n :: a) (n :: Vec n a).
(Sing n) -> (Sing n) -> SVec (VCons n n :: Vec ('Succ n) a)
type instance Sing @(Vec a a) = SVec
data SEqual :: forall (a :: Type) (a :: Type). Equal a a -> Type
where SReflexive :: forall a. SEqual (Reflexive :: Equal a a)
type instance Sing @(Equal a a) = SEqual
data SHList :: forall (a :: [Type]). HList a -> Type
where
SHNil :: SHList (HNil :: HList '[])
SHCons :: forall x xs (n :: x) (n :: HList xs).
(Sing n) -> (Sing n) -> SHList (HCons n n :: HList ('(:) x xs))
type instance Sing @(HList a) = SHList
data SObj :: Obj -> Type
where SObj :: forall a (n :: a). (Sing n) -> SObj (Obj n :: Obj)
type instance Sing @Obj = SObj
instance SingI FZ where
sing = SFZ
instance SingI n => SingI (FS (n :: Fin n)) where
sing = SFS sing
instance SingI1 FS where
liftSing = SFS
instance SingI (FSSym0 :: (~>) (Fin n) (Fin ('Succ n))) where
sing = singFun1 @FSSym0 SFS
instance SingI MkFoo1 where
sing = SMkFoo1
instance SingI MkFoo2 where
sing = SMkFoo2
instance SingI VNil where
sing = SVNil
instance (SingI n, SingI n) =>
SingI (VCons (n :: a) (n :: Vec n a)) where
sing = SVCons sing sing
instance SingI n => SingI1 (VCons (n :: a)) where
liftSing = SVCons sing
instance SingI2 VCons where
liftSing2 = SVCons
instance SingI (VConsSym0 :: (~>) a ((~>) (Vec n a) (Vec ('Succ n) a))) where
sing = singFun2 @VConsSym0 SVCons
instance SingI d =>
SingI (VConsSym1 (d :: a) :: (~>) (Vec n a) (Vec ('Succ n) a)) where
sing = singFun1 @(VConsSym1 (d :: a)) (SVCons (sing @d))
instance SingI1 (VConsSym1 :: a
-> (~>) (Vec n a) (Vec ('Succ n) a)) where
liftSing (s :: Sing (d :: a))
= singFun1 @(VConsSym1 (d :: a)) (SVCons s)
instance SingI Reflexive where
sing = SReflexive
instance SingI HNil where
sing = SHNil
instance (SingI n, SingI n) =>
SingI (HCons (n :: x) (n :: HList xs)) where
sing = SHCons sing sing
instance SingI n => SingI1 (HCons (n :: x)) where
liftSing = SHCons sing
instance SingI2 HCons where
liftSing2 = SHCons
instance SingI (HConsSym0 :: (~>) x ((~>) (HList xs) (HList ('(:) x xs)))) where
sing = singFun2 @HConsSym0 SHCons
instance SingI d =>
SingI (HConsSym1 (d :: x) :: (~>) (HList xs) (HList ('(:) x xs))) where
sing = singFun1 @(HConsSym1 (d :: x)) (SHCons (sing @d))
instance SingI1 (HConsSym1 :: x
-> (~>) (HList xs) (HList ('(:) x xs))) where
liftSing (s :: Sing (d :: x))
= singFun1 @(HConsSym1 (d :: x)) (SHCons s)
instance SingI n => SingI (Obj (n :: a)) where
sing = SObj sing
instance SingI1 Obj where
liftSing = SObj
instance SingI (ObjSym0 :: (~>) a Obj) where
sing = singFun1 @ObjSym0 SObj