This BIG PATCH contains most of the work for the New Coercion Representation
[ghc-hetmet.git] / compiler / typecheck / TcSMonad.lhs
index ad24eb7..13c7377 100644 (file)
@@ -8,6 +8,10 @@ module TcSMonad (
     isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
     isCFrozenErr,
 
+    WorkList, unionWorkList, unionWorkLists, isEmptyWorkList, emptyWorkList,
+    workListFromEq, workListFromNonEq,
+    workListFromEqs, workListFromNonEqs, foldrWorkListM,
+
     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
     deCanonicalise, mkFrozenError,
 
@@ -26,13 +30,12 @@ module TcSMonad (
     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
 
        -- Creation of evidence variables
-    newEvVar, newCoVar, newWantedCoVar, newGivenCoVar,
+    newEvVar, newCoVar, newGivenCoVar,
     newDerivedId, 
     newIPVar, newDictVar, newKindConstraint,
 
        -- Setting evidence variables 
-    setWantedCoBind,
-    setIPBind, setDictBind, setEvBind,
+    setCoBind, setIPBind, setDictBind, setEvBind,
 
     setWantedTyBind,
 
@@ -79,6 +82,7 @@ import qualified TcRnMonad as TcM
 import qualified TcMType as TcM
 import qualified TcEnv as TcM 
        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
+import Kind
 import TcType
 import DynFlags
 
@@ -94,6 +98,7 @@ import Outputable
 import Bag
 import MonadUtils
 import VarSet
+import Pair
 import FastString
 
 import HsBinds               -- for TcEvBinds stuff 
@@ -201,9 +206,9 @@ instance Outputable CanonicalCt where
   ppr (CIPCan ip fl ip_nm ty)     
       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
   ppr (CTyEqCan co fl tv ty)      
-      = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
+      = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyVarTy tv) ty)
   ppr (CFunEqCan co fl tc tys ty) 
-      = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
+      = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyConApp tc tys) ty)
   ppr (CFrozenErr co fl)
       = ppr fl <+> pprEvVarWithType co
 \end{code}
@@ -258,8 +263,58 @@ isCFunEqCan_Maybe _ = Nothing
 isCFrozenErr :: CanonicalCt -> Bool
 isCFrozenErr (CFrozenErr {}) = True
 isCFrozenErr _               = False
+
+
+-- A mixture of Given, Wanted, and Derived constraints. 
+-- We split between equalities and the rest to process equalities first. 
+data WorkList = WorkList { weqs  :: CanonicalCts 
+                                 -- NB: weqs includes equalities /and/ family equalities
+                         , wrest :: CanonicalCts }
+
+unionWorkList :: WorkList -> WorkList -> WorkList
+unionWorkList wl1 wl2
+  = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
+             , wrest = wrest wl1 `andCCan` wrest wl2 }
+
+unionWorkLists :: [WorkList] -> WorkList 
+unionWorkLists = foldr unionWorkList emptyWorkList
+
+isEmptyWorkList :: WorkList -> Bool
+isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
+
+emptyWorkList :: WorkList
+emptyWorkList
+  = WorkList { weqs = emptyBag, wrest = emptyBag }
+
+workListFromEq :: CanonicalCt -> WorkList
+workListFromEq = workListFromEqs . singleCCan
+
+workListFromNonEq :: CanonicalCt -> WorkList
+workListFromNonEq = workListFromNonEqs . singleCCan 
+
+workListFromNonEqs :: CanonicalCts -> WorkList
+workListFromNonEqs cts
+  = WorkList { weqs = emptyCCan, wrest = cts }
+
+workListFromEqs :: CanonicalCts -> WorkList
+workListFromEqs cts
+  = WorkList { weqs = cts, wrest = emptyCCan }
+
+foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r) 
+                           -> r -> WorkList -> m r
+-- Prioritizes equalities
+foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
+  = do { r1 <- foldrBagM on_ct r eqs
+       ; foldrBagM on_ct r1 rest }
+
+instance Outputable WorkList where 
+  ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
+                , text "WorkList (Other)      = " <+> ppr (wrest wl) ]
+
 \end{code}
 
+
+
 %************************************************************************
 %*                                                                     *
                     CtFlavor
@@ -290,12 +345,14 @@ canSolve :: CtFlavor -> CtFlavor -> Bool
 --  active(tv ~ xi)    = tv 
 --  active(D xis)      = D xis 
 --  active(IP nm ty)   = nm 
+--
+-- NB:  either (a `canSolve` b) or (b `canSolve` a) must hold
 -----------------------------------------
 canSolve (Given {})   _            = True 
-canSolve (Derived {}) (Wanted {})  = False -- DV: changing the semantics
-canSolve (Derived {}) (Derived {}) = True  -- DV: changing the semantics of derived 
+canSolve (Wanted {})  (Derived {}) = True
 canSolve (Wanted {})  (Wanted {})  = True
-canSolve _ _ = False
+canSolve (Derived {}) (Derived {}) = True  -- Important: derived can't solve wanted/given
+canSolve _ _ = False                      -- (There is no *evidence* for a derived.)
 
 canRewrite :: CtFlavor -> CtFlavor -> Bool 
 -- canRewrite ctid1 ctid2 
@@ -470,8 +527,8 @@ runTcS context untouch tcs
        ; mapM_ do_unification (varEnvElts ty_binds)
 
 #ifdef DEBUG
-       ; count <- TcM.readTcRef step_count
-       ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count)
+--       ; count <- TcM.readTcRef step_count
+--       ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count)
 #endif
              -- And return
        ; ev_binds      <- TcM.readTcRef evb_ref
@@ -548,10 +605,8 @@ getTcEvBindsBag
   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
        ; wrapTcS $ TcM.readTcRef ev_ref }
 
-setWantedCoBind :: CoVar -> Coercion -> TcS () 
-setWantedCoBind cv co 
-  = setEvBind cv (EvCoercion co)
-     -- Was: wrapTcS $ TcM.writeWantedCoVar cv co 
+setCoBind :: CoVar -> Coercion -> TcS () 
+setCoBind cv co = setEvBind cv (EvCoercion co)
 
 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
 -- Add a type binding
@@ -619,7 +674,7 @@ checkWellStagedDFun pred dfun_id loc
     bind_lvl = TcM.topIdLvl dfun_id
 
 pprEq :: TcType -> TcType -> SDoc
-pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
+pprEq ty1 ty2 = pprPredTy $ mkEqPred (ty1,ty2)
 
 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
 isTouchableMetaTyVar tv 
@@ -706,7 +761,7 @@ newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
 newKindConstraint tv knd 
   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
        ; let ty_k = mkTyVarTy tv_k
-       ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
+       ; co_var <- newCoVar (mkTyVarTy tv) ty_k
        ; return co_var }
 
 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
@@ -737,9 +792,6 @@ newGivenCoVar ty1 ty2 co
        ; setEvBind cv (EvCoercion co) 
        ; return cv } 
 
-newWantedCoVar :: TcType -> TcType -> TcS EvVar 
-newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2 
-
 newCoVar :: TcType -> TcType -> TcS EvVar
 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2