Make sure self-recursive checks only happen after typechecking

Programs like

```
after : ({} -> a), ({} -> b) -> ({} -> b)

fx = after (\{} -> {}) \{} -> if Bool.true then fx {} else {}
```

are legal because they always decay to functions, even if they may not
look like functions syntactically. Rather than using a syntactic check
to check for illegally-recursive functions, we should only perform such
checks after we know the types of values.

Closes #4291
This commit is contained in:
Ayaz Hafiz 2022-10-11 12:58:05 -05:00
parent 99ad019d75
commit ecab8fa25a
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
4 changed files with 74 additions and 80 deletions

View file

@ -8009,4 +8009,39 @@ mod solve_expr {
print_only_under_alias: true
);
}
#[test]
fn self_recursive_function_not_syntactically_a_function() {
infer_eq_without_problem(
indoc!(
r#"
app "test" provides [fx] to "./platform"
after : ({} -> a), ({} -> b) -> ({} -> b)
fx = after (\{} -> {}) \{} -> if Bool.true then fx {} else {}
"#
),
"{} -> {}",
);
}
#[test]
fn self_recursive_function_not_syntactically_a_function_nested() {
infer_eq_without_problem(
indoc!(
r#"
app "test" provides [main] to "./platform"
main =
after : ({} -> a), ({} -> b) -> ({} -> b)
fx = after (\{} -> {}) \{} -> if Bool.true then fx {} else {}
fx
"#
),
"{} -> {}",
);
}
}