Improve diagnostic messages for errors in elaborating record projections

fathom/src/core/semantics.rs

@@ -77,6 +77,13 @@ impl<'arena> Value<'arena> {
         }
     }
 
+    pub fn is_unit_type(&self) -> bool {
+        match self {
+            Value::RecordType(labels, _) => labels.is_empty(),
+            _ => false,
+        }
+    }
+
     pub fn is_error(&self) -> bool {
         matches!(self, Value::Stuck(Head::Prim(Prim::ReportedError), _))
     }

fathom/src/surface/elaboration.rs

@@ -1597,14 +1597,24 @@ impl<'arena> Context<'arena> {
                 (term, r#type)
             }
             Term::Proj(range, head_expr, labels) => {
-                let head_range = head_expr.range();
+                let mut head_range = head_expr.range();
                 let (mut head_expr, mut head_type) = self.synth_and_insert_implicit_apps(head_expr);
 
                 'labels: for (label_range, proj_label) in *labels {
                     head_type = self.elim_env().force(&head_type);
-                    match (&head_expr, head_type.as_ref()) {
+                    match head_type.as_ref() {
+                        r#type if r#type.is_unit_type() => {
+                            self.push_message(Message::RecordProjUnit {
+                                head_range: self.file_range(head_range),
+                                head_type: self.pretty_value(&head_type),
+                                label_range: self.file_range(*label_range),
+                                label: *proj_label,
+                            });
+                            return self.synth_reported_error(*range);
+                        }
+
                         // Ensure that the head of the projection is a record
-                        (_, Value::RecordType(labels, types)) => {
+                        Value::RecordType(labels, types) => {
                             let mut labels = labels.iter().copied();
                             let mut types = types.clone();
 
@@ -1618,9 +1628,9 @@ impl<'arena> Context<'arena> {
                                 if *proj_label == label {
                                     // The field was found. Update the head expression
                                     // and continue elaborating the next projection.
+                                    head_range = ByteRange::merge(head_range, *label_range);
                                     head_expr = core::Term::RecordProj(
-                                        self.file_range(ByteRange::merge(head_range, *label_range))
-                                            .into(),
+                                        self.file_range(head_range).into(),
                                         self.scope.to_scope(head_expr),
                                         *proj_label,
                                     );
@@ -1636,28 +1646,32 @@ impl<'arena> Context<'arena> {
                                 }
                             }
                             // Couldn't find the field in the record type.
-                            // Fallthrough with an error.
+                            self.push_message(Message::RecordProjNotFound {
+                                head_range: self.file_range(head_range),
+                                head_type: self.pretty_value(&head_type),
+                                label_range: self.file_range(*label_range),
+                                label: *proj_label,
+                                suggested_label: suggest_name(*proj_label, labels),
+                            });
+                            return self.synth_reported_error(*range);
                         }
                         // There's been an error when elaborating the head of
                         // the projection, so avoid trying to elaborate any
                         // further to prevent cascading type errors.
-                        (core::Term::Prim(_, Prim::ReportedError), _)
-                        | (_, Value::Stuck(Head::Prim(Prim::ReportedError), _)) => {
+                        _ if head_expr.is_error() || head_type.is_error() => {
                             return self.synth_reported_error(*range);
                         }
                         // The head expression was not a record type.
-                        // Fallthrough with an error.
-                        _ => {}
+                        _ => {
+                            self.push_message(Message::RecordProjNotRecord {
+                                head_range: self.file_range(head_range),
+                                head_type: self.pretty_value(&head_type),
+                                label_range: self.file_range(*label_range),
+                                label: *proj_label,
+                            });
+                            return self.synth_reported_error(*range);
+                        }
                     }
-
-                    self.push_message(Message::UnknownField {
-                        head_range: self.file_range(head_range),
-                        head_type: self.pretty_value(&head_type),
-                        label_range: self.file_range(*label_range),
-                        label: *proj_label,
-                        suggested_label: suggest_name(*proj_label, labels.iter().map(|(_, l)| *l)),
-                    });
-                    return self.synth_reported_error(*range);
                 }
 
                 (head_expr, head_type)

fathom/src/surface/elaboration/reporting.rs

@@ -42,7 +42,19 @@ pub enum Message {
         arg_range: FileRange,
         arg_plicity: Plicity,
     },
-    UnknownField {
+    RecordProjNotRecord {
+        head_range: FileRange,
+        head_type: String,
+        label_range: FileRange,
+        label: Symbol,
+    },
+    RecordProjUnit {
+        head_range: FileRange,
+        head_type: String,
+        label_range: FileRange,
+        label: Symbol,
+    },
+    RecordProjNotFound {
         head_range: FileRange,
         head_type: String,
         label_range: FileRange,
@@ -205,18 +217,48 @@ impl Message {
                     secondary_label(head_range)
                         .with_message(format!("{head_plicity} function of type {head_type}")),
                 ]),
-            Message::UnknownField {
+            Message::RecordProjNotRecord {
+                head_range,
+                head_type,
+                label_range,
+                label,
+            } => Diagnostic::error()
+                .with_message(format!(
+                    "tried to access field `{}` of non-record expression",
+                    label.resolve()
+                ))
+                .with_labels(vec![
+                    primary_label(head_range)
+                        .with_message(format!("expression of type `{head_type}`")),
+                    secondary_label(label_range).with_message("field access"),
+                ]),
+            Message::RecordProjUnit {
+                head_range,
+                head_type,
+                label_range,
+                label,
+            } => Diagnostic::error()
+                .with_message(format!(
+                    "tried to access field `{}` of empty record",
+                    label.resolve()
+                ))
+                .with_labels(vec![
+                    primary_label(head_range)
+                        .with_message(format!("expression of type `{head_type}`")),
+                    secondary_label(label_range).with_message("field access"),
+                ]),
+            Message::RecordProjNotFound {
                 head_range,
                 head_type,
                 label_range,
                 label,
                 suggested_label,
             } => Diagnostic::error()
-                .with_message(format!("cannot find `{}` in expression", label.resolve()))
+                .with_message(format!("no field named `{}` in record", label.resolve()))
                 .with_labels(vec![
-                    primary_label(label_range).with_message("unknown label"),
-                    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(label_range).with_message("unknown field"),
                 ])
                 .with_notes(suggested_label.map_or(Vec::new(), |label| {
                     vec![format!("help: did you mean `{}`?", label.resolve())]

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

@@ -0,0 +1,6 @@
+//~ exit-code = 1
+
+let _ : Bool = {x=false}.y;
+let _ : Bool = {x=false}.x.y;
+
+{}

tests/fail/elaboration/record-proj/field-not-found.snap

@@ -0,0 +1,19 @@
+stdout = ''
+stderr = '''
+error: no field named `y` in record
+  ┌─ tests/fail/elaboration/record-proj/field-not-found.fathom:3:16
+  │
+3 │ let _ : Bool = {x=false}.y;
+  │                ^^^^^^^^^ - unknown field
+  │                │          
+  │                expression of type `{ x : Bool }`
+
+error: tried to access field `y` of non-record expression
+  ┌─ tests/fail/elaboration/record-proj/field-not-found.fathom:4:16
+  │
+4 │ let _ : Bool = {x=false}.x.y;
+  │                ^^^^^^^^^^^ - field access
+  │                │            
+  │                expression of type `Bool`
+
+'''

tests/fail/elaboration/record-proj/head-is-unit.fathom

@@ -0,0 +1,5 @@
+//~ exit-code = 1
+
+let _ : Bool = {}.foo;
+
+{}

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

@@ -0,0 +1,11 @@
+stdout = ''
+stderr = '''
+error: tried to access field `foo` of empty record
+  ┌─ tests/fail/elaboration/record-proj/head-is-unit.fathom:3:16
+  │
+3 │ let _ : Bool = {}.foo;
+  │                ^^ --- field access
+  │                │   
+  │                expression of type `()`
+
+'''

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

@@ -0,0 +1,6 @@
+//~ exit-code = 1
+
+let _ : Bool = Bool.foo;
+let _ : Bool = {x=false}.x.foo;
+
+{}

tests/fail/elaboration/record-proj/head-not-record.snap

@@ -0,0 +1,19 @@
+stdout = ''
+stderr = '''
+error: tried to access field `foo` of non-record expression
+  ┌─ tests/fail/elaboration/record-proj/head-not-record.fathom:3:16
+  │
+3 │ let _ : Bool = Bool.foo;
+  │                ^^^^ --- field access
+  │                │     
+  │                expression of type `Type`
+
+error: tried to access field `foo` of non-record expression
+  ┌─ tests/fail/elaboration/record-proj/head-not-record.fathom:4:16
+  │
+4 │ let _ : Bool = {x=false}.x.foo;
+  │                ^^^^^^^^^^^ --- field access
+  │                │            
+  │                expression of type `Bool`
+
+'''