Better extension from meet

[lthls]

The goal of this PR is to prevent meet functions from generating spurious extensions, in particular extensions that merely add again the type that is already present.
To do this, I introduce the module Meet_result, whose main type is defined as follows:

type 'a return_value =
  | Left_input
  | Right_input
  | Both_inputs
  | New_result of 'a

type ('a, 'ext) t =
  | Bottom
  | Ok of 'a return_value * 'ext

Most meet functions are patched to return (t, Typing_env_extension.t) Meet_result.t instead of (t * Typing_env_extension.t) Or_bottom.t.
Note that in many cases several results are correct. For instance, if both inputs are Bottom, then any return value is sound, and purely in terms of approximation all of them except New_result x, with x non-bottom, are a best approximation.
However, correct detection of spurious extensions require that the following rules are followed:

• If both inputs are equivalent and any of them can be used as the result, then Both_inputs must be returned
• If the result is equivalent to one of the inputs, and the input could have been returned as the result, then the corresponding constructor (Left_input or Right_input) must be used
• Otherwise, if the result is obviously bottom then Bottom should be returned, if not then New_result.

This PR also contains two adjacent changes:

• Adding equations that are obviously bottom to a typing environment will generate a compile error. This is probably not going to stay in the final version (either the errors will be removed or a proper Or_bottom type will be used instead).
• Some Typing_env functions have changed to stricter semantics. In particular, add_equation will always meet the new equation with the existing env, so it is not suitable for replacing existing equations. Typing_env_level.join has been patched to not rely on this anymore (the previous implementation was likely buggy anyway, as add_equation would end up doing a meet in some cases anyway). This patch could be extracted and submitted independently with a bit of work.

It also contains a few small fixes for bugs that only showed up with this patch (commits c0dfa82 and 52f85a6). I haven't investigated why they were harmless before the patch, but the fix seems clearly better in both cases.

I've managed to compile Coq with the version of this PR at the time of submission.

[lthls]

I've rebased this PR, and updated it a bit: bottom equations in the typing environment are no longer forbidden.
I've done a few quick performance tests on typecore.ml, with -dprofile and perf stat, and the difference is mostly noise. It's a bit disappointing, as I was hoping that this PR would prevent the meet functions from adding redundant extensions, but it's possible that there weren't that many such extensions to start with, or that adding these extensions was cheap anyway, or that this PR introduces some performance regressions that happen to cancel the improvements.

I've also got an error when compiling Coq with this branch; I'll investigate this a bit and make a patch (here or a PR on stable) once I've found the cause.

[lthls]

The bug with Coq seems to be linked to the conversion of exception handlers into regular ones. I don't have all the details yet, but I have some Pop trap actions that point to a continuation that has been turned into a normal continuation.
The problematic function is the following, in lib/future.ml:

let get x =
  match !x with
  | Finished v -> unnamed, UUID.invalid, id, ref (Val v)
  | Ongoing (name, x) ->
      try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c
      with CEphemeron.InvalidKey ->
        name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null))

(cc @mshinwell)

[Gbury]

Maybe #464 can help with the coq bug ?

[lthls]

Ah, I thought it was merged already. Yes, that's probably the same issue.