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