A raft more changes,
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 30 Aug 2012 13:38:10 +0000 (14:38 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 30 Aug 2012 13:38:10 +0000 (14:38 +0100)
 * simplifying and tidying up canonicalisation,
 * removing the flat cache altogether
 * making the FunEq worklist into a deque

compiler/typecheck/Inst.lhs
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcErrors.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

index 80c925b..d9f7083 100644 (file)
@@ -85,7 +85,7 @@ emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
 emitWanted origin pred 
   = do { loc <- getCtLoc origin
        ; ev  <- newWantedEvVar pred
-       ; emitFlat (mkNonCanonical (Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev }))
+       ; emitFlat (mkNonCanonical (CtWanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev }))
        ; return ev }
 
 newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
@@ -557,12 +557,12 @@ tidyCt env ct
     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 })
+    tidy_flavor env ctev@(CtGiven { 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 })
+    tidy_flavor env ctev@(CtWanted { ctev_pred = pred })
       = ctev { ctev_pred = tidyType env pred }
-    tidy_flavor env ctev@(Derived { ctev_pred = pred })
+    tidy_flavor env ctev@(CtDerived { ctev_pred = pred })
       = ctev { ctev_pred = tidyType env pred }
 
 tidyEvVar :: TidyEnv -> EvVar -> EvVar
@@ -624,14 +624,14 @@ substEvVar :: TvSubst -> EvVar -> EvVar
 substEvVar subst var = setVarType var (substTy subst (varType var))
 
 substFlavor :: TvSubst -> CtEvidence -> CtEvidence
-substFlavor subst ctev@(Given { ctev_gloc = gloc, ctev_pred = pred })
+substFlavor subst ctev@(CtGiven { ctev_gloc = gloc, ctev_pred = pred })
   = ctev { ctev_gloc = substGivenLoc subst gloc
           , ctev_pred = substTy subst pred }
 
-substFlavor subst ctev@(Wanted { ctev_pred = pred })
+substFlavor subst ctev@(CtWanted { ctev_pred = pred })
   = ctev  { ctev_pred = substTy subst pred }
 
-substFlavor subst ctev@(Derived { ctev_pred = pty })
+substFlavor subst ctev@(CtDerived { ctev_pred = pty })
   = ctev { ctev_pred = substTy subst pty }
 
 substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
index 12c1b85..cb907c7 100644 (file)
@@ -7,8 +7,7 @@
 -- for details
 
 module TcCanonical(
-    canonicalize, flatten, flattenMany, occurCheckExpand,
-    FlattenMode (..),
+    canonicalize, occurCheckExpand,
     StopOrContinue (..)
  ) where
 
@@ -28,18 +27,14 @@ import Outputable
 import Control.Monad    ( when )
 import MonadUtils
 import Control.Applicative ( (<|>) )
+import TysWiredIn ( eqTyCon )
 
 import VarSet
 import TcSMonad
 import FastString
 
 import Util
-
-
-import TysWiredIn ( eqTyCon )
-
-import Data.Maybe ( isJust, fromMaybe )
--- import Data.List  ( zip4 )
+import Maybes( isJust, fromMaybe, catMaybes )
 \end{code}
 
 
@@ -173,7 +168,7 @@ canonicalize :: Ct -> TcS StopOrContinue
 canonicalize ct@(CNonCanonical { cc_ev = fl, cc_depth  = d })
   = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
        ; {-# SCC "canEvVar" #-}
-         canEvVar d fl }
+         canEvNC d fl }
 
 canonicalize (CDictCan { cc_depth  = d
                        , cc_ev = fl
@@ -193,8 +188,8 @@ canonicalize (CFunEqCan { cc_depth = d
                         , cc_fun    = fn
                         , cc_tyargs = xis1
                         , cc_rhs    = xi2 })
-  = {-# SCC "canEqLeafFunEqLeftRec" #-}
-    canEqLeafFunEqLeftRec d fl (fn,xis1) xi2
+  = {-# SCC "canEqLeafFunEq" #-}
+    canEqLeafFunEq d fl (fn,xis1) xi2
 
 canonicalize (CIrredEvCan { cc_ev = fl
                           , cc_depth = d
@@ -202,11 +197,11 @@ canonicalize (CIrredEvCan { cc_ev = fl
   = canIrred d fl xi
 
 
-canEvVar :: SubGoalDepth 
-         -> CtEvidence 
-         -> TcS StopOrContinue
+canEvNC :: SubGoalDepth 
+        -> CtEvidence 
+        -> TcS StopOrContinue
 -- Called only for non-canonical EvVars 
-canEvVar d fl 
+canEvNC d fl 
   = case classifyPredType (ctEvPred fl) of
       ClassPred cls tys -> canClassNC d fl cls tys 
       EqPred ty1 ty2    -> canEqNC    d fl ty1 ty2 
@@ -229,10 +224,7 @@ canTuple d fl tys
        ; let xcomp = EvTupleMk
              xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]             
        ; ctevs <- xCtFlavor fl tys (XEvTerm xcomp xdecomp)
-       ; mapM_ add_to_work ctevs
-       ; return Stop }
-  where
-    add_to_work fl = addToWork $ canEvVar d fl
+       ; canEvVarsCreated d ctevs }
 \end{code}
 
 
@@ -366,9 +358,7 @@ newSCWorkFromFlavored d flavor cls xis
              xev = XEvTerm { ev_comp   = panic "Can't compose for given!" 
                            , ev_decomp = xev_decomp }
        ; ctevs <- xCtFlavor flavor sc_theta xev
-
-       ; traceTcS "newSCWork/Given" $ ppr "ctevs =" <+> ppr ctevs 
-       ; mapM_ emit_non_can ctevs }
+       ; emitWorkNC d ctevs }
 
   | isEmptyVarSet (tyVarsOfTypes xis)
   = return () -- Wanteds with no variables yield no deriveds.
@@ -378,13 +368,8 @@ newSCWorkFromFlavored d flavor cls xis
   = do { let sc_rec_theta = transSuperClasses cls xis 
              impr_theta   = filter is_improvement_pty sc_rec_theta
        ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
-       ; mapM_ emit_der impr_theta }
-
-  where emit_der pty = newDerived (ctev_wloc flavor) pty >>= mb_emit
-        mb_emit Nothing     = return ()
-        mb_emit (Just ctev) = emit_non_can ctev 
-        emit_non_can ctev   = updWorkListTcS $ 
-                              extendWorkListCt (CNonCanonical ctev d)
+       ; mb_der_evs <- mapM (newDerived (ctev_wloc flavor)) impr_theta
+       ; emitWorkNC d (catMaybes mb_der_evs) }
 
 is_improvement_pty :: PredType -> Bool 
 -- Either it's an equality, or has some functional dependency
@@ -423,7 +408,7 @@ canIrred d fl ty
                  -> continueWith $
                     CIrredEvCan { cc_ev = new_fl, cc_ty = xi, cc_depth = d }
                | otherwise
-                 -> canEvVar d new_fl
+                 -> canEvNC d new_fl
              Nothing -> return Stop }
 \end{code}
 
@@ -484,7 +469,9 @@ flattenMany :: SubGoalDepth -- Depth
             -> 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
+-- NB: The EvVar inside the 'ctxt :: CtEvidence' is unused, 
+--     we merely want (a) Given/Solved/Derived/Wanted info
+--                    (b) the GivenLoc/WantedLoc for when we create new evidence
 flattenMany d f ctxt tys 
   = -- pprTrace "flattenMany" empty $
     go tys 
@@ -521,11 +508,11 @@ flatten d f ctxt (FunTy ty1 ty2)
        ; (xi2,co2) <- flatten d f ctxt ty2
        ; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) }
 
