singletons-2.4: tests/compile-and-dump/Singletons/TopLevelPatterns.ghc84.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. SameKind (Apply (BarSym1 l) arg) (BarSym2 l arg) =>
BarSym1KindInference
type instance Apply (BarSym1 l) l = Bar 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. SameKind (Apply BarSym0 arg) (BarSym1 arg) =>
BarSym0KindInference
type instance Apply BarSym0 l = BarSym1 l
data instance Sing (z :: Bool)
where
SFalse :: Sing False
STrue :: Sing True
type SBool = (Sing :: Bool -> GHC.Types.Type)
instance SingKind Bool where
type Demote Bool = Bool
fromSing SFalse = False
fromSing STrue = True
toSing False = SomeSing SFalse
toSing True = SomeSing STrue
data instance Sing (z :: Foo)
where
SBar :: forall (n :: Bool) (n :: Bool).
(Sing (n :: Bool)) -> (Sing (n :: Bool)) -> Sing (Bar n n)
type SFoo = (Sing :: Foo -> GHC.Types.Type)
instance SingKind Foo where
type Demote Foo = Foo
fromSing (SBar b b) = (Bar (fromSing b)) (fromSing b)
toSing (Bar (b :: Demote Bool) (b :: Demote Bool))
= 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 :: 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_0123456789876543210 a_0123456789876543210 t where
Case_0123456789876543210 a_0123456789876543210 '[y_0123456789876543210,
_] = y_0123456789876543210
type family Case_0123456789876543210 a_0123456789876543210 t where
Case_0123456789876543210 a_0123456789876543210 '[_,
y_0123456789876543210] = y_0123456789876543210
type family Case_0123456789876543210 a_0123456789876543210 t where
Case_0123456789876543210 a_0123456789876543210 '(y_0123456789876543210,
_) = y_0123456789876543210
type family Case_0123456789876543210 a_0123456789876543210 t where
Case_0123456789876543210 a_0123456789876543210 '(_,
y_0123456789876543210) = y_0123456789876543210
type family Case_0123456789876543210 t where
Case_0123456789876543210 (Bar y_0123456789876543210 _) = y_0123456789876543210
type family Case_0123456789876543210 t where
Case_0123456789876543210 (Bar _ y_0123456789876543210) = y_0123456789876543210
type family Case_0123456789876543210 t where
Case_0123456789876543210 '[y_0123456789876543210,
_] = y_0123456789876543210
type family Case_0123456789876543210 t where
Case_0123456789876543210 '[_,
y_0123456789876543210] = y_0123456789876543210
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. SameKind (Apply NotSym0 arg) (NotSym1 arg) =>
NotSym0KindInference
type instance Apply NotSym0 l = Not l
type IdSym1 (t :: a0123456789876543210) = Id t
instance SuppressUnusedWarnings IdSym0 where
suppressUnusedWarnings
= Data.Tuple.snd ((GHC.Tuple.(,) IdSym0KindInference) GHC.Tuple.())
data IdSym0 (l :: TyFun a0123456789876543210 a0123456789876543210)
= forall arg. SameKind (Apply IdSym0 arg) (IdSym1 arg) =>
IdSym0KindInference
type instance Apply IdSym0 l = Id 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. SameKind (Apply FSym0 arg) (FSym1 arg) =>
FSym0KindInference
type instance Apply FSym0 l = F 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. SameKind (Apply GSym0 arg) (GSym1 arg) =>
GSym0KindInference
type instance Apply GSym0 l = G 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. SameKind (Apply HSym0 arg) (HSym1 arg) =>
HSym0KindInference
type instance Apply HSym0 l = H 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. SameKind (Apply ISym0 arg) (ISym1 arg) =>
ISym0KindInference
type instance Apply ISym0 l = I l
type JSym0 = J
type KSym0 = K
type LSym0 = L
type MSym0 = M
type OtherwiseSym0 = Otherwise
type X_0123456789876543210Sym0 = X_0123456789876543210
type X_0123456789876543210Sym0 = X_0123456789876543210
type X_0123456789876543210Sym0 = X_0123456789876543210
type X_0123456789876543210Sym0 = X_0123456789876543210
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_0123456789876543210 = Apply (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0) a_0123456789876543210
type family G (a :: Bool) :: Bool where
G a_0123456789876543210 = Apply (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0) a_0123456789876543210
type family H (a :: Bool) :: Bool where
H a_0123456789876543210 = Apply (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0) a_0123456789876543210
type family I (a :: Bool) :: Bool where
I a_0123456789876543210 = Apply (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0) a_0123456789876543210
type family J :: Bool where
J = Case_0123456789876543210 X_0123456789876543210Sym0
type family K :: Bool where
K = Case_0123456789876543210 X_0123456789876543210Sym0
type family L :: Bool where
L = Case_0123456789876543210 X_0123456789876543210Sym0
type family M :: Bool where
M = Case_0123456789876543210 X_0123456789876543210Sym0
type family Otherwise :: Bool where
Otherwise = TrueSym0
type family X_0123456789876543210 where
X_0123456789876543210 = Apply (Apply (:@#@$) NotSym0) (Apply (Apply (:@#@$) IdSym0) '[])
type family X_0123456789876543210 where
X_0123456789876543210 = Apply (Apply Tuple2Sym0 FSym0) GSym0
type family X_0123456789876543210 where
X_0123456789876543210 = Apply (Apply BarSym0 TrueSym0) (Apply HSym0 FalseSym0)
type family X_0123456789876543210 where
X_0123456789876543210 = 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_0123456789876543210 :: Sing X_0123456789876543210Sym0
sX_0123456789876543210 :: Sing X_0123456789876543210Sym0
sX_0123456789876543210 :: Sing X_0123456789876543210Sym0
sX_0123456789876543210 :: Sing X_0123456789876543210Sym0
sFalse_ = SFalse
sNot STrue = SFalse
sNot SFalse = STrue
sId (sX :: Sing x) = sX
sF (sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
(case sX_0123456789876543210 of {
SCons (sY_0123456789876543210 :: Sing y_0123456789876543210)
(SCons _ SNil)
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0)))
sA_0123456789876543210
sG (sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
(case sX_0123456789876543210 of {
SCons _
(SCons (sY_0123456789876543210 :: Sing y_0123456789876543210) SNil)
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0)))
sA_0123456789876543210
sH (sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
(case sX_0123456789876543210 of {
STuple2 (sY_0123456789876543210 :: Sing y_0123456789876543210) _
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0)))
sA_0123456789876543210
sI (sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
(case sX_0123456789876543210 of {
STuple2 _ (sY_0123456789876543210 :: Sing y_0123456789876543210)
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0)))
sA_0123456789876543210
sJ
= case sX_0123456789876543210 of {
SBar (sY_0123456789876543210 :: Sing y_0123456789876543210) _
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Bool)
sK
= case sX_0123456789876543210 of {
SBar _ (sY_0123456789876543210 :: Sing y_0123456789876543210)
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Bool)
sL
= case sX_0123456789876543210 of {
SCons (sY_0123456789876543210 :: Sing y_0123456789876543210)
(SCons _ SNil)
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Bool)
sM
= case sX_0123456789876543210 of {
SCons _
(SCons (sY_0123456789876543210 :: Sing y_0123456789876543210) SNil)
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Bool)
sOtherwise = STrue
sX_0123456789876543210
= (applySing
((applySing ((singFun2 @(:@#@$)) SCons))
((singFun1 @NotSym0) sNot)))
((applySing
((applySing ((singFun2 @(:@#@$)) SCons)) ((singFun1 @IdSym0) sId)))
SNil)
sX_0123456789876543210
= (applySing
((applySing ((singFun2 @Tuple2Sym0) STuple2))
((singFun1 @FSym0) sF)))
((singFun1 @GSym0) sG)
sX_0123456789876543210
= (applySing ((applySing ((singFun2 @BarSym0) SBar)) STrue))
((applySing ((singFun1 @HSym0) sH)) SFalse)
sX_0123456789876543210
= (applySing
((applySing ((singFun2 @(:@#@$)) SCons))
((applySing ((singFun1 @NotSym0) sNot)) STrue)))
((applySing
((applySing ((singFun2 @(:@#@$)) SCons))
((applySing ((singFun1 @IdSym0) sId)) SFalse)))
SNil)