singletons-2.2: tests/compile-and-dump/Singletons/TopLevelPatterns.ghc80.template
Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| data Bool = False | True
data Foo = Bar Bool Bool |]
======>
data Bool = False | True
data Foo = Bar Bool Bool
type FalseSym0 = False
type TrueSym0 = True
type BarSym2 (t :: Bool) (t :: Bool) = Bar t t
instance SuppressUnusedWarnings BarSym1 where
suppressUnusedWarnings _
= Data.Tuple.snd (GHC.Tuple.(,) BarSym1KindInference GHC.Tuple.())
data BarSym1 (l :: Bool) (l :: TyFun Bool Foo)
= forall arg. KindOf (Apply (BarSym1 l) arg) ~ KindOf (BarSym2 l arg) =>
BarSym1KindInference
type instance Apply (BarSym1 l) l = BarSym2 l l
instance SuppressUnusedWarnings BarSym0 where
suppressUnusedWarnings _
= Data.Tuple.snd (GHC.Tuple.(,) BarSym0KindInference GHC.Tuple.())
data BarSym0 (l :: TyFun Bool (TyFun Bool Foo -> GHC.Types.Type))
= forall arg. KindOf (Apply BarSym0 arg) ~ KindOf (BarSym1 arg) =>
BarSym0KindInference
type instance Apply BarSym0 l = BarSym1 l
data instance Sing (z :: Bool)
= z ~ False => SFalse | z ~ True => STrue
type SBool = (Sing :: Bool -> GHC.Types.Type)
instance SingKind Bool where
type DemoteRep Bool = Bool
fromSing SFalse = False
fromSing STrue = True
toSing False = SomeSing SFalse
toSing True = SomeSing STrue
data instance Sing (z :: Foo)
= forall (n :: Bool) (n :: Bool). z ~ Bar n n =>
SBar (Sing (n :: Bool)) (Sing (n :: Bool))
type SFoo = (Sing :: Foo -> GHC.Types.Type)
instance SingKind Foo where
type DemoteRep Foo = Foo
fromSing (SBar b b) = Bar (fromSing b) (fromSing b)
toSing (Bar b b)
= case
GHC.Tuple.(,)
(toSing b :: SomeSing Bool) (toSing b :: SomeSing Bool)
of {
GHC.Tuple.(,) (SomeSing c) (SomeSing c) -> SomeSing (SBar c c) }
instance SingI False where
sing = SFalse
instance SingI True where
sing = STrue
instance (SingI n, SingI n) =>
SingI (Bar (n :: Bool) (n :: Bool)) where
sing = SBar sing sing
Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| otherwise :: Bool
otherwise = True
id :: a -> a
id x = x
not :: Bool -> Bool
not True = False
not False = True
false_ = False
f, g :: Bool -> Bool
[f, g] = [not, id]
h, i :: Bool -> Bool
(h, i) = (f, g)
j, k :: Bool
(Bar j k) = Bar True (h False)
l, m :: Bool
[l, m] = [not True, id False] |]
======>
otherwise :: Bool
otherwise = True
id :: forall a. a -> a
id x = x
not :: Bool -> Bool
not True = False
not False = True
false_ = False
f :: Bool -> Bool
g :: Bool -> Bool
[f, g] = [not, id]
h :: Bool -> Bool
i :: Bool -> Bool
(h, i) = (f, g)
j :: Bool
k :: Bool
Bar j k = Bar True (h False)
l :: Bool
m :: Bool
[l, m] = [not True, id False]
type family Case_0123456789 a_0123456789 t where
Case_0123456789 a_0123456789 '[y_0123456789,
_z_0123456789] = y_0123456789
type family Case_0123456789 a_0123456789 t where
Case_0123456789 a_0123456789 '[_z_0123456789,
y_0123456789] = y_0123456789
type family Case_0123456789 a_0123456789 t where
Case_0123456789 a_0123456789 '(y_0123456789,
_z_0123456789) = y_0123456789
type family Case_0123456789 a_0123456789 t where
Case_0123456789 a_0123456789 '(_z_0123456789,
y_0123456789) = y_0123456789
type family Case_0123456789 t where
Case_0123456789 (Bar y_0123456789 _z_0123456789) = y_0123456789
type family Case_0123456789 t where
Case_0123456789 (Bar _z_0123456789 y_0123456789) = y_0123456789
type family Case_0123456789 t where
Case_0123456789 '[y_0123456789, _z_0123456789] = y_0123456789
type family Case_0123456789 t where
Case_0123456789 '[_z_0123456789, y_0123456789] = y_0123456789
type False_Sym0 = False_
type NotSym1 (t :: Bool) = Not t
instance SuppressUnusedWarnings NotSym0 where
suppressUnusedWarnings _
= Data.Tuple.snd (GHC.Tuple.(,) NotSym0KindInference GHC.Tuple.())
data NotSym0 (l :: TyFun Bool Bool)
= forall arg. KindOf (Apply NotSym0 arg) ~ KindOf (NotSym1 arg) =>
NotSym0KindInference
type instance Apply NotSym0 l = NotSym1 l
type IdSym1 (t :: a0123456789) = Id t
instance SuppressUnusedWarnings IdSym0 where
suppressUnusedWarnings _
= Data.Tuple.snd (GHC.Tuple.(,) IdSym0KindInference GHC.Tuple.())
data IdSym0 (l :: TyFun a0123456789 a0123456789)
= forall arg. KindOf (Apply IdSym0 arg) ~ KindOf (IdSym1 arg) =>
IdSym0KindInference
type instance Apply IdSym0 l = IdSym1 l
type FSym1 (t :: Bool) = F t
instance SuppressUnusedWarnings FSym0 where
suppressUnusedWarnings _
= Data.Tuple.snd (GHC.Tuple.(,) FSym0KindInference GHC.Tuple.())
data FSym0 (l :: TyFun Bool Bool)
= forall arg. KindOf (Apply FSym0 arg) ~ KindOf (FSym1 arg) =>
FSym0KindInference
type instance Apply FSym0 l = FSym1 l
type GSym1 (t :: Bool) = G t
instance SuppressUnusedWarnings GSym0 where
suppressUnusedWarnings _
= Data.Tuple.snd (GHC.Tuple.(,) GSym0KindInference GHC.Tuple.())
data GSym0 (l :: TyFun Bool Bool)
= forall arg. KindOf (Apply GSym0 arg) ~ KindOf (GSym1 arg) =>
GSym0KindInference
type instance Apply GSym0 l = GSym1 l
type HSym1 (t :: Bool) = H t
instance SuppressUnusedWarnings HSym0 where
suppressUnusedWarnings _
= Data.Tuple.snd (GHC.Tuple.(,) HSym0KindInference GHC.Tuple.())
data HSym0 (l :: TyFun Bool Bool)
= forall arg. KindOf (Apply HSym0 arg) ~ KindOf (HSym1 arg) =>
HSym0KindInference
type instance Apply HSym0 l = HSym1 l
type ISym1 (t :: Bool) = I t
instance SuppressUnusedWarnings ISym0 where
suppressUnusedWarnings _
= Data.Tuple.snd (GHC.Tuple.(,) ISym0KindInference GHC.Tuple.())
data ISym0 (l :: TyFun Bool Bool)
= forall arg. KindOf (Apply ISym0 arg) ~ KindOf (ISym1 arg) =>
ISym0KindInference
type instance Apply ISym0 l = ISym1 l
type JSym0 = J
type KSym0 = K
type LSym0 = L
type MSym0 = M
type OtherwiseSym0 = Otherwise
type X_0123456789Sym0 = X_0123456789
type X_0123456789Sym0 = X_0123456789
type X_0123456789Sym0 = X_0123456789
type X_0123456789Sym0 = X_0123456789
type family False_ where
False_ = FalseSym0
type family Not (a :: Bool) :: Bool where
Not True = FalseSym0
Not False = TrueSym0
type family Id (a :: a) :: a where
Id x = x
type family F (a :: Bool) :: Bool where
F a_0123456789 = Apply (Case_0123456789 a_0123456789 X_0123456789Sym0) a_0123456789
type family G (a :: Bool) :: Bool where
G a_0123456789 = Apply (Case_0123456789 a_0123456789 X_0123456789Sym0) a_0123456789
type family H (a :: Bool) :: Bool where
H a_0123456789 = Apply (Case_0123456789 a_0123456789 X_0123456789Sym0) a_0123456789
type family I (a :: Bool) :: Bool where
I a_0123456789 = Apply (Case_0123456789 a_0123456789 X_0123456789Sym0) a_0123456789
type family J :: Bool where
J = Case_0123456789 X_0123456789Sym0
type family K :: Bool where
K = Case_0123456789 X_0123456789Sym0
type family L :: Bool where
L = Case_0123456789 X_0123456789Sym0
type family M :: Bool where
M = Case_0123456789 X_0123456789Sym0
type family Otherwise :: Bool where
Otherwise = TrueSym0
type family X_0123456789 where
X_0123456789 = Apply (Apply (:$) NotSym0) (Apply (Apply (:$) IdSym0) '[])
type family X_0123456789 where
X_0123456789 = Apply (Apply Tuple2Sym0 FSym0) GSym0
type family X_0123456789 where
X_0123456789 = Apply (Apply BarSym0 TrueSym0) (Apply HSym0 FalseSym0)
type family X_0123456789 where
X_0123456789 = Apply (Apply (:$) (Apply NotSym0 TrueSym0)) (Apply (Apply (:$) (Apply IdSym0 FalseSym0)) '[])
sFalse_ :: Sing False_Sym0
sNot ::
forall (t :: Bool). Sing t -> Sing (Apply NotSym0 t :: Bool)
sId :: forall (t :: a). Sing t -> Sing (Apply IdSym0 t :: a)
sF :: forall (t :: Bool). Sing t -> Sing (Apply FSym0 t :: Bool)
sG :: forall (t :: Bool). Sing t -> Sing (Apply GSym0 t :: Bool)
sH :: forall (t :: Bool). Sing t -> Sing (Apply HSym0 t :: Bool)
sI :: forall (t :: Bool). Sing t -> Sing (Apply ISym0 t :: Bool)
sJ :: Sing (JSym0 :: Bool)
sK :: Sing (KSym0 :: Bool)
sL :: Sing (LSym0 :: Bool)
sM :: Sing (MSym0 :: Bool)
sOtherwise :: Sing (OtherwiseSym0 :: Bool)
sX_0123456789 :: Sing X_0123456789Sym0
sX_0123456789 :: Sing X_0123456789Sym0
sX_0123456789 :: Sing X_0123456789Sym0
sX_0123456789 :: Sing X_0123456789Sym0
sFalse_ = SFalse
sNot STrue
= let
lambda :: t ~ TrueSym0 => Sing (Apply NotSym0 t :: Bool)
lambda = SFalse
in lambda
sNot SFalse
= let
lambda :: t ~ FalseSym0 => Sing (Apply NotSym0 t :: Bool)
lambda = STrue
in lambda
sId sX
= let
lambda :: forall x. t ~ x => Sing x -> Sing (Apply IdSym0 t :: a)
lambda x = x
in lambda sX
sF sA_0123456789
= let
lambda ::
forall a_0123456789.
t ~ a_0123456789 =>
Sing a_0123456789 -> Sing (Apply FSym0 t :: Bool)
lambda a_0123456789
= applySing
(case sX_0123456789 of {
SCons sY_0123456789 (SCons _s_z_0123456789 SNil)
-> let
lambda ::
forall y_0123456789 _z_0123456789.
Apply (Apply (:$) y_0123456789) (Apply (Apply (:$) _z_0123456789) '[]) ~ X_0123456789Sym0 =>
Sing y_0123456789
-> Sing _z_0123456789
-> Sing (Case_0123456789 a_0123456789 (Apply (Apply (:$) y_0123456789) (Apply (Apply (:$) _z_0123456789) '[])))
lambda y_0123456789 _z_0123456789 = y_0123456789
in lambda sY_0123456789 _s_z_0123456789 } ::
Sing (Case_0123456789 a_0123456789 X_0123456789Sym0))
a_0123456789
in lambda sA_0123456789
sG sA_0123456789
= let
lambda ::
forall a_0123456789.
t ~ a_0123456789 =>
Sing a_0123456789 -> Sing (Apply GSym0 t :: Bool)
lambda a_0123456789
= applySing
(case sX_0123456789 of {
SCons _s_z_0123456789 (SCons sY_0123456789 SNil)
-> let
lambda ::
forall _z_0123456789 y_0123456789.
Apply (Apply (:$) _z_0123456789) (Apply (Apply (:$) y_0123456789) '[]) ~ X_0123456789Sym0 =>
Sing _z_0123456789
-> Sing y_0123456789
-> Sing (Case_0123456789 a_0123456789 (Apply (Apply (:$) _z_0123456789) (Apply (Apply (:$) y_0123456789) '[])))
lambda _z_0123456789 y_0123456789 = y_0123456789
in lambda _s_z_0123456789 sY_0123456789 } ::
Sing (Case_0123456789 a_0123456789 X_0123456789Sym0))
a_0123456789
in lambda sA_0123456789
sH sA_0123456789
= let
lambda ::
forall a_0123456789.
t ~ a_0123456789 =>
Sing a_0123456789 -> Sing (Apply HSym0 t :: Bool)
lambda a_0123456789
= applySing
(case sX_0123456789 of {
STuple2 sY_0123456789 _s_z_0123456789
-> let
lambda ::
forall y_0123456789 _z_0123456789.
Apply (Apply Tuple2Sym0 y_0123456789) _z_0123456789 ~ X_0123456789Sym0 =>
Sing y_0123456789
-> Sing _z_0123456789
-> Sing (Case_0123456789 a_0123456789 (Apply (Apply Tuple2Sym0 y_0123456789) _z_0123456789))
lambda y_0123456789 _z_0123456789 = y_0123456789
in lambda sY_0123456789 _s_z_0123456789 } ::
Sing (Case_0123456789 a_0123456789 X_0123456789Sym0))
a_0123456789
in lambda sA_0123456789
sI sA_0123456789
= let
lambda ::
forall a_0123456789.
t ~ a_0123456789 =>
Sing a_0123456789 -> Sing (Apply ISym0 t :: Bool)
lambda a_0123456789
= applySing
(case sX_0123456789 of {
STuple2 _s_z_0123456789 sY_0123456789
-> let
lambda ::
forall _z_0123456789 y_0123456789.
Apply (Apply Tuple2Sym0 _z_0123456789) y_0123456789 ~ X_0123456789Sym0 =>
Sing _z_0123456789
-> Sing y_0123456789
-> Sing (Case_0123456789 a_0123456789 (Apply (Apply Tuple2Sym0 _z_0123456789) y_0123456789))
lambda _z_0123456789 y_0123456789 = y_0123456789
in lambda _s_z_0123456789 sY_0123456789 } ::
Sing (Case_0123456789 a_0123456789 X_0123456789Sym0))
a_0123456789
in lambda sA_0123456789
sJ
= case sX_0123456789 of {
SBar sY_0123456789 _s_z_0123456789
-> let
lambda ::
forall y_0123456789 _z_0123456789.
Apply (Apply BarSym0 y_0123456789) _z_0123456789 ~ X_0123456789Sym0 =>
Sing y_0123456789
-> Sing _z_0123456789
-> Sing (Case_0123456789 (Apply (Apply BarSym0 y_0123456789) _z_0123456789) :: Bool)
lambda y_0123456789 _z_0123456789 = y_0123456789
in lambda sY_0123456789 _s_z_0123456789 } ::
Sing (Case_0123456789 X_0123456789Sym0 :: Bool)
sK
= case sX_0123456789 of {
SBar _s_z_0123456789 sY_0123456789
-> let
lambda ::
forall _z_0123456789 y_0123456789.
Apply (Apply BarSym0 _z_0123456789) y_0123456789 ~ X_0123456789Sym0 =>
Sing _z_0123456789
-> Sing y_0123456789
-> Sing (Case_0123456789 (Apply (Apply BarSym0 _z_0123456789) y_0123456789) :: Bool)
lambda _z_0123456789 y_0123456789 = y_0123456789
in lambda _s_z_0123456789 sY_0123456789 } ::
Sing (Case_0123456789 X_0123456789Sym0 :: Bool)
sL
= case sX_0123456789 of {
SCons sY_0123456789 (SCons _s_z_0123456789 SNil)
-> let
lambda ::
forall y_0123456789 _z_0123456789.
Apply (Apply (:$) y_0123456789) (Apply (Apply (:$) _z_0123456789) '[]) ~ X_0123456789Sym0 =>
Sing y_0123456789
-> Sing _z_0123456789
-> Sing (Case_0123456789 (Apply (Apply (:$) y_0123456789) (Apply (Apply (:$) _z_0123456789) '[])) :: Bool)
lambda y_0123456789 _z_0123456789 = y_0123456789
in lambda sY_0123456789 _s_z_0123456789 } ::
Sing (Case_0123456789 X_0123456789Sym0 :: Bool)
sM
= case sX_0123456789 of {
SCons _s_z_0123456789 (SCons sY_0123456789 SNil)
-> let
lambda ::
forall _z_0123456789 y_0123456789.
Apply (Apply (:$) _z_0123456789) (Apply (Apply (:$) y_0123456789) '[]) ~ X_0123456789Sym0 =>
Sing _z_0123456789
-> Sing y_0123456789
-> Sing (Case_0123456789 (Apply (Apply (:$) _z_0123456789) (Apply (Apply (:$) y_0123456789) '[])) :: Bool)
lambda _z_0123456789 y_0123456789 = y_0123456789
in lambda _s_z_0123456789 sY_0123456789 } ::
Sing (Case_0123456789 X_0123456789Sym0 :: Bool)
sOtherwise = STrue
sX_0123456789
= applySing
(applySing
(singFun2 (Proxy :: Proxy (:$)) SCons)
(singFun1 (Proxy :: Proxy NotSym0) sNot))
(applySing
(applySing
(singFun2 (Proxy :: Proxy (:$)) SCons)
(singFun1 (Proxy :: Proxy IdSym0) sId))
SNil)
sX_0123456789
= applySing
(applySing
(singFun2 (Proxy :: Proxy Tuple2Sym0) STuple2)
(singFun1 (Proxy :: Proxy FSym0) sF))
(singFun1 (Proxy :: Proxy GSym0) sG)
sX_0123456789
= applySing
(applySing (singFun2 (Proxy :: Proxy BarSym0) SBar) STrue)
(applySing (singFun1 (Proxy :: Proxy HSym0) sH) SFalse)
sX_0123456789
= applySing
(applySing
(singFun2 (Proxy :: Proxy (:$)) SCons)
(applySing (singFun1 (Proxy :: Proxy NotSym0) sNot) STrue))
(applySing
(applySing
(singFun2 (Proxy :: Proxy (:$)) SCons)
(applySing (singFun1 (Proxy :: Proxy IdSym0) sId) SFalse))
SNil)