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 (:+:$$$) (t :: Foo) (t :: Foo) = (:+:) t t instance SuppressUnusedWarnings (:+:$$) where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) (:+:$$###)) GHC.Tuple.()) data (:+:$$) (l :: Foo) (l :: TyFun Foo Foo) = forall arg. SameKind (Apply ((:+:$$) l) arg) ((:+:$$$) l arg) => (:+:$$###) type instance Apply ((:+:$$) l) l = (:+:) l l instance SuppressUnusedWarnings (:+:$) where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) (:+:$###)) GHC.Tuple.()) data (:+:$) (l :: TyFun Foo (TyFun Foo Foo -> GHC.Types.Type)) = forall arg. SameKind (Apply (:+:$) arg) ((:+:$$) arg) => (:+:$###) type instance Apply (:+:$) l = (:+:$$) l type (:+$$$) (t :: Nat) (t :: Nat) = (:+) t t instance SuppressUnusedWarnings (:+$$) where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) (:+$$###)) GHC.Tuple.()) data (:+$$) (l :: Nat) (l :: TyFun Nat Nat) = forall arg. SameKind (Apply ((:+$$) l) arg) ((:+$$$) l arg) => (:+$$###) type instance Apply ((:+$$) l) l = (:+) l l instance SuppressUnusedWarnings (:+$) where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) (:+$###)) GHC.Tuple.()) data (:+$) (l :: TyFun Nat (TyFun Nat Nat -> GHC.Types.Type)) = forall arg. SameKind (Apply (:+$) arg) ((:+$$) arg) => (:+$###) type instance Apply (:+$) l = (:+$$) l type ChildSym1 (t :: Foo) = Child t instance SuppressUnusedWarnings ChildSym0 where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) ChildSym0KindInference) GHC.Tuple.()) data ChildSym0 (l :: TyFun Foo Foo) = forall arg. SameKind (Apply ChildSym0 arg) (ChildSym1 arg) => ChildSym0KindInference type instance Apply ChildSym0 l = Child l 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 _z_0123456789876543210) = 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 data instance Sing (z :: Foo) = z ~ FLeaf => SFLeaf | forall (n :: Foo) (n :: Foo). z ~ (:+:) n n => (:%+:) (Sing (n :: Foo)) (Sing (n :: Foo)) 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 b) = case (GHC.Tuple.(,) (toSing b :: SomeSing Foo)) (toSing b :: SomeSing Foo) of { GHC.Tuple.(,) (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