Commit 04b0a73a authored by Simon Peyton Jones's avatar Simon Peyton Jones

Pattern synonyms: swap provided/required

This patch swaps the order of provided and required constraints in
a pattern signature, so it now goes

      pattern P :: req => prov => t1 -> ... tn -> res_ty

See the long discussion in Trac #10928.

I think I have found all the places, but I could have missed something
particularly in comments.

There is a Haddock changes; so a submodule update.
parent 9fc2d777
......@@ -46,6 +46,7 @@ import Data.Function
-- | A pattern synonym
-- See Note [Pattern synonym representation]
-- See Note [Patten synonym signatures]
data PatSyn
= MkPatSyn {
psName :: Name,
......@@ -89,7 +90,44 @@ data PatSyn
}
deriving Data.Typeable.Typeable
{-
{- Note [Patten synonym signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a pattern synonym signature we write
pattern P :: req => prov => t1 -> ... tn -> res_ty
Note that the "required" context comes first, then the "provided"
context. Moreover, the "required" context must not mention
existentially-bound type variables; that is, ones not mentioned in
res_ty. See lots of discussion in Trac #10928.
If there is no "provided" context, you can omit it; but you
can't omit the "required" part (unless you omit both).
Example 1:
pattern P1 :: (Num a, Eq a) => b -> Maybe (a,b)
pattern P1 x = Just (3,x)
We require (Num a, Eq a) to match the 3; there is no provided
context.
Example 2:
data T2 where
MkT2 :: (Num a, Eq a) => a -> a -> T2
patttern P2 :: () => (Num a, Eq a) => a -> T2
pattern P2 x = MkT2 3 x
When we match against P2 we get a Num dictionary provided.
We can use that to check the match against 3.
Example 3:
pattern P3 :: Eq a => a -> b -> T3 b
This signature is illegal because the (Eq a) is a required
constraint, but it mentions the existentially-bound variable 'a'.
You can see it's existential because it doesn't appear in the
result type (T3 b).
Note [Pattern synonym representation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following pattern synonym declaration
......@@ -267,6 +305,7 @@ patSynName = psName
patSynType :: PatSyn -> Type
-- The full pattern type, used only in error messages
-- See Note [Patten synonym signatures]
patSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta
, psExTyVars = ex_tvs, psProvTheta = prov_theta
, psArgs = orig_args, psOrigResTy = orig_res_ty })
......@@ -288,11 +327,11 @@ patSynArgs = psArgs
patSynExTyVars :: PatSyn -> [TyVar]
patSynExTyVars = psExTyVars
patSynSig :: PatSyn -> ([TyVar], [TyVar], ThetaType, ThetaType, [Type], Type)
patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Type], Type)
patSynSig (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs
, psProvTheta = prov, psReqTheta = req
, psArgs = arg_tys, psOrigResTy = res_ty })
= (univ_tvs, ex_tvs, prov, req, arg_tys, res_ty)
= (univ_tvs, req, ex_tvs, prov, arg_tys, res_ty)
patSynMatcher :: PatSyn -> (Id,Bool)
patSynMatcher = psMatcher
......
......@@ -641,8 +641,8 @@ data Sig name
-- For details on above see note [Api annotations] in ApiAnnotation
| PatSynSig (Located name)
(HsExplicitFlag, LHsTyVarBndrs name)
(LHsContext name) -- Provided context
(LHsContext name) -- Required context
(LHsContext name) -- Provided context
(LHsType name)
-- | A type signature for a default method inside a class
......@@ -839,23 +839,23 @@ ppr_sig (InlineSig var inl) = pragBrackets (ppr inl <+> pprPrefixOcc (unLo
ppr_sig (SpecInstSig _ ty)
= pragBrackets (ptext (sLit "SPECIALIZE instance") <+> ppr ty)
ppr_sig (MinimalSig _ bf) = pragBrackets (pprMinimalSig bf)
ppr_sig (PatSynSig name (flag, qtvs) (L _ prov) (L _ req) ty)
ppr_sig (PatSynSig name (flag, qtvs) (L _ req) (L _ prov) ty)
= pprPatSynSig (unLoc name) False -- TODO: is_bindir
(pprHsForAll flag qtvs (noLoc []))
(pprHsContextMaybe prov) (pprHsContextMaybe req)
(pprHsContextMaybe req) (pprHsContextMaybe prov)
(ppr ty)
pprPatSynSig :: (OutputableBndr name)
=> name -> Bool -> SDoc -> Maybe SDoc -> Maybe SDoc -> SDoc -> SDoc
pprPatSynSig ident _is_bidir tvs prov req ty
pprPatSynSig ident _is_bidir tvs req prov ty
= ptext (sLit "pattern") <+> pprPrefixOcc ident <+> dcolon <+>
tvs <+> context <+> ty
where
context = case (prov, req) of
context = case (req, prov) of
(Nothing, Nothing) -> empty
(Nothing, Just req) -> parens empty <+> darrow <+> req <+> darrow
(Just prov, Nothing) -> prov <+> darrow
(Just prov, Just req) -> prov <+> darrow <+> req <+> darrow
(Nothing, Just prov) -> parens empty <+> darrow <+> prov <+> darrow
(Just req, Nothing) -> req <+> darrow
(Just req, Just prov) -> req <+> darrow <+> prov <+> darrow
instance OutputableBndr name => Outputable (FixitySig name) where
ppr (FixitySig names fixity) = sep [ppr fixity, pprops]
......
......@@ -772,8 +772,8 @@ pprIfaceDecl _ (IfacePatSyn { ifName = name, ifPatBuilder = builder,
ifPatTy = pat_ty} )
= pprPatSynSig name is_bidirectional
(pprUserIfaceForAll tvs)
(pprIfaceContextMaybe prov_ctxt)
(pprIfaceContextMaybe req_ctxt)
(pprIfaceContextMaybe prov_ctxt)
(pprIfaceType ty)
where
is_bidirectional = isJust builder
......
......@@ -1524,7 +1524,7 @@ patSynToIfaceDecl ps
, ifPatTy = tidyToIfaceType env2 rhs_ty
}
where
(univ_tvs, ex_tvs, prov_theta, req_theta, args, rhs_ty) = patSynSig ps
(univ_tvs, req_theta, ex_tvs, prov_theta, args, rhs_ty) = patSynSig ps
(env1, univ_tvs') = tidyTyVarBndrs emptyTidyEnv univ_tvs
(env2, ex_tvs') = tidyTyVarBndrs env1 ex_tvs
to_if_pr (id, needs_dummy) = (idName id, needs_dummy)
......
......@@ -923,7 +923,7 @@ renameSig ctxt sig@(MinimalSig s bf)
= do new_bf <- traverse (lookupSigOccRn ctxt sig) bf
return (MinimalSig s new_bf, emptyFVs)
renameSig ctxt sig@(PatSynSig v (flag, qtvs) prov req ty)
renameSig ctxt sig@(PatSynSig v (flag, qtvs) req prov ty)
= do { v' <- lookupSigOccRn ctxt sig v
; let doc = TypeSigCtx $ quotes (ppr v)
; loc <- getSrcSpanM
......@@ -940,12 +940,12 @@ renameSig ctxt sig@(PatSynSig v (flag, qtvs) prov req ty)
Qualified -> panic "renameSig: Qualified"
; bindHsTyVars doc Nothing tv_kvs tv_bndrs $ \ tyvars -> do
{ (prov', fvs1) <- rnContext doc prov
; (req', fvs2) <- rnContext doc req
{ (req', fvs2) <- rnContext doc req
; (prov', fvs1) <- rnContext doc prov
; (ty', fvs3) <- rnLHsType doc ty
; let fvs = plusFVs [fvs1, fvs2, fvs3]
; return (PatSynSig v' (flag, tyvars) prov' req' ty', fvs) }}
; return (PatSynSig v' (flag, tyvars) req' prov' ty', fvs) }}
ppr_sig_bndrs :: [Located RdrName] -> SDoc
ppr_sig_bndrs bs = quotes (pprWithCommas ppr bs)
......
......@@ -1621,20 +1621,31 @@ tcTySig (L loc (TypeSig names@(L _ name1 : _) hs_ty wcs))
; sig <- instTcTySig ctxt hs_ty sigma_ty (extra_cts hs_ty) wc_prs name
; return (TcIdSig sig) }
tcTySig (L loc (PatSynSig (L _ name) (_, qtvs) prov req ty))
tcTySig (L loc (PatSynSig (L _ name) (_, qtvs) req prov ty))
= setSrcSpan loc $
do { traceTc "tcTySig {" $ ppr name $$ ppr qtvs $$ ppr prov $$ ppr req $$ ppr ty
do { traceTc "tcTySig {" $ ppr name $$ ppr qtvs $$ ppr req $$ ppr prov $$ ppr ty
; let ctxt = PatSynCtxt name
; tcHsTyVarBndrs qtvs $ \ qtvs' -> do
{ ty' <- tcHsSigType ctxt ty
; req' <- tcHsContext req
; prov' <- tcHsContext prov
-- These are /signatures/ so we zonk to squeeze out any kind
-- unification variables. Thta has happened automatically in tcHsSigType
; req' <- zonkTcThetaType req'
; prov' <- zonkTcThetaType prov'
; qtvs' <- mapM zonkQuantifiedTyVar qtvs'
; let (_, pat_ty) = tcSplitFunTys ty'
univ_set = tyVarsOfType pat_ty
(univ_tvs, ex_tvs) = partition (`elemVarSet` univ_set) qtvs'
bad_tvs = varSetElems (tyVarsOfTypes req' `minusVarSet` univ_set)
; unless (null bad_tvs) $ addErr $
hang (ptext (sLit "The 'required' context") <+> quotes (pprTheta req'))
2 (ptext (sLit "mentions existential type variable") <> plural bad_tvs
<+> pprQuotedList bad_tvs)
; traceTc "tcTySig }" $ ppr (ex_tvs, prov') $$ ppr (univ_tvs, req') $$ ppr ty'
; let tpsi = TPSI{ patsig_name = name,
......
......@@ -882,7 +882,7 @@ tcPatSynPat :: PatEnv -> Located Name -> PatSyn
-> HsConPatDetails Name -> TcM a
-> TcM (Pat TcId, a)
tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
= do { let (univ_tvs, ex_tvs, prov_theta, req_theta, arg_tys, ty) = patSynSig pat_syn
= do { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
; (subst, univ_tvs') <- tcInstTyVars univ_tvs
......
......@@ -830,17 +830,17 @@ it is assigned a *pattern type* of the form
::
pattern P :: CProv => CReq => t1 -> t2 -> ... -> tN -> t
pattern P :: CReq => CProf => t1 -> t2 -> ... -> tN -> t
where ⟨CProv⟩ and ⟨CReq⟩ are type contexts, and ⟨t1⟩, ⟨t2⟩, ..., ⟨tN⟩
and ⟨t⟩ are types. Notice the unusual form of the type, with two
contexts ⟨CProv⟩ and ⟨CReq⟩:
- ⟨CReq⟩ are the constraints *required* to match the pattern.
- ⟨CProv⟩ are the constraints *made available (provided)* by a
successful pattern match.
- ⟨CReq⟩ are the constraints *required* to match the pattern.
For example, consider
::
......@@ -851,7 +851,7 @@ For example, consider
f1 :: (Eq a, Num a) => T a -> String
f1 (MkT 42 x) = show x
pattern ExNumPat :: (Show b) => (Num a, Eq a) => b -> T a
pattern ExNumPat :: (Num a, Eq a) => (Show b) => b -> T a
pattern ExNumPat x = MkT 42 x
f2 :: (Eq a, Num a) => T a -> String
......@@ -871,7 +871,7 @@ Exactly the same reasoning applies to ``ExNumPat``: matching against
Note also the following points
- In the common case where ``CReq`` is empty, ``()``, it can be omitted
- In the common case where ``Prov`` is empty, ``()``, it can be omitted
altogether.
- You may specify an explicit *pattern signature*, as we did for
......@@ -892,14 +892,14 @@ Note also the following points
::
(CProv, CReq) => t1 -> t2 -> ... -> tN -> t
(CReq, CProv) => t1 -> t2 -> ... -> tN -> t
So in the previous example, when used in an expression, ``ExNumPat``
has type
::
ExNumPat :: (Show b, Num a, Eq a) => b -> T t
ExNumPat :: (Num a, Eq a, Show b) => b -> T t
Notice that this is a tiny bit more restrictive than the expression
``MkT 42 x`` which would not require ``(Eq a)``.
......@@ -911,8 +911,8 @@ Note also the following points
data S a where
S1 :: Bool -> S Bool
pattern P1 b = Just b -- P1 :: Bool -> Maybe Bool
pattern P2 b = S1 b -- P2 :: (b~Bool) => Bool -> S b
pattern P1 b = Just b -- P1 :: Bool -> Maybe Bool
pattern P2 b = S1 b -- P2 :: () => (b~Bool) => Bool -> S b
f :: Maybe a -> String
f (P1 x) = "no no no" -- Type-incorrect
......
pattern P :: (Num t, Eq t1) => A t t1 -- Defined at T8776.hs:6:1
pattern P :: () => (Num t, Eq t1) => A t t1
-- Defined at T8776.hs:6:1
......@@ -11,7 +11,7 @@ extractJust :: Maybe a -> (Bool, a)
extractJust (Just a) = (True, a)
extractJust _ = (False, undefined)
pattern Just' :: () => (Showable a) => a -> (Maybe a)
pattern Just' :: Showable a => a -> (Maybe a)
pattern Just' a <- (extractJust -> (True, a)) where
Just' a = Just a
......@@ -5,7 +5,7 @@ module T10997a where
data Exp ty where
LitB :: Bool -> Exp Bool
pattern Tru :: b ~ Bool => Exp b
pattern Tru :: () => b ~ Bool => Exp b
pattern Tru = LitB True
......@@ -3,7 +3,7 @@
module ShouldCompile where
pattern Single :: () => (Show a) => a -> [a]
pattern Single :: Show a => a -> [a]
pattern Single x = [x]
f :: (Show a) => [a] -> a
......
{-# LANGUAGE PatternSynonyms, ExistentialQuantification, GADTSyntax #-}
module T11010 where
data Expr a where
Fun :: String -> (a -> b) -> (Expr a -> Expr b)
pattern IntFun :: (a ~ Int) => String -> (a -> b) -> (Expr a -> Expr b)
pattern IntFun str f x = Fun str f x
-- Alternative syntax for pattern synonyms:
-- pattern
-- Suc :: () => (a ~ Int) => Expr a -> Expr Int
-- Suc n <- IntFun _ _ n where
-- Suc n = IntFun "suc" (+ 1) n
pattern Suc :: (a ~ Int) => Expr a -> Expr Int
pattern Suc n <- IntFun _ _ n where
Suc n = IntFun "suc" (+ 1) n
T11010.hs:8:1: error:
The 'required' context ‘a ~ Int’
mentions existential type variable ‘a’
T11010.hs:16:1: error:
The 'required' context ‘a ~ Int’
mentions existential type variable ‘a’
......@@ -8,3 +8,4 @@ test('T9705-1', normal, compile_fail, [''])
test('T9705-2', normal, compile_fail, [''])
test('unboxed-bind', normal, compile_fail, [''])
test('unboxed-wrapper-naked', normal, compile_fail, [''])
test('T11010', normal, compile_fail, [''])
\ No newline at end of file
Subproject commit 85b7ed6147c18611b5ef6b606f157086a8203e7d
Subproject commit 18de4f2f992d3ed41eb83cb073e63304f0271dca
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment