packages feed

singletons-base-3.5: tests/compile-and-dump/Singletons/T54.golden

Singletons/T54.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| g :: Bool -> Bool
          g e = (case [not] of [_] -> not) e |]
  ======>
    g :: Bool -> Bool
    g e = (case [not] of [_] -> not) e
    type family LamCases_0123456789876543210 (e0123456789876543210 :: Bool) a_0123456789876543210 where
      LamCases_0123456789876543210 e '[_] = NotSym0
    data LamCases_0123456789876543210Sym0 (e0123456789876543210 :: Bool) a_01234567898765432100123456789876543210
      where
        LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 e0123456789876543210) arg) (LamCases_0123456789876543210Sym1 e0123456789876543210 arg) =>
                                                         LamCases_0123456789876543210Sym0 e0123456789876543210 a_01234567898765432100123456789876543210
    type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 e0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 e0123456789876543210 a_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 e0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) LamCases_0123456789876543210Sym0KindInference ())
    type family LamCases_0123456789876543210Sym1 (e0123456789876543210 :: Bool) a_01234567898765432100123456789876543210 where
      LamCases_0123456789876543210Sym1 e0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 e0123456789876543210 a_01234567898765432100123456789876543210
    type GSym0 :: (~>) Bool Bool
    data GSym0 :: (~>) Bool Bool
      where
        GSym0KindInference :: SameKind (Apply GSym0 arg) (GSym1 arg) =>
                              GSym0 a0123456789876543210
    type instance Apply @Bool @Bool GSym0 a0123456789876543210 = G a0123456789876543210
    instance SuppressUnusedWarnings GSym0 where
      suppressUnusedWarnings = snd ((,) GSym0KindInference ())
    type GSym1 :: Bool -> Bool
    type family GSym1 (a0123456789876543210 :: Bool) :: Bool where
      GSym1 a0123456789876543210 = G a0123456789876543210
    type G :: Bool -> Bool
    type family G (a :: Bool) :: Bool where
      G e = Apply (Apply (LamCases_0123456789876543210Sym0 e) (Apply (Apply (:@#@$) NotSym0) NilSym0)) e
    sG :: (forall (t :: Bool). Sing t -> Sing (G t :: Bool) :: Type)
    sG (sE :: Sing e)
      = applySing
          (applySing
             (singFun1
                @(LamCases_0123456789876543210Sym0 e)
                (\cases (SCons _ SNil) -> singFun1 @NotSym0 sNot))
             (applySing
                (applySing (singFun2 @(:@#@$) SCons) (singFun1 @NotSym0 sNot))
                SNil))
          sE
    instance SingI (GSym0 :: (~>) Bool Bool) where
      sing = singFun1 @GSym0 sG