X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=6819d5a693e29b694cf9366de3166803492597e8;hb=fd7f8e936e50b3ee589efc36ac2fc54cc6c05300;hp=d433a8c86c3fa7ba646a17cb3efdbd74bb54a08b;hpb=f8d2c44cedbfef40cc9b6497ad8f62bb090c02c8;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index d433a8c..6819d5a 100644
--- 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")