[commit: ghc] wip/T8503: Prevent recursive Coercible dictionaries (1818464)
git at git.haskell.org
git at git.haskell.org
Thu Nov 21 16:55:35 UTC 2013
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/T8503
Link : http://ghc.haskell.org/trac/ghc/changeset/1818464a6993942978dcf87b52b33b23f0838a6c/ghc
>---------------------------------------------------------------
commit 1818464a6993942978dcf87b52b33b23f0838a6c
Author: Joachim Breitner <mail at joachim-breitner.de>
Date: Wed Nov 20 14:09:08 2013 +0000
Prevent recursive Coercible dictionaries
>---------------------------------------------------------------
1818464a6993942978dcf87b52b33b23f0838a6c
compiler/typecheck/TcErrors.lhs | 3 ---
compiler/typecheck/TcInteract.lhs | 9 ++++-----
compiler/typecheck/TcRnTypes.lhs | 30 ++++++++++++++++++++++++++++--
compiler/typecheck/TcSMonad.lhs | 14 +++++++++++++-
4 files changed, 45 insertions(+), 11 deletions(-)
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 7315b57..3721d2f 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -1168,9 +1168,6 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
all (null . lookupGRE_Name rdr_env) (map dataConName (tyConDataCons tc))
coercible_msg_for_tycon rdr_env tc
- | isRecursiveTyCon tc
- = Just $ nest 2 $ hsep [ ptext $ sLit "because", quotes (ppr tc)
- , ptext $ sLit "is a recursive type constuctor" ]
| isNewTyCon tc
= tyConAbstractMsg rdr_env tc empty
| otherwise
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 4840b3f..312a640 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -1443,6 +1443,7 @@ doTopReactDict inerts fl cls xis
= try_fundeps_and_return
| Just ev <- lookupSolvedDict inerts pred -- Cached
+ , ctEvCheckDepth (ctLocDepth (ctev_loc fl)) ev
= do { setEvBind dict_id (ctEvTerm ev);
; return $ SomeTopInt { tir_rule = "Dict/Top (cached)"
, tir_new_item = Stop } }
@@ -1842,7 +1843,7 @@ matchClassInst _ clas [ ty ] _
matchClassInst _ clas [ _k, ty1, ty2 ] loc
| clas == coercibleClass = do
- traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2
+ traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2 <+> text "at depth" <+> ppr (ctLocDepth loc)
rdr_env <- getGlobalRdrEnvTcS
safeMode <- safeLanguageOn `fmap` getDynFlags
ev <- getCoercibleInst safeMode rdr_env loc ty1 ty2
@@ -1957,7 +1958,6 @@ getCoercibleInst safeMode rdr_env loc ty1 ty2
| Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
Just (_, _, _) <- unwrapNewTyCon_maybe tc,
- not (isRecursiveTyCon tc),
newTyConEtadArity tc <= length tyArgs,
dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
= do markDataConsAsUsed rdr_env tc
@@ -1968,7 +1968,6 @@ getCoercibleInst safeMode rdr_env loc ty1 ty2
| Just (tc,tyArgs) <- splitTyConApp_maybe ty2,
Just (_, _, _) <- unwrapNewTyCon_maybe tc,
- not (isRecursiveTyCon tc),
newTyConEtadArity tc <= length tyArgs,
dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
= do markDataConsAsUsed rdr_env tc
@@ -2005,7 +2004,8 @@ markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
requestCoercible :: CtLoc -> TcType -> TcType -> TcS MaybeNew
requestCoercible loc ty1 ty2 =
ASSERT2( typeKind ty1 `eqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
- newWantedEvVar loc (coercibleClass `mkClassPred` [typeKind ty1, ty1, ty2])
+ newWantedEvVarNonrec loc' (coercibleClass `mkClassPred` [typeKind ty1, ty1, ty2])
+ where loc' = bumpCtLocDepth CountConstraints loc
\end{code}
@@ -2039,7 +2039,6 @@ are present:
3. instance Coercible r b => Coercible (NT t1 t2 ...) b
instance Coercible a r => Coercible a (NT t1 t2 ...)
for a newtype constructor NT where
- * NT is not recursive
* r is the concrete type of NT, instantiated with the arguments t1 t2 ...
* the data constructors of NT are in scope.
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 6cb29bf..e71f178 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -49,7 +49,7 @@ module TcRnTypes(
isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
isGivenCt, isHoleCt,
ctEvidence, mkNonCanonical, mkNonCanonicalCt,
- ctPred, ctEvPred, ctEvTerm, ctEvId,
+ ctPred, ctEvPred, ctEvTerm, ctEvCheckDepth, ctEvId,
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, unionsWC, addFlats, addImplics, mkFlatWC, addInsols,
@@ -1388,7 +1388,6 @@ data CtEvidence
-- rewrite anything other than a derived (there's no evidence!)
-- but if we do manage to solve it may help in solving other goals.
-
ctEvPred :: CtEvidence -> TcPredType
-- The predicate of a flavor
ctEvPred = ctev_pred
@@ -1399,6 +1398,12 @@ ctEvTerm (CtWanted { ctev_evar = ev }) = EvId ev
ctEvTerm ctev@(CtDerived {}) = pprPanic "ctEvTerm: 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 (ctev_loc 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)
@@ -1546,6 +1551,27 @@ subGoalDepthExceeded (SubGoalDepth mc mf) (SubGoalDepth c f)
| otherwise = Nothing
\end{code}
+Note [Preventing recursive dictionaries]
+
+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 conservativey ensure this property using the subgoal depth of
+the constraints: When solving a Coercible constraint at depth d, we do not
+consider evicence from a depth <= d as suitable.
+
+Therefore we need to record the minimum depth allowed to solve a CtWanted. This
+is done in the SubGoalDepth field of CtWanted. Most code now uses mkCtWanted,
+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)
+
%************************************************************************
%* *
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 6dabbed..72d7007 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -43,7 +43,7 @@ module TcSMonad (
xCtFlavor, -- Transform a CtEvidence during a step
rewriteCtFlavor, -- Specialized version of xCtFlavor for coercions
- newWantedEvVar, newWantedEvVarNC, instDFunConstraints,
+ newWantedEvVar, newWantedEvVarNC, newWantedEvVarNonrec, instDFunConstraints,
newDerived,
-- Creation of evidence variables
@@ -1549,6 +1549,18 @@ newWantedEvVarNC loc pty
= do { new_ev <- wrapTcS $ TcM.newEvVar pty
; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
+-- | Variant of newGivenEvVar that has a lower bound on the depth of the result
+newWantedEvVarNonrec :: CtLoc -> TcPredType -> TcS MaybeNew
+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 (Cached (ctEvTerm ctev)) }
+ _ -> do { ctev <- newWantedEvVarNC loc pty
+ ; traceTcS "newWantedEvVarNonrec/cache miss" $ ppr ctev
+ ; return (Fresh ctev) } }
+
newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
newWantedEvVar loc pty
= do { mb_ct <- lookupInInerts pty
More information about the ghc-commits
mailing list