Typing_env_level.join_types: use correct typing env

[lthls]

There is an issue during Typing_env_level.join_types where the environment used for the accumulated equations is wrong.

Here is how the code works, on the following example inputs (in this case the result is correct even without this patch though):

Use 1:
x : (= 0)
y : (= x)

Use 2:
x : (= 1)
y : (= 1)

The aim of this function is to compute a map of equations that are a sound approximation of the equations of each input.
In this case, one possible result would be:

x : {0, 1}
y : (= x)

However, other correct but less precise results can be returned too.

Because the number of uses can be arbitrary, the join is not done between two inputs but instead built by folding on the list of uses, accumulating the result so far. So in practice we will have two steps:

• Join an empty map with Use 1, producing Join 1
• Join Join 1 with Use 2, producing the final result.

All of this is not changed by this patch.
However, to be able to join types, we need an environment in which they are valid. For the empty map, the original env_at_fork works (it's actually used even if the map is empty). For each of the uses, we have a corresponding env_at_use that we can use (for some reason, in one place env_at_fork was used instead. I'm not convinced by the comment justifying this, and chose to use env_at_use as it's more coherent). The problem is in having an environment for the partial results (like Join 1 earlier).

Before the patch, this environment was computed along the result equations by accumulation: starting from env_at_fork for the empty equations, for the following steps environments are computed by first resolving which equations will end up in the joined types (with all joins done using the accumulated environment at the start of the step), and then adding all those equations to the environment that we had at the start of the step; the resulting environment will be used for the next step.

There are two main problems with this approach:

• First, and this is why I had already patched this code in Better extension from meet #316, it relies on Typing_env.add_equation being able to replace an existing equation with a less precise one. This isn't even actually ensured in all cases by the code of add_equation, but the fact that in some cases it was still possible to lose information by doing add_equation was already problematic in a number of other places so in Better extension from meet #316 Typing_env.add_equation always meets with the current type if any. This means it is not suitable for this particular case anymore, so I had to patch this part of the code.
• Second, in a Typing_env.t not all information is held in the equations. The aliases part of the structure also contain information, and this information is not removed if an equation (say, x : (= 0)) is replaced by another (x : {0, 1}). This means that the result is an environment where x has type {0, 1} but is known from the aliases to be equal to 0.

To fix this, this patch simply re-computes at each step a suitable environment for the join functions. Starting from env_at_fork, the equations from the accumulator (joined_types in the code) are added to this environment using a Typing_env_extension, which yields an environment in which the equations from joined_types are valid. This environment is discarded at the end of the step and a new one is created for the next step.
This avoids both problems: the first because we're never trying to forget equations so we don't need to rely on a replace semantics for add_equation, and the second one because since we start from env_at_fork at each step the only aliases we will have are the ones coming from env_at_fork (which are always valid in all branches) and the ones that are created by the joined_types.

[chambart]

I would prefer this one to be named env_at_fork

[chambart]

We might want to add a comment mentionning that there might be some cost here (to look if there is something too expensive hapennening aroung join)

[chambart]

Good when the CI is good.