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. KindOf (Apply (BazSym2 l l) arg) ~ KindOf (BazSym3 l l arg) =>
        BazSym2KindInference
    type instance Apply (BazSym2 l l) l = BazSym3 l l l
    instance SuppressUnusedWarnings BazSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) BazSym1KindInference GHC.Tuple.())
    data BazSym1 (l :: Nat) (l :: TyFun Nat (TyFun Nat Baz -> *))
      = forall arg. KindOf (Apply (BazSym1 l) arg) ~ KindOf (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 -> *) -> *))
      = forall arg. KindOf (Apply BazSym0 arg) ~ KindOf (BazSym1 arg) =>
        BazSym0KindInference
    type instance Apply BazSym0 l = BazSym1 l
    type Let0123456789PSym0 = Let0123456789P
    type family Let0123456789P where
      Let0123456789P = '[]
    type Let0123456789PSym1 t = Let0123456789P t
    instance SuppressUnusedWarnings Let0123456789PSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789PSym0KindInference GHC.Tuple.())
    data Let0123456789PSym0 l
      = forall arg. KindOf (Apply Let0123456789PSym0 arg) ~ KindOf (Let0123456789PSym1 arg) =>
        Let0123456789PSym0KindInference
    type instance Apply Let0123456789PSym0 l = Let0123456789PSym1 l
    type family Let0123456789P wild_0123456789 where
      Let0123456789P wild_0123456789 = Apply (Apply (:$) wild_0123456789) '[]
    type Let0123456789PSym3 t t t = Let0123456789P t t t
    instance SuppressUnusedWarnings Let0123456789PSym2 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789PSym2KindInference GHC.Tuple.())
    data Let0123456789PSym2 l l l
      = forall arg. KindOf (Apply (Let0123456789PSym2 l l) arg) ~ KindOf (Let0123456789PSym3 l l arg) =>
        Let0123456789PSym2KindInference
    type instance Apply (Let0123456789PSym2 l l) l = Let0123456789PSym3 l l l
    instance SuppressUnusedWarnings Let0123456789PSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789PSym1KindInference GHC.Tuple.())
    data Let0123456789PSym1 l l
      = forall arg. KindOf (Apply (Let0123456789PSym1 l) arg) ~ KindOf (Let0123456789PSym2 l arg) =>
        Let0123456789PSym1KindInference
    type instance Apply (Let0123456789PSym1 l) l = Let0123456789PSym2 l l
    instance SuppressUnusedWarnings Let0123456789PSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789PSym0KindInference GHC.Tuple.())
    data Let0123456789PSym0 l
      = forall arg. KindOf (Apply Let0123456789PSym0 arg) ~ KindOf (Let0123456789PSym1 arg) =>
        Let0123456789PSym0KindInference
    type instance Apply Let0123456789PSym0 l = Let0123456789PSym1 l
    type family Let0123456789P wild_0123456789
                               wild_0123456789
                               wild_0123456789 where
      Let0123456789P wild_0123456789 wild_0123456789 wild_0123456789 = Apply (Apply (:$) wild_0123456789) (Apply (Apply (:$) wild_0123456789) wild_0123456789)
    type Let0123456789PSym2 t t = Let0123456789P t t
    instance SuppressUnusedWarnings Let0123456789PSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789PSym1KindInference GHC.Tuple.())
    data Let0123456789PSym1 l l
      = forall arg. KindOf (Apply (Let0123456789PSym1 l) arg) ~ KindOf (Let0123456789PSym2 l arg) =>
        Let0123456789PSym1KindInference
    type instance Apply (Let0123456789PSym1 l) l = Let0123456789PSym2 l l
    instance SuppressUnusedWarnings Let0123456789PSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789PSym0KindInference GHC.Tuple.())
    data Let0123456789PSym0 l
      = forall arg. KindOf (Apply Let0123456789PSym0 arg) ~ KindOf (Let0123456789PSym1 arg) =>
        Let0123456789PSym0KindInference
    type instance Apply Let0123456789PSym0 l = Let0123456789PSym1 l
    type family Let0123456789P wild_0123456789 wild_0123456789 where
      Let0123456789P wild_0123456789 wild_0123456789 = Apply (Apply Tuple2Sym0 wild_0123456789) wild_0123456789
    type Let0123456789PSym0 = Let0123456789P
    type family Let0123456789P where
      Let0123456789P = NothingSym0
    type Let0123456789PSym3 t t t = Let0123456789P t t t
    instance SuppressUnusedWarnings Let0123456789PSym2 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789PSym2KindInference GHC.Tuple.())
    data Let0123456789PSym2 l l l
      = forall arg. KindOf (Apply (Let0123456789PSym2 l l) arg) ~ KindOf (Let0123456789PSym3 l l arg) =>
        Let0123456789PSym2KindInference
    type instance Apply (Let0123456789PSym2 l l) l = Let0123456789PSym3 l l l
    instance SuppressUnusedWarnings Let0123456789PSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789PSym1KindInference GHC.Tuple.())
    data Let0123456789PSym1 l l
      = forall arg. KindOf (Apply (Let0123456789PSym1 l) arg) ~ KindOf (Let0123456789PSym2 l arg) =>
        Let0123456789PSym1KindInference
    type instance Apply (Let0123456789PSym1 l) l = Let0123456789PSym2 l l
    instance SuppressUnusedWarnings Let0123456789PSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789PSym0KindInference GHC.Tuple.())
    data Let0123456789PSym0 l
      = forall arg. KindOf (Apply Let0123456789PSym0 arg) ~ KindOf (Let0123456789PSym1 arg) =>
        Let0123456789PSym0KindInference
    type instance Apply Let0123456789PSym0 l = Let0123456789PSym1 l
    type family Let0123456789P wild_0123456789
                               wild_0123456789
                               wild_0123456789 where
      Let0123456789P wild_0123456789 wild_0123456789 wild_0123456789 = Apply JustSym0 (Apply (Apply (Apply BazSym0 wild_0123456789) wild_0123456789) wild_0123456789)
    type Let0123456789XSym1 t = Let0123456789X t
    instance SuppressUnusedWarnings Let0123456789XSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789XSym0KindInference GHC.Tuple.())
    data Let0123456789XSym0 l
      = forall arg. KindOf (Apply Let0123456789XSym0 arg) ~ KindOf (Let0123456789XSym1 arg) =>
        Let0123456789XSym0KindInference
    type instance Apply Let0123456789XSym0 l = Let0123456789XSym1 l
    type family Let0123456789X wild_0123456789 where
      Let0123456789X wild_0123456789 = Apply JustSym0 wild_0123456789
    type Let0123456789PSym0 = Let0123456789P
    type family Let0123456789P where
      Let0123456789P = 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. KindOf (Apply FooSym0 arg) ~ KindOf (FooSym1 arg) =>
        FooSym0KindInference
    type instance Apply FooSym0 l = FooSym1 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. KindOf (Apply TupSym0 arg) ~ KindOf (TupSym1 arg) =>
        TupSym0KindInference
    type instance Apply TupSym0 l = TupSym1 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. KindOf (Apply Baz_Sym0 arg) ~ KindOf (Baz_Sym1 arg) =>
        Baz_Sym0KindInference
    type instance Apply Baz_Sym0 l = Baz_Sym1 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. KindOf (Apply BarSym0 arg) ~ KindOf (BarSym1 arg) =>
        BarSym0KindInference
    type instance Apply BarSym0 l = BarSym1 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. KindOf (Apply MaybePlusSym0 arg) ~ KindOf (MaybePlusSym1 arg) =>
        MaybePlusSym0KindInference
    type instance Apply MaybePlusSym0 l = MaybePlusSym1 l
    type family Foo (a :: [Nat]) :: [Nat] where
      Foo '[] = Let0123456789PSym0
      Foo '[wild_0123456789] = Let0123456789PSym1 wild_0123456789
      Foo ((:) wild_0123456789 ((:) wild_0123456789 wild_0123456789)) = Let0123456789PSym3 wild_0123456789 wild_0123456789 wild_0123456789
    type family Tup (a :: (Nat, Nat)) :: (Nat, Nat) where
      Tup '(wild_0123456789,
            wild_0123456789) = Let0123456789PSym2 wild_0123456789 wild_0123456789
    type family Baz_ (a :: Maybe Baz) :: Maybe Baz where
      Baz_ Nothing = Let0123456789PSym0
      Baz_ (Just (Baz wild_0123456789 wild_0123456789 wild_0123456789)) = Let0123456789PSym3 wild_0123456789 wild_0123456789 wild_0123456789
    type family Bar (a :: Maybe Nat) :: Maybe Nat where
      Bar (Just wild_0123456789) = Let0123456789XSym1 wild_0123456789
      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 = Let0123456789PSym0
    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
          lambda :: t ~ '[] => Sing (Apply FooSym0 t :: [Nat])
          lambda
            = let
                sP :: Sing Let0123456789PSym0
                sP = SNil
              in sP
        in lambda
    sFoo (SCons sWild_0123456789 SNil)
      = let
          lambda ::
            forall wild_0123456789. t ~ Apply (Apply (:$) wild_0123456789) '[] =>
            Sing wild_0123456789 -> Sing (Apply FooSym0 t :: [Nat])
          lambda wild_0123456789
            = let
                sP :: Sing (Let0123456789PSym1 wild_0123456789)
                sP
                  = applySing
                      (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) wild_0123456789)
                      SNil
              in sP
        in lambda sWild_0123456789
    sFoo
      (SCons sWild_0123456789 (SCons sWild_0123456789 sWild_0123456789))
      = let
          lambda ::
            forall wild_0123456789
                   wild_0123456789
                   wild_0123456789. t ~ Apply (Apply (:$) wild_0123456789) (Apply (Apply (:$) wild_0123456789) wild_0123456789) =>
            Sing wild_0123456789
            -> Sing wild_0123456789
               -> Sing wild_0123456789 -> Sing (Apply FooSym0 t :: [Nat])
          lambda wild_0123456789 wild_0123456789 wild_0123456789
            = let
                sP ::
                  Sing (Let0123456789PSym3 wild_0123456789 wild_0123456789 wild_0123456789)
                sP
                  = applySing
                      (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) wild_0123456789)
                      (applySing
                         (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) wild_0123456789)
                         wild_0123456789)
              in sP
        in lambda sWild_0123456789 sWild_0123456789 sWild_0123456789
    sTup (STuple2 sWild_0123456789 sWild_0123456789)
      = let
          lambda ::
            forall wild_0123456789
                   wild_0123456789. t ~ Apply (Apply Tuple2Sym0 wild_0123456789) wild_0123456789 =>
            Sing wild_0123456789
            -> Sing wild_0123456789 -> Sing (Apply TupSym0 t :: (Nat, Nat))
          lambda wild_0123456789 wild_0123456789
            = let
                sP :: Sing (Let0123456789PSym2 wild_0123456789 wild_0123456789)
                sP
                  = applySing
                      (applySing
                         (singFun2 (Proxy :: Proxy Tuple2Sym0) STuple2) wild_0123456789)
                      wild_0123456789
              in sP
        in lambda sWild_0123456789 sWild_0123456789
    sBaz_ SNothing
      = let
          lambda :: t ~ NothingSym0 => Sing (Apply Baz_Sym0 t :: Maybe Baz)
          lambda
            = let
                sP :: Sing Let0123456789PSym0
                sP = SNothing
              in sP
        in lambda
    sBaz_
      (SJust (SBaz sWild_0123456789 sWild_0123456789 sWild_0123456789))
      = let
          lambda ::
            forall wild_0123456789
                   wild_0123456789
                   wild_0123456789. t ~ Apply JustSym0 (Apply (Apply (Apply BazSym0 wild_0123456789) wild_0123456789) wild_0123456789) =>
            Sing wild_0123456789
            -> Sing wild_0123456789
               -> Sing wild_0123456789 -> Sing (Apply Baz_Sym0 t :: Maybe Baz)
          lambda wild_0123456789 wild_0123456789 wild_0123456789
            = let
                sP ::
                  Sing (Let0123456789PSym3 wild_0123456789 wild_0123456789 wild_0123456789)
                sP
                  = applySing
                      (singFun1 (Proxy :: Proxy JustSym0) SJust)
                      (applySing
                         (applySing
                            (applySing
                               (singFun3 (Proxy :: Proxy BazSym0) SBaz) wild_0123456789)
                            wild_0123456789)
                         wild_0123456789)
              in sP
        in lambda sWild_0123456789 sWild_0123456789 sWild_0123456789
    sBar (SJust sWild_0123456789)
      = let
          lambda ::
            forall wild_0123456789. t ~ Apply JustSym0 wild_0123456789 =>
            Sing wild_0123456789 -> Sing (Apply BarSym0 t :: Maybe Nat)
          lambda wild_0123456789
            = let
                sX :: Sing (Let0123456789XSym1 wild_0123456789)
                sX
                  = applySing
                      (singFun1 (Proxy :: Proxy JustSym0) SJust) wild_0123456789
              in sX
        in lambda sWild_0123456789
    sBar SNothing
      = let
          lambda :: t ~ NothingSym0 => Sing (Apply BarSym0 t :: Maybe Nat)
          lambda = SNothing
        in lambda
    sMaybePlus (SJust sN)
      = let
          lambda ::
            forall n. t ~ Apply JustSym0 n =>
            Sing n -> Sing (Apply MaybePlusSym0 t :: Maybe Nat)
          lambda n
            = applySing
                (singFun1 (Proxy :: Proxy JustSym0) SJust)
                (applySing
                   (applySing
                      (singFun2 (Proxy :: Proxy PlusSym0) sPlus)
                      (applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero))
                   n)
        in lambda sN
    sMaybePlus SNothing
      = let
          lambda ::
            t ~ NothingSym0 => Sing (Apply MaybePlusSym0 t :: Maybe Nat)
          lambda
            = let
                sP :: Sing Let0123456789PSym0
                sP = SNothing
              in sP
        in lambda
    data instance Sing (z :: Baz)
      = forall (n :: Nat) (n :: Nat) (n :: Nat). z ~ Baz n n n =>
        SBaz (Sing (n :: Nat)) (Sing (n :: Nat)) (Sing (n :: Nat))
    type SBaz = (Sing :: Baz -> *)
    instance SingKind (KProxy :: KProxy Baz) where
      type DemoteRep (KProxy :: KProxy Baz) = Baz
      fromSing (SBaz b b b) = Baz (fromSing b) (fromSing b) (fromSing b)
      toSing (Baz b b b)
        = case
              GHC.Tuple.(,,)
                (toSing b :: SomeSing (KProxy :: KProxy Nat))
                (toSing b :: SomeSing (KProxy :: KProxy Nat))
                (toSing b :: SomeSing (KProxy :: KProxy 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