singletons-2.7: tests/compile-and-dump/Singletons/T145.golden
Singletons/T145.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| class Column (f :: Type -> Type) where
col :: f a -> a -> Bool |]
======>
class Column (f :: Type -> Type) where
col :: f a -> a -> Bool
type ColSym0 :: forall f a. (~>) (f a) ((~>) a Bool)
data ColSym0 a0123456789876543210
where
ColSym0KindInference :: SameKind (Apply ColSym0 arg) (ColSym1 arg) =>
ColSym0 a0123456789876543210
type instance Apply ColSym0 a0123456789876543210 = ColSym1 a0123456789876543210
instance SuppressUnusedWarnings ColSym0 where
suppressUnusedWarnings = snd (((,) ColSym0KindInference) ())
type ColSym1 :: forall f a. f a -> (~>) a Bool
data ColSym1 a0123456789876543210 a0123456789876543210
where
ColSym1KindInference :: SameKind (Apply (ColSym1 a0123456789876543210) arg) (ColSym2 a0123456789876543210 arg) =>
ColSym1 a0123456789876543210 a0123456789876543210
type instance Apply (ColSym1 a0123456789876543210) a0123456789876543210 = ColSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ColSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) ColSym1KindInference) ())
type ColSym2 (a0123456789876543210 :: f a) (a0123456789876543210 :: a) =
Col a0123456789876543210 a0123456789876543210 :: Bool
class PColumn (f :: Type -> Type) where
type Col (arg :: f a) (arg :: a) :: Bool
class SColumn (f :: Type -> Type) where
sCol ::
forall a (t :: f a) (t :: a).
Sing t -> Sing t -> Sing (Apply (Apply ColSym0 t) t :: Bool)
instance SColumn f =>
SingI (ColSym0 :: (~>) (f a) ((~>) a Bool)) where
sing = (singFun2 @ColSym0) sCol
instance (SColumn f, SingI d) =>
SingI (ColSym1 (d :: f a) :: (~>) a Bool) where
sing = (singFun1 @(ColSym1 (d :: f a))) (sCol (sing @d))