Use "on the spot" solving for fundeps

When we spot an equality arising from a functional dependency,
we now use that equality (a "wanted") to rewrite the work-item
constraint right away.  This avoids two dangers

 Danger 1: If we send the original constraint on down the pipeline
           it may react with an instance declaration, and in delicate
	   situations (when a Given overlaps with an instance) that
	   may produce new insoluble goals: see Trac #4952

 Danger 2: If we don't rewrite the constraint, it may re-react
           with the same thing later, and produce the same equality
           again --> termination worries.

To achieve this required some refactoring of FunDeps.lhs (nicer
now!).

This patch also contains a couple of unrelated improvements

* A bad bug in TcSMonad.nestImplicTcS whereby the Tcs tyvars
  of an outer implication were not untouchable inside

* Improved logging machinery for the type constraint solver;
  use -ddump-cs-trace (probably with a wider default line width
  -dppr-cols=200 or something)

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 9147a92..7bd4d84 100644 (file)
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -153,6 +153,7 @@ data DynFlag
    | Opt_D_dump_rn_stats
    | Opt_D_dump_opt_cmm
    | Opt_D_dump_simpl_stats
    | Opt_D_dump_rn_stats
    | Opt_D_dump_opt_cmm
    | Opt_D_dump_simpl_stats

+   | Opt_D_dump_cs_trace       -- Constraint solver in type checker

    | Opt_D_dump_tc_trace
    | Opt_D_dump_if_trace
    | Opt_D_dump_splices
    | Opt_D_dump_tc_trace
    | Opt_D_dump_if_trace
    | Opt_D_dump_splices

@@ -1259,6 +1260,7 @@ dynamic_flags = [
   , Flag "ddump-worker-wrapper"    (setDumpFlag Opt_D_dump_worker_wrapper)
   , Flag "ddump-rn-trace"          (setDumpFlag Opt_D_dump_rn_trace)
   , Flag "ddump-if-trace"          (setDumpFlag Opt_D_dump_if_trace)
   , Flag "ddump-worker-wrapper"    (setDumpFlag Opt_D_dump_worker_wrapper)
   , Flag "ddump-rn-trace"          (setDumpFlag Opt_D_dump_rn_trace)
   , Flag "ddump-if-trace"          (setDumpFlag Opt_D_dump_if_trace)

+  , Flag "ddump-cs-trace"          (setDumpFlag Opt_D_dump_cs_trace)

   , Flag "ddump-tc-trace"          (setDumpFlag Opt_D_dump_tc_trace)
   , Flag "ddump-splices"           (setDumpFlag Opt_D_dump_splices)
   , Flag "ddump-rn-stats"          (setDumpFlag Opt_D_dump_rn_stats)
   , Flag "ddump-tc-trace"          (setDumpFlag Opt_D_dump_tc_trace)
   , Flag "ddump-splices"           (setDumpFlag Opt_D_dump_splices)
   , Flag "ddump-rn-stats"          (setDumpFlag Opt_D_dump_rn_stats)

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 861b262..8668d90 100644 (file)
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -1,7 +1,8 @@
 \begin{code}
 module TcCanonical(
     mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens,
 \begin{code}
 module TcCanonical(
     mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens,

-    canOccursCheck, canEq
+    canOccursCheck, canEq,
+    rewriteWithFunDeps

  ) where
 
 #include "HsVersions.h"
  ) where
 
 #include "HsVersions.h"

@@ -9,7 +10,8 @@ module TcCanonical(
 import BasicTypes
 import Type
 import TcRnTypes
 import BasicTypes
 import Type
 import TcRnTypes

-
+import FunDeps
+import qualified TcMType as TcM

 import TcType
 import TcErrors
 import Coercion
 import TcType
 import TcErrors
 import Coercion

@@ -18,6 +20,7 @@ import TyCon
 import TypeRep
 import Name
 import Var
 import TypeRep
 import Name
 import Var

+import VarEnv          ( TidyEnv )

 import Outputable
 import Control.Monad    ( unless, when, zipWithM, zipWithM_ )
 import MonadUtils
 import Outputable
 import Control.Monad    ( unless, when, zipWithM, zipWithM_ )
 import MonadUtils

@@ -28,6 +31,7 @@ import Bag
 
 import HsBinds
 import TcSMonad
 
 import HsBinds
 import TcSMonad

+import FastString

 \end{code}
 
 Note [Canonicalisation]
 \end{code}
 
 Note [Canonicalisation]

@@ -991,4 +995,75 @@ a.  If this turns out to be impossible, we next try expanding F
 itself, and so on.
 
 
 itself, and so on.
 
 

+%************************************************************************
+%*                                                                      *
+%*          Functional dependencies, instantiation of equations
+%*                                                                      *
+%************************************************************************

 
 

+\begin{code}
+rewriteWithFunDeps :: [Equation]
+                   -> [Xi] -> CtFlavor
+                   -> TcS (Maybe ([Xi], [Coercion], CanonicalCts))
+rewriteWithFunDeps eqn_pred_locs xis fl
+ = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
+      ; let fd_ev_pos :: [(Int,FlavoredEvVar)]
+            fd_ev_pos = concat fd_ev_poss
+            (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
+      ; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
+      ; let fd_work = unionManyBags fds
+      ; if isEmptyBag fd_work 
+        then return Nothing
+        else return (Just (rewritten_xis, cos, fd_work)) }
+
+instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
+              -> Equation
+              -> TcS [(Int, FlavoredEvVar)]
+-- Post: Returns the position index as well as the corresponding FunDep equality
+instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
+                        , fd_pred1 = d1, fd_pred2 = d2 })
+  = do { let tvs = varSetElems qtvs
+       ; tvs' <- mapM instFlexiTcS tvs
+       ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
+       ; mapM (do_one subst) eqs }
+  where 
+    fl' = case fl of 
+             Given _     -> panic "mkFunDepEqns"
+             Wanted  loc -> Wanted  (push_ctx loc)
+             Derived loc -> Derived (push_ctx loc)
+
+    push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
+
+    do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
+       = do { let sty1 = substTy subst ty1
+                  sty2 = substTy subst ty2
+            ; ev <- newCoVar sty1 sty2
+            ; return (i, mkEvVarX ev fl') }
+
+rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
+                  -> [Type]                -- A sequence of types: tys
+                  -> [(Type,Coercion)]     -- Returns            : [(ty', co : ty' ~ ty)]
+rewriteDictParams param_eqs tys
+  = zipWith do_one tys [0..]
+  where
+    do_one :: Type -> Int -> (Type,Coercion)
+    do_one ty n = case lookup n param_eqs of
+                    Just wev -> (get_fst_ty wev, mkCoVarCoercion (evVarOf wev))
+                    Nothing  -> (ty,ty)                -- Identity
+
+    get_fst_ty wev = case evVarOfPred wev of
+                          EqPred ty1 _ -> ty1
+                          _ -> panic "rewriteDictParams: non equality fundep"
+
+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+         -> TcM (TidyEnv, SDoc)
+mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
+  = do  { zpred1 <- TcM.zonkTcPredType pred1
+        ; zpred2 <- TcM.zonkTcPredType pred2
+       ; let { tpred1 = tidyPred tidy_env zpred1
+              ; tpred2 = tidyPred tidy_env zpred2 }
+       ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
+                         nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), 
+                         nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
+       ; return (tidy_env, msg) }
+\end{code}
\ No newline at end of file

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index f9d3d97..3f166cf 100644 (file)
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -20,7 +20,6 @@ import TcType
 import HsBinds
 
 import Inst( tyVarsOfEvVar )
 import HsBinds
 
 import Inst( tyVarsOfEvVar )

-import InstEnv

 import Class
 import TyCon
 import Name
 import Class
 import TyCon
 import Name

@@ -270,21 +269,24 @@ instance Outputable StageResult where
                  , ptext (sLit "new work =") <+> ppr work <> comma
                  , ptext (sLit "stop =") <+> ppr stop])
 
                  , ptext (sLit "new work =") <+> ppr work <> comma
                  , ptext (sLit "stop =") <+> ppr stop])
 

-type SimplifierStage = WorkItem -> InertSet -> TcS StageResult 
+type SubGoalDepth = Int          -- Starts at zero; used to limit infinite
+                         -- recursion of sub-goals
+type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult 

 
 -- Combine a sequence of simplifier 'stages' to create a pipeline 
 
 -- Combine a sequence of simplifier 'stages' to create a pipeline 

-runSolverPipeline :: [(String, SimplifierStage)]
-                  -> InertSet -> WorkItem 
+runSolverPipeline :: SubGoalDepth
+                  -> [(String, SimplifierStage)]
+                 -> InertSet -> WorkItem 

                   -> TcS (InertSet, WorkList)
 -- Precondition: non-empty list of stages 
                   -> TcS (InertSet, WorkList)
 -- Precondition: non-empty list of stages 

