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 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 (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 (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 :: GHC.Num.Natural.Natural -> Pair a b -> Symbol -> Symbol type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (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_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) where ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) => ShowsPrec_0123456789876543210Sym0 a0123456789876543210 type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) ShowsPrec_0123456789876543210Sym0KindInference ()) type ShowsPrec_0123456789876543210Sym1 :: GHC.Num.Natural.Natural -> (~>) (Pair a b) ((~>) Symbol Symbol) data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) (Pair a b) ((~>) Symbol Symbol) where ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) => ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ShowsPrec_0123456789876543210Sym1KindInference ()) type ShowsPrec_0123456789876543210Sym2 :: GHC.Num.Natural.Natural -> Pair a b -> (~>) Symbol Symbol data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Pair a b) :: (~>) Symbol Symbol where ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) => ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural -> Pair a b -> Symbol -> Symbol type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Pair a b) (a0123456789876543210 :: Symbol) :: Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 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 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)) = case (,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) of (,) (SomeSing c) (SomeSing c) -> SomeSing (SPair c c) instance (SShow a, SShow b) => SShow (Pair a b) where sShowsPrec :: forall (t1 :: GHC.Num.Natural.Natural) (t2 :: Pair a b) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) -> 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 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 Case_0123456789876543210 x t where Case_0123456789876543210 x _ = Tuple0Sym0 data Let0123456789876543210TSym0 x0123456789876543210 where Let0123456789876543210TSym0KindInference :: SameKind (Apply Let0123456789876543210TSym0 arg) (Let0123456789876543210TSym1 arg) => Let0123456789876543210TSym0 x0123456789876543210 type instance Apply Let0123456789876543210TSym0 x0123456789876543210 = Let0123456789876543210TSym1 x0123456789876543210 instance SuppressUnusedWarnings Let0123456789876543210TSym0 where suppressUnusedWarnings = snd ((,) Let0123456789876543210TSym0KindInference ()) data Let0123456789876543210TSym1 x0123456789876543210 y0123456789876543210 where Let0123456789876543210TSym1KindInference :: SameKind (Apply (Let0123456789876543210TSym1 x0123456789876543210) arg) (Let0123456789876543210TSym2 x0123456789876543210 arg) => Let0123456789876543210TSym1 x0123456789876543210 y0123456789876543210 type instance Apply (Let0123456789876543210TSym1 x0123456789876543210) y0123456789876543210 = Let0123456789876543210T x0123456789876543210 y0123456789876543210 instance SuppressUnusedWarnings (Let0123456789876543210TSym1 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210TSym1KindInference ()) type family Let0123456789876543210TSym2 x0123456789876543210 y0123456789876543210 where Let0123456789876543210TSym2 x0123456789876543210 y0123456789876543210 = Let0123456789876543210T x0123456789876543210 y0123456789876543210 type family Let0123456789876543210T x y where Let0123456789876543210T x y = Apply (Apply Tuple2Sym0 x) y type family Case_0123456789876543210 arg_0123456789876543210 a b x y t where Case_0123456789876543210 arg_0123456789876543210 a b x y _ = a type family Lambda_0123456789876543210 a b x y arg_0123456789876543210 where Lambda_0123456789876543210 a b x y arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 a b x y arg_0123456789876543210 data Lambda_0123456789876543210Sym0 a0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) => Lambda_0123456789876543210Sym0 a0123456789876543210 type instance Apply Lambda_0123456789876543210Sym0 a0123456789876543210 = Lambda_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) data Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 a0123456789876543210) arg) (Lambda_0123456789876543210Sym2 a0123456789876543210 arg) => Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 type instance Apply (Lambda_0123456789876543210Sym1 a0123456789876543210) b0123456789876543210 = Lambda_0123456789876543210Sym2 a0123456789876543210 b0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) data Lambda_0123456789876543210Sym2 a0123456789876543210 b0123456789876543210 x0123456789876543210 where Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 a0123456789876543210 b0123456789876543210) arg) (Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 arg) => Lambda_0123456789876543210Sym2 a0123456789876543210 b0123456789876543210 x0123456789876543210 type instance Apply (Lambda_0123456789876543210Sym2 a0123456789876543210 b0123456789876543210) x0123456789876543210 = Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 x0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 a0123456789876543210 b0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) data Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 where Lambda_0123456789876543210Sym3KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 x0123456789876543210) arg) (Lambda_0123456789876543210Sym4 a0123456789876543210 b0123456789876543210 x0123456789876543210 arg) => Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 type instance Apply (Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 x0123456789876543210) y0123456789876543210 = Lambda_0123456789876543210Sym4 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym3KindInference ()) data Lambda_0123456789876543210Sym4 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym4KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym4 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210) arg) (Lambda_0123456789876543210Sym5 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg) => Lambda_0123456789876543210Sym4 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 type instance Apply (Lambda_0123456789876543210Sym4 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210) arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym4 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym4KindInference ()) type family Lambda_0123456789876543210Sym5 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym5 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 type family Case_0123456789876543210 x y t where Case_0123456789876543210 x y '(a, b) = Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 a) b) x) y) b type family Case_0123456789876543210 arg_0123456789876543210 x y t where Case_0123456789876543210 arg_0123456789876543210 x y _ = x type family Lambda_0123456789876543210 x y arg_0123456789876543210 where Lambda_0123456789876543210 x y arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x y arg_0123456789876543210 data Lambda_0123456789876543210Sym0 x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 type instance Apply Lambda_0123456789876543210Sym0 x0123456789876543210 = Lambda_0123456789876543210Sym1 x0123456789876543210 instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) data Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 x0123456789876543210) arg) (Lambda_0123456789876543210Sym2 x0123456789876543210 arg) => Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 type instance Apply (Lambda_0123456789876543210Sym1 x0123456789876543210) y0123456789876543210 = Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) data Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym2KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210) arg) (Lambda_0123456789876543210Sym3 x0123456789876543210 y0123456789876543210 arg) => Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 type instance Apply (Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210) arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 type family Case_0123456789876543210 t where Case_0123456789876543210 '[_, _, 'Succ y_0123456789876543210] = y_0123456789876543210 type family Case_0123456789876543210 t where Case_0123456789876543210 '[_, y_0123456789876543210, 'Succ _] = 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 SillySym0 :: (~>) a () data SillySym0 :: (~>) a () where SillySym0KindInference :: SameKind (Apply SillySym0 arg) (SillySym1 arg) => SillySym0 a0123456789876543210 type instance Apply SillySym0 a0123456789876543210 = Silly a0123456789876543210 instance SuppressUnusedWarnings SillySym0 where suppressUnusedWarnings = snd ((,) SillySym0KindInference ()) type SillySym1 :: a -> () type family SillySym1 (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 Foo2Sym0 a0123456789876543210 = Foo2 a0123456789876543210 instance SuppressUnusedWarnings Foo2Sym0 where suppressUnusedWarnings = snd ((,) Foo2Sym0KindInference ()) type Foo2Sym1 :: (a, b) -> a type family Foo2Sym1 (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 Foo1Sym0 a0123456789876543210 = Foo1 a0123456789876543210 instance SuppressUnusedWarnings Foo1Sym0 where suppressUnusedWarnings = snd ((,) Foo1Sym0KindInference ()) type Foo1Sym1 :: (a, b) -> a type family Foo1Sym1 (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) :: () where Silly x = Case_0123456789876543210 x x type Foo2 :: (a, b) -> a type family Foo2 (a :: (a, b)) :: a where Foo2 '(x, y) = Case_0123456789876543210 x y (Let0123456789876543210TSym2 x y) type Foo1 :: (a, b) -> a type family Foo1 (a :: (a, b)) :: a where Foo1 '(x, y) = Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) y) y type family Blimy where Blimy = Case_0123456789876543210 X_0123456789876543210Sym0 type Lsz :: Nat type family Lsz :: Nat where Lsz = Case_0123456789876543210 X_0123456789876543210Sym0 type family X_0123456789876543210 where X_0123456789876543210 = AListSym0 type family Tt where Tt = Case_0123456789876543210 X_0123456789876543210Sym0 type family Tjz where Tjz = Case_0123456789876543210 X_0123456789876543210Sym0 type family Tf where Tf = Case_0123456789876543210 X_0123456789876543210Sym0 type family X_0123456789876543210 where X_0123456789876543210 = TupleSym0 type Fls :: Bool type family Fls :: Bool where Fls = Case_0123456789876543210 X_0123456789876543210Sym0 type family Zz where Zz = Case_0123456789876543210 X_0123456789876543210Sym0 type family Jz where Jz = Case_0123456789876543210 X_0123456789876543210Sym0 type family X_0123456789876543210 where X_0123456789876543210 = ComplexSym0 type family Lz where Lz = Case_0123456789876543210 X_0123456789876543210Sym0 type family Sz where Sz = Case_0123456789876543210 X_0123456789876543210Sym0 type family X_0123456789876543210 where X_0123456789876543210 = PrSym0 sSilly :: (forall (t :: a). Sing t -> Sing (Apply SillySym0 t :: ()) :: Type) sFoo2 :: (forall (t :: (a, b)). Sing t -> Sing (Apply Foo2Sym0 t :: a) :: Type) sFoo1 :: (forall (t :: (a, b)). Sing t -> Sing (Apply Foo1Sym0 t :: a) :: Type) sBlimy :: Sing @_ BlimySym0 sLsz :: (Sing (LszSym0 :: Nat) :: Type) sX_0123456789876543210 :: Sing @_ X_0123456789876543210Sym0 sTt :: Sing @_ TtSym0 sTjz :: Sing @_ TjzSym0 sTf :: Sing @_ TfSym0 sX_0123456789876543210 :: Sing @_ X_0123456789876543210Sym0 sFls :: (Sing (FlsSym0 :: Bool) :: Type) sZz :: Sing @_ ZzSym0 sJz :: Sing @_ JzSym0 sX_0123456789876543210 :: Sing @_ X_0123456789876543210Sym0 sLz :: Sing @_ LzSym0 sSz :: Sing @_ SzSym0 sX_0123456789876543210 :: Sing @_ X_0123456789876543210Sym0 sSilly (sX :: Sing x) = id @(Sing (Case_0123456789876543210 x x)) (case sX of _ -> STuple0) sFoo2 (STuple2 (sX :: Sing x) (sY :: Sing y)) = let sT :: Sing @_ (Let0123456789876543210TSym2 x y) sT = applySing (applySing (singFun2 @Tuple2Sym0 STuple2) sX) sY in id @(Sing (Case_0123456789876543210 x y (Let0123456789876543210TSym2 x y))) (case sT of STuple2 (sA :: Sing a) (sB :: Sing b) -> applySing (singFun1 @(Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 a) b) x) y) (\ sArg_0123456789876543210 -> case sArg_0123456789876543210 of (_ :: Sing arg_0123456789876543210) -> id @(Sing (Case_0123456789876543210 arg_0123456789876543210 a b x y arg_0123456789876543210)) (case sArg_0123456789876543210 of _ -> sA))) sB) 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) -> id @(Sing (Case_0123456789876543210 arg_0123456789876543210 x y arg_0123456789876543210)) (case sArg_0123456789876543210 of _ -> sX))) sY sBlimy = id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SCons _ (SCons _ (SCons (SSucc (sY_0123456789876543210 :: Sing y_0123456789876543210)) SNil)) -> sY_0123456789876543210) sLsz = id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SCons _ (SCons (sY_0123456789876543210 :: Sing y_0123456789876543210) (SCons (SSucc _) SNil)) -> sY_0123456789876543210) sX_0123456789876543210 = sAList sTt = id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of STuple3 _ _ (sY_0123456789876543210 :: Sing y_0123456789876543210) -> sY_0123456789876543210) sTjz = id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of STuple3 _ (sY_0123456789876543210 :: Sing y_0123456789876543210) _ -> sY_0123456789876543210) sTf = id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of STuple3 (sY_0123456789876543210 :: Sing y_0123456789876543210) _ _ -> sY_0123456789876543210) sX_0123456789876543210 = sTuple sFls = id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SPair (SPair _ _) (sY_0123456789876543210 :: Sing y_0123456789876543210) -> sY_0123456789876543210) sZz = id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SPair (SPair _ (sY_0123456789876543210 :: Sing y_0123456789876543210)) _ -> sY_0123456789876543210) sJz = id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SPair (SPair (sY_0123456789876543210 :: Sing y_0123456789876543210) _) _ -> sY_0123456789876543210) sX_0123456789876543210 = sComplex sLz = id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SPair _ (sY_0123456789876543210 :: Sing y_0123456789876543210) -> sY_0123456789876543210) sSz = id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SPair (sY_0123456789876543210 :: Sing y_0123456789876543210) _ -> sY_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