Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| maybePlus :: Maybe Nat -> Maybe Nat
          maybePlus (Just n) = Just (plus (Succ Zero) n)
          maybePlus p@Nothing = p
          bar :: Maybe Nat -> Maybe Nat
          bar x@(Just _) = x
          bar Nothing = Nothing
          baz_ :: Maybe Baz -> Maybe Baz
          baz_ p@Nothing = p
          baz_ p@(Just (Baz _ _ _)) = p
          tup :: (Nat, Nat) -> (Nat, Nat)
          tup p@(_, _) = p
          foo :: [Nat] -> [Nat]
          foo p@[] = p
          foo p@[_] = p
          foo p@(_ : _ : _) = p
          
          data Baz = Baz Nat Nat Nat |]
  ======>
    maybePlus :: Maybe Nat -> Maybe Nat
    maybePlus (Just n) = Just (plus (Succ Zero) n)
    maybePlus p@Nothing = p
    bar :: Maybe Nat -> Maybe Nat
    bar x@(Just _) = x
    bar Nothing = Nothing
    data Baz = Baz Nat Nat Nat
    baz_ :: Maybe Baz -> Maybe Baz
    baz_ p@Nothing = p
    baz_ p@(Just (Baz _ _ _)) = p
    tup :: (Nat, Nat) -> (Nat, Nat)
    tup p@(_, _) = p
    foo :: [Nat] -> [Nat]
    foo p@[] = p
    foo p@[_] = p
    foo p@(_ : (_ : _)) = p
    type BazSym0 :: (~>) Nat ((~>) Nat ((~>) Nat Baz))
    data BazSym0 :: (~>) Nat ((~>) Nat ((~>) Nat Baz))
      where
        BazSym0KindInference :: SameKind (Apply BazSym0 arg) (BazSym1 arg) =>
                                BazSym0 a0123456789876543210
    type instance Apply BazSym0 a0123456789876543210 = BazSym1 a0123456789876543210
    instance SuppressUnusedWarnings BazSym0 where
      suppressUnusedWarnings = snd ((,) BazSym0KindInference ())
    type BazSym1 :: Nat -> (~>) Nat ((~>) Nat Baz)
    data BazSym1 (a0123456789876543210 :: Nat) :: (~>) Nat ((~>) Nat Baz)
      where
        BazSym1KindInference :: SameKind (Apply (BazSym1 a0123456789876543210) arg) (BazSym2 a0123456789876543210 arg) =>
                                BazSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (BazSym1 a0123456789876543210) a0123456789876543210 = BazSym2 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (BazSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) BazSym1KindInference ())
    type BazSym2 :: Nat -> Nat -> (~>) Nat Baz
    data BazSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: (~>) Nat Baz
      where
        BazSym2KindInference :: SameKind (Apply (BazSym2 a0123456789876543210 a0123456789876543210) arg) (BazSym3 a0123456789876543210 a0123456789876543210 arg) =>
                                BazSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
    type instance Apply (BazSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = Baz a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (BazSym2 a0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) BazSym2KindInference ())
    type BazSym3 :: Nat -> Nat -> Nat -> Baz
    type family BazSym3 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Baz where
      BazSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = Baz a0123456789876543210 a0123456789876543210 a0123456789876543210
    type family Let0123456789876543210PSym0 where
      Let0123456789876543210PSym0 = Let0123456789876543210P
    type family Let0123456789876543210P where
      Let0123456789876543210P = NilSym0
    data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
      where
        Let0123456789876543210PSym0KindInference :: SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
                                                    Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
    type instance Apply Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210PSym0KindInference ())
    type family Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 where
      Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210
    type family Let0123456789876543210P wild_0123456789876543210 where
      Let0123456789876543210P wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) NilSym0
    data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
      where
        Let0123456789876543210PSym0KindInference :: SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
                                                    Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
    type instance Apply Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210PSym0KindInference ())
    data Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
      where
        Let0123456789876543210PSym1KindInference :: SameKind (Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) arg) (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 arg) =>
                                                    Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    type instance Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210PSym1KindInference ())
    data Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
      where
        Let0123456789876543210PSym2KindInference :: SameKind (Apply (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) arg) (Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 arg) =>
                                                    Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    type instance Apply (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210PSym2KindInference ())
    type family Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
      Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 where
      Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) (Apply (Apply (:@#@$) wild_0123456789876543210) wild_0123456789876543210)
    data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
      where
        Let0123456789876543210PSym0KindInference :: SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
                                                    Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
    type instance Apply Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210PSym0KindInference ())
    data Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
      where
        Let0123456789876543210PSym1KindInference :: SameKind (Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) arg) (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 arg) =>
                                                    Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    type instance Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210PSym1KindInference ())
    type family Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
      Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 where
      Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 = Apply (Apply Tuple2Sym0 wild_0123456789876543210) wild_0123456789876543210
    type family Let0123456789876543210PSym0 where
      Let0123456789876543210PSym0 = Let0123456789876543210P
    type family Let0123456789876543210P where
      Let0123456789876543210P = NothingSym0
    data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
      where
        Let0123456789876543210PSym0KindInference :: SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
                                                    Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
    type instance Apply Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210PSym0KindInference ())
    data Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
      where
        Let0123456789876543210PSym1KindInference :: SameKind (Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) arg) (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 arg) =>
                                                    Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    type instance Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210PSym1KindInference ())
    data Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
      where
        Let0123456789876543210PSym2KindInference :: SameKind (Apply (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) arg) (Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 arg) =>
                                                    Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    type instance Apply (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210PSym2KindInference ())
    type family Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
      Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
    type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 where
      Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 = Apply JustSym0 (Apply (Apply (Apply BazSym0 wild_0123456789876543210) wild_0123456789876543210) wild_0123456789876543210)
    data Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210
      where
        Let0123456789876543210XSym0KindInference :: SameKind (Apply Let0123456789876543210XSym0 arg) (Let0123456789876543210XSym1 arg) =>
                                                    Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210
    type instance Apply Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210X wild_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210XSym0 where
      suppressUnusedWarnings
        = snd ((,) Let0123456789876543210XSym0KindInference ())
    type family Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 where
      Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210X wild_01234567898765432100123456789876543210
    type family Let0123456789876543210X wild_0123456789876543210 where
      Let0123456789876543210X wild_0123456789876543210 = Apply JustSym0 wild_0123456789876543210
    type family Let0123456789876543210PSym0 where
      Let0123456789876543210PSym0 = Let0123456789876543210P
    type family Let0123456789876543210P where
      Let0123456789876543210P = NothingSym0
    type FooSym0 :: (~>) [Nat] [Nat]
    data FooSym0 :: (~>) [Nat] [Nat]
      where
        FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
                                FooSym0 a0123456789876543210
    type instance Apply FooSym0 a0123456789876543210 = Foo a0123456789876543210
    instance SuppressUnusedWarnings FooSym0 where
      suppressUnusedWarnings = snd ((,) FooSym0KindInference ())
    type FooSym1 :: [Nat] -> [Nat]
    type family FooSym1 (a0123456789876543210 :: [Nat]) :: [Nat] where
      FooSym1 a0123456789876543210 = Foo a0123456789876543210
    type TupSym0 :: (~>) (Nat, Nat) (Nat, Nat)
    data TupSym0 :: (~>) (Nat, Nat) (Nat, Nat)
      where
        TupSym0KindInference :: SameKind (Apply TupSym0 arg) (TupSym1 arg) =>
                                TupSym0 a0123456789876543210
    type instance Apply TupSym0 a0123456789876543210 = Tup a0123456789876543210
    instance SuppressUnusedWarnings TupSym0 where
      suppressUnusedWarnings = snd ((,) TupSym0KindInference ())
    type TupSym1 :: (Nat, Nat) -> (Nat, Nat)
    type family TupSym1 (a0123456789876543210 :: (Nat, Nat)) :: (Nat,
                                                                 Nat) where
      TupSym1 a0123456789876543210 = Tup a0123456789876543210
    type Baz_Sym0 :: (~>) (Maybe Baz) (Maybe Baz)
    data Baz_Sym0 :: (~>) (Maybe Baz) (Maybe Baz)
      where
        Baz_Sym0KindInference :: SameKind (Apply Baz_Sym0 arg) (Baz_Sym1 arg) =>
                                 Baz_Sym0 a0123456789876543210
    type instance Apply Baz_Sym0 a0123456789876543210 = Baz_ a0123456789876543210
    instance SuppressUnusedWarnings Baz_Sym0 where
      suppressUnusedWarnings = snd ((,) Baz_Sym0KindInference ())
    type Baz_Sym1 :: Maybe Baz -> Maybe Baz
    type family Baz_Sym1 (a0123456789876543210 :: Maybe Baz) :: Maybe Baz where
      Baz_Sym1 a0123456789876543210 = Baz_ a0123456789876543210
    type BarSym0 :: (~>) (Maybe Nat) (Maybe Nat)
    data BarSym0 :: (~>) (Maybe Nat) (Maybe Nat)
      where
        BarSym0KindInference :: SameKind (Apply BarSym0 arg) (BarSym1 arg) =>
                                BarSym0 a0123456789876543210
    type instance Apply BarSym0 a0123456789876543210 = Bar a0123456789876543210
    instance SuppressUnusedWarnings BarSym0 where
      suppressUnusedWarnings = snd ((,) BarSym0KindInference ())
    type BarSym1 :: Maybe Nat -> Maybe Nat
    type family BarSym1 (a0123456789876543210 :: Maybe Nat) :: Maybe Nat where
      BarSym1 a0123456789876543210 = Bar a0123456789876543210
    type MaybePlusSym0 :: (~>) (Maybe Nat) (Maybe Nat)
    data MaybePlusSym0 :: (~>) (Maybe Nat) (Maybe Nat)
      where
        MaybePlusSym0KindInference :: SameKind (Apply MaybePlusSym0 arg) (MaybePlusSym1 arg) =>
                                      MaybePlusSym0 a0123456789876543210
    type instance Apply MaybePlusSym0 a0123456789876543210 = MaybePlus a0123456789876543210
    instance SuppressUnusedWarnings MaybePlusSym0 where
      suppressUnusedWarnings = snd ((,) MaybePlusSym0KindInference ())
    type MaybePlusSym1 :: Maybe Nat -> Maybe Nat
    type family MaybePlusSym1 (a0123456789876543210 :: Maybe Nat) :: Maybe Nat where
      MaybePlusSym1 a0123456789876543210 = MaybePlus a0123456789876543210
    type Foo :: [Nat] -> [Nat]
    type family Foo (a :: [Nat]) :: [Nat] where
      Foo '[] = Let0123456789876543210PSym0
      Foo '[wild_0123456789876543210] = Let0123456789876543210PSym1 wild_0123456789876543210
      Foo ('(:) wild_0123456789876543210 ('(:) wild_0123456789876543210 wild_0123456789876543210)) = Let0123456789876543210PSym3 wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210
    type Tup :: (Nat, Nat) -> (Nat, Nat)
    type family Tup (a :: (Nat, Nat)) :: (Nat, Nat) where
      Tup '(wild_0123456789876543210,
            wild_0123456789876543210) = Let0123456789876543210PSym2 wild_0123456789876543210 wild_0123456789876543210
    type Baz_ :: Maybe Baz -> Maybe Baz
    type family Baz_ (a :: Maybe Baz) :: Maybe Baz where
      Baz_ 'Nothing = Let0123456789876543210PSym0
      Baz_ ('Just (Baz wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210)) = Let0123456789876543210PSym3 wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210
    type Bar :: Maybe Nat -> Maybe Nat
    type family Bar (a :: Maybe Nat) :: Maybe Nat where
      Bar ('Just wild_0123456789876543210) = Let0123456789876543210XSym1 wild_0123456789876543210
      Bar 'Nothing = NothingSym0
    type MaybePlus :: Maybe Nat -> Maybe Nat
    type family MaybePlus (a :: Maybe Nat) :: Maybe Nat where
      MaybePlus ('Just n) = Apply JustSym0 (Apply (Apply PlusSym0 (Apply SuccSym0 ZeroSym0)) n)
      MaybePlus 'Nothing = Let0123456789876543210PSym0
    sFoo ::
      (forall (t :: [Nat]).
       Sing t -> Sing (Apply FooSym0 t :: [Nat]) :: Type)
    sTup ::
      (forall (t :: (Nat, Nat)).
       Sing t -> Sing (Apply TupSym0 t :: (Nat, Nat)) :: Type)
    sBaz_ ::
      (forall (t :: Maybe Baz).
       Sing t -> Sing (Apply Baz_Sym0 t :: Maybe Baz) :: Type)
    sBar ::
      (forall (t :: Maybe Nat).
       Sing t -> Sing (Apply BarSym0 t :: Maybe Nat) :: Type)
    sMaybePlus ::
      (forall (t :: Maybe Nat).
       Sing t -> Sing (Apply MaybePlusSym0 t :: Maybe Nat) :: Type)
    sFoo SNil
      = let
          sP :: Sing @_ Let0123456789876543210PSym0
          sP = SNil
        in sP
    sFoo
      (SCons (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
             SNil)
      = let
          sP ::
            Sing @_ (Let0123456789876543210PSym1 wild_0123456789876543210)
          sP
            = applySing
                (applySing (singFun2 @(:@#@$) SCons) sWild_0123456789876543210)
                SNil
        in sP
    sFoo
      (SCons (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
             (SCons (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
                    (sWild_0123456789876543210 :: Sing wild_0123456789876543210)))
      = let
          sP ::
            Sing @_ (Let0123456789876543210PSym3 wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210)
          sP
            = applySing
                (applySing (singFun2 @(:@#@$) SCons) sWild_0123456789876543210)
                (applySing
                   (applySing (singFun2 @(:@#@$) SCons) sWild_0123456789876543210)
                   sWild_0123456789876543210)
        in sP
    sTup
      (STuple2 (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
               (sWild_0123456789876543210 :: Sing wild_0123456789876543210))
      = let
          sP ::
            Sing @_ (Let0123456789876543210PSym2 wild_0123456789876543210 wild_0123456789876543210)
          sP
            = applySing
                (applySing
                   (singFun2 @Tuple2Sym0 STuple2) sWild_0123456789876543210)
                sWild_0123456789876543210
        in sP
    sBaz_ SNothing
      = let
          sP :: Sing @_ Let0123456789876543210PSym0
          sP = SNothing
        in sP
    sBaz_
      (SJust (SBaz (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
                   (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
                   (sWild_0123456789876543210 :: Sing wild_0123456789876543210)))
      = let
          sP ::
            Sing @_ (Let0123456789876543210PSym3 wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210)
          sP
            = applySing
                (singFun1 @JustSym0 SJust)
                (applySing
                   (applySing
                      (applySing (singFun3 @BazSym0 SBaz) sWild_0123456789876543210)
                      sWild_0123456789876543210)
                   sWild_0123456789876543210)
        in sP
    sBar
      (SJust (sWild_0123456789876543210 :: Sing wild_0123456789876543210))
      = let
          sX ::
            Sing @_ (Let0123456789876543210XSym1 wild_0123456789876543210)
          sX = applySing (singFun1 @JustSym0 SJust) sWild_0123456789876543210
        in sX
    sBar SNothing = SNothing
    sMaybePlus (SJust (sN :: Sing n))
      = applySing
          (singFun1 @JustSym0 SJust)
          (applySing
             (applySing
                (singFun2 @PlusSym0 sPlus)
                (applySing (singFun1 @SuccSym0 SSucc) SZero))
             sN)
    sMaybePlus SNothing
      = let
          sP :: Sing @_ Let0123456789876543210PSym0
          sP = SNothing
        in sP
    instance SingI (FooSym0 :: (~>) [Nat] [Nat]) where
      sing = singFun1 @FooSym0 sFoo
    instance SingI (TupSym0 :: (~>) (Nat, Nat) (Nat, Nat)) where
      sing = singFun1 @TupSym0 sTup
    instance SingI (Baz_Sym0 :: (~>) (Maybe Baz) (Maybe Baz)) where
      sing = singFun1 @Baz_Sym0 sBaz_
    instance SingI (BarSym0 :: (~>) (Maybe Nat) (Maybe Nat)) where
      sing = singFun1 @BarSym0 sBar
    instance SingI (MaybePlusSym0 :: (~>) (Maybe Nat) (Maybe Nat)) where
      sing = singFun1 @MaybePlusSym0 sMaybePlus
    data SBaz :: Baz -> Type
      where
        SBaz :: forall (n :: Nat) (n :: Nat) (n :: Nat).
                (Sing n) -> (Sing n) -> (Sing n) -> SBaz (Baz n n n :: Baz)
    type instance Sing @Baz = SBaz
    instance SingKind Baz where
      type Demote Baz = Baz
      fromSing (SBaz b b b) = Baz (fromSing b) (fromSing b) (fromSing b)
      toSing (Baz (b :: Demote Nat) (b :: Demote Nat) (b :: Demote Nat))
        = case
              (,,)
                (toSing b :: SomeSing Nat) (toSing b :: SomeSing Nat)
                (toSing b :: SomeSing Nat)
          of
            (,,) (SomeSing c) (SomeSing c) (SomeSing c)
              -> SomeSing (SBaz c c c)
    instance (SingI n, SingI n, SingI n) =>
             SingI (Baz (n :: Nat) (n :: Nat) (n :: Nat)) where
      sing = SBaz sing sing sing
    instance (SingI n, SingI n) =>
             SingI1 (Baz (n :: Nat) (n :: Nat)) where
      liftSing = SBaz sing sing
    instance SingI n => SingI2 (Baz (n :: Nat)) where
      liftSing2 = SBaz sing
    instance SingI (BazSym0 :: (~>) Nat ((~>) Nat ((~>) Nat Baz))) where
      sing = singFun3 @BazSym0 SBaz
    instance SingI d =>
             SingI (BazSym1 (d :: Nat) :: (~>) Nat ((~>) Nat Baz)) where
      sing = singFun2 @(BazSym1 (d :: Nat)) (SBaz (sing @d))
    instance SingI1 (BazSym1 :: Nat -> (~>) Nat ((~>) Nat Baz)) where
      liftSing (s :: Sing (d :: Nat))
        = singFun2 @(BazSym1 (d :: Nat)) (SBaz s)
    instance (SingI d, SingI d) =>
             SingI (BazSym2 (d :: Nat) (d :: Nat) :: (~>) Nat Baz) where
      sing
        = singFun1
            @(BazSym2 (d :: Nat) (d :: Nat)) (SBaz (sing @d) (sing @d))
    instance SingI d =>
             SingI1 (BazSym2 (d :: Nat) :: Nat -> (~>) Nat Baz) where
      liftSing (s :: Sing (d :: Nat))
        = singFun1 @(BazSym2 (d :: Nat) (d :: Nat)) (SBaz (sing @d) s)
    instance SingI2 (BazSym2 :: Nat -> Nat -> (~>) Nat Baz) where
      liftSing2 (s :: Sing (d :: Nat)) (s :: Sing (d :: Nat))
        = singFun1 @(BazSym2 (d :: Nat) (d :: Nat)) (SBaz s s)