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@GHC.Types.[] = p
    foo p@[_] = p
    foo p@(_ GHC.Types.: (_ GHC.Types.: _)) = p
    type BazSym3 (t :: Nat) (t :: Nat) (t :: Nat) = Baz t t t
    instance SuppressUnusedWarnings BazSym2 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) BazSym2KindInference) GHC.Tuple.())
    data BazSym2 (l :: Nat) (l :: Nat) (l :: TyFun Nat Baz)
      = forall arg. SameKind (Apply (BazSym2 l l) arg) (BazSym3 l l arg) =>
        BazSym2KindInference
    type instance Apply (BazSym2 l l) l = Baz l l l
    instance SuppressUnusedWarnings BazSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) BazSym1KindInference) GHC.Tuple.())
    data BazSym1 (l :: Nat) (l :: TyFun Nat (TyFun Nat Baz
                                             -> GHC.Types.Type))
      = forall arg. SameKind (Apply (BazSym1 l) arg) (BazSym2 l arg) =>
        BazSym1KindInference
    type instance Apply (BazSym1 l) l = BazSym2 l l
    instance SuppressUnusedWarnings BazSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) BazSym0KindInference) GHC.Tuple.())
    data BazSym0 (l :: TyFun Nat (TyFun Nat (TyFun Nat Baz
                                             -> GHC.Types.Type)
                                  -> GHC.Types.Type))
      = forall arg. SameKind (Apply BazSym0 arg) (BazSym1 arg) =>
        BazSym0KindInference
    type instance Apply BazSym0 l = BazSym1 l
    type Let0123456789876543210PSym0 = Let0123456789876543210P
    type family Let0123456789876543210P where
      Let0123456789876543210P = '[]
    type Let0123456789876543210PSym1 t = Let0123456789876543210P t
    instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Let0123456789876543210PSym0KindInference)
               GHC.Tuple.())
    data Let0123456789876543210PSym0 l
      = forall arg. SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
        Let0123456789876543210PSym0KindInference
    type instance Apply Let0123456789876543210PSym0 l = Let0123456789876543210P l
    type family Let0123456789876543210P wild_0123456789876543210 where
      Let0123456789876543210P wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) '[]
    type Let0123456789876543210PSym3 t t t =
        Let0123456789876543210P t t t
    instance SuppressUnusedWarnings Let0123456789876543210PSym2 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Let0123456789876543210PSym2KindInference)
               GHC.Tuple.())
    data Let0123456789876543210PSym2 l l l
      = forall arg. SameKind (Apply (Let0123456789876543210PSym2 l l) arg) (Let0123456789876543210PSym3 l l arg) =>
        Let0123456789876543210PSym2KindInference
    type instance Apply (Let0123456789876543210PSym2 l l) l = Let0123456789876543210P l l l
    instance SuppressUnusedWarnings Let0123456789876543210PSym1 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Let0123456789876543210PSym1KindInference)
               GHC.Tuple.())
    data Let0123456789876543210PSym1 l l
      = forall arg. SameKind (Apply (Let0123456789876543210PSym1 l) arg) (Let0123456789876543210PSym2 l arg) =>
        Let0123456789876543210PSym1KindInference
    type instance Apply (Let0123456789876543210PSym1 l) l = Let0123456789876543210PSym2 l l
    instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Let0123456789876543210PSym0KindInference)
               GHC.Tuple.())
    data Let0123456789876543210PSym0 l
      = forall arg. SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
        Let0123456789876543210PSym0KindInference
    type instance Apply Let0123456789876543210PSym0 l = Let0123456789876543210PSym1 l
    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)
    type Let0123456789876543210PSym2 t t = Let0123456789876543210P t t
    instance SuppressUnusedWarnings Let0123456789876543210PSym1 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Let0123456789876543210PSym1KindInference)
               GHC.Tuple.())
    data Let0123456789876543210PSym1 l l
      = forall arg. SameKind (Apply (Let0123456789876543210PSym1 l) arg) (Let0123456789876543210PSym2 l arg) =>
        Let0123456789876543210PSym1KindInference
    type instance Apply (Let0123456789876543210PSym1 l) l = Let0123456789876543210P l l
    instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Let0123456789876543210PSym0KindInference)
               GHC.Tuple.())
    data Let0123456789876543210PSym0 l
      = forall arg. SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
        Let0123456789876543210PSym0KindInference
    type instance Apply Let0123456789876543210PSym0 l = Let0123456789876543210PSym1 l
    type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 where
      Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 = Apply (Apply Tuple2Sym0 wild_0123456789876543210) wild_0123456789876543210
    type Let0123456789876543210PSym0 = Let0123456789876543210P
    type family Let0123456789876543210P where
      Let0123456789876543210P = NothingSym0
    type Let0123456789876543210PSym3 t t t =
        Let0123456789876543210P t t t
    instance SuppressUnusedWarnings Let0123456789876543210PSym2 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Let0123456789876543210PSym2KindInference)
               GHC.Tuple.())
    data Let0123456789876543210PSym2 l l l
      = forall arg. SameKind (Apply (Let0123456789876543210PSym2 l l) arg) (Let0123456789876543210PSym3 l l arg) =>
        Let0123456789876543210PSym2KindInference
    type instance Apply (Let0123456789876543210PSym2 l l) l = Let0123456789876543210P l l l
    instance SuppressUnusedWarnings Let0123456789876543210PSym1 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Let0123456789876543210PSym1KindInference)
               GHC.Tuple.())
    data Let0123456789876543210PSym1 l l
      = forall arg. SameKind (Apply (Let0123456789876543210PSym1 l) arg) (Let0123456789876543210PSym2 l arg) =>
        Let0123456789876543210PSym1KindInference
    type instance Apply (Let0123456789876543210PSym1 l) l = Let0123456789876543210PSym2 l l
    instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Let0123456789876543210PSym0KindInference)
               GHC.Tuple.())
    data Let0123456789876543210PSym0 l
      = forall arg. SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
        Let0123456789876543210PSym0KindInference
    type instance Apply Let0123456789876543210PSym0 l = Let0123456789876543210PSym1 l
    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)
    type Let0123456789876543210XSym1 t = Let0123456789876543210X t
    instance SuppressUnusedWarnings Let0123456789876543210XSym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Let0123456789876543210XSym0KindInference)
               GHC.Tuple.())
    data Let0123456789876543210XSym0 l
      = forall arg. SameKind (Apply Let0123456789876543210XSym0 arg) (Let0123456789876543210XSym1 arg) =>
        Let0123456789876543210XSym0KindInference
    type instance Apply Let0123456789876543210XSym0 l = Let0123456789876543210X l
    type family Let0123456789876543210X wild_0123456789876543210 where
      Let0123456789876543210X wild_0123456789876543210 = Apply JustSym0 wild_0123456789876543210
    type Let0123456789876543210PSym0 = Let0123456789876543210P
    type family Let0123456789876543210P where
      Let0123456789876543210P = NothingSym0
    type FooSym1 (t :: [Nat]) = Foo t
    instance SuppressUnusedWarnings FooSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) FooSym0KindInference) GHC.Tuple.())
    data FooSym0 (l :: TyFun [Nat] [Nat])
      = forall arg. SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
        FooSym0KindInference
    type instance Apply FooSym0 l = Foo l
    type TupSym1 (t :: (Nat, Nat)) = Tup t
    instance SuppressUnusedWarnings TupSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) TupSym0KindInference) GHC.Tuple.())
    data TupSym0 (l :: TyFun (Nat, Nat) (Nat, Nat))
      = forall arg. SameKind (Apply TupSym0 arg) (TupSym1 arg) =>
        TupSym0KindInference
    type instance Apply TupSym0 l = Tup l
    type Baz_Sym1 (t :: Maybe Baz) = Baz_ t
    instance SuppressUnusedWarnings Baz_Sym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) Baz_Sym0KindInference) GHC.Tuple.())
    data Baz_Sym0 (l :: TyFun (Maybe Baz) (Maybe Baz))
      = forall arg. SameKind (Apply Baz_Sym0 arg) (Baz_Sym1 arg) =>
        Baz_Sym0KindInference
    type instance Apply Baz_Sym0 l = Baz_ l
    type BarSym1 (t :: Maybe Nat) = Bar t
    instance SuppressUnusedWarnings BarSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) BarSym0KindInference) GHC.Tuple.())
    data BarSym0 (l :: TyFun (Maybe Nat) (Maybe Nat))
      = forall arg. SameKind (Apply BarSym0 arg) (BarSym1 arg) =>
        BarSym0KindInference
    type instance Apply BarSym0 l = Bar l
    type MaybePlusSym1 (t :: Maybe Nat) = MaybePlus t
    instance SuppressUnusedWarnings MaybePlusSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) MaybePlusSym0KindInference) GHC.Tuple.())
    data MaybePlusSym0 (l :: TyFun (Maybe Nat) (Maybe Nat))
      = forall arg. SameKind (Apply MaybePlusSym0 arg) (MaybePlusSym1 arg) =>
        MaybePlusSym0KindInference
    type instance Apply MaybePlusSym0 l = MaybePlus l
    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 family Tup (a :: (Nat, Nat)) :: (Nat, Nat) where
      Tup '(wild_0123456789876543210,
            wild_0123456789876543210) = Let0123456789876543210PSym2 wild_0123456789876543210 wild_0123456789876543210
    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 family Bar (a :: Maybe Nat) :: Maybe Nat where
      Bar (Just wild_0123456789876543210) = Let0123456789876543210XSym1 wild_0123456789876543210
      Bar Nothing = NothingSym0
    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])
    sTup ::
      forall (t :: (Nat, Nat)).
      Sing t -> Sing (Apply TupSym0 t :: (Nat, Nat))
    sBaz_ ::
      forall (t :: Maybe Baz).
      Sing t -> Sing (Apply Baz_Sym0 t :: Maybe Baz)
    sBar ::
      forall (t :: Maybe Nat).
      Sing t -> Sing (Apply BarSym0 t :: Maybe Nat)
    sMaybePlus ::
      forall (t :: Maybe Nat).
      Sing t -> Sing (Apply MaybePlusSym0 t :: Maybe Nat)
    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
    data instance Sing (z :: Baz)
      where
        SBaz :: forall (n :: Nat) (n :: Nat) (n :: Nat).
                (Sing (n :: Nat))
                -> (Sing (n :: Nat)) -> (Sing (n :: Nat)) -> Sing (Baz n n n)
    type SBaz = (Sing :: Baz -> GHC.Types.Type)
    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
              ((GHC.Tuple.(,,) (toSing b :: SomeSing Nat))
                 (toSing b :: SomeSing Nat))
                (toSing b :: SomeSing Nat)
          of {
            GHC.Tuple.(,,) (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