Migrate polymorphic lambda set specialization tests

This commit is contained in:
Ayaz Hafiz 2023-04-02 13:12:51 -05:00
parent e72e17fc82
commit 67364e1a42
No known key found for this signature in database
GPG Key ID: 0E2A37416A25EF58
13 changed files with 272 additions and 453 deletions

View File

@ -6151,34 +6151,6 @@ mod solve_expr {
)
}
#[test]
fn issue_3261() {
infer_queries!(
indoc!(
r#"
Named : [Named Str (List Named)]
foo : Named
foo = Named "outer" [Named "inner" []]
#^^^{-1}
Named name outerList = foo
#^^^^^^^^^^^^^^^^^^^^{-1}
# ^^^^ ^^^^^^^^^
{name, outerList}
"#
),
@r#"
foo : [Named Str (List a)] as a
Named name outerList : [Named Str (List a)] as a
name : Str
outerList : List ([Named Str (List a)] as a)
"#
print_only_under_alias: true
)
}
#[test]
fn function_alias_in_signature() {
infer_eq_without_problem(
@ -6231,98 +6203,6 @@ mod solve_expr {
)
}
#[test]
fn lambda_sets_collide_with_captured_var() {
infer_queries!(
indoc!(
r#"
capture : a -> ({} -> Str)
capture = \val ->
thunk =
\{} ->
when val is
_ -> ""
thunk
x : [True, False]
fun =
when x is
True -> capture ""
# ^^^^^^^
False -> capture {}
# ^^^^^^^
fun
#^^^{-1}
"#
),
@r#"
capture : Str -[[capture(1)]]-> ({} -[[thunk(5) {}, thunk(5) Str]]-> Str)
capture : {} -[[capture(1)]]-> ({} -[[thunk(5) {}, thunk(5) Str]]-> Str)
fun : {} -[[thunk(5) {}, thunk(5) Str]]-> Str
"#
);
}
#[test]
fn lambda_sets_collide_with_captured_function() {
infer_queries!(
indoc!(
r#"
Lazy a : {} -> a
after : Lazy a, (a -> Lazy b) -> Lazy b
after = \effect, map ->
thunk = \{} ->
when map (effect {}) is
b -> b {}
thunk
f = \_ -> \_ -> ""
g = \{ s1 } -> \_ -> s1
x : [True, False]
fun =
when x is
True -> after (\{} -> "") f
False -> after (\{} -> {s1: "s1"}) g
fun
#^^^{-1}
"#
),
@r#"fun : {} -[[thunk(9) (({} -[[15]]-> { s1 : Str })) ({ s1 : Str } -[[g(4)]]-> ({} -[[13 Str]]-> Str)), thunk(9) (({} -[[14]]-> Str)) (Str -[[f(3)]]-> ({} -[[11]]-> Str))]]-> Str"#
print_only_under_alias: true
);
}
#[test]
fn lambda_set_niche_same_layout_different_constructor() {
infer_queries!(
indoc!(
r#"
capture : a -> ({} -> Str)
capture = \val ->
thunk =
\{} ->
when val is
_ -> ""
thunk
x : [True, False]
fun =
when x is
True -> capture {a: ""}
False -> capture (A "")
fun
#^^^{-1}
"#
),
@r#"fun : {} -[[thunk(5) [A Str]w_a, thunk(5) { a : Str }]]-> Str"#
);
}
#[test]
fn check_phantom_type() {
infer_eq_without_problem(
@ -6374,339 +6254,6 @@ mod solve_expr {
)
}
#[test]
fn polymorphic_lambda_set_specialization() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
F has f : a -> (b -> {}) | a has F, b has G
G has g : b -> {} | b has G
Fo := {} has [F {f}]
f = \@Fo {} -> g
#^{-1}
Go := {} has [G {g}]
g = \@Go {} -> {}
#^{-1}
main = (f (@Fo {})) (@Go {})
# ^
# ^^^^^^^^^^
"#
),
@r###"
Fo#f(7) : Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
Go#g(8) : Go -[[g(8)]]-> {}
Fo#f(7) : Fo -[[f(7)]]-> (Go -[[g(8)]]-> {})
f (@Fo {}) : Go -[[g(8)]]-> {}
"###
);
}
#[test]
fn polymorphic_lambda_set_specialization_bound_output() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
F has f : a -> ({} -> b) | a has F, b has G
G has g : {} -> b | b has G
Fo := {} has [F {f}]
f = \@Fo {} -> g
#^{-1}
Go := {} has [G {g}]
g = \{} -> @Go {}
#^{-1}
main =
foo = 1
@Go it = (f (@Fo {})) {}
# ^
# ^^^^^^^^^^
{foo, it}
"#
),
@r###"
Fo#f(7) : Fo -[[f(7)]]-> ({} -[[] + b:g(4):1]-> b) | b has G
Go#g(8) : {} -[[g(8)]]-> Go
Fo#f(7) : Fo -[[f(7)]]-> ({} -[[g(8)]]-> Go)
f (@Fo {}) : {} -[[g(8)]]-> Go
"###
);
}
#[test]
fn polymorphic_lambda_set_specialization_with_let_weakened() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
F has f : a -> (b -> {}) | a has F, b has G
G has g : b -> {} | b has G
Fo := {} has [F {f}]
f = \@Fo {} -> g
#^{-1}
Go := {} has [G {g}]
g = \@Go {} -> {}
#^{-1}
main =
# h should get weakened
h = f (@Fo {})
# ^ ^
h (@Go {})
# ^
"#
),
@r###"
Fo#f(7) : Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
Go#g(8) : Go -[[g(8)]]-> {}
h : Go -[[g(8)]]-> {}
Fo#f(7) : Fo -[[f(7)]]-> (Go -[[g(8)]]-> {})
h : Go -[[g(8)]]-> {}
"###
);
}
#[test]
fn polymorphic_lambda_set_specialization_with_let_weakened_unapplied() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
F has f : a -> (b -> {}) | a has F, b has G
G has g : b -> {} | b has G
Fo := {} has [F {f}]
f = \@Fo {} -> g
#^{-1}
Go := {} has [G {g}]
g = \@Go {} -> {}
#^{-1}
main =
#^^^^{-1}
h = f (@Fo {})
# ^ ^
h
"#
),
@r###"
Fo#f(7) : Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
Go#g(8) : Go -[[g(8)]]-> {}
main : b -[[] + b:g(4):1]-> {} | b has G
h : b -[[] + b:g(4):1]-> {} | b has G
Fo#f(7) : Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
"###
);
}
#[test]
fn polymorphic_lambda_set_specialization_with_deep_specialization_and_capture() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
F has f : a, b -> ({} -> ({} -> {})) | a has F, b has G
G has g : b -> ({} -> {}) | b has G
Fo := {} has [F {f}]
f = \@Fo {}, b -> \{} -> g b
#^{-1}
Go := {} has [G {g}]
g = \@Go {} -> \{} -> {}
#^{-1}
main =
(f (@Fo {}) (@Go {})) {}
# ^
"#
),
@r###"
Fo#f(7) : Fo, b -[[f(7)]]-> ({} -[[13 b]]-> ({} -[[] + b:g(4):2]-> {})) | b has G
Go#g(8) : Go -[[g(8)]]-> ({} -[[14]]-> {})
Fo#f(7) : Fo, Go -[[f(7)]]-> ({} -[[13 Go]]-> ({} -[[14]]-> {}))
"###
);
}
#[test]
fn polymorphic_lambda_set_specialization_varying_over_multiple_variables() {
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}]
k = \@E _ -> {}
#^{-1}
f = \flag, a, b ->
# ^ ^
it =
# ^^
when flag is
A -> j a
# ^
B -> j b
# ^
it
# ^^
main = (f A (@C {}) (@D {})) (@E {})
# ^
# ^^^^^^^^^^^^^^^^^^^
#^^^^{-1}
"#
),
@r###"
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)]]-> {}
a : j | j has J
b : j | j has J
it : k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
J#j(2) : j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + j1:j(2):2]-> {}) | j has J, j1 has J, k has K
J#j(2) : j -[[] + j:j(2):1]-> (k -[[] + j1:j(2):2 + j:j(2):2]-> {}) | j has J, j1 has J, k has K
it : k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 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 = \x ->
# ^^
(f A (@C {}) (@D {})) x
# ^
if Bool.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 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
J#j(2) : j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + j1:j(2):2]-> {}) | j has J, j1 has J, k has K
J#j(2) : j -[[] + j:j(2):1]-> (k -[[] + j1:j(2):2 + j:j(2):2]-> {}) | j has J, j1 has J, k has K
it : k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
main : {}
it : k -[[it(21)]]-> {} | k has K
f : [A, B], C, D -[[f(13)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
it : E -[[it(21)]]-> {}
it : F -[[it(21)]]-> {}
"###
);
}
#[test]
fn polymorphic_lambda_set_specialization_branching_over_single_variable() {
infer_queries!(
indoc!(
r#"
app "test" provides [f] 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
D := {} has [J {j: jD}]
jD = \@D _ -> k
E := {} has [K {k}]
k = \@E _ -> {}
f = \flag, a, c ->
it =
when flag is
A -> j a
B -> j a
it c
# ^^ ^
"#
),
@r###"
it : k -[[] + j:j(2):2]-> {} | j has J, k has K
c : k | k has K
"###
);
}
#[test]
fn wrap_recursive_opaque_negative_position() {
infer_eq_without_problem(

View File

@ -0,0 +1,16 @@
app "test" provides [main] to "./platform"
F has f : a -> (b -> {}) | a has F, b has G
G has g : b -> {} | b has G
Fo := {} has [F {f}]
f = \@Fo {} -> g
#^{-1} Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
Go := {} has [G {g}]
g = \@Go {} -> {}
#^{-1} Go#g(8): Go -[[g(8)]]-> {}
main = (f (@Fo {})) (@Go {})
# ^ Fo#f(7): Fo -[[f(7)]]-> (Go -[[g(8)]]-> {})
# ^^^^^^^^^^ Go -[[g(8)]]-> {}

View File

@ -0,0 +1,20 @@
app "test" provides [main] to "./platform"
F has f : a -> ({} -> b) | a has F, b has G
G has g : {} -> b | b has G
Fo := {} has [F {f}]
f = \@Fo {} -> g
#^{-1} Fo#f(7): Fo -[[f(7)]]-> ({} -[[] + b:g(4):1]-> b) | b has G
Go := {} has [G {g}]
g = \{} -> @Go {}
#^{-1} Go#g(8): {} -[[g(8)]]-> Go
main =
foo = 1
@Go it = (f (@Fo {})) {}
# ^ Fo#f(7): Fo -[[f(7)]]-> ({} -[[g(8)]]-> Go)
# ^^^^^^^^^^ {} -[[g(8)]]-> Go
{foo, it}

View File

@ -0,0 +1,22 @@
app "test" provides [f] 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
D := {} has [J {j: jD}]
jD = \@D _ -> k
E := {} has [K {k}]
k = \@E _ -> {}
f = \flag, a, c ->
it =
when flag is
A -> j a
B -> j a
it c
# ^ k | k has K
# ^^ k -[[] + j:j(2):2]-> {} | j has J, k has K

View File

@ -0,0 +1,34 @@
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} C -[[jC(8)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
D := {} has [J {j: jD}]
jD = \@D _ -> k
#^^{-1} D -[[jD(9)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
E := {} has [K {k}]
k = \@E _ -> {}
#^{-1} E#k(10): E -[[k(10)]]-> {}
f = \flag, a, b ->
# ^ j | j has J
# ^ j | j has J
it =
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
when flag is
A -> j a
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + j1:j(2):2]-> {}) | j has J, j1 has J, k has K
B -> j b
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j1:j(2):2 + j:j(2):2]-> {}) | j has J, j1 has J, k has K
it
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
main = (f A (@C {}) (@D {})) (@E {})
# ^ [A, B], C, D -[[f(11)]]-> (E -[[k(10)]]-> {})
# ^^^^^^^^^^^^^^^^^^^ E -[[k(10)]]-> {}
#^^^^{-1} {}

