Refine GADT casts with GADT approximation of singleton types

[Linyxus]

Fixes #14776.
Fixes #15531.

#12159 refines GADT casts with singleton types to retain the identity of casted stable references.

This causes #14776, where we find that the checker fails when checking some if expressions with GADT constraints. Briefly, the reason why the code snippet in the #14776 crashes:

• The then-branch is typed as T2, the else-body, after GADT casting, is typed as e.data.type & T1.
• When typing the if tree, the assigned type is computed as the union type of T2 and e.data.type & T1, which is T2, with GADT knowledge.
• When checking the if tree, we do not have GADT knowledge any more, and will find the re-computed type T2 | (e.data.type & T1) mismatches with the assigned type T2.
• The checker fails.

It turns out that, the target type in the cast of the then-body, e.data.type & T1, does not contain enough typing information to recover the (simplified) union type of the entire if expression. To fix this issue, we intersect the GADT approximation of the singleton type to preserve as much GADT information as possible. Specifically, now we cast e.data: T to e.data.type & T2 & T1.

This PR also fixes a bug (see #15531) where the typer leaks the internal type parameters in GADT casts, which will break the pickler.

[Linyxus]

It seems that the issue #14776 is not necessarily related to the insertion of GADT casts. So the current fix does not completely solve the problem (See here).

Since the fix for #15531 is valid, I have opened a new PR picked from part of this one to fix #15531 (see #15558). I think we should close this old one now.