Merge pull request #3455 from rtfeldman/opaque-recursion-var

Support recursion var unification in opaque types
This commit is contained in:
Folkert de Vries 2022-07-08 22:18:26 +02:00 committed by GitHub
commit 15fee6fc9c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 137 additions and 27 deletions

View file

@ -41,6 +41,7 @@ use roc_types::types::AliasCommon;
use roc_types::types::AliasKind;
use roc_types::types::AliasVar;
use roc_types::types::LambdaSet;
use roc_types::types::OptAbleType;
use roc_types::types::{Alias, Type};
use std::fmt::Debug;
@ -2359,15 +2360,22 @@ fn make_tag_union_of_alias_recursive<'a>(
let alias_args = alias
.type_variables
.iter()
.map(|l| (l.value.name.clone(), Type::Variable(l.value.var)))
.collect::<Vec<_>>();
.map(|l| Type::Variable(l.value.var));
let alias_opt_able_vars = alias.type_variables.iter().map(|l| OptAbleType {
typ: Type::Variable(l.value.var),
opt_ability: l.value.opt_bound_ability,
});
let lambda_set_vars = alias.lambda_set_variables.iter();
let made_recursive = make_tag_union_recursive_help(
env,
Loc::at(
alias.header_region(),
(alias_name, alias_args.iter().map(|ta| &ta.1)),
),
Loc::at(alias.header_region(), alias_name),
alias_args,
alias_opt_able_vars,
lambda_set_vars,
alias.kind,
alias.region,
others,
&mut alias.typ,
@ -2414,9 +2422,14 @@ enum MakeTagUnionRecursive {
/// ```
///
/// When `Err` is returned, a problem will be added to `env`.
#[allow(clippy::too_many_arguments)]
fn make_tag_union_recursive_help<'a, 'b>(
env: &mut Env<'a>,
recursive_alias: Loc<(Symbol, impl Iterator<Item = &'b Type>)>,
recursive_alias: Loc<Symbol>,
alias_args: impl Iterator<Item = Type>,
alias_opt_able_vars: impl Iterator<Item = OptAbleType>,
lambda_set_variables: impl Iterator<Item = &'b LambdaSet>,
alias_kind: AliasKind,
region: Region,
others: Vec<Symbol>,
typ: &'b mut Type,
@ -2425,21 +2438,33 @@ fn make_tag_union_recursive_help<'a, 'b>(
) -> MakeTagUnionRecursive {
use MakeTagUnionRecursive::*;
let (symbol, args) = recursive_alias.value;
let symbol = recursive_alias.value;
let alias_region = recursive_alias.region;
match typ {
Type::TagUnion(tags, ext) => {
let recursion_variable = var_store.fresh();
let type_arguments: Vec<_> = args.into_iter().cloned().collect();
let type_arguments: Vec<_> = alias_args.collect();
let mut pending_typ =
Type::RecursiveTagUnion(recursion_variable, tags.to_vec(), ext.clone());
let substitution_result = pending_typ.substitute_alias(
symbol,
&type_arguments,
&Type::Variable(recursion_variable),
);
let substitution = match alias_kind {
// Inline recursion var directly wherever the alias is used.
AliasKind::Structural => Type::Variable(recursion_variable),
// Wrap the recursion var in the opaque wherever it's used to avoid leaking the
// inner type out as structural.
AliasKind::Opaque => Type::Alias {
symbol,
type_arguments: alias_opt_able_vars.collect(),
lambda_set_variables: lambda_set_variables.cloned().collect(),
actual: Box::new(Type::Variable(recursion_variable)),
kind: AliasKind::Opaque,
},
};
let substitution_result =
pending_typ.substitute_alias(symbol, &type_arguments, &substitution);
match substitution_result {
Ok(()) => {
// We can substitute the alias presence for the variable exactly.
@ -2464,19 +2489,25 @@ fn make_tag_union_recursive_help<'a, 'b>(
Type::Alias {
actual,
type_arguments,
lambda_set_variables,
kind,
..
} => {
// NB: We need to collect the type arguments to shut off rustc's closure type
// instantiator. Otherwise we get unfortunate errors like
// reached the recursion limit while instantiating `make_tag_union_recursive_help::<...n/src/def.rs:1879:65: 1879:77]>>`
#[allow(clippy::needless_collect)]
let type_arguments: Vec<&Type> = type_arguments.iter().map(|ta| &ta.typ).collect();
let recursive_alias = Loc::at_zero((symbol, type_arguments.into_iter()));
let alias_args: Vec<Type> = type_arguments.iter().map(|ta| ta.typ.clone()).collect();
let recursive_alias = Loc::at_zero(symbol);
// try to make `actual` recursive
make_tag_union_recursive_help(
env,
recursive_alias,
alias_args.into_iter(),
type_arguments.iter().cloned(),
lambda_set_variables.iter(),
*kind,
region,
others,
actual,

View file

@ -7101,4 +7101,42 @@ mod solve_expr {
"F * {}* -> F * Str",
);
}
#[test]
fn wrap_recursive_opaque_negative_position() {
infer_eq_without_problem(
indoc!(
r#"
OList := [Nil, Cons {} OList]
lst : [Cons {} OList]*
olist : OList
olist = (\l -> @OList l) lst
olist
"#
),
"OList",
);
}
#[test]
fn wrap_recursive_opaque_positive_position() {
infer_eq_without_problem(
indoc!(
r#"
OList := [Nil, Cons {} OList]
lst : [Cons {} OList]*
olist : OList
olist = @OList lst
olist
"#
),
"OList",
);
}
}

View file

@ -786,6 +786,7 @@ fn unify_opaque<M: MetaCollector>(
Alias(_, _, other_real_var, AliasKind::Structural) => {
unify_pool(subs, pool, ctx.first, *other_real_var, ctx.mode)
}
RecursionVar { structure, .. } => unify_pool(subs, pool, ctx.first, *structure, ctx.mode),
Alias(other_symbol, other_args, other_real_var, AliasKind::Opaque) => {
// Opaques types are only equal if the opaque symbols are equal!
if symbol == *other_symbol {
@ -2583,19 +2584,14 @@ fn unify_recursion<M: MetaCollector>(
},
),
// _opaque has an underscore because it's unused in --release builds
Alias(_opaque, _, _, AliasKind::Opaque) => {
mismatch!(
"RecursionVar {:?} cannot be equal to opaque {:?}",
ctx.first,
_opaque
)
Alias(_, _, actual, AliasKind::Structural) => {
// look at the type the alias stands for
unify_pool(subs, pool, ctx.first, *actual, ctx.mode)
}
Alias(_, _, actual, _) => {
// look at the type the alias stands for
unify_pool(subs, pool, ctx.first, *actual, ctx.mode)
Alias(_, _, _, AliasKind::Opaque) => {
// look at the type the recursion var stands for
unify_pool(subs, pool, structure, ctx.second, ctx.mode)
}
RangedNumber(..) => mismatch!(