From 70263bb4535c40ffa73548e3f0b4b574a856d764 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 09:44:24 +0000 Subject: Test type error messages --- dhall/tests/type-errors/hurkensParadox.txt | 1 + dhall/tests/type-errors/mixedUnions.txt | 1 + dhall/tests/type-errors/recordOfKind.txt | 1 + dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt | 1 + dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt | 1 + dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 1 + dhall/tests/type-errors/unit/AssertNotEquivalence.txt | 1 + dhall/tests/type-errors/unit/AssertTriviallyFalse.txt | 1 + dhall/tests/type-errors/unit/EquivalenceNotSameType.txt | 1 + dhall/tests/type-errors/unit/EquivalenceNotTerms.txt | 1 + dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt | 1 + dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt | 1 + dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt | 1 + dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt | 1 + dhall/tests/type-errors/unit/FunctionTypeKindSort.txt | 1 + dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt | 1 + dhall/tests/type-errors/unit/IfBranchesNotMatch.txt | 1 + dhall/tests/type-errors/unit/IfBranchesNotType.txt | 1 + dhall/tests/type-errors/unit/IfNotBool.txt | 1 + dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt | 1 + dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt | 1 + dhall/tests/type-errors/unit/ListLiteralNotType.txt | 1 + dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt | 1 + dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt | 1 + dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt | 1 + dhall/tests/type-errors/unit/MergeAnnotationNotType.txt | 1 + dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt | 1 + dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt | 1 + dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt | 1 + dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt | 1 + dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt | 1 + dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt | 1 + dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt | 1 + dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt | 1 + dhall/tests/type-errors/unit/MergeLhsNotRecord.txt | 1 + dhall/tests/type-errors/unit/MergeMissingHandler1.txt | 1 + dhall/tests/type-errors/unit/MergeMissingHandler2.txt | 1 + dhall/tests/type-errors/unit/MergeRhsNotUnion.txt | 1 + dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt | 1 + dhall/tests/type-errors/unit/OperatorAndNotBool.txt | 1 + dhall/tests/type-errors/unit/OperatorEqualNotBool.txt | 1 + dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt | 1 + dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt | 1 + dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt | 1 + dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt | 1 + dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt | 1 + dhall/tests/type-errors/unit/OperatorOrNotBool.txt | 1 + dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt | 1 + dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt | 1 + dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt | 1 + dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt | 1 + dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt | 1 + dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt | 1 + dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt | 1 + dhall/tests/type-errors/unit/RecordMixedKinds3.txt | 1 + dhall/tests/type-errors/unit/RecordProjectionEmpty.txt | 1 + dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt | 1 + dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt | 1 + dhall/tests/type-errors/unit/RecordSelectionEmpty.txt | 1 + dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt | 1 + dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt | 1 + dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt | 1 + dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt | 1 + dhall/tests/type-errors/unit/RecordTypeValueMember.txt | 1 + dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt | 1 + dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt | 1 + dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt | 1 + .../tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt | 1 + dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt | 1 + .../tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt | 1 + dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt | 1 + dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt | 1 + dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt | 1 + dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt | 1 + dhall/tests/type-errors/unit/SomeNotType.txt | 1 + dhall/tests/type-errors/unit/Sort.txt | 1 + dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt | 1 + dhall/tests/type-errors/unit/TypeAnnotationWrong.txt | 1 + dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt | 1 + dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt | 1 + dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt | 1 + dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt | 1 + dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt | 1 + dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt | 1 + dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt | 1 + dhall/tests/type-errors/unit/UnionTypeNotType.txt | 1 + dhall/tests/type-errors/unit/VariableFree.txt | 1 + 87 files changed, 87 insertions(+) create mode 100644 dhall/tests/type-errors/hurkensParadox.txt create mode 100644 dhall/tests/type-errors/mixedUnions.txt create mode 100644 dhall/tests/type-errors/recordOfKind.txt create mode 100644 dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt create mode 100644 dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt create mode 100644 dhall/tests/type-errors/unit/AssertAlphaTrap.txt create mode 100644 dhall/tests/type-errors/unit/AssertNotEquivalence.txt create mode 100644 dhall/tests/type-errors/unit/AssertTriviallyFalse.txt create mode 100644 dhall/tests/type-errors/unit/EquivalenceNotSameType.txt create mode 100644 dhall/tests/type-errors/unit/EquivalenceNotTerms.txt create mode 100644 dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt create mode 100644 dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt create mode 100644 dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt create mode 100644 dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt create mode 100644 dhall/tests/type-errors/unit/FunctionTypeKindSort.txt create mode 100644 dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt create mode 100644 dhall/tests/type-errors/unit/IfBranchesNotMatch.txt create mode 100644 dhall/tests/type-errors/unit/IfBranchesNotType.txt create mode 100644 dhall/tests/type-errors/unit/IfNotBool.txt create mode 100644 dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt create mode 100644 dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt create mode 100644 dhall/tests/type-errors/unit/ListLiteralNotType.txt create mode 100644 dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt create mode 100644 dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt create mode 100644 dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt create mode 100644 dhall/tests/type-errors/unit/MergeAnnotationNotType.txt create mode 100644 dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt create mode 100644 dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt create mode 100644 dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt create mode 100644 dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt create mode 100644 dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt create mode 100644 dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt create mode 100644 dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt create mode 100644 dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt create mode 100644 dhall/tests/type-errors/unit/MergeLhsNotRecord.txt create mode 100644 dhall/tests/type-errors/unit/MergeMissingHandler1.txt create mode 100644 dhall/tests/type-errors/unit/MergeMissingHandler2.txt create mode 100644 dhall/tests/type-errors/unit/MergeRhsNotUnion.txt create mode 100644 dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt create mode 100644 dhall/tests/type-errors/unit/OperatorAndNotBool.txt create mode 100644 dhall/tests/type-errors/unit/OperatorEqualNotBool.txt create mode 100644 dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt create mode 100644 dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt create mode 100644 dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt create mode 100644 dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt create mode 100644 dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt create mode 100644 dhall/tests/type-errors/unit/OperatorOrNotBool.txt create mode 100644 dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt create mode 100644 dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt create mode 100644 dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt create mode 100644 dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt create mode 100644 dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt create mode 100644 dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt create mode 100644 dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt create mode 100644 dhall/tests/type-errors/unit/RecordMixedKinds3.txt create mode 100644 dhall/tests/type-errors/unit/RecordProjectionEmpty.txt create mode 100644 dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt create mode 100644 dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt create mode 100644 dhall/tests/type-errors/unit/RecordSelectionEmpty.txt create mode 100644 dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt create mode 100644 dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt create mode 100644 dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt create mode 100644 dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt create mode 100644 dhall/tests/type-errors/unit/RecordTypeValueMember.txt create mode 100644 dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt create mode 100644 dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt create mode 100644 dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt create mode 100644 dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt create mode 100644 dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt create mode 100644 dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt create mode 100644 dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt create mode 100644 dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt create mode 100644 dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt create mode 100644 dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt create mode 100644 dhall/tests/type-errors/unit/SomeNotType.txt create mode 100644 dhall/tests/type-errors/unit/Sort.txt create mode 100644 dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt create mode 100644 dhall/tests/type-errors/unit/TypeAnnotationWrong.txt create mode 100644 dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt create mode 100644 dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt create mode 100644 dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt create mode 100644 dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt create mode 100644 dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt create mode 100644 dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt create mode 100644 dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt create mode 100644 dhall/tests/type-errors/unit/UnionTypeNotType.txt create mode 100644 dhall/tests/type-errors/unit/VariableFree.txt (limited to 'dhall/tests/type-errors') diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt new file mode 100644 index 0000000..398ca09 --- /dev/null +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -0,0 +1 @@ +TypeError { type_message: TypeMismatch(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Kind, Value@Unevaled { value: Pi(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind })), type: Kind })), type: Kind }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind }), type: Kind }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind })), type: Kind })), type: Kind }), type: Kind }), type: Sort }), context: TypecheckContext([(Label("bottom"), Replaced(Value@Unevaled { value: Pi(AlphaLabel(any), Type, Value@Unevaled { value: Var(AlphaVar(any, 0)), type: Type }), type: Type })), (Label("not"), Replaced(Value@Unevaled { value: Lam(AlphaLabel(p), Type, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(p, 0)), type: Type }, Value@Unevaled { value: Pi(AlphaLabel(any), Type, Value@Unevaled { value: Var(AlphaVar(any, 0)), type: Type }), type: Type }), type: Type }), type: Value@WHNF { value: Pi(AlphaLabel(p), Type, Type), type: Kind } })), (Label("pow"), Replaced(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } })), (Label("U"), Replaced(Value@Unevaled { value: Pi(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind })), type: Kind })), type: Kind }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind }), type: Kind }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind })), type: Kind })), type: Kind }), type: Kind }), type: Sort }))]) } diff --git a/dhall/tests/type-errors/mixedUnions.txt b/dhall/tests/type-errors/mixedUnions.txt new file mode 100644 index 0000000..e163733 --- /dev/null +++ b/dhall/tests/type-errors/mixedUnions.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidFieldType(Label("Right"), Type), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/recordOfKind.txt b/dhall/tests/type-errors/recordOfKind.txt new file mode 100644 index 0000000..37111df --- /dev/null +++ b/dhall/tests/type-errors/recordOfKind.txt @@ -0,0 +1 @@ +TypeError { type_message: Sort, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt new file mode 100644 index 0000000..57ebd63 --- /dev/null +++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt @@ -0,0 +1 @@ +TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("x"): One(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 }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt new file mode 100644 index 0000000..e829fbd --- /dev/null +++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt @@ -0,0 +1 @@ +TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("x"): One(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 }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt new file mode 100644 index 0000000..78d25d8 --- /dev/null +++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt @@ -0,0 +1 @@ +TypeError { type_message: UnboundVariable(V(Label("_"), 0)), context: TypecheckContext([(Label("x"), Kept(AlphaVar(x, 0), Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }))]) } diff --git a/dhall/tests/type-errors/unit/AssertNotEquivalence.txt b/dhall/tests/type-errors/unit/AssertNotEquivalence.txt new file mode 100644 index 0000000..d2aa197 --- /dev/null +++ b/dhall/tests/type-errors/unit/AssertNotEquivalence.txt @@ -0,0 +1 @@ +TypeError { type_message: AssertMustTakeEquivalence, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt new file mode 100644 index 0000000..caf115d --- /dev/null +++ b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt @@ -0,0 +1 @@ +TypeError { type_message: 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 } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt new file mode 100644 index 0000000..ca31211 --- /dev/null +++ b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt @@ -0,0 +1 @@ +TypeError { type_message: 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 } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt new file mode 100644 index 0000000..2ee2629 --- /dev/null +++ b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt @@ -0,0 +1 @@ +TypeError { type_message: EquivalenceArgumentMustBeTerm(true, Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt new file mode 100644 index 0000000..61cd80c --- /dev/null +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -0,0 +1 @@ +TypeError { type_message: TypeMismatch(Value@Unevaled { value: Lam(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: Var(AlphaVar(`_`, 0)), type: Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type } }), type: Value@WHNF { value: Pi(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt new file mode 100644 index 0000000..0ea727a --- /dev/null +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -0,0 +1 @@ +TypeError { type_message: NotAFunction(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt new file mode 100644 index 0000000..77e88e8 --- /dev/null +++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidInputType(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt new file mode 100644 index 0000000..65825de --- /dev/null +++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidInputType(Value@Unevaled { value: PartialExpr(NaturalLit(2)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt b/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt new file mode 100644 index 0000000..37111df --- /dev/null +++ b/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt @@ -0,0 +1 @@ +TypeError { type_message: Sort, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt new file mode 100644 index 0000000..37111df --- /dev/null +++ b/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt @@ -0,0 +1 @@ +TypeError { type_message: Sort, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt new file mode 100644 index 0000000..f9e5a8a --- /dev/null +++ b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt @@ -0,0 +1 @@ +TypeError { type_message: 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 } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/IfBranchesNotType.txt b/dhall/tests/type-errors/unit/IfBranchesNotType.txt new file mode 100644 index 0000000..a906556 --- /dev/null +++ b/dhall/tests/type-errors/unit/IfBranchesNotType.txt @@ -0,0 +1 @@ +TypeError { type_message: IfBranchMustBeTerm(true, Type), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/IfNotBool.txt b/dhall/tests/type-errors/unit/IfNotBool.txt new file mode 100644 index 0000000..49c0522 --- /dev/null +++ b/dhall/tests/type-errors/unit/IfNotBool.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidPredicate(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt new file mode 100644 index 0000000..f44f646 --- /dev/null +++ b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt @@ -0,0 +1 @@ +TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt new file mode 100644 index 0000000..2808281 --- /dev/null +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -0,0 +1 @@ +TypeError { type_message: TypeMismatch(Value@Unevaled { value: AppliedBuiltin(List, []), type: Value@WHNF { value: Pi(AlphaLabel(`_`), Type, Type), type: Kind } }, Type, Type), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/ListLiteralNotType.txt b/dhall/tests/type-errors/unit/ListLiteralNotType.txt new file mode 100644 index 0000000..7c2565d --- /dev/null +++ b/dhall/tests/type-errors/unit/ListLiteralNotType.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidListType(Type), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt new file mode 100644 index 0000000..d7bb559 --- /dev/null +++ b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidListElement(1, Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt new file mode 100644 index 0000000..b2ecee8 --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt @@ -0,0 +1 @@ +TypeError { type_message: MergeVariantMissingHandler(Label("x")), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt b/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt new file mode 100644 index 0000000..194cb5e --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt @@ -0,0 +1 @@ +TypeError { type_message: MergeAnnotMismatch, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt new file mode 100644 index 0000000..0ecd67a --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt @@ -0,0 +1 @@ +TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: UnionType({}), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt new file mode 100644 index 0000000..611abfb --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt @@ -0,0 +1 @@ +TypeError { type_message: MergeEmptyNeedsAnnotation, context: TypecheckContext([(Label("x"), Kept(AlphaVar(x, 0), Value@WHNF { value: UnionType({}), type: Type }))]) } diff --git a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt new file mode 100644 index 0000000..611abfb --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt @@ -0,0 +1 @@ +TypeError { type_message: MergeEmptyNeedsAnnotation, context: TypecheckContext([(Label("x"), Kept(AlphaVar(x, 0), Value@WHNF { value: UnionType({}), type: Type }))]) } diff --git a/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt new file mode 100644 index 0000000..0ecd67a --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt @@ -0,0 +1 @@ +TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: UnionType({}), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt new file mode 100644 index 0000000..ebc53e2 --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt @@ -0,0 +1 @@ +TypeError { type_message: MergeHandlerReturnTypeMustNotBeDependent, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt new file mode 100644 index 0000000..3555147 --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt @@ -0,0 +1 @@ +TypeError { type_message: NotAFunction(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt new file mode 100644 index 0000000..0ecd67a --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt @@ -0,0 +1 @@ +TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: UnionType({}), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt new file mode 100644 index 0000000..6003f32 --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -0,0 +1 @@ +TypeError { type_message: TypeMismatch(Value@WHNF { value: Pi(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }, Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }), type: Type }, Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt new file mode 100644 index 0000000..2e03930 --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt @@ -0,0 +1 @@ +TypeError { type_message: MergeHandlerTypeMismatch, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt new file mode 100644 index 0000000..d0feb80 --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt @@ -0,0 +1 @@ +TypeError { type_message: Merge1ArgMustBeRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler1.txt b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt new file mode 100644 index 0000000..b2ecee8 --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt @@ -0,0 +1 @@ +TypeError { type_message: MergeVariantMissingHandler(Label("x")), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler2.txt b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt new file mode 100644 index 0000000..daa1668 --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt @@ -0,0 +1 @@ +TypeError { type_message: MergeVariantMissingHandler(Label("y")), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt new file mode 100644 index 0000000..3c0edc2 --- /dev/null +++ b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt @@ -0,0 +1 @@ +TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt new file mode 100644 index 0000000..f2c1d54 --- /dev/null +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -0,0 +1 @@ +TypeError { type_message: TypeMismatch(Value@Unevaled { value: AppliedBuiltin(NaturalSubtract, []), type: Value@WHNF { value: Pi(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }), type: Type }), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt new file mode 100644 index 0000000..4c1b625 --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(BoolAnd, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt new file mode 100644 index 0000000..fa484e1 --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(BoolEQ, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt new file mode 100644 index 0000000..6a5e164 --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt new file mode 100644 index 0000000..dd0e6fc --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt @@ -0,0 +1 @@ +TypeError { type_message: 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 } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt new file mode 100644 index 0000000..6a5e164 --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt new file mode 100644 index 0000000..6a5e164 --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt new file mode 100644 index 0000000..7aed0a1 --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(BoolNE, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt new file mode 100644 index 0000000..031600c --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(BoolOr, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt new file mode 100644 index 0000000..cb055e8 --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(NaturalPlus, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt new file mode 100644 index 0000000..aa1d741 --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt new file mode 100644 index 0000000..aa1d741 --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt new file mode 100644 index 0000000..95f6dda --- /dev/null +++ b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt @@ -0,0 +1 @@ +TypeError { type_message: BinOpTypeMismatch(NaturalTimes, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt new file mode 100644 index 0000000..6e3a002 --- /dev/null +++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidListType(Value@WHNF { value: AppliedBuiltin(Optional, [Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }]), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt new file mode 100644 index 0000000..f8a4bd0 --- /dev/null +++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt @@ -0,0 +1 @@ +TypeError { type_message: 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 }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt b/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt new file mode 100644 index 0000000..bda01cc --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt @@ -0,0 +1 @@ +TypeError { type_message: RecordTypeDuplicateField, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordMixedKinds3.txt b/dhall/tests/type-errors/unit/RecordMixedKinds3.txt new file mode 100644 index 0000000..37111df --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordMixedKinds3.txt @@ -0,0 +1 @@ +TypeError { type_message: Sort, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt b/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt new file mode 100644 index 0000000..e0df8ad --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt @@ -0,0 +1 @@ +TypeError { type_message: ProjectionMissingEntry, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt new file mode 100644 index 0000000..e0df8ad --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt @@ -0,0 +1 @@ +TypeError { type_message: ProjectionMissingEntry, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt new file mode 100644 index 0000000..1e0607a --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt @@ -0,0 +1 @@ +TypeError { type_message: ProjectionMustBeRecord, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt new file mode 100644 index 0000000..73b8483 --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt @@ -0,0 +1 @@ +TypeError { type_message: MissingRecordField(Label("x"), Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {}, size: 0 })), type: Value@WHNF { value: RecordType({}), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt new file mode 100644 index 0000000..036b1c9 --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt @@ -0,0 +1 @@ +TypeError { type_message: MissingRecordField(Label("x"), Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("y"): One(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 } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt new file mode 100644 index 0000000..ed34e38 --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt @@ -0,0 +1 @@ +TypeError { type_message: NotARecord(Label("x"), Value@WHNF { value: BoolLit(true), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt new file mode 100644 index 0000000..8c7b9ae --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt @@ -0,0 +1 @@ +TypeError { type_message: NotARecord(Label("x"), Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt b/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt new file mode 100644 index 0000000..bda01cc --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt @@ -0,0 +1 @@ +TypeError { type_message: RecordTypeDuplicateField, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt new file mode 100644 index 0000000..2829d96 --- /dev/null +++ b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt new file mode 100644 index 0000000..2cde255 --- /dev/null +++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt @@ -0,0 +1 @@ +TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt new file mode 100644 index 0000000..2cde255 --- /dev/null +++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt @@ -0,0 +1 @@ +TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt new file mode 100644 index 0000000..2cde255 --- /dev/null +++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt @@ -0,0 +1 @@ +TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt new file mode 100644 index 0000000..2cde255 --- /dev/null +++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt @@ -0,0 +1 @@ +TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt new file mode 100644 index 0000000..2cde255 --- /dev/null +++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt @@ -0,0 +1 @@ +TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt new file mode 100644 index 0000000..2cde255 --- /dev/null +++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt @@ -0,0 +1 @@ +TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt new file mode 100644 index 0000000..9c34fe3 --- /dev/null +++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt @@ -0,0 +1 @@ +TypeError { type_message: MustCombineRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt new file mode 100644 index 0000000..37111df --- /dev/null +++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt @@ -0,0 +1 @@ +TypeError { type_message: Sort, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt new file mode 100644 index 0000000..37111df --- /dev/null +++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt @@ -0,0 +1 @@ +TypeError { type_message: Sort, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt new file mode 100644 index 0000000..9c34fe3 --- /dev/null +++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt @@ -0,0 +1 @@ +TypeError { type_message: MustCombineRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/SomeNotType.txt b/dhall/tests/type-errors/unit/SomeNotType.txt new file mode 100644 index 0000000..7502c06 --- /dev/null +++ b/dhall/tests/type-errors/unit/SomeNotType.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidOptionalType(Type), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/Sort.txt b/dhall/tests/type-errors/unit/Sort.txt new file mode 100644 index 0000000..37111df --- /dev/null +++ b/dhall/tests/type-errors/unit/Sort.txt @@ -0,0 +1 @@ +TypeError { type_message: Sort, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt new file mode 100644 index 0000000..fefa10f --- /dev/null +++ b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidTextInterpolation(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt new file mode 100644 index 0000000..142d81f --- /dev/null +++ b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt @@ -0,0 +1 @@ +TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt new file mode 100644 index 0000000..22ddeec --- /dev/null +++ b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt @@ -0,0 +1 @@ +TypeError { type_message: MissingUnionField(Label("y"), Value@WHNF { value: UnionType({Label("x"): Some(Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type })}), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt new file mode 100644 index 0000000..db9a35a --- /dev/null +++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt @@ -0,0 +1 @@ +TypeError { type_message: UnboundVariable(V(Label("constructors"), 0)), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt new file mode 100644 index 0000000..fcf31b5 --- /dev/null +++ b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt @@ -0,0 +1 @@ +TypeError { type_message: UnionTypeDuplicateField, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt new file mode 100644 index 0000000..fcf31b5 --- /dev/null +++ b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt @@ -0,0 +1 @@ +TypeError { type_message: UnionTypeDuplicateField, context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt new file mode 100644 index 0000000..85e187e --- /dev/null +++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidFieldType(Label("y"), Type), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt new file mode 100644 index 0000000..85e187e --- /dev/null +++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidFieldType(Label("y"), Type), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt new file mode 100644 index 0000000..72210d5 --- /dev/null +++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidFieldType(Label("y"), Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/UnionTypeNotType.txt b/dhall/tests/type-errors/unit/UnionTypeNotType.txt new file mode 100644 index 0000000..2829d96 --- /dev/null +++ b/dhall/tests/type-errors/unit/UnionTypeNotType.txt @@ -0,0 +1 @@ +TypeError { type_message: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt new file mode 100644 index 0000000..8787a2f --- /dev/null +++ b/dhall/tests/type-errors/unit/VariableFree.txt @@ -0,0 +1 @@ +TypeError { type_message: UnboundVariable(V(Label("x"), 0)), context: TypecheckContext([]) } -- cgit v1.2.3 From 539ab468dfeca7a7b863d5166b2516a2573c044e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 10:33:45 +0000 Subject: Implement basicest Display for TypeError --- dhall/tests/type-errors/hurkensParadox.txt | 2 +- dhall/tests/type-errors/mixedUnions.txt | 2 +- dhall/tests/type-errors/recordOfKind.txt | 2 +- dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt | 2 +- dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt | 2 +- dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 2 +- dhall/tests/type-errors/unit/AssertNotEquivalence.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 | 2 +- dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt | 2 +- dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt | 2 +- dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt | 2 +- dhall/tests/type-errors/unit/FunctionTypeKindSort.txt | 2 +- dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt | 2 +- dhall/tests/type-errors/unit/IfBranchesNotMatch.txt | 2 +- dhall/tests/type-errors/unit/IfBranchesNotType.txt | 2 +- dhall/tests/type-errors/unit/IfNotBool.txt | 2 +- dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt | 2 +- dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt | 2 +- dhall/tests/type-errors/unit/ListLiteralNotType.txt | 2 +- dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt | 2 +- dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt | 2 +- dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt | 2 +- dhall/tests/type-errors/unit/MergeAnnotationNotType.txt | 2 +- dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt | 2 +- dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt | 2 +- dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt | 2 +- dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt | 2 +- dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt | 2 +- dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt | 2 +- dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt | 2 +- dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt | 2 +- dhall/tests/type-errors/unit/MergeLhsNotRecord.txt | 2 +- dhall/tests/type-errors/unit/MergeMissingHandler1.txt | 2 +- dhall/tests/type-errors/unit/MergeMissingHandler2.txt | 2 +- dhall/tests/type-errors/unit/MergeRhsNotUnion.txt | 2 +- dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt | 2 +- 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 +- .../tests/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/RecordLitDuplicateFields.txt | 2 +- dhall/tests/type-errors/unit/RecordMixedKinds3.txt | 2 +- dhall/tests/type-errors/unit/RecordProjectionEmpty.txt | 2 +- dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt | 2 +- dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt | 2 +- dhall/tests/type-errors/unit/RecordSelectionEmpty.txt | 2 +- dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt | 2 +- dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt | 2 +- dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt | 2 +- dhall/tests/type-errors/unit/RecordTypeDuplicateFields.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 +- .../tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt | 2 +- dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt | 2 +- .../tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt | 2 +- dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt | 2 +- dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt | 2 +- dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt | 2 +- dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt | 2 +- dhall/tests/type-errors/unit/SomeNotType.txt | 2 +- dhall/tests/type-errors/unit/Sort.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/UnionDeprecatedConstructorsKeyword.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeNotType.txt | 2 +- dhall/tests/type-errors/unit/VariableFree.txt | 2 +- 87 files changed, 87 insertions(+), 87 deletions(-) (limited to 'dhall/tests/type-errors') diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index 398ca09..ab75f15 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -1 +1 @@ -TypeError { type_message: TypeMismatch(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Kind, Value@Unevaled { value: Pi(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind })), type: Kind })), type: Kind }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind }), type: Kind }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind })), type: Kind })), type: Kind }), type: Kind }), type: Sort }), context: TypecheckContext([(Label("bottom"), Replaced(Value@Unevaled { value: Pi(AlphaLabel(any), Type, Value@Unevaled { value: Var(AlphaVar(any, 0)), type: Type }), type: Type })), (Label("not"), Replaced(Value@Unevaled { value: Lam(AlphaLabel(p), Type, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(p, 0)), type: Type }, Value@Unevaled { value: Pi(AlphaLabel(any), Type, Value@Unevaled { value: Var(AlphaVar(any, 0)), type: Type }), type: Type }), type: Type }), type: Value@WHNF { value: Pi(AlphaLabel(p), Type, Type), type: Kind } })), (Label("pow"), Replaced(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } })), (Label("U"), Replaced(Value@Unevaled { value: Pi(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind })), type: Kind })), type: Kind }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind }), type: Kind }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind })), type: Kind })), type: Kind }), type: Kind }), type: Sort }))]) } +Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/mixedUnions.txt b/dhall/tests/type-errors/mixedUnions.txt index e163733..4b68fea 100644 --- a/dhall/tests/type-errors/mixedUnions.txt +++ b/dhall/tests/type-errors/mixedUnions.txt @@ -1 +1 @@ -TypeError { type_message: InvalidFieldType(Label("Right"), Type), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/recordOfKind.txt b/dhall/tests/type-errors/recordOfKind.txt index 37111df..4b68fea 100644 --- a/dhall/tests/type-errors/recordOfKind.txt +++ b/dhall/tests/type-errors/recordOfKind.txt @@ -1 +1 @@ -TypeError { type_message: Sort, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt index 57ebd63..4b68fea 100644 --- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt +++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt @@ -1 +1 @@ -TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("x"): One(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 }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt index e829fbd..4b68fea 100644 --- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt +++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt @@ -1 +1 @@ -TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("x"): One(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 }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt index 78d25d8..df2b6c1 100644 --- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt +++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt @@ -1 +1 @@ -TypeError { type_message: UnboundVariable(V(Label("_"), 0)), context: TypecheckContext([(Label("x"), Kept(AlphaVar(x, 0), Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }))]) } +Type error: Unbound variable diff --git a/dhall/tests/type-errors/unit/AssertNotEquivalence.txt b/dhall/tests/type-errors/unit/AssertNotEquivalence.txt index d2aa197..4b68fea 100644 --- a/dhall/tests/type-errors/unit/AssertNotEquivalence.txt +++ b/dhall/tests/type-errors/unit/AssertNotEquivalence.txt @@ -1 +1 @@ -TypeError { type_message: AssertMustTakeEquivalence, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt index caf115d..4b68fea 100644 --- a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt +++ b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt @@ -1 +1 @@ -TypeError { type_message: 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 } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt index ca31211..4b68fea 100644 --- a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt +++ b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt @@ -1 +1 @@ -TypeError { type_message: 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 } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt index 2ee2629..4b68fea 100644 --- a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt +++ b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt @@ -1 +1 @@ -TypeError { type_message: EquivalenceArgumentMustBeTerm(true, Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 61cd80c..ab75f15 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -1 +1 @@ -TypeError { type_message: TypeMismatch(Value@Unevaled { value: Lam(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: Var(AlphaVar(`_`, 0)), type: Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type } }), type: Value@WHNF { value: Pi(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt index 0ea727a..4757d2d 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -1 +1 @@ -TypeError { type_message: NotAFunction(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Not a function diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt index 77e88e8..faea460 100644 --- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt @@ -1 +1 @@ -TypeError { type_message: InvalidInputType(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Invalid function input diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt index 65825de..faea460 100644 --- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt @@ -1 +1 @@ -TypeError { type_message: InvalidInputType(Value@Unevaled { value: PartialExpr(NaturalLit(2)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Invalid function input diff --git a/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt b/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt index 37111df..4b68fea 100644 --- a/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt +++ b/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt @@ -1 +1 @@ -TypeError { type_message: Sort, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt index 37111df..4b68fea 100644 --- a/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt +++ b/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt @@ -1 +1 @@ -TypeError { type_message: Sort, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt index f9e5a8a..4b68fea 100644 --- a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt +++ b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt @@ -1 +1 @@ -TypeError { type_message: 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 } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/IfBranchesNotType.txt b/dhall/tests/type-errors/unit/IfBranchesNotType.txt index a906556..4b68fea 100644 --- a/dhall/tests/type-errors/unit/IfBranchesNotType.txt +++ b/dhall/tests/type-errors/unit/IfBranchesNotType.txt @@ -1 +1 @@ -TypeError { type_message: IfBranchMustBeTerm(true, Type), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/IfNotBool.txt b/dhall/tests/type-errors/unit/IfNotBool.txt index 49c0522..4b68fea 100644 --- a/dhall/tests/type-errors/unit/IfNotBool.txt +++ b/dhall/tests/type-errors/unit/IfNotBool.txt @@ -1 +1 @@ -TypeError { type_message: InvalidPredicate(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt index f44f646..4b68fea 100644 --- a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt +++ b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt @@ -1 +1 @@ -TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index 2808281..ab75f15 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -1 +1 @@ -TypeError { type_message: TypeMismatch(Value@Unevaled { value: AppliedBuiltin(List, []), type: Value@WHNF { value: Pi(AlphaLabel(`_`), Type, Type), type: Kind } }, Type, Type), context: TypecheckContext([]) } +Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/ListLiteralNotType.txt b/dhall/tests/type-errors/unit/ListLiteralNotType.txt index 7c2565d..4b68fea 100644 --- a/dhall/tests/type-errors/unit/ListLiteralNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralNotType.txt @@ -1 +1 @@ -TypeError { type_message: InvalidListType(Type), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt index d7bb559..4b68fea 100644 --- a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt +++ b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt @@ -1 +1 @@ -TypeError { type_message: InvalidListElement(1, Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt index b2ecee8..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt +++ b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt @@ -1 +1 @@ -TypeError { type_message: MergeVariantMissingHandler(Label("x")), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt b/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt index 194cb5e..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt +++ b/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt @@ -1 +1 @@ -TypeError { type_message: MergeAnnotMismatch, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt index 0ecd67a..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt +++ b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt @@ -1 +1 @@ -TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: UnionType({}), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt index 611abfb..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt +++ b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt @@ -1 +1 @@ -TypeError { type_message: MergeEmptyNeedsAnnotation, context: TypecheckContext([(Label("x"), Kept(AlphaVar(x, 0), Value@WHNF { value: UnionType({}), type: Type }))]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt index 611abfb..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt +++ b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt @@ -1 +1 @@ -TypeError { type_message: MergeEmptyNeedsAnnotation, context: TypecheckContext([(Label("x"), Kept(AlphaVar(x, 0), Value@WHNF { value: UnionType({}), type: Type }))]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt index 0ecd67a..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt +++ b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt @@ -1 +1 @@ -TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: UnionType({}), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt index ebc53e2..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt @@ -1 +1 @@ -TypeError { type_message: MergeHandlerReturnTypeMustNotBeDependent, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt index 3555147..4757d2d 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt @@ -1 +1 @@ -TypeError { type_message: NotAFunction(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Not a function diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt index 0ecd67a..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt @@ -1 +1 @@ -TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: UnionType({}), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt index 6003f32..ab75f15 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -1 +1 @@ -TypeError { type_message: TypeMismatch(Value@WHNF { value: Pi(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }, Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }), type: Type }, Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }), context: TypecheckContext([]) } +Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt index 2e03930..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt @@ -1 +1 @@ -TypeError { type_message: MergeHandlerTypeMismatch, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt index d0feb80..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt +++ b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt @@ -1 +1 @@ -TypeError { type_message: Merge1ArgMustBeRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler1.txt b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt index b2ecee8..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeMissingHandler1.txt +++ b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt @@ -1 +1 @@ -TypeError { type_message: MergeVariantMissingHandler(Label("x")), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler2.txt b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt index daa1668..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeMissingHandler2.txt +++ b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt @@ -1 +1 @@ -TypeError { type_message: MergeVariantMissingHandler(Label("y")), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt index 3c0edc2..4b68fea 100644 --- a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt +++ b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt @@ -1 +1 @@ -TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index f2c1d54..ab75f15 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -1 +1 @@ -TypeError { type_message: TypeMismatch(Value@Unevaled { value: AppliedBuiltin(NaturalSubtract, []), type: Value@WHNF { value: Pi(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }), type: Type }), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt index 4c1b625..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt +++ b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(BoolAnd, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt index fa484e1..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt +++ b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(BoolEQ, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt index 6a5e164..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt index dd0e6fc..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt @@ -1 +1 @@ -TypeError { type_message: 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 } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt index 6a5e164..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt index 6a5e164..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt +++ b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt index 7aed0a1..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt +++ b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(BoolNE, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt index 031600c..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt +++ b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(BoolOr, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt index cb055e8..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt +++ b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(NaturalPlus, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt index aa1d741..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt +++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt index aa1d741..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt +++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt index 95f6dda..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt +++ b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt @@ -1 +1 @@ -TypeError { type_message: BinOpTypeMismatch(NaturalTimes, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt index 6e3a002..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt +++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt @@ -1 +1 @@ -TypeError { type_message: InvalidListType(Value@WHNF { value: AppliedBuiltin(Optional, [Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }]), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt index f8a4bd0..4b68fea 100644 --- a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt +++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt @@ -1 +1 @@ -TypeError { type_message: 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 }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt b/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt index bda01cc..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt +++ b/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt @@ -1 +1 @@ -TypeError { type_message: RecordTypeDuplicateField, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordMixedKinds3.txt b/dhall/tests/type-errors/unit/RecordMixedKinds3.txt index 37111df..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordMixedKinds3.txt +++ b/dhall/tests/type-errors/unit/RecordMixedKinds3.txt @@ -1 +1 @@ -TypeError { type_message: Sort, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt b/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt index e0df8ad..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt +++ b/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt @@ -1 +1 @@ -TypeError { type_message: ProjectionMissingEntry, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt index e0df8ad..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt +++ b/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt @@ -1 +1 @@ -TypeError { type_message: ProjectionMissingEntry, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt index 1e0607a..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt +++ b/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt @@ -1 +1 @@ -TypeError { type_message: ProjectionMustBeRecord, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt index 73b8483..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt +++ b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt @@ -1 +1 @@ -TypeError { type_message: MissingRecordField(Label("x"), Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {}, size: 0 })), type: Value@WHNF { value: RecordType({}), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt index 036b1c9..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt +++ b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt @@ -1 +1 @@ -TypeError { type_message: MissingRecordField(Label("x"), Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("y"): One(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 } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt index ed34e38..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt +++ b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt @@ -1 +1 @@ -TypeError { type_message: NotARecord(Label("x"), Value@WHNF { value: BoolLit(true), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt index 8c7b9ae..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt +++ b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt @@ -1 +1 @@ -TypeError { type_message: NotARecord(Label("x"), Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt b/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt index bda01cc..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt +++ b/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt @@ -1 +1 @@ -TypeError { type_message: RecordTypeDuplicateField, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt index 2829d96..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt +++ b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt @@ -1 +1 @@ -TypeError { type_message: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt index 2cde255..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt @@ -1 +1 @@ -TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt index 2cde255..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt @@ -1 +1 @@ -TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt index 2cde255..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt @@ -1 +1 @@ -TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt index 2cde255..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt @@ -1 +1 @@ -TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt index 2cde255..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt @@ -1 +1 @@ -TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt index 2cde255..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt +++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt @@ -1 +1 @@ -TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt index 9c34fe3..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt +++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt @@ -1 +1 @@ -TypeError { type_message: MustCombineRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt index 37111df..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt +++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt @@ -1 +1 @@ -TypeError { type_message: Sort, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt index 37111df..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt +++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt @@ -1 +1 @@ -TypeError { type_message: Sort, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt index 9c34fe3..4b68fea 100644 --- a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt +++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt @@ -1 +1 @@ -TypeError { type_message: MustCombineRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/SomeNotType.txt b/dhall/tests/type-errors/unit/SomeNotType.txt index 7502c06..4b68fea 100644 --- a/dhall/tests/type-errors/unit/SomeNotType.txt +++ b/dhall/tests/type-errors/unit/SomeNotType.txt @@ -1 +1 @@ -TypeError { type_message: InvalidOptionalType(Type), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/Sort.txt b/dhall/tests/type-errors/unit/Sort.txt index 37111df..4b68fea 100644 --- a/dhall/tests/type-errors/unit/Sort.txt +++ b/dhall/tests/type-errors/unit/Sort.txt @@ -1 +1 @@ -TypeError { type_message: Sort, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt index fefa10f..4b68fea 100644 --- a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt +++ b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt @@ -1 +1 @@ -TypeError { type_message: InvalidTextInterpolation(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt index 142d81f..4b68fea 100644 --- a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt +++ b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt @@ -1 +1 @@ -TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt index 22ddeec..4b68fea 100644 --- a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt +++ b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt @@ -1 +1 @@ -TypeError { type_message: MissingUnionField(Label("y"), Value@WHNF { value: UnionType({Label("x"): Some(Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type })}), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt index db9a35a..df2b6c1 100644 --- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt +++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt @@ -1 +1 @@ -TypeError { type_message: UnboundVariable(V(Label("constructors"), 0)), context: TypecheckContext([]) } +Type error: Unbound variable diff --git a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt index fcf31b5..4b68fea 100644 --- a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt +++ b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt @@ -1 +1 @@ -TypeError { type_message: UnionTypeDuplicateField, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt index fcf31b5..4b68fea 100644 --- a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt +++ b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt @@ -1 +1 @@ -TypeError { type_message: UnionTypeDuplicateField, context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt index 85e187e..4b68fea 100644 --- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt +++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt @@ -1 +1 @@ -TypeError { type_message: InvalidFieldType(Label("y"), Type), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt index 85e187e..4b68fea 100644 --- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt +++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt @@ -1 +1 @@ -TypeError { type_message: InvalidFieldType(Label("y"), Type), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt index 72210d5..4b68fea 100644 --- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt +++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt @@ -1 +1 @@ -TypeError { type_message: InvalidFieldType(Label("y"), Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/UnionTypeNotType.txt b/dhall/tests/type-errors/unit/UnionTypeNotType.txt index 2829d96..4b68fea 100644 --- a/dhall/tests/type-errors/unit/UnionTypeNotType.txt +++ b/dhall/tests/type-errors/unit/UnionTypeNotType.txt @@ -1 +1 @@ -TypeError { type_message: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) } +Type error: Unhandled error diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt index 8787a2f..df2b6c1 100644 --- a/dhall/tests/type-errors/unit/VariableFree.txt +++ b/dhall/tests/type-errors/unit/VariableFree.txt @@ -1 +1 @@ -TypeError { type_message: UnboundVariable(V(Label("x"), 0)), context: TypecheckContext([]) } +Type error: Unbound variable -- cgit v1.2.3 From 330f063e80a51f8f399864f9d01412e1bff34fe9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 12:43:09 +0000 Subject: Display first pretty type error --- dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 7 ++++++- .../tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt | 7 ++++++- dhall/tests/type-errors/unit/VariableFree.txt | 7 ++++++- 3 files changed, 18 insertions(+), 3 deletions(-) (limited to 'dhall/tests/type-errors') diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt index df2b6c1..f2fc8ce 100644 --- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt +++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt @@ -1 +1,6 @@ -Type error: Unbound variable +Type error: --> 1:47 + | +1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)␊ + | ^ + | + = Unbound variable diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt index df2b6c1..f7903de 100644 --- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt +++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt @@ -1 +1,6 @@ -Type error: Unbound variable +Type error: --> 1:1 + | +1 | constructors < Left : Natural | Right : Bool >␊ + | ^----------^ + | + = Unbound variable diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt index df2b6c1..ef1d16e 100644 --- a/dhall/tests/type-errors/unit/VariableFree.txt +++ b/dhall/tests/type-errors/unit/VariableFree.txt @@ -1 +1,6 @@ -Type error: Unbound variable +Type error: --> 1:1 + | +1 | x␊ + | ^ + | + = Unbound variable -- cgit v1.2.3 From 575adf9a7a87ba5d75548f7cd4efdec53c1fe17c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 12:45:20 +0000 Subject: Move "Type error" error prefix --- dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 4 ++-- dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt | 4 ++-- dhall/tests/type-errors/unit/VariableFree.txt | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) (limited to 'dhall/tests/type-errors') diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt index f2fc8ce..2969c18 100644 --- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt +++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt @@ -1,6 +1,6 @@ -Type error: --> 1:47 + --> 1:47 | 1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)␊ | ^ | - = Unbound variable + = Type error: Unbound variable diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt index f7903de..9cc0c19 100644 --- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt +++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt @@ -1,6 +1,6 @@ -Type error: --> 1:1 + --> 1:1 | 1 | constructors < Left : Natural | Right : Bool >␊ | ^----------^ | - = Unbound variable + = Type error: Unbound variable diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt index ef1d16e..a46aac0 100644 --- a/dhall/tests/type-errors/unit/VariableFree.txt +++ b/dhall/tests/type-errors/unit/VariableFree.txt @@ -1,6 +1,6 @@ -Type error: --> 1:1 + --> 1:1 | 1 | x␊ | ^ | - = Unbound variable + = Type error: Unbound variable -- cgit v1.2.3 From c9c248a4cab21fa1ae7692cd193e3b2c698d431d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 13:49:47 +0000 Subject: Add a few more pretty errors --- dhall/tests/type-errors/hurkensParadox.txt | 2 +- .../tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt | 2 +- dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt | 7 ++++++- dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt | 7 ++++++- dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt | 7 ++++++- dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt | 7 ++++++- dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt | 2 +- .../tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt | 2 +- dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt | 7 ++++++- 9 files changed, 34 insertions(+), 9 deletions(-) (limited to 'dhall/tests/type-errors') diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index ab75f15..69428b8 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -1 +1 @@ -Type error: Wrong type of function argument +[unknown location] Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index ab75f15..69428b8 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -1 +1 @@ -Type error: Wrong type of function argument +[unknown location] Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt index 4757d2d..062f9de 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -1 +1,6 @@ -Type error: Not a function + --> 1:1 + | +1 | True True␊ + | ^--^ + | + = Type error: Not a function diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt index faea460..9e43c33 100644 --- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt @@ -1 +1,6 @@ -Type error: Invalid function input + --> 1:7 + | +1 | λ(_ : 1) → _␊ + | ^ + | + = Type error: Invalid function input diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt index faea460..dd2e758 100644 --- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt @@ -1 +1,6 @@ -Type error: Invalid function input + --> 1:1 + | +1 | 2 → _␊ + | ^ + | + = Type error: Invalid function input diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index ab75f15..bc5cc40 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -1 +1,6 @@ -Type error: Wrong type of function argument + --> 1:6 + | +1 | [] : List Type␊ + | ^--^ + | + = Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt index 4757d2d..c5ed223 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt @@ -1 +1 @@ -Type error: Not a function +[unknown location] Type error: Not a function diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt index ab75f15..69428b8 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -1 +1 @@ -Type error: Wrong type of function argument +[unknown location] Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index ab75f15..fd906bf 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -1 +1,6 @@ -Type error: Wrong type of function argument + --> 1:1 + | +1 | Natural/subtract True True␊ + | ^--------------^ + | + = Type error: Wrong type of function argument -- cgit v1.2.3