X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=f7d0021183c98bf0d339d7547d514d7b16b9b9b1;hb=4016ee2f11eaaa0a3f9f5f04aebd84d4c8f68ce4;hp=f651e0f6febdd9b47459496069013e755145e0f2;hpb=0f5e104c36b1dc3d8deeec5fef3d65e7b3a1b5ad;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index f651e0f..f7d0021 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -36,6 +36,7 @@ import TcIface
 import TcTyFuns
 import DsUtils	-- Big-tuple functions
 import Var
+import Id
 import Name
 import NameSet
 import Class
@@ -57,7 +58,6 @@ import Util
 import SrcLoc
 import DynFlags
 import FastString
-
 import Control.Monad
 import Data.List
 \end{code}
@@ -91,34 +91,36 @@ we reduce the (C a b1) constraint from the call of f to (D a b1).
 
 Here is a more complicated example:
 
-| > class Foo a b | a->b
-| >
-| > class Bar a b | a->b
-| >
-| > data Obj = Obj
-| >
-| > instance Bar Obj Obj
-| >
-| > instance (Bar a b) => Foo a b
-| >
-| > foo:: (Foo a b) => a -> String
-| > foo _ = "works"
-| >
-| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
-| > runFoo f = f Obj
-| 
-| *Test> runFoo foo
-| 
-| <interactive>:1:
-|     Could not deduce (Bar a b) from the context (Foo a b)
-|       arising from use of `foo' at <interactive>:1
-|     Probable fix:
-|         Add (Bar a b) to the expected type of an expression
-|     In the first argument of `runFoo', namely `foo'
-|     In the definition of `it': it = runFoo foo
-| 
-| Why all of the sudden does GHC need the constraint Bar a b? The
-| function foo didn't ask for that... 
+@
+  > class Foo a b | a->b
+  >
+  > class Bar a b | a->b
+  >
+  > data Obj = Obj
+  >
+  > instance Bar Obj Obj
+  >
+  > instance (Bar a b) => Foo a b
+  >
+  > foo:: (Foo a b) => a -> String
+  > foo _ = "works"
+  >
+  > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
+  > runFoo f = f Obj
+
+  *Test> runFoo foo
+
+  <interactive>:1:
+      Could not deduce (Bar a b) from the context (Foo a b)
+        arising from use of `foo' at <interactive>:1
+      Probable fix:
+          Add (Bar a b) to the expected type of an expression
+      In the first argument of `runFoo', namely `foo'
+      In the definition of `it': it = runFoo foo
+
+  Why all of the sudden does GHC need the constraint Bar a b? The
+  function foo didn't ask for that...
+@
 
 The trouble is that to type (runFoo foo), GHC has to solve the problem:
 
@@ -1482,27 +1484,55 @@ Instead we want to quantify over the dictionaries separately.
 
 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
 all dicts unchanged, with absolutely no sharing.  It's simpler to do this
-from scratch, rather than further parameterise simpleReduceLoop etc
+from scratch, rather than further parameterise simpleReduceLoop etc.
+Simpler, maybe, but alas not simple (see Trac #2494)
+
+* Type errors may give rise to an (unsatisfiable) equality constraint
+
+* Applications of a higher-rank function on the LHS may give
+  rise to an implication constraint, esp if there are unsatisfiable
+  equality constraints inside.
 
 \begin{code}
 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
 tcSimplifyRuleLhs wanteds
-  = go [] emptyBag wanteds
+  = do	{ wanteds' <- zonkInsts wanteds
+	; (irreds, binds) <- go [] emptyBag wanteds'
+	; let (dicts, bad_irreds) = partition isDict irreds
+	; traceTc (text "tcSimplifyrulelhs" <+> pprInsts bad_irreds)
+	; addNoInstanceErrs (nub bad_irreds)
+		-- The nub removes duplicates, which has
+		-- not happened otherwise (see notes above)
+	; return (dicts, binds) }
   where
-    go dicts binds []
-	= return (dicts, binds)
-    go dicts binds (w:ws)
+    go :: [Inst] -> TcDictBinds -> [Inst] -> TcM ([Inst], TcDictBinds)
+    go irreds binds []
+	= return (irreds, binds)
+    go irreds binds (w:ws)
 	| isDict w
-	= go (w:dicts) binds ws
+	= go (w:irreds) binds ws
+	| isImplicInst w	-- Have a go at reducing the implication
+	= do { (binds1, irreds1) <- reduceImplication red_env w
+	     ; let (bad_irreds, ok_irreds) = partition isImplicInst irreds1
+	     ; go (bad_irreds ++ irreds) 
+		  (binds `unionBags` binds1) 
+		  (ok_irreds ++ ws)}
 	| otherwise
 	= do { w' <- zonkInst w  -- So that (3::Int) does not generate a call
 				 -- to fromInteger; this looks fragile to me
 	     ; lookup_result <- lookupSimpleInst w'
 	     ; case lookup_result of
-		 GenInst ws' rhs -> 
-                   go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)
-		 NoInstance	 -> pprPanic "tcSimplifyRuleLhs" (ppr w)
+		 NoInstance      -> go (w:irreds) binds ws
+		 GenInst ws' rhs -> go irreds binds' (ws' ++ ws)
+			where
+			  binds' = addInstToDictBind binds w rhs
 	  }
+
+	-- Sigh: we need to reduce inside implications
+    red_env = mkRedEnv doc try_me []
+    doc = ptext (sLit "Implication constraint in RULE lhs")
+    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+		| otherwise	     = Stop	-- Be gentle
 \end{code}
 
 tcSimplifyBracket is used when simplifying the constraints arising from
@@ -1771,7 +1801,7 @@ reduceContext env wanteds
 		; return init_state
                 }
 
-	-- *** ToDo: what to do with the "extra_givens"?  For the
+	-- !!! ToDo: what to do with the "extra_givens"?  For the
 	-- moment I'm simply discarding them, which is probably wrong
 
           -- 6. Solve the *wanted* *dictionary* constraints (not implications)