Promote/PatternMatching.hs:0:0: Splicing declarations
    promote
      [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) |]
  ======>
    Promote/PatternMatching.hs:(0,0)-(0,0)
    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 PairTyCtor = Pair
    data PairTyCtorSym1 (l :: *) (l :: TyFun * *)
    data PairTyCtorSym0 (k :: TyFun * (TyFun * * -> *))
    type instance Apply (PairTyCtorSym1 a) a = PairTyCtor a a
    type instance Apply PairTyCtorSym0 a = PairTyCtorSym1 a
    data PairSym1 (l :: a) (l :: TyFun b (Pair a b))
    data PairSym0 (k :: TyFun a (TyFun b (Pair a b) -> *))
    type instance Apply (PairSym1 a) a = Pair a a
    type instance Apply PairSym0 a = PairSym1 a
    type Pr =
        Apply (Apply PairSym0 (Apply SuccSym0 ZeroSym0)) '[ZeroSym0]
    type PrSym0 = Pr
    type Complex =
        Apply (Apply PairSym0 (Apply (Apply PairSym0 (Apply JustSym0 ZeroSym0)) ZeroSym0)) FalseSym0
    type ComplexSym0 = Complex
    type Tuple = '(FalseSym0, Apply JustSym0 ZeroSym0, TrueSym0)
    type TupleSym0 = Tuple
    type AList =
        '[ZeroSym0,
          Apply SuccSym0 ZeroSym0,
          Apply SuccSym0 (Apply SuccSym0 ZeroSym0)]
    type AListSym0 = AList
Promote/PatternMatching.hs:0:0: Splicing declarations
    promote
      [d| Pair sz lz = pr
          Pair (Pair jz zz) fls = complex
          (tf, tjz, tt) = tuple
          [_, lsz, (Succ blimy)] = aList
          foo1 :: (a, b) -> a
          foo1 (x, y) = (\ _ -> x) y
          foo2 :: (# a, b #) -> a
          foo2 t@(# x, y #) = case t of { (# a, b #) -> (\ _ -> a) b } |]
  ======>
    Promote/PatternMatching.hs:(0,0)-(0,0)
    Pair sz lz = pr
    Pair (Pair jz zz) fls = complex
    (tf, tjz, tt) = tuple
    [_, lsz, Succ blimy] = aList
    foo1 :: forall a b. (a, b) -> a
    foo1 (x, y) = \ _ -> x y
    foo2 :: forall a b. (# a, b #) -> a
    foo2 t@(# x, y #) = case t of { (# a, b #) -> \ _ -> a b }
    type Sz = Extract_0123456789 PrSym0
    type SzSym0 = Sz
    type Lz = Extract_0123456789 PrSym0
    type LzSym0 = Lz
    type family Extract_0123456789 (a :: Pair a b) :: a
    type family Extract_0123456789 (a :: Pair a b) :: b
    type instance Extract_0123456789 (Pair a a) = a
    type instance Extract_0123456789 (Pair a a) = a
    type Jz = Extract_0123456789 (Extract_0123456789 ComplexSym0)
    type JzSym0 = Jz
    type Zz = Extract_0123456789 (Extract_0123456789 ComplexSym0)
    type ZzSym0 = Zz
    type Fls = Extract_0123456789 ComplexSym0
    type FlsSym0 = Fls
    type family Extract_0123456789 (a :: Pair a b) :: a
    type family Extract_0123456789 (a :: Pair a b) :: b
    type instance Extract_0123456789 (Pair a a) = a
    type instance Extract_0123456789 (Pair a a) = a
    type family Extract_0123456789 (a :: Pair a b) :: a
    type family Extract_0123456789 (a :: Pair a b) :: b
    type instance Extract_0123456789 (Pair a a) = a
    type instance Extract_0123456789 (Pair a a) = a
    type Tf = Extract_0123456789 TupleSym0
    type TfSym0 = Tf
    type Tjz = Extract_0123456789 TupleSym0
    type TjzSym0 = Tjz
    type Tt = Extract_0123456789 TupleSym0
    type TtSym0 = Tt
    type family Extract_0123456789 (a :: GHC.Tuple.(,,) a b c) :: a
    type family Extract_0123456789 (a :: GHC.Tuple.(,,) a b c) :: b
    type family Extract_0123456789 (a :: GHC.Tuple.(,,) a b c) :: c
    type instance Extract_0123456789 (GHC.Tuple.(,,) a a a) = a
    type instance Extract_0123456789 (GHC.Tuple.(,,) a a a) = a
    type instance Extract_0123456789 (GHC.Tuple.(,,) a a a) = a
    type Lsz = Head (Tail AListSym0)
    type LszSym0 = Lsz
    type Blimy = Extract_0123456789 (Head (Tail (Tail AListSym0)))
    type BlimySym0 = Blimy
    type family Extract_0123456789 (a :: Nat) :: Nat
    type instance Extract_0123456789 (Succ a) = a
    type family Lambda_0123456789 (x :: x) (y :: y) (t :: k) :: r
    type instance Lambda_0123456789 x y z = x
    data Lambda_0123456789Sym2 (l :: x) (l :: y) (l :: TyFun k r)
    type instance Apply (Lambda_0123456789Sym2 a a) a =
        Lambda_0123456789 a a a
    type family Lambda_0123456789 (x :: x)
                                  (y :: y)
                                  (a :: a)
                                  (b :: b)
                                  (t :: k) :: r
    type instance Lambda_0123456789 x y a b z = a
    data Lambda_0123456789Sym4 (l :: x)
                               (l :: y)
                               (l :: a)
                               (l :: b)
                               (l :: TyFun k r)
    type instance Apply (Lambda_0123456789Sym4 a a a a) a =
        Lambda_0123456789 a a a a a
    type family Case_0123456789 (t :: k) (x :: x) (y :: y) :: r
    type instance Case_0123456789 '(a, b) x y =
        Apply (Lambda_0123456789Sym4 x y a b) b
    type family Foo1 (a :: (a, b)) :: a
    type instance Foo1 '(x, y) = Apply (Lambda_0123456789Sym2 x y) y
    data Foo1Sym0 (k :: TyFun (a, b) a)
    type instance Apply Foo1Sym0 a = Foo1 a
    type family Foo2 (a :: (a, b)) :: a
    type instance Foo2 '(x, y) =
        Case_0123456789 (Apply (Apply Tuple2Sym0 x) y) x y
    data Foo2Sym0 (k :: TyFun (a, b) a)
    type instance Apply Foo2Sym0 a = Foo2 a