summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/basicTypes/PatSyn.hs45
-rw-r--r--compiler/hsSyn/HsBinds.hs16
-rw-r--r--compiler/iface/IfaceSyn.hs2
-rw-r--r--compiler/iface/MkIface.hs2
-rw-r--r--compiler/rename/RnBinds.hs8
-rw-r--r--compiler/typecheck/TcBinds.hs15
-rw-r--r--compiler/typecheck/TcPat.hs2
-rw-r--r--docs/users_guide/glasgow_exts.rst18
-rw-r--r--testsuite/tests/ghci/scripts/T8776.stdout3
-rw-r--r--testsuite/tests/patsyn/should_compile/T10997_1a.hs2
-rw-r--r--testsuite/tests/patsyn/should_compile/T10997a.hs2
-rw-r--r--testsuite/tests/patsyn/should_compile/T8584-2.hs2
-rw-r--r--testsuite/tests/patsyn/should_fail/T11010.hs18
-rw-r--r--testsuite/tests/patsyn/should_fail/T11010.stderr8
-rw-r--r--testsuite/tests/patsyn/should_fail/all.T1
m---------utils/haddock0
16 files changed, 111 insertions, 33 deletions
diff --git a/compiler/basicTypes/PatSyn.hs b/compiler/basicTypes/PatSyn.hs
index 503ebd87a4..2546ff4ea0 100644
--- a/compiler/basicTypes/PatSyn.hs
+++ b/compiler/basicTypes/PatSyn.hs
@@ -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
diff --git a/compiler/hsSyn/HsBinds.hs b/compiler/hsSyn/HsBinds.hs
index 4b661ff6cd..18756f632f 100644
--- a/compiler/hsSyn/HsBinds.hs
+++ b/compiler/hsSyn/HsBinds.hs
@@ -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]
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 85210cd6f3..42342aec85 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -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
diff --git a/compiler/iface/MkIface.hs b/compiler/iface/MkIface.hs
index d4b764b613..84d9fd99b5 100644
--- a/compiler/iface/MkIface.hs
+++ b/compiler/iface/MkIface.hs
@@ -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)
diff --git a/compiler/rename/RnBinds.hs b/compiler/rename/RnBinds.hs
index 10c5b7bb03..d63808edb6 100644
--- a/compiler/rename/RnBinds.hs
+++ b/compiler/rename/RnBinds.hs
@@ -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)
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index f927ffa2df..d939ad3ed3 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -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,
diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs
index 486e5f5d24..e39b0f51c6 100644
--- a/compiler/typecheck/TcPat.hs
+++ b/compiler/typecheck/TcPat.hs
@@ -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
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 5f7a4dc9b8..872eb64cd8 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -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
diff --git a/testsuite/tests/ghci/scripts/T8776.stdout b/testsuite/tests/ghci/scripts/T8776.stdout
index 7f8d57e7ee..937a270963 100644
--- a/testsuite/tests/ghci/scripts/T8776.stdout
+++ b/testsuite/tests/ghci/scripts/T8776.stdout
@@ -1 +1,2 @@
-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
diff --git a/testsuite/tests/patsyn/should_compile/T10997_1a.hs b/testsuite/tests/patsyn/should_compile/T10997_1a.hs
index af98f495f7..f6a292aa54 100644
--- a/testsuite/tests/patsyn/should_compile/T10997_1a.hs
+++ b/testsuite/tests/patsyn/should_compile/T10997_1a.hs
@@ -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
diff --git a/testsuite/tests/patsyn/should_compile/T10997a.hs b/testsuite/tests/patsyn/should_compile/T10997a.hs
index bed19f74e9..ec3c54238d 100644
--- a/testsuite/tests/patsyn/should_compile/T10997a.hs
+++ b/testsuite/tests/patsyn/should_compile/T10997a.hs
@@ -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
diff --git a/testsuite/tests/patsyn/should_compile/T8584-2.hs b/testsuite/tests/patsyn/should_compile/T8584-2.hs
index 24147a258d..379a8c872e 100644
--- a/testsuite/tests/patsyn/should_compile/T8584-2.hs
+++ b/testsuite/tests/patsyn/should_compile/T8584-2.hs
@@ -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
diff --git a/testsuite/tests/patsyn/should_fail/T11010.hs b/testsuite/tests/patsyn/should_fail/T11010.hs
new file mode 100644
index 0000000000..c0bdb6e0d4
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T11010.hs
@@ -0,0 +1,18 @@
+{-# 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
diff --git a/testsuite/tests/patsyn/should_fail/T11010.stderr b/testsuite/tests/patsyn/should_fail/T11010.stderr
new file mode 100644
index 0000000000..5f62b1357e
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T11010.stderr
@@ -0,0 +1,8 @@
+
+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’
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index de5d6db3b4..846d2d37d9 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -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
diff --git a/utils/haddock b/utils/haddock
-Subproject 85b7ed6147c18611b5ef6b606f157086a8203e7
+Subproject 18de4f2f992d3ed41eb83cb073e63304f0271dc