Fix the polymorphic recursion problem of #9603

[garrigue]

#1132 , by relying on unification of polytypes, introduced a limitation to polymorphic recursion.

#9603 is an open problem about unification of polytypes.
This PR fixes the polymorphic recursion case, by removing the reliance on unification.

[lpw25]

This is a neat solution and I believe that it is correct.

[lpw25]

For those following along with this saga -- including my future self -- the reason for using unification in #1132 was described in my comment in #6673. It was to catch cases like:

type 'a t = Leaf of 'a | Node of ('a * 'a) t;;
let rec depth : 'a. 'a t -> _ =
function Leaf x -> x | Node x -> depth x;;

where a universal variable leaks out through a unification variable. This is precisely what occur_univar is designed to check during unification, so by calling unification we get that check for free.

However, #9603 demonstrates that occur_univar is not currently complete and will gratuitously fail in the presence of type aliases with constrained parameters. The solution in this PR is to replace the call to unify (and the corresponding call to occur_univar) with some logic that uses levels to ensure that universal variables do not escape via unification variables. This is essentially an implementation of occur_univar that does not suffer from the aforementioned incompleteness -- although the problem is a bit easier because we don't have to worry about recursive types.

I think the long term solution is to use similar level-based logic to replace occur_univar in unification. Then we can return to relying on unification to check this property in check_univars as well.

[gasche]

Thanks for the explanation, very clear.

[Octachron]

Check-typo is complaining about two white spaces, and I think it would be good for readability to at least add the PR number to the change entry of #1132 (in the 4.11 section).

[Octachron]

Thanks! I will be merging and cherry-picking to 4.11 once the CI is green.

[garrigue]

Cherry picked on 4.11 at commit 3a8ab06