Improve handling of implicit parameters

A message to Haskell Cafe from Grzegorz Chrupala made me realise that
GHC was not handling implicit parameters correctly, when it comes to
choosing the variables to quantify, and ambiguity tests.  Here's the
note I added to TcSimplify:

Note [Implicit parameters and ambiguity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
What type should we infer for this?
	f x = (show ?y, x::Int)
Since we must quantify over the ?y, the most plausible type is
	f :: (Show a, ?y::a) => Int -> (String, Int)
But notice that the type of the RHS is (String,Int), with no type
varibables mentioned at all!  The type of f looks ambiguous.  But
it isn't, because at a call site we might have
	let ?y = 5::Int in f 7
and all is well.  In effect, implicit parameters are, well, parameters,
so we can take their type variables into account as part of the
"tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.

The actual changes are in FunDeps.grow, and the tests are
	tc219, tc219

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 2a3691a..2347d37 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -398,8 +398,8 @@ When m is later unified with [], we can solve both constraints.
                Notes on implicit parameters
        --------------------------------------
 
-Question 1: can we "inherit" implicit parameters
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Inheriting implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this:
 
        f x = (x::Int) + ?y
@@ -424,6 +424,21 @@ BOTTOM LINE: when *inferring types* you *must* quantify
 over implicit parameters. See the predicate isFreeWhenInferring.
 
 
+Note [Implicit parameters and ambiguity] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What type should we infer for this?
+       f x = (show ?y, x::Int)
+Since we must quantify over the ?y, the most plausible type is
+       f :: (Show a, ?y::a) => Int -> (String, Int)
+But notice that the type of the RHS is (String,Int), with no type 
+varibables mentioned at all!  The type of f looks ambiguous.  But
+it isn't, because at a call site we might have
+       let ?y = 5::Int in f 7
+and all is well.  In effect, implicit parameters are, well, parameters,
+so we can take their type variables into account as part of the
+"tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
+
+
 Question 2: type signatures
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 BUT WATCH OUT: When you supply a type signature, we can't force you
@@ -719,9 +734,9 @@ The net effect of [NO TYVARS]
 \begin{code}
 isFreeWhenInferring :: TyVarSet -> Inst        -> Bool
 isFreeWhenInferring qtvs inst
-  =  isFreeWrtTyVars qtvs inst         -- Constrains no quantified vars
-  && isInheritableInst inst            -- And no implicit parameter involved
-                                       -- (see "Notes on implicit parameters")
+  =  isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
+  && isInheritableInst inst    -- and no implicit parameter involved
+                               --   see Note [Inheriting implicit parameters]
 
 {-     No longer used (with implication constraints)
 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
@@ -2431,7 +2446,8 @@ addTopIPErrs bndrs ips
   where
     (tidy_env, tidy_ips) = tidyInsts ips
     mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
-                           nest 2 (ptext SLIT("the monomorphic top-level binding(s) of")
+                           nest 2 (ptext SLIT("the monomorphic top-level binding") 
+                                           <> plural bndrs <+> ptext SLIT("of")
                                            <+> pprBinders bndrs <> colon)],
                       nest 2 (vcat (map ppr_ip ips)),
                       monomorphism_fix]

diff --git a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs
index cad292b..b8b97b1 100644 (file)
--- a/compiler/types/FunDeps.lhs
+++ b/compiler/types/FunDeps.lhs
@@ -21,8 +21,6 @@ import Name
 import Var
 import Class
 import TcGadt
-import Type
-import Coercion
 import TcType
 import InstEnv
 import VarSet
@@ -125,24 +123,43 @@ oclose preds fixed_tvs
              ]
 \end{code}
 
+Note [Growing the tau-tvs using constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(grow preds tvs) is the result of extend the set of tyvars tvs
+                using all conceivable links from pred
+
+E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
+Then grow precs tvs = {a,b,c}
+
+All the type variables from an implicit parameter are added, whether or
+not they are mentioned in tvs; see Note [Implicit parameters and ambiguity] 
+in TcSimplify.
+
+See also Note [Ambiguity] in TcSimplify
+
 \begin{code}
 grow :: [PredType] -> TyVarSet -> TyVarSet
--- See Note [Ambiguity] in TcSimplify
 grow preds fixed_tvs 
-  | null preds = fixed_tvs
-  | otherwise  = loop fixed_tvs
+  | null preds = real_fixed_tvs
+  | otherwise  = loop real_fixed_tvs
   where
+       -- Add the implicit parameters; 
+       -- see Note [Implicit parameters and ambiguity] in TcSimplify
+    real_fixed_tvs = foldr unionVarSet fixed_tvs ip_tvs
+ 
     loop fixed_tvs
        | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
        | otherwise                           = loop new_fixed_tvs
        where
-         new_fixed_tvs = foldl extend fixed_tvs pred_sets
+         new_fixed_tvs = foldl extend fixed_tvs non_ip_tvs
 
     extend fixed_tvs pred_tvs 
        | fixed_tvs `intersectsVarSet` pred_tvs = fixed_tvs `unionVarSet` pred_tvs
        | otherwise                             = fixed_tvs
 
-    pred_sets = [tyVarsOfPred pred | pred <- preds]
+    (ip_tvs, non_ip_tvs) = partitionWith get_ip preds
+    get_ip (IParam _ ty) = Left (tyVarsOfType ty)
+    get_ip other         = Right (tyVarsOfPred other)
 \end{code}
     
 %************************************************************************
@@ -276,7 +293,7 @@ improveOne inst_env pred@(ClassP cls tys, _) preds
        , let rough_fd_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
        , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst, 
                            is_tcs = mb_tcs_inst }) <- instances
-       , not (instanceCantMatch mb_tcs_inst rough_tcs)
+       , not (instanceCantMatch mb_tcs_inst rough_fd_tcs)
        , eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys
        , let p_inst = (mkClassPred cls tys_inst, 
                        ptext SLIT("arising from the instance declaration at")