packages feed

singletons-base-3.1: tests/compile-and-dump/Singletons/T209.golden

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 a b (t :: a) (t :: b) (t :: Bool). Sing t
                                                -> Sing t
                                                   -> Sing t
                                                      -> Sing (Apply (Apply (Apply MSym0 t) t) t :: Bool)
    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 -> GHC.Types.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