If a specialization of an ability member has a lambda set that is not
reflected in the unspecialized lambda sets of the member's prototype
signature, then the specialization lambda set is deemed to be immaterial
to the specialization lambda set mapping, and we don't need to associate
it with a particular region from the prototype signature.
This can happen when an opaque contains functions that are some specific
than the generalized prototype signature; for example, when we are
defining a custom impl for an opaque with functions.
Addresses a bug found in 8c3158c3e0
With fixpoint-fixing, we don't want to re-unify type variables that were
just fixed, because doing so may change their shapes in ways that we
explicitly just set them up not to be changed (as fixpoint-fixing
clobbers type variable contents).
However, this restriction need only apply when we re-unify two type
variables that were both involved in the same fixpoint-fixing cycle. If
we have a type variable T that was involved in fixpoint-fixing, and we
unify it with U that wasn't, we know that the $U \notin \bar{T}$, where
$\bar{T}$ is the recursive closure of T. In these cases, we do want to
permit the usual in-band unification of $T \sim U$.
During the unspecialized lambda set compaction procedure, we might end
up trying to merge too many disjoint variables during unspecialized
lambda unification. Avoid doing so, by checking if we're in the
compaction procedure.
Even if there are no changes to alias arguments, and no new variables were
introduced, we may still need to unify the "actual types" of the alias or opaque!
The unification is not necessary from a types perspective (and in fact, we may want
to disable it for `roc check` later on), but it is necessary for the monomorphizer,
which expects identical types to be reflected in the same variable.
As a concrete example, consider the unification of two opaques
P := [Zero, Succ P]
(@P (Succ n)) ~ (@P (Succ o))
`P` has no arguments, and unification of the surface of `P` introduces nothing new.
But if we do not unify the types of `n` and `o`, which are recursion variables, they
will remain disjoint! Currently, the implication of this is that they will be seen
to have separate recursive memory layouts in the monomorphizer - which is no good
for our compilation model.
Closes#3653
