Singletons/Operators.hs:(0,0)-(0,0): Splicing declarations singletons [d| child :: Foo -> Foo child FLeaf = FLeaf child (a :+: _) = a (+) :: Nat -> Nat -> Nat Zero + m = m (Succ n) + m = Succ (n + m) data Foo where FLeaf :: Foo (:+:) :: Foo -> Foo -> Foo |] ======> data Foo where FLeaf :: Foo (:+:) :: Foo -> Foo -> Foo child :: Foo -> Foo child FLeaf = FLeaf child (a :+: _) = a (+) :: Nat -> Nat -> Nat (+) Zero m = m (+) (Succ n) m = Succ (n + m) type FLeafSym0 = FLeaf type (:+:@#@$$$) (t0123456789876543210 :: Foo) (t0123456789876543210 :: Foo) = (:+:) t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings ((:+:@#@$$) t0123456789876543210) where suppressUnusedWarnings = snd (((,) (::+:@#@$$###)) ()) data (:+:@#@$$) (t0123456789876543210 :: Foo) :: (~>) Foo Foo where (::+:@#@$$###) :: forall t0123456789876543210 t0123456789876543210 arg. SameKind (Apply ((:+:@#@$$) t0123456789876543210) arg) ((:+:@#@$$$) t0123456789876543210 arg) => (:+:@#@$$) t0123456789876543210 t0123456789876543210 type instance Apply ((:+:@#@$$) t0123456789876543210) t0123456789876543210 = (:+:) t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings (:+:@#@$) where suppressUnusedWarnings = snd (((,) (::+:@#@$###)) ()) data (:+:@#@$) :: (~>) Foo ((~>) Foo Foo) where (::+:@#@$###) :: forall t0123456789876543210 arg. SameKind (Apply (:+:@#@$) arg) ((:+:@#@$$) arg) => (:+:@#@$) t0123456789876543210 type instance Apply (:+:@#@$) t0123456789876543210 = (:+:@#@$$) t0123456789876543210 type (+@#@$$$) (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) = (+) a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings ((+@#@$$) a0123456789876543210) where suppressUnusedWarnings = snd (((,) (:+@#@$$###)) ()) data (+@#@$$) (a0123456789876543210 :: Nat) :: (~>) Nat Nat where (:+@#@$$###) :: forall a0123456789876543210 a0123456789876543210 arg. SameKind (Apply ((+@#@$$) a0123456789876543210) arg) ((+@#@$$$) a0123456789876543210 arg) => (+@#@$$) a0123456789876543210 a0123456789876543210 type instance Apply ((+@#@$$) a0123456789876543210) a0123456789876543210 = (+) a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (+@#@$) where suppressUnusedWarnings = snd (((,) (:+@#@$###)) ()) data (+@#@$) :: (~>) Nat ((~>) Nat Nat) where (:+@#@$###) :: forall a0123456789876543210 arg. SameKind (Apply (+@#@$) arg) ((+@#@$$) arg) => (+@#@$) a0123456789876543210 type instance Apply (+@#@$) a0123456789876543210 = (+@#@$$) a0123456789876543210 type ChildSym1 (a0123456789876543210 :: Foo) = Child a0123456789876543210 instance SuppressUnusedWarnings ChildSym0 where suppressUnusedWarnings = snd (((,) ChildSym0KindInference) ()) data ChildSym0 :: (~>) Foo Foo where ChildSym0KindInference :: forall a0123456789876543210 arg. SameKind (Apply ChildSym0 arg) (ChildSym1 arg) => ChildSym0 a0123456789876543210 type instance Apply ChildSym0 a0123456789876543210 = Child a0123456789876543210 type family (+) (a :: Nat) (a :: Nat) :: Nat where (+) 'Zero m = m (+) ( 'Succ n) m = Apply SuccSym0 (Apply (Apply (+@#@$) n) m) type family Child (a :: Foo) :: Foo where Child FLeaf = FLeafSym0 Child ((:+:) a _) = a (%+) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t :: Nat) sChild :: forall (t :: Foo). Sing t -> Sing (Apply ChildSym0 t :: Foo) (%+) SZero (sM :: Sing m) = sM (%+) (SSucc (sN :: Sing n)) (sM :: Sing m) = (applySing ((singFun1 @SuccSym0) SSucc)) ((applySing ((applySing ((singFun2 @(+@#@$)) (%+))) sN)) sM) sChild SFLeaf = SFLeaf sChild ((:%+:) (sA :: Sing a) _) = sA instance SingI ((+@#@$) :: (~>) Nat ((~>) Nat Nat)) where sing = (singFun2 @(+@#@$)) (%+) instance SingI d => SingI ((+@#@$$) (d :: Nat) :: (~>) Nat Nat) where sing = (singFun1 @((+@#@$$) (d :: Nat))) ((%+) (sing @d)) instance SingI (ChildSym0 :: (~>) Foo Foo) where sing = (singFun1 @ChildSym0) sChild data instance Sing :: Foo -> GHC.Types.Type where SFLeaf :: Sing FLeaf (:%+:) :: forall (n :: Foo) (n :: Foo). (Sing (n :: Foo)) -> (Sing (n :: Foo)) -> Sing ((:+:) n n) type SFoo = (Sing :: Foo -> GHC.Types.Type) instance SingKind Foo where type Demote Foo = Foo fromSing SFLeaf = FLeaf fromSing ((:%+:) b b) = ((:+:) (fromSing b)) (fromSing b) toSing FLeaf = SomeSing SFLeaf toSing ((:+:) (b :: Demote Foo) (b :: Demote Foo)) = case ((,) (toSing b :: SomeSing Foo)) (toSing b :: SomeSing Foo) of { (,) (SomeSing c) (SomeSing c) -> SomeSing (((:%+:) c) c) } instance SingI FLeaf where sing = SFLeaf instance (SingI n, SingI n) => SingI ((:+:) (n :: Foo) (n :: Foo)) where sing = ((:%+:) sing) sing instance SingI ((:+:@#@$) :: (~>) Foo ((~>) Foo Foo)) where sing = (singFun2 @(:+:@#@$)) (:%+:) instance SingI (TyCon2 (:+:) :: (~>) Foo ((~>) Foo Foo)) where sing = (singFun2 @(TyCon2 (:+:))) (:%+:) instance SingI d => SingI ((:+:@#@$$) (d :: Foo) :: (~>) Foo Foo) where sing = (singFun1 @((:+:@#@$$) (d :: Foo))) ((:%+:) (sing @d)) instance SingI d => SingI (TyCon1 ((:+:) (d :: Foo)) :: (~>) Foo Foo) where sing = (singFun1 @(TyCon1 ((:+:) (d :: Foo)))) ((:%+:) (sing @d))