Fix bug in tcSimplifyInfer (Trac #1382)

[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index d433a8c..6819d5a 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -209,8 +209,8 @@ Notice that
 
 -----------------------------------------
 
-Choosing Q
-~~~~~~~~~~
+Note [Choosing which variables to quantify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Here's a good way to choose Q:
 
        Q = grow( fv(T), C ) \ oclose( fv(G), C )
@@ -670,18 +670,35 @@ tcSimplifyInfer doc tau_tvs wanted
        ; gbl_tvs  <- tcGetGlobalTyVars
        ; let preds = fdPredsOfInsts wanted'
              qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
-             (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
-       ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ ppr (oclose preds gbl_tvs) $$ ppr free $$ ppr bound))
-       ; extendLIEs free
+                       -- See Note [Choosing which variables to quantify]
+
+               -- To maximise sharing, remove from consideration any 
+               -- constraints that don't mention qtvs at all
+       ; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted'
+       ; extendLIEs free1
 
                -- To make types simple, reduce as much as possible
+       ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ 
+                  ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
        ; let try_me inst = ReduceMe AddSCs
        ; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound
-
        ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
 
-       -- We can't abstract over implications
-       ; let (dicts, implics) = partition isDict irreds
+               -- Do not quantify over constraints that *now* do not
+               -- mention quantified type variables, because they are
+               -- simply ambiguous.  Example:
+               --      f :: Eq b => a -> (a, b)
+               --      g x = fst (f x)
+               -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
+               -- We decide to quantify over 'alpha' alone, bur free1 does not include f77
+               -- because f77 mentions 'alpha'.  Then reducing leaves only the (ambiguous)
+               -- constraint (Eq beta), which we dump back into the free set
+               -- See test tcfail181
+       ; let (free2, irreds2) = partition (isFreeWhenInferring (mkVarSet qtvs')) irreds
+       ; extendLIEs free2
+       
+               -- We can't abstract over implications
+       ; let (dicts, implics) = partition isDict irreds2
        ; loc <- getInstLoc (ImplicOrigin doc)
        ; implic_bind <- bindIrreds loc qtvs' dicts implics
 
@@ -889,7 +906,7 @@ makeImplicationBind loc all_tvs reft
  | otherwise                   -- Otherwise we must generate a binding
  = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
-       ; let name = mkInternalName uniq (mkVarOcc "ic") (srcSpanStart span)
+       ; let name = mkInternalName uniq (mkVarOcc "ic") span
              implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
                                         tci_tyvars = all_tvs, 
                                         tci_given = givens,
@@ -1202,9 +1219,22 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        ; gbl_tvs' <- tcGetGlobalTyVars
        ; constrained_dicts' <- mappM zonkInst constrained_dicts
 
-       ; let constrained_tvs' = tyVarsOfInsts constrained_dicts'
-             qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
-                        `minusVarSet` constrained_tvs'
+       ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
+                               -- As in tcSimplifyInfer
+
+               -- Do not quantify over constrained type variables:
+               -- this is the monomorphism restriction
+             constrained_tvs' = tyVarsOfInsts constrained_dicts'
+             qtvs = qtvs1 `minusVarSet` constrained_tvs'
+             pp_bndrs = pprWithCommas (quotes . ppr) bndrs
+
+       -- Warn in the mono
+       ; warn_mono <- doptM Opt_WarnMonomorphism
+       ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
+                (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding")
+                               <> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs,
+                       ptext SLIT("Consider giving a type signature for") <+> pp_bndrs])
+
        ; traceTc (text "tcSimplifyRestricted" <+> vcat [
                pprInsts wanteds, pprInsts constrained_dicts',
                ppr _binds,
@@ -2564,7 +2594,7 @@ report_no_instances tidy_env mb_what insts
                                 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
                              ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
       where
-       ispecs = [ispec | (_, ispec) <- matches]
+       ispecs = [ispec | (ispec, _) <- matches]
 
     mk_no_inst_err insts
       | null insts = empty
@@ -2637,6 +2667,10 @@ mkMonomorphismMsg tidy_env inst_tvs
   = findGlobals (mkVarSet inst_tvs) tidy_env   `thenM` \ (tidy_env, docs) ->
     returnM (tidy_env, mk_msg docs)
   where
+    mk_msg _ | any isRuntimeUnk inst_tvs
+        =  vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+>
+                   (pprWithCommas ppr inst_tvs),
+                ptext SLIT("Use :print or :force to determine these types")]
     mk_msg []   = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
                        -- This happens in things like
                        --      f x = show (read "foo")
@@ -2645,6 +2679,11 @@ mkMonomorphismMsg tidy_env inst_tvs
                        nest 2 (vcat docs),
                        monomorphism_fix
                       ]
+
+isRuntimeUnk :: TcTyVar -> Bool
+isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
+               | otherwise = False
+
 monomorphism_fix :: SDoc
 monomorphism_fix = ptext SLIT("Probable fix:") <+> 
                   (ptext SLIT("give these definition(s) an explicit type signature")