Commit 1a591a0c authored by Simon Peyton Jones's avatar Simon Peyton Jones

Refactor the way we infer types for functions in a mutually recursive group

See Note [Impedence matching] in TcBinds.
Fixes Trac #7173
parent 2c6d11fa
......@@ -548,15 +548,19 @@ mkExport :: PragFun
mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
= do { mono_ty <- zonkTcType (idType mono_id)
; let inferred_poly_ty = mkSigmaTy my_tvs theta mono_ty
my_tvs = filter (`elemVarSet` used_tvs) qtvs
used_tvs = tyVarsOfTypes theta `unionVarSet` tyVarsOfType mono_ty
poly_id = case mb_sig of
; let poly_id = case mb_sig of
Nothing -> mkLocalId poly_name inferred_poly_ty
Just sig -> sig_id sig
-- poly_id has a zonked type
-- In the inference case (no signature) this stuff figures out
-- the right type variables and theta to quantify over
-- See Note [Impedence matching]
my_tv_set = growThetaTyVars theta (tyVarsOfType mono_ty)
my_tvs = filter (`elemVarSet` my_tv_set) qtvs -- Maintain original order
my_theta = filter (quantifyPred my_tv_set) theta
inferred_poly_ty = mkSigmaTy my_tvs my_theta mono_ty
; poly_id <- addInlinePrags poly_id prag_sigs
; spec_prags <- tcSpecPrags poly_id prag_sigs
-- tcPrags requires a zonked poly_id
......@@ -571,6 +575,7 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
-- Remember we are in the tcPolyInfer case, so the type envt is
-- closed (unless we are doing NoMonoLocalBinds in which case all bets
-- are off)
-- See Note [Impedence matching]
; (wrap, wanted) <- addErrCtxtM (mk_msg poly_id) $
captureConstraints $
tcSubType origin sig_ctxt sel_poly_ty (idType poly_id)
......@@ -599,8 +604,48 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
prag_sigs = prag_fn poly_name
origin = AmbigOrigin poly_name
sig_ctxt = InfSigCtxt poly_name
\end{code}
------------------------
Note [Impedence matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f 0 x = x
f n x = g [] (not x)
g [] y = f 10 y
g _ y = f 9 y
After typechecking we'll get
f_mono_ty :: a -> Bool -> Bool
g_mono_ty :: [b] -> Bool -> Bool
with constraints
(Eq a, Num a)
Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
The types we really want for f and g are
f :: forall a. (Eq a, Num a) => a -> Bool -> Bool
g :: forall b. [b] -> Bool -> Bool
We can get these by "impedence matching":
tuple :: forall a b. (Eq a, Num a) => (a -> Bool -> Bool, [b] -> Bool -> Bool)
tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
f a d1 d2 = case tuple a Any d1 d2 of (f, g) -> f
g b = case tuple Integer b dEqInteger dNumInteger of (f,g) -> g
Suppose the shared quantified tyvars are qtvs and constraints theta.
Then we want to check that
f's polytype is more polymorphic than forall qtvs. theta => f_mono_ty
and the proof is the impedence matcher.
Notice that the impedence matcher may do defaulting. See Trac #7173.
It also cleverly does an ambiguity check; for example, rejecting
f :: F a -> a
where F is a non-injective type function.
\begin{code}
type PragFun = Name -> [LSig Name]
mkPragFun :: [LSig Name] -> LHsBinds Name -> PragFun
......
......@@ -55,7 +55,7 @@ module TcMType (
checkValidInstHead, checkValidInstance, validDerivPred,
checkInstTermination, checkValidFamInst, checkTyFamFreeness,
arityErr,
growPredTyVars, growThetaTyVars,
growThetaTyVars, quantifyPred,
--------------------------------
-- Zonking
......@@ -1408,7 +1408,38 @@ Note [Growing the tau-tvs using constraints]
E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
Then grow precs tvs = {a,b,c}
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
f x = (x::Int) + ?y
where f is *not* a top-level binding.
From the RHS of f we'll get the constraint (?y::Int).
There are two types we might infer for f:
f :: Int -> Int
(so we get ?y from the context of f's definition), or
f :: (?y::Int) => Int -> Int
At first you might think the first was better, becuase then
?y behaves like a free variable of the definition, rather than
having to be passed at each call site. But of course, the WHOLE
IDEA is that ?y should be passed at each call site (that's what
dynamic binding means) so we'd better infer the second.
BOTTOM LINE: when *inferring types* you *must* quantify
over implicit parameters. See the predicate isFreeWhenInferring.
\begin{code}
quantifyPred :: TyVarSet -- Quantifying over these
-> PredType -> Bool -- True <=> quantify over this wanted
quantifyPred qtvs pred
| isIPPred pred = True -- Note [Inheriting implicit parameters]
| otherwise = tyVarsOfType pred `intersectsVarSet` qtvs
growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
-- See Note [Growing the tau-tvs using constraints]
growThetaTyVars theta tvs
......@@ -1422,6 +1453,7 @@ growPredTyVars :: TcPredType
-> TyVarSet -- The set to extend
-> TyVarSet -- TyVars of the predicate if it intersects the set,
growPredTyVars pred tvs
| isIPPred pred = pred_tvs -- Always quantify over implicit parameers
| pred_tvs `intersectsVarSet` tvs = pred_tvs
| otherwise = emptyVarSet
where
......
......@@ -148,7 +148,9 @@ More details in Note [DefaultTyVar].
simplifyAmbiguityCheck :: Name -> WantedConstraints -> TcM (Bag EvBind)
simplifyAmbiguityCheck name wanteds
= traceTc "simplifyAmbiguityCheck" (text "name =" <+> ppr name) >>
simplifyCheck wanteds
simplifyTop wanteds -- NB: must be simplifyTop not simplifyCheck, so that we
-- do ambiguity resolution.
-- See Note [Impedence matching] in TcBinds.
------------------
simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
......@@ -404,7 +406,7 @@ simplifyInfer _top_lvl apply_mr name_taus (untch,wanteds)
; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
poly_qtvs = growThetaTyVars final_quant_candidates init_tvs
`minusVarSet` gbl_tvs
pbound = filter (quantifyMe poly_qtvs id) final_quant_candidates
pbound = filter (quantifyPred poly_qtvs) final_quant_candidates
; traceTc "simplifyWithApprox" $
vcat [ ptext (sLit "pbound =") <+> ppr pbound
......@@ -469,8 +471,8 @@ simplifyInfer _top_lvl apply_mr name_taus (untch,wanteds)
\end{code}
Note [Note [Default while Inferring]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Default while Inferring]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Our current plan is that defaulting only happens at simplifyTop and
not simplifyInfer. This may lead to some insoluble deferred constraints
Example:
......@@ -538,16 +540,6 @@ approximateWC wc = float_wc emptyVarSet wc
do_bag :: (a -> Bag c) -> Bag a -> Bag c
do_bag f = foldrBag (unionBags.f) emptyBag
quantifyMe :: TyVarSet -- Quantifying over these
-> (a -> PredType)
-> a -> Bool -- True <=> quantify over this wanted
quantifyMe qtvs toPred ct
| isIPPred pred = True -- Note [Inheriting implicit parameters]
| otherwise = tyVarsOfType pred `intersectsVarSet` qtvs
where
pred = toPred ct
\end{code}
Note [Avoid unecessary constraint simplification]
......@@ -574,32 +566,6 @@ the contraints before simplifying.
This only half-works, but then let-generalisation only half-works.
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
f x = (x::Int) + ?y
where f is *not* a top-level binding.
From the RHS of f we'll get the constraint (?y::Int).
There are two types we might infer for f:
f :: Int -> Int
(so we get ?y from the context of f's definition), or
f :: (?y::Int) => Int -> Int
At first you might think the first was better, becuase then
?y behaves like a free variable of the definition, rather than
having to be passed at each call site. But of course, the WHOLE
IDEA is that ?y should be passed at each call site (that's what
dynamic binding means) so we'd better infer the second.
BOTTOM LINE: when *inferring types* you *must* quantify
over implicit parameters. See the predicate isFreeWhenInferring.
*********************************************************************************
* *
* RULES *
......
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