isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
isCFrozenErr,
+ WorkList, unionWorkList, unionWorkLists, isEmptyWorkList, emptyWorkList,
+ workListFromEq, workListFromNonEq,
+ workListFromEqs, workListFromNonEqs, foldrWorkListM,
+
CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
deCanonicalise, mkFrozenError,
- isWanted, isGiven, isDerived,
- isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
+ isWanted, isGivenOrSolved, isDerived,
+ isGivenOrSolvedCt, isGivenCt_maybe,
+ isWantedCt, isDerivedCt, pprFlavorArising,
isFlexiTcsTv,
canRewrite, canSolve,
- combineCtLoc, mkGivenFlavor, mkWantedFlavor,
+ combineCtLoc, mkSolvedFlavor, mkGivenFlavor,
+ mkWantedFlavor,
getWantedLoc,
TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
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,
+ lookupFlatCacheMap, updateFlatCacheMap,
+
getInstEnvs, getFamInstEnvs, -- Getting the environments
getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
import qualified TcMType as TcM
import qualified TcEnv as TcM
( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
+import Kind
import TcType
import DynFlags
import Bag
import MonadUtils
import VarSet
+import Pair
import FastString
import HsBinds -- for TcEvBinds stuff
import Id
-
import TcRnTypes
-
import Data.IORef
+
+import qualified Data.Map as Map
+
+#ifdef DEBUG
+import StaticFlags( opt_PprStyle_Debug )
+import Control.Monad( when )
+#endif
\end{code}
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}
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
isWantedCt :: CanonicalCt -> Bool
isWantedCt ct = isWanted (cc_flavor ct)
-isGivenCt :: CanonicalCt -> Bool
-isGivenCt ct = isGiven (cc_flavor ct)
isDerivedCt :: CanonicalCt -> Bool
isDerivedCt ct = isDerived (cc_flavor ct)
+isGivenCt_maybe :: CanonicalCt -> Maybe GivenKind
+isGivenCt_maybe ct = isGiven_maybe (cc_flavor ct)
+
+isGivenOrSolvedCt :: CanonicalCt -> Bool
+isGivenOrSolvedCt ct = isGivenOrSolved (cc_flavor ct)
+
+
canSolve :: CtFlavor -> CtFlavor -> Bool
-- canSolve ctid1 ctid2
-- The constraint ctid1 can be used to solve ctid2
-- 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
combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
-- Precondition: At least one of them should be wanted
-combineCtLoc (Wanted loc) _ = loc
-combineCtLoc _ (Wanted loc) = loc
-combineCtLoc (Derived loc ) _ = loc
-combineCtLoc _ (Derived loc ) = loc
+combineCtLoc (Wanted loc) _ = loc
+combineCtLoc _ (Wanted loc) = loc
+combineCtLoc (Derived loc ) _ = loc
+combineCtLoc _ (Derived loc ) = loc
combineCtLoc _ _ = panic "combineCtLoc: both given"
-mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
-mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
-mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
-mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
+mkSolvedFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
+-- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
+mkSolvedFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
+mkSolvedFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
+mkSolvedFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
+mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
+mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
+mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
+mkGivenFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
mkWantedFlavor :: CtFlavor -> CtFlavor
mkWantedFlavor (Wanted loc) = Wanted loc
mkWantedFlavor (Derived loc) = Wanted loc
-mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
+mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavor" (ppr fl)
\end{code}
%************************************************************************
tcs_untch :: TcsUntouchables,
- tcs_ic_depth :: Int, -- Implication nesting depth
- tcs_count :: IORef Int -- Global step count
+ tcs_ic_depth :: Int, -- Implication nesting depth
+ tcs_count :: IORef Int, -- Global step count
+
+ tcs_flat_map :: IORef FlatCache
}
+data FlatCache
+ = FlatCache { givenFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor)
+ -- Invariant: all CtFlavors here satisfy isGiven
+ , wantedFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor) }
+ -- Invariant: all CtFlavors here satisfy isWanted
+
+emptyFlatCache :: FlatCache
+emptyFlatCache
+ = FlatCache { givenFlatCache = Map.empty, wantedFlatCache = Map.empty }
+
+newtype FunEqHead = FunEqHead (TyCon,[Xi])
+
+instance Eq FunEqHead where
+ FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && eqTypes xis1 xis2
+
+instance Ord FunEqHead where
+ FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2)
+ = case compare tc1 tc2 of
+ EQ -> cmpTypes xis1 xis2
+ other -> other
+
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables,
-- but records extra TcsTv variables generated during simplification
\begin{code}
data SimplContext
- = SimplInfer -- Inferring type of a let-bound thing
- | SimplRuleLhs -- Inferring type of a RULE lhs
- | SimplInteractive -- Inferring type at GHCi prompt
- | SimplCheck -- Checking a type signature or RULE rhs
- deriving Eq
+ = SimplInfer SDoc -- Inferring type of a let-bound thing
+ | SimplRuleLhs RuleName -- Inferring type of a RULE lhs
+ | SimplInteractive -- Inferring type at GHCi prompt
+ | SimplCheck SDoc -- Checking a type signature or RULE rhs
instance Outputable SimplContext where
- ppr SimplInfer = ptext (sLit "SimplInfer")
- ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
+ ppr (SimplInfer d) = ptext (sLit "SimplInfer") <+> d
+ ppr (SimplCheck d) = ptext (sLit "SimplCheck") <+> d
+ ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
ppr SimplInteractive = ptext (sLit "SimplInteractive")
- ppr SimplCheck = ptext (sLit "SimplCheck")
isInteractive :: SimplContext -> Bool
isInteractive SimplInteractive = True
-- Simplify equalities only, not dictionaries
-- This is used for the LHS of rules; ee
-- Note [Simplifying RULE lhs constraints] in TcSimplify
-simplEqsOnly SimplRuleLhs = True
-simplEqsOnly _ = False
+simplEqsOnly (SimplRuleLhs {}) = True
+simplEqsOnly _ = False
performDefaulting :: SimplContext -> Bool
-performDefaulting SimplInfer = False
-performDefaulting SimplRuleLhs = False
-performDefaulting SimplInteractive = True
-performDefaulting SimplCheck = True
+performDefaulting (SimplInfer {}) = False
+performDefaulting (SimplRuleLhs {}) = False
+performDefaulting SimplInteractive = True
+performDefaulting (SimplCheck {}) = True
---------------
newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
= do { ty_binds_var <- TcM.newTcRef emptyVarEnv
; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
; step_count <- TcM.newTcRef 0
+ ; flat_cache_var <- TcM.newTcRef emptyFlatCache
; let env = TcSEnv { tcs_ev_binds = ev_binds_var
, tcs_ty_binds = ty_binds_var
, tcs_context = context
, tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
, tcs_count = step_count
, tcs_ic_depth = 0
+ , tcs_flat_map = flat_cache_var
}
-- Run the computation
#ifdef DEBUG
; count <- TcM.readTcRef step_count
- ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count)
+ ; when (opt_PprStyle_Debug && count > 0) $
+ TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =")
+ <+> int count <+> ppr context)
#endif
-- And return
; ev_binds <- TcM.readTcRef evb_ref
, tcs_untch = (_outer_range, outer_tcs)
, tcs_count = count
, tcs_ic_depth = idepth
- , tcs_context = ctxt } ->
- let
- inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
+ , tcs_context = ctxt
+ , tcs_flat_map = orig_flat_cache_var
+ } ->
+ do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
-- The inner_range should be narrower than the outer one
-- (thus increasing the set of untouchables) but
-- the inner Tcs-untouchables must be unioned with the
-- outer ones!
- nest_env = TcSEnv { tcs_ev_binds = ref
- , tcs_ty_binds = ty_binds
- , tcs_untch = inner_untch
- , tcs_count = count
- , tcs_ic_depth = idepth+1
- , tcs_context = ctxtUnderImplic ctxt }
- in
- thing_inside nest_env
+
+ ; orig_flat_cache <- TcM.readTcRef orig_flat_cache_var
+ ; flat_cache_var <- TcM.newTcRef orig_flat_cache
+ -- One could be more conservative as well:
+ -- ; flat_cache_var <- TcM.newTcRef emptyFlatCache
+
+ -- Consider copying the results the tcs_flat_map of the
+ -- incomping constraint, but we must make sure that we
+ -- have pushed everything in, which seems somewhat fragile
+ ; let nest_env = TcSEnv { tcs_ev_binds = ref
+ , tcs_ty_binds = ty_binds
+ , tcs_untch = inner_untch
+ , tcs_count = count
+ , tcs_ic_depth = idepth+1
+ , tcs_context = ctxtUnderImplic ctxt
+ , tcs_flat_map = flat_cache_var }
+ ; thing_inside nest_env }
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
ctxtUnderImplic :: SimplContext -> SimplContext
-- See Note [Simplifying RULE lhs constraints] in TcSimplify
-ctxtUnderImplic SimplRuleLhs = SimplCheck
-ctxtUnderImplic ctxt = ctxt
+ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
+ <+> doubleQuotes (ftext n))
+ctxtUnderImplic ctxt = ctxt
tryTcS :: TcS a -> TcS a
--- Like runTcS, but from within the TcS monad
+-- Like runTcS, but from within the TcS monad
-- Ignore all the evidence generated, and do not affect caller's evidence!
-tryTcS tcs
+tryTcS tcs
= TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
; ev_binds_var <- TcM.newTcEvBinds
+ ; flat_cache_var <- TcM.newTcRef emptyFlatCache
; let env1 = env { tcs_ev_binds = ev_binds_var
- , tcs_ty_binds = ty_binds_var }
- ; unTcS tcs env1 })
+ , tcs_ty_binds = ty_binds_var
+ , tcs_flat_map = flat_cache_var }
+ ; unTcS tcs env1 })
-- Update TcEvBinds
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
+getFlatCacheMapVar :: TcS (IORef FlatCache)
+getFlatCacheMapVar
+ = TcS (return . tcs_flat_map)
+
+lookupFlatCacheMap :: TyCon -> [Xi] -> CtFlavor
+ -> TcS (Maybe (TcType,Coercion,CtFlavor))
+-- For givens, we lookup in given flat cache
+lookupFlatCacheMap tc xis (Given {})
+ = do { cache_ref <- getFlatCacheMapVar
+ ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
+ ; return $ Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) }
+-- For wanteds, we first lookup in givenFlatCache.
+-- If we get nothing back then we lookup in wantedFlatCache.
+lookupFlatCacheMap tc xis (Wanted {})
+ = do { cache_ref <- getFlatCacheMapVar
+ ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
+ ; case Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) of
+ Nothing -> return $ Map.lookup (FunEqHead (tc,xis)) (wantedFlatCache cache_map)
+ other -> return other }
+lookupFlatCacheMap _tc _xis (Derived {}) = return Nothing
+
+updateFlatCacheMap :: TyCon -> [Xi]
+ -> TcType -> CtFlavor -> Coercion -> TcS ()
+updateFlatCacheMap _tc _xis _tv (Derived {}) _co
+ = return () -- Not caching deriveds
+updateFlatCacheMap tc xis ty fl co
+ = do { cache_ref <- getFlatCacheMapVar
+ ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
+ ; let new_cache_map
+ | isGivenOrSolved fl
+ = cache_map { givenFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
+ givenFlatCache cache_map }
+ | isWanted fl
+ = cache_map { wantedFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
+ wantedFlatCache cache_map }
+ | otherwise = pprPanic "updateFlatCacheMap, met Derived!" $ empty
+ ; wrapTcS $ TcM.writeTcRef cache_ref new_cache_map }
+
getTcEvBindsBag :: TcS EvBindMap
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
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
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
; 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
projects / ghc-hetmet.git / blobdiff