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 :: (~>) (f a) ((~>) a Bool)
      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 :: f a) :: (~>) a Bool
      where
        ColSym1KindInference :: SameKind (Apply (ColSym1 a0123456789876543210) arg) (ColSym2 a0123456789876543210 arg) =>
                                ColSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (ColSym1 a0123456789876543210) a0123456789876543210 = Col a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ColSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) ColSym1KindInference ())
    type ColSym2 :: forall f a. f a -> a -> Bool
    type family ColSym2 @f @a (a0123456789876543210 :: f a) (a0123456789876543210 :: a) :: Bool where
      ColSym2 a0123456789876543210 a0123456789876543210 = Col a0123456789876543210 a0123456789876543210
    class PColumn (f :: Type -> Type) where
      type family Col (arg :: f a) (arg :: a) :: Bool
    class SColumn (f :: Type -> Type) where
      sCol ::
        (forall (t :: f a) (t :: a).
         Sing t
         -> Sing t -> Sing (Apply (Apply ColSym0 t) t :: Bool) :: Type)
    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))
    instance SColumn f => SingI1 (ColSym1 :: f a -> (~>) a Bool) where
      liftSing (s :: Sing (d :: f a))
        = singFun1 @(ColSym1 (d :: f a)) (sCol s)