Save and restore univar_pairs instead of clobbering

[stedolan]

#12910 demonstrates a soundness issue caused by several functions in ctype.ml (e.g. Ctype.equal) incorrectly clobbering univar_pairs. This patch has two changes to resolve this problem:

1. Instead of overwriting, univar_pairs is now temporarily changed and restored afterwards, so e.g. univars remain available across a use of a Ctype.equal
2. During unify_univars, if a univar is found that is missing from univar_pairs, the compiler issues a Misc.fatal_error

Previously, the clobbering of univar_pairs caused mcomp to incorrectly report that two identical types were incompatible, since univar_pairs was overwritten, and unify_univars reported this situation as "not unifiable".

Change (1) above is sufficient to fix the cases found by @yallop, as univar_pairs is no longer clobbered. Change (2) alone turns the soundness issue into a compiler failure, which is less bad. I propose doing both, since I'm not completely convinced that it's correct to reset univar_pairs to the empty list in all the places the compiler does so (even temporarily), and a Misc.fatal_error is better than a silent soundness bug.

[gasche]

I believe that the fix is correct. I would rather move towards less global variables than this glorified dynamic binding, but I don't know how to do it in a sustainable way, so I think that for the time being your approach is better than the current state.

[gasche]

Apologies for forgetting about this. Merged.

[Octachron]

@gasche , my opinion is that the bug fix is subtle enough that it is better to test it in the 5.3 cycle and to not cherry-pick it to 5.2 . Do you agree?

[gasche]

This is a bug that has been there for a while and there is no known urgency. If you believe that it would be costly if it introduced regressions in 5.2 at this stage (I don't realize where things are), it is perfectly fine to delay to 5.3.

[nojb]

For reference, there is now a bug report of actual code in the wild that triggers (2): #13495