From 72938f5890dac81afad52bf58175c1e29ffbc6dd Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Wed, 20 Dec 2017 15:41:02 +0000 Subject: Check for bogus quantified tyvars in partial type sigs This fixes Trac #14479. Not difficult. See Note [Quantification and partial signatures] Wrinkle 4, in TcSimplify. --- compiler/typecheck/TcBinds.hs | 54 ++++++++++------- compiler/typecheck/TcSimplify.hs | 69 ++++++++++++++-------- testsuite/tests/partial-sigs/should_fail/T14479.hs | 9 +++ .../tests/partial-sigs/should_fail/T14479.stderr | 10 ++++ testsuite/tests/partial-sigs/should_fail/all.T | 1 + 5 files changed, 96 insertions(+), 47 deletions(-) create mode 100644 testsuite/tests/partial-sigs/should_fail/T14479.hs create mode 100644 testsuite/tests/partial-sigs/should_fail/T14479.stderr diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs index 6189ba51d2..0c5179c473 100644 --- a/compiler/typecheck/TcBinds.hs +++ b/compiler/typecheck/TcBinds.hs @@ -939,32 +939,35 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs , sig_inst_theta = annotated_theta , sig_inst_skols = annotated_tvs })) = -- Choose quantifiers for a partial type signature - do { psig_qtvs <- mk_psig_qtvs annotated_tvs - ; annotated_theta <- zonkTcTypes annotated_theta - ; (free_tvs, my_theta) <- choose_psig_context psig_qtvs annotated_theta wcx - ; return (mk_final_qtvs psig_qtvs free_tvs, my_theta) } - where - mk_final_qtvs psig_qtvs free_tvs - = [ mkTyVarBinder vis tv - | tv <- qtvs -- Pulling from qtvs maintains original order - , tv `elemVarSet` keep_me - , let vis | tv `elemVarSet` psig_qtvs = Specified - | otherwise = Inferred ] - where - keep_me = free_tvs `unionVarSet` psig_qtvs - - mk_psig_qtvs :: [(Name,TcTyVar)] -> TcM TcTyVarSet - mk_psig_qtvs annotated_tvs - = do { annotated_tvs <- zonkSigTyVarPairs annotated_tvs + do { psig_qtv_prs <- zonkSigTyVarPairs annotated_tvs - -- Report an error if the quantified variables of the + -- Check whether the quantified variables of the -- partial signature have been unified together -- See Note [Quantified variables in partial type signatures] - ; mapM_ report_sig_tv_err (findDupSigTvs annotated_tvs) + ; mapM_ report_dup_sig_tv_err (findDupSigTvs psig_qtv_prs) - ; return (mkVarSet (map snd annotated_tvs)) } + -- Check whether a quantified variable of the partial type + -- signature is not actually quantified. How can that happen? + -- See Note [Quantification and partial signatures] Wrinkle 4 + -- in TcSimplify + ; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs + , not (tv `elem` qtvs) ] + + ; let psig_qtvs = mkVarSet (map snd psig_qtv_prs) + + ; annotated_theta <- zonkTcTypes annotated_theta + ; (free_tvs, my_theta) <- choose_psig_context psig_qtvs annotated_theta wcx - report_sig_tv_err (n1,n2) + ; let keep_me = free_tvs `unionVarSet` psig_qtvs + final_qtvs = [ mkTyVarBinder vis tv + | tv <- qtvs -- Pulling from qtvs maintains original order + , tv `elemVarSet` keep_me + , let vis | tv `elemVarSet` psig_qtvs = Specified + | otherwise = Inferred ] + + ; return (final_qtvs, my_theta) } + where + report_dup_sig_tv_err (n1,n2) | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig = addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1) <+> text "with" <+> quotes (ppr n2)) @@ -974,6 +977,14 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs | otherwise -- Can't happen; by now we know it's a partial sig = pprPanic "report_sig_tv_err" (ppr sig) + report_mono_sig_tv_err n + | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig + = addErrTc (hang (text "Can't quantify over" <+> quotes (ppr n)) + 2 (hang (text "bound by the partial type signature:") + 2 (ppr fn_name <+> dcolon <+> ppr hs_ty))) + | otherwise -- Can't happen; by now we know it's a partial sig + = pprPanic "report_sig_tv_err" (ppr sig) + choose_psig_context :: VarSet -> TcThetaType -> Maybe TcTyVar -> TcM (VarSet, TcThetaType) choose_psig_context _ annotated_theta Nothing @@ -1129,6 +1140,7 @@ So we make a test, one per parital signature, to check that the explicitly-quantified type variables have not been unified together. Trac #14449 showed this up. + Note [Validity of inferred types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We need to check inferred type for validity, in case it uses language diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 16bf345e4e..6ebf27d3e8 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -855,24 +855,36 @@ decideMonoTyVars :: InferMode -- (c) Connected by an equality to (a) or (b) -- Also return the reduced set of constraint we can generalise decideMonoTyVars infer_mode name_taus psigs candidates - = do { (no_quant, yes_quant) <- pick infer_mode candidates + = do { (no_quant, maybe_quant) <- pick infer_mode candidates + + -- If possible, we quantify over partial-sig qtvs, so they are + -- not mono. Need to zonk them because they are meta-tyvar SigTvs + ; psig_qtvs <- mapM zonkTcTyVarToTyVar $ + concatMap (map snd . sig_inst_skols) psigs ; gbl_tvs <- tcGetGlobalTyCoVars ; let eq_constraints = filter isEqPred candidates mono_tvs1 = growThetaTyVars eq_constraints gbl_tvs - constrained_tvs = growThetaTyVars eq_constraints + + constrained_tvs = (growThetaTyVars eq_constraints (tyCoVarsOfTypes no_quant) - `minusVarSet` mono_tvs1 - mono_tvs2 = mono_tvs1 `unionVarSet` constrained_tvs - -- A type variable is only "constrained" (so that the MR bites) - -- if it is not free in the environment (Trac #13785) - - -- Always quantify over partial-sig qtvs, so they are not mono - -- Need to zonk them because they are meta-tyvar SigTvs - -- Note [Quantification and partial signatures], wrinkle 3 - ; psig_qtvs <- mapM zonkTcTyVarToTyVar $ - concatMap (map snd . sig_inst_skols) psigs - ; let mono_tvs = mono_tvs2 `delVarSetList` psig_qtvs + `minusVarSet` mono_tvs1) + `delVarSetList` psig_qtvs + -- constrained_tvs: the tyvars that we are not going to + -- quantify solely because of the moonomorphism restriction + -- + -- (`minusVarSet` mono_tvs`): a type variable is only + -- "constrained" (so that the MR bites) if it is not + -- free in the environment (Trac #13785) + -- + -- (`delVarSetList` psig_qtvs): if the user has explicitly + -- asked for quantification, then that request "wins" + -- over the MR. Note: do /not/ delete psig_qtvs from + -- mono_tvs1, because mono_tvs1 cannot under any circumstances + -- be quantified (Trac #14479); see + -- Note [Quantification and partial signatures], Wrinkle 3, 4 + + mono_tvs = mono_tvs1 `unionVarSet` constrained_tvs -- Warn about the monomorphism restriction ; warn_mono <- woptM Opt_WarnMonomorphism @@ -885,11 +897,11 @@ decideMonoTyVars infer_mode name_taus psigs candidates ; traceTc "decideMonoTyVars" $ vcat [ text "gbl_tvs =" <+> ppr gbl_tvs , text "no_quant =" <+> ppr no_quant - , text "yes_quant =" <+> ppr yes_quant + , text "maybe_quant =" <+> ppr maybe_quant , text "eq_constraints =" <+> ppr eq_constraints , text "mono_tvs =" <+> ppr mono_tvs ] - ; return (mono_tvs, yes_quant) } + ; return (mono_tvs, maybe_quant) } where pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType]) -- Split the candidates into ones we definitely @@ -980,7 +992,7 @@ decideQuantifiedTyVars decideQuantifiedTyVars mono_tvs name_taus psigs candidates = do { -- Why psig_tys? We try to quantify over everything free in here -- See Note [Quantification and partial signatures] - -- wrinkles 2 and 3 + -- Wrinkles 2 and 3 ; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs , (_,tv) <- sig_inst_skols sig ] ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs @@ -1093,17 +1105,22 @@ sure to quantify over them. This leads to several wrinkles: * Wrinkle 3 (Trac #13482). Also consider f :: forall a. _ => Int -> Int - f x = if undefined :: a == undefined then x else 0 + f x = if (undefined :: a) == undefined then x else 0 Here we get an (Eq a) constraint, but it's not mentioned in the - psig_theta nor the type of 'f'. Moreover, if we have - f :: forall a. a -> _ - f x = not x - and a constraint (a ~ g), where 'g' is free in the environment, - we would not usually quanitfy over 'a'. But here we should anyway - (leading to a justified subsequent error) since 'a' is explicitly - quantified by the programmer. - - Bottom line: always quantify over the psig_tvs, regardless. + psig_theta nor the type of 'f'. But we still want to quantify + over 'a' even if the monomorphism restriction is on. + +* Wrinkle 4 (Trac #14479) + foo :: Num a => a -> a + foo xxx = g xxx + where + g :: forall b. Num b => _ -> b + g y = xxx + y + + In the signature for 'g', we cannot quantify over 'b' because it turns out to + get unified with 'a', which is free in g's environment. So we carefully + refrain from bogusly quantifying, in TcSimplify.decideMonoTyVars. We + report the error later, in TcBinds.chooseInferredQuantifiers. Note [Quantifying over equality constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/testsuite/tests/partial-sigs/should_fail/T14479.hs b/testsuite/tests/partial-sigs/should_fail/T14479.hs new file mode 100644 index 0000000000..13ee256e83 --- /dev/null +++ b/testsuite/tests/partial-sigs/should_fail/T14479.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE ScopedTypeVariables, PartialTypeSignatures #-} + +module T14479 where + +foo :: Num a => a -> a +foo xxx = g xxx + where + g :: forall b. Num b => _ -> b + g y = xxx + y diff --git a/testsuite/tests/partial-sigs/should_fail/T14479.stderr b/testsuite/tests/partial-sigs/should_fail/T14479.stderr new file mode 100644 index 0000000000..84ba90a572 --- /dev/null +++ b/testsuite/tests/partial-sigs/should_fail/T14479.stderr @@ -0,0 +1,10 @@ + +T14479.hs:9:5: error: + • Can't quantify over ‘b’ + bound by the partial type signature: g :: forall b. Num b => _ -> b + • In an equation for ‘foo’: + foo xxx + = g xxx + where + g :: forall b. Num b => _ -> b + g y = xxx + y diff --git a/testsuite/tests/partial-sigs/should_fail/all.T b/testsuite/tests/partial-sigs/should_fail/all.T index bb813f0b08..91509c4f36 100644 --- a/testsuite/tests/partial-sigs/should_fail/all.T +++ b/testsuite/tests/partial-sigs/should_fail/all.T @@ -66,3 +66,4 @@ test('T12634', normal, compile_fail, ['']) test('T12732', normal, compile_fail, ['-fobject-code -fdefer-typed-holes']) test('T14040a', normal, compile_fail, ['']) test('T14449', normal, compile_fail, ['']) +test('T14479', normal, compile_fail, ['']) -- cgit v1.2.1