singletons-2.4: tests/compile-and-dump/Singletons/PatternMatching.ghc84.template
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 PairSym2 (t :: a0123456789876543210) (t :: b0123456789876543210) =
Pair t t
instance SuppressUnusedWarnings PairSym1 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) PairSym1KindInference) GHC.Tuple.())
data PairSym1 (l :: a0123456789876543210) (l :: TyFun b0123456789876543210 (Pair a0123456789876543210 b0123456789876543210))
= forall arg. SameKind (Apply (PairSym1 l) arg) (PairSym2 l arg) =>
PairSym1KindInference
type instance Apply (PairSym1 l) l = Pair l l
instance SuppressUnusedWarnings PairSym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) PairSym0KindInference) GHC.Tuple.())
data PairSym0 (l :: TyFun a0123456789876543210 (TyFun b0123456789876543210 (Pair a0123456789876543210 b0123456789876543210)
-> GHC.Types.Type))
= forall arg. SameKind (Apply PairSym0 arg) (PairSym1 arg) =>
PairSym0KindInference
type instance Apply PairSym0 l = PairSym1 l
type AListSym0 = AList
type TupleSym0 = Tuple
type ComplexSym0 = Complex
type PrSym0 = Pr
type family AList where
AList = Apply (Apply (:@#@$) ZeroSym0) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))) '[]))
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) '[])
type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: Pair a b) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 p_0123456789876543210 (Pair arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = 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
type ShowsPrec_0123456789876543210Sym3 (t :: GHC.Types.Nat) (t :: Pair a0123456789876543210 b0123456789876543210) (t :: Symbol) =
ShowsPrec_0123456789876543210 t t t
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym2 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym2KindInference)
GHC.Tuple.())
data ShowsPrec_0123456789876543210Sym2 (l :: GHC.Types.Nat) (l :: Pair a0123456789876543210 b0123456789876543210) (l :: TyFun Symbol Symbol)
= forall arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 l l) arg) (ShowsPrec_0123456789876543210Sym3 l l arg) =>
ShowsPrec_0123456789876543210Sym2KindInference
type instance Apply (ShowsPrec_0123456789876543210Sym2 l l) l = ShowsPrec_0123456789876543210 l l l
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym1 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym1KindInference)
GHC.Tuple.())
data ShowsPrec_0123456789876543210Sym1 (l :: GHC.Types.Nat) (l :: TyFun (Pair a0123456789876543210 b0123456789876543210) (TyFun Symbol Symbol
-> GHC.Types.Type))
= forall arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 l) arg) (ShowsPrec_0123456789876543210Sym2 l arg) =>
ShowsPrec_0123456789876543210Sym1KindInference
type instance Apply (ShowsPrec_0123456789876543210Sym1 l) l = ShowsPrec_0123456789876543210Sym2 l l
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym0KindInference)
GHC.Tuple.())
data ShowsPrec_0123456789876543210Sym0 (l :: TyFun GHC.Types.Nat (TyFun (Pair a0123456789876543210 b0123456789876543210) (TyFun Symbol Symbol
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
ShowsPrec_0123456789876543210Sym0KindInference
type instance Apply ShowsPrec_0123456789876543210Sym0 l = ShowsPrec_0123456789876543210Sym1 l
instance PShow (Pair a b) where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
sAList :: Sing AListSym0
sTuple :: Sing TupleSym0
sComplex :: Sing ComplexSym0
sPr :: Sing PrSym0
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 instance Sing (z :: Pair a b)
where
SPair :: forall (n :: a) (n :: b).
(Sing (n :: a)) -> (Sing (n :: b)) -> Sing (Pair n n)
type SPair = (Sing :: Pair a b -> GHC.Types.Type)
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))
= case
(GHC.Tuple.(,) (toSing b :: SomeSing a)) (toSing b :: SomeSing b)
of {
GHC.Tuple.(,) (SomeSing c) (SomeSing c) -> SomeSing ((SPair c) c) }
instance (SShow a, SShow b) => SShow (Pair a b) where
sShowsPrec ::
forall (t1 :: GHC.Types.Nat) (t2 :: Pair a b) (t3 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat (TyFun (Pair a b) (TyFun Symbol Symbol
-> GHC.Types.Type)
-> GHC.Types.Type)
-> GHC.Types.Type) t1) t2) t3)
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
instance (Data.Singletons.ShowSing.ShowSing a,
Data.Singletons.ShowSing.ShowSing b) =>
Data.Singletons.ShowSing.ShowSing (Pair a b) where
Data.Singletons.ShowSing.showsSingPrec
p_0123456789876543210
(SPair arg_0123456789876543210 arg_0123456789876543210)
= (showParen (((>) p_0123456789876543210) 10))
(((.) (showString "SPair "))
(((.)
((Data.Singletons.ShowSing.showsSingPrec 11)
arg_0123456789876543210))
(((.) GHC.Show.showSpace)
((Data.Singletons.ShowSing.showsSingPrec 11)
arg_0123456789876543210))))
instance (Data.Singletons.ShowSing.ShowSing a,
Data.Singletons.ShowSing.ShowSing b) =>
Show (Sing (z :: Pair a b)) where
showsPrec = Data.Singletons.ShowSing.showsSingPrec
instance (SingI n, SingI n) => SingI (Pair (n :: a) (n :: b)) where
sing = (SPair sing) sing
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 { _ -> GHC.Tuple.() }
type family Case_0123456789876543210 x t where
Case_0123456789876543210 x _ = Tuple0Sym0
type Let0123456789876543210TSym2 t t = Let0123456789876543210T t t
instance SuppressUnusedWarnings Let0123456789876543210TSym1 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Let0123456789876543210TSym1KindInference)
GHC.Tuple.())
data Let0123456789876543210TSym1 l l
= forall arg. SameKind (Apply (Let0123456789876543210TSym1 l) arg) (Let0123456789876543210TSym2 l arg) =>
Let0123456789876543210TSym1KindInference
type instance Apply (Let0123456789876543210TSym1 l) l = Let0123456789876543210T l l
instance SuppressUnusedWarnings Let0123456789876543210TSym0 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Let0123456789876543210TSym0KindInference)
GHC.Tuple.())
data Let0123456789876543210TSym0 l
= forall arg. SameKind (Apply Let0123456789876543210TSym0 arg) (Let0123456789876543210TSym1 arg) =>
Let0123456789876543210TSym0KindInference
type instance Apply Let0123456789876543210TSym0 l = Let0123456789876543210TSym1 l
type family Let0123456789876543210T x y where
Let0123456789876543210T x y = Apply (Apply Tuple2Sym0 x) y
type family Case_0123456789876543210 x y a b arg_0123456789876543210 t where
Case_0123456789876543210 x y a b arg_0123456789876543210 _ = a
type family Lambda_0123456789876543210 x y a b t where
Lambda_0123456789876543210 x y a b arg_0123456789876543210 = Case_0123456789876543210 x y a b arg_0123456789876543210 arg_0123456789876543210
type Lambda_0123456789876543210Sym5 t t t t t =
Lambda_0123456789876543210 t t t t t
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym4 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Lambda_0123456789876543210Sym4KindInference)
GHC.Tuple.())
data Lambda_0123456789876543210Sym4 l l l l l
= forall arg. SameKind (Apply (Lambda_0123456789876543210Sym4 l l l l) arg) (Lambda_0123456789876543210Sym5 l l l l arg) =>
Lambda_0123456789876543210Sym4KindInference
type instance Apply (Lambda_0123456789876543210Sym4 l l l l) l = Lambda_0123456789876543210 l l l l l
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym3 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Lambda_0123456789876543210Sym3KindInference)
GHC.Tuple.())
data Lambda_0123456789876543210Sym3 l l l l
= forall arg. SameKind (Apply (Lambda_0123456789876543210Sym3 l l l) arg) (Lambda_0123456789876543210Sym4 l l l arg) =>
Lambda_0123456789876543210Sym3KindInference
type instance Apply (Lambda_0123456789876543210Sym3 l l l) l = Lambda_0123456789876543210Sym4 l l l l
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym2 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Lambda_0123456789876543210Sym2KindInference)
GHC.Tuple.())
data Lambda_0123456789876543210Sym2 l l l
= forall arg. SameKind (Apply (Lambda_0123456789876543210Sym2 l l) arg) (Lambda_0123456789876543210Sym3 l l arg) =>
Lambda_0123456789876543210Sym2KindInference
type instance Apply (Lambda_0123456789876543210Sym2 l l) l = Lambda_0123456789876543210Sym3 l l l
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym1 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Lambda_0123456789876543210Sym1KindInference)
GHC.Tuple.())
data Lambda_0123456789876543210Sym1 l l
= forall arg. SameKind (Apply (Lambda_0123456789876543210Sym1 l) arg) (Lambda_0123456789876543210Sym2 l arg) =>
Lambda_0123456789876543210Sym1KindInference
type instance Apply (Lambda_0123456789876543210Sym1 l) l = Lambda_0123456789876543210Sym2 l l
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Lambda_0123456789876543210Sym0KindInference)
GHC.Tuple.())
data Lambda_0123456789876543210Sym0 l
= forall arg. SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0KindInference
type instance Apply Lambda_0123456789876543210Sym0 l = Lambda_0123456789876543210Sym1 l
type family Case_0123456789876543210 x y t where
Case_0123456789876543210 x y '(a,
b) = Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) y) a) b) b
type family Case_0123456789876543210 x y arg_0123456789876543210 t where
Case_0123456789876543210 x y arg_0123456789876543210 _ = x
type family Lambda_0123456789876543210 x y t where
Lambda_0123456789876543210 x y arg_0123456789876543210 = Case_0123456789876543210 x y arg_0123456789876543210 arg_0123456789876543210
type Lambda_0123456789876543210Sym3 t t t =
Lambda_0123456789876543210 t t t
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym2 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Lambda_0123456789876543210Sym2KindInference)
GHC.Tuple.())
data Lambda_0123456789876543210Sym2 l l l
= forall arg. SameKind (Apply (Lambda_0123456789876543210Sym2 l l) arg) (Lambda_0123456789876543210Sym3 l l arg) =>
Lambda_0123456789876543210Sym2KindInference
type instance Apply (Lambda_0123456789876543210Sym2 l l) l = Lambda_0123456789876543210 l l l
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym1 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Lambda_0123456789876543210Sym1KindInference)
GHC.Tuple.())
data Lambda_0123456789876543210Sym1 l l
= forall arg. SameKind (Apply (Lambda_0123456789876543210Sym1 l) arg) (Lambda_0123456789876543210Sym2 l arg) =>
Lambda_0123456789876543210Sym1KindInference
type instance Apply (Lambda_0123456789876543210Sym1 l) l = Lambda_0123456789876543210Sym2 l l
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Lambda_0123456789876543210Sym0KindInference)
GHC.Tuple.())
data Lambda_0123456789876543210Sym0 l
= forall arg. SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0KindInference
type instance Apply Lambda_0123456789876543210Sym0 l = Lambda_0123456789876543210Sym1 l
type family Case_0123456789876543210 t where
Case_0123456789876543210 '[_,
y_0123456789876543210,
Succ _] = y_0123456789876543210
type family Case_0123456789876543210 t where
Case_0123456789876543210 '[_,
_,
Succ 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 family Case_0123456789876543210 t where
Case_0123456789876543210 '(_,
_,
y_0123456789876543210) = y_0123456789876543210
type family Case_0123456789876543210 t where
Case_0123456789876543210 (Pair (Pair y_0123456789876543210 _) _) = y_0123456789876543210
type family Case_0123456789876543210 t where
Case_0123456789876543210 (Pair (Pair _ y_0123456789876543210) _) = y_0123456789876543210
type family Case_0123456789876543210 t where
Case_0123456789876543210 (Pair (Pair _ _) y_0123456789876543210) = y_0123456789876543210
type family Case_0123456789876543210 t where
Case_0123456789876543210 (Pair y_0123456789876543210 _) = y_0123456789876543210
type family Case_0123456789876543210 t where
Case_0123456789876543210 (Pair _ y_0123456789876543210) = y_0123456789876543210
type SillySym1 (t :: a0123456789876543210) = Silly t
instance SuppressUnusedWarnings SillySym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) SillySym0KindInference) GHC.Tuple.())
data SillySym0 (l :: TyFun a0123456789876543210 ())
= forall arg. SameKind (Apply SillySym0 arg) (SillySym1 arg) =>
SillySym0KindInference
type instance Apply SillySym0 l = Silly l
type Foo2Sym1 (t :: (a0123456789876543210, b0123456789876543210)) =
Foo2 t
instance SuppressUnusedWarnings Foo2Sym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) Foo2Sym0KindInference) GHC.Tuple.())
data Foo2Sym0 (l :: TyFun (a0123456789876543210,
b0123456789876543210) a0123456789876543210)
= forall arg. SameKind (Apply Foo2Sym0 arg) (Foo2Sym1 arg) =>
Foo2Sym0KindInference
type instance Apply Foo2Sym0 l = Foo2 l
type Foo1Sym1 (t :: (a0123456789876543210, b0123456789876543210)) =
Foo1 t
instance SuppressUnusedWarnings Foo1Sym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) Foo1Sym0KindInference) GHC.Tuple.())
data Foo1Sym0 (l :: TyFun (a0123456789876543210,
b0123456789876543210) a0123456789876543210)
= forall arg. SameKind (Apply Foo1Sym0 arg) (Foo1Sym1 arg) =>
Foo1Sym0KindInference
type instance Apply Foo1Sym0 l = Foo1 l
type LszSym0 = Lsz
type BlimySym0 = Blimy
type TfSym0 = Tf
type TjzSym0 = Tjz
type TtSym0 = Tt
type JzSym0 = Jz
type ZzSym0 = Zz
type FlsSym0 = Fls
type SzSym0 = Sz
type LzSym0 = Lz
type X_0123456789876543210Sym0 = X_0123456789876543210
type X_0123456789876543210Sym0 = X_0123456789876543210
type X_0123456789876543210Sym0 = X_0123456789876543210
type X_0123456789876543210Sym0 = X_0123456789876543210
type family Silly (a :: a) :: () where
Silly x = Case_0123456789876543210 x x
type family Foo2 (a :: (a, b)) :: a where
Foo2 '(x,
y) = Case_0123456789876543210 x y (Let0123456789876543210TSym2 x y)
type family Foo1 (a :: (a, b)) :: a where
Foo1 '(x,
y) = Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) y) y
type family Lsz :: Nat where
Lsz = Case_0123456789876543210 X_0123456789876543210Sym0
type family Blimy where
Blimy = Case_0123456789876543210 X_0123456789876543210Sym0
type family Tf where
Tf = Case_0123456789876543210 X_0123456789876543210Sym0
type family Tjz where
Tjz = Case_0123456789876543210 X_0123456789876543210Sym0
type family Tt where
Tt = Case_0123456789876543210 X_0123456789876543210Sym0
type family Jz where
Jz = Case_0123456789876543210 X_0123456789876543210Sym0
type family Zz where
Zz = Case_0123456789876543210 X_0123456789876543210Sym0
type family Fls :: Bool where
Fls = Case_0123456789876543210 X_0123456789876543210Sym0
type family Sz where
Sz = Case_0123456789876543210 X_0123456789876543210Sym0
type family Lz where
Lz = Case_0123456789876543210 X_0123456789876543210Sym0
type family X_0123456789876543210 where
X_0123456789876543210 = PrSym0
type family X_0123456789876543210 where
X_0123456789876543210 = ComplexSym0
type family X_0123456789876543210 where
X_0123456789876543210 = TupleSym0
type family X_0123456789876543210 where
X_0123456789876543210 = AListSym0
sSilly :: forall (t :: a). Sing t -> Sing (Apply SillySym0 t :: ())
sFoo2 ::
forall (t :: (a, b)). Sing t -> Sing (Apply Foo2Sym0 t :: a)
sFoo1 ::
forall (t :: (a, b)). Sing t -> Sing (Apply Foo1Sym0 t :: a)
sLsz :: Sing (LszSym0 :: Nat)
sBlimy :: Sing BlimySym0
sTf :: Sing TfSym0
sTjz :: Sing TjzSym0
sTt :: Sing TtSym0
sJz :: Sing JzSym0
sZz :: Sing ZzSym0
sFls :: Sing (FlsSym0 :: Bool)
sSz :: Sing SzSym0
sLz :: Sing LzSym0
sX_0123456789876543210 :: Sing X_0123456789876543210Sym0
sX_0123456789876543210 :: Sing X_0123456789876543210Sym0
sX_0123456789876543210 :: Sing X_0123456789876543210Sym0
sX_0123456789876543210 :: Sing X_0123456789876543210Sym0
sSilly (sX :: Sing x)
= case sX of { _ -> STuple0 } ::
Sing (Case_0123456789876543210 x x :: ())
sFoo2 (STuple2 (sX :: Sing x) (sY :: Sing y))
= let
sT :: Sing (Let0123456789876543210TSym2 x y)
sT
= (applySing ((applySing ((singFun2 @Tuple2Sym0) STuple2)) sX)) sY
in case sT of {
STuple2 (sA :: Sing a) (sB :: Sing b)
-> (applySing
((singFun1
@(Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) y) a) b))
(\ sArg_0123456789876543210
-> case sArg_0123456789876543210 of {
_ :: Sing arg_0123456789876543210
-> case sArg_0123456789876543210 of { _ -> sA } ::
Sing (Case_0123456789876543210 x y a b arg_0123456789876543210 arg_0123456789876543210) })))
sB } ::
Sing (Case_0123456789876543210 x y (Let0123456789876543210TSym2 x y) :: a)
sFoo1 (STuple2 (sX :: Sing x) (sY :: Sing y))
= (applySing
((singFun1 @(Apply (Apply Lambda_0123456789876543210Sym0 x) y))
(\ sArg_0123456789876543210
-> case sArg_0123456789876543210 of {
_ :: Sing arg_0123456789876543210
-> case sArg_0123456789876543210 of { _ -> sX } ::
Sing (Case_0123456789876543210 x y arg_0123456789876543210 arg_0123456789876543210) })))
sY
sLsz
= case sX_0123456789876543210 of {
SCons _
(SCons (sY_0123456789876543210 :: Sing y_0123456789876543210)
(SCons (SSucc _) SNil))
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Nat)
sBlimy
= case sX_0123456789876543210 of {
SCons _
(SCons _
(SCons (SSucc (sY_0123456789876543210 :: Sing y_0123456789876543210))
SNil))
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0)
sTf
= case sX_0123456789876543210 of {
STuple3 (sY_0123456789876543210 :: Sing y_0123456789876543210) _ _
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0)
sTjz
= case sX_0123456789876543210 of {
STuple3 _ (sY_0123456789876543210 :: Sing y_0123456789876543210) _
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0)
sTt
= case sX_0123456789876543210 of {
STuple3 _ _ (sY_0123456789876543210 :: Sing y_0123456789876543210)
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0)
sJz
= case sX_0123456789876543210 of {
SPair (SPair (sY_0123456789876543210 :: Sing y_0123456789876543210)
_)
_
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0)
sZz
= case sX_0123456789876543210 of {
SPair (SPair _
(sY_0123456789876543210 :: Sing y_0123456789876543210))
_
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0)
sFls
= case sX_0123456789876543210 of {
SPair (SPair _ _)
(sY_0123456789876543210 :: Sing y_0123456789876543210)
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Bool)
sSz
= case sX_0123456789876543210 of {
SPair (sY_0123456789876543210 :: Sing y_0123456789876543210) _
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0)
sLz
= case sX_0123456789876543210 of {
SPair _ (sY_0123456789876543210 :: Sing y_0123456789876543210)
-> sY_0123456789876543210 } ::
Sing (Case_0123456789876543210 X_0123456789876543210Sym0)
sX_0123456789876543210 = sPr
sX_0123456789876543210 = sComplex
sX_0123456789876543210 = sTuple
sX_0123456789876543210 = sAList