Singletons/FunDeps.hs:(0,0)-(0,0): Splicing declarations singletons [d| t1 = meth True class FD a b | a -> b where meth :: a -> a l2r :: a -> b instance FD Bool Nat where meth = not l2r False = 0 l2r True = 1 |] ======> class FD a b | a -> b where meth :: a -> a l2r :: a -> b instance FD Bool Nat where meth = not l2r False = 0 l2r True = 1 t1 = meth True type T1Sym0 = T1 type family T1 where T1 = Apply MethSym0 TrueSym0 type MethSym1 (t :: a0123456789876543210) = Meth t instance SuppressUnusedWarnings MethSym0 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) MethSym0KindInference) GHC.Tuple.()) data MethSym0 (l :: TyFun a0123456789876543210 a0123456789876543210) = forall arg. SameKind (Apply MethSym0 arg) (MethSym1 arg) => MethSym0KindInference type instance Apply MethSym0 l = Meth l type L2rSym1 (t :: a0123456789876543210) = L2r t instance SuppressUnusedWarnings L2rSym0 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) L2rSym0KindInference) GHC.Tuple.()) data L2rSym0 (l :: TyFun a0123456789876543210 b0123456789876543210) = forall arg. SameKind (Apply L2rSym0 arg) (L2rSym1 arg) => L2rSym0KindInference type instance Apply L2rSym0 l = L2r l class PFD (a :: GHC.Types.Type) (b :: GHC.Types.Type) | a -> b where type Meth (arg :: a) :: a type L2r (arg :: a) :: b type family Meth_0123456789876543210 (a :: Bool) :: Bool where Meth_0123456789876543210 a_0123456789876543210 = Apply NotSym0 a_0123456789876543210 type Meth_0123456789876543210Sym1 (t :: Bool) = Meth_0123456789876543210 t instance SuppressUnusedWarnings Meth_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) Meth_0123456789876543210Sym0KindInference) GHC.Tuple.()) data Meth_0123456789876543210Sym0 (l :: TyFun Bool Bool) = forall arg. SameKind (Apply Meth_0123456789876543210Sym0 arg) (Meth_0123456789876543210Sym1 arg) => Meth_0123456789876543210Sym0KindInference type instance Apply Meth_0123456789876543210Sym0 l = Meth_0123456789876543210 l type family L2r_0123456789876543210 (a :: Bool) :: Nat where L2r_0123456789876543210 False = FromInteger 0 L2r_0123456789876543210 True = FromInteger 1 type L2r_0123456789876543210Sym1 (t :: Bool) = L2r_0123456789876543210 t instance SuppressUnusedWarnings L2r_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) L2r_0123456789876543210Sym0KindInference) GHC.Tuple.()) data L2r_0123456789876543210Sym0 (l :: TyFun Bool Nat) = forall arg. SameKind (Apply L2r_0123456789876543210Sym0 arg) (L2r_0123456789876543210Sym1 arg) => L2r_0123456789876543210Sym0KindInference type instance Apply L2r_0123456789876543210Sym0 l = L2r_0123456789876543210 l instance PFD Bool Nat where type Meth a = Apply Meth_0123456789876543210Sym0 a type L2r a = Apply L2r_0123456789876543210Sym0 a sT1 :: Sing T1Sym0 sT1 = (applySing ((singFun1 @MethSym0) sMeth)) STrue class SFD a b | a -> b where sMeth :: forall (t :: a). Sing t -> Sing (Apply MethSym0 t :: a) sL2r :: forall (t :: a). Sing t -> Sing (Apply L2rSym0 t :: b) instance SFD Bool Nat where sMeth :: forall (t :: Bool). Sing t -> Sing (Apply MethSym0 t :: Bool) sL2r :: forall (t :: Bool). Sing t -> Sing (Apply L2rSym0 t :: Nat) sMeth (sA_0123456789876543210 :: Sing a_0123456789876543210) = (applySing ((singFun1 @NotSym0) sNot)) sA_0123456789876543210 sL2r SFalse = sFromInteger (sing :: Sing 0) sL2r STrue = sFromInteger (sing :: Sing 1)