Commit 28096b27 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix quantification for inference with sigs

When we are *inferring* the type of a let-bound function,
we might still have a type signature.  And we must be sure
to quantify over its type variables, else you get the crash
in Trac #10615.

See Note [Which type variables to quantify] in TcSimplify
parent 95364812
......@@ -650,9 +650,11 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
; let name_taus = [(name, idType mono_id) | (name, _, mono_id) <- mono_infos]
sig_qtvs = [ tv | (_, Just sig, _) <- mono_infos
, (_, tv) <- sig_tvs sig ]
; traceTc "simplifyInfer call" (ppr name_taus $$ ppr wanted)
; (qtvs, givens, _mr_bites, ev_binds)
<- simplifyInfer tclvl mono name_taus wanted
<- simplifyInfer tclvl mono sig_qtvs name_taus wanted
; let inferred_theta = map evVarPred givens
; exports <- checkNoErrs $
......
......@@ -1798,6 +1798,7 @@ tcRnExpr hsc_env rdr_expr
{-# SCC "simplifyInfer" #-}
simplifyInfer tclvl
False {- No MR for now -}
[] {- No sig vars -}
[(fresh_it, res_ty)]
lie ;
-- Wanted constraints from static forms
......
......@@ -384,8 +384,10 @@ has a strictly-increased level compared to the ambient level outside
the let binding.
-}
simplifyInfer :: TcLevel -- Used when generating the constraints
simplifyInfer :: TcLevel -- Used when generating the constraints
-> Bool -- Apply monomorphism restriction
-> [TcTyVar] -- The quantified tyvars of any signatures
-- see Note [Which type variables to quantify]
-> [(Name, TcTauType)] -- Variables to be generalised,
-- and their tau-types
-> WantedConstraints
......@@ -395,7 +397,7 @@ simplifyInfer :: TcLevel -- Used when generating the constraints
-- so the results type is not as general as
-- it could be
TcEvBinds) -- ... binding these evidence variables
simplifyInfer rhs_tclvl apply_mr name_taus wanteds
simplifyInfer rhs_tclvl apply_mr sig_qtvs name_taus wanteds
| isEmptyWC wanteds
= do { gbl_tvs <- tcGetGlobalTyVars
; qtkvs <- quantifyTyVars gbl_tvs (tyVarsOfTypes (map snd name_taus))
......@@ -472,7 +474,7 @@ simplifyInfer rhs_tclvl apply_mr name_taus wanteds
; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
; let zonked_tau_tvs = tyVarsOfTypes zonked_taus
; (qtvs, bound_theta, mr_bites)
<- decideQuantification apply_mr quant_pred_candidates zonked_tau_tvs
<- decideQuantification apply_mr sig_qtvs quant_pred_candidates zonked_tau_tvs
-- Emit an implication constraint for the
-- remaining constraints from the RHS
......@@ -564,18 +566,19 @@ and the quantified constraints are empty.
decideQuantification
:: Bool -- Apply monomorphism restriction
-> [TcTyVar]
-> [PredType] -> TcTyVarSet -- Constraints and type variables from RHS
-> TcM ( [TcTyVar] -- Quantify over these tyvars (skolems)
, [PredType] -- and this context (fully zonked)
, Bool ) -- Did the MR bite?
-- See Note [Deciding quantification]
decideQuantification apply_mr constraints zonked_tau_tvs
decideQuantification apply_mr sig_qtvs constraints zonked_tau_tvs
| apply_mr -- Apply the Monomorphism restriction
= do { gbl_tvs <- tcGetGlobalTyVars
; let constrained_tvs = tyVarsOfTypes constraints
mono_tvs = gbl_tvs `unionVarSet` constrained_tvs
mr_bites = constrained_tvs `intersectsVarSet` zonked_tau_tvs
; qtvs <- quantifyTyVars mono_tvs zonked_tau_tvs
; qtvs <- quantify_tvs mono_tvs zonked_tau_tvs
; traceTc "decideQuantification 1" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs, ppr qtvs])
; return (qtvs, [], mr_bites) }
......@@ -583,7 +586,7 @@ decideQuantification apply_mr constraints zonked_tau_tvs
= do { gbl_tvs <- tcGetGlobalTyVars
; let mono_tvs = growThetaTyVars (filter isEqPred constraints) gbl_tvs
tau_tvs_plus = growThetaTyVars constraints zonked_tau_tvs
; qtvs <- quantifyTyVars mono_tvs tau_tvs_plus
; qtvs <- quantify_tvs mono_tvs tau_tvs_plus
; constraints <- zonkTcThetaType constraints
-- quantifyTyVars turned some meta tyvars into
-- quantified skolems, so we have to zonk again
......@@ -595,6 +598,12 @@ decideQuantification apply_mr constraints zonked_tau_tvs
, ppr tau_tvs_plus, ppr qtvs, ppr min_theta])
; return (qtvs, min_theta, False) }
where
quantify_tvs mono_tvs tau_tvs -- See Note [Which type variable to quantify]
| null sig_qtvs = quantifyTyVars mono_tvs tau_tvs
| otherwise = quantifyTyVars (mono_tvs `delVarSetList` sig_qtvs)
(tau_tvs `extendVarSetList` sig_qtvs)
------------------
pickQuantifiablePreds :: TyVarSet -- Quantifying over these
-> TcThetaType -- Proposed constraints to quantify
......@@ -651,7 +660,34 @@ growThetaTyVars theta tvs
where
pred_tvs = tyVarsOfType pred
{-
{- Note [Which type variables to quantify]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When choosing type variables to quantify, the basic plan is to
quantify over all type variables that are
* free in the tau_tvs, and
* not forced to be monomorphic (mono_tvs),
for example by being free in the environment
However, for a pattern binding, or with wildards, we might
be doing inference *in the presence of a type signature*.
Mostly, if there is a signature we use CheckGen, not InferGen,
but with pattern bindings or wildcards we might do inference
and still have a type signature. For example:
f :: _ -> a
f x = ...
or
p :: a -> a
(p,q) = e
In both cases we use plan InferGen, and hence call simplifyInfer.
But those 'a' variables are skolems, and we should be sure to quantify
over them, regardless of the monomorphism restriction etc. If we
don't, when reporting a type error we panic when we find that a
skolem isn't bound by any enclosing implication.
That's why we pass sig_qtvs to simplifyInfer, and make sure (in
quantify_tvs) that we do quantify over them. Trac #10615 is
a case in point.
Note [Quantifying over equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Should we quantify over an equality constraint (s ~ t)? In general, we don't.
......@@ -1082,6 +1118,7 @@ warnRedundantGivens (SigSkol ctxt _)
FunSigCtxt _ warn_redundant -> warn_redundant
ExprSigCtxt -> True
_ -> False
warnRedundantGivens (InstSkol {}) = True
warnRedundantGivens _ = False
......@@ -1201,9 +1238,12 @@ works:
we do an ambiguity check on the type (which would find that one
of the Ord a constraints was redundant), and then we check that
the definition has that type (which might find that both are
redundant). We don't want to report the same error twice, so
we disable it for the ambiguity check. Hence the flag in
TcType.FunSigCtxt.
redundant). We don't want to report the same error twice, so we
disable it for the ambiguity check. Hence using two different
FunSigCtxts, one with the warn-redundant field set True, and the
other set False in
- TcBinds.tcSpecPrag
- TcBinds.tcTySig
This decision is taken in setImplicationStatus, rather than TcErrors
so that we can discard implication constraints that we don't need.
......
{-# LANGUAGE RankNTypes #-}
module T10615 where
f1 :: _ -> f
f1 = const
f2 :: _ -> _f
f2 = const
T10615.hs:4:7: error:
Found type wildcard ‘_’ standing for ‘a1’
Where: ‘a1’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
In the type signature for:
f1 :: _ -> f
T10615.hs:5:6: error:
Couldn't match type ‘f’ with ‘b1 -> a1’
‘f’ is a rigid type variable bound by
the inferred type of f1 :: a1 -> f at T10615.hs:4:7
Expected type: a1 -> f
Actual type: a1 -> b1 -> a1
Relevant bindings include f1 :: a1 -> f (bound at T10615.hs:5:1)
In the expression: const
In an equation for ‘f1’: f1 = const
T10615.hs:7:7: error:
Found type wildcard ‘_’ standing for ‘a0’
Where: ‘a0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
In the type signature for:
f2 :: _ -> _f
T10615.hs:8:6: error:
Couldn't match type ‘_f’ with ‘b0 -> a0’
‘_f’ is a rigid type variable bound by
the inferred type of f2 :: a0 -> _f at T10615.hs:7:7
Expected type: a0 -> _f
Actual type: a0 -> b0 -> a0
Relevant bindings include f2 :: a0 -> _f (bound at T10615.hs:8:1)
In the expression: const
In an equation for ‘f2’: f2 = const
......@@ -58,3 +58,5 @@ test('WildcardInstantiations', normal, compile_fail, [''])
test('WildcardInTypeFamilyInstanceRHS', normal, compile_fail, [''])
test('WildcardInTypeSynonymLHS', normal, compile_fail, [''])
test('WildcardInTypeSynonymRHS', normal, compile_fail, [''])
test('T10615', 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