X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSMonad.lhs;h=23733446fbe338deddd286b076fc9dfd8439ba65;hb=2207ce8cdc4c33838f77f285c7dd4f7c75dbae1c;hp=3c1961b13a6480df31cf6aaa8bdaeece1507c104;hpb=27225b0c9f799a251c96242f502e8cfd6bf76d7c;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 3c1961b..2373344 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -9,7 +9,7 @@ module TcSMonad (
     mkWantedConstraints, deCanonicaliseWanted, 
     makeGivens, makeSolved,
 
-    CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, 
+    CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, canSolve,
     combineCtLoc, mkGivenFlavor,
 
     TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0,  -- Basic functionality 
@@ -141,8 +141,8 @@ data CanonicalCt
   | CTyEqCan {  -- tv ~ xi	(recall xi means function free)
        -- Invariant: 
        --   * tv not in tvs(xi)   (occurs check)
-       --   * If tv is a MetaTyVar, then typeKind xi <: typeKind tv 
-       --              a skolem,    then typeKind xi =  typeKind tv 
+       --   * If constraint is given then typeKind xi ==  typeKind tv 
+       --                See Note [Spontaneous solving and kind compatibility] 
       cc_id     :: EvVar, 
       cc_flavor :: CtFlavor, 
       cc_tyvar :: TcTyVar, 
@@ -153,7 +153,8 @@ data CanonicalCt
                  -- Invariant: * isSynFamilyTyCon cc_fun 
                  --            * cc_rhs is not a touchable unification variable 
                  --                   See Note [No touchables as FunEq RHS]
-                 --            * typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
+                 --            * If constraint is given then 
+                 --                 typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
       cc_id     :: EvVar,
       cc_flavor :: CtFlavor, 
       cc_fun    :: TyCon,	-- A type function
@@ -288,15 +289,54 @@ isDerived :: CtFlavor -> Bool
 isDerived (Derived {}) = True
 isDerived _            = False
 
+canSolve :: CtFlavor -> CtFlavor -> Bool 
+-- canSolve ctid1 ctid2 
+-- The constraint ctid1 can be used to solve ctid2 
+-- "to solve" means a reaction where the active parts of the two constraints match.
+--  active(F xis ~ xi) = F xis 
+--  active(tv ~ xi)    = tv 
+--  active(D xis)      = D xis 
+--  active(IP nm ty)   = nm 
+-----------------------------------------
+canSolve (Given {})   _            = True 
+canSolve (Derived {}) (Wanted {})  = True 
+canSolve (Derived {}) (Derived {}) = True 
+canSolve (Wanted {})  (Wanted {})  = True
+canSolve _ _ = False
+
 canRewrite :: CtFlavor -> CtFlavor -> Bool 
 -- canRewrite ctid1 ctid2 
--- The constraint ctid1 can be used to rewrite ctid2 
+-- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
 canRewrite (Given {})   _            = True 
 canRewrite (Derived {}) (Wanted {})  = True 
 canRewrite (Derived {}) (Derived {}) = True 
-canRewrite (Wanted {})  (Wanted {})  = True
+  -- See note [Rewriting wanteds with wanteds] 
+canRewrite (Wanted {})  (Wanted {})  = False 
 canRewrite _ _ = False
 
+\end{code}
+Note [Rewriting wanteds with wanteds] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+We will currently never use a wanted to rewrite any other 
+constraint (function @canRewrite@). If a rewriting was possible at all, 
+we simply wait until the wanted equality becomes given or derived and 
+then use it. This way we avoid rewriting by eventually insoluble wanteds, 
+such as in the following situation: 
+    w1 : a ~ Int 
+    w2 : F a ~ a 
+    w3 : F Int ~ G Bool 
+where 'a' is a skolem variable. If we rewrite using w1 inside w2 we will
+get the perhaps mystifying error at the end that we could not solve
+(a ~ Int) and (G Bool ~ Int). But there is no point in rewriting with 
+a ~ Int as long as it is still wanted.
+
+Notice that on the other hand we often do solve one wanted from another, 
+(function @canSolve@) for instance in dictionary interactions, which is 
+a reaction that enables sharing both in the solver and in the final evidence 
+produced. 
+
+\begin{code}
+
 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
 -- Precondition: At least one of them should be wanted 
 combineCtLoc (Wanted loc) _ = loc