Ensure that disjoint nested lambda sets force parents to be disjoint

We must be careful to ensure that if unifying nested lambda sets
results in disjoint lambdas, that the parent lambda sets are
ultimately treated disjointly as well.
Consider

```
  v1: {} -[ foo ({} -[ bar Str ]-> {}) ]-> {}
~ v2: {} -[ foo ({} -[ bar U64 ]-> {}) ]-> {}
```

When considering unification of the nested sets

```
  [ bar Str ]
~ [ bar U64 ]
```

we should not unify these sets, even disjointly, because that would
ultimately lead us to unifying

```
v1 ~ v2
=> {} -[ foo ({} -[ bar Str, bar U64 ]-> {}) ] -> {}
```

which is quite wrong - we do not have a lambda `foo` that captures
either `bar captures: Str` or `bar captures: U64`, we have two
different lambdas `foo` that capture different `bars`. The target
unification is

```
v1 ~ v2
=> {} -[ foo ({} -[ bar Str ]-> {}),
         foo ({} -[ bar U64 ]-> {}) ] -> {}
```

Closes #4712
This commit is contained in:
Ayaz Hafiz 2022-12-12 14:51:18 -06:00
parent 6b2497f342
commit cd2b936a59
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
3 changed files with 128 additions and 16 deletions

View file

@ -8470,4 +8470,63 @@ mod solve_expr {
"###
);
}
#[test]
fn disjoint_nested_lambdas_result_in_disjoint_parents_issue_4712() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Parser a : {} -> a
v1 : {}
v1 = {}
v2 : Str
v2 = ""
apply : Parser (a -> Str), a -> Parser Str
apply = \fnParser, valParser ->
\{} ->
(fnParser {}) (valParser)
map : a, (a -> Str) -> Parser Str
map = \simpleParser, transform ->
apply (\{} -> transform) simpleParser
parseInput = \{} ->
when [ map v1 (\{} -> ""), map v2 (\s -> s) ] is
# ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
_ -> ""
main = parseInput {} == ""
"#
),
@r###"
v1 = {}
v2 = ""
apply = \fnParser, valParser-> \{} -[9]-> (fnParser {}) valParser
map = \simpleParser, transform-> apply \{} -[12]-> transform simpleParser
parseInput =
\{}->
when [
map v1 \{} -[13]-> "",
map v2 \s -[14]-> s,
] is
_ -> ""
main = Bool.isEq (parseInput {}) ""
[ map v1 (\{} -> ""), map v2 (\s -> s) ] : List (({} -[[9 (({} -[[12 (Str -[[14]]-> Str)]]-> (Str -[[14]]-> Str))) Str, 9 (({} -[[12 ({} -[[13]]-> Str)]]-> ({} -[[13]]-> Str))) {}]]-> Str))
"###
print_only_under_alias: true
print_can_decls: true
);
}
}