From 0d4e033c7ca301f03453210fdef345bdf8018892 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 17:12:22 +0000 Subject: Update type-errors --- dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt | 2 +- dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt | 2 +- dhall/tests/type-errors/unit/AssertDoubleZeros.txt | 2 +- dhall/tests/type-errors/unit/AssertTriviallyFalse.txt | 2 +- dhall/tests/type-errors/unit/EquivalenceNotSameType.txt | 2 +- dhall/tests/type-errors/unit/EquivalenceNotTerms.txt | 2 +- dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt | 4 ++-- dhall/tests/type-errors/unit/IfBranchesNotMatch.txt | 2 +- dhall/tests/type-errors/unit/IfNotBool.txt | 2 +- dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt | 2 +- dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt | 2 +- dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt | 2 +- dhall/tests/type-errors/unit/MergeLhsNotRecord.txt | 2 +- dhall/tests/type-errors/unit/MergeRhsNotUnion.txt | 2 +- dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt | 4 ++-- dhall/tests/type-errors/unit/OperatorAndNotBool.txt | 2 +- dhall/tests/type-errors/unit/OperatorEqualNotBool.txt | 2 +- dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt | 2 +- dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt | 2 +- .../type-errors/unit/OperatorListConcatenateNotListsButMatch.txt | 2 +- dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt | 2 +- dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt | 2 +- dhall/tests/type-errors/unit/OperatorOrNotBool.txt | 2 +- dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt | 2 +- dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt | 2 +- dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt | 2 +- dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt | 2 +- dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt | 2 +- dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt | 2 +- dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt | 2 +- dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt | 2 +- dhall/tests/type-errors/unit/RecordTypeValueMember.txt | 2 +- dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt | 2 +- dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt | 2 +- dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt | 2 +- .../type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt | 2 +- dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt | 2 +- .../type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt | 2 +- dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt | 2 +- dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt | 2 +- dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt | 2 +- dhall/tests/type-errors/unit/TypeAnnotationWrong.txt | 2 +- dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeNotType.txt | 2 +- 45 files changed, 47 insertions(+), 47 deletions(-) (limited to 'dhall/tests') diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt index e15da48..3f737c2 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(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 }) diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt index 16b2d83..d211716 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(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 }) diff --git a/dhall/tests/type-errors/unit/AssertDoubleZeros.txt b/dhall/tests/type-errors/unit/AssertDoubleZeros.txt index d9df5c7..6886495 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(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 } }) diff --git a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt index c7bbf8d..6f8e4a7 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(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 } }) diff --git a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt index 4dbe2ad..bdbe0e4 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(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 } }) diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt index dbce067..23b37d3 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(true, Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 3bb1492..8507ccf 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -4,10 +4,10 @@ 1 | (λ(_ : Natural) → _) True␊ | ^--^ | - = This argument has type Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } + = 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 } + = But the function expected an argument of type Value@NF { value: AppliedBuiltin(Natural, [], []), type: Type } diff --git a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt index 262e54f..4d28695 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(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 } }) diff --git a/dhall/tests/type-errors/unit/IfNotBool.txt b/dhall/tests/type-errors/unit/IfNotBool.txt index 64c0465..665093f 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(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt index 0862162..61096d0 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(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt index 7916dbb..2355b7c 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(1, Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt index ae36eef..19f375a 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -10,4 +10,4 @@ 1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1)␊ | ^--^ | - = But the function expected an argument of type Value@NF { value: AppliedBuiltin(Bool, []), type: Type } + = But the function expected an argument of type Value@NF { value: AppliedBuiltin(Bool, [], []), type: Type } diff --git a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt index da600de..785fc63 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(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt index db93650..8954538 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(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index 02a9c45..784fd8a 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -9,5 +9,5 @@ 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 } + = 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 } diff --git a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt index a4346f2..b9314fb 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(BoolAnd, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt index 57f9095..253e2f2 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(BoolEQ, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt index 2bcb4fc..735d101 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(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt index e314702..b931c01 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 }]), type: Type } }) +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 } }) diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt index 2bcb4fc..735d101 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(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt index 2bcb4fc..735d101 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(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt index 32b3549..c3c83b1 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(BoolNE, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt index f91bd83..32caf35 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(BoolOr, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt index 9194f3a..4e578c4 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(NaturalPlus, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt index e67e9e5..58d4b23 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(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt index e67e9e5..58d4b23 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(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt index 8146ba9..8caf338 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(NaturalTimes, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt index c319c81..e524a07 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 }]), type: Type }) +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 }) diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt index 99df27c..5ff6a69 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 }]), type: Type } }, Value@WHNF { value: AppliedBuiltin(Optional, [Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }]), type: Type }) +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 }) diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt index 27db6a2..292ab0e 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(Label("x"), Value@WHNF { value: BoolLit(true), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt index 36c8e28..dff292e 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(Label("x"), Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt index 72d4316..ed3fd6a 100644 --- a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt +++ b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }) +Type error: Unhandled error: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt index 42cdf65..27ed928 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(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt index 42cdf65..27ed928 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(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt index 42cdf65..27ed928 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(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt index 42cdf65..27ed928 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(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt index 42cdf65..27ed928 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(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt index 42cdf65..27ed928 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(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt index 9a2913b..fbb410f 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(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt index 9a2913b..fbb410f 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(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt index ba2aecd..feb6b2e 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(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }) diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt index 77ff57f..869e9c3 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(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt index 7b2e610..eb3e09a 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(Label("y"), Value@WHNF { value: UnionType({Label("x"): Some(Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type })}), type: Type }) diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt index 83fc426..ded0e5c 100644 --- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt +++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidFieldType(Label("y"), Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }) +Type error: Unhandled error: InvalidFieldType(Label("y"), Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type }) diff --git a/dhall/tests/type-errors/unit/UnionTypeNotType.txt b/dhall/tests/type-errors/unit/UnionTypeNotType.txt index 72d4316..ed3fd6a 100644 --- a/dhall/tests/type-errors/unit/UnionTypeNotType.txt +++ b/dhall/tests/type-errors/unit/UnionTypeNotType.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }) +Type error: Unhandled error: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) -- cgit v1.3.1 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(-) (limited to 'dhall/tests') 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.3.1 From 1e466a20533d936f44430b1bc18508cd00e5ccd2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:48:19 +0000 Subject: Use TyExpr in Typed --- dhall/src/semantics/core/value.rs | 7 +- dhall/src/semantics/phase/mod.rs | 69 +++++++----------- dhall/src/semantics/phase/typecheck.rs | 2 +- dhall/src/semantics/tck/typecheck.rs | 9 ++- dhall/src/tests.rs | 85 ++++------------------ dhall/tests/type-errors/hurkensParadox.txt | 2 +- dhall/tests/type-errors/mixedUnions.txt | 2 +- .../unit/AnnotationRecordWrongFieldName.txt | 2 +- .../unit/AnnotationRecordWrongFieldType.txt | 2 +- dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 7 +- .../tests/type-errors/unit/EquivalenceNotTerms.txt | 2 +- .../unit/FunctionApplicationArgumentNotMatch.txt | 2 +- .../unit/FunctionApplicationIsNotFunction.txt | 2 +- .../unit/FunctionArgumentTypeNotAType.txt | 7 +- .../unit/FunctionTypeArgumentTypeNotAType.txt | 7 +- .../type-errors/unit/LetWithWrongAnnotation.txt | 2 +- .../type-errors/unit/ListLiteralEmptyNotType.txt | 2 +- .../tests/type-errors/unit/MergeHandlerFreeVar.txt | 1 - .../unit/MergeHandlerNotMatchAlternativeType.txt | 22 +++++- .../unit/MergeHandlersWithDifferentType.txt | 66 ++++++++++++++++- .../type-errors/unit/NaturalSubtractNotNatural.txt | 2 +- .../unit/OptionalDeprecatedSyntaxPresent.txt | 2 +- .../type-errors/unit/RecordTypeValueMember.txt | 2 +- .../tests/type-errors/unit/TypeAnnotationWrong.txt | 2 +- .../unit/UnionDeprecatedConstructorsKeyword.txt | 7 +- .../tests/type-errors/unit/UnionTypeMixedKinds.txt | 2 +- .../type-errors/unit/UnionTypeMixedKinds2.txt | 2 +- .../type-errors/unit/UnionTypeMixedKinds3.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeNotType.txt | 2 +- dhall/tests/type-errors/unit/VariableFree.txt | 7 +- 30 files changed, 158 insertions(+), 172 deletions(-) delete mode 100644 dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt (limited to 'dhall/tests') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 3dcbd38..aa819d2 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -9,9 +9,7 @@ use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv}; use crate::semantics::phase::typecheck::{ builtin_to_value, builtin_to_value_env, const_to_value, }; -use crate::semantics::phase::{ - Normalized, NormalizedExpr, ToExprOptions, Typed, -}; +use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; use crate::semantics::{TyExpr, TyExprKind}; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, @@ -207,9 +205,6 @@ impl Value { self.check_type(ty); self.to_whnf_ignore_type() } - pub(crate) fn into_typed(self) -> Typed { - Typed::from_value(self) - } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 68c32b2..0f8194c 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,6 +4,7 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; +use crate::semantics::tck::tyexpr::TyExpr; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -29,7 +30,7 @@ pub struct Resolved(ResolvedExpr); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(Value); +pub struct Typed(TyExpr); /// A normalized expression. /// @@ -78,11 +79,14 @@ impl Parsed { } impl Resolved { - pub fn typecheck(self) -> Result { - Ok(typecheck::typecheck(self.0)?.into_typed()) + pub fn typecheck(&self) -> Result { + Ok(Typed(crate::semantics::tck::typecheck::typecheck(&self.0)?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed()) + Ok(Typed(crate::semantics::tck::typecheck::typecheck_with( + &self.0, + ty.to_expr(), + )?)) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { @@ -97,43 +101,22 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction - pub fn normalize(mut self) -> Normalized { - self.0.normalize_mut(); - Normalized(self.0) - } - - pub(crate) fn from_value(th: Value) -> Self { - Typed(th) + pub fn normalize(&self) -> Normalized { + let mut val = self.0.normalize_whnf_noenv(); + val.normalize_mut(); + Normalized(val) } /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr(&self) -> ResolvedExpr { + fn to_expr(&self) -> ResolvedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: false, }) } - /// Converts a value back to the corresponding AST expression, beta-normalizing in the process. - pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: true, - }) - } - /// Converts a value back to the corresponding AST expression, (alpha,beta)-normalizing in the - /// process. - pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: true, - normalize: true, - }) - } - pub(crate) fn into_value(self) -> Value { - self.0 - } - pub(crate) fn get_type(&self) -> Result { - Ok(self.0.get_type()?.into_typed()) + pub(crate) fn get_type(&self) -> Result { + Ok(Normalized(self.0.get_type()?)) } } @@ -142,19 +125,19 @@ impl Normalized { binary::encode(&self.to_expr()) } + /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> NormalizedExpr { - // TODO: do it directly - self.to_typed().normalize_to_expr() + self.0.to_expr(ToExprOptions { + alpha: false, + normalize: false, + }) } + /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - // TODO: do it directly - self.to_typed().normalize_to_expr_alpha() - } - pub(crate) fn to_typed(&self) -> Typed { - Typed(self.0.clone()) - } - pub(crate) fn into_typed(self) -> Typed { - Typed(self.0) + self.0.to_expr(ToExprOptions { + alpha: true, + normalize: false, + }) } pub(crate) fn to_value(&self) -> Value { self.0.clone() @@ -253,7 +236,7 @@ impl std::hash::Hash for Normalized { impl Eq for Typed {} impl PartialEq for Typed { fn eq(&self, other: &Self) -> bool { - self.0 == other.0 + self.normalize() == other.normalize() } } impl Display for Typed { diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index f559323..6de65e8 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -336,7 +336,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { // )) Ok(e) } - Embed(p) => Ok(p.clone().into_typed().into_value()), + Embed(p) => Ok(p.clone().into_value()), Var(var) => match ctx.lookup(&var) { Some(typed) => Ok(typed.clone()), None => Err(TypeError::new(TypeMessage::UnboundVariable(span))), diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index a83f175..5880d92 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -677,7 +677,7 @@ pub(crate) fn type_with( (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) } ExprKind::Embed(p) => { - return Ok(p.clone().into_typed().into_value().to_tyexpr_noenv()) + return Ok(p.clone().into_value().to_tyexpr_noenv()) } ekind => { let ekind = ekind.traverse_ref(|e| type_with(env, e))?; @@ -692,3 +692,10 @@ pub(crate) fn type_with( pub(crate) fn typecheck(e: &Expr) -> Result { type_with(&TyEnv::new(), e) } + +pub(crate) fn typecheck_with( + expr: &Expr, + ty: Expr, +) -> Result { + typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty))) +} diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 1c687f6..08feadf 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -158,65 +158,24 @@ pub fn run_test(test: Test<'_>) -> Result<()> { parse_file_str(&file_path)?.resolve().unwrap_err(); } TypeInferenceSuccess(expr_file_path, expected_file_path) => { - // let expr = - // parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; - // let ty = expr.get_type()?.to_expr(); - // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; - // let ty = tyexpr.get_type()?.to_expr(); - // - let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let ty = crate::semantics::tck::typecheck::typecheck(&expr)? - .get_type()? - .to_expr(crate::semantics::phase::ToExprOptions { - alpha: false, - normalize: true, - }); + let expr = + parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; + let ty = expr.get_type()?.to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); - // - // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - // let ty = crate::semantics::tck::typecheck::typecheck(&expr)? - // .get_type()?; - // let expected = parse_file_str(&expected_file_path)?.to_expr(); - // let expected = crate::semantics::tck::typecheck::typecheck(&expected)? - // .normalize_whnf_noenv(); - // // if ty != expected { - // // assert_eq_display!(ty.to_expr(crate::semantics::phase::ToExprOptions { - // // alpha: false, - // // normalize: true, - // // }), expected.to_expr(crate::semantics::phase::ToExprOptions { - // // alpha: false, - // // normalize: true, - // // })) - // // } - // assert_eq_pretty!(ty, expected); } TypeInferenceFailure(file_path) => { - // let mut res = - // parse_file_str(&file_path)?.skip_resolve()?.typecheck(); - // if let Ok(e) = &res { - // // If e did typecheck, check that get_type fails - // res = e.get_type(); - // } - // res.unwrap_err(); - - let res = crate::semantics::tck::typecheck::typecheck( - &parse_file_str(&file_path)?.skip_resolve()?.to_expr(), - ); + let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck(); if let Ok(e) = &res { // If e did typecheck, check that get_type fails e.get_type().unwrap_err(); - } else { - res.unwrap_err(); } } // Checks the output of the type error against a text file. If the text file doesn't exist, // we instead write to it the output we got. This makes it easy to update those files: just // `rm -r dhall/tests/type-errors` and run the tests again. TypeError(file_path) => { - let mut res = - parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck(); let file_path = PathBuf::from(file_path); let error_file_path = file_path .strip_prefix("../dhall-lang/tests/type-inference/failure/") @@ -224,11 +183,13 @@ pub fn run_test(test: Test<'_>) -> Result<()> { let error_file_path = PathBuf::from("tests/type-errors/").join(error_file_path); let error_file_path = error_file_path.with_extension("txt"); - if let Ok(e) = &res { - // If e did typecheck, check that get_type fails - res = e.get_type(); - } - let err: Error = res.unwrap_err().into(); + let err: Error = match res { + Ok(e) => { + // If e did typecheck, check that get_type fails + e.get_type().unwrap_err().into() + } + Err(e) => e.into(), + }; if error_file_path.is_file() { let expected_msg = std::fs::read_to_string(error_file_path)?; @@ -241,28 +202,10 @@ pub fn run_test(test: Test<'_>) -> Result<()> { } } Normalization(expr_file_path, expected_file_path) => { - // let expr = parse_file_str(&expr_file_path)? - // .resolve()? - // .typecheck()? - // .normalize() - // .to_expr(); - // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? - // .normalize() - // .to_expr(); - // let expr = parse_file_str(&expr_file_path)? - // .resolve()? - // .typecheck()? - // .to_value() - // .to_tyexpr_noenv() - // .normalize_whnf_noenv() - // .to_expr(crate::semantics::phase::ToExprOptions { - // alpha: false, - // normalize: true, - // }); let expr = parse_file_str(&expr_file_path)? .resolve()? - .tck_and_normalize_new_flow()? + .typecheck()? + .normalize() .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index 9342fd8..4dfdcf5 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -1 +1 @@ -Type error: Unhandled error: TypeMismatch +Type error: Unhandled error: function annot mismatch: (U : Sort) : Kind diff --git a/dhall/tests/type-errors/mixedUnions.txt b/dhall/tests/type-errors/mixedUnions.txt index 30fcdf8..fd4de70 100644 --- a/dhall/tests/type-errors/mixedUnions.txt +++ b/dhall/tests/type-errors/mixedUnions.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidFieldType(Label("Right"), Type) +Type error: Unhandled error: InvalidFieldType diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt index 045eb98..946b296 100644 --- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt +++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt @@ -1 +1 @@ -Type error: Unhandled error: AnnotMismatch +Type error: Unhandled error: annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural } diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt index 045eb98..89817db 100644 --- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt +++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt @@ -1 +1 @@ -Type error: Unhandled error: AnnotMismatch +Type error: Unhandled error: annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text } diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt index 2969c18..87cf48e 100644 --- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt +++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt @@ -1,6 +1 @@ - --> 1:47 - | -1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)␊ - | ^ - | - = Type error: Unbound variable +Type error: Unhandled error: unbound variable diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt index 7c48d6f..de11e28 100644 --- a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt +++ b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt @@ -1 +1 @@ -Type error: Unhandled error: EquivalenceArgumentMustBeTerm +Type error: Unhandled error: EquivalenceArgumentsMustBeTerms diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 9342fd8..8d101c3 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -1 +1 @@ -Type error: Unhandled error: TypeMismatch +Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt index f1cdf92..13b0819 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -1 +1 @@ -Type error: Unhandled error: NotAFunction +Type error: Unhandled error: apply to not Pi: AppliedBuiltin(Bool, [], [], NzEnv { items: [] }) diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt index 9e43c33..a13fb3a 100644 --- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt @@ -1,6 +1 @@ - --> 1:7 - | -1 | λ(_ : 1) → _␊ - | ^ - | - = Type error: Invalid function input +[unknown location] Type error: Invalid function input diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt index dd2e758..a13fb3a 100644 --- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt @@ -1,6 +1 @@ - --> 1:1 - | -1 | 2 → _␊ - | ^ - | - = Type error: Invalid function input +[unknown location] Type error: Invalid function input diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt index 045eb98..cae4fea 100644 --- a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt +++ b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt @@ -1 +1 @@ -Type error: Unhandled error: AnnotMismatch +Type error: Unhandled error: annot mismatch: (True : Bool) : Natural diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index 9342fd8..070e461 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -1 +1 @@ -Type error: Unhandled error: TypeMismatch +Type error: Unhandled error: function annot mismatch: (Type : Kind) : Type diff --git a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt deleted file mode 100644 index de9e256..0000000 --- a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt +++ /dev/null @@ -1 +0,0 @@ -Type error: Unhandled error: MergeHandlerReturnTypeMustNotBeDependent diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt index 9342fd8..77fed39 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -1 +1,21 @@ -Type error: Unhandled error: TypeMismatch +Type error: Unhandled error: MergeHandlerTypeMismatch: Value@WHNF { + value: AppliedBuiltin( + Natural, + [], + [], + NzEnv { + items: [], + }, + ), + type: Type, +} != Value@WHNF { + value: AppliedBuiltin( + Bool, + [], + [], + NzEnv { + items: [], + }, + ), + type: Type, +} diff --git a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt index 8b729a4..02d2970 100644 --- a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt @@ -1 +1,65 @@ -Type error: Unhandled error: MergeHandlerTypeMismatch +Type error: Unhandled error: MergeHandlerTypeMismatch: Value@WHNF { + value: AppliedBuiltin( + Bool, + [], + [], + NzEnv { + items: [ + Replaced( + Value@Unevaled { + value: Var( + AlphaVar(0), + Fresh( + 119, + ), + ), + type: Value@WHNF { + value: AppliedBuiltin( + Bool, + [], + [], + NzEnv { + items: [], + }, + ), + type: Type, + }, + }, + ), + ], + }, + ), + type: Type, +} != Value@WHNF { + value: AppliedBuiltin( + Natural, + [], + [], + NzEnv { + items: [ + Replaced( + Value@Unevaled { + value: Var( + AlphaVar(0), + Fresh( + 120, + ), + ), + type: Value@WHNF { + value: AppliedBuiltin( + Natural, + [], + [], + NzEnv { + items: [], + }, + ), + type: Type, + }, + }, + ), + ], + }, + ), + type: Type, +} diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index 9342fd8..8d101c3 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -1 +1 @@ -Type error: Unhandled error: TypeMismatch +Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt index 045eb98..91d7fb0 100644 --- a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt +++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt @@ -1 +1 @@ -Type error: Unhandled error: AnnotMismatch +Type error: Unhandled error: annot mismatch: ([1] : List Natural) : Optional Natural diff --git a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt index ed3fd6a..fd4de70 100644 --- a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt +++ b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) +Type error: Unhandled error: InvalidFieldType diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt index 045eb98..52fc94d 100644 --- a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt +++ b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt @@ -1 +1 @@ -Type error: Unhandled error: AnnotMismatch +Type error: Unhandled error: annot mismatch: (1 : Natural) : Bool diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt index 9cc0c19..87cf48e 100644 --- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt +++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt @@ -1,6 +1 @@ - --> 1:1 - | -1 | constructors < Left : Natural | Right : Bool >␊ - | ^----------^ - | - = Type error: Unbound variable +Type error: Unhandled error: unbound variable diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt index 07604ba..fd4de70 100644 --- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt +++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidFieldType(Label("y"), Type) +Type error: Unhandled error: InvalidFieldType diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt index 07604ba..fd4de70 100644 --- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt +++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidFieldType(Label("y"), Type) +Type error: Unhandled error: InvalidFieldType diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt index ded0e5c..fd4de70 100644 --- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt +++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidFieldType(Label("y"), Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type }) +Type error: Unhandled error: InvalidFieldType diff --git a/dhall/tests/type-errors/unit/UnionTypeNotType.txt b/dhall/tests/type-errors/unit/UnionTypeNotType.txt index ed3fd6a..fd4de70 100644 --- a/dhall/tests/type-errors/unit/UnionTypeNotType.txt +++ b/dhall/tests/type-errors/unit/UnionTypeNotType.txt @@ -1 +1 @@ -Type error: Unhandled error: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }) +Type error: Unhandled error: InvalidFieldType diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt index a46aac0..87cf48e 100644 --- a/dhall/tests/type-errors/unit/VariableFree.txt +++ b/dhall/tests/type-errors/unit/VariableFree.txt @@ -1,6 +1 @@ - --> 1:1 - | -1 | x␊ - | ^ - | - = Type error: Unbound variable +Type error: Unhandled error: unbound variable -- cgit v1.3.1 From a928c3c4f51d87fd942e8a81727962c00abf6808 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 22:06:01 +0000 Subject: Cleanup variable handling --- dhall/src/semantics/core/value.rs | 10 +++---- dhall/src/semantics/core/var.rs | 32 +--------------------- dhall/src/semantics/core/visitor.rs | 2 +- dhall/src/semantics/nze/env.rs | 2 +- dhall/src/semantics/tck/env.rs | 10 +++---- dhall/src/semantics/tck/tyexpr.rs | 26 ++++++++++++++---- dhall/src/syntax/ast/expr.rs | 16 ++++------- dhall/src/syntax/text/parser.rs | 2 +- dhall/src/syntax/text/printer.rs | 2 +- .../unit/MergeHandlersWithDifferentType.txt | 2 -- 10 files changed, 39 insertions(+), 65 deletions(-) (limited to 'dhall/tests') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 7334552..918826b 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -3,7 +3,7 @@ use std::collections::HashMap; use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::var::{AlphaVar, Binder}; +use crate::semantics::core::var::Binder; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{ builtin_to_value, builtin_to_value_env, const_to_value, @@ -83,7 +83,7 @@ pub(crate) enum ValueKind { // Keep env around to construct Foo/build closures; hopefully temporary. AppliedBuiltin(Builtin, Vec, Vec, NzEnv), - Var(AlphaVar, NzVar), + Var(NzVar), Const(Const), BoolLit(bool), NaturalLit(Natural), @@ -258,9 +258,7 @@ impl Value { pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { let tye = match &*self.as_kind() { - // ValueKind::Var(v, _w) => TyExprKind::Var(*v), - // TODO: Only works when we don't normalize under lambdas - ValueKind::Var(_v, w) => TyExprKind::Var(venv.lookup(w)), + ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)), ValueKind::LamClosure { binder, annot, @@ -618,7 +616,7 @@ impl Closure { match self { Closure::Closure { arg_ty, .. } => { let val = Value::from_kind_and_type( - ValueKind::Var(AlphaVar::default(), var), + ValueKind::Var(var), arg_ty.clone(), ); self.apply(val) diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 3458489..264b81d 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -1,16 +1,4 @@ -use crate::syntax::{Label, V}; - -/// Stores an alpha-normalized variable. -#[derive(Clone, Copy, Eq)] -pub struct AlphaVar { - alpha: V<()>, -} -// TODO: temporary hopefully -impl std::cmp::PartialEq for AlphaVar { - fn eq(&self, _other: &Self) -> bool { - true - } -} +use crate::syntax::Label; // Exactly like a Label, but equality returns always true. // This is so that ValueKind equality is exactly alpha-equivalence. @@ -19,18 +7,6 @@ pub struct Binder { name: Label, } -impl AlphaVar { - pub(crate) fn new(alpha: V<()>) -> Self { - AlphaVar { alpha } - } - pub(crate) fn default() -> Self { - AlphaVar { alpha: V((), 0) } - } - pub(crate) fn idx(&self) -> usize { - self.alpha.idx() - } -} - impl Binder { pub(crate) fn new(name: Label) -> Self { Binder { name } @@ -47,12 +23,6 @@ impl std::cmp::PartialEq for Binder { } } -impl std::fmt::Debug for AlphaVar { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "AlphaVar({})", self.alpha.1) - } -} - impl std::fmt::Debug for Binder { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!(f, "Binder({})", &self.name) diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index aec66f8..2191ce3 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -96,7 +96,7 @@ where v.visit_vec(types)?, env.clone(), ), - Var(v, w) => Var(v.clone(), *w), + Var(v) => Var(*v), Const(k) => Const(*k), BoolLit(b) => BoolLit(*b), NaturalLit(n) => NaturalLit(*n), diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 203d99a..3c42ee7 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -66,7 +66,7 @@ impl NzEnv { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(idx)), + ValueKind::Var(NzVar::new(idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index 32c2f21..1276a48 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -37,7 +37,7 @@ impl VarEnv { } pub fn lookup_fallible(&self, var: &NzVar) -> Option { let idx = self.size.checked_sub(var.idx() + 1)?; - Some(AlphaVar::new(V((), idx))) + Some(AlphaVar::new(idx)) } } @@ -68,7 +68,7 @@ impl NameEnv { self.names.pop(); } - pub fn unlabel_var(&self, var: &V