Constrain flex inference variables without re-generalization

When constraining a recursive function like

```
f : _ -> {}
f : \_ -> f {}
```

our first step is to solve the value type of `f` relative to its
annotation. We have to be careful that the inference variable in the
signature of `f` is not generalized until after the body of `f` is
solved. Otherwise, we end up admitting polymorphic recursion.
This commit is contained in:
Ayaz Hafiz 2022-11-22 10:43:59 -06:00 committed by Richard Feldman
parent f8d51473d8
commit 5efdecafc9
No known key found for this signature in database
GPG key ID: F1F21AA5B1D9E43B
2 changed files with 35 additions and 10 deletions

View file

@ -3337,8 +3337,6 @@ fn constraint_recursive_function(
let loc_pattern = Loc::at(loc_symbol.region, Pattern::Identifier(loc_symbol.value));
flex_info.vars.extend(new_infer_variables);
let signature_index = constraints.push_type(types, signature);
let annotation_expected = constraints.push_expected_type(FromAnnotation(
@ -3462,14 +3460,25 @@ fn constraint_recursive_function(
let def_con = constraints.exists(vars, and_constraint);
rigid_info.vars.extend(&new_rigid_variables);
flex_info.vars.extend(&new_infer_variables);
rigid_info.constraints.push(constraints.let_constraint(
new_rigid_variables,
def_pattern_state.vars,
[], // no headers introduced (at this level)
def_con,
Constraint::True,
));
rigid_info.constraints.push({
// Solve the body of the recursive function, making sure it lines up with the
// signature.
let rigids = new_rigid_variables;
let flex = def_pattern_state
.vars
.into_iter()
.chain(new_infer_variables);
constraints.let_constraint(
rigids,
flex,
[], // no headers introduced (at this level)
def_con,
Constraint::True,
)
});
rigid_info.def_types.extend(def_pattern_state.headers);
}
}

View file

@ -380,7 +380,6 @@ mod solve_expr {
let known_specializations = abilities_store.iter_declared_implementations().filter_map(
|(impl_key, member_impl)| match member_impl {
MemberImpl::Impl(impl_symbol) => {
dbg!(impl_symbol);
let specialization = abilities_store.specialization_info(*impl_symbol).expect(
"declared implementations should be resolved conclusively after solving",
);
@ -8320,4 +8319,21 @@ mod solve_expr {
print_only_under_alias: true
)
}
#[test]
fn infer_concrete_type_with_inference_var() {
infer_queries!(indoc!(
r#"
app "test" provides [f] to "./platform"
f : _ -> {}
f = \_ -> f {}
#^{-1}
"#
),
@r###"
f : {} -[[f(0)]]-> {}
"###
)
}
}