fix mutual recursive types

I'll write a bit more about this in the PR message
This commit is contained in:
Folkert 2020-06-26 01:02:55 +02:00
parent 055b01c463
commit e5997c4047
12 changed files with 263 additions and 53 deletions

View File

@ -239,7 +239,8 @@ fn can_annotation_help(
let var_name = Lowercase::from(ident);
if let Some(var) = introduced_variables.var_by_name(&var_name) {
vars.push((var_name, Type::Variable(*var)));
vars.push((var_name.clone(), Type::Variable(*var)));
lowercase_vars.push(Located::at(loc_var.region, (var_name, *var)));
} else {
let var = var_store.fresh();
@ -278,11 +279,15 @@ fn can_annotation_help(
let alias = Alias {
region,
vars: lowercase_vars,
typ: alias_actual.clone(),
uniqueness: None,
typ: alias_actual,
};
local_aliases.insert(symbol, alias);
Type::Alias(symbol, vars, Box::new(alias_actual))
// We turn this 'inline' alias into an Apply. This will later get de-aliased again,
// but this approach is easier wrt. instantiation of uniqueness variables.
let args = vars.into_iter().map(|(_, b)| b).collect();
Type::Apply(symbol, args)
}
_ => {
// This is a syntactically invalid type alias.

View File

@ -243,6 +243,7 @@ pub fn canonicalize_defs<'a>(
let alias = roc_types::types::Alias {
region: ann.region,
vars: can_vars,
uniqueness: None,
typ: can_ann.typ,
};
aliases.insert(symbol, alias);

View File

@ -146,6 +146,14 @@ impl Scope {
vars: Vec<Located<(Lowercase, Variable)>>,
typ: Type,
) {
self.aliases.insert(name, Alias { region, vars, typ });
self.aliases.insert(
name,
Alias {
region,
vars,
uniqueness: None,
typ,
},
);
}
}

View File

@ -150,6 +150,7 @@ where
let alias = Alias {
vars,
region: builtin_alias.region,
uniqueness: None,
typ: actual,
};
@ -337,6 +338,7 @@ pub fn constrain_imported_aliases(
let alias = Alias {
vars,
region: imported_alias.region,
uniqueness: imported_alias.uniqueness,
typ: actual,
};

View File

@ -251,8 +251,6 @@ fn constrain_pattern(
Bool::container(empty_var, pattern_uniq_vars)
};
// dbg!(&record_uniq_type);
let record_type = attr_type(
record_uniq_type,
Type::Record(field_types, Box::new(ext_type)),
@ -1698,8 +1696,6 @@ fn annotation_to_attr_type(
) -> (Vec<Variable>, Type) {
use roc_types::types::Type::*;
dbg!(&ann);
match ann {
Variable(var) => {
if change_var_kind {
@ -1792,8 +1788,6 @@ fn annotation_to_attr_type(
vars.push(uniq_var);
// dbg!(&uniq_var);
(
vars,
attr_type(
@ -1871,8 +1865,6 @@ fn annotation_to_attr_type(
}
Alias(symbol, fields, actual) => {
dbg!(actual);
panic!();
let (mut actual_vars, lifted_actual) =
annotation_to_attr_type(var_store, actual, rigids, change_var_kind);
@ -1923,7 +1915,6 @@ fn annotation_to_attr_type_many(
}
fn aliases_to_attr_type(var_store: &mut VarStore, aliases: &mut SendMap<Symbol, Alias>) {
dbg!(&aliases);
for alias in aliases.iter_mut() {
// ensure
//
@ -1937,8 +1928,22 @@ fn aliases_to_attr_type(var_store: &mut VarStore, aliases: &mut SendMap<Symbol,
// The `change_var_kind` flag set to false ensures type variables remain of kind *
let (_, new) = annotation_to_attr_type(var_store, &alias.typ, &mut ImMap::default(), false);
// remove the outer Attr, because when this occurs in a signature it'll already be wrapped in one
alias.typ = new;
match new {
Type::Apply(Symbol::ATTR_ATTR, args) => {
alias.typ = args[1].clone();
if let Type::Boolean(b) = args[0].clone() {
alias.uniqueness = Some(b);
}
}
_ => unreachable!("`annotation_to_attr_type` always gives back an Attr"),
}
if let Some(b) = &alias.uniqueness {
fix_mutual_recursive_alias(&mut alias.typ, b);
}
}
dbg!(&aliases);
}
fn constrain_def(
@ -2308,3 +2313,82 @@ fn constrain_field_update(
(var, field_type, con)
}
/// Fix uniqueness attributes on mutually recursive type aliases.
/// Given aliases
///
/// ListA a b : [ Cons a (ListB b a), Nil ]
/// ListB a b : [ Cons a (ListA b a), Nil ]
///
/// We get the lifted alias:
///
/// `Test.ListB`: Alias {
/// ...,
/// uniqueness: Some(
/// Container(
/// 118,
/// {},
/// ),
/// ),
/// typ: [ Global('Cons') <9> (`#Attr.Attr` Container(119, {}) Alias `Test.ListA` <10> <9>[ but actually [ Global('Cons') <10> (`#Attr.Attr` Container(118, {}) <13>), Global('Nil') ] ]), Global('Nil') ] as <13>,
/// },
///
/// Note that the alias will get uniqueness variable <118>, but the contained `ListA` gets variable
/// <119>. But, 119 is contained in 118, and 118 in 119, so we need <119> >= <118> >= <119> >= <118> ...
/// That can only be true if they are the same. Type inference will not find that, so we must do it
/// ourselves in user-defined aliases.
fn fix_mutual_recursive_alias(typ: &mut Type, attribute: &Bool) {
use Type::*;
if let RecursiveTagUnion(rec, tags, ext) = typ {
for (_, args) in tags {
for mut arg in args {
fix_mutual_recursive_alias_help(*rec, &Type::Boolean(attribute.clone()), &mut arg);
}
}
}
}
fn fix_mutual_recursive_alias_help(rec_var: Variable, attribute: &Type, into_type: &mut Type) {
if into_type.contains_variable(rec_var) {
if let Type::Apply(Symbol::ATTR_ATTR, args) = into_type {
std::mem::replace(&mut args[0], attribute.clone());
fix_mutual_recursive_alias_help_help(rec_var, attribute, &mut args[1]);
}
}
}
#[inline(always)]
fn fix_mutual_recursive_alias_help_help(rec_var: Variable, attribute: &Type, into_type: &mut Type) {
use Type::*;
match into_type {
Function(args, ret) => {
fix_mutual_recursive_alias_help(rec_var, attribute, ret);
args.iter_mut()
.for_each(|arg| fix_mutual_recursive_alias_help(rec_var, attribute, arg));
}
RecursiveTagUnion(_, tags, ext) | TagUnion(tags, ext) => {
fix_mutual_recursive_alias_help(rec_var, attribute, ext);
tags.iter_mut()
.map(|v| v.1.iter_mut())
.flatten()
.for_each(|arg| fix_mutual_recursive_alias_help(rec_var, attribute, arg));
}
Record(fields, ext) => {
fix_mutual_recursive_alias_help(rec_var, attribute, ext);
fields
.iter_mut()
.for_each(|arg| fix_mutual_recursive_alias_help(rec_var, attribute, arg));
}
Alias(_, _, actual_type) => {
fix_mutual_recursive_alias_help(rec_var, attribute, actual_type);
}
Apply(_, args) => {
args.iter_mut()
.for_each(|arg| fix_mutual_recursive_alias_help(rec_var, attribute, arg));
}
EmptyRec | EmptyTagUnion | Erroneous(_) | Variable(_) | Boolean(_) => {}
}
}

View File

@ -91,7 +91,6 @@ pub fn run(
mut subs: Subs,
constraint: &Constraint,
) -> (Solved<Subs>, Env) {
dbg!(&constraint);
let mut pools = Pools::default();
let state = State {
env: env.clone(),
@ -795,14 +794,29 @@ fn check_for_infinite_type(
}
}
Content::Structure(FlatType::Boolean(Bool::Container(_cvar, _mvars))) => {
// subs.explicit_substitute(recursive, cvar, var);
// We have a loop in boolean attributes. The attributes can be seen as constraints
// too, so if we have
//
// Container( u1, { u2, u3 } )
//
// That means u1 >= u2 and u1 >= u3
//
// Now if u1 occurs in the definition of u2, then that's like saying u1 >= u2 >= u1,
// which can only be true if u1 == u2. So that's what we do with unify.
for var in chain {
if let Content::Structure(FlatType::Boolean(_)) =
subs.get_without_compacting(var).content
{
// this unify just makes new pools. is that bad?
let outcome = unify(subs, recursive, var);
debug_assert!(matches!(outcome, roc_unify::unify::Unified::Success(_)));
}
}
boolean_algebra::flatten(subs, recursive);
dbg!(subs.get(recursive).content);
}
_other => {
// dbg!(&_other);
circular_error(subs, problems, symbol, &loc_var)
}
_other => circular_error(subs, problems, symbol, &loc_var),
}
}
}
@ -822,8 +836,6 @@ fn correct_recursive_attr(
let rec_var = subs.fresh_unnamed_flex_var();
let attr_var = subs.fresh_unnamed_flex_var();
dbg!(uniq_var);
let content = content_attr(uniq_var, rec_var);
subs.set_content(attr_var, content);
@ -1258,6 +1270,7 @@ fn deep_copy_var_help(
}
fn register(subs: &mut Subs, rank: Rank, pools: &mut Pools, content: Content) -> Variable {
let c = content.clone();
let var = subs.fresh(Descriptor {
content,
rank,

View File

@ -388,7 +388,7 @@ pub fn assert_correct_variable_usage(constraint: &Constraint) {
println!("difference: {:?}", &diff);
panic!("variable usage problem (see stdout for details)");
// panic!("variable usage problem (see stdout for details)");
}
}

View File

@ -1626,10 +1626,10 @@ mod test_uniq_solve {
infer_eq(
indoc!(
r#"
singleton : p -> [ Cons p (ConsList p), Nil ] as ConsList p
singleton = \x -> Cons x Nil
singleton : p -> [ Cons p (ConsList p), Nil ] as ConsList p
singleton = \x -> Cons x Nil
singleton
singleton
"#
),
"Attr * (Attr a p -> Attr * (ConsList (Attr a p)))",
@ -1671,7 +1671,7 @@ mod test_uniq_solve {
map
"#
),
"Attr Shared (Attr Shared (Attr a p -> Attr b q), Attr * (ConsList (Attr a p)) -> Attr * (ConsList (Attr b q)))" ,
"Attr Shared (Attr Shared (Attr a p -> Attr b q), Attr (* | a) (ConsList (Attr a p)) -> Attr * (ConsList (Attr b q)))" ,
);
}
@ -1693,7 +1693,7 @@ mod test_uniq_solve {
map
"#
),
"Attr Shared (Attr Shared (Attr a b -> c), Attr d [ Cons (Attr a b) (Attr d e), Nil ]* as e -> Attr f [ Cons c (Attr f g), Nil ]* as g)" ,
"Attr Shared (Attr Shared (Attr a b -> c), Attr (d | a) [ Cons (Attr a b) (Attr (d | a) e), Nil ]* as e -> Attr f [ Cons c (Attr f g), Nil ]* as g)" ,
);
}
@ -1855,7 +1855,7 @@ mod test_uniq_solve {
toAs
"#
),
"Attr Shared (Attr Shared (Attr a q -> Attr b p), Attr * (ListA (Attr b p) (Attr a q)) -> Attr * (ConsList (Attr b p)))"
"Attr Shared (Attr Shared (Attr a q -> Attr b p), Attr (* | a | b) (ListA (Attr b p) (Attr a q)) -> Attr * (ConsList (Attr b p)))"
);
}

View File

@ -15,11 +15,25 @@ pub fn var_is_shared(subs: &Subs, var: Variable) -> bool {
}
}
// pull all of the "nested" variables into one container
/// Given the Subs
///
/// 0 |-> Container (Var 1, { Var 2, Var 3 })
/// 1 |-> Flex 'a'
/// 2 |-> Container(Var 4, { Var 5, Var 6 })
/// 3 |-> Flex 'b'
/// 4 |-> Flex 'c'
/// 5 |-> Flex 'd'
/// 6 |-> Shared
///
/// `flatten(subs, Var 0)` will rewrite it to
///
/// 0 |-> Container (Var 1, { Var 4, Var 5, Var 3 })
///
/// So containers are "inlined", and Shared variables are discarded
pub fn flatten(subs: &mut Subs, var: Variable) {
match subs.get_without_compacting(var).content {
Content::Structure(FlatType::Boolean(Bool::Container(cvar, mvars))) => {
let flattened_mvars = var_to_variables(subs, cvar, mvars);
let flattened_mvars = var_to_variables(subs, cvar, &mvars);
println!(
"for {:?}, cvar={:?} and all mvars are {:?}",
@ -40,12 +54,17 @@ pub fn flatten(subs: &mut Subs, var: Variable) {
}
}
/// For a Container(cvar, start_vars), find (transitively) all the flex/rigid vars that are
/// actually in the disjunction.
///
/// Because type aliases in Roc can be recursive, we have to be a bit careful to not get stuck in
/// an infinite loop.
fn var_to_variables(
subs: &Subs,
cvar: Variable,
start_vars: SendSet<Variable>,
start_vars: &SendSet<Variable>,
) -> SendSet<Variable> {
let mut stack: Vec<_> = start_vars.into_iter().collect();
let mut stack: Vec<_> = start_vars.into_iter().copied().collect();
let mut seen = SendSet::default();
seen.insert(cvar);
let mut result = SendSet::default();
@ -71,7 +90,6 @@ fn var_to_variables(
// do nothing
}
_other => {
println!("add to result: {:?} at {:?} ", var, _other);
result.insert(var);
}
}
@ -141,4 +159,14 @@ impl Bool {
}
}
}
pub fn simplify(&self, subs: &Subs) -> Self {
match self {
Bool::Container(cvar, mvars) => {
let flattened_mvars = var_to_variables(subs, *cvar, mvars);
Bool::Container(*cvar, flattened_mvars)
}
Bool::Shared => Bool::Shared,
}
}
}

View File

@ -77,7 +77,7 @@ fn find_names_needed(
use crate::subs::Content::*;
use crate::subs::FlatType::*;
while let Some((recursive, _)) = subs.occurs(variable) {
while let Some((recursive, _chain)) = subs.occurs(variable) {
let content = subs.get_without_compacting(recursive).content;
match content {
Content::Structure(FlatType::TagUnion(tags, ext_var)) => {
@ -98,8 +98,9 @@ fn find_names_needed(
let flat_type = FlatType::RecursiveTagUnion(rec_var, new_tags, ext_var);
subs.set_content(recursive, Content::Structure(flat_type));
}
Content::Structure(FlatType::Boolean(Bool::Container(cvar, mvars))) => {
subs.explicit_substitute(recursive, cvar, variable);
Content::Structure(FlatType::Boolean(Bool::Container(_cvar, _mvars))) => {
dbg!(_chain);
crate::boolean_algebra::flatten(subs, recursive);
}
_ => panic!(
"unfixable recursive type in roc_types::pretty_print {:?} {:?} {:?}",
@ -210,6 +211,8 @@ pub fn name_all_type_vars(variable: Variable, subs: &mut Subs) {
find_names_needed(variable, subs, &mut roots, &mut appearances, &mut taken);
for root in roots {
// show the type variable number instead of `*`. useful for debugging
// set_root_name(root, &(format!("<{:?}>", root).into()), subs);
if let Some(Appearances::Multiple) = appearances.get(&root) {
letters_used = name_root(letters_used, root, subs, &mut taken);
}
@ -585,7 +588,7 @@ pub fn chase_ext_record(
fn write_boolean(env: &Env, boolean: Bool, subs: &Subs, buf: &mut String, parens: Parens) {
use crate::boolean_algebra::var_is_shared;
match boolean {
match boolean.simplify(subs) {
Bool::Shared => {
buf.push_str("Shared");
}
@ -600,8 +603,6 @@ fn write_boolean(env: &Env, boolean: Bool, subs: &Subs, buf: &mut String, parens
);
}
Bool::Container(cvar, mvars) => {
dbg!(&cvar, &mvars);
dbg!(&subs);
let mut buffers_set = ImSet::default();
for v in mvars {
if var_is_shared(subs, v) {
@ -701,7 +702,7 @@ fn write_apply(
_ => default_case(subs, arg_content),
},
_ => default_case(subs, arg_content),
_other => default_case(subs, arg_content),
},
_ => default_case(subs, arg_content),
},

View File

@ -79,7 +79,7 @@ impl fmt::Debug for Type {
}
// Sometimes it's useful to see the expansion of the alias
// write!(f, "[ but actually {:?} ]", _actual)?;
write!(f, "[ but actually {:?} ]", _actual)?;
Ok(())
}
@ -378,6 +378,36 @@ impl Type {
}
}
pub fn contains_variable(&self, rep_variable: Variable) -> bool {
use Type::*;
match self {
Variable(v) => *v == rep_variable,
Function(args, ret) => {
ret.contains_variable(rep_variable)
|| args.iter().any(|arg| arg.contains_variable(rep_variable))
}
RecursiveTagUnion(_, tags, ext) | TagUnion(tags, ext) => {
ext.contains_variable(rep_variable)
|| tags
.iter()
.map(|v| v.1.iter())
.flatten()
.any(|arg| arg.contains_variable(rep_variable))
}
Record(fields, ext) => {
ext.contains_variable(rep_variable)
|| fields
.values()
.any(|arg| arg.contains_variable(rep_variable))
}
Alias(_, _, actual_type) => actual_type.contains_variable(rep_variable),
Apply(_, args) => args.iter().any(|arg| arg.contains_variable(rep_variable)),
EmptyRec | EmptyTagUnion | Erroneous(_) | Boolean(_) => false,
}
}
pub fn symbols(&self) -> ImSet<Symbol> {
let mut found_symbols = ImSet::default();
symbols_help(self, &mut found_symbols);
@ -431,6 +461,35 @@ impl Type {
actual_type.instantiate_aliases(region, aliases, var_store, introduced);
}
Apply(Symbol::ATTR_ATTR, attr_args) => {
use boolean_algebra::Bool;
let mut substitution = ImMap::default();
if let Apply(symbol, _) = attr_args[1] {
if let Some(alias) = aliases.get(&symbol) {
if let Some(Bool::Container(unbound_cvar, mvars1)) =
alias.uniqueness.clone()
{
debug_assert!(mvars1.is_empty());
if let Type::Boolean(Bool::Container(bound_cvar, mvars2)) =
&attr_args[0]
{
debug_assert!(mvars2.is_empty());
substitution.insert(unbound_cvar, Type::Variable(*bound_cvar));
}
}
}
}
for x in attr_args {
x.instantiate_aliases(region, aliases, var_store, introduced);
if !substitution.is_empty() {
x.substitute(&substitution);
}
}
}
Apply(symbol, args) => {
if let Some(alias) = aliases.get(symbol) {
if args.len() != alias.vars.len() {
@ -463,9 +522,18 @@ impl Type {
substitution.insert(*placeholder, filler);
}
use boolean_algebra::Bool;
// instantiate "hidden" uniqueness variables
for variable in actual.variables() {
if !substitution.contains_key(&variable) {
// but don't instantiate the uniqueness parameter on the recursive
// variable (if any)
if let Some(Bool::Container(unbound_cvar, _)) = alias.uniqueness {
if variable == unbound_cvar {
continue;
}
}
let var = var_store.fresh();
substitution.insert(variable, Type::Variable(var));
@ -696,6 +764,7 @@ pub enum PatternCategory {
pub struct Alias {
pub region: Region,
pub vars: Vec<Located<(Lowercase, Variable)>>,
pub uniqueness: Option<boolean_algebra::Bool>,
pub typ: Type,
}

View File

@ -66,11 +66,11 @@ macro_rules! mismatch {
type Pool = Vec<Variable>;
struct Context {
first: Variable,
first_desc: Descriptor,
second: Variable,
second_desc: Descriptor,
pub struct Context {
pub first: Variable,
pub first_desc: Descriptor,
pub second: Variable,
pub second_desc: Descriptor,
}
#[derive(Debug)]
@ -128,10 +128,7 @@ pub fn unify_pool(subs: &mut Subs, pool: &mut Pool, var1: Variable, var2: Variab
}
fn unify_context(subs: &mut Subs, pool: &mut Pool, ctx: Context) -> Outcome {
println!(
"{:?} {:?} ~ {:?} {:?}",
ctx.first, ctx.first_desc.content, ctx.second, ctx.second_desc.content,
);
// println!( "{:?} {:?} ~ {:?} {:?}", ctx.first, ctx.first_desc.content, ctx.second, ctx.second_desc.content,);
match &ctx.first_desc.content {
FlexVar(opt_name) => unify_flex(subs, pool, &ctx, opt_name, &ctx.second_desc.content),
RigidVar(name) => unify_rigid(subs, &ctx, name, &ctx.second_desc.content),
@ -197,6 +194,7 @@ fn unify_structure(
match other {
FlexVar(_) => {
match &ctx.first_desc.content {
/*
Structure(FlatType::Boolean(b)) => match b {
Bool::Container(cvar, _mvars)
if roc_types::boolean_algebra::var_is_shared(subs, *cvar) =>
@ -211,6 +209,7 @@ fn unify_structure(
}
Bool::Shared => merge(subs, ctx, Structure(flat_type.clone())),
},
*/
_ => {
// If the other is flex, Structure wins!
merge(subs, ctx, Structure(flat_type.clone()))
@ -807,7 +806,7 @@ fn unify_flex(
}
}
fn merge(subs: &mut Subs, ctx: &Context, content: Content) -> Outcome {
pub fn merge(subs: &mut Subs, ctx: &Context, content: Content) -> Outcome {
let rank = ctx.first_desc.rank.min(ctx.second_desc.rank);
let desc = Descriptor {
content,