Singletons/AsPattern.hs: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 |]
  ======>
    Singletons/AsPattern.hs:(0,0)-(0,0)
    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.: _) = 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 Let_0123456789PSym0 = Let_0123456789P
    type Let_0123456789P = '[]
    type Let_0123456789PSym1 t = Let_0123456789P t
    instance SuppressUnusedWarnings Let_0123456789PSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let_0123456789PSym0KindInference GHC.Tuple.())
    data Let_0123456789PSym0 l
      = forall arg. KindOf (Apply Let_0123456789PSym0 arg) ~ KindOf (Let_0123456789PSym1 arg) =>
        Let_0123456789PSym0KindInference
    type instance Apply Let_0123456789PSym0 l = Let_0123456789PSym1 l
    type Let_0123456789P wild_0123456789 =
        Apply (Apply (:$) wild_0123456789) '[]
    type Let_0123456789PSym2 t t = Let_0123456789P t t
    instance SuppressUnusedWarnings Let_0123456789PSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let_0123456789PSym1KindInference GHC.Tuple.())
    data Let_0123456789PSym1 l l
      = forall arg. KindOf (Apply (Let_0123456789PSym1 l) arg) ~ KindOf (Let_0123456789PSym2 l arg) =>
        Let_0123456789PSym1KindInference
    type instance Apply (Let_0123456789PSym1 l) l = Let_0123456789PSym2 l l
    instance SuppressUnusedWarnings Let_0123456789PSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let_0123456789PSym0KindInference GHC.Tuple.())
    data Let_0123456789PSym0 l
      = forall arg. KindOf (Apply Let_0123456789PSym0 arg) ~ KindOf (Let_0123456789PSym1 arg) =>
        Let_0123456789PSym0KindInference
    type instance Apply Let_0123456789PSym0 l = Let_0123456789PSym1 l
    type Let_0123456789P wild_0123456789 wild_0123456789 =
        Apply (Apply (:$) wild_0123456789) wild_0123456789
    type Let_0123456789PSym2 t t = Let_0123456789P t t
    instance SuppressUnusedWarnings Let_0123456789PSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let_0123456789PSym1KindInference GHC.Tuple.())
    data Let_0123456789PSym1 l l
      = forall arg. KindOf (Apply (Let_0123456789PSym1 l) arg) ~ KindOf (Let_0123456789PSym2 l arg) =>
        Let_0123456789PSym1KindInference
    type instance Apply (Let_0123456789PSym1 l) l = Let_0123456789PSym2 l l
    instance SuppressUnusedWarnings Let_0123456789PSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let_0123456789PSym0KindInference GHC.Tuple.())
    data Let_0123456789PSym0 l
      = forall arg. KindOf (Apply Let_0123456789PSym0 arg) ~ KindOf (Let_0123456789PSym1 arg) =>
        Let_0123456789PSym0KindInference
    type instance Apply Let_0123456789PSym0 l = Let_0123456789PSym1 l
    type Let_0123456789P wild_0123456789 wild_0123456789 =
        Apply (Apply Tuple2Sym0 wild_0123456789) wild_0123456789
    type Let_0123456789PSym0 = Let_0123456789P
    type Let_0123456789P = NothingSym0
    type Let_0123456789PSym3 t t t = Let_0123456789P t t t
    instance SuppressUnusedWarnings Let_0123456789PSym2 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let_0123456789PSym2KindInference GHC.Tuple.())
    data Let_0123456789PSym2 l l l
      = forall arg. KindOf (Apply (Let_0123456789PSym2 l l) arg) ~ KindOf (Let_0123456789PSym3 l l arg) =>
        Let_0123456789PSym2KindInference
    type instance Apply (Let_0123456789PSym2 l l) l = Let_0123456789PSym3 l l l
    instance SuppressUnusedWarnings Let_0123456789PSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let_0123456789PSym1KindInference GHC.Tuple.())
    data Let_0123456789PSym1 l l
      = forall arg. KindOf (Apply (Let_0123456789PSym1 l) arg) ~ KindOf (Let_0123456789PSym2 l arg) =>
        Let_0123456789PSym1KindInference
    type instance Apply (Let_0123456789PSym1 l) l = Let_0123456789PSym2 l l
    instance SuppressUnusedWarnings Let_0123456789PSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let_0123456789PSym0KindInference GHC.Tuple.())
    data Let_0123456789PSym0 l
      = forall arg. KindOf (Apply Let_0123456789PSym0 arg) ~ KindOf (Let_0123456789PSym1 arg) =>
        Let_0123456789PSym0KindInference
    type instance Apply Let_0123456789PSym0 l = Let_0123456789PSym1 l
    type Let_0123456789P wild_0123456789
                         wild_0123456789
                         wild_0123456789 =
        Apply JustSym0 (Apply (Apply (Apply BazSym0 wild_0123456789) wild_0123456789) wild_0123456789)
    type Let_0123456789XSym1 t = Let_0123456789X t
    instance SuppressUnusedWarnings Let_0123456789XSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let_0123456789XSym0KindInference GHC.Tuple.())
    data Let_0123456789XSym0 l
      = forall arg. KindOf (Apply Let_0123456789XSym0 arg) ~ KindOf (Let_0123456789XSym1 arg) =>
        Let_0123456789XSym0KindInference
    type instance Apply Let_0123456789XSym0 l = Let_0123456789XSym1 l
    type Let_0123456789X wild_0123456789 =
        Apply JustSym0 wild_0123456789
    type Let_0123456789PSym0 = Let_0123456789P
    type Let_0123456789P = 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 '[] = Let_0123456789PSym0
      Foo '[wild_0123456789] = Let_0123456789PSym1 wild_0123456789
      Foo ((:) wild_0123456789 wild_0123456789) = Let_0123456789PSym2 wild_0123456789 wild_0123456789
    type family Tup (a :: (Nat, Nat)) :: (Nat, Nat) where
      Tup '(wild_0123456789,
            wild_0123456789) = Let_0123456789PSym2 wild_0123456789 wild_0123456789
    type family Baz_ (a :: Maybe Baz) :: Maybe Baz where
      Baz_ Nothing = Let_0123456789PSym0
      Baz_ (Just (Baz wild_0123456789 wild_0123456789 wild_0123456789)) = Let_0123456789PSym3 wild_0123456789 wild_0123456789 wild_0123456789
    type family Bar (a :: Maybe Nat) :: Maybe Nat where
      Bar (Just wild_0123456789) = Let_0123456789XSym1 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 = Let_0123456789PSym0
    sFoo :: forall (t :: [Nat]). Sing t -> Sing (Apply FooSym0 t)
    sTup :: forall (t :: (Nat, Nat)). Sing t -> Sing (Apply TupSym0 t)
    sBaz_ :: forall (t :: Maybe Baz). Sing t -> Sing (Apply Baz_Sym0 t)
    sBar :: forall (t :: Maybe Nat). Sing t -> Sing (Apply BarSym0 t)
    sMaybePlus ::
      forall (t :: Maybe Nat). Sing t -> Sing (Apply MaybePlusSym0 t)
    sFoo SNil
      = let
          lambda :: t ~ '[] => Sing (Apply FooSym0 '[])
          lambda
            = let
                sP :: Sing Let_0123456789PSym0
                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 (Apply (Apply (:$) wild_0123456789) '[]))
          lambda wild_0123456789
            = let
                sP :: Sing (Let_0123456789PSym1 wild_0123456789)
                sP
                  = applySing
                      (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) wild_0123456789)
                      SNil
              in sP
        in lambda sWild_0123456789
    sFoo (SCons sWild_0123456789 sWild_0123456789)
      = let
          lambda ::
            forall wild_0123456789
                   wild_0123456789. t ~ Apply (Apply (:$) wild_0123456789) wild_0123456789 =>
            Sing wild_0123456789
            -> Sing wild_0123456789
               -> Sing (Apply FooSym0 (Apply (Apply (:$) wild_0123456789) wild_0123456789))
          lambda wild_0123456789 wild_0123456789
            = let
                sP :: Sing (Let_0123456789PSym2 wild_0123456789 wild_0123456789)
                sP
                  = applySing
                      (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) wild_0123456789)
                      wild_0123456789
              in sP
        in lambda 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 (Apply (Apply Tuple2Sym0 wild_0123456789) wild_0123456789))
          lambda wild_0123456789 wild_0123456789
            = let
                sP :: Sing (Let_0123456789PSym2 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 NothingSym0)
          lambda
            = let
                sP :: Sing Let_0123456789PSym0
                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 (Apply JustSym0 (Apply (Apply (Apply BazSym0 wild_0123456789) wild_0123456789) wild_0123456789)))
          lambda wild_0123456789 wild_0123456789 wild_0123456789
            = let
                sP ::
                  Sing (Let_0123456789PSym3 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 (Apply JustSym0 wild_0123456789))
          lambda wild_0123456789
            = let
                sX :: Sing (Let_0123456789XSym1 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 NothingSym0)
          lambda = SNothing
        in lambda
    sMaybePlus (SJust sN)
      = let
          lambda ::
            forall n. t ~ Apply JustSym0 n =>
            Sing n -> Sing (Apply MaybePlusSym0 (Apply JustSym0 n))
          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 NothingSym0)
          lambda
            = let
                sP :: Sing Let_0123456789PSym0
                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) (Sing n) (Sing n)
    type SBaz (z :: Baz) = Sing z
    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