From 958dc5636c49c26b43de806b0d291372caba2e79 Mon Sep 17 00:00:00 2001 From: Karl Meakin Date: Fri, 17 Feb 2023 01:42:59 +0000 Subject: [PATCH] Improve diagnostic messages for errors in elaborating fun apps --- fathom/src/surface/elaboration.rs | 46 ++++++++-- fathom/src/surface/elaboration/reporting.rs | 63 ++++++++++++-- .../elaboration/fun-app/head-not-fun.fathom | 5 ++ .../elaboration/fun-app/head-not-fun.snap | 19 +++++ .../elaboration/fun-app/too-many-args.fathom | 21 +++++ .../elaboration/fun-app/too-many-args.snap | 83 +++++++++++++++++++ .../unbound-head-1.fathom | 0 .../unbound-head-1.snap | 2 +- .../unbound-head-2.fathom | 0 .../unbound-head-2.snap | 2 +- .../implicit-args/unexpected-argument.snap | 8 +- .../unexpected-argument/record-type.fathom | 3 - .../unexpected-argument/record-type.snap | 11 --- 13 files changed, 227 insertions(+), 36 deletions(-) create mode 100644 tests/fail/elaboration/fun-app/head-not-fun.fathom create mode 100644 tests/fail/elaboration/fun-app/head-not-fun.snap create mode 100644 tests/fail/elaboration/fun-app/too-many-args.fathom create mode 100644 tests/fail/elaboration/fun-app/too-many-args.snap rename tests/fail/elaboration/{unexpected-argument => fun-app}/unbound-head-1.fathom (100%) rename tests/fail/elaboration/{unexpected-argument => fun-app}/unbound-head-1.snap (55%) rename tests/fail/elaboration/{unexpected-argument => fun-app}/unbound-head-2.fathom (100%) rename tests/fail/elaboration/{unexpected-argument => fun-app}/unbound-head-2.snap (56%) delete mode 100644 tests/fail/elaboration/unexpected-argument/record-type.fathom delete mode 100644 tests/fail/elaboration/unexpected-argument/record-type.snap diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index cf4a19466..a1b1b8653 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -1474,9 +1474,13 @@ impl<'arena> Context<'arena> { } Term::App(range, head_expr, args) => { let mut head_range = head_expr.range(); - let (mut head_expr, mut head_type) = self.synth(head_expr); + let (mut head_expr, head_type) = self.synth(head_expr); - for arg in *args { + let original_head_range = head_range; + let original_head_type = self.elim_env().force(&head_type); + let mut head_type = original_head_type.clone(); + + for (arity, arg) in args.iter().enumerate() { head_type = self.elim_env().force(&head_type); match arg.plicity { @@ -1509,13 +1513,39 @@ impl<'arena> Context<'arena> { _ if head_expr.is_error() || head_type.is_error() => { return self.synth_reported_error(*range); } + // NOTE: We could try to infer that this is a function type, + // but this takes more work to prevent cascading type errors + _ if arity == 0 => { + self.push_message(Message::FunAppNotFun { + head_range: self.file_range(original_head_range), + head_type: self.pretty_value(&original_head_type), + num_args: args.len(), + args_range: { + let first = args.first().unwrap(); + let last = args.last().unwrap(); + self.file_range(ByteRange::merge( + first.term.range(), + last.term.range(), + )) + }, + }); + return self.synth_reported_error(*range); + } _ => { - // NOTE: We could try to infer that this is a function type, - // but this takes more work to prevent cascading type errors - self.push_message(Message::UnexpectedArgument { - head_range: self.file_range(head_range), - head_type: self.pretty_value(&head_type), - arg_range: self.file_range(arg.term.range()), + self.push_message(Message::FunAppTooManyArgs { + head_range: self.file_range(original_head_range), + head_type: self.pretty_value(&original_head_type), + expected_arity: arity, + actual_arity: args.len(), + extra_args_range: { + let extra_args = &args[arity..]; + let first = extra_args.first().unwrap(); + let last = extra_args.last().unwrap(); + self.file_range(ByteRange::merge( + first.term.range(), + last.term.range(), + )) + }, }); return self.synth_reported_error(*range); } diff --git a/fathom/src/surface/elaboration/reporting.rs b/fathom/src/surface/elaboration/reporting.rs index 8982d02be..4d2474c2b 100644 --- a/fathom/src/surface/elaboration/reporting.rs +++ b/fathom/src/surface/elaboration/reporting.rs @@ -30,10 +30,18 @@ pub enum Message { UnexpectedParameter { param_range: FileRange, }, - UnexpectedArgument { + FunAppNotFun { head_range: FileRange, head_type: String, - arg_range: FileRange, + num_args: usize, + args_range: FileRange, + }, + FunAppTooManyArgs { + head_range: FileRange, + head_type: String, + expected_arity: usize, + actual_arity: usize, + extra_args_range: FileRange, }, PlicityArgumentMismatch { head_range: FileRange, @@ -179,17 +187,48 @@ impl Message { primary_label(param_range).with_message("unexpected parameter") ]) .with_notes(vec!["this parameter can be removed".to_owned()]), - Message::UnexpectedArgument { + Message::FunAppNotFun { head_range, head_type, - arg_range, + num_args, + args_range, } => Diagnostic::error() - .with_message("expression was applied to an unexpected argument") + .with_message(pluralize( + *num_args, + "tried to apply argument to non-function expression", + "tried to apply arguments to non-function expression", + )) .with_labels(vec![ - primary_label(arg_range).with_message("unexpected argument"), - secondary_label(head_range) - .with_message(format!("expression of type {head_type}")), + primary_label(head_range) + .with_message(format!("expression of type `{head_type}`")), + secondary_label(args_range).with_message(pluralize( + *num_args, + "argument", + "arguments", + )), ]), + Message::FunAppTooManyArgs { + head_range, + head_type, + expected_arity, + actual_arity, + extra_args_range, + } => Diagnostic::error() + .with_message("tried to apply too many arguments to function") + .with_labels(vec![ + primary_label(head_range) + .with_message(format!("expression of type `{head_type}`")), + secondary_label(extra_args_range).with_message(pluralize( + actual_arity - expected_arity, + "extra argument", + "extra arguments", + )), + ]) + .with_notes(vec![format!( + "help: function expects {expected_arity} {}, but recieved {actual_arity} {}", + pluralize(*expected_arity, "argument", "arguments"), + pluralize(*actual_arity, "argument", "arguments"), + )]), Message::PlicityArgumentMismatch { head_range, head_plicity, @@ -485,3 +524,11 @@ impl Message { } } } + +fn pluralize(amount: usize, single: T, plural: T) -> T { + if amount == 1 { + single + } else { + plural + } +} diff --git a/tests/fail/elaboration/fun-app/head-not-fun.fathom b/tests/fail/elaboration/fun-app/head-not-fun.fathom new file mode 100644 index 000000000..a707e7721 --- /dev/null +++ b/tests/fail/elaboration/fun-app/head-not-fun.fathom @@ -0,0 +1,5 @@ +//~ exit-code = 1 + +let _ : Type = Type true; +let _ : Type = Type true false; +{} diff --git a/tests/fail/elaboration/fun-app/head-not-fun.snap b/tests/fail/elaboration/fun-app/head-not-fun.snap new file mode 100644 index 000000000..138375787 --- /dev/null +++ b/tests/fail/elaboration/fun-app/head-not-fun.snap @@ -0,0 +1,19 @@ +stdout = '' +stderr = ''' +error: tried to apply argument to non-function expression + ┌─ tests/fail/elaboration/fun-app/head-not-fun.fathom:3:16 + │ +3 │ let _ : Type = Type true; + │ ^^^^ ---- argument + │ │ + │ expression of type `Type` + +error: tried to apply arguments to non-function expression + ┌─ tests/fail/elaboration/fun-app/head-not-fun.fathom:4:16 + │ +4 │ let _ : Type = Type true false; + │ ^^^^ ---------- arguments + │ │ + │ expression of type `Type` + +''' diff --git a/tests/fail/elaboration/fun-app/too-many-args.fathom b/tests/fail/elaboration/fun-app/too-many-args.fathom new file mode 100644 index 000000000..4761e9052 --- /dev/null +++ b/tests/fail/elaboration/fun-app/too-many-args.fathom @@ -0,0 +1,21 @@ +//~ exit-code = 1 + +let id = fun (x : Bool) => x; +let always = fun (x : Bool) (y : Bool) => y; + +let _ : Bool = id true false; +let _ : Bool = id true false false; + +let _ : Bool = always true true false; +let _ : Bool = always true true false false; + +let id_poly = fun (@A : Type) (a : A) => a; +let always_poly = fun (@A : Type) (@B : Type) (a : A) (b: B) => B; + +let _ : Bool = id_poly true false; +let _ : Bool = id_poly true false false; + +let _ : Bool = always_poly true true false; +let _ : Bool = always_poly true true false false; + +{} diff --git a/tests/fail/elaboration/fun-app/too-many-args.snap b/tests/fail/elaboration/fun-app/too-many-args.snap new file mode 100644 index 000000000..14d1c4e73 --- /dev/null +++ b/tests/fail/elaboration/fun-app/too-many-args.snap @@ -0,0 +1,83 @@ +stdout = '' +stderr = ''' +error: tried to apply too many arguments to function + ┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:6:16 + │ +6 │ let _ : Bool = id true false; + │ ^^ ----- extra argument + │ │ + │ expression of type `Bool -> Bool` + │ + = help: function expects 1 argument, but recieved 2 arguments + +error: tried to apply too many arguments to function + ┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:7:16 + │ +7 │ let _ : Bool = id true false false; + │ ^^ ----------- extra arguments + │ │ + │ expression of type `Bool -> Bool` + │ + = help: function expects 1 argument, but recieved 3 arguments + +error: tried to apply too many arguments to function + ┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:9:16 + │ +9 │ let _ : Bool = always true true false; + │ ^^^^^^ ----- extra argument + │ │ + │ expression of type `Bool -> Bool -> Bool` + │ + = help: function expects 2 arguments, but recieved 3 arguments + +error: tried to apply too many arguments to function + ┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:10:16 + │ +10 │ let _ : Bool = always true true false false; + │ ^^^^^^ ----------- extra arguments + │ │ + │ expression of type `Bool -> Bool -> Bool` + │ + = help: function expects 2 arguments, but recieved 4 arguments + +error: tried to apply too many arguments to function + ┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:15:16 + │ +15 │ let _ : Bool = id_poly true false; + │ ^^^^^^^ ----- extra argument + │ │ + │ expression of type `fun (@A : Type) -> A -> A` + │ + = help: function expects 1 argument, but recieved 2 arguments + +error: tried to apply too many arguments to function + ┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:16:16 + │ +16 │ let _ : Bool = id_poly true false false; + │ ^^^^^^^ ----------- extra arguments + │ │ + │ expression of type `fun (@A : Type) -> A -> A` + │ + = help: function expects 1 argument, but recieved 3 arguments + +error: tried to apply too many arguments to function + ┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:18:16 + │ +18 │ let _ : Bool = always_poly true true false; + │ ^^^^^^^^^^^ ----- extra argument + │ │ + │ expression of type `fun (@A : Type) (@B : Type) -> A -> B -> Type` + │ + = help: function expects 2 arguments, but recieved 3 arguments + +error: tried to apply too many arguments to function + ┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:19:16 + │ +19 │ let _ : Bool = always_poly true true false false; + │ ^^^^^^^^^^^ ----------- extra arguments + │ │ + │ expression of type `fun (@A : Type) (@B : Type) -> A -> B -> Type` + │ + = help: function expects 2 arguments, but recieved 4 arguments + +''' diff --git a/tests/fail/elaboration/unexpected-argument/unbound-head-1.fathom b/tests/fail/elaboration/fun-app/unbound-head-1.fathom similarity index 100% rename from tests/fail/elaboration/unexpected-argument/unbound-head-1.fathom rename to tests/fail/elaboration/fun-app/unbound-head-1.fathom diff --git a/tests/fail/elaboration/unexpected-argument/unbound-head-1.snap b/tests/fail/elaboration/fun-app/unbound-head-1.snap similarity index 55% rename from tests/fail/elaboration/unexpected-argument/unbound-head-1.snap rename to tests/fail/elaboration/fun-app/unbound-head-1.snap index 68ec9b0b0..5107f7c64 100644 --- a/tests/fail/elaboration/unexpected-argument/unbound-head-1.snap +++ b/tests/fail/elaboration/fun-app/unbound-head-1.snap @@ -1,7 +1,7 @@ stdout = '' stderr = ''' error: cannot find `f` in scope - ┌─ tests/fail/elaboration/unexpected-argument/unbound-head-1.fathom:3:1 + ┌─ tests/fail/elaboration/fun-app/unbound-head-1.fathom:3:1 │ 3 │ f x │ ^ unbound name diff --git a/tests/fail/elaboration/unexpected-argument/unbound-head-2.fathom b/tests/fail/elaboration/fun-app/unbound-head-2.fathom similarity index 100% rename from tests/fail/elaboration/unexpected-argument/unbound-head-2.fathom rename to tests/fail/elaboration/fun-app/unbound-head-2.fathom diff --git a/tests/fail/elaboration/unexpected-argument/unbound-head-2.snap b/tests/fail/elaboration/fun-app/unbound-head-2.snap similarity index 56% rename from tests/fail/elaboration/unexpected-argument/unbound-head-2.snap rename to tests/fail/elaboration/fun-app/unbound-head-2.snap index 85a0b4fff..41074ba6b 100644 --- a/tests/fail/elaboration/unexpected-argument/unbound-head-2.snap +++ b/tests/fail/elaboration/fun-app/unbound-head-2.snap @@ -1,7 +1,7 @@ stdout = '' stderr = ''' error: cannot find `f` in scope - ┌─ tests/fail/elaboration/unexpected-argument/unbound-head-2.fathom:3:1 + ┌─ tests/fail/elaboration/fun-app/unbound-head-2.fathom:3:1 │ 3 │ f x y │ ^ unbound name diff --git a/tests/fail/elaboration/implicit-args/unexpected-argument.snap b/tests/fail/elaboration/implicit-args/unexpected-argument.snap index ca98c3062..e62bfe2d1 100644 --- a/tests/fail/elaboration/implicit-args/unexpected-argument.snap +++ b/tests/fail/elaboration/implicit-args/unexpected-argument.snap @@ -1,11 +1,11 @@ stdout = '' stderr = ''' -error: expression was applied to an unexpected argument - ┌─ tests/fail/elaboration/implicit-args/unexpected-argument.fathom:3:7 +error: tried to apply argument to non-function expression + ┌─ tests/fail/elaboration/implicit-args/unexpected-argument.fathom:3:1 │ 3 │ true @Bool - │ ---- ^^^^ unexpected argument + │ ^^^^ ---- argument │ │ - │ expression of type Bool + │ expression of type `Bool` ''' diff --git a/tests/fail/elaboration/unexpected-argument/record-type.fathom b/tests/fail/elaboration/unexpected-argument/record-type.fathom deleted file mode 100644 index 6bd365dd3..000000000 --- a/tests/fail/elaboration/unexpected-argument/record-type.fathom +++ /dev/null @@ -1,3 +0,0 @@ -//~ exit-code = 1 - -{ x : Type } x y diff --git a/tests/fail/elaboration/unexpected-argument/record-type.snap b/tests/fail/elaboration/unexpected-argument/record-type.snap deleted file mode 100644 index 8604d1380..000000000 --- a/tests/fail/elaboration/unexpected-argument/record-type.snap +++ /dev/null @@ -1,11 +0,0 @@ -stdout = '' -stderr = ''' -error: expression was applied to an unexpected argument - ┌─ tests/fail/elaboration/unexpected-argument/record-type.fathom:3:14 - │ -3 │ { x : Type } x y - │ ------------ ^ unexpected argument - │ │ - │ expression of type Type - -'''