fix uniqueness attribute on nested recursive aliases

This commit is contained in:
Folkert 2020-06-29 17:08:39 +02:00
parent 3ddfa7c7ce
commit b4480e212a
4 changed files with 102 additions and 22 deletions

View file

@ -1872,6 +1872,57 @@ mod test_uniq_solve {
);
}
#[test]
fn alias_assoc_list_head() {
infer_eq(
indoc!(
r#"
ConsList a : [ Cons a (ConsList a), Nil ]
AssocList a b : ConsList { key: a, value : b }
Maybe a : [ Just a, Nothing ]
# AssocList2 a b : [ Cons { key: a, value : b } (AssocList2 a b), Nil ]
head : AssocList k v -> Maybe { key: k , value: v }
head = \alist ->
when alist is
Cons first _ ->
Just first
Nil ->
Nothing
head
"#
),
"Attr * (Attr (* | a) (AssocList (Attr b k) (Attr c v)) -> Attr * (Maybe (Attr a { key : (Attr b k), value : (Attr c v) })))"
);
}
#[test]
fn cons_list_as_assoc_list_head() {
infer_eq(
indoc!(
r#"
ConsList a : [ Cons a (ConsList a), Nil ]
Maybe a : [ Just a, Nothing ]
head : ConsList { key: k, value: v } -> Maybe { key: k , value: v }
head = \alist ->
when alist is
Cons first _ ->
Just first
Nil ->
Nothing
head
"#
),
"Attr * (Attr (* | a) (ConsList (Attr a { key : (Attr c k), value : (Attr b v) })) -> Attr * (Maybe (Attr a { key : (Attr c k), value : (Attr b v) })))"
);
}
// #[test]
// fn assoc_list_map() {
// infer_eq(

View file

@ -188,10 +188,11 @@ fn find_names_needed(
find_names_needed(args[0].1, subs, roots, root_appearances, names_taken);
find_names_needed(args[1].1, subs, roots, root_appearances, names_taken);
} else {
// TODO should we also look in the actual variable?
for (_, var) in args {
find_names_needed(var, subs, roots, root_appearances, names_taken);
}
// TODO should we also look in the actual variable?
// find_names_needed(_actual, subs, roots, root_appearances, names_taken);
}
}
Error | Structure(Erroneous(_)) | Structure(EmptyRecord) | Structure(EmptyTagUnion) => {
@ -334,8 +335,7 @@ fn write_content(env: &Env, content: Content, subs: &Subs, buf: &mut String, par
}
// useful for debugging
let write_out_alias = false;
if write_out_alias {
if false {
buf.push_str("[[ but really ");
let content = subs.get_without_compacting(_actual).content;
write_content(env, content, subs, buf, parens);

View file

@ -458,29 +458,30 @@ impl Type {
Apply(Symbol::ATTR_ATTR, attr_args) => {
use boolean_algebra::Bool;
let mut substitution = ImMap::default();
debug_assert_eq!(attr_args.len(), 2);
let mut it = attr_args.iter_mut();
let uniqueness_type = it.next().unwrap();
let base_type = it.next().unwrap();
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()
// instantiate the rest
base_type.instantiate_aliases(region, aliases, var_store, introduced);
// correct uniqueness type
// if this attr contains an alias of a recursive tag union, then the uniqueness
// attribute on the recursion variable must match the uniqueness of the whole tag
// union. We enforce that here.
if let Some(rec_uvar) = find_rec_var_uniqueness(base_type, aliases) {
if let Bool::Container(unbound_cvar, mvars1) = rec_uvar {
if let Type::Boolean(Bool::Container(bound_cvar, mvars2)) = uniqueness_type
{
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);
let mut substitution = ImMap::default();
substitution.insert(unbound_cvar, Type::Variable(*bound_cvar));
base_type.substitute(&substitution);
}
}
}
}
@ -689,6 +690,34 @@ fn variables_help(tipe: &Type, accum: &mut ImSet<Variable>) {
}
}
/// We're looking for an alias whose actual type is a recursive tag union
/// if `base_type` is one, return the uniqueness variable of the alias.
fn find_rec_var_uniqueness(
base_type: &Type,
aliases: &ImMap<Symbol, Alias>,
) -> Option<boolean_algebra::Bool> {
use Type::*;
if let Alias(symbol, _, actual) = base_type {
match **actual {
Alias(_, _, _) => find_rec_var_uniqueness(actual, aliases),
RecursiveTagUnion(_, _, _) => {
if let Some(alias) = aliases.get(symbol) {
// alias with a recursive tag union must have its uniqueness set
debug_assert!(alias.uniqueness.is_some());
alias.uniqueness.clone()
} else {
unreachable!("aliases must be defined in the set of aliases!")
}
}
_ => None,
}
} else {
None
}
}
pub struct RecordStructure {
pub fields: MutMap<Lowercase, Variable>,
pub ext: Variable,

View file

@ -553,7 +553,7 @@ fn unify_shared_tags(
}
} else {
// we always unify NonRecursive with Recursive, so this should never happen
debug_assert!(Some(actual) != recursion_var);
debug_assert_ne!(Some(actual), recursion_var);
unify_pool(subs, pool, actual, expected)
};