From ce721cdc0bc98361fd20defc5f919bb12abe1634 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Tue, 21 Aug 2012 14:37:20 +0100
Subject: [PATCH] Refactor the way we infer types for functions in a mutually
recursive group
See Note [Impedence matching] in TcBinds.
Fixes Trac #7173
MERGED from commit 1a591a0ce0e1b70eb5e6646542d5f110bfefc9af
---
compiler/typecheck/TcBinds.lhs | 57 +++++++++++++++++++++++++++----
compiler/typecheck/TcMType.lhs | 34 +++++++++++++++++-
compiler/typecheck/TcSimplify.lhs | 46 ++++---------------------
3 files changed, 90 insertions(+), 47 deletions(-)
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index 5eb8e150efca..f9c58ccd992e 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -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
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 2817ea9d637d..411d85a19b85 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -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
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index a848e7fdff4f..c36ee43f8371 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -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 *
--
GitLab