Commit db3d9711 authored by Joachim Breitner's avatar Joachim Breitner
Browse files

Prevent recursive Coercible dictionaries

parent 310e7e7f
......@@ -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
......
......@@ -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 `tcEqKind` 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.
......
......@@ -50,7 +50,7 @@ module TcRnTypes(
isGivenCt, isHoleCt,
ctEvidence, ctLoc, ctPred,
mkNonCanonical, mkNonCanonicalCt,
ctEvPred, ctEvTerm, ctEvId,
ctEvPred, ctEvTerm, ctEvId, ctEvCheckDepth,
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, unionsWC, addFlats, addImplics, mkFlatWC, addInsols,
......@@ -1396,7 +1396,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
......@@ -1407,6 +1406,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)
......@@ -1554,6 +1559,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)
%************************************************************************
%* *
......
......@@ -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,19 @@ 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
-- (see Note [Preventing recursive dictionaries])
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
......
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