Singletons/T209.hs:(0,0)-(0,0): Splicing declarations singletons [d| m :: a -> b -> Bool -> Bool m _ _ x = x class C a b data Hm = Hm deriving anyclass (C Bool) deriving anyclass instance C a a => C a (Maybe a) |] ======> class C a b m :: a -> b -> Bool -> Bool m _ _ x = x data Hm = Hm deriving anyclass (C Bool) deriving anyclass instance C a a => C a (Maybe a) type HmSym0 :: Hm type family HmSym0 :: Hm where HmSym0 = Hm type MSym0 :: (~>) a ((~>) b ((~>) Bool Bool)) data MSym0 :: (~>) a ((~>) b ((~>) Bool Bool)) where MSym0KindInference :: SameKind (Apply MSym0 arg) (MSym1 arg) => MSym0 a0123456789876543210 type instance Apply MSym0 a0123456789876543210 = MSym1 a0123456789876543210 instance SuppressUnusedWarnings MSym0 where suppressUnusedWarnings = snd ((,) MSym0KindInference ()) type MSym1 :: a -> (~>) b ((~>) Bool Bool) data MSym1 (a0123456789876543210 :: a) :: (~>) b ((~>) Bool Bool) where MSym1KindInference :: SameKind (Apply (MSym1 a0123456789876543210) arg) (MSym2 a0123456789876543210 arg) => MSym1 a0123456789876543210 a0123456789876543210 type instance Apply (MSym1 a0123456789876543210) a0123456789876543210 = MSym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (MSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) MSym1KindInference ()) type MSym2 :: a -> b -> (~>) Bool Bool data MSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: (~>) Bool Bool where MSym2KindInference :: SameKind (Apply (MSym2 a0123456789876543210 a0123456789876543210) arg) (MSym3 a0123456789876543210 a0123456789876543210 arg) => MSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (MSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = M a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (MSym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) MSym2KindInference ()) type MSym3 :: a -> b -> Bool -> Bool type family MSym3 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: Bool) :: Bool where MSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = M a0123456789876543210 a0123456789876543210 a0123456789876543210 type M :: a -> b -> Bool -> Bool type family M (a :: a) (a :: b) (a :: Bool) :: Bool where M _ _ x = x class PC a b instance PC Bool Hm instance PC a (Maybe a) sM :: (forall (t :: a) (t :: b) (t :: Bool). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply MSym0 t) t) t :: Bool) :: Type) sM _ _ (sX :: Sing x) = sX instance SingI (MSym0 :: (~>) a ((~>) b ((~>) Bool Bool))) where sing = singFun3 @MSym0 sM instance SingI d => SingI (MSym1 (d :: a) :: (~>) b ((~>) Bool Bool)) where sing = singFun2 @(MSym1 (d :: a)) (sM (sing @d)) instance SingI1 (MSym1 :: a -> (~>) b ((~>) Bool Bool)) where liftSing (s :: Sing (d :: a)) = singFun2 @(MSym1 (d :: a)) (sM s) instance (SingI d, SingI d) => SingI (MSym2 (d :: a) (d :: b) :: (~>) Bool Bool) where sing = singFun1 @(MSym2 (d :: a) (d :: b)) (sM (sing @d) (sing @d)) instance SingI d => SingI1 (MSym2 (d :: a) :: b -> (~>) Bool Bool) where liftSing (s :: Sing (d :: b)) = singFun1 @(MSym2 (d :: a) (d :: b)) (sM (sing @d) s) instance SingI2 (MSym2 :: a -> b -> (~>) Bool Bool) where liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b)) = singFun1 @(MSym2 (d :: a) (d :: b)) (sM s s) data SHm :: Hm -> Type where SHm :: SHm (Hm :: Hm) type instance Sing @Hm = SHm instance SingKind Hm where type Demote Hm = Hm fromSing SHm = Hm toSing Hm = SomeSing SHm class SC a b instance SC Bool Hm instance SC a a => SC a (Maybe a) instance SingI Hm where sing = SHm