This is a follow-up on #59740.

Per e-mail from @findleyr :

I think these types of problems can only arise when we allow taking 'under' when we shouldn't. Consider the abbreviated sequence below.

That 'under' in step 4 is not actually valid. The function types of step 1 are only assignable to each other if they are identical, at which point the 'under' transformation should be invalid.

I think the trick of taking 'under' is just a lossy encoding of the assignability condition for function argument type inference, and should not be a part of the core unification step.

1. func(p.F[int]) ≡ func(func(p.F[T₃]))
2. => (p.F[int]) ≡ (func(p.F[T₃]))
3. => p.F[int] ≡ func(p.F[T₃])
4. => func(func(p.F[int])) ≡ func(p.F[T₃]) (under)

Investigation: a quick change to the code shows:

1. If we only call "under" at the top level this case fails with an error message (as predicted):
   type func(F[int]) of f does not match F[T] (cannot infer T)

2. Some existing tests fail, too, though just about a dozen or so. I've done a cursory examination and it might be possible to address them by being slightly more careful about the under calls (e.g., also allow them at the top-level after looking up a type parameter value).

3. Simply not panicking (but silently return) when we reach the recursion stack limit (i.e., setting panicAtUnificationDepthLimit to false) produces the same error:
   type func(F[int]) of f does not match F[T] (cannot infer T)

We should investigate if we can solve #59740 more correctly by using a more careful approach to calling under.