singletons-2.3: tests/compile-and-dump/Singletons/AsPattern.ghc82.template
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
= '[]
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
= 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
= 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)
= 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 -> 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 b b)
= 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