View File

@ -0,0 +1,45 @@
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} C -[[jC(9)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
D := {} has [J {j: jD}]
jD = \@D _ -> k
#^^{-1} D -[[jD(10)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
E := {} has [K {k: kE}]
kE = \@E _ -> {}
#^^{-1} E -[[kE(11)]]-> {}
F := {} has [K {k: kF}]
kF = \@F _ -> {}
#^^{-1} F -[[kF(12)]]-> {}
f = \flag, a, b ->
# ^ j | j has J
# ^ j | j has J
it =
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
when flag is
A -> j a
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + j1:j(2):2]-> {}) | j has J, j1 has J, k has K
B -> j b
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j1:j(2):2 + j:j(2):2]-> {}) | j has J, j1 has J, k has K
it
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
main =
#^^^^{-1} {}
it = \x ->
# ^^ k -[[it(21)]]-> {} | k has K
(f A (@C {}) (@D {})) x
# ^ [A, B], C, D -[[f(13)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
if Bool.true
then it (@E {})
# ^^ E -[[it(21)]]-> {}
else it (@F {})
# ^^ F -[[it(21)]]-> {}

View File

@ -0,0 +1,16 @@
app "test" provides [main] to "./platform"
F has f : a, b -> ({} -> ({} -> {})) | a has F, b has G
G has g : b -> ({} -> {}) | b has G
Fo := {} has [F {f}]
f = \@Fo {}, b -> \{} -> g b
#^{-1} Fo#f(7): Fo, b -[[f(7)]]-> ({} -[[13 b]]-> ({} -[[] + b:g(4):2]-> {})) | b has G
Go := {} has [G {g}]
g = \@Go {} -> \{} -> {}
#^{-1} Go#g(8): Go -[[g(8)]]-> ({} -[[14]]-> {})
main =
(f (@Fo {}) (@Go {})) {}
# ^ Fo#f(7): Fo, Go -[[f(7)]]-> ({} -[[13 Go]]-> ({} -[[14]]-> {}))