-flatten d f fl (TyConApp tc tys)
+flatten d f ctxt (TyConApp tc tys)
   -- For a normal type constructor or data family application, we just
   -- recursively flatten the arguments.
   | not (isSynFamilyTyCon tc)
-    = do { (xis,cos) <- flattenMany d f fl tys
+    = do { (xis,cos) <- flattenMany d f ctxt tys
          ; return (mkTyConApp tc xis, mkTcTyConAppCo tc cos) }
 
   -- Otherwise, it's a type function application, and we have to
@@ -533,7 +520,7 @@ flatten d f fl (TyConApp tc tys)
   -- between the application and a newly generated flattening skolem variable.
   | otherwise
   = ASSERT( tyConArity tc <= length tys )      -- Type functions are saturated
-      do { (xis, cos) <- flattenMany d f fl tys
+      do { (xis, cos) <- flattenMany d f ctxt tys
          ; let (xi_args,  xi_rest)  = splitAt (tyConArity tc) xis
                (cos_args, cos_rest) = splitAt (tyConArity tc) cos
                 -- The type function might be *over* saturated
@@ -550,7 +537,7 @@ flatten d f fl (TyConApp tc tys)
                     ; case mb_ct of
                         Just ct 
                           | let ctev = cc_ev ct
-                          , ctev `canRewrite` fl 
+                          , ctEvFlavour ctev `canRewrite` ctEvFlavour ctxt 
                           -> -- 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 
@@ -566,20 +553,18 @@ flatten d f fl (TyConApp tc tys)
                                                 `mkTcTransCo` mkTcSymCo co
                                ; return (final_co, flat_rhs_xi) }
                           
-                        _ | isGiven fl -- Given: make new flatten skolem
+                        _ | isGiven ctxt -- Given: make new flatten skolem
                           -> do { traceTcS "flatten/flat-cache miss" $ empty 
                                 ; rhs_ty <- newFlattenSkolemTy fam_ty
-                                      -- Update the flat cache
                                 ; let co     = mkTcReflCo fam_ty
-                                      new_fl = Given { ctev_gloc = ctev_gloc fl
-                                                     , ctev_pred = mkTcEqPred fam_ty rhs_ty
-                                                     , ctev_evtm = EvCoercion co }
+                                      new_fl = CtGiven { ctev_gloc = ctev_gloc ctxt
+                                                       , ctev_pred = mkTcEqPred fam_ty rhs_ty
+                                                       , ctev_evtm = EvCoercion co }
                                       ct = CFunEqCan { cc_ev = new_fl
                                                      , cc_fun    = tc 
                                                     , cc_tyargs = xi_args    
                                                     , cc_rhs    = rhs_ty
                                                     , cc_depth  = d }
-                                ; updFlatCache ct
                                 ; updWorkListTcS $ extendWorkListEq ct
                                 ; return (co, rhs_ty) }
 
@@ -587,7 +572,7 @@ flatten d f fl (TyConApp tc tys)
                          -> do { traceTcS "flatten/flat-cache miss" $ empty 
                                ; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
                                ; let pred = mkTcEqPred fam_ty rhs_xi_var
-                                     wloc = ctev_wloc fl
+                                     wloc = ctev_wloc ctxt
                                ; mw <- newWantedEvVar wloc pred
                                ; case mw of
                                    Fresh ctev -> 
@@ -596,8 +581,6 @@ flatten d f fl (TyConApp tc tys)
                                                              , cc_tyargs = xi_args
                                                              , cc_rhs    = rhs_xi_var 
                                                              , cc_depth  = d }
-                                          -- Update the flat cache: just an optimisation!
-                                        ; updFlatCache ct
                                         ; updWorkListTcS $ extendWorkListEq ct
                                         ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }
                                    Cached {} -> panic "flatten TyConApp, var must be fresh!" } 
@@ -675,7 +658,7 @@ flattenTyVar d f ctxt tv
     tv_eq_subst subst tv
        | Just ct <- lookupVarEnv subst tv
        , let ctev = cc_ev ct
-       , ctev `canRewrite` ctxt
+       , ctEvFlavour ctev `canRewrite` ctEvFlavour 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. 
@@ -710,16 +693,6 @@ so that we can make sure that the inert substitution /is/ fully applied.
 
 Insufficient (non-recursive) rewriting was the reason for #5668.
 
-\begin{code}
-
------------------
-addToWork :: TcS StopOrContinue -> TcS ()
-addToWork tcs_action = tcs_action >>= stop_or_emit
-  where stop_or_emit Stop              = return ()
-        stop_or_emit (ContinueWith ct) = updWorkListTcS $ 
-                                         extendWorkListCt ct
-\end{code}
-
 
 %************************************************************************
 %*                                                                      *
@@ -728,17 +701,20 @@ addToWork tcs_action = tcs_action >>= stop_or_emit
 %************************************************************************
 
 \begin{code}
-canEqEvVarsCreated :: SubGoalDepth
-                   -> [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 $ 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
+canEvVarsCreated :: SubGoalDepth -> [CtEvidence] -> TcS StopOrContinue
+canEvVarsCreated _d [] = return Stop
+    -- Add all but one to the work list
+    -- and return the first (if any) for futher processing
+canEvVarsCreated d (ev : evs) 
+  = do { emitWorkNC d evs; canEvNC d ev }
+          -- Note the "NC": these are fresh goals, not necessarily canonical
+
+emitWorkNC :: SubGoalDepth -> [CtEvidence] -> TcS ()
+emitWorkNC depth evs 
+  | null evs  = return ()
+  | otherwise = updWorkListTcS (extendWorkListCts (map mk_nc evs))
+  where
+    mk_nc ev = CNonCanonical { cc_ev = ev, cc_depth  = depth }
 
 -------------------------
 canEqNC, canEq 
@@ -791,7 +767,7 @@ canEq d fl ty1 ty2
              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 }
+       ; canEvVarsCreated d ctevs }
 
 -- See Note [Equality between type applications]
 --     Note [Care with type applications] in TcUnify
@@ -803,7 +779,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 { ctev_wloc = loc, ctev_evar = orig_ev } <- fl 
+ , CtWanted { ctev_wloc = loc, ctev_evar = orig_ev } <- fl 
  = do { let (tvs1,body1) = tcSplitForAllTys s1
             (tvs2,body2) = tcSplitForAllTys s2
       ; if not (equalLength tvs1 tvs2) then 
@@ -839,14 +815,14 @@ canEqAppTy d fl s1 t1 s2 t2
              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 }
+       ; canEvVarsCreated d ctevs }
 
 canEqFailure :: SubGoalDepth -> CtEvidence -> TcS StopOrContinue
 canEqFailure d fl = emitFrozenError fl d >> return Stop
 
 ------------------------
 emitKindConstraint :: Ct -> TcS StopOrContinue
