Merge pull request #2054 from rtfeldman/i/1804-inference-var

Implement type checking in the presence of `_` inference variables
This commit is contained in:
Richard Feldman 2021-11-21 23:58:17 -05:00 committed by GitHub
commit 22adbe0bce
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
5 changed files with 335 additions and 2 deletions

View file

@ -2492,4 +2492,121 @@ pub mod test_constrain {
"custom",
);
}
#[test]
fn inference_var_inside_arrow() {
infer_eq(
indoc!(
r#"
id : _ -> _
id = \x -> x
id
"#
),
"a -> a",
)
}
#[test]
#[ignore = "TODO: Type2::substitute"]
fn inference_var_inside_ctor() {
infer_eq(
indoc!(
r#"
canIGo : _ -> Result _ _
canIGo = \color ->
when color is
"green" -> Ok "go!"
"yellow" -> Err (SlowIt "whoa, let's slow down!")
"red" -> Err (StopIt "absolutely not")
_ -> Err (UnknownColor "this is a weird stoplight")
canIGo
"#
),
"Str -> Result Str [ SlowIt Str, StopIt Str, UnknownColor Str ]*",
)
}
#[test]
#[ignore = "TODO: Gives { x : *, y : * } -> { x : *, y : * }. This is a bug in typechecking defs with annotations."]
fn inference_var_inside_ctor_linked() {
infer_eq(
indoc!(
r#"
swapRcd: {x: _, y: _} -> {x: _, y: _}
swapRcd = \{x, y} -> {x: y, y: x}
swapRcd
"#
),
"{ x : a, y : b } -> { x : b, y : a }",
)
}
#[test]
fn inference_var_link_with_rigid() {
infer_eq(
indoc!(
r#"
swapRcd: {x: tx, y: ty} -> {x: _, y: _}
swapRcd = \{x, y} -> {x: y, y: x}
swapRcd
"#
),
"{ x : tx, y : ty } -> { x : ty, y : tx }",
)
}
#[test]
#[ignore = "TODO: Type2::substitute"]
fn inference_var_inside_tag_ctor() {
infer_eq(
indoc!(
r#"
badComics: Bool -> [ CowTools _, Thagomizer _ ]
badComics = \c ->
when c is
True -> CowTools "The Far Side"
False -> Thagomizer "The Far Side"
badComics
"#
),
"Bool -> [ CowTools Str, Thagomizer Str ]",
)
}
#[test]
fn inference_var_tag_union_ext() {
// TODO: we should really be inferring [ Blue, Orange ]a -> [ Lavender, Peach ]a here.
// See https://github.com/rtfeldman/roc/issues/2053
infer_eq(
indoc!(
r#"
pastelize: _ -> [ Lavender, Peach ]_
pastelize = \color ->
when color is
Blue -> Lavender
Orange -> Peach
col -> col
pastelize
"#
),
"[ Blue, Lavender, Orange, Peach ]a -> [ Blue, Lavender, Orange, Peach ]a",
)
}
#[test]
#[ignore = "TODO: gives { email : a, name : b }c -> { email : a, name : b }c. This is a bug in typechecking defs with annotations."]
fn inference_var_rcd_union_ext() {
infer_eq(
indoc!(
r#"
setRocEmail : _ -> { name: Str, email: Str }_
setRocEmail = \person ->
{ person & email: "\(person.name)@roclang.com" }
setRocEmail
"#
),
"{ email : Str, name : Str }a -> { email : Str, name : Str }a",
)
}
}

View file

