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
parent 03e6d6d7e0
commit 414a320358
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
2 changed files with 35 additions and 10 deletions

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)]]-> {}
"###
)
}
}