From 8f140ac64482354e709b301a71d92f342bd71111 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 19 May 2022 14:59:21 +0100 Subject: [PATCH] Improve error message on duplicate non-mergeable fields --- dhall/src/operations/typecheck.rs | 21 ++++++++----------- dhall/src/syntax/ast/span.rs | 2 +- dhall/src/syntax/text/parser.rs | 10 ++++++--- .../unit/RecordLitDuplicateFieldsAbstract.txt | 13 +++++++++++- ...cordLitDuplicateFieldsCollidingRecords.txt | 8 ++++++- .../RecordLitDuplicateFieldsNotRecords.txt | 8 ++++++- 6 files changed, 43 insertions(+), 19 deletions(-) diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs index e62a8ccb..ba3d746d 100644 --- a/dhall/src/operations/typecheck.rs +++ b/dhall/src/operations/typecheck.rs @@ -17,23 +17,20 @@ fn check_rectymerge( x: Nir<'_>, y: Nir<'_>, ) -> Result<(), TypeError> { + let not_record_err = || match span { + Span::DuplicateRecordFieldsSugar(_, r) => { + mk_span_err((**r).clone(), "DuplicateFieldName") + } + _ => mk_span_err(span.clone(), "RecordTypeMergeRequiresRecordType"), + }; + let kts_x = match x.kind() { NirKind::RecordType(kts) => kts, - _ => { - return mk_span_err( - span.clone(), - "RecordTypeMergeRequiresRecordType", - ) - } + _ => return not_record_err(), }; let kts_y = match y.kind() { NirKind::RecordType(kts) => kts, - _ => { - return mk_span_err( - span.clone(), - "RecordTypeMergeRequiresRecordType", - ) - } + _ => return not_record_err(), }; for (k, tx) in kts_x { if let Some(ty) = kts_y.get(k) { diff --git a/dhall/src/syntax/ast/span.rs b/dhall/src/syntax/ast/span.rs index b0c7b5ab..948c2219 100644 --- a/dhall/src/syntax/ast/span.rs +++ b/dhall/src/syntax/ast/span.rs @@ -19,7 +19,7 @@ pub enum Span { /// A location in the source text Parsed(ParsedSpan), /// Desugarings - DuplicateRecordFieldsSugar, + DuplicateRecordFieldsSugar(Box, Box), DottedFieldSugar, RecordPunSugar, /// For expressions obtained from decoding binary diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs index d17ac612..0b267cdd 100644 --- a/dhall/src/syntax/text/parser.rs +++ b/dhall/src/syntax/text/parser.rs @@ -97,9 +97,13 @@ fn insert_recordlit_entry(map: &mut BTreeMap, l: Label, e: Expr) { Entry::Occupied(mut entry) => { let dummy = Expr::new(Num(Bool(false)), Span::Artificial); let other = entry.insert(dummy); + let span = Span::DuplicateRecordFieldsSugar( + Box::new(other.span()), + Box::new(e.span()), + ); entry.insert(Expr::new( Op(BinOp(RecursiveRecordMerge, other, e)), - Span::DuplicateRecordFieldsSugar, + span, )); } } @@ -133,11 +137,11 @@ lazy_static::lazy_static! { }; } -// Generate pest parser manually becaue otherwise we'd need to modify something outside of OUT_DIR +// Generate pest parser manually because otherwise we'd need to modify something outside of OUT_DIR // and that's forbidden by docs.rs. // This is equivalent to: // ``` -// #[derive(Parser) +// #[derive(Parser)] // #[grammar = "..."] // struct DhallParser; // ``` diff --git a/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsAbstract.txt b/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsAbstract.txt index f74e8390..55163aad 100644 --- a/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsAbstract.txt +++ b/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsAbstract.txt @@ -1 +1,12 @@ -Type error: error: RecordTypeMergeRequiresRecordType +Type error: error: DuplicateFieldName + --> :6:47 + | + 1 | {- This test illustrates that duplicate fields need not be literals in order + 2 | to be properly normalized. One or both of the duplicate fields can be + 3 | abstract because field duplication delegates its behavior to the `∧` + 4 | operator +... +12 | -} +13 | λ(r : { y : Natural }) → { x = { y = 1 }, x = r } + | ^ DuplicateFieldName + | diff --git a/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsCollidingRecords.txt b/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsCollidingRecords.txt index f74e8390..c517a01c 100644 --- a/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsCollidingRecords.txt +++ b/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsCollidingRecords.txt @@ -1 +1,7 @@ -Type error: error: RecordTypeMergeRequiresRecordType +Type error: error: DuplicateFieldName + --> :1:22 + | +... +8 | { x = { y = 0 }, x = { y = 0 } } + | ^^^^^^^^^ DuplicateFieldName + | diff --git a/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsNotRecords.txt b/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsNotRecords.txt index f74e8390..95867907 100644 --- a/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsNotRecords.txt +++ b/dhall/tests/type-inference/failure/unit/RecordLitDuplicateFieldsNotRecords.txt @@ -1 +1,7 @@ -Type error: error: RecordTypeMergeRequiresRecordType +Type error: error: DuplicateFieldName + --> :1:14 + | +... +7 | { x = 0, x = 0 } + | ^ DuplicateFieldName + |