language-servers/roc
1
0
Fork 0
mirror of https://github.com/roc-lang/roc.git synced 2025-08-17 18:40:17 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions 6

Unify material recursion variables behind aliases and opaques

Browse source 
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
This commit is contained in:
Ayaz Hafiz 2022-07-29 11:01:09 -04:00
parent 94ccfc30a3
commit 1460f60ab1
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
27 changed files with 775 additions and 709 deletions
Download patch file Download diff file Expand all files Collapse all files

40
crates/compiler/unify/src/unify.rs
View file

@ -686,8 +686,6 @@ fn unify_two_aliases<M: MetaCollector>(
.into_iter()
.zip(other_args.all_variables().into_iter());
let length_before = env.subs.len();
for (l, r) in it {
let l_var = env.subs[l];
let r_var = env.subs[r];
@ -695,19 +693,37 @@ fn unify_two_aliases<M: MetaCollector>(
}
if outcome.mismatches.is_empty() {
// 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.
//
// As such, always unify the real vars.
// Don't report real_var mismatches, because they must always be surfaced higher, from
// the argument types.
let mut real_var_outcome =
unify_pool::<M>(env, pool, real_var, other_real_var, ctx.mode);
let _ = real_var_outcome.mismatches.drain(..);
outcome.union(real_var_outcome);
outcome.union(merge(env, ctx, *other_content));
}
let length_after = env.subs.len();
let args_unification_had_changes = length_after != length_before;
if !args.is_empty() && args_unification_had_changes && outcome.mismatches.is_empty() {
// We need to unify the real vars because unification of type variables
// may have made them larger, which then needs to be reflected in the `real_var`.
outcome.union(unify_pool(env, pool, real_var, other_real_var, ctx.mode));
}
outcome
} else {
mismatch!("{:?}", _symbol)