-runSolverPipeline pipeline inerts workItem
+runSolverPipeline depth pipeline inerts workItem

   = do { traceTcS "Start solver pipeline" $ 
             vcat [ ptext (sLit "work item =") <+> ppr workItem
                  , ptext (sLit "inerts    =") <+> ppr inerts]
 
        ; let itr_in = SR { sr_inerts = inerts
   = do { traceTcS "Start solver pipeline" $ 
             vcat [ ptext (sLit "work item =") <+> ppr workItem
                  , ptext (sLit "inerts    =") <+> ppr inerts]
 
        ; let itr_in = SR { sr_inerts = inerts

-                        , sr_new_work = emptyWorkList
-                        , sr_stop = ContinueWith workItem }
+                         , sr_new_work = emptyWorkList
+                         , sr_stop = ContinueWith workItem }

        ; itr_out <- run_pipeline pipeline itr_in
        ; let new_inert 
               = case sr_stop itr_out of 
        ; itr_out <- run_pipeline pipeline itr_in
        ; let new_inert 
               = case sr_stop itr_out of 

@@ -301,7 +303,7 @@ runSolverPipeline pipeline inerts workItem
                  (SR { sr_new_work = accum_work
                      , sr_inerts   = inerts
                      , sr_stop     = ContinueWith work_item })
                  (SR { sr_new_work = accum_work
                      , sr_inerts   = inerts
                      , sr_stop     = ContinueWith work_item })

-      = do { itr <- stage work_item inerts 
+      = do { itr <- stage depth work_item inerts 

            ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
            ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
            ; run_pipeline stages itr' }
            ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
            ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
            ; run_pipeline stages itr' }

@@ -468,21 +470,18 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
 -- new inert set which has assimilated the new information.
 solveOneWithDepth :: (Int, Int, [WorkItem])
                   -> InertSet -> WorkItem -> TcS InertSet
 -- new inert set which has assimilated the new information.
 solveOneWithDepth :: (Int, Int, [WorkItem])
                   -> InertSet -> WorkItem -> TcS InertSet

-solveOneWithDepth (max_depth, n, stack) inert work
-  = do { traceTcS0 (indent ++ "Solving {") (ppr work)
-       ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
+solveOneWithDepth (max_depth, depth, stack) inert work
+  = do { traceFireTcS depth (text "Solving {" <+> ppr work)
+       ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work

          
          

-       ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
-

         -- Recursively solve the new work generated 
          -- from workItem, with a greater depth
         -- Recursively solve the new work generated 
          -- from workItem, with a greater depth

-       ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
+       ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack)

                                 new_inert new_work 
 
                                 new_inert new_work 
 

-       ; traceTcS0 (indent ++ "Done }") (ppr work) 
+       ; traceFireTcS depth (text "Done }" <+> ppr work) 
+

        ; return res_inert }
        ; return res_inert }

-  where
-    indent = replicate (2*n) ' '

 
 thePipeline :: [(String,SimplifierStage)]
 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
 
 thePipeline :: [(String,SimplifierStage)]
 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)

@@ -524,7 +523,7 @@ Case 3: IP improvement work
 
 \begin{code}
 spontaneousSolveStage :: SimplifierStage 
 
 \begin{code}
 spontaneousSolveStage :: SimplifierStage 

-spontaneousSolveStage workItem inerts 
+spontaneousSolveStage depth workItem inerts 

   = do { mSolve <- trySpontaneousSolve workItem
 
        ; case mSolve of 
   = do { mSolve <- trySpontaneousSolve workItem
 
        ; case mSolve of 

@@ -540,7 +539,9 @@ spontaneousSolveStage workItem inerts
                  -- its status change. This in turn may produce more work.
                 -- We do this *right now* (rather than just putting workItem'
                 -- back into the work-list) because we've solved 
                  -- its status change. This in turn may produce more work.
                 -- We do this *right now* (rather than just putting workItem'
                 -- back into the work-list) because we've solved 

-               -> do { (new_inert, new_work) <- runSolverPipeline 
+               -> do { bumpStepCountTcS
+                    ; traceFireTcS depth (ptext (sLit "Spontaneous (w/d)") <+> ppr workItem)
+                     ; (new_inert, new_work) <- runSolverPipeline depth

                              [ ("recursive interact with inert eqs", interactWithInertEqsStage)
                              , ("recursive interact with inerts", interactWithInertsStage)
                              ] inerts workItem'
                              [ ("recursive interact with inert eqs", interactWithInertEqsStage)
                              , ("recursive interact with inerts", interactWithInertsStage)
                              ] inerts workItem'

@@ -551,9 +552,11 @@ spontaneousSolveStage workItem inerts
                | otherwise 
                    -> -- Original was given; he must then be inert all right, and
                       -- workList' are all givens from flattening
                | otherwise 
                    -> -- Original was given; he must then be inert all right, and
                       -- workList' are all givens from flattening

-                      return $ SR { sr_new_work = emptyWorkList
-                                  , sr_inerts   = inerts `updInertSet` workItem' 
-                                  , sr_stop     = Stop }
+                      do { bumpStepCountTcS
+                        ; traceFireTcS depth (ptext (sLit "Spontaneous (g)") <+> ppr workItem)
+                         ; return $ SR { sr_new_work = emptyWorkList
+                                       , sr_inerts   = inerts `updInertSet` workItem' 
+                                       , sr_stop     = Stop } }

            SPError -> -- Return with no new work
                return $ SR { sr_new_work = emptyWorkList
                            , sr_inerts   = inerts
            SPError -> -- Return with no new work
                return $ SR { sr_new_work = emptyWorkList
                            , sr_inerts   = inerts

@@ -584,7 +587,8 @@ trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar =
   | otherwise
   = do { tch1 <- isTouchableMetaTyVar tv1
        ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
   | otherwise
   = do { tch1 <- isTouchableMetaTyVar tv1
        ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi

-                 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem) 
+                 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" 
+                                    (ppr workItem) 

                          ; return SPCantSolve }
        }
 
                          ; return SPCantSolve }
        }
 

@@ -758,24 +762,27 @@ data InteractResult
 
         , ir_new_work     :: WorkList
             -- new work items to add to the WorkList
 
         , ir_new_work     :: WorkList
             -- new work items to add to the WorkList

+
+        , ir_fire :: Maybe String    -- Tells whether a rule fired, and if so what

         }
 
 -- What to do with the inert reactant.
         }
 
 -- What to do with the inert reactant.

-data InertAction = KeepInert 
-                 | DropInert 
-                 | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert
-
-mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
-mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork 
+data InertAction = KeepInert | DropInert 

 
 

-mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
-mkIRStop keep newWork = return $ IR Stop keep newWork 
+mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult
+mkIRContinue rule wi keep newWork 
+  = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep
+                , ir_new_work = newWork, ir_fire = Just rule }

 
 

-dischargeWorkItem :: Monad m => m InteractResult
-dischargeWorkItem = mkIRStop KeepInert emptyWorkList
+mkIRStop :: String -> WorkList -> TcS InteractResult
+mkIRStop rule newWork
+  = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert
+                , ir_new_work = newWork, ir_fire = Just rule }

 
 noInteraction :: Monad m => WorkItem -> m InteractResult
 
 noInteraction :: Monad m => WorkItem -> m InteractResult

-noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
+noInteraction wi
+  = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert
+                , ir_new_work = emptyWorkList, ir_fire = Nothing }

 
 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert 
      -- See Note [Efficient Orientation] 
 
 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert 
      -- See Note [Efficient Orientation] 

@@ -788,8 +795,8 @@ data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
 -- interact the WorkItem with the entire equalities of the InertSet
 
 interactWithInertEqsStage :: SimplifierStage 
 -- interact the WorkItem with the entire equalities of the InertSet
 
 interactWithInertEqsStage :: SimplifierStage 

-interactWithInertEqsStage workItem inert
-  = Bag.foldlBagM interactNext initITR (inert_eqs inert)
+interactWithInertEqsStage depth workItem inert
+  = Bag.foldlBagM (interactNext depth) initITR (inert_eqs inert)

   where
     initITR = SR { sr_inerts   = inert { inert_eqs = emptyCCan }
                  , sr_new_work = emptyWorkList
   where
     initITR = SR { sr_inerts   = inert { inert_eqs = emptyCCan }
                  , sr_new_work = emptyWorkList

@@ -802,12 +809,12 @@ interactWithInertEqsStage workItem inert
 -- "Other" constraints it contains!
 
 interactWithInertsStage :: SimplifierStage
 -- "Other" constraints it contains!
 
 interactWithInertsStage :: SimplifierStage

-interactWithInertsStage workItem inert
+interactWithInertsStage depth workItem inert

   = let (relevant, inert_residual) = getISRelevant workItem inert 
         initITR = SR { sr_inerts   = inert_residual
                      , sr_new_work = emptyWorkList
                      , sr_stop     = ContinueWith workItem } 
   = let (relevant, inert_residual) = getISRelevant workItem inert 
         initITR = SR { sr_inerts   = inert_residual
                      , sr_new_work = emptyWorkList
                      , sr_stop     = ContinueWith workItem } 

-    in Bag.foldlBagM interactNext initITR relevant 
+    in Bag.foldlBagM (interactNext depth) initITR relevant 

   where 
     getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet) 
     getISRelevant (CFrozenErr {}) is = (emptyCCan, is)
   where 
     getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet) 
     getISRelevant (CFrozenErr {}) is = (emptyCCan, is)

