diff options
| -rw-r--r-- | compiler/typecheck/TcExpr.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcPatSyn.hs | 177 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 16 | ||||
| -rw-r--r-- | compiler/typecheck/TcType.hs | 32 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/T11977.hs | 8 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/T12108.hs | 8 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/all.T | 2 |
7 files changed, 145 insertions, 100 deletions
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index 834287a0d0..d4a9f38179 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -621,7 +621,7 @@ tcExpr expr@(RecordCon { rcon_con_name = L loc con_name -- a shallow instantiation should really be enough for -- a data constructor. ; let arity = conLikeArity con_like - (arg_tys, actual_res_ty) = tcSplitFunTysN con_tau arity + Right (arg_tys, actual_res_ty) = tcSplitFunTysN arity con_tau ; case conLikeWrapId_maybe con_like of Nothing -> nonBidirectionalErr (conLikeName con_like) Just con_id -> do { diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 260a3f23d3..6418a2184a 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -49,7 +49,7 @@ import Bag import Util import ErrUtils import FV -import Control.Monad ( unless, zipWithM ) +import Control.Monad ( zipWithM ) import Data.List( partition ) #include "HsVersions.h" @@ -65,16 +65,16 @@ Note [Pattern synonym signatures] Pattern synonym signatures are surprisingly tricky (see Trac #11224 for example). In general they look like this: - pattern P :: forall univ_tvs. req - => forall ex_tvs. prov - => arg1 -> .. -> argn -> body_ty + pattern P :: forall univ_tvs. req_theta + => forall ex_tvs. prov_theta + => arg1 -> .. -> argn -> res_ty For parsing and renaming we treat the signature as an ordinary LHsSigType. Once we get to type checking, we decompose it into its parts, in tcPatSynSig. -* Note that 'forall univ_tvs' and 'req =>' - and 'forall ex_tvs' and 'prov =>' +* Note that 'forall univ_tvs' and 'req_theta =>' + and 'forall ex_tvs' and 'prov_theta =>' are all optional. We gather the pieces at the the top of tcPatSynSig * Initially the implicitly-bound tyvars (added by the renamer) include both @@ -82,46 +82,71 @@ Once we get to type checking, we decompose it into its parts, in tcPatSynSig. * After we kind-check the pieces and convert to Types, we do kind generalisation. -* Note [Splitting the implicit tyvars in a pattern synonym] - Now the tricky bit: we must split - the implicitly-bound variables, and - the kind-generalised variables - into universal and existential. We do so as follows: +Note [The pattern-synonym signature splitting rule] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Given a pattern signature, we must split + the kind-generalised variables, and + the implicitly-bound variables +into universal and existential. The rule is this +(see discussion on Trac #11224): - Note [The pattern-synonym signature splitting rule] - the universals are the ones mentioned in - - univ_tvs (and the kinds thereof) - - req - - body_ty - the existentials are the rest + The universal tyvars are the ones mentioned in + - univ_tvs: the user-specified (forall'd) universals + - req_theta + - res_ty + The existential tyvars are all the rest -* Moreover see Note +For example + + pattern P :: () => b -> T a + pattern P x = ... + +Here 'a' is universal, and 'b' is existential. But there is a wrinkle: +how do we split the arg_tys from req_ty? Consider + + pattern Q :: () => b -> S c -> T a + pattern Q x = ... + +This is an odd example because Q has only one syntactic argument, and +so presumably is defined by a view pattern matching a function. But +it can happen (Trac #11977, #12108). + +We don't know Q's arity from the pattern signature, so we have to wait +until we see the pattern declaration itself before deciding res_ty is, +and hence which variables are existential and which are universal. + +And that in turn is why TcPatSynInfo has a separate field, +patsig_implicit_bndrs, to capture the implicitly bound type variables, +because we don't yet know how to split them up. + +It's a slight compromise, because it means we don't really know the +pattern synonym's real signature until we see its declaration. So, +for example, in hs-boot file, we may need to think what to do... +(eg don't have any implicitly-bound variables). -} tcPatSynSig :: Name -> LHsSigType Name -> TcM TcPatSynInfo tcPatSynSig name sig_ty | HsIB { hsib_vars = implicit_hs_tvs , hsib_body = hs_ty } <- sig_ty - , (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTy hs_ty - , (ex_hs_tvs, hs_prov, hs_ty2) <- splitLHsSigmaTy hs_ty1 - , (hs_arg_tys, hs_body_ty) <- splitHsFunType hs_ty2 - = do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty)) + , (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTy hs_ty + , (ex_hs_tvs, hs_prov, hs_body_ty) <- splitLHsSigmaTy hs_ty1 + = do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, body_ty)) <- solveEqualities $ tcImplicitTKBndrs implicit_hs_tvs $ tcExplicitTKBndrs univ_hs_tvs $ \ univ_tvs -> tcExplicitTKBndrs ex_hs_tvs $ \ ex_tvs -> do { req <- tcHsContext hs_req ; prov <- tcHsContext hs_prov - ; arg_tys <- mapM tcHsOpenType (hs_arg_tys :: [LHsType Name]) - -- A (literal) pattern can be unlifted; - -- -- e.g. pattern Zero <- 0# (Trac #12094) ; body_ty <- tcHsOpenType hs_body_ty + -- A (literal) pattern can be unlifted; + -- e.g. pattern Zero <- 0# (Trac #12094) ; let bound_tvs = unionVarSets [ allBoundVariabless req , allBoundVariabless prov - , allBoundVariabless (body_ty : arg_tys) + , allBoundVariables body_ty ] - ; return ( (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty) + ; return ( (univ_tvs, req, ex_tvs, prov, body_ty) , bound_tvs) } -- Kind generalisation @@ -130,7 +155,6 @@ tcPatSynSig name sig_ty mkFunTys req $ mkSpecForAllTys ex_tvs $ mkFunTys prov $ - mkFunTys arg_tys $ body_ty -- These are /signatures/ so we zonk to squeeze out any kind @@ -143,45 +167,24 @@ tcPatSynSig name sig_ty ; ex_tvs <- mapM zonkTcTyCoVarBndr ex_tvs ; req <- zonkTcTypes req ; prov <- zonkTcTypes prov - ; arg_tys <- zonkTcTypes arg_tys ; body_ty <- zonkTcType body_ty - -- Complain about: pattern P :: () => forall x. x -> P x - -- The renamer thought it was fine, but the existential 'x' - -- should not appear in the result type - ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType body_ty) ex_tvs - ; unless (null bad_tvs) $ addErr $ - hang (text "The result type" <+> quotes (ppr body_ty)) - 2 (text "mentions existential type variable" <> plural bad_tvs - <+> pprQuotedList bad_tvs) - - -- Split [Splitting the implicit tyvars in a pattern synonym] - ; let univ_fvs = closeOverKinds $ - (tyCoVarsOfTypes (body_ty : req) `extendVarSetList` univ_tvs) - (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . - binderVar "tcPatSynSig") $ - mkNamedBinders Invisible kvs ++ - mkNamedBinders Specified implicit_tvs ; traceTc "tcTySig }" $ vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs , text "kvs" <+> ppr_tvs kvs - , text "extra_univ" <+> ppr extra_univ , text "univ_tvs" <+> ppr_tvs univ_tvs , text "req" <+> ppr req - , text "extra_ex" <+> ppr extra_ex , text "ex_tvs" <+> ppr_tvs ex_tvs , text "prov" <+> ppr prov - , text "arg_tys" <+> ppr arg_tys , text "body_ty" <+> ppr body_ty ] ; return (TPSI { patsig_name = name - , patsig_univ_bndrs = extra_univ ++ - mkNamedBinders Specified univ_tvs - , patsig_req = req - , patsig_ex_bndrs = extra_ex ++ - mkNamedBinders Specified ex_tvs - , patsig_prov = prov - , patsig_arg_tys = arg_tys - , patsig_body_ty = body_ty }) } + , patsig_implicit_bndrs = mkNamedBinders Invisible kvs ++ + mkNamedBinders Specified implicit_tvs + , patsig_univ_bndrs = univ_tvs + , patsig_req = req + , patsig_ex_bndrs = ex_tvs + , patsig_prov = prov + , patsig_body_ty = body_ty }) } where ppr_tvs :: [TyVar] -> SDoc @@ -238,26 +241,44 @@ tcCheckPatSynDecl :: PatSynBind Name Name -> TcM (LHsBinds Id, TcGblEnv) tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details , psb_def = lpat, psb_dir = dir } - TPSI{ patsig_univ_bndrs = univ_bndrs, patsig_prov = prov_theta - , patsig_ex_bndrs = ex_bndrs, patsig_req = req_theta - , patsig_arg_tys = arg_tys, patsig_body_ty = pat_ty } + TPSI{ patsig_implicit_bndrs = implicit_tvs + , patsig_univ_bndrs = explicit_univ_tvs, patsig_prov = prov_theta + , patsig_ex_bndrs = explicit_ex_tvs, patsig_req = req_theta + , patsig_body_ty = sig_body_ty } = addPatSynCtxt lname $ do { let decl_arity = length arg_names - ty_arity = length arg_tys (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details - univ_tvs = map (binderVar "tcCheckPatSynDecl 1") univ_bndrs - ex_tvs = map (binderVar "tcCheckPatSynDecl 2") ex_bndrs - ; traceTc "tcCheckPatSynDecl" $ - vcat [ ppr univ_bndrs, ppr req_theta, ppr ex_bndrs - , ppr prov_theta, ppr arg_tys, ppr pat_ty ] - - ; checkTc (decl_arity == ty_arity) - (wrongNumberOfParmsErr name decl_arity ty_arity) + vcat [ ppr implicit_tvs, ppr explicit_univ_tvs, ppr req_theta + , ppr explicit_ex_tvs, ppr prov_theta, ppr sig_body_ty ] ; tcCheckPatSynPat lpat + ; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of + Right stuff -> return stuff + Left missing -> wrongNumberOfParmsErr name decl_arity missing + + -- Complain about: pattern P :: () => forall x. x -> P x + -- The existential 'x' should not appear in the result type + -- Can't check this until we know P's arity + ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) explicit_ex_tvs + ; checkTc (null bad_tvs) $ + hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma + , text "namely" <+> quotes (ppr pat_ty) ]) + 2 (text "mentions existential type variable" <> plural bad_tvs + <+> pprQuotedList bad_tvs) + + -- See Note [The pattern-synonym signature splitting rule] + ; let get_tv = binderVar "tcCheckPatSynDecl" + univ_fvs = closeOverKinds $ + (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` explicit_univ_tvs) + (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . get_tv) implicit_tvs + univ_bndrs = extra_univ ++ mkNamedBinders Specified explicit_univ_tvs + ex_bndrs = extra_ex ++ mkNamedBinders Specified explicit_ex_tvs + univ_tvs = map get_tv univ_bndrs + ex_tvs = map get_tv ex_bndrs + -- Right! Let's check the pattern against the signature -- See Note [Checking against a pattern signature] ; req_dicts <- newEvVars req_theta @@ -386,11 +407,12 @@ addPatSynCtxt (L loc name) thing_inside <+> quotes (ppr name)) $ thing_inside -wrongNumberOfParmsErr :: Name -> Arity -> Arity -> SDoc -wrongNumberOfParmsErr name decl_arity ty_arity - = hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has") +wrongNumberOfParmsErr :: Name -> Arity -> Arity -> TcM a +wrongNumberOfParmsErr name decl_arity missing + = failWithTc $ + hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has") <+> speakNOf decl_arity (text "argument")) - 2 (text "but its type signature has" <+> speakN ty_arity) + 2 (text "but its type signature has" <+> int missing <+> text "fewer arrows") ------------------------- -- Shared by both tcInferPatSyn and tcCheckPatSyn @@ -700,11 +722,11 @@ tcPatSynBuilderBind sig_fun PSB{ psb_id = L loc name, psb_def = lpat get_builder_sig :: TcSigFun -> Name -> Id -> Bool -> TcM TcIdSigInfo get_builder_sig sig_fun name builder_id need_dummy_arg | Just (TcPatSynSig sig) <- sig_fun name - , TPSI { patsig_univ_bndrs = univ_bndrs + , TPSI { patsig_implicit_bndrs = implicit_bndrs + , patsig_univ_bndrs = univ_bndrs , patsig_req = req , patsig_ex_bndrs = ex_bndrs , patsig_prov = prov - , patsig_arg_tys = arg_tys , patsig_body_ty = body_ty } <- sig = -- Constuct a TcIdSigInfo from a TcPatSynInfo -- This does unfortunately mean that we have to know how to @@ -714,11 +736,10 @@ get_builder_sig sig_fun name builder_id need_dummy_arg -- the actual sigature, so this is really the Right Thing return (TISI { sig_bndr = CompleteSig builder_id , sig_skols = [ (tyVarName tv, tv) - | bndr <- univ_bndrs ++ ex_bndrs - , let tv = binderVar "get_builder_sig" bndr ] + | tv <- map (binderVar "get_builder_sig") implicit_bndrs + ++ univ_bndrs ++ ex_bndrs ] , sig_theta = req ++ prov - , sig_tau = add_void need_dummy_arg $ - mkFunTys arg_tys body_ty + , sig_tau = add_void need_dummy_arg body_ty , sig_ctxt = PatSynCtxt name , sig_loc = getSrcSpan name }) | otherwise diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index dede93233e..da9878f09c 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -1211,13 +1211,15 @@ data TcIdSigBndr -- See Note [Complete and partial type signatures] data TcPatSynInfo = TPSI { - patsig_name :: Name, - patsig_univ_bndrs :: [TcTyBinder], - patsig_req :: TcThetaType, - patsig_ex_bndrs :: [TcTyBinder], - patsig_prov :: TcThetaType, - patsig_arg_tys :: [TcSigmaType], - patsig_body_ty :: TcSigmaType + patsig_name :: Name, + patsig_implicit_bndrs :: [TyBinder], -- Implicitly-bound kind vars (Invisible) and + -- implicitly-bound type vars (Specified) + -- See Note [The pattern-synonym signature splitting rule] in TcPatSyn + patsig_univ_bndrs :: [TyVar], -- Bound by explicit user forall + patsig_req :: TcThetaType, + patsig_ex_bndrs :: [TyVar], -- Bound by explicit user forall + patsig_prov :: TcThetaType, + patsig_body_ty :: TcSigmaType } findScopedTyVars -- See Note [Binding scoped type variables] diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index fbb80bda47..ea4224d7d6 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -1329,20 +1329,24 @@ tcSplitFunTy_maybe _ = Nothing -- -- g = f () () -tcSplitFunTysN - :: TcRhoType - -> Arity -- N: Number of desired args - -> ([TcSigmaType], -- Arg types (N or fewer) - TcSigmaType) -- The rest of the type - -tcSplitFunTysN ty n_args - | n_args == 0 - = ([], ty) - | Just (arg,res) <- tcSplitFunTy_maybe ty - = case tcSplitFunTysN res (n_args - 1) of - (args, res) -> (arg:args, res) - | otherwise - = ([], ty) +tcSplitFunTysN :: Arity -- N: Number of desired args + -> TcRhoType + -> Either Arity -- Number of missing arrows + ([TcSigmaType], -- Arg types (N or fewer) + TcSigmaType) -- The rest of the type +-- ^ Split off exactly the specified number argument types +-- Returns +-- (Left m) if there are 'm' missing arrows in the type +-- (Right (tys,res)) if the type looks like t1 -> ... -> tn -> res +tcSplitFunTysN n ty + | n == 0 + = Right ([], ty) + | Just (arg,res) <- tcSplitFunTy_maybe ty + = case tcSplitFunTysN (n-1) res of + Left m -> Left m + Right (args,body) -> Right (arg:args, body) + | otherwise + = Left n tcSplitFunTy :: Type -> (Type, Type) tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty) diff --git a/testsuite/tests/patsyn/should_compile/T11977.hs b/testsuite/tests/patsyn/should_compile/T11977.hs new file mode 100644 index 0000000000..bc5f3e4a1c --- /dev/null +++ b/testsuite/tests/patsyn/should_compile/T11977.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE ViewPatterns, PatternSynonyms #-} + +module T11977 where + +-- A pattern synonym for a /function/ + +pattern F :: b -> Char -> b +pattern F a <- (($ 'a') -> a) diff --git a/testsuite/tests/patsyn/should_compile/T12108.hs b/testsuite/tests/patsyn/should_compile/T12108.hs new file mode 100644 index 0000000000..26ee75dfc6 --- /dev/null +++ b/testsuite/tests/patsyn/should_compile/T12108.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE PatternSynonyms #-} + +module T12108 where + +type Endo a = a -> a + +pattern Id :: Endo a +pattern Id x = x diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T index 035cd00401..ff2f14afa1 100644 --- a/testsuite/tests/patsyn/should_compile/all.T +++ b/testsuite/tests/patsyn/should_compile/all.T @@ -54,3 +54,5 @@ test('T11351', normal, compile, ['']) test('T11633', normal, compile, ['']) test('T11959', expect_broken(11959), multimod_compile, ['T11959', '-v0']) test('T12094', normal, compile, ['']) +test('T11977', normal, compile, ['']) +test('T12108', normal, compile, [''])
\ No newline at end of file |