Handle recursion limit for subtype and well-formed predicates

[matthewjasper]

Adds a recursion limit check for subtype predicates and well-formed predicates.
-Ztrait-solver=next currently panics with unimplemented for these cases.
These cases are arguably bugs in the occurs check but:

• I could not find a simple way to fix the occurs check
• There should still be a recursion limit check to prevent hangs anyway.

closes #117151

r? types

[compiler-errors]

I think this makes sense but @lcnr knows overflow handling better so passing to them

r? lcnr

[lcnr]

This test feels a bit :/ currently the way we generalize higher ranked types is wrong when subtyping.

we currently do the following (using x for the infer var in x: None<_>):

• emit (and stall on) a Subtype(x <: y) obligation
• the w = a assignment sets x to for<'a> fn(&'a ()), emits a Subtype(y <: z) obligation and generalizes z to fn(&'0 ()).
• we then prove Subtype(x <: y) setting y to for<'a> fn(&'a ()) and then prove Subtype(y <: z) which is now trivial as both types are rigid.

If we were to prove the Subtype obligations before generalizing z we'd get an incorrect error, e.g:

fn main() {
    let mut x = None;
    let y = x;
    let z = Default::default();
    let mut w = (&mut x, z, z);
    let mut temp = None::<for<'a> fn(&'a ())>;
    w.0 = &mut temp;
    w.1 = y;
    w.2 = None::<fn(&'static ())>; //~ ERROR mismatched types
}

It feels like this test mostly tests a very specific impl detail of our subtyping algorithm where we do not try to eagerly make progress on previous Subtype obligations while relating.

I think the explanation here is somewhat misleading. The reason this works is because generalization does not care about subtype relations (apart from the occurs check). I would instead use sth like "Subtyping of inference variables is currently handled via delayed Subtype obligations. We do not immediately process them after constraining one of the involved inference variables. We'd otherwise incorrectly constrain the type of z as generalization does not handle binders correctly".

[lcnr]

r=me on the impl changes, would like to improve the test explanation however

[bors]

☔ The latest upstream changes (presumably #118120) made this pull request unmergeable. Please resolve the merge conflicts.

[lcnr]

@bors r+ rollup

thanks 👍

[bors]

📌 Commit 942e939 has been approved by lcnr

It is now in the queue for this repository.

[bors]

⌛ Testing commit 942e939 with merge 0919ad1...

[bors]

☀️ Test successful - checks-actions
Approved by: lcnr
Pushing 0919ad1 to master...

[rust-timer]

Finished benchmarking commit (0919ad1): comparison URL.

Overall result: no relevant changes - no action needed

@rustbot label: -perf-regression

Instruction count

This benchmark run did not return any relevant results for this metric.

Max RSS (memory usage)

Results

This is a less reliable metric that may be of interest but was not used to determine the overall result at the top of this comment.

	mean	range	count
Regressions ❌ (primary)	-	-	0
Regressions ❌ (secondary)	-	-	0
Improvements ✅ (primary)	-2.5%	[-2.5%, -2.5%]	1
Improvements ✅ (secondary)	-	-	0
All ❌✅ (primary)	-2.5%	[-2.5%, -2.5%]	1

Cycles

This benchmark run did not return any relevant results for this metric.

Binary size

This benchmark run did not return any relevant results for this metric.

Bootstrap: 671.261s -> 672.207s (0.14%)
Artifact size: 313.93 MiB -> 313.91 MiB (-0.01%)