@@ -834,23 +841,37 @@ interactWithInertsStage workItem inert
                     , inert_ips    = emptyCCanMap
                     , inert_funeqs = emptyCCanMap })
 
                     , inert_ips    = emptyCCanMap
                     , inert_funeqs = emptyCCanMap })
 

-interactNext :: StageResult -> AtomicInert -> TcS StageResult 
-interactNext it inert  
-  | ContinueWith workItem <- sr_stop it
-  = do { let inerts      = sr_inerts it 
-
-       ; ir <- interactWithInert inert workItem
-
-       -- New inerts depend on whether we KeepInert or not and must
-       -- be updated with FD improvement information from the interaction result (ir)
-       ; let inerts_new = case ir_inert_action ir of
-                            KeepInert                   -> inerts `updInertSet` inert
-                            DropInert                   -> inerts
-                            KeepTransformedInert inert' -> inerts `updInertSet` inert'
+interactNext :: SubGoalDepth -> StageResult -> AtomicInert -> TcS StageResult 
+interactNext depth it inert  
+  | ContinueWith work_item <- sr_stop it
+  = do { let inerts = sr_inerts it 
+
+       ; IR { ir_new_work = new_work, ir_inert_action = inert_action
+            , ir_fire = fire_info, ir_stop = stop } 
+            <- interactWithInert inert work_item
+
+       ; let mk_msg rule 
+              = text rule <+> keep_doc
+                <+> vcat [ ptext (sLit "Inert =") <+> ppr inert
+                         , ptext (sLit "Work =")  <+> ppr work_item
+                         , ppUnless (isEmptyBag new_work) $
+                            ptext (sLit "New =") <+> ppr new_work ]
+             keep_doc = case inert_action of
+                         KeepInert -> ptext (sLit "[keep]")
+                         DropInert -> ptext (sLit "[drop]")
+       ; case fire_info of
+           Just rule -> do { bumpStepCountTcS
+                           ; traceFireTcS depth (mk_msg rule) }
+           Nothing  -> return ()
+
+       -- New inerts depend on whether we KeepInert or not 
+       ; let inerts_new = case inert_action of
+                            KeepInert -> inerts `updInertSet` inert
+                            DropInert -> inerts

 
        ; return $ SR { sr_inerts   = inerts_new
 
        ; return $ SR { sr_inerts   = inerts_new

-                     , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
-                     , sr_stop     = ir_stop ir } }
+                     , sr_new_work = sr_new_work it `unionWorkLists` new_work
+                     , sr_stop     = stop } }

   | otherwise 
   = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
 
   | otherwise 
   = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
 

@@ -878,7 +899,7 @@ doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
 
 doInteractWithInert
            (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) 
 
 doInteractWithInert
            (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) 

-  workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
+  workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })

   | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
   = solveOneFromTheOther (d1,fl1) workItem 
 
   | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
   = solveOneFromTheOther (d1,fl1) workItem 
 

@@ -886,18 +907,46 @@ doInteractWithInert
   =     -- See Note [When improvement happens]
     do { let pty1 = ClassP cls1 tys1
              pty2 = ClassP cls2 tys2
   =     -- See Note [When improvement happens]
     do { let pty1 = ClassP cls1 tys1
              pty2 = ClassP cls2 tys2

-             work_item_pred_loc = (pty2, pprFlavorArising fl2)

              inert_pred_loc     = (pty1, pprFlavorArising fl1)
              inert_pred_loc     = (pty1, pprFlavorArising fl1)

-            loc                = combineCtLoc fl1 fl2
-             eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
-                             -- See Note [Efficient Orientation]
-
-       ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs
-       ; fd_work <- mapM mkCanonicalFEV derived_evs
-                 -- See Note [Generating extra equalities]
-
-       ; mkIRContinue workItem KeepInert (unionManyBags fd_work)
-       }
+             work_item_pred_loc = (pty2, pprFlavorArising fl2)
+             fd_eqns = improveFromAnother 
+                                  inert_pred_loc     -- the template
+                                  work_item_pred_loc -- the one we aim to rewrite
+                                  -- See Note [Efficient Orientation]
+
+       ; m <- rewriteWithFunDeps fd_eqns tys2 fl2
+       ; case m of 
+           Nothing -> noInteraction workItem
+           Just (rewritten_tys2, cos2, fd_work)
+
+             | tcEqTypes tys1 rewritten_tys2
+             -> -- Solve him on the spot in this case
+                do { let dict_co = mkTyConCoercion (classTyCon cls1) cos2
+                   ; when (isWanted fl2) $ setDictBind d2 (EvCast d1 dict_co)
+                   ; mkIRStop "Cls/Cls fundep (solved)" fd_work }
+
+             | isWanted fl2
+             -> -- We could not quite solve him, but we stil rewrite him
+               -- Example: class C a b c | a -> b
+               --          Given: C Int Bool x, Wanted: C Int beta y
+               --          Then rewrite the wanted to C Int Bool y
+               --          but note that is still not identical to the given
+               -- The important thing is that the rewritten constraint is
+               -- inert wrt the given.
+               -- In fact, it is inert wrt all the previous inerts too, so
+               -- we can keep on going rather than sending it back to the work list
+                do { let dict_co = mkTyConCoercion (classTyCon cls1) cos2
+                   ; d2' <- newDictVar cls1 rewritten_tys2
+                   ; setDictBind d2 (EvCast d2' dict_co)
+                   ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 }
+                   ; mkIRContinue "Cls/Cls fundep (partial)" workItem' KeepInert fd_work } 
+
+             | otherwise
+             -> ASSERT (isDerived fl2) -- Derived constraints have no evidence,
+                                       -- so just produce the rewritten constraint
+                let workItem' = workItem { cc_tyargs = rewritten_tys2 }
+                in mkIRContinue "Cls/Cls fundep" workItem' KeepInert fd_work 
+  }

 
 -- Class constraint and given equality: use the equality to rewrite
 -- the class constraint. 
 
 -- Class constraint and given equality: use the equality to rewrite
 -- the class constraint. 

@@ -908,14 +957,14 @@ doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_r
   = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
             -- Continue with rewritten Dictionary because we can only be in the 
             -- interactWithEqsStage, so the dictionary is inert. 
   = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
             -- Continue with rewritten Dictionary because we can only be in the 
             -- interactWithEqsStage, so the dictionary is inert. 

-       ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
+       ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList }

     
 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis }) 
            workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
   | wfl `canRewrite` ifl
   , tv `elemVarSet` tyVarsOfTypes xis
   = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
     
 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis }) 
            workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
   | wfl `canRewrite` ifl
   , tv `elemVarSet` tyVarsOfTypes xis
   = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)

-       ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
+       ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromCCan rewritten_dict) }

 
 -- Class constraint and given equality: use the equality to rewrite
 -- the class constraint.
 
 -- Class constraint and given equality: use the equality to rewrite
 -- the class constraint.

@@ -924,14 +973,14 @@ doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_r
   | ifl `canRewrite` wfl
   , tv `elemVarSet` tyVarsOfType ty 
   = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty) 
   | ifl `canRewrite` wfl
   , tv `elemVarSet` tyVarsOfType ty 
   = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty) 

-       ; mkIRContinue rewritten_ip KeepInert emptyWorkList } 
+       ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList } 

 
 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty }) 
            workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
   | wfl `canRewrite` ifl
   , tv `elemVarSet` tyVarsOfType ty
   = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty) 
 
 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty }) 
            workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
   | wfl `canRewrite` ifl
   , tv `elemVarSet` tyVarsOfType ty
   = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty) 

-       ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
+       ; mkIRContinue "IP/Eq" workItem DropInert (workListFromCCan rewritten_ip) }

 
 -- Two implicit parameter constraints.  If the names are the same,
 -- but their types are not, we generate a wanted type equality 
 
 -- Two implicit parameter constraints.  If the names are the same,
 -- but their types are not, we generate a wanted type equality 

