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