@ -390,7 +390,9 @@ pub fn to_type2<'a>(
}
}
Inferred => {
unimplemented!();
let var = env.var_store.fresh();
Type2::Variable(var)
}
Wildcard | Malformed(_) => {
let var = env.var_store.fresh();

View file

@ -460,7 +460,10 @@ fn can_annotation_help(
Type::Variable(var)
}
Inferred => {
unimplemented!();
// Inference variables aren't bound to a rigid or a wildcard, so all we have to do is
// make a fresh unconstrained variable, and let the type solver fill it in for us 🤠
let var = var_store.fresh();
Type::Variable(var)
}
Malformed(string) => {
malformed(env, region, string);

View file

@ -4604,4 +4604,117 @@ mod solve_expr {
"RBTree {}",
);
}
#[test]
fn inference_var_inside_arrow() {
infer_eq_without_problem(
indoc!(
r#"
id : _ -> _
id = \x -> x
id
"#
),
"a -> a",
)
}
#[test]
fn inference_var_inside_ctor() {
infer_eq_without_problem(
indoc!(
r#"
canIGo : _ -> Result _ _
canIGo = \color ->
when color is
"green" -> Ok "go!"
"yellow" -> Err (SlowIt "whoa, let's slow down!")
"red" -> Err (StopIt "absolutely not")
_ -> Err (UnknownColor "this is a weird stoplight")
canIGo
"#
),
"Str -> Result Str [ SlowIt Str, StopIt Str, UnknownColor Str ]*",
)
}
#[test]
fn inference_var_inside_ctor_linked() {
infer_eq_without_problem(
indoc!(
r#"
swapRcd: {x: _, y: _} -> {x: _, y: _}
swapRcd = \{x, y} -> {x: y, y: x}
swapRcd
"#
),
"{ x : a, y : b } -> { x : b, y : a }",
)
}
#[test]
fn inference_var_link_with_rigid() {
infer_eq_without_problem(
indoc!(
r#"
swapRcd: {x: tx, y: ty} -> {x: _, y: _}
swapRcd = \{x, y} -> {x: y, y: x}
swapRcd
"#
),
"{ x : tx, y : ty } -> { x : ty, y : tx }",
)
}
#[test]
fn inference_var_inside_tag_ctor() {
infer_eq_without_problem(
indoc!(
r#"
badComics: Bool -> [ CowTools _, Thagomizer _ ]
badComics = \c ->
when c is
True -> CowTools "The Far Side"
False -> Thagomizer "The Far Side"
badComics
"#
),
"Bool -> [ CowTools Str, Thagomizer Str ]",
)
}
#[test]
fn inference_var_tag_union_ext() {
// TODO: we should really be inferring [ Blue, Orange ]a -> [ Lavender, Peach ]a here.
// See https://github.com/rtfeldman/roc/issues/2053
infer_eq_without_problem(
indoc!(
r#"
pastelize: _ -> [ Lavender, Peach ]_
pastelize = \color ->
when color is
Blue -> Lavender
Orange -> Peach
col -> col
pastelize
"#
),
"[ Blue, Lavender, Orange, Peach ]a -> [ Blue, Lavender, Orange, Peach ]a",
)
}
#[test]
fn inference_var_rcd_union_ext() {
infer_eq_without_problem(
indoc!(
r#"
setRocEmail : _ -> { name: Str, email: Str }_
setRocEmail = \person ->
{ person & email: "\(person.name)@roclang.com" }
setRocEmail
"#
),
"{ email : Str, name : Str }a -> { email : Str, name : Str }a",
)
}
}

View file

@ -6667,4 +6667,102 @@ I need all branches in an `if` to have the same type!
),
)
}
#[test]
fn inference_var_not_enough_in_alias() {
report_problem_as(
indoc!(
r#"
canIGo : _ -> Result _
canIGo = \color ->
when color is
"green" -> Ok "go!"
"yellow" -> Err (SlowIt "whoa, let's slow down!")
"red" -> Err (StopIt "absolutely not")
_ -> Err (UnknownColor "this is a weird stoplight")
canIGo
"#
),
indoc!(
r#"
TOO FEW TYPE ARGUMENTS
The `Result` alias expects 2 type arguments, but it got 1 instead:
1 canIGo : _ -> Result _
^^^^^^^^
Are there missing parentheses?
"#
),
)
}
#[test]
fn inference_var_too_many_in_alias() {
report_problem_as(
indoc!(
r#"
canIGo : _ -> Result _ _ _
canIGo = \color ->
when color is
"green" -> Ok "go!"
"yellow" -> Err (SlowIt "whoa, let's slow down!")
"red" -> Err (StopIt "absolutely not")
_ -> Err (UnknownColor "this is a weird stoplight")
canIGo
"#
),
indoc!(
r#"
TOO MANY TYPE ARGUMENTS
The `Result` alias expects 2 type arguments, but it got 3 instead:
1 canIGo : _ -> Result _ _ _
^^^^^^^^^^^^
Are there missing parentheses?
"#
),
)
}
#[test]
fn inference_var_conflict_in_rigid_links() {
report_problem_as(
indoc!(
r#"
f : a -> (_ -> b)
f = \x -> \y -> if x == y then x else y
f
"#
),
// TODO: We should tell the user that we inferred `_` as `a`
indoc!(
r#"
TYPE MISMATCH
Something is off with the body of the `f` definition:
1 f : a -> (_ -> b)
2 f = \x -> \y -> if x == y then x else y
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The body is an anonymous function of type:
a -> a
But the type annotation on `f` says it should be:
a -> b
Tip: Your type annotation uses `a` and `b` as separate type variables.
Your code seems to be saying they are the same though. Maybe they
should be the same your type annotation? Maybe your code uses them in
a weird way?
"#
),
)
}
}