singletons-base-3.2: 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_0123456789876543210 e0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference
())
type family Let0123456789876543210Scrutinee_0123456789876543210Sym1 e0123456789876543210 where
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 :: (~>) Bool Bool
where
GSym0KindInference :: SameKind (Apply GSym0 arg) (GSym1 arg) =>
GSym0 a0123456789876543210
type instance Apply 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 (Case_0123456789876543210 e (Let0123456789876543210Scrutinee_0123456789876543210Sym1 e)) e
sG ::
(forall (t :: Bool).
Sing t -> Sing (Apply GSym0 t :: Bool) :: Type)
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