Improve diagnostic messages for errors in elaborating fun apps

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);
                         }

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<T>(amount: usize, single: T, plural: T) -> T {
+    if amount == 1 {
+        single
+    } else {
+        plural
+    }
+}

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;
+{}

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`
+
+'''

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;
+
+{}

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
+
+'''

tests/fail/elaboration/unexpected-argument/unbound-head-1.snap → 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

tests/fail/elaboration/unexpected-argument/unbound-head-2.snap → 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

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`
 
 '''