Commit 203cf0e4 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Refactor the code that prevents recursion among Coercible constraints

The main description is in Note [Preventing recursive dictionaries]
in TcRnTypes, which applies only to Coercible dictionaries.

But it was a bit of a mess:
 - It wasn't applied consistently
 - It was being applied to non-Coercible dictionaries in some places

This patch tidies it up.

This hack will largely go away when Richard starts treating Coercible
constraints more like equalities than like dictionaries.
parent ec38deb2
......@@ -394,8 +394,7 @@ interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
\begin{code}
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
| Just ct_i <- findDict (inert_dicts inerts) cls tys
, let ctev_i = ctEvidence ct_i
| Just ctev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
= do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
; case inert_effect of
IRKeep -> return ()
......@@ -1391,8 +1390,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
| not (isWanted fl) -- Never use instances for Given or Derived constraints
= try_fundeps_and_return
| Just ev <- lookupSolvedDict inerts cls xis -- Cached
, ctEvCheckDepth (ctLocDepth loc) ev
| Just ev <- lookupSolvedDict inerts loc cls xis -- Cached
= do { setEvBind dict_id (ctEvTerm ev);
; stopWith fl "Dict/Top (cached)" }
......@@ -2037,7 +2035,7 @@ requestCoercible :: CtLoc -> TcType -> TcType
, TcCoercion ) -- Coercion witnessing (Coercible t1 t2)
requestCoercible loc ty1 ty2
= ASSERT2( typeKind ty1 `tcEqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
do { (new_ev, freshness) <- newWantedEvVarNonrec loc' (mkCoerciblePred ty1 ty2)
do { (new_ev, freshness) <- newWantedEvVar loc' (mkCoerciblePred ty1 ty2)
; return ( case freshness of { Fresh -> [new_ev]; Cached -> [] }
, ctEvCoercion new_ev) }
-- Evidence for a Coercible constraint is always a coercion t1 ~R t2
......
......@@ -95,6 +95,7 @@ import TyCon ( TyCon )
import ConLike ( ConLike(..) )
import DataCon ( DataCon, dataConUserType, dataConOrigArgTys )
import PatSyn ( PatSyn, patSynType )
import TysWiredIn ( coercibleClass )
import TcType
import Annotations
import InstEnv
......@@ -1511,12 +1512,6 @@ ctEvCoercion (CtWanted { ctev_evar = v }) = mkTcCoVarCo v
ctEvCoercion ctev@(CtDerived {}) = pprPanic "ctEvCoercion: derived constraint cannot have id"
(ppr ctev)
-- | Checks whether the evidence can be used to solve a goal with the given minimum depth
ctEvCheckDepth :: SubGoalDepth -> CtEvidence -> Bool
ctEvCheckDepth _ (CtGiven {}) = True -- Given evidence has infinite depth
ctEvCheckDepth min ev@(CtWanted {}) = min <= ctLocDepth (ctEvLoc ev)
ctEvCheckDepth _ ev@(CtDerived {}) = pprPanic "ctEvCheckDepth: cannot consider derived evidence" (ppr ev)
ctEvId :: CtEvidence -> TcId
ctEvId (CtWanted { ctev_evar = ev }) = ev
ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
......@@ -1621,10 +1616,21 @@ subGoalDepthExceeded (SubGoalDepth mc mf) (SubGoalDepth c f)
| c > mc = Just CountConstraints
| f > mf = Just CountTyFunApps
| otherwise = Nothing
-- | Checks whether the evidence can be used to solve a goal with the given minimum depth
-- See Note [Preventing recursive dictionaries]
ctEvCheckDepth :: Class -> CtLoc -> CtEvidence -> Bool
ctEvCheckDepth cls target ev
| isWanted ev
, cls == coercibleClass -- The restriction applies only to Coercible
= ctLocDepth target <= ctLocDepth (ctEvLoc ev)
| otherwise = True
\end{code}
Note [Preventing recursive dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
NB: this will go away when we start treating Coercible as an equality.
We have some classes where it is not very useful to build recursive
dictionaries (Coercible, at the moment). So we need the constraint solver to
prevent that. We conservatively ensure this property using the subgoal depth of
......@@ -1637,12 +1643,11 @@ which initializes it to initialSubGoalDepth (i.e. 0); but when requesting a
Coercible instance (requestCoercible in TcInteract), we bump the current depth
by one and use that.
There are two spots where wanted contraints attempted to be solved using
existing constraints; doTopReactDict in TcInteract (in the general solver) and
newWantedEvVarNonrec (only used by requestCoercible) in TcSMonad. Both use
ctEvCheckDepth to make the check. That function ensures that a Given constraint
can always be used to solve a goal (i.e. they are at depth infinity, for our
purposes)
There are two spots where wanted contraints attempted to be solved
using existing constraints: lookupInertDict and lookupSolvedDict in
TcSMonad. Both use ctEvCheckDepth to make the check. That function
ensures that a Given constraint can always be used to solve a goal
(i.e. they are at depth infinity, for our purposes)
%************************************************************************
......
......@@ -48,7 +48,7 @@ module TcSMonad (
rewriteEqEvidence, -- Yet more specialised, for equality coercions
maybeSym,
newTcEvBinds, newWantedEvVar, newWantedEvVarNC, newWantedEvVarNonrec,
newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
newEvVar, newGivenEvVar,
emitNewDerived, emitNewDerivedEq,
instDFunConstraints,
......@@ -75,7 +75,7 @@ module TcSMonad (
EqualCtList,
lookupSolvedDict, extendFlatCache,
findDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
findFunEq, findTyEqs,
findFunEqsByTyCon, findFunEqs, partitionFunEqs,
......@@ -768,26 +768,34 @@ lookupFlatCache fam_tc tys
lookup_flats flat_cache = findFunEq flat_cache fam_tc tys
lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
-- Is this exact predicate type cached in the solved or canonicals of the InertSet?
lookupInInerts pty
= do { IS { inert_solved_dicts = solved_dicts
, inert_cans = inert_cans }
<- getTcSInerts
lookupInInerts loc pty
= do { inerts <- getTcSInerts
; return $ case (classifyPredType pty) of
ClassPred cls tys
| Just ctev <- findDict solved_dicts cls tys
-> Just ctev
| Just ct <- findDict (inert_dicts inert_cans) cls tys
-> Just (ctEvidence ct)
| Just ev <- lookupSolvedDict inerts loc cls tys
-> Just ev
| otherwise
-> lookupInertDict (inert_cans inerts) loc cls tys
_other -> Nothing -- NB: No caching for equalities, IPs, holes, or errors
}
lookupSolvedDict :: InertSet -> Class -> [Type] -> Maybe CtEvidence
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
= case findDict dicts cls tys of
Just ct | let ev = ctEvidence ct
, ctEvCheckDepth cls loc ev
-> Just ev
_ -> Nothing
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
= findDict solved cls tys
lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
= case findDict solved cls tys of
Just ev | ctEvCheckDepth cls loc ev -> Just ev
_ -> Nothing
\end{code}
......@@ -1574,22 +1582,9 @@ newWantedEvVarNC loc pty
= do { new_ev <- newEvVar pty
; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
-- | Variant of newWantedEvVar that has a lower bound on the depth of the result
-- (see Note [Preventing recursive dictionaries])
newWantedEvVarNonrec :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
newWantedEvVarNonrec loc pty
= do { mb_ct <- lookupInInerts pty
; case mb_ct of
Just ctev | not (isDerived ctev) && ctEvCheckDepth (ctLocDepth loc) ctev
-> do { traceTcS "newWantedEvVarNonrec/cache hit" $ ppr ctev
; return (ctev, Cached) }
_ -> do { ctev <- newWantedEvVarNC loc pty
; traceTcS "newWantedEvVarNonrec/cache miss" $ ppr ctev
; return (ctev, Fresh) } }
newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
newWantedEvVar loc pty
= do { mb_ct <- lookupInInerts pty
= do { mb_ct <- lookupInInerts loc pty
; case mb_ct of
Just ctev | not (isDerived ctev)
-> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
......@@ -1619,7 +1614,7 @@ newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
-- Returns Nothing if cached,
-- Just pred if not cached
newDerived loc pred
= do { mb_ct <- lookupInInerts pred
= do { mb_ct <- lookupInInerts loc pred
; return (case mb_ct of
Just {} -> Nothing
Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment