Skip to content

Commit 49665d9

Browse files
KmeakinKmeakin
committed
Improve diagnostic messages for errors in elaborating record projections
1 parent 3960a94 commit 49665d9

17 files changed

+157
-85
lines changed

‎fathom/src/core/semantics.rs

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,13 @@ impl<'arena> Value<'arena> {
7777
}
7878
}
7979

80+
pub fn is_unit_type(&self) -> bool {
81+
match self {
82+
Value::RecordType(labels, _) => labels.is_empty(),
83+
_ => false,
84+
}
85+
}
86+
8087
pub fn is_error(&self) -> bool {
8188
matches!(self, Value::Stuck(Head::Prim(Prim::ReportedError), _))
8289
}

‎fathom/src/surface/elaboration.rs

Lines changed: 33 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1597,14 +1597,24 @@ impl<'arena> Context<'arena> {
15971597
(term, r#type)
15981598
}
15991599
Term::Proj(range, head_expr, labels) => {
1600-
let head_range = head_expr.range();
1600+
let mut head_range = head_expr.range();
16011601
let (mut head_expr, mut head_type) = self.synth_and_insert_implicit_apps(head_expr);
16021602

16031603
'labels: for (label_range, proj_label) in *labels {
16041604
head_type = self.elim_env().force(&head_type);
1605-
match (&head_expr, head_type.as_ref()) {
1605+
match head_type.as_ref() {
1606+
r#type if r#type.is_unit_type() => {
1607+
self.push_message(Message::RecordProjUnit {
1608+
head_range: self.file_range(head_range),
1609+
head_type: self.pretty_value(&head_type),
1610+
label_range: self.file_range(*label_range),
1611+
label: *proj_label,
1612+
});
1613+
return self.synth_reported_error(*range);
1614+
}
1615+
16061616
// Ensure that the head of the projection is a record
1607-
(_, Value::RecordType(labels, types)) => {
1617+
Value::RecordType(labels, types) => {
16081618
let mut labels = labels.iter().copied();
16091619
let mut types = types.clone();
16101620

@@ -1618,9 +1628,9 @@ impl<'arena> Context<'arena> {
16181628
if *proj_label == label {
16191629
// The field was found. Update the head expression
16201630
// and continue elaborating the next projection.
1631+
head_range = ByteRange::merge(head_range, *label_range);
16211632
head_expr = core::Term::RecordProj(
1622-
self.file_range(ByteRange::merge(head_range, *label_range))
1623-
.into(),
1633+
self.file_range(head_range).into(),
16241634
self.scope.to_scope(head_expr),
16251635
*proj_label,
16261636
);
@@ -1636,28 +1646,32 @@ impl<'arena> Context<'arena> {
16361646
}
16371647
}
16381648
// Couldn't find the field in the record type.
1639-
// Fallthrough with an error.
1649+
self.push_message(Message::RecordProjNotFound {
1650+
head_range: self.file_range(head_range),
1651+
head_type: self.pretty_value(&head_type),
1652+
label_range: self.file_range(*label_range),
1653+
label: *proj_label,
1654+
suggested_label: suggest_name(*proj_label, labels),
1655+
});
1656+
return self.synth_reported_error(*range);
16401657
}
16411658
// There's been an error when elaborating the head of
16421659
// the projection, so avoid trying to elaborate any
16431660
// further to prevent cascading type errors.
1644-
(core::Term::Prim(_, Prim::ReportedError), _)
1645-
| (_, Value::Stuck(Head::Prim(Prim::ReportedError), _)) => {
1661+
_ if head_expr.is_error() || head_type.is_error() => {
16461662
return self.synth_reported_error(*range);
16471663
}
16481664
// The head expression was not a record type.
1649-
// Fallthrough with an error.
1650-
_ => {}
1665+
_ => {
1666+
self.push_message(Message::RecordProjNotRecord {
1667+
head_range: self.file_range(head_range),
1668+
head_type: self.pretty_value(&head_type),
1669+
label_range: self.file_range(*label_range),
1670+
label: *proj_label,
1671+
});
1672+
return self.synth_reported_error(*range);
1673+
}
16511674
}
1652-
1653-
self.push_message(Message::UnknownField {
1654-
head_range: self.file_range(head_range),
1655-
head_type: self.pretty_value(&head_type),
1656-
label_range: self.file_range(*label_range),
1657-
label: *proj_label,
1658-
suggested_label: suggest_name(*proj_label, labels.iter().map(|(_, l)| *l)),
1659-
});
1660-
return self.synth_reported_error(*range);
16611675
}
16621676

16631677
(head_expr, head_type)

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

Lines changed: 51 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,19 @@ pub enum Message {
4242
arg_range: FileRange,
4343
arg_plicity: Plicity,
4444
},
45-
UnknownField {
45+
RecordProjNotRecord {
46+
head_range: FileRange,
47+
head_type: String,
48+
label_range: FileRange,
49+
label: Symbol,
50+
},
51+
RecordProjUnit {
52+
head_range: FileRange,
53+
head_type: String,
54+
label_range: FileRange,
55+
label: Symbol,
56+
},
57+
RecordProjNotFound {
4658
head_range: FileRange,
4759
head_type: String,
4860
label_range: FileRange,
@@ -205,18 +217,51 @@ impl Message {
205217
secondary_label(head_range)
206218
.with_message(format!("{head_plicity} function of type {head_type}")),
207219
]),
208-
Message::UnknownField {
220+
Message::RecordProjUnit {
221+
head_range,
222+
head_type,
223+
label_range,
224+
label,
225+
} => Diagnostic::error()
226+
.with_message(format!(
227+
"tried to access field `{}` of empty record",
228+
label.resolve()
229+
))
230+
.with_labels(vec![
231+
primary_label(head_range)
232+
.with_message(format!("expression of type `{head_type}`")),
233+
secondary_label(label_range).with_message("field access"),
234+
]),
235+
Message::RecordProjNotRecord {
236+
head_range,
237+
head_type,
238+
label_range,
239+
label,
240+
} => Diagnostic::error()
241+
.with_message(format!(
242+
"tried to access field `{}` of non-record expression",
243+
label.resolve()
244+
))
245+
.with_labels(vec![
246+
primary_label(head_range)
247+
.with_message(format!("expression of type `{head_type}`")),
248+
secondary_label(label_range).with_message("field access"),
249+
]),
250+
Message::RecordProjNotFound {
209251
head_range,
210252
head_type,
211253
label_range,
212254
label,
213255
suggested_label,
214256
} => Diagnostic::error()
215-
.with_message(format!("cannot find `{}` in expression", label.resolve()))
257+
.with_message(format!(
258+
"tried to access unknown field `{}`",
259+
label.resolve()
260+
))
216261
.with_labels(vec![
217-
primary_label(label_range).with_message("unknown label"),
218-
secondary_label(head_range)
219-
.with_message(format!("expression of type {head_type}")),
262+
primary_label(head_range)
263+
.with_message(format!("expression of type `{head_type}`")),
264+
secondary_label(label_range).with_message("unknown field"),
220265
])
221266
.with_notes(suggested_label.map_or(Vec::new(), |label| {
222267
vec![format!("help: did you mean `{}`?", label.resolve())]

‎tests/fail/elaboration/record-proj/field-not-found.fathom

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

‎tests/fail/elaboration/record-proj/field-not-found.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 access unknown field `y`
4+
┌─ tests/fail/elaboration/record-proj/field-not-found.fathom:3:16
5+
│
6+
3 │ let _ : Bool = {x=false}.y;
7+
│ ^^^^^^^^^ - unknown field
8+
│ │
9+
│ expression of type `{ x : Bool }`
10+
11+
error: tried to access field `y` of non-record expression
12+
┌─ tests/fail/elaboration/record-proj/field-not-found.fathom:4:16
13+
│
14+
4 │ let _ : Bool = {x=false}.x.y;
15+
│ ^^^^^^^^^^^ - field access
16+
│ │
17+
│ expression of type `Bool`
18+
19+
'''

‎tests/fail/elaboration/record-proj/head-is-unit.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 _ : Bool = {}.foo;
4+
5+
{}

‎tests/fail/elaboration/record-proj/head-is-unit.snap

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
stdout = ''
2+
stderr = '''
3+
error: tried to access field `foo` of empty record
4+
┌─ tests/fail/elaboration/record-proj/head-is-unit.fathom:3:16
5+
│
6+
3 │ let _ : Bool = {}.foo;
7+
│ ^^ --- field access
8+
│ │
9+
│ expression of type `()`
10+
11+
'''

‎tests/fail/elaboration/record-proj/head-not-record.fathom

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

‎tests/fail/elaboration/record-proj/head-not-record.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 access field `foo` of non-record expression
4+
┌─ tests/fail/elaboration/record-proj/head-not-record.fathom:3:16
5+
│
6+
3 │ let _ : Bool = Bool.foo;
7+
│ ^^^^ --- field access
8+
│ │
9+
│ expression of type `Type`
10+
11+
error: tried to access field `foo` of non-record expression
12+
┌─ tests/fail/elaboration/record-proj/head-not-record.fathom:4:16
13+
│
14+
4 │ let _ : Bool = {x=false}.x.foo;
15+
│ ^^^^^^^^^^^ --- field access
16+
│ │
17+
│ expression of type `Bool`
18+
19+
'''

‎tests/fail/elaboration/unknown-field/record-literal.fathom

Lines changed: 0 additions & 3 deletions
This file was deleted.

0 commit comments

Comments
 (0)