Loopy constraints cause ocamlc to loop

[goldfirere]

(Credit to @ccasin, who devised this example.)

When ocamlc sees

  type 'a t constraint 'a = 'b * 'c

  type cycle = cycle id
  and 'a id = 'a
  and s = cycle t

it goes into a loop and never returns. Tested on 5.0.0. 4.14.0 stack-overflows (but doesn't hang).

This is not a real problem for me or anyone else -- instead, it was what happened after I asked Chris "why do you think that the constraint consistency check for mutually recursive type definitions is OK before the well-foundedness check?". It turns out that it's likely not OK.

[ccasin]

To be clear about "credit", @lpw25 and I devised this a while ago while trying to understand this part of type declaration checking. I should have reported it at the time, but there is some older issue I'm having trouble tracking down now that I thought might be the same problem (but I ran out of time thinking about that and then forgot about it until yesterday). As Richard says, I think this is more a curiosity than a real problem.

[gasche]

If we don't know how to order these tests, maybe we should try to check both well-formedness properties at once?

[garrigue]

Actually here the loop is not in the constraint consistency check, but in update_types, whose role is to close the recursion between mutually recursive type abbreviations.
The point is that it should not call unify before checking well-foundedness. However, we do need to close the recursion, so there is no easy solution.