Singletons/T312.hs:(0,0)-(0,0): Splicing declarations singletons [d| class Foo a where bar :: a -> b -> b bar _ x = x baz :: forall b. a -> b -> b baz = h where h :: forall c. c -> b -> b h _ x = x |] ======> class Foo a where bar :: a -> b -> b baz :: forall b. a -> b -> b bar _ x = x baz = h where h :: forall c. c -> b -> b h _ x = x type BarSym0 :: forall a b. (~>) a ((~>) b b) data BarSym0 :: (~>) a ((~>) b b) where BarSym0KindInference :: SameKind (Apply BarSym0 arg) (BarSym1 arg) => BarSym0 a0123456789876543210 type instance Apply BarSym0 a0123456789876543210 = BarSym1 a0123456789876543210 instance SuppressUnusedWarnings BarSym0 where suppressUnusedWarnings = snd ((,) BarSym0KindInference ()) type BarSym1 :: forall a b. a -> (~>) b b data BarSym1 (a0123456789876543210 :: a) :: (~>) b b where BarSym1KindInference :: SameKind (Apply (BarSym1 a0123456789876543210) arg) (BarSym2 a0123456789876543210 arg) => BarSym1 a0123456789876543210 a0123456789876543210 type instance Apply (BarSym1 a0123456789876543210) a0123456789876543210 = Bar a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (BarSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) BarSym1KindInference ()) type BarSym2 :: forall a b. a -> b -> b type family BarSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where BarSym2 a0123456789876543210 a0123456789876543210 = Bar a0123456789876543210 a0123456789876543210 type BazSym0 :: forall a b. (~>) a ((~>) b b) data BazSym0 :: (~>) a ((~>) b b) where BazSym0KindInference :: SameKind (Apply BazSym0 arg) (BazSym1 arg) => BazSym0 a0123456789876543210 type instance Apply BazSym0 a0123456789876543210 = BazSym1 a0123456789876543210 instance SuppressUnusedWarnings BazSym0 where suppressUnusedWarnings = snd ((,) BazSym0KindInference ()) type BazSym1 :: forall a b. a -> (~>) b b data BazSym1 (a0123456789876543210 :: a) :: (~>) b b where BazSym1KindInference :: SameKind (Apply (BazSym1 a0123456789876543210) arg) (BazSym2 a0123456789876543210 arg) => BazSym1 a0123456789876543210 a0123456789876543210 type instance Apply (BazSym1 a0123456789876543210) a0123456789876543210 = Baz a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (BazSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) BazSym1KindInference ()) type BazSym2 :: forall a b. a -> b -> b type family BazSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where BazSym2 a0123456789876543210 a0123456789876543210 = Baz a0123456789876543210 a0123456789876543210 type Bar_0123456789876543210 :: a -> b -> b type family Bar_0123456789876543210 (a :: a) (a :: b) :: b where Bar_0123456789876543210 _ x = x type Bar_0123456789876543210Sym0 :: (~>) a ((~>) b b) data Bar_0123456789876543210Sym0 :: (~>) a ((~>) b b) where Bar_0123456789876543210Sym0KindInference :: SameKind (Apply Bar_0123456789876543210Sym0 arg) (Bar_0123456789876543210Sym1 arg) => Bar_0123456789876543210Sym0 a0123456789876543210 type instance Apply Bar_0123456789876543210Sym0 a0123456789876543210 = Bar_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings Bar_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) Bar_0123456789876543210Sym0KindInference ()) type Bar_0123456789876543210Sym1 :: a -> (~>) b b data Bar_0123456789876543210Sym1 (a0123456789876543210 :: a) :: (~>) b b where Bar_0123456789876543210Sym1KindInference :: SameKind (Apply (Bar_0123456789876543210Sym1 a0123456789876543210) arg) (Bar_0123456789876543210Sym2 a0123456789876543210 arg) => Bar_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (Bar_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Bar_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Bar_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Bar_0123456789876543210Sym1KindInference ()) type Bar_0123456789876543210Sym2 :: a -> b -> b type family Bar_0123456789876543210Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where Bar_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Bar_0123456789876543210 a0123456789876543210 a0123456789876543210 data Let0123456789876543210HSym0 a_01234567898765432100123456789876543210 where Let0123456789876543210HSym0KindInference :: SameKind (Apply Let0123456789876543210HSym0 arg) (Let0123456789876543210HSym1 arg) => Let0123456789876543210HSym0 a_01234567898765432100123456789876543210 type instance Apply Let0123456789876543210HSym0 a_01234567898765432100123456789876543210 = Let0123456789876543210HSym1 a_01234567898765432100123456789876543210 instance SuppressUnusedWarnings Let0123456789876543210HSym0 where suppressUnusedWarnings = snd ((,) Let0123456789876543210HSym0KindInference ()) data Let0123456789876543210HSym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 where Let0123456789876543210HSym1KindInference :: SameKind (Apply (Let0123456789876543210HSym1 a_01234567898765432100123456789876543210) arg) (Let0123456789876543210HSym2 a_01234567898765432100123456789876543210 arg) => Let0123456789876543210HSym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 type instance Apply (Let0123456789876543210HSym1 a_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = Let0123456789876543210HSym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 instance SuppressUnusedWarnings (Let0123456789876543210HSym1 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210HSym1KindInference ()) data Let0123456789876543210HSym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 :: (~>) c0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210) where Let0123456789876543210HSym2KindInference :: SameKind (Apply (Let0123456789876543210HSym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Let0123456789876543210HSym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Let0123456789876543210HSym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 type instance Apply (Let0123456789876543210HSym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) a0123456789876543210 = Let0123456789876543210HSym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Let0123456789876543210HSym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210HSym2KindInference ()) data Let0123456789876543210HSym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a0123456789876543210 :: c0123456789876543210) :: (~>) b0123456789876543210 b0123456789876543210 where Let0123456789876543210HSym3KindInference :: SameKind (Apply (Let0123456789876543210HSym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210) arg) (Let0123456789876543210HSym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 arg) => Let0123456789876543210HSym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (Let0123456789876543210HSym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210) a0123456789876543210 = Let0123456789876543210H a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Let0123456789876543210HSym3 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210HSym3KindInference ()) type family Let0123456789876543210HSym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a0123456789876543210 :: c0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: b0123456789876543210 where Let0123456789876543210HSym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210H a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 type family Let0123456789876543210H a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a :: c) (a :: b) :: b where Let0123456789876543210H a_0123456789876543210 a_0123456789876543210 (_ :: c) (x :: b) = x type Baz_0123456789876543210 :: a -> b -> b type family Baz_0123456789876543210 (a :: a) (a :: b) :: b where Baz_0123456789876543210 a_0123456789876543210 a_0123456789876543210 = Apply (Apply (Let0123456789876543210HSym2 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210) a_0123456789876543210 type Baz_0123456789876543210Sym0 :: (~>) a ((~>) b b) data Baz_0123456789876543210Sym0 :: (~>) a ((~>) b b) where Baz_0123456789876543210Sym0KindInference :: SameKind (Apply Baz_0123456789876543210Sym0 arg) (Baz_0123456789876543210Sym1 arg) => Baz_0123456789876543210Sym0 a0123456789876543210 type instance Apply Baz_0123456789876543210Sym0 a0123456789876543210 = Baz_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings Baz_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) Baz_0123456789876543210Sym0KindInference ()) type Baz_0123456789876543210Sym1 :: a -> (~>) b b data Baz_0123456789876543210Sym1 (a0123456789876543210 :: a) :: (~>) b b where Baz_0123456789876543210Sym1KindInference :: SameKind (Apply (Baz_0123456789876543210Sym1 a0123456789876543210) arg) (Baz_0123456789876543210Sym2 a0123456789876543210 arg) => Baz_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (Baz_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Baz_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Baz_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Baz_0123456789876543210Sym1KindInference ()) type Baz_0123456789876543210Sym2 :: a -> b -> b type family Baz_0123456789876543210Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where Baz_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Baz_0123456789876543210 a0123456789876543210 a0123456789876543210 class PFoo a where type family Bar (arg :: a) (arg :: b) :: b type family Baz (arg :: a) (arg :: b) :: b type Bar a a = Apply (Apply Bar_0123456789876543210Sym0 a) a type Baz a a = Apply (Apply Baz_0123456789876543210Sym0 a) a class SFoo a where sBar :: (forall (t :: a) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply BarSym0 t) t :: b) :: Type) sBaz :: forall b (t :: a) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply BazSym0 t) t :: b) default sBar :: (forall (t :: a) (t :: b). ((Apply (Apply BarSym0 t) t :: b) ~ Apply (Apply Bar_0123456789876543210Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply BarSym0 t) t :: b) :: Type) default sBaz :: forall b (t :: a) (t :: b). ((Apply (Apply BazSym0 t) t :: b) ~ Apply (Apply Baz_0123456789876543210Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply BazSym0 t) t :: b) sBar _ (sX :: Sing x) = sX sBaz (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing (applySing (let sH :: forall c (t :: c) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply (Let0123456789876543210HSym2 a_0123456789876543210 a_0123456789876543210) t) t :: b) sH _ (sX :: Sing x) = sX in singFun2 @(Let0123456789876543210HSym2 a_0123456789876543210 a_0123456789876543210) sH) sA_0123456789876543210) sA_0123456789876543210 instance SFoo a => SingI (BarSym0 :: (~>) a ((~>) b b)) where sing = singFun2 @BarSym0 sBar instance (SFoo a, SingI d) => SingI (BarSym1 (d :: a) :: (~>) b b) where sing = singFun1 @(BarSym1 (d :: a)) (sBar (sing @d)) instance SFoo a => SingI1 (BarSym1 :: a -> (~>) b b) where liftSing (s :: Sing (d :: a)) = singFun1 @(BarSym1 (d :: a)) (sBar s) instance SFoo a => SingI (BazSym0 :: (~>) a ((~>) b b)) where sing = singFun2 @BazSym0 sBaz instance (SFoo a, SingI d) => SingI (BazSym1 (d :: a) :: (~>) b b) where sing = singFun1 @(BazSym1 (d :: a)) (sBaz (sing @d)) instance SFoo a => SingI1 (BazSym1 :: a -> (~>) b b) where liftSing (s :: Sing (d :: a)) = singFun1 @(BazSym1 (d :: a)) (sBaz s)