Sometimes, we might need to fixpoint-fix a unification like
[ Bar [ Bar <a>, Foo ], Foo ] as <a> 🛠️ [ Bar <b>, Foo ] as <b>
where we hit a comparison between <a> and <b>. In this case, follow each
recursion point independently and see if we can find the chain to the needle
we were searching for.
Closes#5476
At times we can have alias arguments that are recursive in their
position, but whose recursiveness is not immediately visible in the real
var.
Closes#5330
While unifying two unions, we may turn one of them into a recursive
union. If we don't recognize the recursiveness before merging, we'll
have lost the recursive value of the union.
There are times that multiple concrete types may appear in
unspecialized lambda sets that are being unified. The primary case is
during monomorphization, when unspecialized lambda sets join at the same
time that concrete types get instantiated. Since lambda set
specialization and compaction happens only after unifications are
complete, unifications that monomorphize can induce the above-described
situation.
In these cases,
- unspecialized lambda sets that are due to equivalent type variables
can be compacted, since they are in fact the same specialization.
- unspecialized lambda sets that are due to different type variables
cannot be compacted, even if their types unify, since they may point
to different specializations. For example, consider the unspecialized
lambda set `[[] + [A]:toEncoder:1 + [B]:toEncoder:1]` - this set wants
two encoders, one for `[A]` and one for `[B]`, which is materially
different from the set `[[] + [A, B]:toEncoder:1]`.
When we unify variables in mono, we must invalidate the sections of the
layout cache reached by those variables. Previously we did this by
recording changed variables as those that were `merge`d. However this is
not enough; we must also record all the parent types they came from. The
reason is we may have something like
```
Alias (Foo, a) ~ Alias (Bar, U8)
```
where we will merge `a = U8` but we do not merge the aliases.
Closes#4919
🤦 when we check whether lambdas can be unified or must be
treated as disjoint we previously had a code path that is actually
exponential in its runtime, regardless of whether it succeeds or fails.
Now, it is linear, though degraded (with a clone) if it fails.
We must be careful to ensure that if unifying nested lambda sets
results in disjoint lambdas, that the parent lambda sets are
ultimately treated disjointly as well.
Consider
```
v1: {} -[ foo ({} -[ bar Str ]-> {}) ]-> {}
~ v2: {} -[ foo ({} -[ bar U64 ]-> {}) ]-> {}
```
When considering unification of the nested sets
```
[ bar Str ]
~ [ bar U64 ]
```
we should not unify these sets, even disjointly, because that would
ultimately lead us to unifying
```
v1 ~ v2
=> {} -[ foo ({} -[ bar Str, bar U64 ]-> {}) ] -> {}
```
which is quite wrong - we do not have a lambda `foo` that captures
either `bar captures: Str` or `bar captures: U64`, we have two
different lambdas `foo` that capture different `bars`. The target
unification is
```
v1 ~ v2
=> {} -[ foo ({} -[ bar Str ]-> {}),
foo ({} -[ bar U64 ]-> {}) ] -> {}
```
Closes#4712
