singletons-2.2: tests/compile-and-dump/Singletons/AsPattern.ghc80.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. 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 -> GHC.Types.Type))
= 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
-> GHC.Types.Type)
-> GHC.Types.Type))
= 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 -> GHC.Types.Type)
instance SingKind Baz where
type DemoteRep 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