diff options
-rw-r--r-- | compiler/basicTypes/PatSyn.hs | 45 | ||||
-rw-r--r-- | compiler/hsSyn/HsBinds.hs | 16 | ||||
-rw-r--r-- | compiler/iface/IfaceSyn.hs | 2 | ||||
-rw-r--r-- | compiler/iface/MkIface.hs | 2 | ||||
-rw-r--r-- | compiler/rename/RnBinds.hs | 8 | ||||
-rw-r--r-- | compiler/typecheck/TcBinds.hs | 15 | ||||
-rw-r--r-- | compiler/typecheck/TcPat.hs | 2 | ||||
-rw-r--r-- | docs/users_guide/glasgow_exts.rst | 18 | ||||
-rw-r--r-- | testsuite/tests/ghci/scripts/T8776.stdout | 3 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_compile/T10997_1a.hs | 2 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_compile/T10997a.hs | 2 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_compile/T8584-2.hs | 2 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/T11010.hs | 18 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/T11010.stderr | 8 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/all.T | 1 | ||||
m--------- | utils/haddock | 0 |
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 |