Description
WfPredicates::compute
returns false
if it can't make progress on an inference variable, and the original obligation should be retried later.
However, wf::predicate_obligations
doesn't check that return type and may (incorrectly) return no obligations.
On #70107 I suggested this:
Maybe it would be better to have a
struct NoProgress;
andcompute
returnResult<(), NoProgress>
instead ofbool
.
I'm pretty sure now that it would've prevented this bug.
Looking at the users, only wfcheck
uses this function, and only for the user-specified bounds, so it's possible inference variables are impossible to find (unless normalization introduces them, I guess?).
It might be fine to just create WellFormed
obligation for the ty::Infer
instead of bailing out (see below, this is the same as moving return false
out of WfPredicats::compute
)
Related, this looks wrong, or perhaps outdated?
It's true that ty::Infer
can't be found as the first type in the recursive call, but compute
is a loop
, and it uses Ty::walk
.
I'm amazed nobody has triggered this assert by e.g. causing an inference variable to be unified with Vec<_>
, how is that possible?
Maybe ty::Infer
should only cause return false
(i.e. return Err(NoProgress)
) for ty0
), not any of its descendants?
(EDIT: Read the code more carefully and the check is ty == ty0
, so while it's not an early like I would prefer, it does seem to only trigger on the root type)
However, a few other things call WfPredicats::compute
and it would be fine for them to create an obligation rather than erroring out, so maybe wf::obligations
itself should do that check?