Commit 72938f58 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

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.
parent 584cbd4a
...@@ -939,32 +939,35 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs ...@@ -939,32 +939,35 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
, sig_inst_theta = annotated_theta , sig_inst_theta = annotated_theta
, sig_inst_skols = annotated_tvs })) , sig_inst_skols = annotated_tvs }))
= -- Choose quantifiers for a partial type signature = -- Choose quantifiers for a partial type signature
do { psig_qtvs <- mk_psig_qtvs annotated_tvs do { psig_qtv_prs <- zonkSigTyVarPairs 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
-- Report an error if the quantified variables of the -- Check whether the quantified variables of the
-- partial signature have been unified together -- partial signature have been unified together
-- See Note [Quantified variables in partial type signatures] -- 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 | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
= addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1) = addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1)
<+> text "with" <+> quotes (ppr n2)) <+> text "with" <+> quotes (ppr n2))
...@@ -974,6 +977,14 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs ...@@ -974,6 +977,14 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
| otherwise -- Can't happen; by now we know it's a partial sig | otherwise -- Can't happen; by now we know it's a partial sig
= pprPanic "report_sig_tv_err" (ppr 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 choose_psig_context :: VarSet -> TcThetaType -> Maybe TcTyVar
-> TcM (VarSet, TcThetaType) -> TcM (VarSet, TcThetaType)
choose_psig_context _ annotated_theta Nothing choose_psig_context _ annotated_theta Nothing
...@@ -1129,6 +1140,7 @@ So we make a test, one per parital signature, to check that the ...@@ -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. explicitly-quantified type variables have not been unified together.
Trac #14449 showed this up. Trac #14449 showed this up.
Note [Validity of inferred types] Note [Validity of inferred types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to check inferred type for validity, in case it uses language We need to check inferred type for validity, in case it uses language
......
...@@ -855,24 +855,36 @@ decideMonoTyVars :: InferMode ...@@ -855,24 +855,36 @@ decideMonoTyVars :: InferMode
-- (c) Connected by an equality to (a) or (b) -- (c) Connected by an equality to (a) or (b)
-- Also return the reduced set of constraint we can generalise -- Also return the reduced set of constraint we can generalise
decideMonoTyVars infer_mode name_taus psigs candidates 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 ; gbl_tvs <- tcGetGlobalTyCoVars
; let eq_constraints = filter isEqPred candidates ; let eq_constraints = filter isEqPred candidates
mono_tvs1 = growThetaTyVars eq_constraints gbl_tvs mono_tvs1 = growThetaTyVars eq_constraints gbl_tvs
constrained_tvs = growThetaTyVars eq_constraints
constrained_tvs = (growThetaTyVars eq_constraints
(tyCoVarsOfTypes no_quant) (tyCoVarsOfTypes no_quant)
`minusVarSet` mono_tvs1 `minusVarSet` mono_tvs1)
mono_tvs2 = mono_tvs1 `unionVarSet` constrained_tvs `delVarSetList` psig_qtvs
-- A type variable is only "constrained" (so that the MR bites) -- constrained_tvs: the tyvars that we are not going to
-- if it is not free in the environment (Trac #13785) -- quantify solely because of the moonomorphism restriction
--
-- Always quantify over partial-sig qtvs, so they are not mono -- (`minusVarSet` mono_tvs`): a type variable is only
-- Need to zonk them because they are meta-tyvar SigTvs -- "constrained" (so that the MR bites) if it is not
-- Note [Quantification and partial signatures], wrinkle 3 -- free in the environment (Trac #13785)
; psig_qtvs <- mapM zonkTcTyVarToTyVar $ --
concatMap (map snd . sig_inst_skols) psigs -- (`delVarSetList` psig_qtvs): if the user has explicitly
; let mono_tvs = mono_tvs2 `delVarSetList` psig_qtvs -- 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 about the monomorphism restriction
; warn_mono <- woptM Opt_WarnMonomorphism ; warn_mono <- woptM Opt_WarnMonomorphism
...@@ -885,11 +897,11 @@ decideMonoTyVars infer_mode name_taus psigs candidates ...@@ -885,11 +897,11 @@ decideMonoTyVars infer_mode name_taus psigs candidates
; traceTc "decideMonoTyVars" $ vcat ; traceTc "decideMonoTyVars" $ vcat
[ text "gbl_tvs =" <+> ppr gbl_tvs [ text "gbl_tvs =" <+> ppr gbl_tvs
, text "no_quant =" <+> ppr no_quant , 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 "eq_constraints =" <+> ppr eq_constraints
, text "mono_tvs =" <+> ppr mono_tvs ] , text "mono_tvs =" <+> ppr mono_tvs ]
; return (mono_tvs, yes_quant) } ; return (mono_tvs, maybe_quant) }
where where
pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType]) pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
-- Split the candidates into ones we definitely -- Split the candidates into ones we definitely
...@@ -980,7 +992,7 @@ decideQuantifiedTyVars ...@@ -980,7 +992,7 @@ decideQuantifiedTyVars
decideQuantifiedTyVars mono_tvs name_taus psigs candidates decideQuantifiedTyVars mono_tvs name_taus psigs candidates
= do { -- Why psig_tys? We try to quantify over everything free in here = do { -- Why psig_tys? We try to quantify over everything free in here
-- See Note [Quantification and partial signatures] -- See Note [Quantification and partial signatures]
-- wrinkles 2 and 3 -- Wrinkles 2 and 3
; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs ; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs
, (_,tv) <- sig_inst_skols sig ] , (_,tv) <- sig_inst_skols sig ]
; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
...@@ -1093,17 +1105,22 @@ sure to quantify over them. This leads to several wrinkles: ...@@ -1093,17 +1105,22 @@ sure to quantify over them. This leads to several wrinkles:
* Wrinkle 3 (Trac #13482). Also consider * Wrinkle 3 (Trac #13482). Also consider
f :: forall a. _ => Int -> Int 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 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 psig_theta nor the type of 'f'. But we still want to quantify
f :: forall a. a -> _ over 'a' even if the monomorphism restriction is on.
f x = not x
and a constraint (a ~ g), where 'g' is free in the environment, * Wrinkle 4 (Trac #14479)
we would not usually quanitfy over 'a'. But here we should anyway foo :: Num a => a -> a
(leading to a justified subsequent error) since 'a' is explicitly foo xxx = g xxx
quantified by the programmer. where
g :: forall b. Num b => _ -> b
Bottom line: always quantify over the psig_tvs, regardless. 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] Note [Quantifying over equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
{-# 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
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
...@@ -66,3 +66,4 @@ test('T12634', normal, compile_fail, ['']) ...@@ -66,3 +66,4 @@ test('T12634', normal, compile_fail, [''])
test('T12732', normal, compile_fail, ['-fobject-code -fdefer-typed-holes']) test('T12732', normal, compile_fail, ['-fobject-code -fdefer-typed-holes'])
test('T14040a', normal, compile_fail, ['']) test('T14040a', normal, compile_fail, [''])
test('T14449', normal, compile_fail, ['']) test('T14449', normal, compile_fail, [''])
test('T14479', normal, compile_fail, [''])
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