Yet another major refactoring of the constraint solver
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 7 May 2012 16:40:34 +0000 (17:40 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 7 May 2012 16:40:34 +0000 (17:40 +0100)
This is the result of Simon and Dimitrios doing a code walk through.
There is no change in behaviour, but the structure is much better.
Main changes:

* Given constraints contain an EvTerm not an EvVar

* Correspondingly, TcEvidence is a recursive types that uses
  EvTerms rather than EvVars

* Rename CtFlavor to CtEvidence

* Every CtEvidence has a ctev_pred field.  And use record fields
  consistently for CtEvidence

* The solved-constraint fields of InertSet (namely inert_solved and
  inert_solved_funeqs) contain CtEvidence, not Ct

There is a long cascade of follow-on changes.

16 files changed:
compiler/coreSyn/CoreUtils.lhs
compiler/deSugar/DsBinds.lhs
compiler/typecheck/Inst.lhs
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcEvidence.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcUnify.lhs
compiler/types/Coercion.lhs
compiler/types/Type.lhs

index 8ec132f..7858b20 100644 (file)
@@ -187,15 +187,7 @@ mkCast (Coercion e_co) co
        -- The guard here checks that g has a (~#) on both sides,
        -- otherwise decomposeCo fails.  Can in principle happen
        -- with unsafeCoerce
-  = Coercion new_co
-  where
-       -- g :: (s1 ~# s2) ~# (t1 ~#  t2)
-       -- g1 :: s1 ~# t1
-       -- g2 :: s2 ~# t2
-       new_co = mkSymCo g1 `mkTransCo` e_co `mkTransCo` g2
-       [_reflk, g1, g2] = decomposeCo 3 co
-            -- Remember, (~#) :: forall k. k -> k -> *
-            -- so it takes *three* arguments, not two
+  = Coercion (mkCoCast e_co co)
 
 mkCast (Cast expr co2) co
   = ASSERT(let { Pair  from_ty  _to_ty  = coercionKind co;
index 8fc6bd9..9dd95cd 100644 (file)
@@ -726,39 +726,51 @@ sccEvBinds bs = stronglyConnCompFromEdgedVertices edges
     edges = foldrBag ((:) . mk_node) [] bs 
 
     mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
-    mk_node b@(EvBind var term) = (b, var, evVarsOfTerm term)
+    mk_node b@(EvBind var term) = (b, var, varSetElems (evVarsOfTerm term))
 
 
 ---------------------------------------
 dsEvTerm :: MonadThings m => EvTerm -> m CoreExpr
 dsEvTerm (EvId v) = return (Var v)
 
-dsEvTerm (EvCast v co) 
-  = return $ dsTcCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is
-                                     -- unnecessary to call varToCoreExpr v here.
+dsEvTerm (EvCast tm co) 
+  = do { tm' <- dsEvTerm tm
+       ; return $ dsTcCoercion co $ mkCast tm' }
+                        -- 'v' is always a lifted evidence variable so it is
+                        -- unnecessary to call varToCoreExpr v here.
+
 dsEvTerm (EvKindCast v co)
-  = return $ dsTcCoercion co $ (\_ -> Var v)
+  = do { v' <- dsEvTerm v
+       ; return $ dsTcCoercion co $ (\_ -> v') }
 
-dsEvTerm (EvDFunApp df tys vars) = return (Var df `mkTyApps` tys `mkVarApps` vars)
+dsEvTerm (EvDFunApp df tys tms) = do { tms' <- mapM dsEvTerm tms
+                                     ; return (Var df `mkTyApps` tys `mkApps` tms') }
 dsEvTerm (EvCoercion co)         = return $ dsTcCoercion co mkEqBox
 dsEvTerm (EvTupleSel v n)
-   = ASSERT( isTupleTyCon tc )
-     return $
-     Case (Var v) (mkWildValBinder (varType v)) (tys !! n) [(DataAlt dc, xs, Var v')]
-  where
-    (tc, tys) = splitTyConApp (evVarPred v)
-    Just [dc] = tyConDataCons_maybe tc
-    v' = v `setVarType` ty_want
-    xs = map mkWildValBinder tys_before ++ v' : map mkWildValBinder tys_after
-    (tys_before, ty_want:tys_after) = splitAt n tys
-dsEvTerm (EvTupleMk vs) = return $ Var (dataConWorkId dc) `mkTyApps` tys `mkVarApps` vs
-  where dc = tupleCon ConstraintTuple (length vs)
-        tys = map varType vs
+   = do { tm' <- dsEvTerm v
+        ; let scrut_ty = exprType tm'
+              (tc, tys) = splitTyConApp scrut_ty
+             Just [dc] = tyConDataCons_maybe tc
+             xs = mkTemplateLocals tys
+              the_x = xs !! n
+        ; ASSERT( isTupleTyCon tc )
+          return $
+          Case tm' (mkWildValBinder scrut_ty) (idType the_x) [(DataAlt dc, xs, Var the_x)] }
+
+dsEvTerm (EvTupleMk tms) 
+  = do { tms' <- mapM dsEvTerm tms
+       ; let tys = map exprType tms'
+       ; return $ Var (dataConWorkId dc) `mkTyApps` tys `mkApps` tms' }
+  where 
+    dc = tupleCon ConstraintTuple (length tms)
+
 dsEvTerm (EvSuperClass d n)
-  = return $ Var sc_sel_id `mkTyApps` tys `App` Var d
+  = do { d' <- dsEvTerm d
+       ; let (cls, tys) = getClassPredTys (exprType d')
+             sc_sel_id  = classSCSelId cls n   -- Zero-indexed
+       ; return $ Var sc_sel_id `mkTyApps` tys `App` d' }
   where
-    sc_sel_id  = classSCSelId cls n    -- Zero-indexed
-    (cls, tys) = getClassPredTys (evVarPred d)   
+
 dsEvTerm (EvDelayedError ty msg) = return $ Var errorId `mkTyApps` [ty] `mkApps` [litMsg]
   where 
     errorId = rUNTIME_ERROR_ID
@@ -816,6 +828,7 @@ ds_tc_coercion subst tc_co
     go (TcNthCo n co)         = mkNthCo n (go co)
     go (TcInstCo co ty)       = mkInstCo (go co) ty
     go (TcLetCo bs co)        = ds_tc_coercion (ds_co_binds bs) co
+    go (TcCastCo co1 co2)     = mkCoCast (go co1) (go co2)
     go (TcCoVarCo v)          = ds_ev_id subst v
 
     ds_co_binds :: TcEvBinds -> CvSubst
index d8ba828..0b4364b 100644 (file)
@@ -83,10 +83,11 @@ emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
 emitWanteds origin theta = mapM (emitWanted origin) theta
 
 emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
-emitWanted origin pred = do { loc <- getCtLoc origin
-                            ; ev  <- newWantedEvVar pred
-                            ; emitFlat (mkNonCanonical (Wanted loc ev))
-                            ; return ev }
+emitWanted origin pred 
+  = do { loc <- getCtLoc origin
+       ; ev  <- newWantedEvVar pred
+       ; emitFlat (mkNonCanonical (Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev }))
+       ; return ev }
 
 newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
 -- Used when Name is the wired-in name for a wired-in class method,
@@ -530,7 +531,7 @@ tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
 tyVarsOfCt (CDictCan { cc_tyargs = tys })              = tyVarsOfTypes tys
 tyVarsOfCt (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
 tyVarsOfCt (CIrredEvCan { cc_ty = ty })                 = tyVarsOfType ty
-tyVarsOfCt (CNonCanonical { cc_flavor = fl })           = tyVarsOfType (ctFlavPred fl)
+tyVarsOfCt (CNonCanonical { cc_ev = fl })           = tyVarsOfType (ctEvPred fl)
 
 tyVarsOfCDict :: Ct -> TcTyVarSet 
 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
@@ -564,24 +565,22 @@ tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
 ---------------- Tidying -------------------------
 
 tidyCt :: TidyEnv -> Ct -> Ct
+-- Used only in error reporting
 -- Also converts it to non-canonical
 tidyCt env ct 
-  = CNonCanonical { cc_flavor = tidy_flavor env (cc_flavor ct)
+  = CNonCanonical { cc_ev = tidy_flavor env (cc_ev ct)
                   , cc_depth  = cc_depth ct } 
-  where tidy_flavor :: TidyEnv -> CtFlavor -> CtFlavor
-        tidy_flavor env (Given { flav_gloc = gloc, flav_evar = evar })
-          = Given { flav_gloc = tidyGivenLoc env gloc
-                  , flav_evar = tidyEvVar env evar }
-        tidy_flavor env (Solved { flav_gloc = gloc
-                                , flav_evar = evar }) 
-          = Solved { flav_gloc  = tidyGivenLoc env gloc
-                   , flav_evar = tidyEvVar env evar }
-        tidy_flavor env (Wanted { flav_wloc = wloc
-                                , flav_evar = evar })
-          = Wanted { flav_wloc = wloc -- Interesting: no tidying needed?
-                   , flav_evar = tidyEvVar env evar }
-        tidy_flavor env (Derived { flav_wloc = wloc, flav_der_pty = pty })
-          = Derived { flav_wloc = wloc, flav_der_pty = tidyType env pty }
+  where 
+    tidy_flavor :: TidyEnv -> CtEvidence -> CtEvidence
+     -- NB: we do not tidy the ctev_evtm/var field because we don't 
+     --     show it in error messages
+    tidy_flavor env ctev@(Given { ctev_gloc = gloc, ctev_pred = pred })
+      = ctev { ctev_gloc = tidyGivenLoc env gloc
+             , ctev_pred = tidyType env pred }
+    tidy_flavor env ctev@(Wanted { ctev_pred = pred })
+      = ctev { ctev_pred = tidyType env pred }
+    tidy_flavor env ctev@(Derived { ctev_pred = pred })
+      = ctev { ctev_pred = tidyType env pred }
 
 tidyEvVar :: TidyEnv -> EvVar -> EvVar
 tidyEvVar env var = setVarType var (tidyType env (varType var))
@@ -604,6 +603,10 @@ tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
 tidySkolemInfo _   info            = info
 
 ---------------- Substitution -------------------------
+-- This is used only in TcSimpify, for substituations that are *also* 
+-- reflected in the unification variables.  So we don't substitute
+-- in the evidence.
+
 substCt :: TvSubst -> Ct -> Ct 
 -- Conservatively converts it to non-canonical:
 -- Postcondition: if the constraint does not get rewritten
@@ -611,9 +614,9 @@ substCt subst ct
   | pty <- ctPred ct
   , sty <- substTy subst pty 
   = if sty `eqType` pty then 
-        ct { cc_flavor = substFlavor subst (cc_flavor ct) }
+        ct { cc_ev = substFlavor subst (cc_ev ct) }
     else 
-        CNonCanonical { cc_flavor = substFlavor subst (cc_flavor ct)
+        CNonCanonical { cc_ev = substFlavor subst (cc_ev ct)
                       , cc_depth  = cc_depth ct }
 
 substWC :: TvSubst -> WantedConstraints -> WantedConstraints
@@ -637,21 +640,16 @@ substImplication subst implic@(Implic { ic_skols = tvs
 substEvVar :: TvSubst -> EvVar -> EvVar
 substEvVar subst var = setVarType var (substTy subst (varType var))
 
-substFlavor :: TvSubst -> CtFlavor -> CtFlavor
-substFlavor subst (Given { flav_gloc = gloc, flav_evar = evar })
-  = Given { flav_gloc = substGivenLoc subst gloc
-          , flav_evar = substEvVar subst evar }
-substFlavor subst (Solved { flav_gloc = gloc, flav_evar = evar })
-  = Solved { flav_gloc = substGivenLoc subst gloc
-           , flav_evar = substEvVar subst evar }
-
-substFlavor subst (Wanted { flav_wloc = wloc, flav_evar = evar })
-  = Wanted { flav_wloc  = wloc
-           , flav_evar = substEvVar subst evar }
-
-substFlavor subst (Derived { flav_wloc = wloc, flav_der_pty = pty })
-  = Derived { flav_wloc = wloc
-            , flav_der_pty = substTy subst pty }
+substFlavor :: TvSubst -> CtEvidence -> CtEvidence
+substFlavor subst ctev@(Given { ctev_gloc = gloc, ctev_pred = pred })
+  = ctev { ctev_gloc = substGivenLoc subst gloc
+          , ctev_pred = substTy subst pred }
+
+substFlavor subst ctev@(Wanted { ctev_pred = pred })
+  = ctev  { ctev_pred = substTy subst pred }
+
+substFlavor subst ctev@(Derived { ctev_pred = pty })
+  = ctev { ctev_pred = substTy subst pty }
 
 substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
 substGivenLoc subst (CtLoc skol span ctxt) 
index d293f0e..2e87c9e 100644 (file)
@@ -173,26 +173,26 @@ EvBinds, so we are again good.
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 canonicalize :: Ct -> TcS StopOrContinue
-canonicalize ct@(CNonCanonical { cc_flavor = fl, cc_depth  = d })
+canonicalize ct@(CNonCanonical { cc_ev = fl, cc_depth  = d })
   = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
        ; {-# SCC "canEvVar" #-}
          canEvVar d fl (classifyPredType (ctPred ct)) }
 
 canonicalize (CDictCan { cc_depth  = d
-                       , cc_flavor = fl
+                       , cc_ev = fl
                        , cc_class  = cls
                        , cc_tyargs = xis })
   = {-# SCC "canClass" #-}
     canClass d fl cls xis -- Do not add any superclasses
 canonicalize (CTyEqCan { cc_depth  = d
-                       , cc_flavor = fl
+                       , cc_ev = fl
                        , cc_tyvar  = tv
                        , cc_rhs    = xi })
   = {-# SCC "canEqLeafTyVarLeftRec" #-}
     canEqLeafTyVarLeftRec d fl tv xi
 
 canonicalize (CFunEqCan { cc_depth = d
-                        , cc_flavor = fl
+                        , cc_ev = fl
                         , cc_fun    = fn
                         , cc_tyargs = xis1
                         , cc_rhs    = xi2 })
@@ -200,18 +200,18 @@ canonicalize (CFunEqCan { cc_depth = d
     canEqLeafFunEqLeftRec d fl (fn,xis1) xi2
 
 canonicalize (CIPCan { cc_depth = d
-                     , cc_flavor = fl
+                     , cc_ev = fl
                      , cc_ip_nm  = nm
                      , cc_ip_ty  = xi })
   = canIP d fl nm xi
-canonicalize (CIrredEvCan { cc_flavor = fl
+canonicalize (CIrredEvCan { cc_ev = fl
                           , cc_depth = d
                           , cc_ty = xi })
   = canIrred d fl xi
 
 
 canEvVar :: SubGoalDepth 
-         -> CtFlavor 
+         -> CtEvidence 
          -> PredTree 
          -> TcS StopOrContinue
 -- Called only for non-canonical EvVars 
@@ -233,15 +233,16 @@ canEvVar d fl pred_classifier
 
 \begin{code}
 canTuple :: SubGoalDepth -- Depth 
-         -> CtFlavor -> [PredType] -> TcS StopOrContinue
+         -> CtEvidence -> [PredType] -> TcS StopOrContinue
 canTuple d fl tys
   = do { traceTcS "can_pred" (text "TuplePred!")
        ; let xcomp = EvTupleMk
              xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]             
-       ; xCtFlavor fl tys (XEvTerm xcomp xdecomp) what_next }
-  where what_next fls  = mapM_ add_to_work fls >> return Stop
-        add_to_work fl = addToWork $ canEvVar d fl (classifyPredType (ctFlavPred fl))
-        
+       ; ctevs <- xCtFlavor fl tys (XEvTerm xcomp xdecomp)
+       ; mapM_ add_to_work ctevs
+       ; return Stop }
+  where
+    add_to_work fl = addToWork $ canEvVar d fl (classifyPredType (ctEvPred fl))
 \end{code}
 
 
@@ -253,7 +254,7 @@ canTuple d fl tys
 
 \begin{code}
 canIP :: SubGoalDepth -- Depth 
-      -> CtFlavor
+      -> CtEvidence
       -> IPName Name -> Type -> TcS StopOrContinue
 -- Precondition: EvVar is implicit parameter evidence
 canIP d fl nm ty
@@ -264,7 +265,7 @@ canIP d fl nm ty
        ; mb <- rewriteCtFlavor fl xi co 
        ; case mb of
             Just new_fl -> let IPPred _ xi_in = classifyPredType xi
-                           in continueWith $ CIPCan { cc_flavor = new_fl
+                           in continueWith $ CIPCan { cc_ev = new_fl
                                                     , cc_ip_nm = nm, cc_ip_ty = xi_in
                                                     , cc_depth = d }
             Nothing -> return Stop }
@@ -291,7 +292,7 @@ flattened in the first place to facilitate comparing them.)
 \begin{code}
 canClass, canClassNC 
    :: SubGoalDepth -- Depth
-   -> CtFlavor  
+   -> CtEvidence  
    -> Class -> [Type] -> TcS StopOrContinue
 -- Precondition: EvVar is class evidence 
 
@@ -314,14 +315,14 @@ canClass d fl cls tys
 
        ; case mb of
            Just new_fl -> 
-             let (ClassPred cls xis_for_dict) = classifyPredType (ctFlavPred new_fl)
+             let (ClassPred cls xis_for_dict) = classifyPredType (ctEvPred new_fl)
              in continueWith $ 
-                CDictCan { cc_flavor = new_fl
+                CDictCan { cc_ev = new_fl
                          , cc_tyargs = xis_for_dict, cc_class = cls, cc_depth = d }
            Nothing -> return Stop }
 
 emitSuperclasses :: Ct -> TcS StopOrContinue
-emitSuperclasses ct@(CDictCan { cc_depth = d, cc_flavor = fl
+emitSuperclasses ct@(CDictCan { cc_depth = d, cc_ev = fl
                               , cc_tyargs = xis_new, cc_class = cls })
             -- Add superclasses of this one here, See Note [Adding superclasses]. 
             -- But only if we are not simplifying the LHS of a rule. 
@@ -399,20 +400,19 @@ happen.
 \begin{code}
 
 newSCWorkFromFlavored :: SubGoalDepth -- Depth
-                      -> CtFlavor -> Class -> [Xi] -> TcS ()
+                      -> CtEvidence -> Class -> [Xi] -> TcS ()
 -- Returns superclasses, see Note [Adding superclasses]
 newSCWorkFromFlavored d flavor cls xis 
   | isDerived flavor 
   = return ()  -- Deriveds don't yield more superclasses because we will
                -- add them transitively in the case of wanteds. 
-  | isSolved flavor
-  = return ()
     
   | isGiven flavor 
   = do { let sc_theta = immSuperClasses cls xis 
              xev = XEvTerm { ev_comp = panic "Can't compose for given!" 
-                           , ev_decomp = \x->zipWith (\_ i->EvSuperClass x i) sc_theta [0..] }
-       ; xCtFlavor flavor sc_theta xev (emit_sc_flavs d) }
+                           , ev_decomp = \x -> zipWith (\_ i -> EvSuperClass x i) sc_theta [0..] }
+       ; ctevs <- xCtFlavor flavor sc_theta xev
+       ; emit_sc_flavs d ctevs }
 
   | isEmptyVarSet (tyVarsOfTypes xis)
   = return () -- Wanteds/Derived with no variables yield no deriveds.
@@ -422,15 +422,17 @@ newSCWorkFromFlavored d flavor cls xis
   = do { let sc_rec_theta = transSuperClasses cls xis 
              impr_theta   = filter is_improvement_pty sc_rec_theta              
              xev = panic "Derived's are not supposed to transform evidence!" 
-       ; xCtFlavor (Derived (flav_wloc flavor) (ctFlavPred flavor)) impr_theta xev $ 
-         emit_sc_flavs d }
+             der_ev = Derived { ctev_wloc = ctev_wloc flavor, ctev_pred = ctev_pred flavor }
+       ; ctevs <- xCtFlavor der_ev impr_theta xev
+       ; emit_sc_flavs d ctevs }
 
-emit_sc_flavs :: SubGoalDepth -> [CtFlavor] -> TcS ()
+emit_sc_flavs :: SubGoalDepth -> [CtEvidence] -> TcS ()
 emit_sc_flavs d fls 
   = do { traceTcS "newSCWorkFromFlavored" $
          text "Emitting superclass work:" <+> ppr sc_cts
        ; updWorkListTcS $ appendWorkListCt sc_cts }
-  where sc_cts = map (\fl -> CNonCanonical { cc_flavor = fl, cc_depth  = d }) fls
+  where 
+    sc_cts = map (\fl -> CNonCanonical { cc_ev = fl, cc_depth  = d }) fls
 
 is_improvement_pty :: PredType -> Bool 
 -- Either it's an equality, or has some functional dependency
@@ -454,7 +456,7 @@ is_improvement_pty ty = go (classifyPredType ty)
 
 \begin{code}
 canIrred :: SubGoalDepth -- Depth
-         -> CtFlavor -> TcType -> TcS StopOrContinue
+         -> CtEvidence -> TcType -> TcS StopOrContinue
 -- Precondition: ty not a tuple and no other evidence form
 canIrred d fl ty 
   = do { traceTcS "can_pred" (text "IrredPred = " <+> ppr ty) 
@@ -468,9 +470,9 @@ canIrred d fl ty
              Just new_fl 
                | no_flattening
                  -> continueWith $
-                    CIrredEvCan { cc_flavor = new_fl, cc_ty = xi, cc_depth = d }
+                    CIrredEvCan { cc_ev = new_fl, cc_ty = xi, cc_depth = d }
                | otherwise
-                 -> canEvVar d new_fl (classifyPredType (ctFlavPred new_fl))
+                 -> canEvVar d new_fl (classifyPredType (ctEvPred new_fl))
              Nothing -> return Stop }
 
 \end{code}
@@ -529,7 +531,7 @@ data FlattenMode = FMSubstOnly
 -- Flatten a bunch of types all at once.
 flattenMany :: SubGoalDepth -- Depth
             -> FlattenMode
-            -> CtFlavor -> [Type] -> TcS ([Xi], [TcCoercion])
+            -> CtEvidence -> [Type] -> TcS ([Xi], [TcCoercion])
 -- Coercions :: Xi ~ Type 
 -- Returns True iff (no flattening happened)
 -- NB: The EvVar inside the flavor is unused, we merely want Given/Solved/Derived/Wanted info
@@ -546,7 +548,7 @@ flattenMany d f ctxt tys
 -- constraints.  See Note [Flattening] for more detail.
 flatten :: SubGoalDepth -- Depth
         -> FlattenMode 
-        -> CtFlavor -> TcType -> TcS (Xi, TcCoercion)
+        -> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
 -- Postcondition: Coercion :: Xi ~ TcType
 flatten d f ctxt ty 
   | Just ty' <- tcView ty
@@ -595,7 +597,8 @@ flatten d f fl (TyConApp tc tys)
                  do { flat_cache <- getFlatCache
                     ; case lookupTM fam_ty flat_cache of
                         Just ct 
-                          | cc_flavor ct `canRewrite` fl 
+                          | let ctev = cc_ev ct
+                          , ctev `canRewrite` fl 
                           -> -- You may think that we can just return (cc_rhs ct) but not so. 
                              --            return (mkTcCoVarCo (ctId ct), cc_rhs ct, []) 
                              -- The cached constraint resides in the cache so we have to flatten 
@@ -606,42 +609,42 @@ flatten d f fl (TyConApp tc tys)
                              -- For now I say we don't keep it fully rewritten.
                             do { traceTcS "flatten/flat-cache hit" $ ppr ct
                                ; let rhs_xi = cc_rhs ct
-                               ; (flat_rhs_xi,co) <- flatten (cc_depth ct) f (cc_flavor ct) rhs_xi
-                               ; let final_co = mkTcCoVarCo (ctId ct) `mkTcTransCo` (mkTcSymCo co)
+                               ; (flat_rhs_xi,co) <- flatten (cc_depth ct) f ctev rhs_xi
+                               ; let final_co = evTermCoercion (ctEvTerm ctev)
+                                                `mkTcTransCo` mkTcSymCo co
                                ; return (final_co, flat_rhs_xi,[]) }
                           
-                        _ | isGivenOrSolved fl -- Given or Solved: make new flatten skolem
+                        _ | isGiven fl -- Given: make new flatten skolem
                           -> do { traceTcS "flatten/flat-cache miss" $ empty 
                                 ; rhs_xi_var <- newFlattenSkolemTy fam_ty
-                                ; mg <- newGivenEvVar (mkTcEqPred fam_ty rhs_xi_var) 
-                                                      (EvCoercion (mkTcReflCo fam_ty)) 
-                                ; case mg of 
-                                   Fresh eqv -> 
-                                     do { let new_fl = Given (flav_gloc fl) eqv
-                                              ct = CFunEqCan { cc_flavor = new_fl
-                                                             , cc_fun    = tc 
-                                                             , cc_tyargs = xi_args 
-                                                             , cc_rhs    = rhs_xi_var 
-                                                             , cc_depth  = d }
-                                              -- Update the flat cache
-                                        ; updFlatCache ct
-                                        ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
-                                   Cached {} -> panic "flatten TyConApp, var must be fresh!" }
+                                ; let co = mkTcReflCo fam_ty
+                                      new_fl = Given { ctev_gloc = ctev_gloc fl
+                                                     , ctev_pred = mkTcEqPred fam_ty rhs_xi_var
+                                                     , ctev_evtm = EvCoercion co }
+                                      ct = CFunEqCan { cc_ev = new_fl
+                                                     , cc_fun    = tc 
+                                                     , cc_tyargs = xi_args 
+                                                     , cc_rhs    = rhs_xi_var 
+                                                     , cc_depth  = d }
+                                      -- Update the flat cache
+                                ; updFlatCache ct
+                                ; return (co, rhs_xi_var, [ct]) }
                          | otherwise -- Wanted or Derived: make new unification variable
                          -> do { traceTcS "flatten/flat-cache miss" $ empty 
                                ; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
-                               ; mw <- newWantedEvVar (mkTcEqPred fam_ty rhs_xi_var)
+                               ; let pred = mkTcEqPred fam_ty rhs_xi_var
+                                     wloc = ctev_wloc fl
+                               ; mw <- newWantedEvVar wloc pred
                                ; case mw of
-                                   Fresh eqv -> 
-                                     do { let new_fl = Wanted (flav_wloc fl) eqv
-                                              ct = CFunEqCan { cc_flavor = new_fl
+                                   Fresh ctev -> 
+                                     do { let ct = CFunEqCan { cc_ev = ctev
                                                              , cc_fun = tc
                                                              , cc_tyargs = xi_args
                                                              , cc_rhs    = rhs_xi_var 
                                                              , cc_depth  = d }
                                           -- Update the flat cache: just an optimisation!
                                         ; updFlatCache ct
-                                        ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
+                                        ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var, [ct]) }
                                    Cached {} -> panic "flatten TyConApp, var must be fresh!" } 
                     }
                   -- Emit the flat constraints
@@ -691,7 +694,7 @@ flatten d _f ctxt ty@(ForAllTy {})
 \begin{code}
 flattenTyVar :: SubGoalDepth 
              -> FlattenMode 
-             -> CtFlavor -> TcTyVar -> TcS (Xi, TcCoercion)
+             -> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion)
 -- "Flattening" a type variable means to apply the substitution to it
 flattenTyVar d f ctxt tv
   = do { ieqs <- getInertEqs
@@ -709,13 +712,15 @@ flattenTyVar d f ctxt tv
            Just (co,ty) -> 
                do { (ty_final,co') <- flatten d f ctxt ty
                   ; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } }  
-  where tv_eq_subst subst tv
-          | Just ct <- lookupVarEnv subst tv
-          , cc_flavor ct `canRewrite` ctxt
-          = Just (mkTcCoVarCo (ctId ct),cc_rhs ct)
-                 -- NB: even if ct is Derived we are not going to 
-                 -- touch the actual coercion so we are fine. 
-          | otherwise = Nothing
+  where 
+    tv_eq_subst subst tv
+       | Just ct <- lookupVarEnv subst tv
+       , let ctev = cc_ev ct
+       , ctev `canRewrite` ctxt
+       = Just (evTermCoercion (ctEvTerm ctev), cc_rhs ct)
+              -- NB: even if ct is Derived we are not going to 
+              -- touch the actual coercion so we are fine. 
+       | otherwise = Nothing
 \end{code}
 
 Note [Non-idempotent inert substitution]
@@ -765,13 +770,13 @@ addToWork tcs_action = tcs_action >>= stop_or_emit
 
 \begin{code}
 canEqEvVarsCreated :: SubGoalDepth
-                   -> [CtFlavor] -> TcS StopOrContinue
+                   -> [CtEvidence] -> TcS StopOrContinue
 canEqEvVarsCreated _d [] = return Stop
 canEqEvVarsCreated d (quad:quads) 
   = mapM_ (addToWork . do_quad) quads >> do_quad quad
            -- Add all but one to the work list
            -- and return the first (if any) for futher processing
-  where do_quad fl = let EqPred ty1 ty2 = classifyPredType $ ctFlavPred fl
+  where do_quad fl = let EqPred ty1 ty2 = classifyPredType $ ctEvPred fl
                      in canEqNC d fl ty1 ty2
           -- Note the "NC": these are fresh equalities so we must be
           -- careful to add their kind constraints
@@ -779,7 +784,7 @@ canEqEvVarsCreated d (quad:quads)
 -------------------------
 canEqNC, canEq 
   :: SubGoalDepth 
-  -> CtFlavor 
+  -> CtEvidence 
   -> Type -> Type -> TcS StopOrContinue
 
 canEqNC d fl ty1 ty2
@@ -790,7 +795,7 @@ canEq _d fl ty1 ty2
   | eqType ty1 ty2     -- Dealing with equality here avoids
                        -- later spurious occurs checks for a~a
   = if isWanted fl then
-      setEvBind (flav_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop
+      setEvBind (ctev_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop
     else
       return Stop
 
@@ -823,11 +828,11 @@ canEq d fl ty1 ty2
     -- Fail straight away for better error messages
     then canEqFailure d fl
     else
-      let xcomp xs  = EvCoercion (mkTcTyConAppCo tc1 (map mkTcCoVarCo xs))
-          xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (mkTcCoVarCo x)) tys1 [0..]
-          xev = XEvTerm xcomp xdecomp
-      in xCtFlavor fl (zipWith mkTcEqPred tys1 tys2) xev (canEqEvVarsCreated d)
-         
+    do { let xcomp xs  = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs))
+             xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
+             xev = XEvTerm xcomp xdecomp
+       ; ctevs <- xCtFlavor fl (zipWith mkTcEqPred tys1 tys2) xev
+       ; canEqEvVarsCreated d ctevs }
 
 -- See Note [Equality between type applications]
 --     Note [Care with type applications] in TcUnify
@@ -839,7 +844,7 @@ canEq d fl ty1 ty2    -- e.g.  F a b ~ Maybe c
 
 canEq d fl s1@(ForAllTy {}) s2@(ForAllTy {})
  | tcIsForAllTy s1, tcIsForAllTy s2
- , Wanted loc orig_ev <- fl 
+ , Wanted { ctev_wloc = loc, ctev_evar = orig_ev } <- fl 
  = do { let (tvs1,body1) = tcSplitForAllTys s1
             (tvs2,body2) = tcSplitForAllTys s2
       ; if not (equalLength tvs1 tvs2) then 
@@ -857,12 +862,12 @@ canEq d fl _ _  = canEqFailure d fl
 ------------------------
 -- Type application
 canEqAppTy :: SubGoalDepth 
-           -> CtFlavor 
+           -> CtEvidence 
            -> Type -> Type -> Type -> Type
            -> TcS StopOrContinue
 canEqAppTy d fl s1 t1 s2 t2
   = ASSERT( not (isKind t1) && not (isKind t2) )
-    if isGivenOrSolved fl then 
+    if isGiven fl then 
         do { traceTcS "canEq (app case)" $
                 text "Ommitting decomposition of given equality between: " 
                     <+> ppr (AppTy s1 t1) <+> text "and" <+> ppr (AppTy s2 t2)
@@ -870,14 +875,14 @@ canEqAppTy d fl s1 t1 s2 t2
                    -- because we no longer have 'left' and 'right'
            ; return Stop }
     else 
-      let xevcomp [x,y] = EvCoercion (mkTcAppCo (mkTcCoVarCo x) (mkTcCoVarCo y))
-          xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
-          xev = XEvTerm { ev_comp = xevcomp
-                        , ev_decomp = error "canEqAppTy: can't happen" }
-      in xCtFlavor fl [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev $
-         canEqEvVarsCreated d
-
-canEqFailure :: SubGoalDepth -> CtFlavor -> TcS StopOrContinue
+    do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
+             xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
+             xev = XEvTerm { ev_comp = xevcomp
+                           , ev_decomp = error "canEqAppTy: can't happen" }
+       ; ctevs <- xCtFlavor fl [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev 
+       ; canEqEvVarsCreated d ctevs }
+
+canEqFailure :: SubGoalDepth -> CtEvidence -> TcS StopOrContinue
 canEqFailure d fl = emitFrozenError fl d >> return Stop
 
 ------------------------
@@ -885,12 +890,12 @@ emitKindConstraint :: Ct -> TcS StopOrContinue
 emitKindConstraint ct
   = case ct of 
       CTyEqCan { cc_depth = d
-               , cc_flavor = fl, cc_tyvar = tv
+               , cc_ev = fl, cc_tyvar = tv
                , cc_rhs = ty }
           -> emit_kind_constraint d fl (mkTyVarTy tv) ty
 
       CFunEqCan { cc_depth = d
-                , cc_flavor = fl
+                , cc_ev = fl
                 , cc_fun = fn, cc_tyargs = xis1
                 , cc_rhs = xi2 }
           -> emit_kind_constraint d fl (mkTyConApp fn xis1) xi2
@@ -904,41 +909,43 @@ emitKindConstraint ct
        | otherwise
        = ASSERT( isKind k1 && isKind k2 )
          do { kev <- 
-                 do { mw <- newWantedEvVar (mkEqPred k1 k2) 
+                 do { mw <- newWantedEvVar kind_co_wloc (mkEqPred k1 k2) 
                     ; case mw of
-                         Cached x -> return x
-                         Fresh x  -> addToWork (canEq d (kind_co_fl x) k1 k2) >> return x }
-            ; let xcomp [x] = mkEvKindCast x (mkTcCoVarCo kev)
+                         Cached ev_tm -> return ev_tm
+                         Fresh ctev   -> do { addToWork (canEq d ctev k1 k2) 
+                                            ; return (ctEvTerm ctev) } }
+
+            ; let xcomp [x] = mkEvKindCast x (evTermCoercion kev)
                   xcomp _   = panic "emit_kind_constraint:can't happen"
-                  xdecomp x = [mkEvKindCast x (mkTcCoVarCo kev)]
+                  xdecomp x = [mkEvKindCast x (evTermCoercion kev)]
                   xev = XEvTerm xcomp xdecomp
-              in xCtFlavor_cache False fl [mkTcEqPred ty1 ty2] xev what_next }
+
+            ; ctevs <- xCtFlavor_cache False fl [mkTcEqPred ty1 ty2] xev 
                      -- Important: Do not cache original as Solved since we are supposed to 
                      -- solve /exactly/ the same constraint later! Example:
                      -- (alpha :: kappa0) 
                      -- (T :: *)
                      -- Equality is: (alpha ~ T), so we will emitConstraint (kappa0 ~ *) but
                      -- we don't want to say that (alpha ~ T) is now Solved!
-       where 
-         what_next [new_fl] = continueWith (ct { cc_flavor = new_fl }) 
-         what_next _ = return Stop
 
+            ; case ctevs of
+                []         -> return Stop
+                [new_ctev] -> continueWith (ct { cc_ev = new_ctev }) 
+                _          -> panic "emitKindConstraint" }
+       where
          k1 = typeKind ty1
          k2 = typeKind ty2
          ctxt = mkKindErrorCtxtTcS ty1 k1 ty2 k2
+
          -- Always create a Wanted kind equality even if 
          -- you are decomposing a given constraint.
          -- NB: DV finds this reasonable for now. Maybe we have to revisit.
-         kind_co_fl x 
-           | isGivenOrSolved fl
-           = let (CtLoc _sk_info src_span err_ctxt) = flav_gloc fl
-                 orig = TypeEqOrigin (UnifyOrigin ty1 ty2)
-                 ctloc = pushErrCtxtSameOrigin ctxt $
-                         CtLoc orig src_span err_ctxt
-             in Wanted ctloc x
-           | otherwise 
-           = Wanted (pushErrCtxtSameOrigin ctxt (flav_wloc fl)) x
-             
+         kind_co_wloc = pushErrCtxtSameOrigin ctxt wanted_loc
+         wanted_loc = case fl of
+                         Wanted  { ctev_wloc = wloc } -> wloc
+                         Derived { ctev_wloc = wloc } -> wloc
+                         Given { ctev_gloc = gloc }   -> setCtLocOrigin gloc orig
+         orig = TypeEqOrigin (UnifyOrigin ty1 ty2)
 \end{code}
 
 Note [Combining insoluble constraints]
@@ -1106,7 +1113,7 @@ classify ty                | Just ty' <- tcView ty
                            = OtherCls ty
 
 -- See note [Canonical ordering for equality constraints].
-reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool       
+reOrient :: CtEvidence -> TypeClassifier -> TypeClassifier -> Bool     
 -- (t1 `reOrient` t2) responds True 
 --   iff we should flip to (t2~t1)
 -- We try to say False if possible, to minimise evidence generation
@@ -1143,7 +1150,7 @@ reOrient _fl (FskCls {}) (OtherCls {})   = False
 ------------------
 
 canEqLeaf :: SubGoalDepth -- Depth
-          -> CtFlavor 
+          -> CtEvidence 
           -> Type -> Type 
           -> TcS StopOrContinue
 -- Canonicalizing "leaf" equality constraints which cannot be
@@ -1156,13 +1163,16 @@ canEqLeaf :: SubGoalDepth -- Depth
 canEqLeaf d fl s1 s2 
   | cls1 `re_orient` cls2
   = do { traceTcS "canEqLeaf (reorienting)" $ ppr fl <+> dcolon <+> pprEq s1 s2
-       ; let xcomp [x] = EvCoercion (mkTcSymCo (mkTcCoVarCo x))
+       ; let xcomp [x] = EvCoercion (mkTcSymCo (evTermCoercion x))
              xcomp _ = panic "canEqLeaf: can't happen"
-             xdecomp x = [EvCoercion (mkTcSymCo (mkTcCoVarCo x))]
+             xdecomp x = [EvCoercion (mkTcSymCo (evTermCoercion x))]
              xev = XEvTerm xcomp xdecomp
-             what_next [fl] = canEqLeafOriented d fl s2 s1
-             what_next _ = return Stop
-       ; xCtFlavor fl [mkTcEqPred s2 s1] xev what_next }
+       ; ctevs <- xCtFlavor fl [mkTcEqPred s2 s1] xev 
+       ; case ctevs of
+           []     -> return Stop
+           [ctev] -> canEqLeafOriented d ctev s2 s1
+           _      -> panic "canEqLeaf" }
+
   | otherwise
   = do { traceTcS "canEqLeaf" $ ppr (mkTcEqPred s1 s2)
        ; canEqLeafOriented d fl s1 s2 }
@@ -1172,7 +1182,7 @@ canEqLeaf d fl s1 s2
     cls2 = classify s2
 
 canEqLeafOriented :: SubGoalDepth -- Depth
-                  -> CtFlavor
+                  -> CtEvidence
                   -> TcType -> TcType -> TcS StopOrContinue
 -- By now s1 will either be a variable or a type family application
 canEqLeafOriented d fl s1 s2
@@ -1184,10 +1194,10 @@ canEqLeafOriented d fl s1 s2
           = canEqLeafTyVarLeftRec d fl tv s2
           | otherwise
           = pprPanic "canEqLeafOriented" $
-            text "Non-variable or non-family equality LHS" <+> ppr (ctFlavPred fl)
+            text "Non-variable or non-family equality LHS" <+> ppr (ctEvPred fl)
 
 canEqLeafFunEqLeftRec :: SubGoalDepth
-                      -> CtFlavor
+                      -> CtEvidence
                       -> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
 canEqLeafFunEqLeftRec d fl (fn,tys1) ty2  -- fl :: F tys1 ~ ty2
   = do { traceTcS "canEqLeafFunEqLeftRec" $ pprEq (mkTyConApp fn tys1) ty2
@@ -1210,7 +1220,7 @@ canEqLeafFunEqLeftRec d fl (fn,tys1) ty2  -- fl :: F tys1 ~ ty2
 
 
 canEqLeafFunEqLeft :: SubGoalDepth -- Depth
-                   -> CtFlavor
+                   -> CtEvidence
                    -> (TyCon,[Xi])
                    -> TcType -> TcS StopOrContinue
 -- Precondition: No more flattening is needed for the LHS
@@ -1232,12 +1242,12 @@ canEqLeafFunEqLeft d fl (fn,xis1) s2
       ; case mb of
           Nothing -> return Stop
           Just new_fl -> continueWith $ 
-                         CFunEqCan { cc_flavor = new_fl, cc_depth = d
+                         CFunEqCan { cc_ev = new_fl, cc_depth = d
                                    , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } }   
 
 
 canEqLeafTyVarLeftRec :: SubGoalDepth
-                      -> CtFlavor
+                      -> CtEvidence
                       -> TcTyVar -> TcType -> TcS StopOrContinue
 canEqLeafTyVarLeftRec d fl tv s2              -- fl :: tv ~ s2
   = do {  traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2
@@ -1262,7 +1272,7 @@ canEqLeafTyVarLeftRec d fl tv s2              -- fl :: tv ~ s2
                Nothing  -> canEq d new_fl xi1 s2 }
     
 canEqLeafTyVarLeft :: SubGoalDepth -- Depth
-                   -> CtFlavor 
+                   -> CtEvidence 
                    -> TcTyVar -> TcType -> TcS StopOrContinue
 -- Precondition LHS is fully rewritten from inerts (but not RHS)
 canEqLeafTyVarLeft d fl tv s2       -- eqv : tv ~ s2
@@ -1276,7 +1286,7 @@ canEqLeafTyVarLeft d fl tv s2       -- eqv : tv ~ s2
 
        -- Reflexivity exposed through flattening        
        ; if tv_ty `eqType` xi2 then
-           when (isWanted fl) (setEvBind (flav_evar fl) (EvCoercion co2)) >> 
+           when (isWanted fl) (setEvBind (ctev_evar fl) (EvCoercion co2)) >> 
            return Stop
          else do
        -- Not reflexivity but maybe an occurs error
@@ -1291,7 +1301,7 @@ canEqLeafTyVarLeft d fl tv s2       -- eqv : tv ~ s2
        ; case mb of
            Just new_fl -> if not_occ_err then 
                             continueWith $
-                            CTyEqCan { cc_flavor = new_fl, cc_depth = d
+                            CTyEqCan { cc_ev = new_fl, cc_depth = d
                                      , cc_tyvar  = tv, cc_rhs    = xi2' }
                           else
                             canEqFailure d new_fl
@@ -1307,7 +1317,7 @@ canEqLeafTyVarLeft d fl tv s2       -- eqv : tv ~ s2
 -- variable, then the same type is returned.
 --
 -- Precondition: the two types are not equal (looking though synonyms)
-canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi)
+canOccursCheck :: CtEvidence -> TcTyVar -> Xi -> TcS (Maybe Xi)
 canOccursCheck _gw tv xi = return (expandAway tv xi)
 \end{code}
 
index 020d42c..483de07 100644 (file)
@@ -158,17 +158,15 @@ reportTidyWanteds ctxt insols flats implics
 deferToRuntime :: EvBindsVar -> ReportErrCtxt -> (ReportErrCtxt -> Ct -> TcM ErrMsg) 
                -> Ct -> TcM ()
 deferToRuntime ev_binds_var ctxt mk_err_msg ct 
-  | fl <- cc_flavor ct
-  , Wanted loc _ <- fl
+  | Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev_id } <- cc_ev ct
   = do { err <- setCtLoc loc $
                 mk_err_msg ctxt ct
-       ; let ev_id   = ctId ct -- Prec satisfied: Wanted
-             err_msg = pprLocErrMsg err
+       ; let err_msg = pprLocErrMsg err
              err_fs  = mkFastString $ showSDoc $ 
                        err_msg $$ text "(deferred type error)"
 
          -- Create the binding
-       ; addTcEvBind ev_binds_var ev_id (EvDelayedError (idType ev_id) err_fs)
+       ; addTcEvBind ev_binds_var ev_id (EvDelayedError pred err_fs)
 
          -- And emit a warning
        ; reportWarning (makeIntoWarning err) }
@@ -231,7 +229,7 @@ type Reporter = [Ct] -> TcM ()
 
 mkReporter :: (Ct -> TcM ErrMsg) -> [Ct] -> TcM ()
 -- Reports errors one at a time
-mkReporter mk_err = mapM_ (\ct -> do { err <- setCtFlavorLoc (cc_flavor ct) $
+mkReporter mk_err = mapM_ (\ct -> do { err <- setCtFlavorLoc (cc_ev ct) $
                                               mk_err ct; 
                                      ; reportError err })
 
@@ -316,15 +314,15 @@ groupErrs mk_err (ct1 : rest)
         ; reportError err
         ; groupErrs mk_err others }
   where
-   flavor            = cc_flavor ct1
+   flavor            = cc_ev ct1
    cts               = ct1 : friends
    (friends, others) = partition is_friend rest
-   is_friend friend  = cc_flavor friend `same_group` flavor
+   is_friend friend  = cc_ev friend `same_group` flavor
 
-   same_group :: CtFlavor -> CtFlavor -> Bool
-   same_group (Given l1 _) (Given l2 _) = same_loc l1 l2
-   same_group (Derived l1 _) (Derived l2 _) = same_loc l1 l2
-   same_group (Wanted l1 _)  (Wanted l2 _)  = same_loc l1 l2
+   same_group :: CtEvidence -> CtEvidence -> Bool
+   same_group (Given   {ctev_gloc = l1}) (Given   {ctev_gloc = l2}) = same_loc l1 l2
+   same_group (Wanted  {ctev_wloc = l1}) (Wanted  {ctev_wloc = l2}) = same_loc l1 l2
+   same_group (Derived {ctev_wloc = l1}) (Derived {ctev_wloc = l2}) = same_loc l1 l2
    same_group _ _ = False
 
    same_loc :: CtLoc o -> CtLoc o -> Bool
@@ -425,7 +423,7 @@ mkEqErr _ [] = panic "mkEqErr"
 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
 -- Wanted constraints only!
 mkEqErr1 ctxt ct
-  = if isGivenOrSolved flav then 
+  = if isGiven flav then 
       let ctx2 = ctxt { cec_extra = cec_extra ctxt $$ inaccessible_msg flav }
       in mkEqErr_help ctx2 ct False ty1 ty2
     else
@@ -434,10 +432,11 @@ mkEqErr1 ctxt ct
          ; mk_err ctxt1 orig' }
   where
 
-    flav = cc_flavor ct
+    flav = cc_ev ct
 
-    inaccessible_msg (Given loc _) = hang (ptext (sLit "Inaccessible code in"))
-                                        2 (ppr (ctLocOrigin loc))
+    inaccessible_msg (Given { ctev_gloc = loc }) 
+       = hang (ptext (sLit "Inaccessible code in"))
+            2 (ppr (ctLocOrigin loc))
     -- If a Solved then we should not report inaccessible code
     inaccessible_msg _ = empty
 
@@ -571,7 +570,7 @@ misMatchOrCND :: ReportErrCtxt -> Ct -> Bool -> TcType -> TcType -> SDoc
 misMatchOrCND ctxt ct oriented ty1 ty2
   | null givens || 
     (isRigid ty1 && isRigid ty2) || 
-    isGivenOrSolved (cc_flavor ct)
+    isGiven (cc_ev ct)
        -- If the equality is unconditionally insoluble
        -- or there is no context, don't report the context
   = misMatchMsg oriented ty1 ty2
@@ -1066,7 +1065,7 @@ solverDepthErrorTcS depth stack
   | null stack     -- Shouldn't happen unless you say -fcontext-stack=0
   = failWith msg
   | otherwise
-  = setCtFlavorLoc (cc_flavor top_item) $
+  = setCtFlavorLoc (cc_ev top_item) $
     do { zstack <- mapM zonkCt stack
        ; env0 <- tcInitTidyEnv
        ; let zstack_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet zstack
@@ -1079,7 +1078,7 @@ solverDepthErrorTcS depth stack
                , ptext (sLit "Use -fcontext-stack=N to increase stack size to N") ]
 
 {- DV: Changing this because Derived's no longer have ids ... Kind of a corner case ...
-  = setCtFlavorLoc (cc_flavor top_item) $
+  = setCtFlavorLoc (cc_ev top_item) $
     do { ev_vars <- mapM (zonkEvVar . cc_id) stack
        ; env0 <- tcInitTidyEnv
        ; let tidy_env = tidyFreeTyVars env0 (tyVarsOfEvVars ev_vars)
@@ -1092,7 +1091,7 @@ solverDepthErrorTcS depth stack
 -}
 
 
-flattenForAllErrorTcS :: CtFlavor -> TcType -> TcM a
+flattenForAllErrorTcS :: CtEvidence -> TcType -> TcM a
 flattenForAllErrorTcS fl ty
   = setCtFlavorLoc fl $ 
     do { env0 <- tcInitTidyEnv
@@ -1109,11 +1108,10 @@ flattenForAllErrorTcS fl ty
 %************************************************************************
 
 \begin{code}
-setCtFlavorLoc :: CtFlavor -> TcM a -> TcM a
-setCtFlavorLoc (Wanted  loc _) thing = setCtLoc loc thing
-setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing
-setCtFlavorLoc (Given loc _)   thing = setCtLoc loc thing
-setCtFlavorLoc (Solved loc _)  thing = setCtLoc loc thing
+setCtFlavorLoc :: CtEvidence -> TcM a -> TcM a
+setCtFlavorLoc (Wanted  { ctev_wloc = loc }) thing = setCtLoc loc thing
+setCtFlavorLoc (Derived { ctev_wloc = loc }) thing = setCtLoc loc thing
+setCtFlavorLoc (Given   { ctev_gloc = loc }) thing = setCtLoc loc thing
 \end{code}
 
 %************************************************************************
index 8ec0a57..2955676 100644 (file)
@@ -17,7 +17,7 @@ module TcEvidence (
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, 
 
   EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,
-  EvLit(..),
+  EvLit(..), evTermCoercion,
 
   -- TcCoercion
   TcCoercion(..), 
@@ -36,7 +36,7 @@ import Var
 import PprCore ()   -- Instance OutputableBndr TyVar
 import TypeRep  -- Knows type representation
 import TcType
-import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe )
+import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe, getEqPredTys )
 import TysPrim( funTyCon )
 import TyCon
 import PrelNames
@@ -102,6 +102,7 @@ data TcCoercion
   | TcSymCo TcCoercion
   | TcTransCo TcCoercion TcCoercion
   | TcNthCo Int TcCoercion
+  | TcCastCo TcCoercion TcCoercion     -- co1 |> co2
   | TcLetCo TcEvBinds TcCoercion
   deriving (Data.Data, Data.Typeable)
 
@@ -199,6 +200,8 @@ tcCoercionKind co = go co
   where 
     go (TcRefl ty)            = Pair ty ty
     go (TcLetCo _ co)         = go co
+    go (TcCastCo _ co)        = case getEqPredTys (pSnd (go co)) of
+                                   (ty1,ty2) -> Pair ty1 ty2
     go (TcTyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
     go (TcAppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
     go (TcForAllCo tv co)     = mkForAllTy tv <$> go co
@@ -206,8 +209,8 @@ tcCoercionKind co = go co
     go (TcCoVarCo cv)         = eqVarKind cv
     go (TcAxiomInstCo ax tys) = Pair (substTyWith (co_ax_tvs ax) tys (co_ax_lhs ax)) 
                                      (substTyWith (co_ax_tvs ax) tys (co_ax_rhs ax))
-    go (TcSymCo co)           = swap $ go co
-    go (TcTransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)
+    go (TcSymCo co)           = swap (go co)
+    go (TcTransCo co1 co2)    = Pair (pFst (go co1)) (pSnd (go co2))
     go (TcNthCo d co)         = tyConAppArgN d <$> go co
 
     -- c.f. Coercion.coercionKind
@@ -219,7 +222,7 @@ eqVarKind cv
  | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
  = ASSERT (tc `hasKey` eqTyConKey)
    Pair ty1 ty2
- | otherwise = panic "eqVarKind, non coercion variable"
+ | otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv))
 
 coVarsOfTcCo :: TcCoercion -> VarSet
 -- Only works on *zonked* coercions, because of TcLetCo
@@ -229,6 +232,7 @@ coVarsOfTcCo tc_co
     go (TcRefl _)                = emptyVarSet
     go (TcTyConAppCo _ cos)      = foldr (unionVarSet . go) emptyVarSet cos
     go (TcAppCo co1 co2)         = go co1 `unionVarSet` go co2
+    go (TcCastCo co1 co2)        = go co1 `unionVarSet` go co2
     go (TcForAllCo _ co)         = go co
     go (TcInstCo co _)           = go co
     go (TcCoVarCo v)             = unitVarSet v
@@ -289,6 +293,8 @@ ppr_co p (TcLetCo bs co)         = maybeParen p TopPrec $
                                    sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
 ppr_co p (TcAppCo co1 co2)       = maybeParen p TyConPrec $
                                    pprTcCo co1 <+> ppr_co TyConPrec co2
+ppr_co p (TcCastCo co1 co2)      = maybeParen p FunPrec $
+                                   ppr_co FunPrec co1 <+> ptext (sLit "|>") <+> ppr_co FunPrec co2
 ppr_co p co@(TcForAllCo {})      = ppr_forall_co p co
 ppr_co p (TcInstCo co ty)        = maybeParen p TyConPrec $
                                    pprParendTcCo co <> ptext (sLit "@") <> pprType ty
@@ -454,24 +460,24 @@ data EvTerm
 
   | EvCoercion TcCoercion        -- (Boxed) coercion bindings
 
-  | EvCast EvVar TcCoercion      -- d |> co
+  | EvCast EvTerm TcCoercion     -- d |> co
 
   | EvDFunApp DFunId             -- Dictionary instance application
-       [Type] [EvVar]
+       [Type] [EvTerm]
 
-  | EvTupleSel EvId  Int         -- n'th component of the tuple
+  | EvTupleSel EvTerm  Int       -- n'th component of the tuple, 0-indexed
 
-  | EvTupleMk [EvId]             -- tuple built from this stuff
+  | EvTupleMk [EvTerm]           -- tuple built from this stuff
 
   | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors
                                -- See Note [Deferring coercion errors to runtime]
                                -- in TcSimplify
 
-  | EvSuperClass DictId Int      -- n'th superclass. Used for both equalities and
+  | EvSuperClass EvTerm Int      -- n'th superclass. Used for both equalities and
                                  -- dictionaries, even though the former have no
                                  -- selector Id.  We count up from _0_
 
-  | EvKindCast EvVar TcCoercion  -- See Note [EvKindCast]
+  | EvKindCast EvTerm TcCoercion  -- See Note [EvKindCast]
 
   | EvLit EvLit                  -- Dictionary for class "SingI" for type lits.
                                  -- Note [EvLit]
@@ -555,14 +561,14 @@ and another to make it into "SingI" evidence.
 
 
 \begin{code}
-mkEvCast :: EvVar -> TcCoercion -> EvTerm
+mkEvCast :: EvTerm -> TcCoercion -> EvTerm
 mkEvCast ev lco
-  | isTcReflCo lco = EvId ev
+  | isTcReflCo lco = ev
   | otherwise      = EvCast ev lco
 
-mkEvKindCast :: EvVar -> TcCoercion -> EvTerm
+mkEvKindCast :: EvTerm -> TcCoercion -> EvTerm
 mkEvKindCast ev lco
-  | isTcReflCo lco = EvId ev
+  | isTcReflCo lco = ev
   | otherwise      = EvKindCast ev lco
 
 emptyTcEvBinds :: TcEvBinds
@@ -573,17 +579,27 @@ isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b
 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
 
 
-evVarsOfTerm :: EvTerm -> [EvVar]
-evVarsOfTerm (EvId v) = [v]
-evVarsOfTerm (EvCoercion co)      = varSetElems (coVarsOfTcCo co)
-evVarsOfTerm (EvDFunApp _ _ evs)  = evs
-evVarsOfTerm (EvTupleSel v _)     = [v]
-evVarsOfTerm (EvSuperClass v _)   = [v]
-evVarsOfTerm (EvCast v co)        = v : varSetElems (coVarsOfTcCo co)
-evVarsOfTerm (EvTupleMk evs)      = evs
-evVarsOfTerm (EvDelayedError _ _) = []
-evVarsOfTerm (EvKindCast v co)   = v : varSetElems (coVarsOfTcCo co)
-evVarsOfTerm (EvLit _)            = []
+evTermCoercion :: EvTerm -> TcCoercion
+-- Applied only to EvTerms of type (s~t)
+evTermCoercion (EvId v)        = mkTcCoVarCo v
+evTermCoercion (EvCoercion co) = co
+evTermCoercion (EvCast tm co)  = TcCastCo (evTermCoercion tm) co
+evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
+
+evVarsOfTerm :: EvTerm -> VarSet
+evVarsOfTerm (EvId v)             = unitVarSet v
+evVarsOfTerm (EvCoercion co)      = coVarsOfTcCo co
+evVarsOfTerm (EvDFunApp _ _ evs)  = evVarsOfTerms evs
+evVarsOfTerm (EvTupleSel v _)     = evVarsOfTerm v
+evVarsOfTerm (EvSuperClass v _)   = evVarsOfTerm v
+evVarsOfTerm (EvCast tm co)       = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
+evVarsOfTerm (EvTupleMk evs)      = evVarsOfTerms evs
+evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
+evVarsOfTerm (EvKindCast v co)    = coVarsOfTcCo co `unionVarSet` evVarsOfTerm v
+evVarsOfTerm (EvLit _)            = emptyVarSet
+
+evVarsOfTerms :: [EvTerm] -> VarSet
+evVarsOfTerms = foldr (unionVarSet . evVarsOfTerm) emptyVarSet 
 \end{code}
 
 
index aec09e9..9104016 100644 (file)
@@ -1095,21 +1095,24 @@ zonkEvTerm env (EvId v)           = ASSERT2( isId v, ppr v )
                                     return (EvId (zonkIdOcc env v))
 zonkEvTerm env (EvCoercion co)    = do { co' <- zonkTcLCoToLCo env co
                                        ; return (EvCoercion co') }
-zonkEvTerm env (EvCast v co)      = ASSERT( isId v) 
-                                    do { co' <- zonkTcLCoToLCo env co
-                                       ; return (mkEvCast (zonkIdOcc env v) co') }
-
-zonkEvTerm env (EvKindCast v co) = ASSERT( isId v) 
-                                    do { co' <- zonkTcLCoToLCo env co
-                                       ; return (mkEvKindCast (zonkIdOcc env v) co') }
-
-zonkEvTerm env (EvTupleSel v n)   = return (EvTupleSel (zonkIdOcc env v) n)
-zonkEvTerm env (EvTupleMk vs)     = return (EvTupleMk (map (zonkIdOcc env) vs))
+zonkEvTerm env (EvCast tm co)     = do { tm' <- zonkEvTerm env tm
+                                       ; co' <- zonkTcLCoToLCo env co
+                                       ; return (mkEvCast tm' co') }
+
+zonkEvTerm env (EvKindCast v co)  = do { v'  <- zonkEvTerm env v
+                                       ; co' <- zonkTcLCoToLCo env co
+                                       ; return (mkEvKindCast v' co') }
+
+zonkEvTerm env (EvTupleSel tm n)  = do { tm' <- zonkEvTerm env tm
+                                       ; return (EvTupleSel tm' n) }
+zonkEvTerm env (EvTupleMk tms)    = do { tms' <- mapM (zonkEvTerm env) tms
+                                       ; return (EvTupleMk tms') }
 zonkEvTerm _   (EvLit l)          = return (EvLit l)
-zonkEvTerm env (EvSuperClass d n) = return (EvSuperClass (zonkIdOcc env d) n)
+zonkEvTerm env (EvSuperClass d n) = do { d' <- zonkEvTerm env d
+                                       ; return (EvSuperClass d' n) }
 zonkEvTerm env (EvDFunApp df tys tms)
   = do { tys' <- zonkTcTypeToTypes env tys
-       ; let tms' = map (zonkEvVarOcc env) tms
+       ; tms' <- mapM (zonkEvTerm env) tms
        ; return (EvDFunApp (zonkIdOcc env df) tys' tms') }
 zonkEvTerm env (EvDelayedError ty msg)
   = do { ty' <- zonkTcTypeToType env ty
@@ -1344,6 +1347,8 @@ zonkTcLCoToLCo env co
     go (TcAxiomInstCo ax tys) = do { tys' <- zonkTcTypeToTypes env tys; return (TcAxiomInstCo ax tys') }
     go (TcAppCo co1 co2)      = do { co1' <- go co1; co2' <- go co2
                                    ; return (mkTcAppCo co1' co2') }
+    go (TcCastCo co1 co2)     = do { co1' <- go co1; co2' <- go co2
+                                   ; return (TcCastCo co1' co2') }
     go (TcSymCo co)           = do { co' <- go co; return (mkTcSymCo co')  }
     go (TcNthCo n co)         = do { co' <- go co; return (mkTcNthCo n co')  }
     go (TcTransCo co1 co2)    = do { co1' <- go co1; co2' <- go co2
index 7766890..bc217bb 100644 (file)
@@ -840,7 +840,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
              mk_sc_ev_term sc
                | null inst_tv_tys
                , null dfun_ev_vars = EvId sc
-               | otherwise         = EvDFunApp sc inst_tv_tys dfun_ev_vars
+               | otherwise         = EvDFunApp sc inst_tv_tys (map EvId dfun_ev_vars)
 
              inst_tv_tys    = mkTyVarTys inst_tyvars
              arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
@@ -1141,7 +1141,7 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
 
            ; self_dict <- newDict clas inst_tys
            ; let self_ev_bind = EvBind self_dict
-                                (EvDFunApp dfun_id (mkTyVarTys tyvars) dfun_ev_vars)
+                                (EvDFunApp dfun_id (mkTyVarTys tyvars) (map EvId dfun_ev_vars))
 
            ; (meth_id, local_meth_sig) <- mkMethIds sig_fn clas tyvars dfun_ev_vars
                                                    inst_tys sel_id
index 884331d..44d6a8d 100644 (file)
@@ -31,7 +31,6 @@ import TyCon
 import Name
 import IParam
 
-import TysWiredIn ( eqTyCon )
 import FunDeps
 
 import TcEvidence
@@ -46,7 +45,6 @@ import Maybes( orElse )
 import Bag
 
 import Control.Monad ( foldM )
-import TrieMap
 
 import VarEnv
 import qualified Data.Traversable as Traversable
@@ -106,8 +104,11 @@ solveInteractGiven :: GivenLoc -> [EvVar] -> TcS (Bag Implication)
 -- if this can happen in practice though.
 solveInteractGiven gloc evs
   = solveInteractCts (map mk_noncan evs)
-  where mk_noncan ev = CNonCanonical { cc_flavor = Given gloc ev
-                                     , cc_depth = 0 }
+  where 
+    mk_noncan ev = CNonCanonical { cc_ev = Given { ctev_gloc = gloc 
+                                                 , ctev_evtm = EvId ev
+                                                 , ctev_pred = evVarPred ev }
+                                 , cc_depth = 0 }
 
 -- The main solver loop implements Note [Basic Simplifier Plan]
 ---------------------------------------------------------------
@@ -229,13 +230,13 @@ thePipeline = [ ("lookup-in-inerts",        lookupInInertsStage)
 --------------------------------------------------------------------
 lookupInInertsStage :: SimplifierStage
 lookupInInertsStage ct
-  | isWantedCt ct
+  | Wanted { ctev_evar = ev_id, ctev_pred = pred } <- cc_ev ct
   = do { is <- getTcSInerts
-       ; case lookupInInerts is (ctPred ct) of
-           Just ct_cached 
-             |  not (isDerivedCt ct_cached)
-             -> setEvBind (ctId ct) (EvId (ctId ct_cached)) >> 
-                return Stop
+       ; case lookupInInerts is pred of
+           Just ctev
+             |  not (isDerived ctev)
+             -> do { setEvBind ev_id (ctEvTerm ctev)
+                   ; return Stop }
            _ -> continueWith ct }
   | otherwise -- I could do something like that for givens 
               -- as well I suppose but it is not a big deal
@@ -246,7 +247,6 @@ lookupInInertsStage ct
 ----------------------------------------------------------
 canonicalizationStage :: SimplifierStage
 canonicalizationStage = TcCanonical.canonicalize 
-
 \end{code}
 
 *********************************************************************************
@@ -321,7 +321,7 @@ kickOutRewritableInerts ct
 
        ; new_ieqs <- {-# SCC "rewriteInertEqsFromInertEq" #-}
                      rewriteInertEqsFromInertEq (cc_tyvar ct,
-                                                 ct_coercion,cc_flavor ct) ieqs
+                                                 ct_coercion,cc_ev ct) ieqs
        ; let upd_eqs is = is { inert_cans = new_ics }
                         where ics     = inert_cans is
                               new_ics = ics { inert_eqs = new_ieqs }
@@ -336,7 +336,7 @@ kickOutRewritableInerts ct
        ; traceTcS "Kick out" (ppr ct $$ ppr wl)
        ; updWorkListTcS (unionWorkList wl) }
 
-rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtFlavor) -- A new substitution
+rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtEvidence) -- A new substitution
                            -> TyVarEnv Ct                     -- All the inert equalities
                            -> TcS (TyVarEnv Ct)               -- The new inert equalities
 rewriteInertEqsFromInertEq (subst_tv, _subst_co, subst_fl) ieqs
@@ -366,7 +366,7 @@ rewriteInertEqsFromInertEq (subst_tv, _subst_co, subst_fl) ieqs
          | otherwise -- Just keep it there
          = return (Just ct)
          where 
-           fl  = cc_flavor ct
+           fl  = cc_ev ct
 
 kick_out_rewritable :: Ct 
                     -> InertSet 
@@ -401,7 +401,7 @@ kick_out_rewritable ct is@(IS { inert_cans =
                 -- inert_solved, inert_flat_cache and inert_solved_funeqs
                 -- optimistically. But when we lookup we have to take the 
                 -- subsitution into account
-    fl = cc_flavor ct
+    fl = cc_ev ct
     tv = cc_tyvar ct
                                
     (ips_out,   ips_in)     = partitionCCanMap rewritable ipmap
@@ -412,7 +412,7 @@ kick_out_rewritable ct is@(IS { inert_cans =
     (irs_out,   irs_in)   = partitionBag rewritable irreds
     (fro_out,   fro_in)   = partitionBag rewritable frozen
 
-    rewritable ct = (fl `canRewrite` cc_flavor ct)  &&
+    rewritable ct = (fl `canRewrite` cc_ev ct)  &&
                     (tv `elemVarSet` tyVarsOfCt ct) 
                     -- NB: tyVarsOfCt will return the type 
                     --     variables /and the kind variables/ that are 
@@ -461,9 +461,9 @@ data SPSolveResult = SPCantSolve
 -- touchable unification variable.
 --                 See Note [Touchables and givens] 
 trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
-trySpontaneousSolve workItem@(CTyEqCan { cc_flavor = gw
+trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
                                        , cc_tyvar = tv1, cc_rhs = xi, cc_depth = d })
-  | isGivenOrSolved gw
+  | isGiven gw
   = return SPCantSolve
   | Just tv2 <- tcGetTyVar_maybe xi
   = do { tch1 <- isTouchableMetaTyVar tv1
@@ -488,7 +488,7 @@ trySpontaneousSolve _ = return SPCantSolve
 
 ----------------
 trySpontaneousEqOneWay :: SubGoalDepth 
-                       -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
+                       -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
 -- tv is a MetaTyVar, not untouchable
 trySpontaneousEqOneWay d gw tv xi
   | not (isSigTyVar tv) || isTyVarTy xi
@@ -498,7 +498,7 @@ trySpontaneousEqOneWay d gw tv xi
 
 ----------------
 trySpontaneousEqTwoWay :: SubGoalDepth 
-                       -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
+                       -> CtEvidence -> TcTyVar -> TcTyVar -> TcS SPSolveResult
 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
 
 trySpontaneousEqTwoWay d gw tv1 tv2
@@ -585,10 +585,10 @@ unification variables as RHS of type family equations: F xis ~ alpha.
 ----------------
 
 solveWithIdentity :: SubGoalDepth 
-                  -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
+                  -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
 -- Solve with the identity coercion 
 -- Precondition: kind(xi) is a sub-kind of kind(tv)
--- Precondition: CtFlavor is Wanted or Derived
+-- Precondition: CtEvidence is Wanted or Derived
 -- See [New Wanted Superclass Work] to see why solveWithIdentity 
 --     must work for Derived as well as Wanted
 -- Returns: workItem where 
@@ -607,17 +607,18 @@ solveWithIdentity d wd tv xi
                -- cf TcUnify.uUnboundKVar
 
        ; setWantedTyBind tv xi'
-       ; let refl_xi = mkTcReflCo xi'
+       ; let refl_evtm = EvCoercion (mkTcReflCo xi')
+             refl_pred = mkTcEqPred tv_ty xi'
 
        ; when (isWanted wd) $ 
-              setEvBind (flav_evar wd) (EvCoercion refl_xi)
+              setEvBind (ctev_evar wd) refl_evtm
 
-       ; ev_given <- newGivenEvVar (mkTcEqPred tv_ty xi') 
-                                   (EvCoercion refl_xi) >>= (return . mn_thing)
-       ; let given_fl = Given (mkGivenLoc (flav_wloc wd) UnkSkol) ev_given
+       ; let given_fl = Given { ctev_gloc = mkGivenLoc (ctev_wloc wd) UnkSkol
+                              , ctev_pred = refl_pred
+                              , ctev_evtm = refl_evtm }
              
        ; return $ 
-         SPSolved (CTyEqCan { cc_flavor = given_fl
+         SPSolved (CTyEqCan { cc_ev = given_fl
                             , cc_tyvar  = tv, cc_rhs = xi', cc_depth = d }) }
 \end{code}
 
@@ -654,7 +655,7 @@ or, equivalently,
    then there is no reaction
 
 \begin{code}
--- Interaction result of  WorkItem <~> AtomicInert
+-- Interaction result of  WorkItem <~> Ct
 
 data InteractResult 
     = IRWorkItemConsumed { ir_fire :: String } 
@@ -715,8 +716,8 @@ interactWithInertsStage wi
 doInteractWithInert :: Ct -> Ct -> TcS InteractResult
 -- Identical class constraints.
 doInteractWithInert
-  inertItem@(CDictCan { cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) 
-   workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
+  inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1 }) 
+   workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2 })
 
   | cls1 == cls2  
   = do { let pty1 = mkClassPred cls1 tys1
@@ -728,13 +729,13 @@ doInteractWithInert
                                               , text "workItem  = " <+> ppr workItem ])
 
        ; any_fundeps 
-           <- if isGivenOrSolved fl1 && isGivenOrSolved fl2 then return Nothing
+           <- if isGiven fl1 && isGiven fl2 then return Nothing
               -- NB: We don't create fds for given (and even solved), have not seen a useful
               -- situation for these and even if we did we'd have to be very careful to only
               -- create Derived's and not Wanteds. 
 
               else do { let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
-                      ; wloc  <- get_workitem_wloc fl2 
+                            wloc    = getWantedLoc fl2 
                       ; rewriteWithFunDeps fd_eqns tys2 wloc }
                       -- See Note [Efficient Orientation], [When improvement happens]
 
@@ -745,23 +746,18 @@ doInteractWithInert
                | otherwise         -> irKeepGoing "NOP"
 
            -- Actual Functional Dependencies
-           Just (_rewritten_tys2,_cos2,fd_work)
+           Just (_rewritten_tys2, fd_work)
               -- Standard thing: create derived fds and keep on going. Importantly we don't
                -- throw workitem back in the worklist because this can cause loops. See #5236.
                -> do { emitFDWorkAsDerived fd_work (cc_depth workItem)
                      ; irKeepGoing "Cls/Cls (new fundeps)" } -- Just keep going without droping the inert 
        }
-  where get_workitem_wloc (Wanted wl _)  = return wl 
-        get_workitem_wloc (Derived wl _) = return wl
-        get_workitem_wloc _ = pprPanic "Unexpected given workitem!" $
-                              vcat [ text "Work item =" <+> ppr workItem
-                                   , text "Inert item=" <+> ppr inertItem]
-
 -- Two pieces of irreducible evidence: if their types are *exactly identical* 
 -- we can rewrite them. We can never improve using this: 
 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not 
 -- mean that (ty1 ~ ty2)
-doInteractWithInert (CIrredEvCan { cc_flavor = ifl, cc_ty = ty1 })
+doInteractWithInert (CIrredEvCan { cc_ev = ifl, cc_ty = ty1 })
            workItem@(CIrredEvCan { cc_ty = ty2 })
   | ty1 `eqType` ty2
   = solveOneFromTheOther "Irred/Irred" ifl workItem
@@ -771,9 +767,9 @@ doInteractWithInert (CIrredEvCan { cc_flavor = ifl, cc_ty = ty1 })
 -- that equates the type (this is "improvement").  
 -- However, we don't actually need the coercion evidence,
 -- so we just generate a fresh coercion variable that isn't used anywhere.
-doInteractWithInert (CIPCan { cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) 
-           workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
-  | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
+doInteractWithInert (CIPCan { cc_ev = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) 
+           workItem@(CIPCan { cc_ev = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
+  | nm1 == nm2 && isGiven wfl && isGiven ifl
   =    -- See Note [Overriding implicit parameters]
         -- Dump the inert item, override totally with the new one
        -- Do not require type equality
@@ -786,44 +782,43 @@ doInteractWithInert (CIPCan { cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
 
   | nm1 == nm2
   =    -- See Note [When improvement happens]
-    do { mb_eqv <- newWantedEvVar (mkEqPred ty2 ty1)
+    do { mb_eqv <- newWantedEvVar new_wloc (mkEqPred ty2 ty1)
          -- co :: ty2 ~ ty1, see Note [Efficient orientation]
        ; cv <- case mb_eqv of
                  Fresh eqv  -> 
                    do { updWorkListTcS $ extendWorkListEq $ 
-                        CNonCanonical { cc_flavor = Wanted new_wloc eqv
+                        CNonCanonical { cc_ev = eqv
                                       , cc_depth = cc_depth workItem }
-                      ; return eqv }
+                      ; return (ctEvTerm eqv) }
                  Cached eqv -> return eqv
        ; case wfl of
-            Wanted  {} ->
-              let ip_co = mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo cv]
-              in do { setEvBind (ctId workItem) $
-                      mkEvCast (flav_evar ifl) (mkTcSymCo ip_co)
+            Wanted { ctev_evar = ev_id } ->
+              let ip_co = mkTcTyConAppCo (ipTyCon nm1) [evTermCoercion cv]
+              in do { setEvBind ev_id $
+                      mkEvCast (ctEvTerm ifl) (mkTcSymCo ip_co)
                     ; irWorkItemConsumed "IP/IP (solved by rewriting)" }
             _ -> pprPanic "Unexpected IP constraint" (ppr workItem) }
-  where new_wloc
-          | Wanted wl _  <- wfl = wl
-          | Derived wl _ <- wfl = wl
-          | Wanted wl _  <- ifl = wl
-          | Derived wl _ <- ifl = wl
-          | otherwise = panic "Solve IP: no WantedLoc!"
-    
+  where 
+    new_wloc | isGiven wfl = getWantedLoc ifl
+             | otherwise   = getWantedLoc wfl
 
-doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1
+doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
                                   , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 }) 
-                    wi@(CFunEqCan { cc_flavor = fl2, cc_fun = tc2
+                    wi@(CFunEqCan { cc_ev = fl2, cc_fun = tc2
                                   , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
+{-  ToDo: Check with Dimitrios
   | lhss_match  
   , isSolved fl1 -- Inert is solved and we can simply ignore it
                  -- when workitem is given/solved
-  , isGivenOrSolved fl2
+  , isGiven fl2
   = irInertConsumed "FunEq/FunEq"
   | lhss_match
   , isSolved fl2 -- Workitem is solved and we can ignore it when
                  -- the inert is given/solved
-  , isGivenOrSolved fl1                 
+  , isGiven fl1                 
   = irWorkItemConsumed "FunEq/FunEq" 
+-}
+
   | fl1 `canSolve` fl2 && lhss_match
   = do { traceTcS "interact with inerts: FunEq/FunEq" $ 
          vcat [ text "workItem =" <+> ppr wi
@@ -836,10 +831,12 @@ doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1
              -- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]                 
              xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]
 
-       ; xCtFlavor_cache False fl2 [mkTcEqPred xi2 xi1] xev $ what_next d2
+       ; ctevs <- xCtFlavor_cache False fl2 [mkTcEqPred xi2 xi1] xev
                          -- Why not simply xCtFlavor? See Note [Cache-caused loops]
                          -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
+       ; add_to_work d2 ctevs 
        ; irWorkItemConsumed "FunEq/FunEq" }
+
   | fl2 `canSolve` fl1 && lhss_match
   = do { traceTcS "interact with inerts: FunEq/FunEq" $ 
          vcat [ text "workItem =" <+> ppr wi
@@ -847,25 +844,26 @@ doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1
 
        ; let xev = XEvTerm xcomp xdecomp
               -- xcomp : [(xi2 ~ xi1)] -> [(F args ~ xi1)]
-             xcomp [x] = EvCoercion (co2 `mkTcTransCo` mkTcCoVarCo x)
+             xcomp [x] = EvCoercion (co2 `mkTcTransCo` evTermCoercion x)
              xcomp _ = panic "No more goals!"
              -- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)]
-             xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` mkTcCoVarCo x)]
+             xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]
 
-       ; xCtFlavor_cache False fl1 [mkTcEqPred xi2 xi1] xev $ what_next d1
+       ; ctevs <- xCtFlavor_cache False fl1 [mkTcEqPred xi2 xi1] xev 
                           -- Why not simply xCtFlavor? See Note [Cache-caused loops]
                           -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
 
+       ; add_to_work d1 ctevs 
        ; irInertConsumed "FunEq/FunEq"}
   where
+    add_to_work d [ctev] = updWorkListTcS $ extendWorkListEq $
+                           CNonCanonical {cc_ev = ctev, cc_depth = d}
+    add_to_work _ _ = return ()
+
     lhss_match = tc1 == tc2 && eqTypes args1 args2 
-    what_next d [new_fl] 
-      = updWorkListTcS $ 
-        extendWorkListEq (CNonCanonical {cc_flavor=new_fl,cc_depth = d})
-    what_next _ _ = return ()
-    co1 = mkTcCoVarCo $ flav_evar fl1
-    co2 = mkTcCoVarCo $ flav_evar fl2
-    mk_sym_co x = mkTcSymCo (mkTcCoVarCo x)
+    co1 = evTermCoercion $ ctEvTerm fl1
+    co2 = evTermCoercion $ ctEvTerm fl2
+    mk_sym_co x = mkTcSymCo (evTermCoercion x)
     
 doInteractWithInert _ _ = irKeepGoing "NOP"
 
@@ -905,7 +903,7 @@ solving.
 \begin{code}
 
 solveOneFromTheOther :: String    -- Info 
-                     -> CtFlavor  -- Inert 
+                     -> CtEvidence  -- Inert 
                      -> Ct        -- WorkItem 
                      -> TcS InteractResult
 -- Preconditions: 
@@ -920,22 +918,23 @@ solveOneFromTheOther info ifl workItem
                  -- so it's safe to continue on from this point
   = irInertConsumed ("Solved[DI] " ++ info)
   
-  | isSolved ifl, isGivenOrSolved wfl
+{-  ToDo: Check with Dimitrios
+  | isSolved ifl, isGiven wfl
     -- Same if the inert is a GivenSolved -- just get rid of it
   = irInertConsumed ("Solved[SI] " ++ info)
+-}
 
   | otherwise
   = ASSERT( ifl `canSolve` wfl )
       -- Because of Note [The Solver Invariant], plus Derived dealt with
-    do { when (isWanted wfl) $ setEvBind wid (EvId iid)
+    do { case wfl of
+           Wanted { ctev_evar = ev_id } -> setEvBind ev_id (ctEvTerm ifl)
+           _                            -> return ()
            -- Overwrite the binding, if one exists
           -- If both are Given, we already have evidence; no need to duplicate
        ; irWorkItemConsumed ("Solved " ++ info) }
   where 
-     wfl = cc_flavor workItem
-     wid = ctId workItem
-     iid = flav_evar ifl
-
+     wfl = cc_ev workItem
 \end{code}
 
 Note [Superclasses and recursive dictionaries]
@@ -1305,7 +1304,7 @@ now!).
 rewriteWithFunDeps :: [Equation]
                    -> [Xi] 
                    -> WantedLoc 
-                   -> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)])) 
+                   -> TcS (Maybe ([Xi], [CtEvidence])) 
                                            -- Not quite a WantedEvVar unfortunately
                                            -- Because our intention could be to make 
                                            -- it derived at the end of the day
@@ -1313,13 +1312,13 @@ rewriteWithFunDeps :: [Equation]
 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
 rewriteWithFunDeps eqn_pred_locs xis wloc
  = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
-      ; let fd_ev_pos :: [(Int,(EqVar,WantedLoc))]
+      ; let fd_ev_pos :: [(Int,CtEvidence)]
             fd_ev_pos = concat fd_ev_poss
-            (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
+            rewritten_xis = rewriteDictParams fd_ev_pos xis
       ; if null fd_ev_pos then return Nothing
-        else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
+        else return (Just (rewritten_xis, map snd fd_ev_pos)) }
 
-instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
+instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,CtEvidence)]
 -- Post: Returns the position index as well as the corresponding FunDep equality
 instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
                         , fd_pred1 = d1, fd_pred2 = d2 })
@@ -1332,10 +1331,10 @@ instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
        = let sty1 = Type.substTy subst ty1 
              sty2 = Type.substTy subst ty2 
          in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
-            else do { mb_eqv <- newWantedEvVar (mkTcEqPred sty1 sty2)
+            else do { mb_eqv <- newDerived (push_ctx wl) (mkTcEqPred sty1 sty2)
                     ; case mb_eqv of
-                         Fresh eqv -> return $ (i,(eqv, push_ctx wl)):ievs
-                         Cached {} -> return ievs }
+                         Just ctev -> return $ (i,ctev):ievs
+                         Nothing   -> return ievs }
                            -- We are eventually going to emit FD work back in the work list so 
                            -- it is important that we only return the /freshly created/ and not 
                            -- some existing equality!
@@ -1355,34 +1354,30 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
                          nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
        ; return (tidy_env, msg) }
 
-rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
-                  -> [Type]                    -- A sequence of types: tys
-                  -> [(Type, TcCoercion)]      -- Returns: [(ty', co : ty' ~ ty)]
+rewriteDictParams :: [(Int,CtEvidence)] -- A set of coercions : (pos, ty' ~ ty)
+                  -> [Type]             -- A sequence of types: tys
+                  -> [Type]                   
 rewriteDictParams param_eqs tys
   = zipWith do_one tys [0..]
   where
-    do_one :: Type -> Int -> (Type, TcCoercion)
+    do_one :: Type -> Int -> Type
     do_one ty n = case lookup n param_eqs of
-                    Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev))
-                    Nothing  -> (ty,             mkTcReflCo ty)        -- Identity
+                    Just wev -> get_fst_ty wev
+                    Nothing  -> ty
 
-    get_fst_ty (wev,_wloc) 
-      | Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev )
+    get_fst_ty ctev
+      | Just (ty1, _) <- getEqPredTys_maybe (ctEvPred ctev)
       = ty1
       | otherwise 
       = panic "rewriteDictParams: non equality fundep!?"
 
         
-emitFDWorkAsDerived :: [(EvVar,WantedLoc)] 
+emitFDWorkAsDerived :: [CtEvidence]   -- All Derived
                     -> SubGoalDepth -> TcS () 
 emitFDWorkAsDerived evlocs d 
-  = updWorkListTcS $ appendWorkListEqs fd_cts
-  where fd_cts = map mk_fd_ct evlocs 
-        mk_fd_ct (v,wl) 
-          = CNonCanonical { cc_flavor = Derived wl (evVarPred v) 
-                          , cc_depth = d }
-
-
+  = updWorkListTcS $ appendWorkListEqs (map mk_fd_ct evlocs)
+  where 
+    mk_fd_ct der_ev = CNonCanonical { cc_ev = der_ev, cc_depth = d }
 \end{code}
 
 
@@ -1432,11 +1427,11 @@ doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
 
 -- Given dictionary
 -- See Note [Given constraint that matches an instance declaration]
-doTopReact _inerts (CDictCan { cc_flavor = Given {} })
+doTopReact _inerts (CDictCan { cc_ev = Given {} })
   = return NoTopInt -- NB: Superclasses already added since it's canonical
 
 -- Derived dictionary: just look for functional dependencies
-doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc _pty
+doTopReact _inerts workItem@(CDictCan { cc_ev = Derived loc _pty
                                       , cc_class = cls, cc_tyargs = xis })
   = do { instEnvs <- getInstEnvs
        ; let fd_eqns = improveFromInstEnv instEnvs
@@ -1444,7 +1439,7 @@ doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc _pty
        ; m <- rewriteWithFunDeps fd_eqns xis loc
        ; case m of
            Nothing -> return NoTopInt
-           Just (xis',_,fd_work) ->
+           Just (xis', fd_work) ->
                let workItem' = workItem { cc_tyargs = xis' }
                    -- Deriveds are not supposed to have identity
                in do { emitFDWorkAsDerived fd_work (cc_depth workItem)
@@ -1454,7 +1449,7 @@ doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc _pty
        }
 
 -- Wanted dictionary
-doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc dict_id)
+doTopReact inerts workItem@(CDictCan { cc_ev = fl@(Wanted { ctev_wloc = loc, ctev_evar = dict_id })
                                      , cc_class = cls, cc_tyargs = xis
                                      , cc_depth = depth })
   -- See Note [MATCHING-SYNONYMS]
@@ -1470,108 +1465,103 @@ doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc dict_id)
            Nothing ->
                do { lkup_inst_res  <- matchClassInst inerts cls xis loc
                   ; case lkup_inst_res of
-                      GenInst wtvs ev_term
-                          -> let sfl = Solved (mkSolvedLoc loc UnkSkol) dict_id 
-                             in addToSolved (workItem { cc_flavor = sfl }) >> 
-                                doSolveFromInstance wtvs ev_term
-                      NoInstance
-                          -> return NoTopInt
+                      GenInst wtvs ev_term -> do { addToSolved fl
+                                                 ; doSolveFromInstance wtvs ev_term }
+                      NoInstance -> return NoTopInt
                   }
            -- Actual Functional Dependencies
-           Just (_xis',_cos,fd_work) ->
+           Just (_xis', fd_work) ->
                do { emitFDWorkAsDerived fd_work (cc_depth workItem)
                   ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
                                       , tir_new_item = ContinueWith workItem } } }
 
-   where doSolveFromInstance :: [EvVar] -> EvTerm -> TcS TopInteractResult
-         -- Precondition: evidence term matches the predicate workItem
-         doSolveFromInstance evs ev_term 
-            | null evs
-            = do { traceTcS "doTopReact/found nullary instance for" $
-                   ppr dict_id
-                 ; setEvBind dict_id ev_term
-                 ; return $ 
-                   SomeTopInt { tir_rule = "Dict/Top (solved, no new work)" 
-                              , tir_new_item = Stop } }
-            | otherwise 
-            = do { traceTcS "doTopReact/found non-nullary instance for" $ 
-                   ppr dict_id
-                 ; setEvBind dict_id ev_term
-                 ; let mk_new_wanted ev
-                           = CNonCanonical { cc_flavor = fl { flav_evar = ev }
-                                           , cc_depth  = depth + 1 }
-                 ; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs))
-                 ; return $
-                   SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
-                              , tir_new_item = Stop }
-                 }
+   where 
+     doSolveFromInstance :: [CtEvidence] -> EvTerm -> TcS TopInteractResult
+      -- Precondition: evidence term matches the predicate workItem
+     doSolveFromInstance evs ev_term 
+        | null evs
+        = do { traceTcS "doTopReact/found nullary instance for" $
+               ppr dict_id
+             ; setEvBind dict_id ev_term
+             ; return $ 
+               SomeTopInt { tir_rule = "Dict/Top (solved, no new work)" 
+                          , tir_new_item = Stop } }
+        | otherwise 
+        = do { traceTcS "doTopReact/found non-nullary instance for" $ 
+               ppr dict_id
+             ; setEvBind dict_id ev_term
+             ; let mk_new_wanted ev
+                       = CNonCanonical { cc_ev   = ev
+                                       , cc_depth = depth + 1 }
+             ; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs))
+             ; return $
+               SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
+                          , tir_new_item = Stop }
+             }
 
 -- Type functions
-doTopReact _inerts (CFunEqCan { cc_flavor = fl })
+{-  ToDo: Check with Dimitrios
+doTopReact _inerts (CFunEqCan { cc_ev = fl })
   | isSolved fl
   = return NoTopInt -- If Solved, no more interactions should happen
+-}
 
 -- Otherwise, it's a Given, Derived, or Wanted
-doTopReact _inerts workItem@(CFunEqCan { cc_flavor = fl, cc_depth = d
+doTopReact _inerts workItem@(CFunEqCan { cc_ev = fl, cc_depth = d
                                        , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
   = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far 
     do { match_res <- matchFam tc args   -- See Note [MATCHING-SYNONYMS]
        ; case match_res of
            Nothing -> return NoTopInt 
            Just (famInst, rep_tys)
-             -> do { mb_already_solved <- lkpFunEqCache (mkTyConApp tc args)
+             -> do { mb_already_solved <- lkpSolvedFunEqCache (mkTyConApp tc args)
                    ; traceTcS "doTopReact: Family instance matches" $ 
                      vcat [ text "solved-fun-cache" <+> if isJust mb_already_solved then text "hit" else text "miss"
                           , text "workItem =" <+> ppr workItem ]
                    ; let (coe,rhs_ty) 
-                           | Just cached_ct <- mb_already_solved
-                           = (mkTcCoVarCo (ctId cached_ct), 
-                                  cc_rhs cached_ct)
+                           | Just ctev <- mb_already_solved
+                           , not (isDerived ctev)
+                           = ASSERT( isEqPred (ctEvPred ctev) )
+                             (evTermCoercion (ctEvTerm ctev), snd (getEqPredTys (ctEvPred ctev)))
                            | otherwise 
                            = let coe_ax = famInstAxiom famInst
                              in (mkTcAxInstCo coe_ax rep_tys, 
                                               mkAxInstRHS coe_ax rep_tys)
                                 
-                         xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` mkTcCoVarCo x)]
-                         xcomp [x] = EvCoercion (coe `mkTcTransCo` mkTcCoVarCo x)
+                         xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
+                         xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
                          xcomp _   = panic "No more goals!"
                          
                          xev = XEvTerm xcomp xdecomp
-                   ; xCtFlavor fl [mkTcEqPred rhs_ty xi] xev what_next } }
-    where what_next [ct_flav]
-            = do { updWorkListTcS $ 
-                   extendWorkListEq (CNonCanonical { cc_flavor = ct_flav
-                                                   , cc_depth  = d+1 })
-                 ; cache_in_solved fl
-                 ; return $ SomeTopInt { tir_rule = "Fun/Top"
-                                       , tir_new_item = Stop } }
-          what_next _ -- No subgoal (because it's cached)
-            = do { cache_in_solved fl
-                 ; return $ SomeTopInt { tir_rule = "Fun/Top"
-                                       , tir_new_item = Stop } }
-
-          cache_in_solved (Derived {})   = return ()
-          cache_in_solved (Wanted wl ev) = 
-            let sfl = Solved (mkSolvedLoc wl UnkSkol) ev  
-                solved = workItem { cc_flavor = sfl }
-            in updFunEqCache solved >> addToSolved solved
-          cache_in_solved fl =
-            let sfl = Solved (flav_gloc fl) (flav_evar fl)
-                solved = workItem { cc_flavor = sfl }
-            in updFunEqCache solved >> addToSolved solved
+                   ; ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
+                   ; case ctevs of
+                       [ctev] -> updWorkListTcS $ extendWorkListEq $
+                                 CNonCanonical { cc_ev = ctev
+                                               , cc_depth  = d+1 }
+                       ctevs -> -- No subgoal (because it's cached)
+                                ASSERT( null ctevs) return () 
+
+                   ; unless (isDerived fl) $
+                     do { addSolvedFunEq fl
+                        ; addToSolved fl }
+                   ; return $ SomeTopInt { tir_rule = "Fun/Top"
+                                       , tir_new_item = Stop } } }
             
 -- Any other work item does not react with any top-level equations
 doTopReact _inerts _workItem = return NoTopInt 
 
 
-lkpFunEqCache :: TcType -> TcS (Maybe Ct)
-lkpFunEqCache fam_head 
+lkpSolvedFunEqCache :: TcType -> TcS (Maybe CtEvidence)
+lkpSolvedFunEqCache fam_head 
   = do { (_subst,_inscope) <- getInertEqs 
        ; fun_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
        ; traceTcS "lkpFunEqCache" $ vcat [ text "fam_head    =" <+> ppr fam_head
-                                         , text "funeq cache =" <+> pprCtTypeMap (unCtFamHeadMap fun_cache) ]
-       ; rewrite_cached $ 
-         lookupTM fam_head (unCtFamHeadMap fun_cache) }
+                                         , text "funeq cache =" <+> ppr fun_cache ]
+       ; return (lookupFamHead fun_cache fam_head) }
+
+{-             ToDo; talk to Dimitrios.  I have no idea what is happening here
+
+       ; rewrite_cached (lookupFamHead fun_cache fam_head) }
 -- The two different calls do not seem to make a significant difference in 
 -- terms of hit/miss rate for many memory-critical/performance tests but the
 -- latter blows up the space on the heap somehow ... It maybe the niFixTvSubst.
@@ -1579,11 +1569,10 @@ lkpFunEqCache fam_head
 --       lookupTypeMap_mod subst cc_rhs fam_head (unCtFamHeadMap fun_cache) }
  
   where rewrite_cached Nothing = return Nothing
-        rewrite_cached (Just ct@(CFunEqCan { cc_flavor = fl, cc_depth = d
+        rewrite_cached (Just ct@(CFunEqCan { cc_ev = fl, cc_depth = d
                                            , cc_fun = tc, cc_tyargs = xis
                                            , cc_rhs = xi}))
-          = ASSERT (isSolved fl)
-            do { (xis_subst,cos) <- flattenMany d FMFullFlatten fl xis 
+          = do { (xis_subst,cos) <- flattenMany d FMFullFlatten fl xis 
                                     -- cos :: xis_subst ~ xis 
                ; (xi_subst,co) <- flatten d FMFullFlatten fl xi
                                     -- co :: xi_subst ~ xi
@@ -1607,27 +1596,14 @@ lkpFunEqCache fam_head
                       -> return Nothing -- Strange: cached?
                     Just fl' 
                       -> return $ 
-                         Just (CFunEqCan { cc_flavor = fl'
+                         Just (CFunEqCan { cc_ev = fl'
                                          , cc_depth = d
                                          , cc_fun = tc
                                          , cc_tyargs = xis_subst
                                          , cc_rhs = xi_subst }) }
         rewrite_cached (Just other_ct) 
           = pprPanic "lkpFunEqCache:not family equation!" $ ppr other_ct
-
-updFunEqCache :: Ct -> TcS ()
-updFunEqCache fun_eq@(CFunEqCan { cc_fun = tc, cc_tyargs = xis })
-  = modifyInertTcS $ \inert -> ((), upd_inert inert)
-  where upd_inert inert 
-          = let slvd = unCtFamHeadMap (inert_solved_funeqs inert)
-            in inert { inert_solved_funeqs =
-                          CtFamHeadMap (alterTM key upd_funeqs slvd) }       
-        upd_funeqs Nothing    = Just fun_eq
-        upd_funeqs (Just _ct) = Just fun_eq 
-             -- Or _ct? depends on which caches more steps of computation
-        key = mkTyConApp tc xis
-updFunEqCache other = pprPanic "updFunEqCache:Non family equation" $ ppr other
-
+-}
 \end{code}
 
 
@@ -1830,7 +1806,7 @@ NB: The desugarer needs be more clever to deal with equalities
 \begin{code}
 data LookupInstResult
   = NoInstance
-  | GenInst [EvVar] EvTerm 
+  | GenInst [CtEvidence] EvTerm 
 
 matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
 
@@ -1875,12 +1851,11 @@ matchClassInst inerts clas tys loc
                  ; if null theta then
                        return (GenInst [] (EvDFunApp dfun_id tys []))
                    else do
-                     { evc_vars <- instDFunConstraints theta
-                     ; let ev_vars = map mn_thing evc_vars
-                           new_ev_vars = [mn_thing evc | evc <- evc_vars
-                                                       , isFresh evc ]
+                     { evc_vars <- instDFunConstraints loc theta
+                     ; let new_ev_vars = freshGoals evc_vars
                            -- new_ev_vars are only the real new variables that can be emitted 
-                     ; return $ GenInst new_ev_vars (EvDFunApp dfun_id tys ev_vars) } }
+                           dfun_app = EvDFunApp dfun_id tys (getEvTerms evc_vars)
+                     ; return $ GenInst new_ev_vars dfun_app } }
         }
    where 
      givens_for_this_clas :: Cts
@@ -1892,7 +1867,7 @@ matchClassInst inerts clas tys loc
      given_overlap untch = anyBag (matchable untch) givens_for_this_clas
 
      matchable untch (CDictCan { cc_class = clas_g, cc_tyargs = sys
-                               , cc_flavor = fl })
+                               , cc_ev = fl })
        | isGiven fl
        = ASSERT( clas_g == clas )
          case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv && 
index 3ba80e3..79b6b02 100644 (file)
@@ -627,29 +627,24 @@ zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
 zonkCt :: Ct -> TcM Ct 
 -- Zonking a Ct conservatively gives back a CNonCanonical
 zonkCt ct 
-  = do { fl' <- zonkFlavor (cc_flavor ct)
+  = do { fl' <- zonkCtEvidence (cc_ev ct)
        ; return $ 
-         CNonCanonical { cc_flavor = fl'
+         CNonCanonical { cc_ev = fl'
                        , cc_depth = cc_depth ct } }
 zonkCts :: Cts -> TcM Cts
 zonkCts = mapBagM zonkCt
 
-zonkFlavor :: CtFlavor -> TcM CtFlavor
-zonkFlavor (Given loc evar
+zonkCtEvidence :: CtEvidence -> TcM CtEvidence
+zonkCtEvidence ctev@(Given { ctev_gloc = loc, ctev_pred = pred }
   = do { loc' <- zonkGivenLoc loc
-       ; evar' <- zonkEvVar evar
-       ; return (Given loc' evar') }
-zonkFlavor (Solved loc evar) 
-  = do { loc' <- zonkGivenLoc loc
-       ; evar' <- zonkEvVar evar
-       ; return (Solved loc' evar') }
-zonkFlavor (Wanted loc evar)
-  = do { evar' <- zonkEvVar evar
-       ; return (Wanted loc evar') }
-zonkFlavor (Derived loc pty)
-  = do { pty' <- zonkTcType pty
-       ; return (Derived loc pty') }
-
+       ; pred' <- zonkTcType pred
+       ; return (ctev { ctev_gloc = loc', ctev_pred = pred'}) }
+zonkCtEvidence ctev@(Wanted { ctev_pred = pred })
+  = do { pred' <- zonkTcType pred
+       ; return (ctev { ctev_pred = pred' }) }
+zonkCtEvidence ctev@(Derived { ctev_pred = pred })
+  = do { pred' <- zonkTcType pred
+       ; return (ctev { ctev_pred = pred' }) }
 
 zonkGivenLoc :: GivenLoc -> TcM GivenLoc
 -- GivenLocs may have unification variables inside them!
index 6a79b73..d17d3e6 100644 (file)
@@ -55,9 +55,9 @@ module TcRnTypes(
         singleCt, extendCts, isEmptyCts, isCTyEqCan, isCFunEqCan,
         isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
         isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt, 
-        isGivenCt, isGivenOrSolvedCt,
-        ctWantedLoc,
-        SubGoalDepth, mkNonCanonical, ctPred, ctFlavPred, ctId, ctFlavId,
+        isGivenCt, 
+        ctWantedLoc, ctEvidence,
+        SubGoalDepth, mkNonCanonical, ctPred, ctEvPred, ctEvTerm, ctEvId,
 
         WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
         andWC, addFlats, addImplics, mkFlatWC,
@@ -70,9 +70,9 @@ module TcRnTypes(
 
        SkolemInfo(..),
 
-        CtFlavor(..), pprFlavorArising,
-        mkSolvedLoc, mkGivenLoc,
-        isWanted, isGivenOrSolved, isGiven, isSolved,
+        CtEvidence(..), pprFlavorArising,
+        mkGivenLoc,
+        isWanted, isGiven,
         isDerived, getWantedLoc, getGivenLoc, canSolve, canRewrite,
 
        -- Pretty printing
@@ -89,7 +89,7 @@ module TcRnTypes(
 
 import HsSyn
 import HscTypes
-import TcEvidence( EvBind, EvBindsVar )
+import TcEvidence
 import Type
 import Class    ( Class )
 import TyCon    ( TyCon )
@@ -850,7 +850,7 @@ type SubGoalDepth = Int -- An ever increasing number used to restrict
 data Ct
   -- Atomic canonical constraints 
   = CDictCan {  -- e.g.  Num xi
-      cc_flavor :: CtFlavor
+      cc_ev :: CtEvidence
       cc_class  :: Class, 
       cc_tyargs :: [Xi],
 
@@ -860,14 +860,14 @@ data Ct
 
   | CIPCan {   -- ?x::tau
       -- See note [Canonical implicit parameter constraints].
-      cc_flavor :: CtFlavor,
+      cc_ev :: CtEvidence,
       cc_ip_nm  :: IPName Name,
-      cc_ip_ty  :: TcTauType, -- Not a Xi! See same not as above
+      cc_ip_ty  :: TcTauType,          -- Not a Xi! See same not as above
       cc_depth  :: SubGoalDepth        -- See Note [WorkList]
     }
 
   | CIrredEvCan {  -- These stand for yet-unknown predicates
-      cc_flavor :: CtFlavor,
+      cc_ev :: CtEvidence,
       cc_ty     :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
                        -- Since, if it were a type constructor application, that'd make the
                        -- whole constraint a CDictCan, CIPCan, or CTyEqCan. And it can't be
@@ -881,7 +881,7 @@ data Ct
        --   * typeKind xi `compatKind` typeKind tv
        --       See Note [Spontaneous solving and kind compatibility]
        --   * We prefer unification variables on the left *JUST* for efficiency
-      cc_flavor :: CtFlavor
+      cc_ev :: CtEvidence
       cc_tyvar  :: TcTyVar, 
       cc_rhs    :: Xi,
 
@@ -891,7 +891,7 @@ data Ct
   | CFunEqCan {  -- F xis ~ xi  
                  -- Invariant: * isSynFamilyTyCon cc_fun 
                  --            * typeKind (F xis) `compatKind` typeKind xi
-      cc_flavor :: CtFlavor
+      cc_ev :: CtEvidence
       cc_fun    :: TyCon,      -- A type function
       cc_tyargs :: [Xi],       -- Either under-saturated or exactly saturated
       cc_rhs    :: Xi,         --    *never* over-saturated (because if so
@@ -902,18 +902,24 @@ data Ct
     }
 
   | CNonCanonical { -- See Note [NonCanonical Semantics] 
-      cc_flavor :: CtFlavor
+      cc_ev :: CtEvidence
       cc_depth  :: SubGoalDepth
     }
 
 \end{code}
 
 \begin{code}
-mkNonCanonical :: CtFlavor -> Ct
-mkNonCanonical flav = CNonCanonical { cc_flavor = flav, cc_depth = 0}
+mkNonCanonical :: CtEvidence -> Ct
+mkNonCanonical flav = CNonCanonical { cc_ev = flav, cc_depth = 0}
+
+ctEvidence :: Ct -> CtEvidence
+ctEvidence = cc_ev
 
 ctPred :: Ct -> PredType 
-ctPred (CNonCanonical { cc_flavor = fl }) = ctFlavPred fl
+ctPred ct = ctEvPred (cc_ev ct)
+-- ToDo Check with Dimitrios
+{-
+ctPred (CNonCanonical { cc_ev = fl }) = ctEvPred fl
 ctPred (CDictCan { cc_class = cls, cc_tyargs = xis }) 
   = mkClassPred cls xis
 ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) 
@@ -923,18 +929,13 @@ ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 })
 ctPred (CIPCan { cc_ip_nm = nm, cc_ip_ty = xi }) 
   = mkIPPred nm xi
 ctPred (CIrredEvCan { cc_ty = xi }) = xi
-
-
-ctId :: Ct -> EvVar
--- Precondition: not a derived!
-ctId ct = ctFlavId (cc_flavor ct)
-
+-}
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-                    CtFlavor
+                    CtEvidence
          The "flavor" of a canonical constraint
 %*                                                                     *
 %************************************************************************
@@ -942,20 +943,17 @@ ctId ct = ctFlavId (cc_flavor ct)
 \begin{code}
 ctWantedLoc :: Ct -> WantedLoc
 -- Only works for Wanted/Derived
-ctWantedLoc ct = ASSERT2( not (isGivenOrSolved (cc_flavor ct)), ppr ct )
-                 getWantedLoc (cc_flavor ct)
+ctWantedLoc ct = ASSERT2( not (isGiven (cc_ev ct)), ppr ct )
+                 getWantedLoc (cc_ev ct)
 
 isWantedCt :: Ct -> Bool
-isWantedCt = isWanted . cc_flavor 
+isWantedCt = isWanted . cc_ev 
 
 isGivenCt :: Ct -> Bool
-isGivenCt = isGiven . cc_flavor
+isGivenCt = isGiven . cc_ev
 
 isDerivedCt :: Ct -> Bool
-isDerivedCt = isDerived . cc_flavor
-
-isGivenOrSolvedCt :: Ct -> Bool
-isGivenOrSolvedCt = isGivenOrSolved . cc_flavor
+isDerivedCt = isDerived . cc_ev
 
 isCTyEqCan :: Ct -> Bool 
 isCTyEqCan (CTyEqCan {})  = True 
@@ -989,7 +987,7 @@ isCNonCanonical _ = False
 
 \begin{code}
 instance Outputable Ct where
-  ppr ct = ppr (cc_flavor ct) <+> 
+  ppr ct = ppr (cc_ev ct) <+> 
            braces (ppr (cc_depth ct)) <+> parens (text ct_sort)
          where ct_sort = case ct of 
                            CTyEqCan {}      -> "CTyEqCan"
@@ -1229,86 +1227,80 @@ pprWantedsWithLocs wcs
 %*                                                                     *
 %************************************************************************
 
+Note [Evidence field of CtEvidence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+During constraint solving we never look at the type of ctev_evtm, or
+ctev_evar; instead we look at the cte_pred field.  The evtm/evar field
+may be un-zonked.
+
 \begin{code}
-data CtFlavor
-  = Given { flav_gloc :: GivenLoc, flav_evar :: EvVar } 
-    -- Trully given, not depending on subgoals
+data CtEvidence   -- Rename to CtEvidence
+  = Given { ctev_gloc :: GivenLoc
+          , ctev_pred :: TcPredType
+          , ctev_evtm :: EvTerm }          -- See Note [Evidence field of CtEvidence]
+    -- Truly given, not depending on subgoals
     -- NB: Spontaneous unifications belong here
     -- DV TODOs: (i)  Consider caching actual evidence _term_
     --           (ii) Revisit Note [Optimizing Spontaneously Solved Coercions]
     
-  | Solved { flav_gloc :: GivenLoc, flav_evar :: EvVar }
-    -- Originally wanted, but now we've produced and 
-    -- bound some partial evidence for this constraint.
-    -- NB: Evidence may rely on yet-wanted constraints or other solved or given
-    
-  | Wanted { flav_wloc :: WantedLoc, flav_evar :: EvVar }
+  | Wanted { ctev_wloc :: WantedLoc
+           , ctev_pred :: TcPredType
+           , ctev_evar :: EvVar }          -- See Note [Evidence field of CtEvidence]
     -- Wanted goal 
     
-  | Derived { flav_wloc :: WantedLoc, flav_der_pty :: TcPredType }
+  | Derived { ctev_wloc :: WantedLoc 
+            , ctev_pred :: TcPredType }
     -- A goal that we don't really have to solve and can't immediately 
-    -- rewrite anything other than a derived (there's no evidence variable!) 
+    -- rewrite anything other than a derived (there's no evidence!) 
     -- but if we do manage to solve it may help in solving other goals.
 
-ctFlavPred :: CtFlavor -> TcPredType
+ctEvPred :: CtEvidence -> TcPredType
 -- The predicate of a flavor
-ctFlavPred (Given _ evar)  = evVarPred evar
-ctFlavPred (Solved _ evar) = evVarPred evar
-ctFlavPred (Wanted _ evar) = evVarPred evar
-ctFlavPred (Derived { flav_der_pty = pty }) = pty
-
-ctFlavId :: CtFlavor -> EvVar
--- Precondition: can't be derived
-ctFlavId (Derived _ pty) 
-  = pprPanic "ctFlavId: derived constraint cannot have id" $ 
-    text "pty   =" <+> ppr pty
-ctFlavId fl = flav_evar fl
-
-instance Outputable CtFlavor where
+ctEvPred = ctev_pred
+
+ctEvTerm :: CtEvidence -> EvTerm
+ctEvTerm (Given   { ctev_evtm = tm }) = tm
+ctEvTerm (Wanted  { ctev_evar = ev }) = EvId ev
+ctEvTerm ctev@(Derived {}) = pprPanic "ctEvTerm: derived constraint cannot have id" 
+                                      (ppr ctev)
+
+ctEvId :: CtEvidence -> TcId
+ctEvId (Wanted  { ctev_evar = ev }) = ev
+ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
+
+instance Outputable CtEvidence where
   ppr fl = case fl of
-             (Given _ evar)  -> ptext (sLit "[G]") <+> ppr evar <+> ppr_pty
-             (Solved _ evar) -> ptext (sLit "[S]") <+> ppr evar <+> ppr_pty
-             (Wanted _ evar) -> ptext (sLit "[W]") <+> ppr evar <+> ppr_pty
-             (Derived {})    -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty
-         where ppr_pty = dcolon <+> ppr (ctFlavPred fl)
+             Given {}   -> ptext (sLit "[G]") <+> ppr (ctev_evtm fl) <+> ppr_pty
+             Wanted {}  -> ptext (sLit "[W]") <+> ppr (ctev_evar fl) <+> ppr_pty
+             Derived {} -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty
+         where ppr_pty = dcolon <+> ppr (ctEvPred fl)
 
-getWantedLoc :: CtFlavor -> WantedLoc
+getWantedLoc :: CtEvidence -> WantedLoc
 -- Precondition: Wanted or Derived
-getWantedLoc fl = flav_wloc fl
+getWantedLoc fl = ctev_wloc fl
 
-getGivenLoc :: CtFlavor -> GivenLoc 
--- Precondition: Given or Solved
-getGivenLoc fl = flav_gloc fl
+getGivenLoc :: CtEvidence -> GivenLoc 
+-- Precondition: Given
+getGivenLoc fl = ctev_gloc fl
 
-pprFlavorArising :: CtFlavor -> SDoc
-pprFlavorArising (Given gl _)   = pprArisingAt gl
-pprFlavorArising (Solved gl _)  = pprArisingAt gl
-pprFlavorArising (Wanted wl _)  = pprArisingAt wl
-pprFlavorArising (Derived wl _) = pprArisingAt wl
+pprFlavorArising :: CtEvidence -> SDoc
+pprFlavorArising (Given { ctev_gloc = gl }) = pprArisingAt gl
+pprFlavorArising ctev                       = pprArisingAt (ctev_wloc ctev)
 
 
-isWanted :: CtFlavor -> Bool
+isWanted :: CtEvidence -> Bool
 isWanted (Wanted {}) = True
 isWanted _ = False
 
-isGivenOrSolved :: CtFlavor -> Bool
-isGivenOrSolved (Given {})  = True
-isGivenOrSolved (Solved {}) = True
-isGivenOrSolved _ = False
-
-isSolved :: CtFlavor -> Bool
-isSolved (Solved {}) = True
-isSolved _ = False
-
-isGiven :: CtFlavor -> Bool 
-isGiven (Given {}) = True
+isGiven :: CtEvidence -> Bool
+isGiven (Given {})  = True
 isGiven _ = False
 
-isDerived :: CtFlavor -> Bool
+isDerived :: CtEvidence -> Bool
 isDerived (Derived {}) = True
 isDerived _             = False
 
-canSolve :: CtFlavor -> CtFlavor -> Bool
+canSolve :: CtEvidence -> CtEvidence -> 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.
@@ -1325,18 +1317,13 @@ canSolve (Wanted {})  (Wanted {})  = True
 canSolve (Derived {}) (Derived {}) = True  -- Derived can't solve wanted/given
 canSolve _ _ = False                      -- No evidence for a derived, anyway
 
-canRewrite :: CtFlavor -> CtFlavor -> Bool 
+canRewrite :: CtEvidence -> CtEvidence -> Bool 
 -- canRewrite ct1 ct2 
 -- The equality constraint ct1 can be used to rewrite inside ct2 
 canRewrite = canSolve 
 
-
 mkGivenLoc :: WantedLoc -> SkolemInfo -> GivenLoc
 mkGivenLoc wl sk = setCtLocOrigin wl sk
-
-mkSolvedLoc :: WantedLoc -> SkolemInfo -> GivenLoc
-mkSolvedLoc wl sk = setCtLocOrigin wl sk
-
 \end{code}
 
 %************************************************************************
index ca7cf88..5b7d650 100644 (file)
@@ -24,15 +24,13 @@ module TcSMonad (
     Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, tyVarsOfCDicts, 
     emitFrozenError,
 
-    isWanted, isGivenOrSolved, isDerived,
-    isGivenOrSolvedCt, isGivenCt, 
-    isWantedCt, isDerivedCt, pprFlavorArising,
+    isWanted, isDerived, 
+    isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
 
     isFlexiTcsTv,
 
     canRewrite, canSolve,
-    mkSolvedLoc, mkGivenLoc,
-    ctWantedLoc,
+    mkGivenLoc, ctWantedLoc,
 
     TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality 
     traceFireTcS, bumpStepCountTcS, doWithInert,
@@ -42,16 +40,17 @@ module TcSMonad (
     SimplContext(..), isInteractive, performDefaulting,
 
     -- Getting and setting the flattening cache
-    getFlatCache, updFlatCache, addToSolved, 
+    getFlatCache, updFlatCache, addToSolved, addSolvedFunEq,
     
     deferTcSForAllEq, 
     
     setEvBind,
     XEvTerm(..),
-    MaybeNew (..), isFresh,
-    xCtFlavor, -- Transform a CtFlavor during a step 
+    MaybeNew (..), isFresh, freshGoals, getEvTerms,
+
+    xCtFlavor, -- Transform a CtEvidence during a step 
     rewriteCtFlavor,          -- Specialized version of xCtFlavor for coercions
-    newWantedEvVar, newGivenEvVar, instDFunConstraints, newKindConstraint,
+    newWantedEvVar, instDFunConstraints, newKindConstraint,
     newDerived,
     xCtFlavor_cache, rewriteCtFlavor_cache,
     
@@ -68,12 +67,14 @@ module TcSMonad (
         -- Inerts 
     InertSet(..), InertCans(..), 
     getInertEqs, getCtCoercion,
-    emptyInert, getTcSInerts, lookupInInerts, updInertSet, extractUnsolved,
+    emptyInert, getTcSInerts, lookupInInerts, 
+    extractUnsolved,
     extractUnsolvedTcS, modifyInertTcS,
     updInertSetTcS, partitionCCanMap, partitionEqMap,
     getRelevantCts, extractRelevantInerts,
-    CCanMap (..), CtTypeMap, CtFamHeadMap(..), CtPredMap(..),
-    pprCtTypeMap, partCtFamHeadMap,
+    CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
+    PredMap, FamHeadMap,
+    partCtFamHeadMap, lookupFamHead,
 
 
     instDFunType,                              -- Instantiation
@@ -136,14 +137,12 @@ import TcRnTypes
 
 import Unique 
 import UniqFM
-import Maybes ( orElse )
+import Maybes ( orElse, catMaybes )
 
 
 import Control.Monad( when )
 import StaticFlags( opt_PprStyle_Debug )
 import Data.IORef
-import Data.List ( find )
-import Control.Monad ( zipWithM )
 import TrieMap
 
 \end{code}
@@ -298,11 +297,10 @@ emptyCCanMap = CCanMap { cts_given = emptyUFM, cts_derived = emptyUFM, cts_wante
 
 updCCanMap:: Uniquable a => (a,Ct) -> CCanMap a -> CCanMap a 
 updCCanMap (a,ct) cmap 
-  = case cc_flavor ct of 
+  = case cc_ev ct of 
       Wanted {}  -> cmap { cts_wanted  = insert_into (cts_wanted cmap)  } 
       Given {}   -> cmap { cts_given   = insert_into (cts_given cmap)   }
       Derived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
-      Solved {}  -> panic "updCCanMap update with solved!" 
   where 
     insert_into m = addToUFM_C unionBags m a (singleCt ct)
 
@@ -319,13 +317,24 @@ getRelevantCts a cmap
   where
     lookup map = lookupUFM map a `orElse` emptyCts
 
-lookupCCanMap :: Uniquable a => a -> (Ct -> Bool) -> CCanMap a -> Maybe Ct
-lookupCCanMap a p map
-   = let possible_cts = lookupUFM (cts_given map)   a `orElse` 
-                        lookupUFM (cts_wanted map)  a `orElse` 
-                        lookupUFM (cts_derived map) a `orElse` emptyCts
-     in find p (bagToList possible_cts)
+lookupCCanMap :: Uniquable a => a -> (CtEvidence -> Bool) -> CCanMap a -> Maybe CtEvidence
+lookupCCanMap a pick_me map
+  = findEvidence pick_me possible_cts
+  where
+     possible_cts = lookupUFM (cts_given map)   a `plus` (
+                    lookupUFM (cts_wanted map)  a `plus` (
+                    lookupUFM (cts_derived map) a `plus` emptyCts))
 
+     plus Nothing     cts2 = cts2
+     plus (Just cts1) cts2 = cts1 `unionBags` cts2
+
+findEvidence :: (CtEvidence -> Bool) -> Cts -> Maybe CtEvidence
+findEvidence pick_me cts
+  = foldrBag pick Nothing cts
+  where
+     pick :: Ct -> Maybe CtEvidence -> Maybe CtEvidence
+     pick ct deflt | let ctev = cc_ev ct, pick_me ctev = Just ctev
+                   | otherwise                             = deflt
 
 partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a) 
 -- All constraints that /match/ the predicate go in the bag, the rest remain in the map
@@ -360,27 +369,33 @@ extractUnsolvedCMap cmap =
 
 
 -- Maps from PredTypes to Constraints
-type CtTypeMap = TypeMap Ct
-newtype CtPredMap = 
-  CtPredMap { unCtPredMap :: CtTypeMap }       -- Indexed by TcPredType
-newtype CtFamHeadMap = 
-  CtFamHeadMap { unCtFamHeadMap :: CtTypeMap } -- Indexed by family head
+type CtTypeMap    = TypeMap    Ct
+type CtPredMap    = PredMap    Ct
+type CtFamHeadMap = FamHeadMap Ct
+
+newtype PredMap    a = PredMap    { unPredMap    :: TypeMap a } -- Indexed by TcPredType
+newtype FamHeadMap a = FamHeadMap { unFamHeadMap :: TypeMap a } -- Indexed by family head
 
-pprCtTypeMap :: TypeMap Ct -> SDoc 
-pprCtTypeMap ctmap = ppr (foldTM (:) ctmap [])
+instance Outputable a => Outputable (PredMap a) where
+   ppr (PredMap m) = ppr (foldTM (:) m [])
+
+instance Outputable a => Outputable (FamHeadMap a) where
+   ppr (FamHeadMap m) = ppr (foldTM (:) m [])
 
 ctTypeMapCts :: TypeMap Ct -> Cts
 ctTypeMapCts ctmap = foldTM (\ct cts -> extendCts cts ct) ctmap emptyCts
 
+lookupFamHead :: FamHeadMap a -> TcType -> Maybe a
+lookupFamHead (FamHeadMap m) key = lookupTM key m
 
 partCtFamHeadMap :: (Ct -> Bool) 
                  -> CtFamHeadMap 
                  -> (Cts, CtFamHeadMap)
 partCtFamHeadMap f ctmap
   = let (cts,tymap_final) = foldTM upd_acc tymap_inside (emptyBag, tymap_inside)
-    in (cts, CtFamHeadMap tymap_final)
+    in (cts, FamHeadMap tymap_final)
   where
-    tymap_inside = unCtFamHeadMap ctmap 
+    tymap_inside = unFamHeadMap ctmap 
     upd_acc ct (cts,acc_map)
          | f ct      = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map)
          | otherwise = (cts,acc_map)
@@ -388,8 +403,6 @@ partCtFamHeadMap f ctmap
                       = ty1 
                       | otherwise 
                       = panic "partCtFamHeadMap, encountered non equality!"
-
-
 \end{code}
 
 %************************************************************************
@@ -400,9 +413,7 @@ partCtFamHeadMap f ctmap
 %************************************************************************
 
 \begin{code}
-
-
--- All Given (fully known) or Wanted or Derived, never Solved
+-- All Given (fully known) or Wanted or Derived
 -- See Note [Detailed InertCans Invariants] for more
 data InertCans 
   = IC { inert_eqs :: TyVarEnv Ct
@@ -467,29 +478,51 @@ The InertCans represents a collection of constraints with the following properti
          occurs errors. 
 
   9 Given family or dictionary constraints don't mention touchable unification variables
-\begin{code}
 
+Note [Solved constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+When we take a step to simplify a constraint 'c', we call the original constraint "solved".
+For example:   Wanted:    ev  :: [s] ~ [t]
+               New goal:  ev1 :: s ~ t
+               Then 'ev' is now "solved".
+
+The reason for all this is simply to avoid re-solving goals we have solved already.
+
+* A solved Wanted may depend on as-yet-unsolved goals, so (for example) we should not
+  use it to rewrite a Given; in that sense the solved goal is still a Wanted
+
+* A solved Given is just given
+
+* A solved Derived is possible; purpose is to avoid creating tons of identical
+  Derived goals.
 
+
+\begin{code}
 -- The Inert Set
 data InertSet
   = IS { inert_cans :: InertCans
-              -- Canonical Given,Wanted,Solved
+              -- Canonical Given, Wanted, Derived (no Solved)
+             -- Sometimes called "the inert set"
+
        , inert_frozen :: Cts       
               -- Frozen errors (as non-canonicals)
                                
-       , inert_solved :: CtPredMap
-              -- Solved constraints (for caching): 
-              -- (i) key is by predicate type
-              -- (ii) all of 'Solved' flavor, may or may not be canonicals
-              -- (iii) we use this field for avoiding creating newEvVars
        , inert_flat_cache :: CtFamHeadMap 
               -- All ``flattening equations'' are kept here. 
               -- Always canonical CTyFunEqs (Given or Wanted only!)
-              -- Key is by family head. We used this field during flattening only
-       , inert_solved_funeqs :: CtFamHeadMap
-              -- Memoized Solved family equations co :: F xis ~ xi
-              -- Stored not necessarily as fully rewritten; we'll do that lazily
-              -- when we lookup
+              -- Key is by family head. We use this field during flattening only
+              -- Not necessarily inert wrt top-level equations (or inert_cans)
+
+       , inert_solved_funeqs :: FamHeadMap CtEvidence  -- Of form co :: F xis ~ xi
+       , inert_solved        :: PredMap    CtEvidence  -- All others
+                     -- These two fields constitute a cache of solved (only!) constraints
+              -- See Note [Solved constraints]
+                     -- * Constraints of form (F xis ~ xi) live in inert_solved_funeqs, 
+                     --   all the others are in inert_solved
+                     -- * Used to avoid creating a new EvVar when we have a new goal that we
+                     --   have solvedin the past
+                     -- * Stored not necessarily as fully rewritten 
+                     --   (ToDo: rewrite lazily when we lookup)
        }
 
 
@@ -498,7 +531,7 @@ instance Outputable InertCans where
                  , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics)))
                  , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips ics))) 
                  , vcat (map ppr (Bag.bagToList $ 
-                                  ctTypeMapCts (unCtFamHeadMap $ inert_funeqs ics)))
+                                  ctTypeMapCts (unFamHeadMap $ inert_funeqs ics)))
                  , vcat (map ppr (Bag.bagToList $ inert_irreds ics))
                  ]
             
@@ -508,7 +541,7 @@ instance Outputable InertSet where
                     braces (vcat (map ppr (Bag.bagToList $ inert_frozen is)))
                 , text "Solved and cached" <+>
                     int (foldTypeMap (\_ x -> x+1) 0 
-                             (unCtPredMap $ inert_solved is)) <+> 
+                             (unPredMap $ inert_solved is)) <+> 
                     text "more constraints" ]
 
 emptyInert :: InertSet
@@ -517,28 +550,27 @@ emptyInert
                          , inert_eq_tvs = emptyInScopeSet
                          , inert_dicts  = emptyCCanMap
                          , inert_ips    = emptyCCanMap
-                         , inert_funeqs = CtFamHeadMap emptyTM 
+                         , inert_funeqs = FamHeadMap emptyTM 
                          , inert_irreds = emptyCts }
        , inert_frozen        = emptyCts
-       , inert_flat_cache    = CtFamHeadMap emptyTM
-       , inert_solved        = CtPredMap emptyTM 
-       , inert_solved_funeqs = CtFamHeadMap emptyTM }
+       , inert_flat_cache    = FamHeadMap emptyTM
+       , inert_solved        = PredMap emptyTM 
+       , inert_solved_funeqs = FamHeadMap emptyTM }
 
-type AtomicInert = Ct 
-
-updInertSet :: InertSet -> AtomicInert -> InertSet 
--- Add a new inert element to the inert set. 
-updInertSet is item 
-  | isSolved (cc_flavor item)
-    -- Solved items go in their special place
-  = let pty = ctPred item
+updSolvedSet :: InertSet -> CtEvidence -> InertSet 
+updSolvedSet is item 
+  = let pty = ctEvPred item
         upd_solved Nothing = Just item
         upd_solved (Just _existing_solved) = Just item 
                -- .. or Just existing_solved? Is this even possible to happen?
     in is { inert_solved = 
-               CtPredMap $ 
-               alterTM pty upd_solved (unCtPredMap $ inert_solved is) }
+               PredMap $ 
+               alterTM pty upd_solved (unPredMap $ inert_solved is) }
+
 
+updInertSet :: InertSet -> Ct -> InertSet 
+-- Add a new inert element to the inert set. 
+updInertSet is item 
   | isCNonCanonical item 
     -- NB: this may happen if we decide to kick some frozen error 
     -- out to rewrite him. Frozen errors are just NonCanonicals
@@ -548,7 +580,7 @@ updInertSet is item
     -- A canonical Given, Wanted, or Derived
   = is { inert_cans = upd_inert_cans (inert_cans is) item }
   
-  where upd_inert_cans :: InertCans -> AtomicInert -> InertCans
+  where upd_inert_cans :: InertCans -> Ct -> InertCans
         -- Precondition: item /is/ canonical
         upd_inert_cans ics item
           | isCTyEqCan item                     
@@ -578,14 +610,14 @@ updInertSet is item
                 upd_funeqs Nothing = Just item
                 upd_funeqs (Just _already_there) 
                   = panic "updInertSet: item already there!"
-            in ics { inert_funeqs = CtFamHeadMap 
+            in ics { inert_funeqs = FamHeadMap 
                                       (alterTM fam_head upd_funeqs $ 
-                                         (unCtFamHeadMap $ inert_funeqs ics)) }
+                                         (unFamHeadMap $ inert_funeqs ics)) }
           | otherwise
           = pprPanic "upd_inert set: can't happen! Inserting " $ 
             ppr item 
 
-updInertSetTcS :: AtomicInert -> TcS ()
+updInertSetTcS :: Ct -> TcS ()
 -- Add a new item in the inerts of the monad
 updInertSetTcS item
   = do { traceTcS "updInertSetTcs {" $ 
@@ -596,6 +628,32 @@ updInertSetTcS item
        ; traceTcS "updInertSetTcs }" $ empty }
 
 
+addToSolved :: CtEvidence -> TcS ()
+-- Add a new item in the solved set of the monad
+addToSolved item
+  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
+  = return () 
+  | otherwise
+  = do { traceTcS "updSolvedSetTcs {" $ 
+         text "Trying to insert new solved item:" <+> ppr item
+
+       ; modifyInertTcS (\is -> ((), updSolvedSet is item)) 
+                        
+       ; traceTcS "updSolvedSetTcs }" $ empty }
+
+addSolvedFunEq :: CtEvidence -> TcS ()
+addSolvedFunEq fun_eq
+  = modifyInertTcS $ \inert -> ((), upd_inert inert)
+  where 
+    upd_inert inert 
+      = let slvd = unFamHeadMap (inert_solved_funeqs inert)
+        in inert { inert_solved_funeqs =
+                      FamHeadMap (alterTM key upd_funeqs slvd) }       
+    upd_funeqs Nothing    = Just fun_eq
+    upd_funeqs (Just _ct) = Just fun_eq 
+         -- Or _ct? depends on which caches more steps of computation
+    key = ctEvPred fun_eq
+
 modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a 
 -- Modify the inert set with the supplied function
 modifyInertTcS upd 
@@ -606,20 +664,10 @@ modifyInertTcS upd
        ; return a }
 
 
-addToSolved :: Ct -> TcS ()
--- Don't do any caching for IP preds because of delicate shadowing
-addToSolved ct
-  | isIPPred (ctPred ct)  
-  = return () 
-  | otherwise
-  = ASSERT ( isSolved (cc_flavor ct) )
-    updInertSetTcS ct
-
 extractUnsolvedTcS :: TcS (Cts,Cts) 
 -- Extracts frozen errors and remaining unsolved and sets the 
 -- inert set to be the remaining! 
-extractUnsolvedTcS = 
-  modifyInertTcS extractUnsolved 
+extractUnsolvedTcS = modifyInertTcS extractUnsolved 
 
 extractUnsolved :: InertSet -> ((Cts,Cts), InertSet)
 -- Postcondition
@@ -660,22 +708,20 @@ extractUnsolved (IS { inert_cans = IC { inert_eqs    = eqs
                               -- At some point, I used to flush all the solved, in 
                               -- fear of evidence loops. But I think we are safe, 
                               -- flushing is why T3064 had become slower
-                        , inert_solved        = solved      -- CtPredMap emptyTM
-                        , inert_flat_cache    = flat_cache  -- CtFamHeadMap emptyTM
-                        , inert_solved_funeqs = funeq_cache -- CtFamHeadMap emptyTM
+                        , inert_solved        = solved      -- PredMap emptyTM
+                        , inert_flat_cache    = flat_cache  -- FamHeadMap emptyTM
+                        , inert_solved_funeqs = funeq_cache -- FamHeadMap emptyTM
                         }
     in ((frozen, unsolved), is_solved)
 
-  where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenOrSolvedCt ct) eqs
+  where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
         unsolved_eqs = foldVarEnv (\ct cts -> cts `extendCts` ct) emptyCts $
                        eqs `minusVarEnv` solved_eqs
 
-        (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenOrSolvedCt) irreds
+        (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenCt) irreds
         (unsolved_ips, solved_ips)       = extractUnsolvedCMap ips
         (unsolved_dicts, solved_dicts)   = extractUnsolvedCMap dicts
-
-        (unsolved_funeqs, solved_funeqs) = 
-          partCtFamHeadMap (not . isGivenOrSolved . cc_flavor) funeqs
+        (unsolved_funeqs, solved_funeqs) = partCtFamHeadMap (not . isGivenCt) funeqs
 
         unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
                    unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
@@ -697,7 +743,7 @@ extractRelevantInerts wi
             in (cts, ics { inert_dicts = dict_map })
         extract_ics_relevants ct@(CFunEqCan {}) ics = 
             let (cts,feqs_map)  = 
-                  let funeq_map = unCtFamHeadMap $ inert_funeqs ics
+                  let funeq_map = unFamHeadMap $ inert_funeqs ics
                       fam_head = mkTyConApp (cc_fun ct) (cc_tyargs ct)
                       lkp = lookupTM fam_head funeq_map
                       new_funeq_map = alterTM fam_head xtm funeq_map
@@ -706,7 +752,7 @@ extractRelevantInerts wi
                   in case lkp of 
                     Nothing -> (emptyCts, funeq_map)
                     Just ct -> (singleCt ct, new_funeq_map)
-            in (cts, ics { inert_funeqs = CtFamHeadMap feqs_map })
+            in (cts, ics { inert_funeqs = FamHeadMap feqs_map })
         extract_ics_relevants (CIPCan { cc_ip_nm = nm } ) ics = 
             let (cts, ips_map) = getRelevantCts nm (inert_ips ics) 
             in (cts, ics { inert_ips = ips_map })
@@ -716,36 +762,40 @@ extractRelevantInerts wi
         extract_ics_relevants _ ics = (emptyCts,ics)
         
 
-lookupInInerts :: InertSet -> TcPredType -> Maybe Ct
+lookupInInerts :: InertSet -> TcPredType -> Maybe CtEvidence
 -- Is this exact predicate type cached in the solved or canonicals of the InertSet
 lookupInInerts (IS { inert_solved = solved, inert_cans = ics }) pty
   = case lookupInSolved solved pty of
-      Just ct -> return ct
-      Nothing -> lookupInInertCans ics pty
+      Just ctev -> return ctev
+      Nothing   -> lookupInInertCans ics pty
 
-lookupInSolved :: CtPredMap -> TcPredType -> Maybe Ct
+lookupInSolved :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
 -- Returns just if exactly this predicate type exists in the solved.
-lookupInSolved tm pty = lookupTM pty $ unCtPredMap tm
+lookupInSolved tm pty = lookupTM pty $ unPredMap tm
 
-lookupInInertCans :: InertCans -> TcPredType -> Maybe Ct
+lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence
 -- Returns Just if exactly this pred type exists in the inert canonicals
 lookupInInertCans ics pty
-  = lkp_ics (classifyPredType pty)
-  where lkp_ics (ClassPred cls _)
-          = lookupCCanMap cls (\ct -> ctPred ct `eqType` pty) (inert_dicts ics)
-        lkp_ics (EqPred ty1 _ty2)
-          | Just tv <- getTyVar_maybe ty1
-          , Just ct <- lookupVarEnv (inert_eqs ics) tv
-          , ctPred ct `eqType` pty
-          = Just ct
-        lkp_ics (EqPred ty1 _ty2) -- Family equation
-          | Just _ <- splitTyConApp_maybe ty1
-          , Just ct <- lookupTM ty1 (unCtFamHeadMap $ inert_funeqs ics)
-          , ctPred ct `eqType` pty
-          = Just ct
-        lkp_ics (IrredPred {}) 
-          = find (\ct -> ctPred ct `eqType` pty) (bagToList (inert_irreds ics))
-        lkp_ics _ = Nothing -- NB: No caching for IPs
+  = case (classifyPredType pty) of
+      ClassPred cls _ 
+         -> lookupCCanMap cls (\ct -> ctEvPred ct `eqType` pty) (inert_dicts ics)
+
+      EqPred ty1 _ty2 
+         | Just tv <- getTyVar_maybe ty1      -- Tyvar equation
+         , Just ct <- lookupVarEnv (inert_eqs ics) tv
+        , let ctev = ctEvidence ct
+        , ctEvPred ctev `eqType` pty
+        -> Just ctev
+
+        | Just _ <- splitTyConApp_maybe ty1  -- Family equation
+        , Just ct <- lookupTM ty1 (unFamHeadMap $ inert_funeqs ics)
+        , let ctev = ctEvidence ct
+        , ctEvPred ctev `eqType` pty
+        -> Just ctev
+
+      IrredPred {} -> findEvidence (\ct -> ctEvPred ct `eqType` pty) (inert_irreds ics)
+    
+      _other -> Nothing -- NB: No caching for IPs
 \end{code}
 
 
@@ -1038,13 +1088,13 @@ emitTcSImplication :: Implication -> TcS ()
 emitTcSImplication imp = updTcSImplics (consBag imp)
 
 
-emitFrozenError :: CtFlavor -> SubGoalDepth -> TcS ()
+emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts. 
 emitFrozenError fl depth 
-  = do { traceTcS "Emit frozen error" (ppr (ctFlavPred fl))
+  = do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
        ; inert_ref <- getTcSInertsRef 
        ; inerts <- wrapTcS (TcM.readTcRef inert_ref)
-       ; let ct = CNonCanonical { cc_flavor = fl
+       ; let ct = CNonCanonical { cc_ev = fl
                                 , cc_depth = depth } 
              inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct } 
        ; wrapTcS (TcM.writeTcRef inert_ref inerts_new) }
@@ -1059,24 +1109,23 @@ getTcEvBinds :: TcS EvBindsVar
 getTcEvBinds = TcS (return . tcs_ev_binds) 
 
 getFlatCache :: TcS CtTypeMap 
-getFlatCache = getTcSInerts >>= (return . unCtFamHeadMap . inert_flat_cache)
+getFlatCache = getTcSInerts >>= (return . unFamHeadMap . inert_flat_cache)
 
 updFlatCache :: Ct -> TcS ()
 -- Pre: constraint is a flat family equation (equal to a flatten skolem)
-updFlatCache flat_eq@(CFunEqCan { cc_flavor = fl, cc_fun = tc, cc_tyargs = xis })
+updFlatCache flat_eq@(CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = xis })
   = modifyInertTcS upd_inert_cache
-  where upd_inert_cache is = ((), is { inert_flat_cache = CtFamHeadMap new_fc })
+  where upd_inert_cache is = ((), is { inert_flat_cache = FamHeadMap new_fc })
                            where new_fc = alterTM pred_key upd_cache fc
-                                 fc = unCtFamHeadMap $ inert_flat_cache is
+                                 fc = unFamHeadMap $ inert_flat_cache is
         pred_key = mkTyConApp tc xis
-        upd_cache (Just ct) | cc_flavor ct `canSolve` fl = Just ct 
+        upd_cache (Just ct) | cc_ev ct `canSolve` fl = Just ct 
         upd_cache (Just _ct) = Just flat_eq 
         upd_cache Nothing    = Just flat_eq
 updFlatCache other_ct = pprPanic "updFlatCache: non-family constraint" $
                         ppr other_ct
                         
 
-
 getUntouchables :: TcS TcsUntouchables
 getUntouchables = TcS (return . tcs_untch)
 
@@ -1296,142 +1345,176 @@ instFlexiTcSHelper tvname tvkind
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 data XEvTerm = 
-  XEvTerm { ev_comp   :: [EvVar] -> EvTerm
+  XEvTerm { ev_comp   :: [EvTerm] -> EvTerm
                          -- How to compose evidence 
-          , ev_decomp :: EvVar -> [EvTerm]
+          , ev_decomp :: EvTerm -> [EvTerm]
                          -- How to decompose evidence 
           }
 
-data MaybeNew a = Fresh  { mn_thing :: a } 
-                | Cached { mn_thing :: a }
+data MaybeNew = Fresh CtEvidence | Cached EvTerm
 
-isFresh :: MaybeNew -> Bool
+isFresh :: MaybeNew -> Bool
 isFresh (Fresh {}) = True
 isFresh _ = False
 
+getEvTerm :: MaybeNew -> EvTerm
+getEvTerm (Fresh ctev) = ctEvTerm ctev
+getEvTerm (Cached tm)  = tm
+
+getEvTerms :: [MaybeNew] -> [EvTerm]
+getEvTerms = map getEvTerm
+
+freshGoals :: [MaybeNew] -> [CtEvidence]
+freshGoals mns = [ ctev | Fresh ctev <- mns ]
+
 setEvBind :: EvVar -> EvTerm -> TcS ()
-setEvBind ev t
+setEvBind the_ev t
   = do { tc_evbinds <- getTcEvBinds
-       ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t
+       ; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev t
 
-       ; traceTcS "setEvBind" $ vcat [ text "ev =" <+> ppr ev
+       ; traceTcS "setEvBind" $ vcat [ text "ev =" <+> ppr the_ev
                                      , text "t  =" <+> ppr t ]
 
 #ifndef DEBUG
        ; return () }
 #else
        ; binds <- getTcEvBindsMap
-       ; let cycle = any (reaches binds) (evVarsOfTerm t)
+       ; let cycle = reaches_tm binds t
        ; when cycle (fail_if_co_loop binds) }
 
   where fail_if_co_loop binds
-          = do { traceTcS "Cycle in evidence binds" $ vcat [ text "evvar =" <+> ppr ev
+          = do { traceTcS "Cycle in evidence binds" $ vcat [ text "evvar =" <+> ppr the_ev
                                                            , ppr (evBindMapBinds binds) ]
-               ; when (isEqVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!")) }
+               ; when (isEqVar the_ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!")) }
+
+        reaches_tm :: EvBindMap -> EvTerm -> Bool
+        -- Does any free variable of 'tm' reach 'the_ev'
+        reaches_tm ebm tm = foldVarSet ((||) . reaches ebm) False (evVarsOfTerm tm)
 
         reaches :: EvBindMap -> Var -> Bool 
-        -- Does this evvar reach ev? 
-        reaches ebm ev0 = go ev0
-          where go ev0
-                  | ev0 == ev = True
-                  | Just (EvBind _ evtrm) <- lookupEvBind ebm ev0
-                  = any go (evVarsOfTerm evtrm)
-                  | otherwise = False
+        -- Does this evvar reach the_ev? 
+        reaches ebm ev 
+          | ev == the_ev                                 = True
+          | Just (EvBind _ evtrm) <- lookupEvBind ebm ev = reaches_tm ebm evtrm
+          | otherwise                                    = False
 #endif
 
-newGivenEvVar  :: TcPredType -> EvTerm -> TcS (MaybeNew EvVar)
-newGivenEvVar pty evterm
-  = do { is <- getTcSInerts
-       ; case lookupInInerts is pty of
-            Just ct | isGivenOrSolvedCt ct 
-                    -> return (Cached (ctId ct))
-            _ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
-                    ; setEvBind new_ev evterm
-                    ; return (Fresh new_ev) } }
-
-newWantedEvVar :: TcPredType -> TcS (MaybeNew EvVar)
-newWantedEvVar pty
+newWantedEvVar :: WantedLoc -> TcPredType -> TcS MaybeNew
+newWantedEvVar loc pty
   = do { is <- getTcSInerts
        ; case lookupInInerts is pty of
-            Just ct | not (isDerivedCt ct
-                    -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ct
-                          ; return (Cached (ctId ct)) }
+            Just ctev | not (isDerived ctev
+                      -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
+                            ; return (Cached (ctEvTerm ctev)) }
             _ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
                     ; traceTcS "newWantedEvVar/cache miss" $ ppr new_ev
-                    ; return (Fresh new_ev) } }
-
-newDerived :: TcPredType -> TcS (MaybeNew TcPredType)
-newDerived pty
+                    ; let ctev = Wanted { ctev_wloc = loc
+                                        , ctev_pred = pty
+                                        , ctev_evar = new_ev }
+                    ; return (Fresh ctev) } }
+
+newDerived :: WantedLoc -> TcPredType -> TcS (Maybe CtEvidence)
+-- Returns Nothing    if cached, 
+--         Just pred  if not cached
+newDerived loc pty
   = do { is <- getTcSInerts
        ; case lookupInInerts is pty of
-            Just {} -> return (Cached pty)
-            _       -> return (Fresh pty) }
+            Just {} -> return Nothing
+            _       -> return (Just Derived { ctev_wloc = loc
+                                            , ctev_pred = pty }) }
     
-newKindConstraint :: TcTyVar -> Kind -> TcS (MaybeNew EvVar)
+newKindConstraint :: WantedLoc -> TcTyVar -> Kind -> TcS MaybeNew
 -- Create new wanted CoVar that constrains the type to have the specified kind. 
-newKindConstraint tv knd
+newKindConstraint loc tv knd
   = do { ty_k <- wrapTcS (instFlexiTcSHelper (tyVarName tv) knd)
-       ; newWantedEvVar (mkTcEqPred (mkTyVarTy tv) ty_k) }
-
-instDFunConstraints :: TcThetaType -> TcS [MaybeNew EvVar]
-instDFunConstraints = mapM newWantedEvVar
+       ; newWantedEvVar loc (mkTcEqPred (mkTyVarTy tv) ty_k) }
 
+instDFunConstraints :: WantedLoc -> TcThetaType -> TcS [MaybeNew]
+instDFunConstraints wl = mapM (newWantedEvVar wl)
+\end{code}
                 
-xCtFlavor :: CtFlavor              -- Original flavor   
+
+Note [xCFlavor]
+~~~~~~~~~~~~~~~
+A call might look like this:
+
+    xCtFlavor ev subgoal-preds evidence-transformer
+
+  ev is Given   => use ev_decomp to create new Givens for subgoal-preds, 
+                   and return them
+
+  ev is Wanted  => create new wanteds for subgoal-preds, 
+                   use ev_comp to bind ev, 
+                   return fresh wanteds (ie ones not cached in inert_cans or solved)
+
+  ev is Derived => create new deriveds for subgoal-preds 
+                      (unless cached in inert_cans or solved)
+
+Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
+      Ones that are already cached are not returned
+
+Example
+    ev : Tree a b ~ Tree c d
+    xCtFlavor ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
+                                     , ev_decomp = \c. [nth 1 c, nth 2 c] })
+              (\fresh-goals.  stuff)
+
+\begin{code}
+xCtFlavor :: CtEvidence              -- Original flavor   
           -> [TcPredType]          -- New predicate types
           -> XEvTerm               -- Instructions about how to manipulate evidence
-          -> ([CtFlavor] -> TcS a) -- What to do with any remaining /fresh/ goals!
-          -> TcS a
+          -> TcS [CtEvidence]
 xCtFlavor = xCtFlavor_cache True          
 
-
 xCtFlavor_cache :: Bool            -- True = if wanted add to the solved bag!    
-          -> CtFlavor              -- Original flavor   
+          -> CtEvidence            -- Original flavor   
           -> [TcPredType]          -- New predicate types
           -> XEvTerm               -- Instructions about how to manipulate evidence
-          -> ([CtFlavor] -> TcS a) -- What to do with any remaining /fresh/ goals!
-          -> TcS a
-xCtFlavor_cache _ (Given { flav_gloc = gl, flav_evar = evar }) ptys xev cont_with
-  = do { let ev_trms = ev_decomp xev evar
-       ; new_evars <- zipWithM newGivenEvVar ptys ev_trms
-       ; cont_with $
-         map (\x -> Given gl (mn_thing x)) (filter isFresh new_evars) }
+          -> TcS [CtEvidence]
+xCtFlavor_cache _ (Given { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
+  = return [ Given { ctev_gloc = gl, ctev_pred = pred, ctev_evtm = sub_tm } 
+           | (pred, sub_tm) <- zipEqual "xCtFlavor" ptys (ev_decomp xev tm) ]
+    -- ToDo: consider creating new evidence variables for superclasses
   
-xCtFlavor_cache cache (Wanted { flav_wloc = wl, flav_evar = evar }) ptys xev cont_with
-  = do { new_evars <- mapM newWantedEvVar ptys
-       ; let evars  = map mn_thing new_evars
-             evterm = ev_comp xev evars
-       ; setEvBind evar evterm
-       ; let solved_flav = Solved { flav_gloc = mkSolvedLoc wl UnkSkol
-                                  , flav_evar = evar }
-       ; when cache $ addToSolved (mkNonCanonical solved_flav)
-       ; cont_with $
-         map (\x -> Wanted wl (mn_thing x)) (filter isFresh new_evars) }
-    
-xCtFlavor_cache _ (Derived { flav_wloc = wl }) ptys _xev cont_with
-  = do { ders <- mapM newDerived ptys
-       ; cont_with $ 
-         map (\x -> Derived wl (mn_thing x)) (filter isFresh ders) }
+xCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
+  = do { new_evars <- mapM (newWantedEvVar wl) ptys
+       ; setEvBind evar (ev_comp xev (getEvTerms new_evars))
+
+           -- Add the now-solved wanted constraint to the cache
+       ; when cache $ addToSolved ctev
+
+       ; return (freshGoals new_evars) }
     
-    -- I am not sure I actually want to do this (e.g. from recanonicalizing a solved?)
-    -- but if we plan to use xCtFlavor for rewriting as well then I might as well add a case
-xCtFlavor_cache _ (Solved { flav_gloc = gl, flav_evar = evar }) ptys xev cont_with
-  = do { let ev_trms = ev_decomp xev evar
-       ; new_evars <- zipWithM newGivenEvVar ptys ev_trms
-       ; cont_with $
-         map (\x -> Solved gl (mn_thing x)) (filter isFresh new_evars) }
-
-rewriteCtFlavor :: CtFlavor
+xCtFlavor_cache _ (Derived { ctev_wloc = wl }) ptys _xev
+  = do { ders <- mapM (newDerived wl) ptys
+       ; return (catMaybes ders) }
+
+-----------------------------
+rewriteCtFlavor :: CtEvidence
                 -> TcPredType   -- new predicate
                 -> TcCoercion   -- new ~ old     
-                -> TcS (Maybe CtFlavor)
---      rewriteCtFlavor old_fl new_pred co
--- Main purpose: create a new identity (flavor) for new_pred;
---               unless new_pred is cached already
--- * Returns a new_fl : new_pred, with same wanted/given/derived flag as old_fl
--- * If old_fl was wanted, create a binding for old_fl, in terms of new_fl
--- * If old_fl was given, AND not cached, create a binding for new_fl, in terms of old_fl
--- * Returns Nothing if new_fl is already cached
+                -> TcS (Maybe CtEvidence)
+{- 
+     rewriteCtFlavor old_fl new_pred co
+Main purpose: create a new identity (flavor) for new_pred;
+              unless new_pred is cached already
+* Returns a new_fl : new_pred, with same wanted/given/derived flag as old_fl
+* If old_fl was wanted, create a binding for old_fl, in terms of new_fl
+* If old_fl was given, AND not cached, create a binding for new_fl, in terms of old_fl
+* Returns Nothing if new_fl is already cached
+
+
+        Old evidence    New predicate is               Return new evidence
+        flavour                                        of same flavor
+        -------------------------------------------------------------------
+        Wanted          Already solved or in inert     Nothing
+        or Derived      Not                            Just new_evidence
+
+        Given           Already in inert               Nothing
+                        Not                            Just new_evidence
+
+        Solved          NEVER HAPPENS
+-}
 
 rewriteCtFlavor = rewriteCtFlavor_cache True
 -- Returns Just new_fl iff either (i)  'co' is reflexivity
@@ -1439,40 +1522,40 @@ rewriteCtFlavor = rewriteCtFlavor_cache True
 -- In either case, there is nothing new to do with new_fl
 
 rewriteCtFlavor_cache :: Bool 
-                -> CtFlavor
+                -> CtEvidence
                 -> TcPredType   -- new predicate
                 -> TcCoercion   -- new ~ old     
-                -> TcS (Maybe CtFlavor)
+                -> TcS (Maybe CtEvidence)
 -- If derived, don't even look at the coercion
 -- NB: this allows us to sneak away with ``error'' thunks for 
 -- coercions that come from derived ids (which don't exist!) 
-rewriteCtFlavor_cache _cache (Derived wl _pty_orig) pty_new _co
-  = newDerived pty_new >>= from_mn
-  where from_mn (Cached {}) = return Nothing
-        from_mn (Fresh {})  = return $ Just (Derived wl pty_new)
+rewriteCtFlavor_cache _cache (Derived { ctev_wloc = wl }) pty_new _co
+  = newDerived wl pty_new
         
-rewriteCtFlavor_cache cache fl pty co
-  | isTcReflCo co
-  -- If just reflexivity then you may re-use the same variable as optimization
-  = if ctFlavPred fl `eqType` pty then 
-      -- E.g. for type synonyms we want to use the original type 
-      -- since it's not flattened to report better error messages.
-      return $ Just fl
-    else 
-      -- E.g. because we rewrite with a spontaneously solved one
-      return (Just $ case fl of
-                 Derived wl _pty_orig -> Derived wl pty
-                 Given gl ev  -> Given  gl (setVarType ev pty)
-                 Wanted wl ev -> Wanted wl (setVarType ev pty)
-                 Solved gl ev -> Solved gl (setVarType ev pty))
-  | otherwise 
-  = xCtFlavor_cache cache fl [pty] (XEvTerm ev_comp ev_decomp) cont
-  where ev_comp [x] = mkEvCast x co
-        ev_comp _   = panic "Coercion can only have one subgoal"
-        ev_decomp x = [mkEvCast x (mkTcSymCo co)]
-        cont []     = return Nothing
-        cont [fl]   = return $ Just fl
-        cont _      = panic "At most one constraint can be subgoal of coercion!"
+rewriteCtFlavor_cache _cache (Given { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
+  = return (Just (Given { ctev_gloc = gl, ctev_pred = pty_new, ctev_evtm = new_tm }))
+  where
+    new_tm = mkEvCast old_tm (mkTcSymCo co)  -- mkEvCase optimises ReflCo
+  
+rewriteCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = pty_old }) pty_new co
+  | isTcReflCo co  -- If just reflexivity then you may re-use the same variable
+  = return (Just (if pty_old `eqType` pty_new 
+                  then ctev 
+                  else ctev { ctev_pred = pty_new }))
+       -- If the old and new types compare equal (eqType looks through synonyms)
+       -- then retain the old type, so that error messages come out mentioning synonyms
+
+  | otherwise
+  = do { new_evar <- newWantedEvVar wl pty_new
+       ; setEvBind evar (mkEvCast (getEvTerm new_evar) co)
+
+           -- Add the now-solved wanted constraint to the cache
+       ; when cache $ addToSolved ctev
+
+       ; case new_evar of
+            Fresh ctev -> return (Just ctev) 
+            _          -> return Nothing }
+
 
 
 -- Matching and looking up classes and family instances
@@ -1537,29 +1620,29 @@ deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
             phi1 = Type.substTy subst1 body1
             phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
             skol_info = UnifyForAllSkol skol_tvs phi1
-        ; mev <- newWantedEvVar (mkTcEqPred phi1 phi2)
-        ; let new_fl = Wanted loc (mn_thing mev)
-              new_ct = mkNonCanonical new_fl
-              new_co = mkTcCoVarCo (mn_thing mev)
-        ; coe_inside <- if isFresh mev then
-                           do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds
-                              ; let ev_binds = TcEvBinds ev_binds_var
-                              ; lcl_env <- wrapTcS $ TcM.getLclTypeEnv
-                              ; loc <- wrapTcS $ TcM.getCtLoc skol_info
-                              ; let wc = WC { wc_flat  = singleCt new_ct 
-                                            , wc_impl  = emptyBag
-                                            , wc_insol = emptyCts }
-                                    imp = Implic { ic_untch  = all_untouchables
-                                                 , ic_env    = lcl_env
-                                                 , ic_skols  = skol_tvs
-                                                 , ic_given  = []
-                                                 , ic_wanted = wc 
-                                                 , ic_insol  = False
-                                                 , ic_binds  = ev_binds_var
-                                                 , ic_loc    = loc }
-                           ; updTcSImplics (consBag imp) 
-                           ; return (TcLetCo ev_binds new_co) }
-                        else (return new_co)
+        ; mev <- newWantedEvVar loc (mkTcEqPred phi1 phi2)
+        ; coe_inside <- case mev of
+            Cached ev_tm -> return (evTermCoercion ev_tm)
+            Fresh ctev   -> do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds
+                               ; let ev_binds = TcEvBinds ev_binds_var
+                                     new_ct = mkNonCanonical ctev
+                                    new_co = evTermCoercion (ctEvTerm ctev)
+                               ; lcl_env <- wrapTcS $ TcM.getLclTypeEnv
+                               ; loc <- wrapTcS $ TcM.getCtLoc skol_info
+                               ; let wc = WC { wc_flat  = singleCt new_ct 
+                                             , wc_impl  = emptyBag
+                                             , wc_insol = emptyCts }
+                                     imp = Implic { ic_untch  = all_untouchables
+                                                  , ic_env    = lcl_env
+                                                  , ic_skols  = skol_tvs
+                                                  , ic_given  = []
+                                                  , ic_wanted = wc 
+                                                  , ic_insol  = False
+                                                  , ic_binds  = ev_binds_var
+                                                  , ic_loc    = loc }
+                               ; updTcSImplics (consBag imp) 
+                               ; return (TcLetCo ev_binds new_co) }
+
         ; setEvBind orig_ev $
           EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs)
         }
@@ -1573,7 +1656,6 @@ deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
 -- Rewriting with respect to the inert equalities 
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 \begin{code}
-
 getInertEqs :: TcS (TyVarEnv Ct, InScopeSet)
 getInertEqs = do { inert <- getTcSInerts
                  ; let ics = inert_cans inert
@@ -1581,11 +1663,14 @@ getInertEqs = do { inert <- getTcSInerts
 
 getCtCoercion :: EvBindMap -> Ct -> TcCoercion
 -- Precondition: A CTyEqCan which is either Wanted or Given, never Derived or Solved!
-getCtCoercion bs ct 
+getCtCoercion _bs ct 
+  = ASSERT( not (isDerivedCt ct) )
+    evTermCoercion (ctEvTerm (ctEvidence ct))
+{-       ToDo: check with Dimitrios that we can dump this stuff
   = case lookupEvBind bs cc_id of
         -- Given and bound to a coercion term
       Just (EvBind _ (EvCoercion co)) -> co
-                      -- NB: The constraint could have been rewritten due to spontaneous 
+                -- NB: The constraint could have been rewritten due to spontaneous 
                 -- unifications but because we are optimizing away mkRefls the evidence
                 -- variable may still have type (alpha ~ [beta]). The constraint may 
                 -- however have a more accurate type (alpha ~ [Int]) (where beta ~ Int has
@@ -1596,6 +1681,9 @@ getCtCoercion bs ct
 
       _ -> mkTcCoVarCo (setVarType cc_id (ctPred ct))
       
-  where cc_id = ctId ct
-
+  where 
+    cc_id = ctId ct
+-}
 \end{code}
+
+
index e6a4fd2..f97347a 100644 (file)
@@ -558,7 +558,7 @@ simplifyRule name lhs_wanted rhs_wanted
                 -- variables; hence NoUntouchables
 
        ; (resid_wanted, _) <- runTcS (SimplInfer doc) untch emptyInert emptyWorkList $
-              solveWanteds zonked_all
+                              solveWanteds zonked_all
 
        ; zonked_lhs <- zonkWC lhs_wanted
 
@@ -579,7 +579,8 @@ simplifyRule name lhs_wanted rhs_wanted
          vcat [ text "zonked_lhs" <+> ppr zonked_lhs 
               , text "q_cts"      <+> ppr q_cts ]
 
-       ; return (map ctId (bagToList q_cts), zonked_lhs { wc_flat = non_q_cts }) }
+       ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
+                , zonked_lhs { wc_flat = non_q_cts }) }
 \end{code}
 
 
@@ -784,10 +785,11 @@ solveNestedImplications implics
   where givens_from_wanteds = foldrBag get_wanted []
         get_wanted cc rest_givens
             | pushable_wanted cc
-            = let fl = cc_flavor cc
-                  wloc = flav_wloc fl
-                  gfl = Given (mkGivenLoc wloc UnkSkol) (flav_evar fl) 
-                  this_given = cc { cc_flavor = gfl }
+            = let fl   = ctEvidence cc
+                  gfl  = Given { ctev_gloc = setCtLocOrigin (ctev_wloc fl) UnkSkol
+                               , ctev_evtm = EvId (ctev_evar fl)
+                               , ctev_pred = ctev_pred fl }
+                  this_given = cc { cc_ev = gfl }
               in this_given : rest_givens
             | otherwise = rest_givens 
 
@@ -1025,20 +1027,20 @@ solveCTyFunEqs cts
 
       ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
   where
-    solve_one (Wanted _ cv,tv,ty) 
+    solve_one (Wanted { ctev_evar = cv }, tv, ty) 
       = setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
     solve_one (Derived {}, tv, ty)
       = setWantedTyBind tv ty
     solve_one arg
       = pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
 ------------
-type FunEqBinds = (TvSubstEnv, [(CtFlavor, TcTyVar, TcType)])
+type FunEqBinds = (TvSubstEnv, [(CtEvidence, TcTyVar, TcType)])
   -- The TvSubstEnv is not idempotent, but is loop-free
   -- See Note [Non-idempotent substitution] in Unify
 emptyFunEqBinds :: FunEqBinds
 emptyFunEqBinds = (emptyVarEnv, [])
 
-extendFunEqBinds :: FunEqBinds -> CtFlavor -> TcTyVar -> TcType -> FunEqBinds
+extendFunEqBinds :: FunEqBinds -> CtEvidence -> TcTyVar -> TcType -> FunEqBinds
 extendFunEqBinds (tv_subst, cv_binds) fl tv ty
   = (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds)
 
@@ -1052,7 +1054,7 @@ getSolvableCTyFunEqs untch cts
     dflt_funeq :: (Cts, FunEqBinds) -> Ct
                -> (Cts, FunEqBinds)
     dflt_funeq (cts_in, feb@(tv_subst, _))
-               (CFunEqCan { cc_flavor = fl
+               (CFunEqCan { cc_ev = fl
                           , cc_fun = tc
                           , cc_tyargs = xis
                           , cc_rhs = xi })
@@ -1071,7 +1073,7 @@ getSolvableCTyFunEqs untch cts
 
       , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
            -- Occurs check: see Note [Solving Family Equations], Point 2
-      = ASSERT ( not (isGivenOrSolved fl) )
+      = ASSERT ( not (isGiven fl) )
         (cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis))
 
     dflt_funeq (cts_in, fun_eq_binds) ct
@@ -1210,16 +1212,16 @@ defaultTyVar untch the_tv
   , not (k `eqKind` default_k)
   = tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
     do { let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
-       ; eqv <- TcSMonad.newKindConstraint the_tv default_k
+       ; eqv <- TcSMonad.newKindConstraint loc the_tv default_k
        ; case eqv of
            Fresh x -> 
              return $ unitBag $
-             CNonCanonical { cc_flavor = Wanted loc x, cc_depth = 0 }
+             CNonCanonical { cc_ev = x, cc_depth = 0 }
            Cached _ -> return emptyBag }
 {- DELETEME
          if isNewEvVar eqv then 
              return $ unitBag (CNonCanonical { cc_id = evc_the_evvar eqv
-                                             , cc_flavor = fl, cc_depth = 0 })
+                                             , cc_ev = fl, cc_depth = 0 })
          else return emptyBag }
 -}
 
@@ -1300,13 +1302,12 @@ disambigGroup (default_ty:default_tys) group
        ; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
                     do { derived_eq <- tryTcS $
                                        -- I need a new tryTcS because we will call solveInteractCts below!
-                            do { md <- newDerived (mkTcEqPred (mkTyVarTy the_tv) default_ty)
+                            do { md <- newDerived (ctev_wloc the_fl) 
+                                                  (mkTcEqPred (mkTyVarTy the_tv) default_ty)
+                                                  -- ctev_wloc because constraint is not Given!
                                ; case md of 
-                                    Cached _ -> return []
-                                    Fresh pty -> 
-                                      -- flav_wloc because constraint is not Given/Solved!
-                                      let dfl = Derived (flav_wloc the_fl) pty
-                                      in return [ CNonCanonical { cc_flavor = dfl, cc_depth = 0 } ] }
+                                    Nothing   -> return []
+                                    Just ctev -> return [ mkNonCanonical ctev ] }
                             
                        ; traceTcS "disambigGroup (solving) {" 
                                   (text "trying to solve constraints along with default equations ...")
@@ -1335,7 +1336,7 @@ disambigGroup (default_ty:default_tys) group
                        ; disambigGroup default_tys group } }
   where
     ((the_ct,the_tv):_) = group
-    the_fl              = cc_flavor the_ct
+    the_fl              = cc_ev the_ct
     wanteds             = map fst group
 \end{code}
 
@@ -1365,9 +1366,12 @@ newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
 newFlatWanteds orig theta
   = do { loc <- getCtLoc orig
        ; mapM (inst_to_wanted loc) theta }
-  where inst_to_wanted loc pty 
+  where 
+    inst_to_wanted loc pty 
           = do { v <- TcMType.newWantedEvVar pty 
                ; return $ 
-                 CNonCanonical { cc_flavor = Wanted loc v
+                 CNonCanonical { cc_ev = Wanted { ctev_evar = v
+                                                , ctev_wloc = loc
+                                                , ctev_pred = pty }
                                , cc_depth = 0 } }
 \end{code}
index 0b24298..c44ce31 100644 (file)
@@ -533,7 +533,9 @@ uType_defer items ty1 ty2
   = ASSERT( not (null items) )
     do { eqv <- newEq ty1 ty2
        ; loc <- getCtLoc (TypeEqOrigin (last items))
-       ; emitFlat $ mkNonCanonical (Wanted loc eqv)
+       ; let ctev = Wanted { ctev_wloc = loc, ctev_evar = eqv
+                           , ctev_pred = mkTcEqPred ty1 ty2 }
+       ; emitFlat $ mkNonCanonical ctev 
 
        -- Error trace only
        -- NB. do *not* call mkErrInfo unless tracing is on, because
index 1360bac..42e54ba 100644 (file)
@@ -30,7 +30,7 @@ module Coercion (
        -- ** Constructing coercions
         mkReflCo, mkCoVarCo, 
         mkAxInstCo, mkAxInstRHS,
-        mkPiCo, mkPiCos,
+        mkPiCo, mkPiCos, mkCoCast,
         mkSymCo, mkTransCo, mkNthCo,
        mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
         mkForAllCo, mkUnsafeCo,
@@ -672,6 +672,18 @@ mkPiCos vs co = foldr mkPiCo co vs
 mkPiCo  :: Var -> Coercion -> Coercion
 mkPiCo v co | isTyVar v = mkForAllCo v co
             | otherwise = mkFunCo (mkReflCo (varType v)) co
+
+mkCoCast :: Coercion -> Coercion -> Coercion
+-- (mkCoCast (c :: s1 ~# t1) (g :: (s1 ~# t1) ~# (s2 ~# t2)
+mkCoCast c g
+  = mkSymCo g1 `mkTransCo` c `mkTransCo` g2
+  where
+       -- g  :: (s1 ~# s2) ~# (t1 ~#  t2)
+       -- g1 :: s1 ~# t1
+       -- g2 :: s2 ~# t2
+    [_reflk, g1, g2] = decomposeCo 3 g
+            -- Remember, (~#) :: forall k. k -> k -> *
+            -- so it takes *three* arguments, not two
 \end{code}
 
 %************************************************************************
index e0de629..f81aebb 100644 (file)
@@ -973,14 +973,17 @@ getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
         _ -> Nothing
 
 getEqPredTys :: PredType -> (Type, Type)
-getEqPredTys ty = case getEqPredTys_maybe ty of
-        Just (ty1, ty2) -> (ty1, ty2)
-        Nothing         -> pprPanic "getEqPredTys" (ppr ty)
+getEqPredTys ty 
+  = case splitTyConApp_maybe ty of 
+      Just (tc, (_ : ty1 : ty2 : tys)) -> ASSERT( tc `hasKey` eqTyConKey && null tys )
+                                          (ty1, ty2)
+      _ -> pprPanic "getEqPredTys" (ppr ty)
 
 getEqPredTys_maybe :: PredType -> Maybe (Type, Type)
-getEqPredTys_maybe ty = case splitTyConApp_maybe ty of 
-        Just (tc, [_, ty1, ty2]) | tc `hasKey` eqTyConKey -> Just (ty1, ty2)
-        _ -> Nothing
+getEqPredTys_maybe ty 
+  = case splitTyConApp_maybe ty of 
+      Just (tc, [_, ty1, ty2]) | tc `hasKey` eqTyConKey -> Just (ty1, ty2)
+      _ -> Nothing
 
 getIPPredTy_maybe :: PredType -> Maybe (IPName Name, Type)
 getIPPredTy_maybe ty = case splitTyConApp_maybe ty of