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 MethSym0 :: forall a. (~>) a a data MethSym0 a0123456789876543210 where MethSym0KindInference :: SameKind (Apply MethSym0 arg) (MethSym1 arg) => MethSym0 a0123456789876543210 type instance Apply MethSym0 a0123456789876543210 = MethSym1 a0123456789876543210 instance SuppressUnusedWarnings MethSym0 where suppressUnusedWarnings = snd (((,) MethSym0KindInference) ()) type MethSym1 (a0123456789876543210 :: a) = Meth a0123456789876543210 :: a type L2rSym0 :: forall a b. (~>) a b data L2rSym0 a0123456789876543210 where L2rSym0KindInference :: SameKind (Apply L2rSym0 arg) (L2rSym1 arg) => L2rSym0 a0123456789876543210 type instance Apply L2rSym0 a0123456789876543210 = L2rSym1 a0123456789876543210 instance SuppressUnusedWarnings L2rSym0 where suppressUnusedWarnings = snd (((,) L2rSym0KindInference) ()) type L2rSym1 (a0123456789876543210 :: a) = L2r a0123456789876543210 :: b class PFD a b | a -> b where type Meth (arg :: a) :: a type L2r (arg :: a) :: b type Meth_0123456789876543210 :: Bool -> Bool type family Meth_0123456789876543210 a where Meth_0123456789876543210 a_0123456789876543210 = Apply NotSym0 a_0123456789876543210 type Meth_0123456789876543210Sym0 :: (~>) Bool Bool data Meth_0123456789876543210Sym0 a0123456789876543210 where Meth_0123456789876543210Sym0KindInference :: SameKind (Apply Meth_0123456789876543210Sym0 arg) (Meth_0123456789876543210Sym1 arg) => Meth_0123456789876543210Sym0 a0123456789876543210 type instance Apply Meth_0123456789876543210Sym0 a0123456789876543210 = Meth_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings Meth_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) Meth_0123456789876543210Sym0KindInference) ()) type Meth_0123456789876543210Sym1 (a0123456789876543210 :: Bool) = Meth_0123456789876543210 a0123456789876543210 :: Bool type L2r_0123456789876543210 :: Bool -> Nat type family L2r_0123456789876543210 a where L2r_0123456789876543210 'False = FromInteger 0 L2r_0123456789876543210 'True = FromInteger 1 type L2r_0123456789876543210Sym0 :: (~>) Bool Nat data L2r_0123456789876543210Sym0 a0123456789876543210 where L2r_0123456789876543210Sym0KindInference :: SameKind (Apply L2r_0123456789876543210Sym0 arg) (L2r_0123456789876543210Sym1 arg) => L2r_0123456789876543210Sym0 a0123456789876543210 type instance Apply L2r_0123456789876543210Sym0 a0123456789876543210 = L2r_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings L2r_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) L2r_0123456789876543210Sym0KindInference) ()) type L2r_0123456789876543210Sym1 (a0123456789876543210 :: Bool) = L2r_0123456789876543210 a0123456789876543210 :: Nat 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) instance SFD a b => SingI (MethSym0 :: (~>) a a) where sing = (singFun1 @MethSym0) sMeth instance SFD a b => SingI (L2rSym0 :: (~>) a b) where sing = (singFun1 @L2rSym0) sL2r