AsPattern.ghc76.template

Singletons/AtPattern.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/AtPattern.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 BazTyCtor = Baz
    type BazTyCtorSym0 = BazTyCtor
    data BazSym2 (l :: Nat) (l :: Nat) (l :: TyFun Nat Baz)
    data BazSym1 (l :: Nat) (l :: TyFun Nat (TyFun Nat Baz -> *))
    data BazSym0 (k :: TyFun Nat (TyFun Nat (TyFun Nat Baz -> *) -> *))
    type instance Apply (BazSym2 a a) a = Baz a a a
    type instance Apply (BazSym1 a) a = BazSym2 a a
    type instance Apply BazSym0 a = BazSym1 a
    type family MaybePlus (a :: Maybe Nat) :: Maybe Nat
    type instance MaybePlus (Just n) =
        Apply JustSym0 (Apply (Apply PlusSym0 (Apply SuccSym0 ZeroSym0)) n)
    type instance MaybePlus Nothing = NothingSym0
    data MaybePlusSym0 (k :: TyFun (Maybe Nat) (Maybe Nat))
    type instance Apply MaybePlusSym0 a = MaybePlus a
    type family Bar (a :: Maybe Nat) :: Maybe Nat
    type instance Bar (Just z) = Apply JustSym0 z
    type instance Bar Nothing = NothingSym0
    data BarSym0 (k :: TyFun (Maybe Nat) (Maybe Nat))
    type instance Apply BarSym0 a = Bar a
    type family Baz_ (a :: Maybe Baz) :: Maybe Baz
    type instance Baz_ Nothing = NothingSym0
    type instance Baz_ (Just (Baz z z z)) =
        Apply JustSym0 (Apply (Apply (Apply BazSym0 z) z) z)
    data Baz_Sym0 (k :: TyFun (Maybe Baz) (Maybe Baz))
    type instance Apply Baz_Sym0 a = Baz_ a
    type family Tup (a :: (Nat, Nat)) :: (Nat, Nat)
    type instance Tup '(z, z) = Apply (Apply Tuple2Sym0 z) z
    data TupSym0 (k :: TyFun (Nat, Nat) (Nat, Nat))
    type instance Apply TupSym0 a = Tup a
    type family Foo (a :: [Nat]) :: [Nat]
    type instance Foo GHC.Types.[] = GHC.Types.[]
    type instance Foo '[z] = Apply (Apply :$ z) GHC.Types.[]
    type instance Foo (GHC.Types.: z z) = Apply (Apply :$ z) z
    data FooSym0 (k :: TyFun [Nat] [Nat])
    type instance Apply FooSym0 a = Foo a
    sMaybePlus :: forall (t :: Maybe Nat). Sing t -> Sing (MaybePlus t)
    sMaybePlus (SJust n) = SJust (sPlus (SSucc SZero) n)
    sMaybePlus p@SNothing = p
    sBar :: forall (t :: Maybe Nat). Sing t -> Sing (Bar t)
    sBar x@(SJust _) = x
    sBar SNothing = SNothing
    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 instance DemoteRep (KProxy :: KProxy Baz) = Baz
      fromSing (SBaz b b b) = Baz (fromSing b) (fromSing b) (fromSing b)
      toSing (Baz b b b)
        = case
              (toSing b :: SomeSing (KProxy :: KProxy Nat), 
               toSing b :: SomeSing (KProxy :: KProxy Nat), 
               toSing b :: SomeSing (KProxy :: KProxy 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
    sBaz_ :: forall (t :: Maybe Baz). Sing t -> Sing (Baz_ t)
    sBaz_ p@SNothing = p
    sBaz_ p@(SJust (SBaz _ _ _)) = p
    sTup :: forall (t :: (Nat, Nat)). Sing t -> Sing (Tup t)
    sTup p@(STuple2 _ _) = p
    sFoo :: forall (t :: [Nat]). Sing t -> Sing (Foo t)
    sFoo p@SNil = p
    sFoo p@(SCons _ SNil) = p
    sFoo p@(SCons _ _) = p