Merge pull request #4563 from roc-lang/fix-recursion-checks-of-inferred-vars

Force occurs check for introduced types after checking annotated bodies
This commit is contained in:
Folkert de Vries 2022-11-23 13:02:50 +01:00 committed by GitHub
commit df7f57e4a3
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 32 additions and 41 deletions

View file

@ -3435,6 +3435,10 @@ fn constraint_recursive_function(
rigid_info.constraints.push({
// Solve the body of the recursive function, making sure it lines up with the
// signature.
//
// This happens when we're checking that the def of a recursive function actually
// aligns with what the (mutually-)recursive signature says, so finish
// generalization of the function.
let rigids = new_rigid_variables;
let flex = def_pattern_state
.vars
@ -3444,7 +3448,16 @@ fn constraint_recursive_function(
constraints.let_constraint(
rigids,
flex,
[], // no headers introduced (at this level)
// Although we will have already introduced the headers of the def in the
// outermost scope when we introduced the rigid variables, we now re-introduce
// them to force an occurs check and appropriate fixing, since we might end up
// inferring recursive types at inference variable points. E.g.
//
// f : _ -> _
// f = \F c -> F (List.map f c)
//
// TODO: I (Ayaz) believe we can considerably simplify all this.
def_pattern_state.headers.clone(),
def_con,
Constraint::True,
)

View file

@ -621,6 +621,7 @@ fn run_in_place(
state.env
}
#[derive(Debug)]
enum Work<'a> {
Constraint {
env: &'a Env,

View file

@ -8336,4 +8336,20 @@ mod solve_expr {
"###
)
}
#[test]
fn solve_inference_var_in_annotation_requiring_recursion_fix() {
infer_queries!(indoc!(
r#"
app "test" provides [translateStatic] to "./platform"
translateStatic : _ -> _
translateStatic = \Element c ->
#^^^^^^^^^^^^^^^{-1}
Element (List.map c translateStatic)
"#
),
@"translateStatic : [Element (List a)] as a -[[translateStatic(0)]]-> [Element (List b)]* as b"
)
}
}

View file

@ -2,7 +2,7 @@
use crate::subs::{
self, AliasVariables, Content, FlatType, GetSubsSlice, Label, Subs, SubsIndex, UnionLabels,
UnionTags, UnsortedUnionLabels, Variable,
UnsortedUnionLabels, Variable,
};
use crate::types::{
name_type_var, name_type_var_with_hint, AbilitySet, Polarity, RecordField, Uls,
@ -101,45 +101,6 @@ fn find_names_needed(
use crate::subs::Content::*;
use crate::subs::FlatType::*;
while let Err((recursive, _chain)) = subs.occurs(variable) {
let rec_var = subs.fresh_unnamed_flex_var();
let content = subs.get_content_without_compacting(recursive);
match content {
Content::Structure(FlatType::TagUnion(tags, ext_var)) => {
let ext_var = *ext_var;
let mut new_tags = MutMap::default();
for (name_index, slice_index) in tags.iter_all() {
let slice = subs[slice_index];
let mut new_vars = Vec::new();
for var_index in slice {
let var = subs[var_index];
new_vars.push(if var == recursive { rec_var } else { var });
}
new_tags.insert(subs[name_index].clone(), new_vars);
}
let mut x: Vec<_> = new_tags.into_iter().collect();
x.sort();
let union_tags = UnionTags::insert_into_subs(subs, x);
let flat_type = FlatType::RecursiveTagUnion(rec_var, union_tags, ext_var);
subs.set_content(recursive, Content::Structure(flat_type));
}
_ => panic!(
"unfixable recursive type in roc_types::pretty_print {:?} {:?} {:?}",
recursive,
variable,
subs.dbg(recursive)
),
}
}
match &subs.get_content_without_compacting(variable).clone() {
RecursionVar { opt_name: None, .. } | FlexVar(None) => {
let root = subs.get_root_key_without_compacting(variable);