View File

@ -0,0 +1,20 @@
app "test" provides [main] to "./platform"
F has f : a -> (b -> {}) | a has F, b has G
G has g : b -> {} | b has G
Fo := {} has [F {f}]
f = \@Fo {} -> g
#^{-1} Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
Go := {} has [G {g}]
g = \@Go {} -> {}
#^{-1} Go#g(8): Go -[[g(8)]]-> {}
main =
# h should get weakened
h = f (@Fo {})
# ^ Fo#f(7): Fo -[[f(7)]]-> (Go -[[g(8)]]-> {})
# ^ Go -[[g(8)]]-> {}
h (@Go {})
# ^ Go -[[g(8)]]-> {}

View File

@ -0,0 +1,19 @@
app "test" provides [main] to "./platform"
F has f : a -> (b -> {}) | a has F, b has G
G has g : b -> {} | b has G
Fo := {} has [F {f}]
f = \@Fo {} -> g
#^{-1} Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
Go := {} has [G {g}]
g = \@Go {} -> {}
#^{-1} Go#g(8): Go -[[g(8)]]-> {}
main =
#^^^^{-1} b -[[] + b:g(4):1]-> {} | b has G
h = f (@Fo {})
# ^ Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
# ^ b -[[] + b:g(4):1]-> {} | b has G
h

