singletons-base-3.5: tests/compile-and-dump/Singletons/PatternMatching.golden
Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| pr = Pair (Succ Zero) ([Zero])
complex = Pair (Pair (Just Zero) Zero) False
tuple = (False, Just Zero, True)
aList = [Zero, Succ Zero, Succ (Succ Zero)]
data Pair a b
= Pair a b
deriving Show |]
======>
data Pair a b
= Pair a b
deriving Show
pr = Pair (Succ Zero) [Zero]
complex = Pair (Pair (Just Zero) Zero) False
tuple = (False, Just Zero, True)
aList = [Zero, Succ Zero, Succ (Succ Zero)]
type PairSym0 :: forall a b. (~>) a ((~>) b (Pair a b))
data PairSym0 :: (~>) a ((~>) b (Pair a b))
where
PairSym0KindInference :: SameKind (Apply PairSym0 arg) (PairSym1 arg) =>
PairSym0 a0123456789876543210
type instance Apply @a @((~>) b (Pair a b)) PairSym0 a0123456789876543210 = PairSym1 a0123456789876543210
instance SuppressUnusedWarnings PairSym0 where
suppressUnusedWarnings = snd ((,) PairSym0KindInference ())
type PairSym1 :: forall a b. a -> (~>) b (Pair a b)
data PairSym1 (a0123456789876543210 :: a) :: (~>) b (Pair a b)
where
PairSym1KindInference :: SameKind (Apply (PairSym1 a0123456789876543210) arg) (PairSym2 a0123456789876543210 arg) =>
PairSym1 a0123456789876543210 a0123456789876543210
type instance Apply @b @(Pair a b) (PairSym1 a0123456789876543210) a0123456789876543210 = Pair a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (PairSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) PairSym1KindInference ())
type PairSym2 :: forall a b. a -> b -> Pair a b
type family PairSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where
PairSym2 a0123456789876543210 a0123456789876543210 = Pair a0123456789876543210 a0123456789876543210
type family AListSym0 where
AListSym0 = AList
type family TupleSym0 where
TupleSym0 = Tuple
type family ComplexSym0 where
ComplexSym0 = Complex
type family PrSym0 where
PrSym0 = Pr
type family AList where
AList = Apply (Apply (:@#@$) ZeroSym0) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))) NilSym0))
type family Tuple where
Tuple = Apply (Apply (Apply Tuple3Sym0 FalseSym0) (Apply JustSym0 ZeroSym0)) TrueSym0
type family Complex where
Complex = Apply (Apply PairSym0 (Apply (Apply PairSym0 (Apply JustSym0 ZeroSym0)) ZeroSym0)) FalseSym0
type family Pr where
Pr = Apply (Apply PairSym0 (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) ZeroSym0) NilSym0)
type ShowsPrec_0123456789876543210 :: forall a
b. GHC.Num.Natural.Natural
-> Pair a b -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 @a @b (a :: GHC.Num.Natural.Natural) (a :: Pair a b) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 @a @b (p_0123456789876543210 :: GHC.Num.Natural.Natural) (Pair arg_0123456789876543210 arg_0123456789876543210 :: Pair a b) (a_0123456789876543210 :: Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Pair ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
instance PShow (Pair a b) where
type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
sAList :: Sing @_ AList
sTuple :: Sing @_ Tuple
sComplex :: Sing @_ Complex
sPr :: Sing @_ Pr
sAList
= applySing
(applySing (singFun2 @(:@#@$) SCons) SZero)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing (singFun1 @SuccSym0 SSucc) SZero))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(singFun1 @SuccSym0 SSucc)
(applySing (singFun1 @SuccSym0 SSucc) SZero)))
SNil))
sTuple
= applySing
(applySing
(applySing (singFun3 @Tuple3Sym0 STuple3) SFalse)
(applySing (singFun1 @JustSym0 SJust) SZero))
STrue
sComplex
= applySing
(applySing
(singFun2 @PairSym0 SPair)
(applySing
(applySing
(singFun2 @PairSym0 SPair)
(applySing (singFun1 @JustSym0 SJust) SZero))
SZero))
SFalse
sPr
= applySing
(applySing
(singFun2 @PairSym0 SPair)
(applySing (singFun1 @SuccSym0 SSucc) SZero))
(applySing (applySing (singFun2 @(:@#@$) SCons) SZero) SNil)
data SPair :: forall a b. Pair a b -> Type
where
SPair :: forall a b (n :: a) (n :: b).
(Sing n) -> (Sing n) -> SPair (Pair n n :: Pair a b)
type instance Sing @(Pair a b) = SPair
instance (SingKind a, SingKind b) => SingKind (Pair a b) where
type Demote (Pair a b) = Pair (Demote a) (Demote b)
fromSing (SPair b b) = Pair (fromSing b) (fromSing b)
toSing (Pair (b :: Demote a) (b :: Demote b))
= (\cases (SomeSing c) (SomeSing c) -> SomeSing (SPair c c))
(toSing b :: SomeSing a) (toSing b :: SomeSing b)
instance (SShow a, SShow b) => SShow (Pair a b) where
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
(SPair (sArg_0123456789876543210 :: Sing arg_0123456789876543210)
(sArg_0123456789876543210 :: Sing arg_0123456789876543210))
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(applySing
(singFun3 @ShowParenSym0 sShowParen)
(applySing
(applySing (singFun2 @(>@#@$) (%>)) sP_0123456789876543210)
(sFromInteger (sing :: Sing 10))))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Pair ")))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 11)))
sArg_0123456789876543210))
(applySing
(applySing
(singFun3 @(.@#@$) (%.)) (singFun1 @ShowSpaceSym0 sShowSpace))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 11)))
sArg_0123456789876543210)))))
sA_0123456789876543210
deriving instance (Data.Singletons.ShowSing.ShowSing a,
Data.Singletons.ShowSing.ShowSing b) =>
Show (SPair (z :: Pair a b))
instance (SingI n, SingI n) => SingI (Pair (n :: a) (n :: b)) where
sing = SPair sing sing
instance SingI n => SingI1 (Pair (n :: a)) where
liftSing = SPair sing
instance SingI2 Pair where
liftSing2 = SPair
instance SingI (PairSym0 :: (~>) a ((~>) b (Pair a b))) where
sing = singFun2 @PairSym0 SPair
instance SingI d =>
SingI (PairSym1 (d :: a) :: (~>) b (Pair a b)) where
sing = singFun1 @(PairSym1 (d :: a)) (SPair (sing @d))
instance SingI1 (PairSym1 :: a -> (~>) b (Pair a b)) where
liftSing (s :: Sing (d :: a))
= singFun1 @(PairSym1 (d :: a)) (SPair s)
Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| Pair sz lz = pr
Pair (Pair jz zz) fls = complex
(tf, tjz, tt) = tuple
[_, lsz, (Succ blimy)] = aList
lsz :: Nat
fls :: Bool
foo1 :: (a, b) -> a
foo1 (x, y) = (\ _ -> x) y
foo2 :: (# a, b #) -> a
foo2 t@(# x, y #) = case t of (# a, b #) -> (\ _ -> a) b
silly :: a -> ()
silly x = case x of _ -> () |]
======>
Pair sz lz = pr
Pair (Pair jz zz) fls = complex
(tf, tjz, tt) = tuple
[_, lsz, Succ blimy] = aList
lsz :: Nat
fls :: Bool
foo1 :: (a, b) -> a
foo1 (x, y) = (\ _ -> x) y
foo2 :: (# a, b #) -> a
foo2 t@(# x, y #) = case t of (# a, b #) -> (\ _ -> a) b
silly :: a -> ()
silly x = case x of _ -> ()
type family LamCases_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) a_0123456789876543210 where
LamCases_0123456789876543210 x _ = Tuple0Sym0
data LamCases_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 x0123456789876543210) arg) (LamCases_0123456789876543210Sym1 x0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 x0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 x0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 x0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 (x0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 x0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type family Let0123456789876543210TSym0 x0123456789876543210 y0123456789876543210 where
Let0123456789876543210TSym0 x0123456789876543210 y0123456789876543210 = Let0123456789876543210T x0123456789876543210 y0123456789876543210
type family Let0123456789876543210T x0123456789876543210 y0123456789876543210 where
Let0123456789876543210T x y = Apply (Apply Tuple2Sym0 x) y
type family LamCases_0123456789876543210 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 a b x y _ = a
data LamCases_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210) arg) (LamCases_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 x0123456789876543210 y0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 x y '(a,
b) = Apply (LamCases_0123456789876543210Sym0 a b x y) b
data LamCases_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) arg) (LamCases_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 x0123456789876543210 y0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 x y _ = x
data LamCases_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) arg) (LamCases_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 y0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 '[_,
_,
'Succ y_0123456789876543210] = y_0123456789876543210
data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 '[_,
y_0123456789876543210,
'Succ _] = y_0123456789876543210
data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 '(_,
_,
y_0123456789876543210) = y_0123456789876543210
data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 '(_,
y_0123456789876543210,
_) = y_0123456789876543210
data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 '(y_0123456789876543210,
_,
_) = y_0123456789876543210
data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 ('Pair ('Pair _ _) y_0123456789876543210) = y_0123456789876543210
data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 ('Pair ('Pair _ y_0123456789876543210) _) = y_0123456789876543210
data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 ('Pair ('Pair y_0123456789876543210 _) _) = y_0123456789876543210
data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 ('Pair _ y_0123456789876543210) = y_0123456789876543210
data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 ('Pair y_0123456789876543210 _) = y_0123456789876543210
data LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply @_ @_ LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210
type SillySym0 :: (~>) a ()
data SillySym0 :: (~>) a ()
where
SillySym0KindInference :: SameKind (Apply SillySym0 arg) (SillySym1 arg) =>
SillySym0 a0123456789876543210
type instance Apply @a @() SillySym0 a0123456789876543210 = Silly a0123456789876543210
instance SuppressUnusedWarnings SillySym0 where
suppressUnusedWarnings = snd ((,) SillySym0KindInference ())
type SillySym1 :: a -> ()
type family SillySym1 @a (a0123456789876543210 :: a) :: () where
SillySym1 a0123456789876543210 = Silly a0123456789876543210
type Foo2Sym0 :: (~>) (a, b) a
data Foo2Sym0 :: (~>) (a, b) a
where
Foo2Sym0KindInference :: SameKind (Apply Foo2Sym0 arg) (Foo2Sym1 arg) =>
Foo2Sym0 a0123456789876543210
type instance Apply @(a,
b) @a Foo2Sym0 a0123456789876543210 = Foo2 a0123456789876543210
instance SuppressUnusedWarnings Foo2Sym0 where
suppressUnusedWarnings = snd ((,) Foo2Sym0KindInference ())
type Foo2Sym1 :: (a, b) -> a
type family Foo2Sym1 @a @b (a0123456789876543210 :: (a,
b)) :: a where
Foo2Sym1 a0123456789876543210 = Foo2 a0123456789876543210
type Foo1Sym0 :: (~>) (a, b) a
data Foo1Sym0 :: (~>) (a, b) a
where
Foo1Sym0KindInference :: SameKind (Apply Foo1Sym0 arg) (Foo1Sym1 arg) =>
Foo1Sym0 a0123456789876543210
type instance Apply @(a,
b) @a Foo1Sym0 a0123456789876543210 = Foo1 a0123456789876543210
instance SuppressUnusedWarnings Foo1Sym0 where
suppressUnusedWarnings = snd ((,) Foo1Sym0KindInference ())
type Foo1Sym1 :: (a, b) -> a
type family Foo1Sym1 @a @b (a0123456789876543210 :: (a,
b)) :: a where
Foo1Sym1 a0123456789876543210 = Foo1 a0123456789876543210
type family BlimySym0 where
BlimySym0 = Blimy
type LszSym0 :: Nat
type family LszSym0 :: Nat where
LszSym0 = Lsz
type family X_0123456789876543210Sym0 where
X_0123456789876543210Sym0 = X_0123456789876543210
type family TtSym0 where
TtSym0 = Tt
type family TjzSym0 where
TjzSym0 = Tjz
type family TfSym0 where
TfSym0 = Tf
type family X_0123456789876543210Sym0 where
X_0123456789876543210Sym0 = X_0123456789876543210
type FlsSym0 :: Bool
type family FlsSym0 :: Bool where
FlsSym0 = Fls
type family ZzSym0 where
ZzSym0 = Zz
type family JzSym0 where
JzSym0 = Jz
type family X_0123456789876543210Sym0 where
X_0123456789876543210Sym0 = X_0123456789876543210
type family LzSym0 where
LzSym0 = Lz
type family SzSym0 where
SzSym0 = Sz
type family X_0123456789876543210Sym0 where
X_0123456789876543210Sym0 = X_0123456789876543210
type Silly :: a -> ()
type family Silly @a (a :: a) :: () where
Silly x = Apply (LamCases_0123456789876543210Sym0 x) x
type Foo2 :: (a, b) -> a
type family Foo2 @a @b (a :: (a, b)) :: a where
Foo2 '(x,
y) = Apply (LamCases_0123456789876543210Sym0 x y) (Let0123456789876543210TSym0 x y)
type Foo1 :: (a, b) -> a
type family Foo1 @a @b (a :: (a, b)) :: a where
Foo1 '(x, y) = Apply (LamCases_0123456789876543210Sym0 x y) y
type family Blimy where
Blimy = Apply LamCases_0123456789876543210Sym0 X_0123456789876543210Sym0
type Lsz :: Nat
type family Lsz :: Nat where
Lsz = Apply LamCases_0123456789876543210Sym0 X_0123456789876543210Sym0
type family X_0123456789876543210 where
X_0123456789876543210 = AListSym0
type family Tt where
Tt = Apply LamCases_0123456789876543210Sym0 X_0123456789876543210Sym0
type family Tjz where
Tjz = Apply LamCases_0123456789876543210Sym0 X_0123456789876543210Sym0
type family Tf where
Tf = Apply LamCases_0123456789876543210Sym0 X_0123456789876543210Sym0
type family X_0123456789876543210 where
X_0123456789876543210 = TupleSym0
type Fls :: Bool
type family Fls :: Bool where
Fls = Apply LamCases_0123456789876543210Sym0 X_0123456789876543210Sym0
type family Zz where
Zz = Apply LamCases_0123456789876543210Sym0 X_0123456789876543210Sym0
type family Jz where
Jz = Apply LamCases_0123456789876543210Sym0 X_0123456789876543210Sym0
type family X_0123456789876543210 where
X_0123456789876543210 = ComplexSym0
type family Lz where
Lz = Apply LamCases_0123456789876543210Sym0 X_0123456789876543210Sym0
type family Sz where
Sz = Apply LamCases_0123456789876543210Sym0 X_0123456789876543210Sym0
type family X_0123456789876543210 where
X_0123456789876543210 = PrSym0
sSilly :: (forall (t :: a). Sing t -> Sing (Silly t :: ()) :: Type)
sFoo2 ::
(forall (t :: (a, b)). Sing t -> Sing (Foo2 t :: a) :: Type)
sFoo1 ::
(forall (t :: (a, b)). Sing t -> Sing (Foo1 t :: a) :: Type)
sBlimy :: Sing @_ Blimy
sLsz :: (Sing (Lsz :: Nat) :: Type)
sX_0123456789876543210 :: Sing @_ X_0123456789876543210
sTt :: Sing @_ Tt
sTjz :: Sing @_ Tjz
sTf :: Sing @_ Tf
sX_0123456789876543210 :: Sing @_ X_0123456789876543210
sFls :: (Sing (Fls :: Bool) :: Type)
sZz :: Sing @_ Zz
sJz :: Sing @_ Jz
sX_0123456789876543210 :: Sing @_ X_0123456789876543210
sLz :: Sing @_ Lz
sSz :: Sing @_ Sz
sX_0123456789876543210 :: Sing @_ X_0123456789876543210
sSilly (sX :: Sing x)
= applySing
(singFun1
@(LamCases_0123456789876543210Sym0 x) (\cases _ -> STuple0))
sX
sFoo2 (STuple2 (sX :: Sing x) (sY :: Sing y))
= let
sT :: Sing @_ (Let0123456789876543210T x y)
sT = applySing (applySing (singFun2 @Tuple2Sym0 STuple2) sX) sY
in
applySing
(singFun1
@(LamCases_0123456789876543210Sym0 x y)
(\cases
(STuple2 (sA :: Sing a) (sB :: Sing b))
-> applySing
(singFun1
@(LamCases_0123456789876543210Sym0 a b x y) (\cases _ -> sA))
sB))
sT
sFoo1 (STuple2 (sX :: Sing x) (sY :: Sing y))
= applySing
(singFun1 @(LamCases_0123456789876543210Sym0 x y) (\cases _ -> sX))
sY
sBlimy
= applySing
(singFun1
@LamCases_0123456789876543210Sym0
(\cases
(SCons _
(SCons _
(SCons (SSucc (sY_0123456789876543210 :: Sing y_0123456789876543210))
SNil)))
-> sY_0123456789876543210))
sX_0123456789876543210
sLsz
= applySing
(singFun1
@LamCases_0123456789876543210Sym0
(\cases
(SCons _
(SCons (sY_0123456789876543210 :: Sing y_0123456789876543210)
(SCons (SSucc _) SNil)))
-> sY_0123456789876543210))
sX_0123456789876543210
sX_0123456789876543210 = sAList
sTt
= applySing
(singFun1
@LamCases_0123456789876543210Sym0
(\cases
(STuple3 _ _
(sY_0123456789876543210 :: Sing y_0123456789876543210))
-> sY_0123456789876543210))
sX_0123456789876543210
sTjz
= applySing
(singFun1
@LamCases_0123456789876543210Sym0
(\cases
(STuple3 _ (sY_0123456789876543210 :: Sing y_0123456789876543210)
_)
-> sY_0123456789876543210))
sX_0123456789876543210
sTf
= applySing
(singFun1
@LamCases_0123456789876543210Sym0
(\cases
(STuple3 (sY_0123456789876543210 :: Sing y_0123456789876543210) _
_)
-> sY_0123456789876543210))
sX_0123456789876543210
sX_0123456789876543210 = sTuple
sFls
= applySing
(singFun1
@LamCases_0123456789876543210Sym0
(\cases
(SPair (SPair _ _)
(sY_0123456789876543210 :: Sing y_0123456789876543210))
-> sY_0123456789876543210))
sX_0123456789876543210
sZz
= applySing
(singFun1
@LamCases_0123456789876543210Sym0
(\cases
(SPair (SPair _
(sY_0123456789876543210 :: Sing y_0123456789876543210))
_)
-> sY_0123456789876543210))
sX_0123456789876543210
sJz
= applySing
(singFun1
@LamCases_0123456789876543210Sym0
(\cases
(SPair (SPair (sY_0123456789876543210 :: Sing y_0123456789876543210)
_)
_)
-> sY_0123456789876543210))
sX_0123456789876543210
sX_0123456789876543210 = sComplex
sLz
= applySing
(singFun1
@LamCases_0123456789876543210Sym0
(\cases
(SPair _ (sY_0123456789876543210 :: Sing y_0123456789876543210))
-> sY_0123456789876543210))
sX_0123456789876543210
sSz
= applySing
(singFun1
@LamCases_0123456789876543210Sym0
(\cases
(SPair (sY_0123456789876543210 :: Sing y_0123456789876543210) _)
-> sY_0123456789876543210))
sX_0123456789876543210
sX_0123456789876543210 = sPr
instance SingI (SillySym0 :: (~>) a ()) where
sing = singFun1 @SillySym0 sSilly
instance SingI (Foo2Sym0 :: (~>) (a, b) a) where
sing = singFun1 @Foo2Sym0 sFoo2
instance SingI (Foo1Sym0 :: (~>) (a, b) a) where
sing = singFun1 @Foo1Sym0 sFoo1