When storing variables, merge them directly with the target rather than unifying

When we unify two variables that end up merged, the rank of the
resulting content is the lower of the two variables being merged. But
during storage, we really do mean, take the target descriptor of the
type we're merging against, and don't try to lower to a
possibly-generalized rank! This fixes a couple bugs I didn't even
realize were present!
This commit is contained in:
Ayaz Hafiz 2022-07-29 14:53:14 -04:00
parent 5f115685e4
commit 4657a957f7
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
4 changed files with 106 additions and 59 deletions

View file

@ -6715,7 +6715,7 @@ mod solve_expr {
),
@r#"
A#id(5) : {} -[[id(5)]]-> ({} -[[8(8)]]-> {})
Id#id(3) : {} -[[id(5)]]-> ({} -[[8(8)]]-> {})
Id#id(3) : a -[[] + a:id(3):1]-> ({} -[[] + a:id(3):2]-> a) | a has Id
alias : {} -[[id(5)]]-> ({} -[[8(8)]]-> {})
"#
print_only_under_alias: true
@ -7347,6 +7347,7 @@ mod solve_expr {
#^{-1}
f = \flag, a, b ->
# ^ ^
it =
# ^^
when flag is
@ -7367,17 +7368,90 @@ mod solve_expr {
jC : C -[[jC(8)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
jD : D -[[jD(9)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
E#k(10) : E -[[k(10)]]-> {}
it : k -[[] + j:j(2):2 + j:j(2):2]-> {} | j has J, k has K
J#j(2) : j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + j:j(2):2]-> {}) | j has J, k has K
J#j(2) : j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + j:j(2):2]-> {}) | j has J, k has K
it : k -[[] + j:j(2):2 + j:j(2):2]-> {} | j has J, k has K
f : [A, B], C, D -[[f(11)]]-> (E -[[] + j:j(2):2 + j:j(2):2]-> {}) | j has J
f A (@C {}) (@D {}) : E -[[] + j:j(2):2 + j:j(2):2]-> {} | j has J
a : j | j has J
b : j | j has J
it : k -[[] + j:j(2):2 + a:j(2):2]-> {} | a has J, j has J, k has K
J#j(2) : j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + a:j(2):2]-> {}) | a has J, j has J, k has K
J#j(2) : j -[[] + j:j(2):1]-> (k -[[] + a:j(2):2 + j:j(2):2]-> {}) | a has J, j has J, k has K
it : k -[[] + j:j(2):2 + a:j(2):2]-> {} | a has J, j has J, k has K
f : [A, B], C, D -[[f(11)]]-> (E -[[k(10)]]-> {})
f A (@C {}) (@D {}) : E -[[k(10)]]-> {}
main : {}
"###
);
}
#[test]
fn polymorphic_lambda_set_specialization_varying_over_multiple_variables_two_results() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
J has j : j -> (k -> {}) | j has J, k has K
K has k : k -> {} | k has K
C := {} has [J {j: jC}]
jC = \@C _ -> k
#^^{-1}
D := {} has [J {j: jD}]
jD = \@D _ -> k
#^^{-1}
E := {} has [K {k: kE}]
kE = \@E _ -> {}
#^^{-1}
F := {} has [K {k: kF}]
kF = \@F _ -> {}
#^^{-1}
f = \flag, a, b ->
# ^ ^
it =
# ^^
when flag is
A -> j a
# ^
B -> j b
# ^
it
# ^^
main =
#^^^^{-1}
it =
# ^^
(f A (@C {}) (@D {}))
# ^
if True
then it (@E {})
# ^^
else it (@F {})
# ^^
"#
),
@r###"
jC : C -[[jC(9)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
jD : D -[[jD(10)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
kE : E -[[kE(11)]]-> {}
kF : F -[[kF(12)]]-> {}
a : j | j has J
b : j | j has J
it : k -[[] + j:j(2):2 + a:j(2):2]-> {} | a has J, j has J, k has K
J#j(2) : j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + a:j(2):2]-> {}) | a has J, j has J, k has K
J#j(2) : j -[[] + j:j(2):1]-> (k -[[] + a:j(2):2 + j:j(2):2]-> {}) | a has J, j has J, k has K
it : k -[[] + j:j(2):2 + a:j(2):2]-> {} | a has J, j has J, k has K
main : {}
it : k -[[] + k:k(4):1]-> {} | k has K
f : [A, B], C, D -[[f(13)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
it : E -[[kE(11)]]-> {}
it : F -[[kF(12)]]-> {}
"###
);
}
#[test]
fn polymorphic_lambda_set_specialization_branching_over_single_variable() {
infer_queries!(