View File

@ -0,0 +1,19 @@
app "test" provides [main] to "./platform"
main =
capture : a -> ({} -> Str)
capture = \val ->
thunk =
\{} ->
when val is
_ -> ""
thunk
x : [True, False]
fun =
when x is
True -> capture {a: ""}
False -> capture (A "")
fun
# ^^^ {} -[[thunk(5) [A Str]w_a, thunk(5) { a : Str }]]-> Str

View File

@ -0,0 +1,24 @@
# +opt infer:print_only_under_alias
app "test" provides [main] to "./platform"
main =
Lazy a : {} -> a
after : Lazy a, (a -> Lazy b) -> Lazy b
after = \effect, map ->
thunk = \{} ->
when map (effect {}) is
b -> b {}
thunk
f = \_ -> \_ -> ""
g = \{ s1 } -> \_ -> s1
x : [True, False]
fun =
when x is
True -> after (\{} -> "") f
False -> after (\{} -> {s1: "s1"}) g
fun
# ^^^ {} -[[thunk(9) (({} -[[15]]-> { s1 : Str })) ({ s1 : Str } -[[g(4)]]-> ({} -[[13 Str]]-> Str)), thunk(9) (({} -[[14]]-> Str)) (Str -[[f(3)]]-> ({} -[[11]]-> Str))]]-> Str

View File

@ -0,0 +1,21 @@
app "test" provides [main] to "./platform"
main =
capture : a -> ({} -> Str)
capture = \val ->
thunk =
\{} ->
when val is
_ -> ""
thunk
x : [True, False]
fun =
when x is
True -> capture ""
# ^^^^^^^ Str -[[capture(1)]]-> ({} -[[thunk(5) {}, thunk(5) Str]]-> Str)
False -> capture {}
# ^^^^^^^ {} -[[capture(1)]]-> ({} -[[thunk(5) {}, thunk(5) Str]]-> Str)
fun
# ^^^ {} -[[thunk(5) {}, thunk(5) Str]]-> Str

View File

@ -0,0 +1,16 @@
# +opt infer:print_only_under_alias
app "test" provides [main] to "./platform"
main =
Named : [Named Str (List Named)]
foo : Named
foo = Named "outer" [Named "inner" []]
# ^^^ [Named Str (List a)] as a
Named name outerList = foo
# ^^^^^^^^^^^^^^^^^^^^ [Named Str (List a)] as a
# ^^^^^^^^^ List ([Named Str (List a)] as a)
# ^^^^ Str
{name, outerList}