Singletons/ReturnFunc.hs:(0,0)-(0,0): Splicing declarations singletons [d| returnFunc :: Nat -> Nat -> Nat returnFunc _ = Succ id :: a -> a id x = x idFoo :: c -> a -> a idFoo _ = id |] ======> returnFunc :: Nat -> Nat -> Nat returnFunc _ = Succ id :: a -> a id x = x idFoo :: c -> a -> a idFoo _ = id type IdSym1 (t :: a0123456789876543210) = Id t instance SuppressUnusedWarnings IdSym0 where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) IdSym0KindInference) GHC.Tuple.()) data IdSym0 (l :: TyFun a0123456789876543210 a0123456789876543210) = forall arg. SameKind (Apply IdSym0 arg) (IdSym1 arg) => IdSym0KindInference type instance Apply IdSym0 l = Id l type IdFooSym2 (t :: c0123456789876543210) (t :: a0123456789876543210) = IdFoo t t instance SuppressUnusedWarnings IdFooSym1 where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) IdFooSym1KindInference) GHC.Tuple.()) data IdFooSym1 (l :: c0123456789876543210) (l :: TyFun a0123456789876543210 a0123456789876543210) = forall arg. SameKind (Apply (IdFooSym1 l) arg) (IdFooSym2 l arg) => IdFooSym1KindInference type instance Apply (IdFooSym1 l) l = IdFoo l l instance SuppressUnusedWarnings IdFooSym0 where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) IdFooSym0KindInference) GHC.Tuple.()) data IdFooSym0 (l :: TyFun c0123456789876543210 (TyFun a0123456789876543210 a0123456789876543210 -> GHC.Types.Type)) = forall arg. SameKind (Apply IdFooSym0 arg) (IdFooSym1 arg) => IdFooSym0KindInference type instance Apply IdFooSym0 l = IdFooSym1 l type ReturnFuncSym2 (t :: Nat) (t :: Nat) = ReturnFunc t t instance SuppressUnusedWarnings ReturnFuncSym1 where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) ReturnFuncSym1KindInference) GHC.Tuple.()) data ReturnFuncSym1 (l :: Nat) (l :: TyFun Nat Nat) = forall arg. SameKind (Apply (ReturnFuncSym1 l) arg) (ReturnFuncSym2 l arg) => ReturnFuncSym1KindInference type instance Apply (ReturnFuncSym1 l) l = ReturnFunc l l instance SuppressUnusedWarnings ReturnFuncSym0 where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) ReturnFuncSym0KindInference) GHC.Tuple.()) data ReturnFuncSym0 (l :: TyFun Nat (TyFun Nat Nat -> GHC.Types.Type)) = forall arg. SameKind (Apply ReturnFuncSym0 arg) (ReturnFuncSym1 arg) => ReturnFuncSym0KindInference type instance Apply ReturnFuncSym0 l = ReturnFuncSym1 l type family Id (a :: a) :: a where Id x = x type family IdFoo (a :: c) (a :: a) :: a where IdFoo _z_0123456789876543210 a_0123456789876543210 = Apply IdSym0 a_0123456789876543210 type family ReturnFunc (a :: Nat) (a :: Nat) :: Nat where ReturnFunc _z_0123456789876543210 a_0123456789876543210 = Apply SuccSym0 a_0123456789876543210 sId :: forall (t :: a). Sing t -> Sing (Apply IdSym0 t :: a) sIdFoo :: forall (t :: c) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply IdFooSym0 t) t :: a) sReturnFunc :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply ReturnFuncSym0 t) t :: Nat) sId (sX :: Sing x) = sX sIdFoo _ (sA_0123456789876543210 :: Sing a_0123456789876543210) = (applySing ((singFun1 @IdSym0) sId)) sA_0123456789876543210 sReturnFunc _ (sA_0123456789876543210 :: Sing a_0123456789876543210) = (applySing ((singFun1 @SuccSym0) SSucc)) sA_0123456789876543210