Skip to content

Commit 958dc56

Browse files
KmeakinKmeakin
committed
Improve diagnostic messages for errors in elaborating fun apps
1 parent 3960a94 commit 958dc56

File tree

13 files changed

+227
-36
lines changed

13 files changed

+227
-36
lines changed

‎fathom/src/surface/elaboration.rs

Lines changed: 38 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1474,9 +1474,13 @@ impl<'arena> Context<'arena> {
14741474
}
14751475
Term::App(range, head_expr, args) => {
14761476
let mut head_range = head_expr.range();
1477-
let (mut head_expr, mut head_type) = self.synth(head_expr);
1477+
let (mut head_expr, head_type) = self.synth(head_expr);
14781478

1479-
for arg in *args {
1479+
let original_head_range = head_range;
1480+
let original_head_type = self.elim_env().force(&head_type);
1481+
let mut head_type = original_head_type.clone();
1482+
1483+
for (arity, arg) in args.iter().enumerate() {
14801484
head_type = self.elim_env().force(&head_type);
14811485

14821486
match arg.plicity {
@@ -1509,13 +1513,39 @@ impl<'arena> Context<'arena> {
15091513
_ if head_expr.is_error() || head_type.is_error() => {
15101514
return self.synth_reported_error(*range);
15111515
}
1516+
// NOTE: We could try to infer that this is a function type,
1517+
// but this takes more work to prevent cascading type errors
1518+
_ if arity == 0 => {
1519+
self.push_message(Message::FunAppNotFun {
1520+
head_range: self.file_range(original_head_range),
1521+
head_type: self.pretty_value(&original_head_type),
1522+
num_args: args.len(),
1523+
args_range: {
1524+
let first = args.first().unwrap();
1525+
let last = args.last().unwrap();
1526+
self.file_range(ByteRange::merge(
1527+
first.term.range(),
1528+
last.term.range(),
1529+
))
1530+
},
1531+
});
1532+
return self.synth_reported_error(*range);
1533+
}
15121534
_ => {
1513-
// NOTE: We could try to infer that this is a function type,
1514-
// but this takes more work to prevent cascading type errors
1515-
self.push_message(Message::UnexpectedArgument {
1516-
head_range: self.file_range(head_range),
1517-
head_type: self.pretty_value(&head_type),
1518-
arg_range: self.file_range(arg.term.range()),
1535+
self.push_message(Message::FunAppTooManyArgs {
1536+
head_range: self.file_range(original_head_range),
1537+
head_type: self.pretty_value(&original_head_type),
1538+
expected_arity: arity,
1539+
actual_arity: args.len(),
1540+
extra_args_range: {
1541+
let extra_args = &args[arity..];
1542+
let first = extra_args.first().unwrap();
1543+
let last = extra_args.last().unwrap();
1544+
self.file_range(ByteRange::merge(
1545+
first.term.range(),
1546+
last.term.range(),
1547+
))
1548+
},
15191549
});
15201550
return self.synth_reported_error(*range);
15211551
}

‎fathom/src/surface/elaboration/reporting.rs

Lines changed: 55 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -30,10 +30,18 @@ pub enum Message {
3030
UnexpectedParameter {
3131
param_range: FileRange,
3232
},
33-
UnexpectedArgument {
33+
FunAppNotFun {
3434
head_range: FileRange,
3535
head_type: String,
36-
arg_range: FileRange,
36+
num_args: usize,
37+
args_range: FileRange,
38+
},
39+
FunAppTooManyArgs {
40+
head_range: FileRange,
41+
head_type: String,
42+
expected_arity: usize,
43+
actual_arity: usize,
44+
extra_args_range: FileRange,
3745
},
3846
PlicityArgumentMismatch {
3947
head_range: FileRange,
@@ -179,17 +187,48 @@ impl Message {
179187
primary_label(param_range).with_message("unexpected parameter")
180188
])
181189
.with_notes(vec!["this parameter can be removed".to_owned()]),
182-
Message::UnexpectedArgument {
190+
Message::FunAppNotFun {
183191
head_range,
184192
head_type,
185-
arg_range,
193+
num_args,
194+
args_range,
186195
} => Diagnostic::error()
187-
.with_message("expression was applied to an unexpected argument")
196+
.with_message(pluralize(
197+
*num_args,
198+
"tried to apply argument to non-function expression",
199+
"tried to apply arguments to non-function expression",
200+
))
188201
.with_labels(vec![
189-
primary_label(arg_range).with_message("unexpected argument"),
190-
secondary_label(head_range)
191-
.with_message(format!("expression of type {head_type}")),
202+
primary_label(head_range)
203+
.with_message(format!("expression of type `{head_type}`")),
204+
secondary_label(args_range).with_message(pluralize(
205+
*num_args,
206+
"argument",
207+
"arguments",
208+
)),
192209
]),
210+
Message::FunAppTooManyArgs {
211+
head_range,
212+
head_type,
213+
expected_arity,
214+
actual_arity,
215+
extra_args_range,
216+
} => Diagnostic::error()
217+
.with_message("tried to apply too many arguments to function")
218+
.with_labels(vec![
219+
primary_label(head_range)
220+
.with_message(format!("expression of type `{head_type}`")),
221+
secondary_label(extra_args_range).with_message(pluralize(
222+
actual_arity - expected_arity,
223+
"extra argument",
224+
"extra arguments",
225+
)),
226+
])
227+
.with_notes(vec![format!(
228+
"help: function expects {expected_arity} {}, but recieved {actual_arity} {}",
229+
pluralize(*expected_arity, "argument", "arguments"),
230+
pluralize(*actual_arity, "argument", "arguments"),
231+
)]),
193232
Message::PlicityArgumentMismatch {
194233
head_range,
195234
head_plicity,
@@ -485,3 +524,11 @@ impl Message {
485524
}
486525
}
487526
}
527+
528+
fn pluralize<T>(amount: usize, single: T, plural: T) -> T {
529+
if amount == 1 {
530+
single
531+
} else {
532+
plural
533+
}
534+
}

‎tests/fail/elaboration/fun-app/head-not-fun.fathom

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
//~ exit-code = 1
2+
3+
let _ : Type = Type true;
4+
let _ : Type = Type true false;
5+
{}

‎tests/fail/elaboration/fun-app/head-not-fun.snap

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
stdout = ''
2+
stderr = '''
3+
error: tried to apply argument to non-function expression
4+
┌─ tests/fail/elaboration/fun-app/head-not-fun.fathom:3:16
5+
│
6+
3 │ let _ : Type = Type true;
7+
│ ^^^^ ---- argument
8+
│ │
9+
│ expression of type `Type`
10+
11+
error: tried to apply arguments to non-function expression
12+
┌─ tests/fail/elaboration/fun-app/head-not-fun.fathom:4:16
13+
│
14+
4 │ let _ : Type = Type true false;
15+
│ ^^^^ ---------- arguments
16+
│ │
17+
│ expression of type `Type`
18+
19+
'''

‎tests/fail/elaboration/fun-app/too-many-args.fathom

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
//~ exit-code = 1
2+
3+
let id = fun (x : Bool) => x;
4+
let always = fun (x : Bool) (y : Bool) => y;
5+
6+
let _ : Bool = id true false;
7+
let _ : Bool = id true false false;
8+
9+
let _ : Bool = always true true false;
10+
let _ : Bool = always true true false false;
11+
12+
let id_poly = fun (@A : Type) (a : A) => a;
13+
let always_poly = fun (@A : Type) (@B : Type) (a : A) (b: B) => B;
14+
15+
let _ : Bool = id_poly true false;
16+
let _ : Bool = id_poly true false false;
17+
18+
let _ : Bool = always_poly true true false;
19+
let _ : Bool = always_poly true true false false;
20+
21+
{}

‎tests/fail/elaboration/fun-app/too-many-args.snap

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
stdout = ''
2+
stderr = '''
3+
error: tried to apply too many arguments to function
4+
┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:6:16
5+
│
6+
6 │ let _ : Bool = id true false;
7+
│ ^^ ----- extra argument
8+
│ │
9+
│ expression of type `Bool -> Bool`
10+
│
11+
= help: function expects 1 argument, but recieved 2 arguments
12+
13+
error: tried to apply too many arguments to function
14+
┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:7:16
15+
│
16+
7 │ let _ : Bool = id true false false;
17+
│ ^^ ----------- extra arguments
18+
│ │
19+
│ expression of type `Bool -> Bool`
20+
│
21+
= help: function expects 1 argument, but recieved 3 arguments
22+
23+
error: tried to apply too many arguments to function
24+
┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:9:16
25+
│
26+
9 │ let _ : Bool = always true true false;
27+
│ ^^^^^^ ----- extra argument
28+
│ │
29+
│ expression of type `Bool -> Bool -> Bool`
30+
│
31+
= help: function expects 2 arguments, but recieved 3 arguments
32+
33+
error: tried to apply too many arguments to function
34+
┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:10:16
35+
│
36+
10 │ let _ : Bool = always true true false false;
37+
│ ^^^^^^ ----------- extra arguments
38+
│ │
39+
│ expression of type `Bool -> Bool -> Bool`
40+
│
41+
= help: function expects 2 arguments, but recieved 4 arguments
42+
43+
error: tried to apply too many arguments to function
44+
┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:15:16
45+
│
46+
15 │ let _ : Bool = id_poly true false;
47+
│ ^^^^^^^ ----- extra argument
48+
│ │
49+
│ expression of type `fun (@A : Type) -> A -> A`
50+
│
51+
= help: function expects 1 argument, but recieved 2 arguments
52+
53+
error: tried to apply too many arguments to function
54+
┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:16:16
55+
│
56+
16 │ let _ : Bool = id_poly true false false;
57+
│ ^^^^^^^ ----------- extra arguments
58+
│ │
59+
│ expression of type `fun (@A : Type) -> A -> A`
60+
│
61+
= help: function expects 1 argument, but recieved 3 arguments
62+
63+
error: tried to apply too many arguments to function
64+
┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:18:16
65+
│
66+
18 │ let _ : Bool = always_poly true true false;
67+
│ ^^^^^^^^^^^ ----- extra argument
68+
│ │
69+
│ expression of type `fun (@A : Type) (@B : Type) -> A -> B -> Type`
70+
│
71+
= help: function expects 2 arguments, but recieved 3 arguments
72+
73+
error: tried to apply too many arguments to function
74+
┌─ tests/fail/elaboration/fun-app/too-many-args.fathom:19:16
75+
│
76+
19 │ let _ : Bool = always_poly true true false false;
77+
│ ^^^^^^^^^^^ ----------- extra arguments
78+
│ │
79+
│ expression of type `fun (@A : Type) (@B : Type) -> A -> B -> Type`
80+
│
81+
= help: function expects 2 arguments, but recieved 4 arguments
82+
83+
'''

‎tests/fail/elaboration/unexpected-argument/unbound-head-1.fathom renamed to ‎tests/fail/elaboration/fun-app/unbound-head-1.fathom

File renamed without changes.

‎tests/fail/elaboration/unexpected-argument/unbound-head-1.snap renamed to ‎tests/fail/elaboration/fun-app/unbound-head-1.snap

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
stdout = ''
22
stderr = '''
33
error: cannot find `f` in scope
4-
┌─ tests/fail/elaboration/unexpected-argument/unbound-head-1.fathom:3:1
4+
┌─ tests/fail/elaboration/fun-app/unbound-head-1.fathom:3:1
55
│
66
3 │ f x
77
│ ^ unbound name

‎tests/fail/elaboration/unexpected-argument/unbound-head-2.fathom renamed to ‎tests/fail/elaboration/fun-app/unbound-head-2.fathom

File renamed without changes.

‎tests/fail/elaboration/unexpected-argument/unbound-head-2.snap renamed to ‎tests/fail/elaboration/fun-app/unbound-head-2.snap

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
stdout = ''
22
stderr = '''
33
error: cannot find `f` in scope
4-
┌─ tests/fail/elaboration/unexpected-argument/unbound-head-2.fathom:3:1
4+
┌─ tests/fail/elaboration/fun-app/unbound-head-2.fathom:3:1
55
│
66
3 │ f x y
77
│ ^ unbound name

0 commit comments

Comments
 (0)