-emitKindConstraint ct
+emitKindConstraint ct   -- By now ct is canonical
   = case ct of 
       CTyEqCan { cc_depth = d
                , cc_ev = fl, cc_tyvar = tv
@@ -867,25 +843,27 @@ emitKindConstraint ct
        
        | otherwise
        = ASSERT( isKind k1 && isKind k2 )
-         do { kev <- 
-                 do { mw <- newWantedEvVar kind_co_wloc (mkEqPred k1 k2) 
-                    ; case mw of
+         do { mw <- newWantedEvVar kind_co_wloc (mkEqPred k1 k2) 
+            ; kev_tm <- case mw of
                          Cached ev_tm -> return ev_tm
-                         Fresh ctev   -> do { addToWork (canEq d ctev k1 k2) 
-                                            ; return (ctEvTerm ctev) } }
+                         Fresh kev   -> do { emitWorkNC d [kev]
+                                           ; return (ctEvTerm kev) } 
 
-            ; let xcomp [x] = mkEvKindCast x (evTermCoercion kev)
+            ; let xcomp [x] = mkEvKindCast x (evTermCoercion kev_tm)
                   xcomp _   = panic "emit_kind_constraint:can't happen"
-                  xdecomp x = [mkEvKindCast x (evTermCoercion kev)]
+                  xdecomp x = [mkEvKindCast x (evTermCoercion kev_tm)]
                   xev = XEvTerm xcomp xdecomp
 
             ; 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:
+                     -- 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!
+                     --
+                     -- We do need to do this xCtFlavor so that in the case of
+                     -- -fdefer-type-errors we still make a demand on kev_tm
 
             ; case ctevs of
                 []         -> return Stop
@@ -901,9 +879,9 @@ emitKindConstraint ct
          -- NB: DV finds this reasonable for now. Maybe we have to revisit.
          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
+                         CtWanted  { ctev_wloc = wloc } -> wloc
+                         CtDerived { ctev_wloc = wloc } -> wloc
+                         CtGiven { ctev_gloc = gloc }   -> setCtLocOrigin gloc orig
          orig = TypeEqOrigin (UnifyOrigin ty1 ty2)
 \end{code}
 
@@ -1141,61 +1119,42 @@ canEqLeafOriented d fl s1 s2
   = can_eq_split_lhs d fl s1 s2
   where can_eq_split_lhs d fl s1 s2
           | Just (fn,tys1) <- splitTyConApp_maybe s1
-          = canEqLeafFunEqLeftRec d fl (fn,tys1) s2
+          = canEqLeafFunEq d fl (fn,tys1) s2
           | Just tv <- getTyVar_maybe s1
           = canEqLeafTyVarLeftRec d fl tv s2
           | otherwise
           = pprPanic "canEqLeafOriented" $
             text "Non-variable or non-family equality LHS" <+> ppr (ctEvPred fl)
 
-canEqLeafFunEqLeftRec :: SubGoalDepth
+canEqLeafFunEq :: SubGoalDepth
                       -> CtEvidence
                       -> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
-canEqLeafFunEqLeftRec d fl (fn,tys1) ty2  -- fl :: F tys1 ~ ty2
-  = do { traceTcS "canEqLeafFunEqLeftRec" $ pprEq (mkTyConApp fn tys1) ty2
+canEqLeafFunEq d ev (fn,tys1) ty2  -- ev :: F tys1 ~ ty2
+  = do { traceTcS "canEqLeafFunEq" $ pprEq (mkTyConApp fn tys1) ty2
        ; (xis1,cos1) <- 
            {-# SCC "flattenMany" #-}
-           flattenMany d FMFullFlatten fl tys1 -- Flatten type function arguments
+           flattenMany d FMFullFlatten ev tys1 -- Flatten type function arguments
                                                -- cos1 :: xis1 ~ tys1
+      ; (xi2,co2) <- {-# SCC "flatten" #-} 
+                     flatten d FMFullFlatten ev ty2 -- co2 :: xi2 ~ ty2
            
        ; let fam_head = mkTyConApp fn xis1
          -- Fancy higher-dimensional coercion between equalities!
-       ; let co = mkTcTyConAppCo eqTyCon $ 
-                  [mkTcReflCo (defaultKind $ typeKind ty2), mkTcTyConAppCo fn cos1, mkTcReflCo ty2]
-             -- Why defaultKind? Same reason as the comment on TcType/mkTcEqPred. I trully hate this (DV)
-             -- co :: (F xis1 ~ ty2) ~ (F tys1 ~ ty2)
+         -- SPJ asks why?  Why not just co : F xis1 ~ F tys1?
+       ; let xco = mkTcTyConAppCo eqTyCon $ 
+                  [mkTcReflCo (defaultKind $ typeKind ty2), mkTcTyConAppCo fn cos1, co2]
+             -- Why defaultKind? Same reason as the comment on TcType/mkTcEqPred. I truly hate this (DV)
+             -- xco :: (F xis1 ~ xi2) ~ (F tys1 ~ ty2)
              
-       ; mb <- rewriteCtFlavor fl (mkTcEqPred fam_head ty2) co
-       ; case mb of 
-           Nothing -> return Stop
-           Just new_fl -> canEqLeafFunEqLeft d new_fl (fn,xis1) ty2 }
-
-
-canEqLeafFunEqLeft :: SubGoalDepth -- Depth
-                   -> CtEvidence
-                   -> (TyCon,[Xi])
-                   -> TcType -> TcS StopOrContinue
--- Precondition: No more flattening is needed for the LHS
-canEqLeafFunEqLeft d fl (fn,xis1) s2
- = {-# SCC "canEqLeafFunEqLeft" #-}
-   do { traceTcS "canEqLeafFunEqLeft" $ pprEq (mkTyConApp fn xis1) s2
-      ; (xi2,co2) <- 
-          {-# SCC "flatten" #-} 
-          flatten d FMFullFlatten fl s2 -- co2 :: xi2 ~ s2
-          
-      ; let fam_head = mkTyConApp fn xis1
-      -- Fancy coercion between equalities! But it should just work! 
-      ; let co = mkTcTyConAppCo eqTyCon $ [ mkTcReflCo (defaultKind $ typeKind s2)
-                                          , mkTcReflCo fam_head, co2 ]
-            -- Why defaultKind? Same reason as the comment at TcType/mkTcEqPred
-            -- co :: (F xis1 ~ xi2) ~ (F xis1 ~ s2)
-            --           new pred         old pred
-      ; mb <- rewriteCtFlavor fl (mkTcEqPred fam_head xi2) co
-      ; case mb of
-          Nothing -> return Stop
-          Just new_fl -> continueWith $ 
-                         CFunEqCan { cc_ev = new_fl, cc_depth = d
-                                   , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } }   
+       ; mb <- rewriteCtFlavor ev (mkTcEqPred fam_head xi2) xco
+       ; case mb of {
+           Nothing -> return Stop ;
+           Just new_ev 
+             | isTcReflCo xco -> continueWith new_ct
+             | otherwise      -> do { updWorkListTcS (extendWorkListEq new_ct); return Stop }
+             where
+               new_ct = CFunEqCan { cc_ev = new_ev, cc_depth = d
+                                  , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } } } 
 
 
 canEqLeafTyVarLeftRec :: SubGoalDepth
index 1f1db0a..869ccc2 100644 (file)
@@ -166,7 +166,7 @@ reportTidyWanteds ctxt insols flats implics
 deferToRuntime :: EvBindsVar -> ReportErrCtxt -> (ReportErrCtxt -> Ct -> TcM ErrMsg) 
                -> Ct -> TcM ()
 deferToRuntime ev_binds_var ctxt mk_err_msg ct 
-  | Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev_id } <- cc_ev ct
+  | CtWanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev_id } <- cc_ev ct
   = do { err <- setCtLoc loc $
                 mk_err_msg ctxt ct
        ; dflags <- getDynFlags
@@ -332,9 +332,9 @@ groupErrs mk_err (ct1 : rest)
    is_friend friend  = cc_ev friend `same_group` flavor
 
    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 (CtGiven   {ctev_gloc = l1}) (CtGiven   {ctev_gloc = l2}) = same_loc l1 l2
+   same_group (CtWanted  {ctev_wloc = l1}) (CtWanted  {ctev_wloc = l2}) = same_loc l1 l2
+   same_group (CtDerived {ctev_wloc = l1}) (CtDerived {ctev_wloc = l2}) = same_loc l1 l2
    same_group _ _ = False
 
    same_loc :: CtLoc o -> CtLoc o -> Bool
@@ -496,7 +496,7 @@ mkEqErr1 ctxt ct
 
     flav = cc_ev ct
 
-    inaccessible_msg (Given { ctev_gloc = loc }) 
+    inaccessible_msg (CtGiven { ctev_gloc = loc }) 
        = hang (ptext (sLit "Inaccessible code in"))
             2 (ppr (ctLocOrigin loc))
     -- If a Solved then we should not report inaccessible code
@@ -1151,9 +1151,9 @@ flattenForAllErrorTcS fl ty
 
 \begin{code}
 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
+setCtFlavorLoc (CtWanted  { ctev_wloc = loc }) thing = setCtLoc loc thing
+setCtFlavorLoc (CtDerived { ctev_wloc = loc }) thing = setCtLoc loc thing
+setCtFlavorLoc (CtGiven   { ctev_gloc = loc }) thing = setCtLoc loc thing
 \end{code}
 
 %************************************************************************
index 65dacfa..20f17e0 100644 (file)
@@ -99,16 +99,14 @@ solveInteractGiven gloc fsks givens
                       -- See Note [Do not decompose given polytype equalities]
                       -- in TcCanonical
   where 
-    given_bag = listToBag [ CNonCanonical { cc_ev = Given { ctev_gloc = gloc 
-                                                          , ctev_evtm = EvId ev_id
-                                                          , ctev_pred = evVarPred ev_id }
-                                          , cc_depth = 0 }
+    given_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_gloc = gloc 
+                                                     , ctev_evtm = EvId ev_id
+                                                     , ctev_pred = evVarPred ev_id }
                           | ev_id <- givens ]
 
-    fsk_bag = listToBag [ CNonCanonical { cc_ev = Given { ctev_gloc = gloc 
-                                                        , ctev_evtm = EvCoercion (mkTcReflCo tv_ty)
-                                                        , ctev_pred = pred  }
-                                        , cc_depth = 0 }
+    fsk_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_gloc = gloc 
+                                                   , ctev_evtm = EvCoercion (mkTcReflCo tv_ty)
+                                                   , ctev_pred = pred  }
                         | tv <- fsks
                         , let FlatSkol fam_ty = tcTyVarDetails tv
                               tv_ty = mkTyVarTy tv
@@ -237,7 +235,7 @@ thePipeline = [ ("lookup-in-inerts",        lookupInInertsStage)
 --------------------------------------------------------------------
 lookupInInertsStage :: SimplifierStage
 lookupInInertsStage ct
-  | Wanted { ctev_evar = ev_id, ctev_pred = pred } <- cc_ev ct
+  | CtWanted { ctev_evar = ev_id, ctev_pred = pred } <- cc_ev ct
   = do { mb_ct <- lookupInInerts pred
        ; case mb_ct of
            Just ctev
@@ -290,12 +288,11 @@ spontaneousSolveStage workItem
   where spont_solve SPCantSolve
           | CTyEqCan { cc_tyvar = tv, cc_ev = fl } <- workItem
           -- Unsolved equality
-          = do { wl <- modifyInertTcS $
-                       kickOutRewritable (fl `canRewrite`) (`canRewrite` fl) tv
+          = do { wl <- modifyInertTcS (kickOutRewritable (ctEvFlavour fl) tv)
                ; traceTcS "kickOutRewritableInerts" $
                  vcat [ text "WorkItem (unsolved) =" <+> ppr workItem
                       , text "Kicked out =" <+> ppr wl ]
-               ; updWorkListTcS (unionWorkList wl)
+               ; updWorkListTcS (appendWorkList wl)
                ; insertInertItemTcS workItem
                ; return Stop }
           | otherwise
@@ -306,11 +303,10 @@ spontaneousSolveStage workItem
           = do { bumpStepCountTcS
                ; traceFireTcS (cc_depth workItem) $
                  ptext (sLit "Spontaneously solved:") <+> ppr workItem
-               ; wl <- modifyInertTcS $
-                       kickOutRewritable (const True) isGiven new_tv
+               ; wl <- modifyInertTcS (kickOutRewritable Given new_tv)
 
                ; traceTcS "kickOutRewritableInerts" $ ptext (sLit "Kicked out =") <+> ppr wl
-               ; updWorkListTcS (unionWorkList wl) 
+               ; updWorkListTcS (appendWorkList wl) 
                ; return Stop }
 
 \end{code}
@@ -331,11 +327,11 @@ these binds /and/ the inerts for potentially unsolved or other given equalities.
 
 \begin{code}
 
-kickOutRewritable :: (CtEvidence -> Bool) -- Can the new item rewrite a CtEvidence?
-                  -> (CtEvidence -> Bool) -- Can some CtEvidence rewrite the new item?
-                  -> TcTyVar
+kickOutRewritable :: CtFlavour    -- Flavour of the equality that is 
+                                  -- being added to the inert set
+                  -> TcTyVar      -- The new equality is tv ~ ty
                   -> InertSet -> (WorkList,InertSet)
-kickOutRewritable can_rewrite can_be_rewritten_by new_tv
+kickOutRewritable new_flav new_tv
        is@(IS { inert_cans = IC { inert_eqs    = tv_eqs
                                 , inert_eq_tvs = inscope
                                 , inert_dicts  = dictmap
@@ -346,7 +342,7 @@ kickOutRewritable can_rewrite can_be_rewritten_by new_tv
   where
     rest_out = fro_out `andCts` dicts_out `andCts` irs_out
     kicked_out = WorkList { wl_eqs    = varEnvElts tv_eqs_out
-                          , wl_funeqs = bagToList feqs_out
+                          , wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
                           , wl_rest   = bagToList rest_out }
   
     remaining = is { inert_cans = IC { inert_eqs = tv_eqs_in
@@ -367,7 +363,7 @@ kickOutRewritable can_rewrite can_be_rewritten_by new_tv
     (irs_out,   irs_in)     = partitionBag     kick_out irreds
     (fro_out,   fro_in)     = partitionBag     kick_out frozen
 
-    kick_out inert_ct = can_rewrite (cc_ev inert_ct) &&
+    kick_out inert_ct = new_flav `canRewrite` (ctFlavour inert_ct) &&
                         (new_tv `elemVarSet` tyVarsOfCt inert_ct) 
                     -- NB: tyVarsOfCt will return the type 
                     --     variables /and the kind variables/ that are 
@@ -378,7 +374,7 @@ kickOutRewritable can_rewrite can_be_rewritten_by new_tv
                     --     constraints that mention type variables whose
                     --     kinds could contain this variable!
 
-    kick_out_eq inert_ct = kick_out inert_ct && not (can_be_rewritten_by (cc_ev inert_ct))
+    kick_out_eq inert_ct = kick_out inert_ct && not (ctFlavour inert_ct `canRewrite` new_flav)
                -- If also the inert can rewrite the subst then there is no danger of 
                -- occurs check errors sor keep it there. No need to rewrite the inert equality
                -- (as we did in the past) because of point (8) of 
@@ -719,9 +715,9 @@ doInteractWithInert (CIrredEvCan { cc_ev = ifl, cc_ty = ty1 })
   | ty1 `eqType` ty2
   = solveOneFromTheOther "Irred/Irred" ifl workItem
 
-doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
+doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
                                   , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 }) 
-                    wi@(CFunEqCan { cc_ev = fl2, cc_fun = tc2
+                    wi@(CFunEqCan { cc_ev = ev2, cc_fun = tc2
                                   , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
   | fl1 `canSolve` fl2 && lhss_match
   = do { traceTcS "interact with inerts: FunEq/FunEq" $ 
@@ -735,7 +731,7 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
              -- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]                 
              xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]
 
-       ; ctevs <- xCtFlavor_cache False fl2 [mkTcEqPred xi2 xi1] xev
+       ; ctevs <- xCtFlavor_cache False ev2 [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 
@@ -753,7 +749,7 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
              -- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)]
              xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]
 
-       ; ctevs <- xCtFlavor_cache False fl1 [mkTcEqPred xi2 xi1] xev 
+       ; ctevs <- xCtFlavor_cache False ev1 [mkTcEqPred xi2 xi1] xev 
                           -- Why not simply xCtFlavor? See Note [Cache-caused loops]
                           -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
 
@@ -765,9 +761,11 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
     add_to_work _ _ = return ()
 
     lhss_match = tc1 == tc2 && eqTypes args1 args2 
-    co1 = evTermCoercion $ ctEvTerm fl1
-    co2 = evTermCoercion $ ctEvTerm fl2
+    co1 = evTermCoercion $ ctEvTerm ev1
+    co2 = evTermCoercion $ ctEvTerm ev2
     mk_sym_co x = mkTcSymCo (evTermCoercion x)
+    fl1 = ctEvFlavour ev1
+    fl2 = ctEvFlavour ev2
     
 doInteractWithInert _ _ = return (IRKeepGoing "NOP")
 
@@ -873,10 +871,10 @@ solveOneFromTheOther info ifl workItem
                  -- so it's safe to continue on from this point
   = return (IRInertConsumed ("Solved[DI] " ++ info))
   
-  | Wanted { ctev_evar = ev_id } <- wfl
+  | CtWanted { ctev_evar = ev_id } <- wfl
   = do { setEvBind ev_id (ctEvTerm ifl); return (IRWorkItemConsumed ("Solved(w) " ++ info)) }
 
-  | Wanted { ctev_evar = ev_id } <- ifl
+  | CtWanted { ctev_evar = ev_id } <- ifl
   = do { setEvBind ev_id (ctEvTerm wfl); return (IRInertConsumed ("Solved(g) " ++ info)) }
 
   | otherwise     -- If both are Given, we already have evidence; no need to duplicate
@@ -1300,8 +1298,8 @@ rewriteWithFunDeps eqn_pred_locs fl
       ; if null fd_ev_pos then return Nothing
         else return (Just (map snd fd_ev_pos)) }
  where 
-   wloc | Given { ctev_gloc = gl } <- fl = setCtLocOrigin gl FunDepOrigin
-        | otherwise                      = ctev_wloc fl
+   wloc | CtGiven { ctev_gloc = gl } <- fl = setCtLocOrigin gl FunDepOrigin
+        | otherwise                        = ctev_wloc fl
 
 instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,CtEvidence)]
 -- Post: Returns the position index as well as the corresponding FunDep equality
@@ -1341,7 +1339,7 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
 emitFDWorkAsDerived :: [CtEvidence]   -- All Derived
                     -> SubGoalDepth -> TcS () 
 emitFDWorkAsDerived evlocs d 
-  = updWorkListTcS $ appendWorkListEqs (map mk_fd_ct evlocs)
+  = updWorkListTcS $ extendWorkListEqs (map mk_fd_ct evlocs)
   where 
     mk_fd_ct der_ev = CNonCanonical { cc_ev = der_ev, cc_depth = d }
 \end{code}
@@ -1452,7 +1450,7 @@ doTopReactDict inerts workItem fl cls xis depth
              ; let mk_new_wanted ev
                        = CNonCanonical { cc_ev   = ev
                                        , cc_depth = depth + 1 }
-             ; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs))
+             ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
              ; return $
                SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
                           , tir_new_item = Stop } }
@@ -1460,8 +1458,8 @@ doTopReactDict inerts workItem fl cls xis depth
 --------------------
 doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
                 -> SubGoalDepth -> TcS TopInteractResult
-doTopReactFunEq ct fl tc args xi d
-  = ASSERT (isSynFamilyTyCon tc) -- No associated data families have 
+doTopReactFunEq ct fl fun_tc args xi d
+  = ASSERT (isSynFamilyTyCon fun_tc) -- No associated data families have 
                                  -- reached that far 
 
     -- First look in the cache of solved funeqs
@@ -1469,12 +1467,12 @@ doTopReactFunEq ct fl tc args xi d
        ; case lookupFamHead fun_eq_cache fam_ty of {
             Just (CFunEqCan { cc_ev = ctev, cc_rhs = rhs_ty })
                 -> ASSERT( not (isDerived ctev) )
-                   succeed_with (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
+                   succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
             Just {}  -> pprPanic "doTopReactFunEq" (ppr ct) ;
             Nothing -> 
 
     -- No cached solved, so look up in top-level instances
-    do { match_res <- matchFam tc args   -- See Note [MATCHING-SYNONYMS]
+    do { match_res <- matchFam fun_tc args   -- See Note [MATCHING-SYNONYMS]
        ; case match_res of {
            Nothing -> return NoTopInt ;
            Just (famInst, rep_tys) -> 
@@ -1484,13 +1482,13 @@ doTopReactFunEq ct fl tc args xi d
          unless (isDerived fl) (addSolvedFunEq ct fam_ty)
 
        ; let coe_ax = famInstAxiom famInst 
-       ; succeed_with (mkTcAxInstCo coe_ax rep_tys)
+       ; succeed_with "Fun/Top"(mkTcAxInstCo coe_ax rep_tys)
                       (mkAxInstRHS coe_ax rep_tys) } } } } }
   where
-    fam_ty = mkTyConApp tc args
+    fam_ty = mkTyConApp fun_tc args
 
-    succeed_with :: TcCoercion -> TcType -> TcS TopInteractResult
-    succeed_with coe rhs_ty 
+    succeed_with :: String -> TcCoercion -> TcType -> TcS TopInteractResult
+    succeed_with str co rhs_ty    -- co :: fun_tc args ~ rhs_ty
       = do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
            ; case ctevs of
                [ctev] -> updWorkListTcS $ extendWorkListEq $
@@ -1498,11 +1496,11 @@ doTopReactFunEq ct fl tc args xi d
                                        , cc_depth  = d+1 }
                ctevs -> -- No subgoal (because it's cached)
                         ASSERT( null ctevs) return () 
-           ; return $ SomeTopInt { tir_rule = "Fun/Top"
+           ; return $ SomeTopInt { tir_rule = str
                                  , tir_new_item = Stop } }
       where
-        xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
-        xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
+        xdecomp x = [EvCoercion (mkTcSymCo co `mkTcTransCo` evTermCoercion x)]
+        xcomp [x] = EvCoercion (co `mkTcTransCo` evTermCoercion x)
         xcomp _   = panic "No more goals!"
         xev = XEvTerm xcomp xdecomp
 \end{code}
index 3733549..4dbf787 100644 (file)
@@ -652,14 +652,14 @@ zonkCts :: Cts -> TcM Cts
 zonkCts = mapBagM zonkCt
 
 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
-zonkCtEvidence ctev@(Given { ctev_gloc = loc, ctev_pred = pred }) 
+zonkCtEvidence ctev@(CtGiven { ctev_gloc = loc, ctev_pred = pred }) 
   = do { loc' <- zonkGivenLoc loc
        ; pred' <- zonkTcType pred
        ; return (ctev { ctev_gloc = loc', ctev_pred = pred'}) }
-zonkCtEvidence ctev@(Wanted { ctev_pred = pred })
+zonkCtEvidence ctev@(CtWanted { ctev_pred = pred })
   = do { pred' <- zonkTcType pred
        ; return (ctev { ctev_pred = pred' }) }
-zonkCtEvidence ctev@(Derived { ctev_pred = pred })
+zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
   = do { pred' <- zonkTcType pred
        ; return (ctev { ctev_pred = pred' }) }
 
index dd4f83c..5199f01 100644 (file)
@@ -73,6 +73,7 @@ module TcRnTypes(
         mkGivenLoc,
         isWanted, isGiven,
         isDerived, getWantedLoc, getGivenLoc, canSolve, canRewrite,
+        CtFlavour(..), ctEvFlavour, ctFlavour,
 
        -- Pretty printing
         pprEvVarTheta, pprWantedsWithLocs,
@@ -1205,42 +1206,57 @@ may be un-zonked.
 
 \begin{code}
 data CtEvidence 
-  = Given { ctev_gloc :: GivenLoc
-          , ctev_pred :: TcPredType
-          , ctev_evtm :: EvTerm }          -- See Note [Evidence field of CtEvidence]
+  = CtGiven { 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
     
-  | Wanted { ctev_wloc :: WantedLoc
-           , ctev_pred :: TcPredType
-           , ctev_evar :: EvVar }          -- See Note [Evidence field of CtEvidence]
+  | CtWanted { ctev_wloc :: WantedLoc
+             , ctev_pred :: TcPredType
+             , ctev_evar :: EvVar }          -- See Note [Evidence field of CtEvidence]
     -- Wanted goal 
     
-  | Derived { ctev_wloc :: WantedLoc 
-            , ctev_pred :: TcPredType }
+  | CtDerived { 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!) 
     -- but if we do manage to solve it may help in solving other goals.
 
+data CtFlavour = Given | Wanted | Derived
+
+ctFlavour :: Ct -> CtFlavour
+ctFlavour ct = ctEvFlavour (cc_ev ct)
+
+ctEvFlavour :: CtEvidence -> CtFlavour
+ctEvFlavour (CtGiven {})   = Given
+ctEvFlavour (CtWanted {})  = Wanted
+ctEvFlavour (CtDerived {}) = Derived
+
 ctEvPred :: CtEvidence -> TcPredType
 -- The predicate of a flavor
 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" 
+ctEvTerm (CtGiven   { ctev_evtm = tm }) = tm
+ctEvTerm (CtWanted  { ctev_evar = ev }) = EvId ev
+ctEvTerm ctev@(CtDerived {}) = pprPanic "ctEvTerm: derived constraint cannot have id" 
                                       (ppr ctev)
 
 ctEvId :: CtEvidence -> TcId
-ctEvId (Wanted  { ctev_evar = ev }) = ev
+ctEvId (CtWanted  { ctev_evar = ev }) = ev
 ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
 
+instance Outputable CtFlavour where
+  ppr Given   = ptext (sLit "[G]")
+  ppr Wanted  = ptext (sLit "[W]")
+  ppr Derived = ptext (sLit "[D]")
+
 instance Outputable CtEvidence where
   ppr fl = case fl of
-             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
+             CtGiven {}   -> ptext (sLit "[G]") <+> ppr (ctev_evtm fl) <+> ppr_pty
+             CtWanted {}  -> ptext (sLit "[W]") <+> ppr (ctev_evar fl) <+> ppr_pty
+             CtDerived {} -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty
          where ppr_pty = dcolon <+> ppr (ctEvPred fl)
 
 getWantedLoc :: CtEvidence -> WantedLoc
@@ -1252,23 +1268,23 @@ getGivenLoc :: CtEvidence -> GivenLoc
 getGivenLoc fl = ctev_gloc fl
 
 pprFlavorArising :: CtEvidence -> SDoc
-pprFlavorArising (Given { ctev_gloc = gl }) = pprArisingAt gl
-pprFlavorArising ctev                       = pprArisingAt (ctev_wloc ctev)
+pprFlavorArising (CtGiven { ctev_gloc = gl }) = pprArisingAt gl
+pprFlavorArising ctev                         = pprArisingAt (ctev_wloc ctev)
 
 
 isWanted :: CtEvidence -> Bool
-isWanted (Wanted {}) = True
+isWanted (CtWanted {}) = True
 isWanted _ = False
 
 isGiven :: CtEvidence -> Bool
-isGiven (Given {})  = True
+isGiven (CtGiven {})  = True
 isGiven _ = False
 
 isDerived :: CtEvidence -> Bool
-isDerived (Derived {}) = True
-isDerived _             = False
+isDerived (CtDerived {}) = True
+isDerived _              = False
 
-canSolve :: CtEvidence -> CtEvidence -> Bool
+canSolve :: CtFlavour -> CtFlavour -> 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.
@@ -1279,13 +1295,13 @@ canSolve :: CtEvidence -> CtEvidence -> Bool
 --
 -- NB:  either (a `canSolve` b) or (b `canSolve` a) must hold
 -----------------------------------------
-canSolve (Given {})   _            = True 
-canSolve (Wanted {})  (Derived {}) = True
-canSolve (Wanted {})  (Wanted {})  = True
-canSolve (Derived {}) (Derived {}) = True  -- Derived can't solve wanted/given
+canSolve Given   _       = True 
+canSolve Wanted  Derived = True
+canSolve Wanted  Wanted  = True
+canSolve Derived Derived = True  -- Derived can't solve wanted/given
 canSolve _ _ = False                      -- No evidence for a derived, anyway
 
-canRewrite :: CtEvidence -> CtEvidence -> Bool 
+canRewrite :: CtFlavour -> CtFlavour -> Bool 
 -- canRewrite ct1 ct2 
 -- The equality constraint ct1 can be used to rewrite inside ct2 
 canRewrite = canSolve 
index 782d795..e3cc592 100644 (file)
@@ -1,5 +1,5 @@
 \begin{code}
-{-# OPTIONS -fno-warn-tabs #-}
+{-# OPTIONS -fno-warn-tabs -w #-}
 -- The above warning supression flag is a temporary kludge.
 -- While working on this module you are encouraged to remove it and
 -- detab the module (please do the detabbing in a separate patch). See
@@ -14,10 +14,10 @@ module TcSMonad (
     WorkList(..), isEmptyWorkList, emptyWorkList,
     workListFromEq, workListFromNonEq, workListFromCt, 
     extendWorkListEq, extendWorkListNonEq, extendWorkListCt, 
-    appendWorkListCt, appendWorkListEqs, unionWorkList, selectWorkItem,
+    extendWorkListCts, extendWorkListEqs, appendWorkList, selectWorkItem,
     withWorkList,
 
-    getTcSWorkList, updWorkListTcS, updWorkListTcS_return,
+    updWorkListTcS, updWorkListTcS_return,
     
     getTcSImplics, updTcSImplics, emitTcSImplication, 
 
@@ -36,7 +36,7 @@ module TcSMonad (
     wrapErrTcS, wrapWarnTcS,
 
     -- Getting and setting the flattening cache
-    getFlatCache, updFlatCache, addToSolved, addSolvedFunEq, getFlattenSkols,
+    addToSolved, addSolvedFunEq, getFlattenSkols,
     
     deferTcSForAllEq, 
     
@@ -60,6 +60,9 @@ module TcSMonad (
 
     newFlattenSkolemTy,                         -- Flatten skolems 
 
+        -- Deque
+    Deque(..), insertDeque, emptyDeque,
+
         -- Inerts 
     InertSet(..), InertCans(..), 
     getInertEqs, 
@@ -193,29 +196,57 @@ be rewritten by equalities (for instance if a non canonical exists in the inert,
 better rewrite it as much as possible before reporting it as an error to the user)
 
 \begin{code}
+data Deque a = DQ [a] [a]   -- Insert in RH field, remove from LH field
+                            -- First to remove is at head of LH field
+
+instance Outputable a => Outputable (Deque a) where
+  ppr (DQ as bs) = ppr (as ++ reverse bs)   -- Show first one to come out at the start
+
+emptyDeque :: Deque a
+emptyDeque = DQ [] []
+
+isEmptyDeque :: Deque a -> Bool
+isEmptyDeque (DQ as bs) = null as && null bs
+
+insertDeque :: a -> Deque a -> Deque a
+insertDeque b (DQ as bs) = DQ as (b:bs)
+
+appendDeque :: Deque a -> Deque a -> Deque a
+appendDeque (DQ as1 bs1) (DQ as2 bs2) = DQ (as1 ++ reverse bs1 ++ as2) bs2
+
+extractDeque :: Deque a -> Maybe (Deque a, a)
+extractDeque (DQ [] [])     = Nothing
+extractDeque (DQ (a:as) bs) = Just (DQ as bs, a)
+extractDeque (DQ [] bs)     = case reverse bs of
+                                (a:as) -> Just (DQ as [], a)
+                                [] -> panic "extractDeque"
 
 -- See Note [WorkList]
 data WorkList = WorkList { wl_eqs    :: [Ct]
-                         , wl_funeqs :: [Ct]
+                         , wl_funeqs :: Deque Ct
                          , wl_rest   :: [Ct] 
                          }
 
 
-unionWorkList :: WorkList -> WorkList -> WorkList
-unionWorkList new_wl orig_wl = 
-   WorkList { wl_eqs    = wl_eqs new_wl ++ wl_eqs orig_wl
-            , wl_funeqs = wl_funeqs new_wl ++ wl_funeqs orig_wl
-            , wl_rest   = wl_rest new_wl ++ wl_rest orig_wl }
+appendWorkList :: WorkList -> WorkList -> WorkList
+appendWorkList new_wl orig_wl 
+   = WorkList { wl_eqs    = wl_eqs new_wl    ++            wl_eqs orig_wl
+              , wl_funeqs = wl_funeqs new_wl `appendDeque` wl_funeqs orig_wl
+              , wl_rest   = wl_rest new_wl   ++            wl_rest orig_wl }
 
 
 extendWorkListEq :: Ct -> WorkList -> WorkList
 -- Extension by equality
 extendWorkListEq ct wl 
   | Just {} <- isCFunEqCan_Maybe ct
-  = wl { wl_funeqs = ct : wl_funeqs wl }
+  = wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
   | otherwise
   = wl { wl_eqs = ct : wl_eqs wl }
 
+extendWorkListEqs :: [Ct] -> WorkList -> WorkList
+-- Append a list of equalities
+extendWorkListEqs cts wl = foldr extendWorkListEq wl cts
+
 extendWorkListNonEq :: Ct -> WorkList -> WorkList
 -- Extension by non equality
 extendWorkListNonEq ct wl 
@@ -227,20 +258,16 @@ extendWorkListCt ct wl
  | isEqPred (ctPred ct) = extendWorkListEq ct wl
  | otherwise = extendWorkListNonEq ct wl
 
-appendWorkListCt :: [Ct] -> WorkList -> WorkList
+extendWorkListCts :: [Ct] -> WorkList -> WorkList
 -- Agnostic
-appendWorkListCt cts wl = foldr extendWorkListCt wl cts
-
-appendWorkListEqs :: [Ct] -> WorkList -> WorkList
--- Append a list of equalities
-appendWorkListEqs cts wl = foldr extendWorkListEq wl cts
+extendWorkListCts cts wl = foldr extendWorkListCt wl cts
 
 isEmptyWorkList :: WorkList -> Bool
 isEmptyWorkList wl 
-  = null (wl_eqs wl) &&  null (wl_rest wl) && null (wl_funeqs wl)
+  = null (wl_eqs wl) &&  null (wl_rest wl) && isEmptyDeque (wl_funeqs wl)
 
 emptyWorkList :: WorkList
-emptyWorkList = WorkList { wl_eqs  = [], wl_rest = [], wl_funeqs = [] }
+emptyWorkList = WorkList { wl_eqs  = [], wl_rest = [], wl_funeqs = emptyDeque }
 
 workListFromEq :: Ct -> WorkList
 workListFromEq ct = extendWorkListEq ct emptyWorkList
@@ -258,7 +285,8 @@ selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
 selectWorkItem wl@(WorkList { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
   = case (eqs,feqs,rest) of
       (ct:cts,_,_)     -> (Just ct, wl { wl_eqs    = cts })
-      (_,(ct:cts),_)   -> (Just ct, wl { wl_funeqs = cts })
+      (_,fun_eqs,_)    | Just (fun_eqs', ct) <- extractDeque fun_eqs
+                       -> (Just ct, wl { wl_funeqs = fun_eqs' })
       (_,_,(ct:cts))   -> (Just ct, wl { wl_rest   = cts })
       (_,_,_)          -> (Nothing,wl)
 
@@ -290,9 +318,9 @@ 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_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) }
+      CtWanted {}  -> cmap { cts_wanted  = insert_into (cts_wanted cmap)  } 
+      CtGiven {}   -> cmap { cts_given   = insert_into (cts_given cmap)   }
+      CtDerived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
   where 
     insert_into m = addToUFM_C unionBags m a (singleCt ct)
 
@@ -505,9 +533,7 @@ data InertSet
        , inert_frozen :: Cts       
               -- Frozen errors (as non-canonicals)
                                
-       , inert_flat_cache :: CtFamHeadMap 
        , inert_fsks :: [TcTyVar]  -- Flatten-skolems allocated in this local scope
-                                  -- Subset of inert_flat_cacha
               -- All ``flattening equations'' are kept here. 
               -- Always canonical CTyFunEqs (Given or Wanted only!)
               -- Key is by family head. We use this field during flattening only
@@ -558,7 +584,6 @@ emptyInert
                          , inert_funeqs = FamHeadMap emptyTM 
                          , inert_irreds = emptyCts }
        , inert_frozen        = emptyCts
-       , inert_flat_cache    = FamHeadMap emptyTM
        , inert_fsks          = []
        , inert_solved        = PredMap emptyTM 
        , inert_solved_funeqs = FamHeadMap emptyTM }
@@ -694,9 +719,9 @@ prepareInertsForImplications is
       | otherwise  = funeq { cc_ev = given_ev }
       where
         ev = ctEvidence funeq
-        given_ev = Given { ctev_gloc = setCtLocOrigin (ctev_wloc ev) UnkSkol
-                         , ctev_evtm = EvId (ctev_evar ev)
-                         , ctev_pred = ctev_pred ev }
+        given_ev = CtGiven { ctev_gloc = setCtLocOrigin (ctev_wloc ev) UnkSkol
+                           , ctev_evtm = EvId (ctev_evar ev)
+                           , ctev_pred = ctev_pred ev }
 \end{code}
 
 Note [Preparing inert set for implications]
@@ -819,11 +844,10 @@ extractRelevantInerts wi
 lookupFlatEqn :: TcType -> TcS (Maybe Ct)
 lookupFlatEqn fam_ty 
   = do { IS { inert_solved_funeqs = solved_funeqs
-            , inert_flat_cache = flat_cache
             , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
-       ; return (lookupFamHead solved_funeqs fam_ty `firstJust`
-                 lookupFamHead inert_funeqs fam_ty  `firstJust`
-                 lookupFamHead flat_cache   fam_ty) }
+       ; return (lookupFamHead solved_funeqs fam_ty 
+                 `firstJust` lookupFamHead inert_funeqs fam_ty  
+                 }
 
 lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
 -- Is this exact predicate type cached in the solved or canonicals of the InertSet
@@ -1093,9 +1117,6 @@ getTcSImplicsRef = TcS (return . tcs_implics)
 getTcSImplics :: TcS (Bag Implication)
 getTcSImplics = getTcSImplicsRef >>= wrapTcS . (TcM.readTcRef)
 
-getTcSWorkList :: TcS WorkList
-getTcSWorkList = getTcSWorkListRef >>= wrapTcS . (TcM.readTcRef) 
-
 updWorkListTcS :: (WorkList -> WorkList) -> TcS () 
 updWorkListTcS f 
   = do { wl_var <- getTcSWorkListRef
@@ -1164,25 +1185,6 @@ instance HasDynFlags TcS where
 getTcEvBinds :: TcS EvBindsVar
 getTcEvBinds = TcS (return . tcs_ev_binds) 
 
-getFlatCache :: TcS CtTypeMap 
-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_ev = fl, cc_fun = tc, cc_tyargs = xis })
-  = updInertTcS upd_inert_cache
-  where 
-    upd_inert_cache is = is { inert_flat_cache = FamHeadMap new_fc }
-                       where new_fc = alterTM pred_key upd_cache fc
-                             fc = unFamHeadMap $ inert_flat_cache is
-    pred_key = mkTyConApp tc xis
-    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 Untouchables
 getUntouchables = wrapTcS TcM.getUntouchables
 
@@ -1413,7 +1415,7 @@ newGivenEvVar :: GivenLoc -> TcPredType -> EvTerm -> TcS CtEvidence
 newGivenEvVar gloc pred rhs
   = do { new_ev <- wrapTcS $ TcM.newEvVar pred
        ; setEvBind new_ev rhs
-       ; return (Given { ctev_gloc = gloc, ctev_pred = pred, ctev_evtm = EvId new_ev }) }
+       ; return (CtGiven { ctev_gloc = gloc, ctev_pred = pred, ctev_evtm = EvId new_ev }) }
 
 newWantedEvVar :: WantedLoc -> TcPredType -> TcS MaybeNew
 newWantedEvVar loc pty
@@ -1424,9 +1426,9 @@ newWantedEvVar loc pty
                             ; return (Cached (ctEvTerm ctev)) }
             _ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
                     ; traceTcS "newWantedEvVar/cache miss" $ ppr new_ev
-                    ; let ctev = Wanted { ctev_wloc = loc
-                                        , ctev_pred = pty
-                                        , ctev_evar = new_ev }
+                    ; let ctev = CtWanted { ctev_wloc = loc
+                                          , ctev_pred = pty
+                                          , ctev_evar = new_ev }
                     ; return (Fresh ctev) } }
 
 newDerived :: WantedLoc -> TcPredType -> TcS (Maybe CtEvidence)
@@ -1436,8 +1438,8 @@ newDerived loc pty
   = do { mb_ct <- lookupInInerts pty
        ; return (case mb_ct of
                     Just {} -> Nothing
-                    Nothing -> Just (Derived { ctev_wloc = loc
-                                             , ctev_pred = pty })) }
+                    Nothing -> Just (CtDerived { ctev_wloc = loc
+                                               , ctev_pred = pty })) }
 
 instDFunConstraints :: WantedLoc -> TcThetaType -> TcS [MaybeNew]
 instDFunConstraints wl = mapM (newWantedEvVar wl)
@@ -1482,7 +1484,7 @@ xCtFlavor_cache :: Bool            -- True = if wanted add to the solved bag!
           -> XEvTerm               -- Instructions about how to manipulate evidence
           -> TcS [CtEvidence]
 
-xCtFlavor_cache _ (Given { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
+xCtFlavor_cache _ (CtGiven { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
   = ASSERT( equalLength ptys (ev_decomp xev tm) )
     zipWithM (newGivenEvVar gl) ptys (ev_decomp xev tm)
     -- For Givens we make new EvVars and bind them immediately. We don't worry
@@ -1494,7 +1496,7 @@ xCtFlavor_cache _ (Given { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
     -- But that superclass selector can't (yet) appear in a coercion
     -- (see evTermCoercion), so the easy thing is to bind it to an Id
   
-xCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
+xCtFlavor_cache cache ctev@(CtWanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
   = do { new_evars <- mapM (newWantedEvVar wl) ptys
        ; setEvBind evar (ev_comp xev (getEvTerms new_evars))
 
@@ -1503,7 +1505,7 @@ xCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar }) ptys xe
 
        ; return (freshGoals new_evars) }
     
-xCtFlavor_cache _ (Derived { ctev_wloc = wl }) ptys _xev
+xCtFlavor_cache _ (CtDerived { ctev_wloc = wl }) ptys _xev
   = do { ders <- mapM (newDerived wl) ptys
        ; return (catMaybes ders) }
 
@@ -1514,7 +1516,7 @@ rewriteCtFlavor :: CtEvidence
                 -> TcS (Maybe CtEvidence)
 {- 
      rewriteCtFlavor old_fl new_pred co
-Main purpose: create a new identity (flavor) for new_pred;
+Main purpose: create new evidence 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
@@ -1530,8 +1532,6 @@ Main purpose: create a new identity (flavor) for new_pred;
 
         Given           Already in inert               Nothing
                         Not                            Just new_evidence
-
-        Solved          NEVER HAPPENS
 -}
 
 rewriteCtFlavor = rewriteCtFlavor_cache True
@@ -1547,15 +1547,15 @@ rewriteCtFlavor_cache :: Bool
 -- 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 { ctev_wloc = wl }) pty_new _co
+rewriteCtFlavor_cache _cache (CtDerived { ctev_wloc = wl }) pty_new _co
   = newDerived wl pty_new
         
-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 }))
+rewriteCtFlavor_cache _cache (CtGiven { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
+  = return (Just (CtGiven { 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 = old_pred }) 
+rewriteCtFlavor_cache cache ctev@(CtWanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = old_pred }) 
                       new_pred co
   | isTcReflCo co -- If just reflexivity then you may re-use the same variable
   = return (Just (if old_pred `eqType` new_pred
index 9596c67..737d0e4 100644 (file)
@@ -1056,9 +1056,9 @@ unFlattenWC wc
 
           ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
       where
-        solve_one (Wanted { ctev_evar = cv }, tv, ty) 
+        solve_one (CtWanted { ctev_evar = cv }, tv, ty) 
           = setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
-        solve_one (Derived {}, tv, ty)
+        solve_one (CtDerived {}, tv, ty)
           = setWantedTyBind tv ty
         solve_one arg
           = pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
@@ -1201,8 +1201,8 @@ defaultTyVar the_tv
              -- Why not directly derived_pred = mkTcEqPred k default_k? 
              -- See Note [DefaultTyVar]
              derived_cts = mkNonCanonical $
-                           Derived { ctev_wloc = loc
-                                   , ctev_pred = derived_pred } 
+                           CtDerived { ctev_wloc = loc
+                                     , ctev_pred = derived_pred } 
        
        ; return (unitBag derived_cts) }
 
@@ -1302,8 +1302,8 @@ disambigGroup (default_ty:default_tys) group
        ; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
                     do { let derived_pred = mkTcEqPred (mkTyVarTy the_tv) default_ty
                              derived_cts = unitBag $ mkNonCanonical $
-                                           Derived { ctev_wloc = the_loc
-                                                   , ctev_pred = derived_pred }
+                                           CtDerived { ctev_wloc = the_loc
+                                                     , ctev_pred = derived_pred }
                             
                        ; traceTcS "disambigGroup (solving) {" $
                          text "trying to solve constraints along with default equations ..."
@@ -1366,9 +1366,8 @@ newFlatWanteds orig theta
   where 
     inst_to_wanted loc pty 
           = do { v <- TcMType.newWantedEvVar pty 
-               ; return $ 
-                 CNonCanonical { cc_ev = Wanted { ctev_evar = v
-                                                , ctev_wloc = loc
-                                                , ctev_pred = pty }
-                               , cc_depth = 0 } }
+               ; return $ mkNonCanonical $
+                 CtWanted { ctev_evar = v
+                          , ctev_wloc = loc
+                          , ctev_pred = pty } }
 \end{code}
index aef065f..2ce6865 100644 (file)
@@ -535,8 +535,8 @@ uType_defer items ty1 ty2
   = ASSERT( not (null items) )
     do { eqv <- newEq ty1 ty2
        ; loc <- getCtLoc (TypeEqOrigin (last items))
-       ; let ctev = Wanted { ctev_wloc = loc, ctev_evar = eqv
-                           , ctev_pred = mkTcEqPred ty1 ty2 }
+       ; let ctev = CtWanted { ctev_wloc = loc, ctev_evar = eqv
+                             , ctev_pred = mkTcEqPred ty1 ty2 }
        ; emitFlat $ mkNonCanonical ctev 
 
        -- Error trace only