packages feed

singletons-2.7: 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
    data Let0123456789876543210Scrutinee_0123456789876543210Sym0 e0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym0 e0123456789876543210
    type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 e0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 e0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            (((,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
               ())
    type Let0123456789876543210Scrutinee_0123456789876543210Sym1 e0123456789876543210 =
        Let0123456789876543210Scrutinee_0123456789876543210 e0123456789876543210
    type family Let0123456789876543210Scrutinee_0123456789876543210 e where
      Let0123456789876543210Scrutinee_0123456789876543210 e = Apply (Apply (:@#@$) NotSym0) NilSym0
    type family Case_0123456789876543210 e t where
      Case_0123456789876543210 e '[_] = NotSym0
    type GSym0 :: (~>) Bool Bool
    data GSym0 a0123456789876543210
      where
        GSym0KindInference :: SameKind (Apply GSym0 arg) (GSym1 arg) =>
                              GSym0 a0123456789876543210
    type instance Apply GSym0 a0123456789876543210 = GSym1 a0123456789876543210
    instance SuppressUnusedWarnings GSym0 where
      suppressUnusedWarnings = snd (((,) GSym0KindInference) ())
    type GSym1 (a0123456789876543210 :: Bool) =
        G a0123456789876543210 :: Bool
    type G :: Bool -> Bool
    type family G a where
      G e = Apply (Case_0123456789876543210 e (Let0123456789876543210Scrutinee_0123456789876543210Sym1 e)) e
    sG :: forall (t :: Bool). Sing t -> Sing (Apply GSym0 t :: Bool)
    sG (sE :: Sing e)
      = (applySing
           (let
              sScrutinee_0123456789876543210 ::
                Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym1 e)
              sScrutinee_0123456789876543210
                = (applySing
                     ((applySing ((singFun2 @(:@#@$)) SCons))
                        ((singFun1 @NotSym0) sNot)))
                    SNil
            in
              (id
                 @(Sing (Case_0123456789876543210 e (Let0123456789876543210Scrutinee_0123456789876543210Sym1 e))))
                (case sScrutinee_0123456789876543210 of {
                   SCons _ SNil -> (singFun1 @NotSym0) sNot })))
          sE
    instance SingI (GSym0 :: (~>) Bool Bool) where
      sing = (singFun1 @GSym0) sG