Let build_as_type take an environment directly, not a reference to it

[t6s]

Typecore.build_as_type calls Ctype.unify_pat with a refine parameter and a reference to an environment.
While the refine is needed (see #10738), there is no need to keep the updated environment.

This PR makes build_as_types to take a bare environment as its argument, and reduce interleaving of
the level management and updates to the environment.
This change is intended to be a preparation to move levels into the environment.

[trefis]

Apologies in advance because this comment is going to be somewhat off-topic in this PR, but since I have missed a lot of changes the past few months, I'm seizing the opportunity of this PR to ask some questions.

I just took a look at your PR, and #10738 which … I don't completely understand.
Over there Jacques says (and you reiterate here) : "we need a refine in build_as_type". However, having looked only briefly at the code, it seems that what we actually need is just to remove the incorrect comment, and catch the Unify exception (whith unify_pat_types does regardless of refine).
And in fact, build_as_type is called (through solve_pPat_alias) in only one place, where we statically know that refine is None.

To sum up: I haven't actually started thinking about we need an Env.t or Env.t ref in build_as_type, because I'm confused about the PR this one builds on.
Could someone clarify what I've missed? Or could we consider clarifying the code before considering this PR?
(Under the "clarifying the code" umbrella I'd also add that I personally find the use of optional arguments with a default value of None, as is done in the unify_pat* functions, somewhat distasteful).

[trefis]

IIUC, this comment is stale. Could you remove it while you're here?

[garrigue]

It is actually correct. The point of #10738 is that ~refine used to be needed here when typing counter-examples, but check_counter_example_pat no longer calls this code.

[garrigue]

My apologies. The comment is indeed stale. #10738 just changed from calling unify to unify_pat_types, so that we get a proper error message. ~refine is irrelevant here.

[gasche]

@Octachron, @garrigue, @t6s and myself had a meeting today -- February's occurrence of the "discussing type-system refactoring PRs" monthly meeting -- where I asked similar/related question. (My question was: "is it actually the case that it does not change the behavior"?). The observable result of my question is that Jacques got into an infinite loop tracing what could possibly theoretically go wrong, and we had to interrupt him -- we will never know if he would have eventually concluded that the change was safe. We didn't make a definitive decision about the PR but I think that the general feeling in the room was to make sure that we understand where we want to go on this change.

One point that was interesting to me (and is briefly explained in the description of this PR) is that the type-checking of pattern matching used to mutate the environment (especially when checking GADT patterns), but not change the level. A couple years ago we started raising levels to deal with or-patterns in GADTs. Now @garrigue and @t6s are trying to add level information into the environment (as suggested by @lpw25, a change that is probably quite desirable), but they don't know how to mix changes to the level and changes to the GADT equations in the same environment. This is why they are trying to do this.

[garrigue]

Apparently all this story started from #10738, which rather than fixing #10735 as suggested by @lpw25, turned it into a proper error.
Since this kind of code was never accepted before, I would tend to say that it is reasonable to fail here.
Some might find it strange to fail only when there is an alias, but this is also the case for or-patterns.

Since build_as_type actually never mutated the environment, this PR is correct.
I will clean up the code to clarify that.

[t6s]

Subsumed by #12025 .