From 8c64ae33149db4edaaa89d2d187baf10a2b9f8bf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 13:29:27 +0000 Subject: Make most type errors stringy --- dhall/src/error/mod.rs | 95 ++++++------- dhall/src/semantics/phase/typecheck.rs | 151 ++++++++------------- dhall/tests/type-errors/hurkensParadox.txt | 9 +- .../unit/AnnotationRecordWrongFieldName.txt | 2 +- .../unit/AnnotationRecordWrongFieldType.txt | 2 +- dhall/tests/type-errors/unit/AssertDoubleZeros.txt | 2 +- .../type-errors/unit/AssertTriviallyFalse.txt | 2 +- .../type-errors/unit/EquivalenceNotSameType.txt | 2 +- .../tests/type-errors/unit/EquivalenceNotTerms.txt | 2 +- .../unit/FunctionApplicationArgumentNotMatch.txt | 14 +- .../unit/FunctionApplicationIsNotFunction.txt | 7 +- .../tests/type-errors/unit/IfBranchesNotMatch.txt | 2 +- dhall/tests/type-errors/unit/IfBranchesNotType.txt | 2 +- dhall/tests/type-errors/unit/IfNotBool.txt | 2 +- .../type-errors/unit/LetWithWrongAnnotation.txt | 2 +- .../type-errors/unit/ListLiteralEmptyNotType.txt | 14 +- .../tests/type-errors/unit/ListLiteralNotType.txt | 2 +- .../type-errors/unit/ListLiteralTypesNotMatch.txt | 2 +- .../unit/MergeAlternativeHasNoHandler.txt | 2 +- .../type-errors/unit/MergeAnnotationNotType.txt | 2 +- .../unit/MergeEmptyWithoutAnnotation.txt | 2 +- .../type-errors/unit/MergeHandlerNotFunction.txt | 2 +- .../type-errors/unit/MergeHandlerNotInUnion.txt | 2 +- .../unit/MergeHandlerNotMatchAlternativeType.txt | 14 +- dhall/tests/type-errors/unit/MergeLhsNotRecord.txt | 2 +- .../type-errors/unit/MergeMissingHandler1.txt | 2 +- .../type-errors/unit/MergeMissingHandler2.txt | 2 +- dhall/tests/type-errors/unit/MergeRhsNotUnion.txt | 2 +- .../tests/type-errors/unit/MergeUnusedHandler.txt | 2 +- .../type-errors/unit/NaturalSubtractNotNatural.txt | 14 +- .../tests/type-errors/unit/OperatorAndNotBool.txt | 2 +- .../type-errors/unit/OperatorEqualNotBool.txt | 2 +- .../unit/OperatorListConcatenateLhsNotList.txt | 2 +- .../unit/OperatorListConcatenateListsNotMatch.txt | 2 +- .../OperatorListConcatenateNotListsButMatch.txt | 2 +- .../unit/OperatorListConcatenateRhsNotList.txt | 2 +- .../type-errors/unit/OperatorNotEqualNotBool.txt | 2 +- dhall/tests/type-errors/unit/OperatorOrNotBool.txt | 2 +- .../type-errors/unit/OperatorPlusNotNatural.txt | 2 +- .../unit/OperatorTextConcatenateLhsNotText.txt | 2 +- .../unit/OperatorTextConcatenateRhsNotText.txt | 2 +- .../type-errors/unit/OperatorTimesNotNatural.txt | 2 +- .../unit/OptionalDeprecatedSyntaxAbsent.txt | 2 +- .../unit/OptionalDeprecatedSyntaxPresent.txt | 2 +- .../type-errors/unit/RecordSelectionEmpty.txt | 2 +- .../type-errors/unit/RecordSelectionNotPresent.txt | 2 +- .../type-errors/unit/RecordSelectionNotRecord.txt | 2 +- .../unit/RecordSelectionTypeNotUnionType.txt | 2 +- .../unit/RecursiveRecordMergeLhsNotRecord.txt | 2 +- .../unit/RecursiveRecordMergeOverlapping.txt | 2 +- .../unit/RecursiveRecordMergeRhsNotRecord.txt | 2 +- .../RecursiveRecordTypeMergeLhsNotRecordType.txt | 2 +- .../unit/RecursiveRecordTypeMergeOverlapping.txt | 2 +- .../RecursiveRecordTypeMergeRhsNotRecordType.txt | 2 +- .../unit/RightBiasedRecordMergeLhsNotRecord.txt | 2 +- .../unit/RightBiasedRecordMergeRhsNotRecord.txt | 2 +- dhall/tests/type-errors/unit/SomeNotType.txt | 2 +- .../unit/TextLiteralInterpolateNotText.txt | 2 +- .../tests/type-errors/unit/TypeAnnotationWrong.txt | 2 +- .../unit/UnionConstructorFieldNotPresent.txt | 2 +- 60 files changed, 159 insertions(+), 263 deletions(-) diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 850a792..5330c59 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -3,7 +3,7 @@ use std::io::Error as IOError; use crate::semantics::core::value::Value; use crate::semantics::phase::resolve::ImportStack; use crate::semantics::phase::NormalizedExpr; -use crate::syntax::{BinOp, Import, Label, ParseError, Span}; +use crate::syntax::{Import, Label, ParseError, Span}; pub type Result = std::result::Result; @@ -48,41 +48,41 @@ pub(crate) enum TypeMessage { UnboundVariable(Span), InvalidInputType(Value), InvalidOutputType(Value), - NotAFunction(Value), - TypeMismatch(Value, Value, Value), - AnnotMismatch(Value, Value), - InvalidListElement(usize, Value, Value), - InvalidListType(Value), - InvalidOptionalType(Value), - InvalidPredicate(Value), - IfBranchMismatch(Value, Value), - IfBranchMustBeTerm(bool, Value), + // NotAFunction(Value), + // TypeMismatch(Value, Value, Value), + // AnnotMismatch(Value, Value), + // InvalidListElement(usize, Value, Value), + // InvalidListType(Value), + // InvalidOptionalType(Value), + // InvalidPredicate(Value), + // IfBranchMismatch(Value, Value), + // IfBranchMustBeTerm(bool, Value), InvalidFieldType(Label, Value), - NotARecord(Label, Value), - MustCombineRecord(Value), - MissingRecordField(Label, Value), - MissingUnionField(Label, Value), - BinOpTypeMismatch(BinOp, Value), - InvalidTextInterpolation(Value), - Merge1ArgMustBeRecord(Value), - Merge2ArgMustBeUnionOrOptional(Value), - MergeEmptyNeedsAnnotation, - MergeHandlerMissingVariant(Label), - MergeVariantMissingHandler(Label), - MergeAnnotMismatch, - MergeHandlerTypeMismatch, - MergeHandlerReturnTypeMustNotBeDependent, - ProjectionMustBeRecord, - ProjectionMissingEntry, - ProjectionDuplicateField, + // NotARecord(Label, Value), + // MustCombineRecord(Value), + // MissingRecordField(Label, Value), + // MissingUnionField(Label, Value), + // BinOpTypeMismatch(BinOp, Value), + // InvalidTextInterpolation(Value), + // Merge1ArgMustBeRecord(Value), + // Merge2ArgMustBeUnionOrOptional(Value), + // MergeEmptyNeedsAnnotation, + // MergeHandlerMissingVariant(Label), + // MergeVariantMissingHandler(Label), + // MergeAnnotMismatch, + // MergeHandlerTypeMismatch, + // MergeHandlerReturnTypeMustNotBeDependent, + // ProjectionMustBeRecord, + // ProjectionMissingEntry, + // ProjectionDuplicateField, Sort, RecordTypeDuplicateField, - RecordTypeMergeRequiresRecordType(Value), + // RecordTypeMergeRequiresRecordType(Value), UnionTypeDuplicateField, - EquivalenceArgumentMustBeTerm(bool, Value), - EquivalenceTypeMismatch(Value, Value), - AssertMismatch(Value, Value), - AssertMustTakeEquivalence, + // EquivalenceArgumentMustBeTerm(bool, Value), + // EquivalenceTypeMismatch(Value, Value), + // AssertMismatch(Value, Value), + // AssertMustTakeEquivalence, Custom(String), } @@ -103,21 +103,22 @@ impl std::fmt::Display for TypeError { InvalidOutputType(v) => { v.span().error("Type error: Invalid function output") } - NotAFunction(v) => v.span().error("Type error: Not a function"), - TypeMismatch(x, y, z) => { - x.span() - .error("Type error: Wrong type of function argument") - + "\n" - + &z.span().error(format!( - "This argument has type {:?}", - z.get_type().unwrap() - )) - + "\n" - + &y.span().error(format!( - "But the function expected an argument of type {:?}", - y - )) - } + // NotAFunction(v) => v.span().error("Type error: Not a function"), + // TypeMismatch(x, y, z) => { + // x.span() + // .error("Type error: Wrong type of function argument") + // + "\n" + // + &z.span().error(format!( + // "This argument has type {:?}", + // z.get_type().unwrap() + // )) + // + "\n" + // + &y.span().error(format!( + // "But the function expected an argument of type {:?}", + // y + // )) + // } + Custom(s) => format!("Type error: Unhandled error: {}", s), _ => format!("Type error: Unhandled error: {:?}", self.message), }; write!(f, "{}", msg) diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 0f3754e..44678cd 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -357,8 +357,8 @@ fn type_last_layer( use syntax::Builtin::*; use syntax::Const::Type; use syntax::ExprKind::*; - use TypeMessage::*; - let mkerr = |msg: TypeMessage| Err(TypeError::new(msg)); + let mkerr = + |msg: &str| Err(TypeError::new(TypeMessage::Custom(msg.to_string()))); /// Intermediary return type enum Ret { @@ -381,10 +381,10 @@ fn type_last_layer( let tf_borrow = tf.as_whnf(); let (tx, tb) = match &*tf_borrow { ValueKind::Pi(_, tx, tb) => (tx, tb), - _ => return mkerr(NotAFunction(f.clone())), + _ => return mkerr("NotAFunction"), }; if &a.get_type()? != tx { - return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); + return mkerr("TypeMismatch"); } let ret = tb.subst_shift(&AlphaVar::default(), a); @@ -393,35 +393,33 @@ fn type_last_layer( } Annot(x, t) => { if &x.get_type()? != t { - return mkerr(AnnotMismatch(x.clone(), t.clone())); + return mkerr("AnnotMismatch"); } RetWhole(x.clone()) } Assert(t) => { match &*t.as_whnf() { ValueKind::Equivalence(x, y) if x == y => {} - ValueKind::Equivalence(x, y) => { - return mkerr(AssertMismatch(x.clone(), y.clone())) - } - _ => return mkerr(AssertMustTakeEquivalence), + ValueKind::Equivalence(..) => return mkerr("AssertMismatch"), + _ => return mkerr("AssertMustTakeEquivalence"), } RetTypeOnly(t.clone()) } BoolIf(x, y, z) => { if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) { - return mkerr(InvalidPredicate(x.clone())); + return mkerr("InvalidPredicate"); } if y.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(IfBranchMustBeTerm(true, y.clone())); + return mkerr("IfBranchMustBeTerm"); } if z.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(IfBranchMustBeTerm(false, z.clone())); + return mkerr("IfBranchMustBeTerm"); } if y.get_type()? != z.get_type()? { - return mkerr(IfBranchMismatch(y.clone(), z.clone())); + return mkerr("IfBranchMismatch"); } RetTypeOnly(y.get_type()?) @@ -433,7 +431,7 @@ fn type_last_layer( { args[0].clone() } - _ => return mkerr(InvalidListType(t.clone())), + _ => return mkerr("InvalidListType"), }; RetWhole(Value::from_kind_and_type( ValueKind::EmptyListLit(arg), @@ -443,18 +441,14 @@ fn type_last_layer( NEListLit(xs) => { let mut iter = xs.iter().enumerate(); let (_, x) = iter.next().unwrap(); - for (i, y) in iter { + for (_, y) in iter { if x.get_type()? != y.get_type()? { - return mkerr(InvalidListElement( - i, - x.get_type()?, - y.clone(), - )); + return mkerr("InvalidListElement"); } } let t = x.get_type()?; if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidListType(t)); + return mkerr("InvalidListType"); } RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t)) @@ -462,7 +456,7 @@ fn type_last_layer( SomeLit(x) => { let t = x.get_type()?; if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidOptionalType(t)); + return mkerr("InvalidOptionalType"); } RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t)) @@ -479,48 +473,25 @@ fn type_last_layer( Field(r, x) => { match &*r.get_type()?.as_whnf() { ValueKind::RecordType(kts) => match kts.get(&x) { - Some(tth) => { - RetTypeOnly(tth.clone()) - }, - None => return mkerr(MissingRecordField(x.clone(), - r.clone())), + Some(tth) => RetTypeOnly(tth.clone()), + None => return mkerr("MissingRecordField"), }, // TODO: branch here only when r.get_type() is a Const _ => { match &*r.as_whnf() { ValueKind::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > - Some(Some(t)) => { - RetTypeOnly( - tck_pi_type( - ctx.new_binder(x), - t.clone(), - r.under_binder(), - )? - ) - }, - Some(None) => { - RetTypeOnly(r.clone()) - }, - None => { - return mkerr(MissingUnionField( - x.clone(), - r.clone(), - )) - }, - }, - _ => { - return mkerr(NotARecord( - x.clone(), - r.clone() - )) + Some(Some(t)) => RetTypeOnly(tck_pi_type( + ctx.new_binder(x), + t.clone(), + r.under_binder(), + )?), + Some(None) => RetTypeOnly(r.clone()), + None => return mkerr("MissingUnionField"), }, + _ => return mkerr("NotARecord"), } - } - // _ => mkerr(NotARecord( - // x, - // r?, - // )), + } // _ => mkerr("NotARecord"), } } Const(c) => RetWhole(const_to_value(*c)), @@ -535,7 +506,7 @@ fn type_last_layer( use InterpolatedTextContents::Expr; if let Expr(x) = contents { if x.get_type()? != text_type { - return mkerr(InvalidTextInterpolation(x.clone())); + return mkerr("InvalidTextInterpolation"); } } } @@ -549,14 +520,14 @@ fn type_last_layer( let l_type_borrow = l_type.as_whnf(); let kts_x = match &*l_type_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(MustCombineRecord(l.clone())), + _ => return mkerr("MustCombineRecord"), }; // Extract the RHS record type let r_type_borrow = r_type.as_whnf(); let kts_y = match &*r_type_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(MustCombineRecord(r.clone())), + _ => return mkerr("MustCombineRecord"), }; // Union the two records, prefering @@ -584,18 +555,14 @@ fn type_last_layer( let borrow_l = l.as_whnf(); let kts_x = match &*borrow_l { ValueKind::RecordType(kts) => kts, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) - } + _ => return mkerr("RecordTypeMergeRequiresRecordType"), }; // Extract the RHS record type let borrow_r = r.as_whnf(); let kts_y = match &*borrow_r { ValueKind::RecordType(kts) => kts, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) - } + _ => return mkerr("RecordTypeMergeRequiresRecordType"), }; // Ensure that the records combine without a type error @@ -618,28 +585,28 @@ fn type_last_layer( RetWhole(tck_record_type(kts.into_iter().map(Ok))?) } - BinOp(o @ ListAppend, l, r) => { + BinOp(ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { ValueKind::AppliedBuiltin(List, _, _) => {} - _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), + _ => return mkerr("BinOpTypeMismatch"), } if l.get_type()? != r.get_type()? { - return mkerr(BinOpTypeMismatch(*o, r.clone())); + return mkerr("BinOpTypeMismatch"); } RetTypeOnly(l.get_type()?) } BinOp(Equivalence, l, r) => { if l.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone())); + return mkerr("EquivalenceArgumentMustBeTerm"); } if r.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone())); + return mkerr("EquivalenceArgumentMustBeTerm"); } if l.get_type()? != r.get_type()? { - return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); + return mkerr("EquivalenceTypeMismatch"); } RetWhole(Value::from_kind_and_type( @@ -665,11 +632,11 @@ fn type_last_layer( }); if l.get_type()? != t { - return mkerr(BinOpTypeMismatch(*o, l.clone())); + return mkerr("BinOpTypeMismatch"); } if r.get_type()? != t { - return mkerr(BinOpTypeMismatch(*o, r.clone())); + return mkerr("BinOpTypeMismatch"); } RetTypeOnly(t) @@ -679,7 +646,7 @@ fn type_last_layer( let record_borrow = record_type.as_whnf(); let handlers = match &*record_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(Merge1ArgMustBeRecord(record.clone())), + _ => return mkerr("Merge1ArgMustBeRecord"), }; let union_type = union.get_type()?; @@ -697,9 +664,7 @@ fn type_last_layer( kts.insert("Some".into(), Some(ty.clone())); Cow::Owned(kts) } - _ => { - return mkerr(Merge2ArgMustBeUnionOrOptional(union.clone())) - } + _ => return mkerr("Merge2ArgMustBeUnionOrOptional"), }; let mut inferred_type = None; @@ -711,19 +676,11 @@ fn type_last_layer( let handler_type_borrow = handler_type.as_whnf(); let (tx, tb) = match &*handler_type_borrow { ValueKind::Pi(_, tx, tb) => (tx, tb), - _ => { - return mkerr(NotAFunction( - handler_type.clone(), - )) - } + _ => return mkerr("NotAFunction"), }; if variant_type != tx { - return mkerr(TypeMismatch( - handler_type.clone(), - tx.clone(), - variant_type.clone(), - )); + return mkerr("TypeMismatch"); } // Extract `tb` from under the binder. Fails if the variable was used @@ -731,41 +688,39 @@ fn type_last_layer( match tb.over_binder() { Some(x) => x, None => return mkerr( - MergeHandlerReturnTypeMustNotBeDependent, + "MergeHandlerReturnTypeMustNotBeDependent", ), } } // Union alternative without type Some(None) => handler_type.clone(), - None => { - return mkerr(MergeHandlerMissingVariant(x.clone())) - } + None => return mkerr("MergeHandlerMissingVariant"), }; match &inferred_type { None => inferred_type = Some(handler_return_type), Some(t) => { if t != &handler_return_type { - return mkerr(MergeHandlerTypeMismatch); + return mkerr("MergeHandlerTypeMismatch"); } } } } for x in variants.keys() { if !handlers.contains_key(x) { - return mkerr(MergeVariantMissingHandler(x.clone())); + return mkerr("MergeVariantMissingHandler"); } } match (inferred_type, type_annot.as_ref()) { (Some(t1), Some(t2)) => { if &t1 != t2 { - return mkerr(MergeAnnotMismatch); + return mkerr("MergeAnnotMismatch"); } RetTypeOnly(t1) } (Some(t), None) => RetTypeOnly(t), (None, Some(t)) => RetTypeOnly(t.clone()), - (None, None) => return mkerr(MergeEmptyNeedsAnnotation), + (None, None) => return mkerr("MergeEmptyNeedsAnnotation"), } } ToMap(_, _) => unimplemented!("toMap"), @@ -774,18 +729,18 @@ fn type_last_layer( let record_type_borrow = record_type.as_whnf(); let kts = match &*record_type_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(ProjectionMustBeRecord), + _ => return mkerr("ProjectionMustBeRecord"), }; let mut new_kts = HashMap::new(); for l in labels { match kts.get(l) { - None => return mkerr(ProjectionMissingEntry), + None => return mkerr("ProjectionMissingEntry"), Some(t) => { use std::collections::hash_map::Entry; match new_kts.entry(l.clone()) { Entry::Occupied(_) => { - return mkerr(ProjectionDuplicateField) + return mkerr("ProjectionDuplicateField") } Entry::Vacant(e) => e.insert(t.clone()), } diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index 870388d..9342fd8 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -1,8 +1 @@ -[unknown location] Type error: Wrong type of function argument -[unknown location] This argument has type Sort - --> 5:21 - | -5 | in let pow = λ(X : Kind) → X → Type␊ - | ^--^ - | - = But the function expected an argument of type Kind +Type error: Unhandled error: TypeMismatch diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt index 3f737c2..045eb98 100644 --- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt +++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt @@ -1 +1 @@ -Type error: Unhandled error: AnnotMismatch(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("x"): [Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@Unevaled { value: AppliedBuiltin(Natural, [], []), type: Type } }]}, size: 1 })), type: Value@WHNF { value: RecordType({Label("x"): Value@Unevaled { value: AppliedBuiltin(Natural, [], []), type: Type }}), type: Type } }, Value@WHNF { value: RecordType({Label("y"): Value@Unevaled { value: AppliedBuiltin(Natural, [], []), type: Type }}), type: Type }) +Type error: Unhandled error: AnnotMismatch diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt index d211716..045eb98 100644 --- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt +++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt @@ -1 +1 @@ -Type error: Unhandled error: AnnotMismatch(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("x"): [Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }]}, size: 1 })), type: Value@WHNF { value: RecordType({Label("x"): Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type }}), type: Type } }, Value@WHNF { value: RecordType({Label("x"): Value@WHNF { value: AppliedBuiltin(Text, [], []), type: Type }}), type: Type }) +Type error: Unhandled error: AnnotMismatch diff --git a/dhall/tests/type-errors/unit/AssertDoubleZeros.txt b/dhall/tests/type-errors/unit/AssertDoubleZeros.txt index 6886495..d8627ba 100644 --- a/dhall/tests/type-errors/unit/AssertDoubleZeros.txt +++ b/dhall/tests/type-errors/unit/AssertDoubleZeros.txt @@ -1 +1 @@ -Type error: Unhandled error: AssertMismatch(Value@WHNF { value: DoubleLit(NaiveDouble(-0.0)), type: Value@WHNF { value: AppliedBuiltin(Double, [], []), type: Type } }, Value@WHNF { value: DoubleLit(NaiveDouble(0.0)), type: Value@WHNF { value: AppliedBuiltin(Double, [], []), type: Type } }) +Type error: Unhandled error: AssertMismatch diff --git a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt index 6f8e4a7..d8627ba 100644 --- a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt +++ b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt @@ -1 +1 @@ -Type error: Unhandled error: AssertMismatch(Value@WHNF { value: NaturalLit(1), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }, Value@WHNF { value: NaturalLit(2), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: AssertMismatch diff --git a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt index bdbe0e4..89749e9 100644 --- a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt +++ b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt @@ -1 +1 @@ -Type error: Unhandled error: EquivalenceTypeMismatch(Value@Unevaled { value: PartialExpr(BoolLit(false)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: EquivalenceTypeMismatch diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt index 23b37d3..7c48d6f 100644 --- a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt +++ b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt @@ -1 +1 @@ -Type error: Unhandled error: EquivalenceArgumentMustBeTerm(true, Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type }) +Type error: Unhandled error: EquivalenceArgumentMustBeTerm diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 8507ccf..9342fd8 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -1,13 +1 @@ -[unknown location] Type error: Wrong type of function argument - --> 1:22 - | -1 | (λ(_ : Natural) → _) True␊ - | ^--^ - | - = This argument has type Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } - --> 1:8 - | -1 | (λ(_ : Natural) → _) True␊ - | ^-----^ - | - = But the function expected an argument of type Value@NF { value: AppliedBuiltin(Natural, [], []), type: Type } +Type error: Unhandled error: TypeMismatch diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt index 062f9de..f1cdf92 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -1,6 +1 @@ - --> 1:1 - | -1 | True True␊ - | ^--^ - | - = Type error: Not a function +Type error: Unhandled error: NotAFunction diff --git a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt index 4d28695..6b1dcdd 100644 --- a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt +++ b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt @@ -1 +1 @@ -Type error: Unhandled error: IfBranchMismatch(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }, Value@Unevaled { value: PartialExpr(TextLit(InterpolatedText { head: "", tail: [] })), type: Value@WHNF { value: AppliedBuiltin(Text, [], []), type: Type } }) +Type error: Unhandled error: IfBranchMismatch diff --git a/dhall/tests/type-errors/unit/IfBranchesNotType.txt b/dhall/tests/type-errors/unit/IfBranchesNotType.txt index 8ef3a40..06039a7 100644 --- a/dhall/tests/type-errors/unit/IfBranchesNotType.txt +++ b/dhall/tests/type-errors/unit/IfBranchesNotType.txt @@ -1 +1 @@ -Type error: Unhandled error: IfBranchMustBeTerm(true, Type) +Type error: Unhandled error: IfBranchMustBeTerm diff --git a/dhall/tests/type-errors/unit/IfNotBool.txt b/dhall/tests/type-errors/unit/IfNotBool.txt index 665093f..b2d200c 100644 --- a/dhall/tests/type-errors/unit/IfNotBool.txt +++ b/dhall/tests/type-errors/unit/IfNotBool.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidPredicate(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: InvalidPredicate diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt index 61096d0..045eb98 100644 --- a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt +++ b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt @@ -1 +1 @@ -Type error: Unhandled error: AnnotMismatch(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type }) +Type error: Unhandled error: AnnotMismatch diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index e075521..9342fd8 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -1,13 +1 @@ - --> 1:6 - | -1 | [] : List Type␊ - | ^--^ - | - = Type error: Wrong type of function argument - --> 1:11 - | -1 | [] : List Type␊ - | ^--^ - | - = This argument has type Kind -[unknown location] But the function expected an argument of type Type +Type error: Unhandled error: TypeMismatch diff --git a/dhall/tests/type-errors/unit/ListLiteralNotType.txt b/dhall/tests/type-errors/unit/ListLiteralNotType.txt index 99b95a3..3937453 100644 --- a/dhall/tests/type-errors/unit/ListLiteralNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralNotType.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidListType(Type) +Type error: Unhandled error: InvalidListType diff --git a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt index 2355b7c..a64cf67 100644 --- a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt +++ b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidListElement(1, Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: InvalidListElement diff --git a/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt index d4e9024..711d77d 100644 --- a/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt +++ b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt @@ -1 +1 @@ -Type error: Unhandled error: MergeVariantMissingHandler(Label("x")) +Type error: Unhandled error: MergeVariantMissingHandler diff --git a/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt index 7da5cb9..4c72653 100644 --- a/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt +++ b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt @@ -1 +1 @@ -Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional(Value@Unevaled { value: UnionType({}), type: Type }) +Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional diff --git a/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt index 7da5cb9..4c72653 100644 --- a/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt +++ b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt @@ -1 +1 @@ -Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional(Value@Unevaled { value: UnionType({}), type: Type }) +Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt index c5ed223..f1cdf92 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt @@ -1 +1 @@ -[unknown location] Type error: Not a function +Type error: Unhandled error: NotAFunction diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt index 7da5cb9..4c72653 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt @@ -1 +1 @@ -Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional(Value@Unevaled { value: UnionType({}), type: Type }) +Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt index 19f375a..9342fd8 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -1,13 +1 @@ -[unknown location] Type error: Wrong type of function argument - --> 1:38 - | -1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1)␊ - | ^-----^ - | - = This argument has type Type - --> 1:19 - | -1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1)␊ - | ^--^ - | - = But the function expected an argument of type Value@NF { value: AppliedBuiltin(Bool, [], []), type: Type } +Type error: Unhandled error: TypeMismatch diff --git a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt index 785fc63..d151710 100644 --- a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt +++ b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt @@ -1 +1 @@ -Type error: Unhandled error: Merge1ArgMustBeRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) +Type error: Unhandled error: Merge1ArgMustBeRecord diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler1.txt b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt index d4e9024..711d77d 100644 --- a/dhall/tests/type-errors/unit/MergeMissingHandler1.txt +++ b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt @@ -1 +1 @@ -Type error: Unhandled error: MergeVariantMissingHandler(Label("x")) +Type error: Unhandled error: MergeVariantMissingHandler diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler2.txt b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt index d583de7..711d77d 100644 --- a/dhall/tests/type-errors/unit/MergeMissingHandler2.txt +++ b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt @@ -1 +1 @@ -Type error: Unhandled error: MergeVariantMissingHandler(Label("y")) +Type error: Unhandled error: MergeVariantMissingHandler diff --git a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt index 8954538..4c72653 100644 --- a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt +++ b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt @@ -1 +1 @@ -Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) +Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional diff --git a/dhall/tests/type-errors/unit/MergeUnusedHandler.txt b/dhall/tests/type-errors/unit/MergeUnusedHandler.txt index b7eefdd..a429b89 100644 --- a/dhall/tests/type-errors/unit/MergeUnusedHandler.txt +++ b/dhall/tests/type-errors/unit/MergeUnusedHandler.txt @@ -1 +1 @@ -Type error: Unhandled error: MergeHandlerMissingVariant(Label("y")) +Type error: Unhandled error: MergeHandlerMissingVariant diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index 784fd8a..9342fd8 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -1,13 +1 @@ - --> 1:1 - | -1 | Natural/subtract True True␊ - | ^--------------^ - | - = Type error: Wrong type of function argument - --> 1:18 - | -1 | Natural/subtract True True␊ - | ^--^ - | - = This argument has type Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } -[unknown location] But the function expected an argument of type Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } +Type error: Unhandled error: TypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt index b9314fb..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt +++ b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(BoolAnd, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt index 253e2f2..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt +++ b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(BoolEQ, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt index 735d101..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt index b931c01..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NEListLit([Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }])), type: Value@WHNF { value: AppliedBuiltin(List, [Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type }], [Value@WHNF { value: Pi(Binder(`_`), Type, Type), type: Kind }]), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt index 735d101..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt index 735d101..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt index c3c83b1..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt +++ b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(BoolNE, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt index 32caf35..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt +++ b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(BoolOr, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt index 4e578c4..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt +++ b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(NaturalPlus, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt index 58d4b23..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt +++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt index 58d4b23..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt +++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt index 8caf338..9f10587 100644 --- a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt +++ b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt @@ -1 +1 @@ -Type error: Unhandled error: BinOpTypeMismatch(NaturalTimes, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) +Type error: Unhandled error: BinOpTypeMismatch diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt index e524a07..3937453 100644 --- a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt +++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidListType(Value@WHNF { value: AppliedBuiltin(Optional, [Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type }], [Value@WHNF { value: Pi(Binder(`_`), Type, Type), type: Kind }]), type: Type }) +Type error: Unhandled error: InvalidListType diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt index 5ff6a69..045eb98 100644 --- a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt +++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt @@ -1 +1 @@ -Type error: Unhandled error: AnnotMismatch(Value@Unevaled { value: PartialExpr(NEListLit([Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@Unevaled { value: AppliedBuiltin(Natural, [], []), type: Type } }])), type: Value@WHNF { value: AppliedBuiltin(List, [Value@Unevaled { value: AppliedBuiltin(Natural, [], []), type: Type }], [Value@WHNF { value: Pi(Binder(`_`), Type, Type), type: Kind }]), type: Type } }, Value@WHNF { value: AppliedBuiltin(Optional, [Value@Unevaled { value: AppliedBuiltin(Natural, [], []), type: Type }], [Value@WHNF { value: Pi(Binder(`_`), Type, Type), type: Kind }]), type: Type }) +Type error: Unhandled error: AnnotMismatch diff --git a/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt index 1770faa..ea48374 100644 --- a/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt +++ b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt @@ -1 +1 @@ -Type error: Unhandled error: MissingRecordField(Label("x"), Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {}, size: 0 })), type: Value@WHNF { value: RecordType({}), type: Type } }) +Type error: Unhandled error: MissingRecordField diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt index 9211e05..ea48374 100644 --- a/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt +++ b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt @@ -1 +1 @@ -Type error: Unhandled error: MissingRecordField(Label("x"), Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("y"): [Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {}, size: 0 })), type: Value@Unevaled { value: RecordType({}), type: Type } }]}, size: 1 })), type: Value@WHNF { value: RecordType({Label("y"): Value@Unevaled { value: RecordType({}), type: Type }}), type: Type } }) +Type error: Unhandled error: MissingRecordField diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt index 292ab0e..35d604f 100644 --- a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt +++ b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt @@ -1 +1 @@ -Type error: Unhandled error: NotARecord(Label("x"), Value@WHNF { value: BoolLit(true), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) +Type error: Unhandled error: NotARecord diff --git a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt index dff292e..35d604f 100644 --- a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt +++ b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt @@ -1 +1 @@ -Type error: Unhandled error: NotARecord(Label("x"), Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) +Type error: Unhandled error: NotARecord diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt index 27ed928..7fd03d3 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt @@ -1 +1 @@ -Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) +Type error: Unhandled error: RecordTypeMergeRequiresRecordType diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt index 27ed928..7fd03d3 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt @@ -1 +1 @@ -Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) +Type error: Unhandled error: RecordTypeMergeRequiresRecordType diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt index 27ed928..7fd03d3 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt @@ -1 +1 @@ -Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) +Type error: Unhandled error: RecordTypeMergeRequiresRecordType diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt index 27ed928..7fd03d3 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt @@ -1 +1 @@ -Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) +Type error: Unhandled error: RecordTypeMergeRequiresRecordType diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt index 27ed928..7fd03d3 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt @@ -1 +1 @@ -Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) +Type error: Unhandled error: RecordTypeMergeRequiresRecordType diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt index 27ed928..7fd03d3 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt @@ -1 +1 @@ -Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) +Type error: Unhandled error: RecordTypeMergeRequiresRecordType diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt index fbb410f..42600a4 100644 --- a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt +++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt @@ -1 +1 @@ -Type error: Unhandled error: MustCombineRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) +Type error: Unhandled error: MustCombineRecord diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt index fbb410f..42600a4 100644 --- a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt +++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt @@ -1 +1 @@ -Type error: Unhandled error: MustCombineRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) +Type error: Unhandled error: MustCombineRecord diff --git a/dhall/tests/type-errors/unit/SomeNotType.txt b/dhall/tests/type-errors/unit/SomeNotType.txt index 43581a0..63fec72 100644 --- a/dhall/tests/type-errors/unit/SomeNotType.txt +++ b/dhall/tests/type-errors/unit/SomeNotType.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidOptionalType(Type) +Type error: Unhandled error: InvalidOptionalType diff --git a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt index feb6b2e..f1a77d9 100644 --- a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt +++ b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidTextInterpolation(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) +Type error: Unhandled error: InvalidTextInterpolation diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt index 869e9c3..045eb98 100644 --- a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt +++ b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt @@ -1 +1 @@ -Type error: Unhandled error: AnnotMismatch(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) +Type error: Unhandled error: AnnotMismatch diff --git a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt index eb3e09a..f88cb57 100644 --- a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt +++ b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt @@ -1 +1 @@ -Type error: Unhandled error: MissingUnionField(Label("y"), Value@WHNF { value: UnionType({Label("x"): Some(Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type })}), type: Type }) +Type error: Unhandled error: MissingUnionField -- cgit v1.2.3