@@ -944,7 +993,9 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i
   =    -- See Note [Overriding implicit parameters]
         -- Dump the inert item, override totally with the new one
        -- Do not require type equality
   =    -- See Note [Overriding implicit parameters]
         -- Dump the inert item, override totally with the new one
        -- Do not require type equality

-    mkIRContinue workItem DropInert emptyWorkList
+       -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
+       --              we must *override* the outer one with the inner one
+    mkIRContinue "IP/IP override" workItem DropInert emptyWorkList

 
   | nm1 == nm2 && ty1 `tcEqType` ty2 
   = solveOneFromTheOther (id1,ifl) workItem 
 
   | nm1 == nm2 && ty1 `tcEqType` ty2 
   = solveOneFromTheOther (id1,ifl) workItem 

@@ -954,9 +1005,7 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i
     do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation]
        ; let flav = Wanted (combineCtLoc ifl wfl) 
        ; cans <- mkCanonical flav co_var 
     do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation]
        ; let flav = Wanted (combineCtLoc ifl wfl) 
        ; cans <- mkCanonical flav co_var 

-       ; mkIRContinue workItem KeepInert cans }
-
-
+       ; mkIRContinue "IP/IP fundep" workItem KeepInert cans }

 
 -- Never rewrite a given with a wanted equality, and a type function
 -- equality can never rewrite an equality. We rewrite LHS *and* RHS 
 
 -- Never rewrite a given with a wanted equality, and a type function
 -- equality can never rewrite an equality. We rewrite LHS *and* RHS 

@@ -970,7 +1019,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_
   | ifl `canRewrite` wfl 
   , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
   = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2) 
   | ifl `canRewrite` wfl 
   , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
   = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2) 

-       ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) } 
+       ; mkIRStop "Eq/FunEq" (workListFromCCan rewritten_funeq) } 

          -- Must Stop here, because we may no longer be inert after the rewritting.
 
 -- Inert: function equality, work item: equality
          -- Must Stop here, because we may no longer be inert after the rewritting.
 
 -- Inert: function equality, work item: equality

@@ -980,7 +1029,7 @@ doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
   | wfl `canRewrite` ifl
   , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
   = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1) 
   | wfl `canRewrite` ifl
   , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
   = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1) 

-       ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) } 
+       ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromCCan rewritten_funeq) } 

          -- One may think that we could (KeepTransformedInert rewritten_funeq) 
          -- but that is wrong, because it may end up not being inert with respect 
          -- to future inerts. Example: 
          -- One may think that we could (KeepTransformedInert rewritten_funeq) 
          -- but that is wrong, because it may end up not being inert with respect 
          -- to future inerts. Example: 

@@ -996,10 +1045,10 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
                                , cc_tyargs = args2, cc_rhs = xi2 })
   | fl1 `canSolve` fl2 && lhss_match
   = do { cans <- rewriteEqLHS LeftComesFromInert  (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 
                                , cc_tyargs = args2, cc_rhs = xi2 })
   | fl1 `canSolve` fl2 && lhss_match
   = do { cans <- rewriteEqLHS LeftComesFromInert  (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 

-       ; mkIRStop KeepInert cans } 
+       ; mkIRStop "FunEq/FunEq" cans } 

   | fl2 `canSolve` fl1 && lhss_match
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 
   | fl2 `canSolve` fl1 && lhss_match
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 

-       ; mkIRContinue workItem DropInert cans }
+       ; mkIRContinue "FunEq/FunEq" workItem DropInert cans }

   where
     lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) 
 
   where
     lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) 
 

@@ -1008,30 +1057,32 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc
 -- Check for matching LHS 
   | fl1 `canSolve` fl2 && tv1 == tv2 
   = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 
 -- Check for matching LHS 
   | fl1 `canSolve` fl2 && tv1 == tv2 
   = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 

-       ; mkIRStop KeepInert cans } 
+       ; mkIRStop "Eq/Eq lhs" cans } 

 
   | fl2 `canSolve` fl1 && tv1 == tv2 
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 
 
   | fl2 `canSolve` fl1 && tv1 == tv2 
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 

-       ; mkIRContinue workItem DropInert cans }
+       ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
+

 -- Check for rewriting RHS 
   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2 
   = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2) 
 -- Check for rewriting RHS 
   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2 
   = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2) 

-       ; mkIRStop KeepInert rewritten_eq }
+       ; mkIRStop "Eq/Eq rhs" rewritten_eq }
+

   | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
   = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) 
   | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
   = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) 

-       ; mkIRContinue workItem DropInert rewritten_eq } 
+       ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq } 

 
 doInteractWithInert (CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
                     (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
 
 doInteractWithInert (CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
                     (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)

-       ; mkIRStop KeepInert rewritten_frozen }
+       ; mkIRStop "Frozen/Eq" rewritten_frozen }

 
 doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
            workItem@(CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
 
 doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
            workItem@(CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)

-       ; mkIRContinue workItem DropInert rewritten_frozen }
+       ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen }

 
 -- Fall-through case for all other situations
 doInteractWithInert _ workItem = noInteraction workItem
 
 -- Fall-through case for all other situations
 doInteractWithInert _ workItem = noInteraction workItem

@@ -1188,26 +1239,28 @@ rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
     co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b  -- ty2b ~ ty2b[xi1/tv1]
 
 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
     co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b  -- ty2b ~ ty2b[xi1/tv1]
 
 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult

--- First argument inert, second argument workitem. They both represent 
+-- First argument inert, second argument work-item. They both represent 

 -- wanted/given/derived evidence for the *same* predicate so we try here to 
 -- discharge one directly from the other. 
 --
 -- Precondition: value evidence only (implicit parameters, classes) 
 --               not coercion
 solveOneFromTheOther (iid,ifl) workItem
 -- wanted/given/derived evidence for the *same* predicate so we try here to 
 -- discharge one directly from the other. 
 --
 -- Precondition: value evidence only (implicit parameters, classes) 
 --               not coercion
 solveOneFromTheOther (iid,ifl) workItem

+  | isDerived wfl
+  = mkIRStop "Solved (derived)" emptyWorkList
+

   | ifl `canSolve` wfl
   = do { when (isWanted wfl) $ setEvBind wid (EvId iid)
            -- Overwrite the binding, if one exists
           -- For Givens, which are lambda-bound, nothing to overwrite,
   | ifl `canSolve` wfl
   = do { when (isWanted wfl) $ setEvBind wid (EvId iid)
            -- Overwrite the binding, if one exists
           -- For Givens, which are lambda-bound, nothing to overwrite,

-       ; dischargeWorkItem }
+       ; mkIRStop "Solved" emptyWorkList }
+

   | wfl `canSolve` ifl
   = do { when (isWanted ifl) $ setEvBind iid (EvId wid)
   | wfl `canSolve` ifl
   = do { when (isWanted ifl) $ setEvBind iid (EvId wid)

-       ; mkIRContinue workItem DropInert emptyWorkList }
+       ; mkIRContinue "Solved inert" workItem DropInert emptyWorkList }

 
 

-  | otherwise -- One of the two is Derived, we can just throw it away, 
-              -- preferrably the work item. 
-  = if isDerived wfl then dischargeWorkItem 
-    else mkIRContinue workItem DropInert emptyWorkList
+  | otherwise -- The inert item is Derived, we can just throw it away, 
+  = mkIRContinue "Discard derived inert" workItem DropInert emptyWorkList

   
   where 
      wfl = cc_flavor workItem
   
   where 
      wfl = cc_flavor workItem

@@ -1577,7 +1630,7 @@ data TopInteractResult
                                        -- arising from top-level instances.
 
 topReactionsStage :: SimplifierStage 
                                        -- arising from top-level instances.
 
 topReactionsStage :: SimplifierStage 

-topReactionsStage workItem inerts 
+topReactionsStage depth workItem inerts 

   = do { tir <- tryTopReact workItem 
        ; case tir of 
            NoTopInt -> 
   = do { tir <- tryTopReact workItem 
        ; case tir of 
            NoTopInt -> 

@@ -1585,10 +1638,14 @@ topReactionsStage workItem inerts
                            , sr_new_work = emptyWorkList 
                            , sr_stop     = ContinueWith workItem } 
            SomeTopInt tir_new_work tir_new_inert -> 
                            , sr_new_work = emptyWorkList 
                            , sr_stop     = ContinueWith workItem } 
            SomeTopInt tir_new_work tir_new_inert -> 

-               return $ SR { sr_inerts   = inerts 
-                           , sr_new_work = tir_new_work
-                           , sr_stop     = tir_new_inert
-                           }
+               do { bumpStepCountTcS
+                  ; traceFireTcS depth (ptext (sLit "Top react")
+                       <+> vcat [ ptext (sLit "Work =") <+> ppr workItem
+                                , ptext (sLit "New =") <+> ppr tir_new_work ])
+                  ; return $ SR { sr_inerts   = inerts 
+                               , sr_new_work = tir_new_work
+                               , sr_stop     = tir_new_inert
+                               } }

        }
 
 tryTopReact :: WorkItem -> TcS TopInteractResult 
        }
 
 tryTopReact :: WorkItem -> TcS TopInteractResult 

