singletons-base-3.0: 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 :: 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 (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 :: 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 (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 :: 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 (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 (a0123456789876543210 :: a) :: Obj where
ObjSym1 a0123456789876543210 = Obj a0123456789876543210
type family Case_0123456789876543210 n 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 (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 (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 (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 (!@#@$$$) (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 (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 (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 :: 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 :: Equal a b) :: Equal b a where
Symmetry Reflexive = ReflexiveSym0
type MapVec :: (~>) a b -> Vec n a -> Vec n b
type family MapVec (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 (!) (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 (a :: Vec ('Succ n) a) :: Vec n a where
TailVec (VCons _ xs) = xs
type HeadVec :: Vec ('Succ n) a -> a
type family HeadVec (a :: Vec ('Succ n) a) :: a where
HeadVec (VCons x _) = x
sTransitivity ::
forall a b c (t :: Equal a b) (t :: Equal b c).
Sing t
-> Sing t -> Sing (Apply (Apply TransitivitySym0 t) t :: Equal a c)
sSymmetry ::
forall a b (t :: Equal a b).
Sing t -> Sing (Apply SymmetrySym0 t :: Equal b a)
sMapVec ::
forall a b n (t :: (~>) a b) (t :: Vec n a).
Sing t -> Sing t -> Sing (Apply (Apply MapVecSym0 t) t :: Vec n b)
(%!) ::
forall n a (t :: Vec n a) (t :: Fin n).
Sing t -> Sing t -> Sing (Apply (Apply (!@#@$) t) t :: a)
sTailVec ::
forall n a (t :: Vec ('Succ n) a).
Sing t -> Sing (Apply TailVecSym0 t :: Vec n a)
sHeadVec ::
forall n a (t :: Vec ('Succ n) a).
Sing t -> Sing (Apply HeadVecSym0 t :: a)
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 :: a))) (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 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 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 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 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 (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 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 (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 SingI n => SingI (Obj (n :: a)) where
sing = SObj sing
instance SingI (ObjSym0 :: (~>) a Obj) where
sing = (singFun1 @ObjSym0) SObj