Refactor the way we infer types for functions in a mutually recursive group
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 21 Aug 2012 13:37:20 +0000 (14:37 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 21 Aug 2012 13:37:20 +0000 (14:37 +0100)
See Note [Impedence matching] in TcBinds.
Fixes Trac #7173

compiler/typecheck/TcBinds.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSimplify.lhs

index 5eb8e15..f9c58cc 100644 (file)
@@ -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
index 60bee0b..a80c65d 100644 (file)
@@ -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
index a848e7f..c36ee43 100644 (file)
@@ -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                                               *