@@ -1618,47 +1675,69 @@ doTopReact (CDictCan { cc_flavor = Given {} })
   = return NoTopInt -- NB: Superclasses already added since it's canonical
 
 -- Derived dictionary: just look for functional dependencies
   = return NoTopInt -- NB: Superclasses already added since it's canonical
 
 -- Derived dictionary: just look for functional dependencies

-doTopReact workItem@(CDictCan { cc_flavor = Derived loc
+doTopReact workItem@(CDictCan { cc_flavor = fl@(Derived loc)

                               , cc_class = cls, cc_tyargs = xis })
                               , cc_class = cls, cc_tyargs = xis })

-  = do { fd_work <- findClassFunDeps cls xis loc
-       ; if isEmptyWorkList fd_work then 
-              return NoTopInt
-         else return $ SomeTopInt { tir_new_work = fd_work
-                                  , tir_new_inert = ContinueWith workItem } }
+  = do { instEnvs <- getInstEnvs
+       ; let fd_eqns = improveFromInstEnv instEnvs
+                                                (ClassP cls xis, pprArisingAt loc)
+       ; m <- rewriteWithFunDeps fd_eqns xis fl
+       ; case m of
+           Nothing -> return NoTopInt
+           Just (xis',_,fd_work) ->
+               let workItem' = workItem { cc_tyargs = xis' }
+                   -- Deriveds are not supposed to have identity (cc_id is unused!)
+               in return $ SomeTopInt { tir_new_work  = fd_work 
+                                      , tir_new_inert = ContinueWith workItem' } }
+

 -- Wanted dictionary
 -- Wanted dictionary

-doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
-                              , cc_class = cls, cc_tyargs = xis }) 
+doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
+                              , cc_class = cls, cc_tyargs = xis })

   = do { -- See Note [MATCHING-SYNONYMS]
        ; lkp_inst_res <- matchClassInst cls xis loc
   = do { -- See Note [MATCHING-SYNONYMS]
        ; lkp_inst_res <- matchClassInst cls xis loc

-       ; case lkp_inst_res of 
-           NoInstance -> 
-             do { traceTcS "doTopReact/ no class instance for" (ppr dv) 
-                ; fd_work <- findClassFunDeps cls xis loc
-                ; return $ SomeTopInt
-                              { tir_new_work  = fd_work
-                              , tir_new_inert = ContinueWith workItem } }
-
-           GenInst wtvs ev_term ->  -- Solved 
+       ; case lkp_inst_res of
+           NoInstance ->
+             do { traceTcS "doTopReact/ no class instance for" (ppr dv)
+
+                ; instEnvs <- getInstEnvs
+                ; let fd_eqns = improveFromInstEnv instEnvs
+                                                         (ClassP cls xis, pprArisingAt loc)
+                ; m <- rewriteWithFunDeps fd_eqns xis fl
+                ; case m of
+                    Nothing -> return NoTopInt
+                    Just (xis',cos,fd_work) ->
+                        do { let dict_co = mkTyConCoercion (classTyCon cls) cos
+                           ; dv'<- newDictVar cls xis'
+                           ; setDictBind dv (EvCast dv' dict_co)
+                           ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl, 
+                                                        cc_class = cls, cc_tyargs = xis' }
+                           ; return $ 
+                             SomeTopInt { tir_new_work  = singleCCan workItem' `andCCan` fd_work
+                                        , tir_new_inert = Stop } } }
+
+           GenInst wtvs ev_term -- Solved 

                   -- No need to do fundeps stuff here; the instance 
                   -- matches already so we won't get any more info
                   -- from functional dependencies
                   -- No need to do fundeps stuff here; the instance 
                   -- matches already so we won't get any more info
                   -- from functional dependencies

-               do { traceTcS "doTopReact/ found class instance for" (ppr dv) 
-                  ; setDictBind dv ev_term 
-                  ; inst_work <- canWanteds wtvs
-                  ; if null wtvs
+             | null wtvs
+             -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) 
+                   ; setDictBind dv ev_term 

                     -- Solved in one step and no new wanted work produced. 
                     -- i.e we directly matched a top-level instance
                     -- No point in caching this in 'inert'; hence Stop
                     -- Solved in one step and no new wanted work produced. 
                     -- i.e we directly matched a top-level instance
                     -- No point in caching this in 'inert'; hence Stop

-                    then return $ SomeTopInt { tir_new_work  = emptyWorkList 
-                                             , tir_new_inert = Stop }
-
-                    -- Solved and new wanted work produced, you may cache the 
-                   -- (tentatively solved) dictionary as Given! (used to be: Derived)
-                    else do { let solved = makeSolvedByInst workItem
-                            ; return $ SomeTopInt 
-                                  { tir_new_work  = inst_work
-                                  , tir_new_inert = ContinueWith solved } }
-       }          }
+                   ; return $ SomeTopInt { tir_new_work  = emptyWorkList 
+                                         , tir_new_inert = Stop } }
+
+             | otherwise
+             -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) 
+                   ; setDictBind dv ev_term 
+                        -- Solved and new wanted work produced, you may cache the 
+                        -- (tentatively solved) dictionary as Given! (used to be: Derived)
+                   ; let solved   = workItem { cc_flavor = given_fl }
+                         given_fl = Given (setCtLocOrigin loc UnkSkol) 
+                   ; inst_work <- canWanteds wtvs
+                   ; return $ SomeTopInt { tir_new_work  = inst_work
+                                         , tir_new_inert = ContinueWith solved } }
+       }          

 
 -- Type functions
 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
 
 -- Type functions
 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl

@@ -1694,20 +1773,6 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
 
 -- Any other work item does not react with any top-level equations
 doTopReact _workItem = return NoTopInt 
 
 -- Any other work item does not react with any top-level equations
 doTopReact _workItem = return NoTopInt 

-
-----------------------
-findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList
--- Look for a fundep reaction beween the wanted item 
--- and a top-level instance declaration
-findClassFunDeps cls xis loc
- = do { instEnvs <- getInstEnvs
-      ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
-                                               (ClassP cls xis, pprArisingAt loc)
-      ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs
-                     -- NB: fundeps generate some wanted equalities, but 
-                     --     we don't use their evidence for anything
-      ; cts <- mapM mkCanonicalFEV derived_evs
-      ; return $ unionManyBags cts }

 \end{code}
 
 
 \end{code}
 
 

diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 96ca3b3..f9422a8 100644 (file)
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -935,10 +935,9 @@ data CtFlavor
 -- superclasses. 
 
 instance Outputable CtFlavor where
 -- superclasses. 
 
 instance Outputable CtFlavor where

-  ppr (Given _)    = ptext (sLit "[Given]")
-  ppr (Wanted _)   = ptext (sLit "[Wanted]")
-  ppr (Derived {}) = ptext (sLit "[Derived]") 
-
+  ppr (Given {})   = ptext (sLit "[G]")
+  ppr (Wanted {})  = ptext (sLit "[W]")
+  ppr (Derived {}) = ptext (sLit "[D]") 

 pprFlavorArising :: CtFlavor -> SDoc
 pprFlavorArising (Derived wl )  = pprArisingAt wl
 pprFlavorArising (Wanted  wl)   = pprArisingAt wl
 pprFlavorArising :: CtFlavor -> SDoc
 pprFlavorArising (Derived wl )  = pprArisingAt wl
 pprFlavorArising (Wanted  wl)   = pprArisingAt wl

diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 8d5093d..ad24eb7 100644 (file)
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -10,7 +10,6 @@ module TcSMonad (
 
     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
     deCanonicalise, mkFrozenError,
 
     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
     deCanonicalise, mkFrozenError,

-    makeSolvedByInst,

 
     isWanted, isGiven, isDerived,
     isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
 
     isWanted, isGiven, isDerived,
     isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,

@@ -21,7 +20,8 @@ module TcSMonad (
     combineCtLoc, mkGivenFlavor, mkWantedFlavor,
     getWantedLoc,
 
     combineCtLoc, mkGivenFlavor, mkWantedFlavor,
     getWantedLoc,
 

-    TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0,  -- Basic functionality 
+    TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality 
+    traceFireTcS, bumpStepCountTcS,

     tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
 
     tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
 

@@ -45,7 +45,7 @@ module TcSMonad (
 
     instDFunTypes,                              -- Instantiation
     instDFunConstraints,          
 
     instDFunTypes,                              -- Instantiation
     instDFunConstraints,          

-    newFlexiTcSTy, 
+    newFlexiTcSTy, instFlexiTcS,

 
     compatKind,
 
 
     compatKind,
 

@@ -58,15 +58,11 @@ module TcSMonad (
     matchClass, matchFam, MatchInstResult (..), 
     checkWellStagedDFun, 
     warnTcS,
     matchClass, matchFam, MatchInstResult (..), 
     checkWellStagedDFun, 
     warnTcS,

-    pprEq,                                   -- Smaller utils, re-exported from TcM 
+    pprEq                                   -- Smaller utils, re-exported from TcM 

                                              -- TODO (DV): these are only really used in the 
                                              -- instance matcher in TcSimplify. I am wondering
                                              -- if the whole instance matcher simply belongs
                                              -- here 
                                              -- TODO (DV): these are only really used in the 
                                              -- instance matcher in TcSimplify. I am wondering
                                              -- if the whole instance matcher simply belongs
                                              -- here 

-
-
-    mkDerivedFunDepEqns                       -- Instantiation of 'Equations' from FunDeps
-

 ) where 
 
 #include "HsVersions.h"
 ) where 
 
 #include "HsVersions.h"

@@ -102,7 +98,6 @@ import FastString
 
 import HsBinds               -- for TcEvBinds stuff 
 import Id 
 
 import HsBinds               -- for TcEvBinds stuff 
 import Id 

-import FunDeps

 
 import TcRnTypes
 
 
 import TcRnTypes
 

@@ -180,16 +175,6 @@ mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
 compatKind :: Kind -> Kind -> Bool
 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
 
 compatKind :: Kind -> Kind -> Bool
 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
 

-makeSolvedByInst :: CanonicalCt -> CanonicalCt
--- Record that a constraint is now solved
---       Wanted         -> Given
---       Given, Derived -> no-op
-makeSolvedByInst ct 
-  | Wanted loc <- cc_flavor ct
-  = ct { cc_flavor = Given (setCtLocOrigin loc UnkSkol) }
-  | otherwise     -- Only called on wanteds
-  = pprPanic "makeSolvedByInst" (ppr ct)
-

 deCanonicalise :: CanonicalCt -> FlavoredEvVar
 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
 
 deCanonicalise :: CanonicalCt -> FlavoredEvVar
 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
 

@@ -367,7 +352,10 @@ data TcSEnv
 
       tcs_context :: SimplContext,
                      
 
       tcs_context :: SimplContext,
                      

-      tcs_untch :: TcsUntouchables
+      tcs_untch :: TcsUntouchables,
+
+      tcs_ic_depth :: Int,     -- Implication nesting depth
+      tcs_count    :: IORef Int        -- Global step count

     }
 
 type TcsUntouchables = (Untouchables,TcTyVarSet)
     }
 
 type TcsUntouchables = (Untouchables,TcTyVarSet)

@@ -443,8 +431,21 @@ panicTcS doc = pprPanic "TcCanonical" doc
 traceTcS :: String -> SDoc -> TcS ()
 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
 
 traceTcS :: String -> SDoc -> TcS ()
 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
 

-traceTcS0 :: String -> SDoc -> TcS ()
-traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
+bumpStepCountTcS :: TcS ()
+bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
+                                    ; n <- TcM.readTcRef ref
+                                    ; TcM.writeTcRef ref (n+1) }
+
+traceFireTcS :: Int -> SDoc -> TcS ()
+-- Dump a rule-firing trace
+traceFireTcS depth doc 
+  = TcS $ \env -> 
+    TcM.ifDOptM Opt_D_dump_cs_trace $ 
+    do { n <- TcM.readTcRef (tcs_count env)
+       ; let msg = int n 
+                <> text (replicate (tcs_ic_depth env) '>')
+                <> brackets (int depth) <+> doc
+       ; TcM.dumpTcRn msg }

 
 runTcS :: SimplContext
        -> Untouchables                -- Untouchables
 
 runTcS :: SimplContext
        -> Untouchables                -- Untouchables

@@ -453,10 +454,13 @@ runTcS :: SimplContext
 runTcS context untouch tcs 
   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
 runTcS context untouch tcs 
   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds

+       ; step_count <- TcM.newTcRef 0

        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                           , tcs_ty_binds = ty_binds_var
                           , tcs_context  = context
                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                           , tcs_ty_binds = ty_binds_var
                           , tcs_context  = context
                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet

+                         , tcs_count    = step_count
+                         , tcs_ic_depth = 0

                           }
 
             -- Run the computation
                           }
 
             -- Run the computation

@@ -465,6 +469,10 @@ runTcS context untouch tcs
        ; ty_binds <- TcM.readTcRef ty_binds_var
        ; mapM_ do_unification (varEnvElts ty_binds)
 
        ; ty_binds <- TcM.readTcRef ty_binds_var
        ; mapM_ do_unification (varEnvElts ty_binds)
 

+#ifdef DEBUG
+       ; count <- TcM.readTcRef step_count
+       ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count)
+#endif

              -- And return
        ; ev_binds      <- TcM.readTcRef evb_ref
        ; return (res, evBindMapBinds ev_binds) }
              -- And return
        ; ev_binds      <- TcM.readTcRef evb_ref
        ; return (res, evBindMapBinds ev_binds) }

@@ -472,13 +480,23 @@ runTcS context untouch tcs
     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
 
 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
 
 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a

-nestImplicTcS ref untch (TcS thing_inside)
-  = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, 
-                     tcs_context = ctxt } ->
+nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
+  = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds 
+                  , tcs_untch = (_outer_range, outer_tcs)
+                  , tcs_count = count
+                  , tcs_ic_depth = idepth
+                   , tcs_context = ctxt } ->

     let 
     let 

+       inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
+                          -- The inner_range should be narrower than the outer one
+                  -- (thus increasing the set of untouchables) but 
+                  -- the inner Tcs-untouchables must be unioned with the
+                  -- outer ones!

        nest_env = TcSEnv { tcs_ev_binds = ref
                          , tcs_ty_binds = ty_binds
        nest_env = TcSEnv { tcs_ev_binds = ref
                          , tcs_ty_binds = ty_binds

-                         , tcs_untch    = untch
+                         , tcs_untch    = inner_untch
+                         , tcs_count    = count
+                         , tcs_ic_depth = idepth+1

                          , tcs_context  = ctxtUnderImplic ctxt }
     in 
     thing_inside nest_env
                          , tcs_context  = ctxtUnderImplic ctxt }
     in 
     thing_inside nest_env

@@ -785,48 +803,4 @@ matchFam tycon args
        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
        -- multiple matches. Check. 
        }
        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
        -- multiple matches. Check. 
        }

-
-
--- Functional dependencies, instantiation of equations
--------------------------------------------------------
-
-mkDerivedFunDepEqns :: WantedLoc
-                   -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
-                   -> TcS [FlavoredEvVar]    -- All Derived
-mkDerivedFunDepEqns _   [] = return []
-mkDerivedFunDepEqns loc eqns
-  = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
-       ; evvars <- mapM to_work_item eqns
-       ; return $ concat evvars }
-  where
-    to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar]
-    to_work_item ((qtvs, pairs), d1, d2)
-      = do { let tvs = varSetElems qtvs
-           ; tvs' <- mapM instFlexiTcS tvs
-           ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
-                 loc'  = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
-                 flav  = Derived loc'
-           ; mapM (do_one subst flav) pairs }
-
-    do_one subst flav (ty1, ty2)
-       = do { let sty1 = substTy subst ty1
-                  sty2 = substTy subst ty2
-            ; ev <- newCoVar sty1 sty2
-            ; return (mkEvVarX ev flav) }
-
-pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
-pprEquationDoc (eqn, (p1, _), (p2, _)) 
-  = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
-
-mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
-         -> TcM (TidyEnv, SDoc)
-mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
-  = do  { pred1' <- TcM.zonkTcPredType pred1
-        ; pred2' <- TcM.zonkTcPredType pred2
-       ; let { pred1'' = tidyPred tidy_env pred1'
-              ; pred2'' = tidyPred tidy_env pred2' }
-       ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
-                         nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
-                         nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
-       ; return (tidy_env, msg) }

 \end{code}
 \end{code}

diff --git a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs
index 511472c..6ce932b 100644 (file)
--- a/compiler/types/FunDeps.lhs
+++ b/compiler/types/FunDeps.lhs
@@ -9,7 +9,8 @@ It's better to read it as: "if we know these, then we're going to know these"
 
 \begin{code}
 module FunDeps (
 
 \begin{code}
 module FunDeps (

-       Equation, pprEquation, 
+        FDEq (..),
+       Equation(..), pprEquation,

        oclose, improveFromInstEnv, improveFromAnother,
        checkInstCoverage, checkFunDeps,
        pprFundeps
        oclose, improveFromInstEnv, improveFromAnother,
        checkInstCoverage, checkFunDeps,
        pprFundeps

@@ -140,32 +141,67 @@ oclose preds fixed_tvs
 %************************************************************************
 
 
 %************************************************************************
 
 

+Each functional dependency with one variable in the RHS is responsible
+for generating a single equality. For instance:
+     class C a b | a -> b
+The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha 
+     FDEq { fd_pos      = 1
+          , fd_ty_left  = Bool 
+          , fd_ty_right = alpha }
+However notice that a functional dependency may have more than one variable
+in the RHS which will create more than one FDEq. Example: 
+     class C a b c | a -> b c 
+     [Wanted] C Int alpha alpha 
+     [Wanted] C Int Bool beta 
+Will generate: 
+        fd1 = FDEq { fd_pos = 1, fd_ty_left = alpha, fd_ty_right = Bool } and
+        fd2 = FDEq { fd_pos = 2, fd_ty_left = alpha, fd_ty_right = beta }
+
+We record the paremeter position so that can immediately rewrite a constraint
+using the produced FDEqs and remove it from our worklist.
+
+
+INVARIANT: Corresponding types aren't already equal 
+That is, there exists at least one non-identity equality in FDEqs. 
+
+Assume:
+       class C a b c | a -> b c
+       instance C Int x x
+And:   [Wanted] C Int Bool alpha
+We will /match/ the LHS of fundep equations, producing a matching substitution
+and create equations for the RHS sides. In our last example we'd have generated:
+      ({x}, [fd1,fd2])
+where 
+       fd1 = FDEq 1 Bool x
+       fd2 = FDEq 2 alpha x
+To ``execute'' the equation, make fresh type variable for each tyvar in the set,
+instantiate the two types with these fresh variables, and then unify or generate 
+a new constraint. In the above example we would generate a new unification 
+variable 'beta' for x and produce the following constraints:
+     [Wanted] (Bool ~ beta)
+     [Wanted] (alpha ~ beta)
+
+Notice the subtle difference between the above class declaration and:
+       class C a b c | a -> b, a -> c 
+where we would generate: 
+      ({x},[fd1]),({x},[fd2]) 
+This means that the template variable would be instantiated to different 
+unification variables when producing the FD constraints. 
+
+Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
+

 \begin{code}
 \begin{code}

-type Equation = (TyVarSet, [(Type, Type)])
--- These pairs of types should be equal, for some
--- substitution of the tyvars in the tyvar set
--- INVARIANT: corresponding types aren't already equal
-
--- It's important that we have a *list* of pairs of types.  Consider
---     class C a b c | a -> b c where ...
---     instance C Int x x where ...
--- Then, given the constraint (C Int Bool v) we should improve v to Bool,
--- via the equation ({x}, [(Bool,x), (v,x)])
--- This would not happen if the class had looked like
---     class C a b c | a -> b, a -> c
-
--- To "execute" the equation, make fresh type variable for each tyvar in the set,
--- instantiate the two types with these fresh variables, and then unify.
---
--- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
--- We unify z with Int, but since a and b are quantified we do nothing to them
--- We usually act on an equation by instantiating the quantified type varaibles
--- to fresh type variables, and then calling the standard unifier.
+type Pred_Loc = (PredType, SDoc)       -- SDoc says where the Pred comes from

 
 

-pprEquation :: Equation -> SDoc
-pprEquation (qtvs, pairs) 
-  = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
-         nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (t1,t2) <- pairs])]
+data Equation 
+   = FDEqn { fd_qtvs :: TyVarSet               -- Instantiate these to fresh unification vars
+           , fd_eqs  :: [FDEq]                 --   and then make these equal
+           , fd_pred1, fd_pred2 :: Pred_Loc }  -- The Equation arose from
+                                               -- combining these two constraints
+
+data FDEq = FDEq { fd_pos      :: Int -- We use '0' for the first position
+                 , fd_ty_left  :: Type
+                 , fd_ty_right :: Type }

 \end{code}
 
 Given a bunch of predicates that must hold, such as
 \end{code}
 
 Given a bunch of predicates that must hold, such as

@@ -198,93 +234,97 @@ NOTA BENE:
 
 
 \begin{code}
 
 
 \begin{code}

-type Pred_Loc = (PredType, SDoc)       -- SDoc says where the Pred comes from
+instFD_WithPos :: FunDep TyVar -> [TyVar] -> [Type] -> ([Type], [(Int,Type)]) 
+-- Returns a FunDep between the types accompanied along with their 
+-- position (<=0) in the types argument list.
+instFD_WithPos (ls,rs) tvs tys
+  = (map (snd . lookup) ls, map lookup rs)
+  where
+    ind_tys   = zip [0..] tys 
+    env       = zipVarEnv tvs ind_tys
+    lookup tv = lookupVarEnv_NF env tv

 
 

-improveFromInstEnv :: (Class -> [Instance]) 
-                     -> Pred_Loc 
-                     -> [(Equation,Pred_Loc,Pred_Loc)]
--- Improvement from top-level instances 
-improveFromInstEnv _inst_env pred 
-  = improveOne _inst_env pred []        -- TODO: Refactor to directly use instance_eqnd? 
+zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
+                   -> [Type] 
+                   -> [(Int,Type)] 
+                   -> [FDEq]
+-- Create a list of FDEqs from two lists of types, making sure
+-- that the types are not equal.
+zipAndComputeFDEqs discard (ty1:tys1) ((i2,ty2):tys2)
+ | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
+ | otherwise = FDEq { fd_pos      = i2
+                    , fd_ty_left  = ty1
+                    , fd_ty_right = ty2 } : zipAndComputeFDEqs discard tys1 tys2
+zipAndComputeFDEqs _ _ _ = [] 
+
+-- Improve a class constraint from another class constraint
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+improveFromAnother :: Pred_Loc -- Template item (usually given, or inert) 
+                   -> Pred_Loc -- Workitem [that can be improved]
+                   -> [Equation]
+-- Post: FDEqs always oriented from the other to the workitem 
+--       Equations have empty quantified variables 
+improveFromAnother pred1@(ClassP cls1 tys1, _) pred2@(ClassP cls2 tys2, _)
+  | tys1 `lengthAtLeast` 2 && cls1 == cls2
+  = [ FDEqn { fd_qtvs = emptyVarSet, fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 }
+    | let (cls_tvs, cls_fds) = classTvsFds cls1
+    , fd <- cls_fds
+    , let (ltys1, rs1)  = instFD         fd cls_tvs tys1
+          (ltys2, irs2) = instFD_WithPos fd cls_tvs tys2
+    , tcEqTypes ltys1 ltys2            -- The LHSs match
+    , let eqs = zipAndComputeFDEqs tcEqType rs1 irs2
+    , not (null eqs) ]
+
+improveFromAnother _ _ = []
+
+
+-- Improve a class constraint from instance declarations
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 
 

+pprEquation :: Equation -> SDoc
+pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs }) 
+  = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
+         nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]

 
 

-improveFromAnother :: Pred_Loc
+improveFromInstEnv :: (InstEnv,InstEnv)

                    -> Pred_Loc
                    -> Pred_Loc

-                   -> [(Equation, Pred_Loc, Pred_Loc)]
--- Improvement from another local (given or wanted) constraint
-improveFromAnother pred1 pred2 
-  = improveOne (\_ -> []) pred1 [pred2] -- TODO: Refactor to directly use pairwise_eqns?
-
-
-improveOne :: (Class -> [Instance])            -- Gives instances for given class
-          -> Pred_Loc                          -- Do improvement triggered by this
-          -> [Pred_Loc]                        -- Current constraints 
-          -> [(Equation,Pred_Loc,Pred_Loc)]    -- Derived equalities that must also hold
-                                               -- (NB the above INVARIANT for type Equation)
-                                               -- The Pred_Locs explain which two predicates were
-                                               -- combined (for error messages)
--- Just do improvement triggered by a single, distinguised predicate
-
-improveOne _inst_env pred@(IParam ip ty, _) preds
-  = [ ((emptyVarSet, [(ty,ty2)]), pred, p2) 
-    | p2@(IParam ip2 ty2, _) <- preds
-    , ip==ip2
-    , not (ty `tcEqType` ty2)]
-
-improveOne inst_env pred@(ClassP cls tys, _) preds
+                   -> [Equation] -- Needs to be an Equation because
+                                 -- of quantified variables
+-- Post: Equations oriented from the template (matching instance) to the workitem!
+improveFromInstEnv _inst_env (pred,_loc)
+  | not (isClassPred pred)
+  = panic "improveFromInstEnv: not a class predicate"
+improveFromInstEnv inst_env pred@(ClassP cls tys, _)

   | tys `lengthAtLeast` 2
   | tys `lengthAtLeast` 2

-  = instance_eqns ++ pairwise_eqns
-       -- NB: we put the instance equations first.   This biases the 
-       -- order so that we first improve individual constraints against the
-       -- instances (which are perhaps in a library and less likely to be
-       -- wrong; and THEN perform the pairwise checks.
-       -- The other way round, it's possible for the pairwise check to succeed
-       -- and cause a subsequent, misleading failure of one of the pair with an
-       -- instance declaration.  See tcfail143.hs for an example
-  where
-    (cls_tvs, cls_fds) = classTvsFds cls
-    instances         = inst_env cls
-    rough_tcs         = roughMatchTcs tys
-
-       -- NOTE that we iterate over the fds first; they are typically
-       -- empty, which aborts the rest of the loop.
-    pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
-    pairwise_eqns      -- This group comes from pairwise comparison
-      = [ (eqn, pred, p2)
-       | fd <- cls_fds
-       , p2@(ClassP cls2 tys2, _) <- preds
-       , cls == cls2
-       , eqn <- checkClsFD emptyVarSet fd cls_tvs tys tys2
-       ]
-
-    instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
-    instance_eqns      -- This group comes from comparing with instance decls
-      = [ (eqn, p_inst, pred)
-       | fd <- cls_fds         -- Iterate through the fundeps first, 
+  = [ FDEqn { fd_qtvs = qtvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred }
+    | fd <- cls_fds            -- Iterate through the fundeps first,

                                -- because there often are none!
                                -- because there often are none!

-       , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
+    , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs

                -- Trim the rough_tcs based on the head of the fundep.
                -- Remember that instanceCantMatch treats both argumnents
                -- symmetrically, so it's ok to trim the rough_tcs,
                -- rather than trimming each inst_tcs in turn
                -- Trim the rough_tcs based on the head of the fundep.
                -- Remember that instanceCantMatch treats both argumnents
                -- symmetrically, so it's ok to trim the rough_tcs,
                -- rather than trimming each inst_tcs in turn

-       , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst, 
-                           is_tcs = inst_tcs }) <- instances
-       , not (instanceCantMatch inst_tcs trimmed_tcs)
-       , eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys
-       , let p_inst = (mkClassPred cls tys_inst, 
-                       sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)
-                           , ptext (sLit "in the instance declaration at") 
-                                 <+> ppr (getSrcLoc ispec)])
-       ]
-
-improveOne _ _ _
-  = []
+    , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
+                       is_tcs = inst_tcs }) <- instances
+    , not (instanceCantMatch inst_tcs trimmed_tcs)
+    , let p_inst = (mkClassPred cls tys_inst,
+                   sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)  
+                       , ptext (sLit "in the instance declaration at")
+                                   <+> ppr (getSrcLoc ispec)])
+    , (qtvs, eqs) <- checkClsFD qtvs fd cls_tvs tys_inst tys -- NB: orientation
+    , not (null eqs)
+    ]
+  where 
+     (cls_tvs, cls_fds) = classTvsFds cls
+     instances          = classInstances inst_env cls
+     rough_tcs          = roughMatchTcs tys
+improveFromInstEnv _ _ = []

 
 
 checkClsFD :: TyVarSet                         -- Quantified type variables; see note below
           -> FunDep TyVar -> [TyVar]   -- One functional dependency from the class
           -> [Type] -> [Type]
 
 
 checkClsFD :: TyVarSet                         -- Quantified type variables; see note below
           -> FunDep TyVar -> [TyVar]   -- One functional dependency from the class
           -> [Type] -> [Type]

-          -> [Equation]
+          -> [(TyVarSet, [FDEq])]

 
 checkClsFD qtvs fd clas_tvs tys1 tys2
 -- 'qtvs' are the quantified type variables, the ones which an be instantiated 
 
 checkClsFD qtvs fd clas_tvs tys1 tys2
 -- 'qtvs' are the quantified type variables, the ones which an be instantiated 

@@ -313,52 +353,69 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
             length tys1 == length clas_tvs 
            , ppr tys1 <+> ppr tys2 )
 
             length tys1 == length clas_tvs 
            , ppr tys1 <+> ppr tys2 )
 

-    case tcUnifyTys bind_fn ls1 ls2 of
+    case tcUnifyTys bind_fn ltys1 ltys2 of

        Nothing  -> []
        Nothing  -> []

-       Just subst | isJust (tcUnifyTys bind_fn rs1' rs2') 
-                       -- Don't include any equations that already hold. 
+       Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
+                       -- Don't include any equations that already hold.

                        -- Reason: then we know if any actual improvement has happened,
                        --         in which case we need to iterate the solver
                        -- Reason: then we know if any actual improvement has happened,
                        --         in which case we need to iterate the solver

-                       -- In making this check we must taking account of the fact that any 
-                       -- qtvs that aren't already instantiated can be instantiated to anything 
+                       -- In making this check we must taking account of the fact that any
+                       -- qtvs that aren't already instantiated can be instantiated to anything

                        -- at all
                        -- at all

-                 -> []
-
-                 | otherwise   -- Aha!  A useful equation
-                 -> [ (qtvs', zip rs1' rs2')]
+                        -- NB: We can't do this 'is-useful-equation' check element-wise 
+                        --     because of:
+                        --           class C a b c | a -> b c
+                        --           instance C Int x x
+                        --           [Wanted] C Int alpha Int
+                        -- We would get that  x -> alpha  (isJust) and x -> Int (isJust)
+                        -- so we would produce no FDs, which is clearly wrong. 
+                  -> [] 
+
+                  | otherwise
+                  -> [(qtvs', fdeqs)]

                        -- We could avoid this substTy stuff by producing the eqn
                        -- (qtvs, ls1++rs1, ls2++rs2)
                        -- which will re-do the ls1/ls2 unification when the equation is
                        -- executed.  What we're doing instead is recording the partial
                        -- work of the ls1/ls2 unification leaving a smaller unification problem
                        -- We could avoid this substTy stuff by producing the eqn
                        -- (qtvs, ls1++rs1, ls2++rs2)
                        -- which will re-do the ls1/ls2 unification when the equation is
                        -- executed.  What we're doing instead is recording the partial
                        -- work of the ls1/ls2 unification leaving a smaller unification problem

-                 where
-                   rs1'  = substTys subst rs1 
-                   rs2'  = substTys subst rs2
+                 where
+                    rtys1' = map (substTy subst) rtys1
+                    irs2'  = map (\(i,x) -> (i,substTy subst x)) irs2
+                    rtys2' = map snd irs2'
+ 
+                    fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
+                        -- Don't discard anything! 
+                        -- We could discard equal types but it's an overkill to call 
+                        -- tcEqType again, since we know for sure that /at least one/ 
+                        -- equation in there is useful)
+

                    qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
                    qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs

-                       -- qtvs' are the quantified type variables
-                       -- that have not been substituted out
-                       --      
-                       -- Eg.  class C a b | a -> b
-                       --      instance C Int [y]
-                       -- Given constraint C Int z
-                       -- we generate the equation
-                       --      ({y}, [y], z)
+                       -- qtvs' are the quantified type variables
+                       -- that have not been substituted out
+                       --      
+                       -- Eg.  class C a b | a -> b
+                       --      instance C Int [y]
+                       -- Given constraint C Int z
+                       -- we generate the equation
+                       --      ({y}, [y], z)

   where
     bind_fn tv | tv `elemVarSet` qtvs = BindMe
               | otherwise            = Skolem
 
   where
     bind_fn tv | tv `elemVarSet` qtvs = BindMe
               | otherwise            = Skolem
 

-    (ls1, rs1) = instFD fd clas_tvs tys1
-    (ls2, rs2) = instFD fd clas_tvs tys2
+    (ltys1, rtys1) = instFD         fd clas_tvs tys1
+    (ltys2, irs2)  = instFD_WithPos fd clas_tvs tys2
+\end{code}
+

 
 

+\begin{code}

 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type

+-- A simpler version of instFD_WithPos to be used in checking instance coverage etc.

 instFD (ls,rs) tvs tys
   = (map lookup ls, map lookup rs)
   where
     env       = zipVarEnv tvs tys
     lookup tv = lookupVarEnv_NF env tv
 instFD (ls,rs) tvs tys
   = (map lookup ls, map lookup rs)
   where
     env       = zipVarEnv tvs tys
     lookup tv = lookupVarEnv_NF env tv

-\end{code}

 
 

-\begin{code}

 checkInstCoverage :: Class -> [Type] -> Bool
 -- Check that the Coverage Condition is obeyed in an instance decl
 -- For example, if we have 
 checkInstCoverage :: Class -> [Type] -> Bool
 -- Check that the Coverage Condition is obeyed in an instance decl
 -- For example, if we have