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/build.rs | 29 +++++++++++++++ dhall/src/tests.rs | 42 +++++++++++++++++----- dhall/tests/type-errors/hurkensParadox.txt | 1 + dhall/tests/type-errors/mixedUnions.txt | 1 + dhall/tests/type-errors/recordOfKind.txt | 1 + .../unit/AnnotationRecordWrongFieldName.txt | 1 + .../unit/AnnotationRecordWrongFieldType.txt | 1 + dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 1 + .../type-errors/unit/AssertNotEquivalence.txt | 1 + .../type-errors/unit/AssertTriviallyFalse.txt | 1 + .../type-errors/unit/EquivalenceNotSameType.txt | 1 + .../tests/type-errors/unit/EquivalenceNotTerms.txt | 1 + .../unit/FunctionApplicationArgumentNotMatch.txt | 1 + .../unit/FunctionApplicationIsNotFunction.txt | 1 + .../unit/FunctionArgumentTypeNotAType.txt | 1 + .../unit/FunctionTypeArgumentTypeNotAType.txt | 1 + .../type-errors/unit/FunctionTypeKindSort.txt | 1 + .../type-errors/unit/FunctionTypeTypeSort.txt | 1 + .../tests/type-errors/unit/IfBranchesNotMatch.txt | 1 + dhall/tests/type-errors/unit/IfBranchesNotType.txt | 1 + dhall/tests/type-errors/unit/IfNotBool.txt | 1 + .../type-errors/unit/LetWithWrongAnnotation.txt | 1 + .../type-errors/unit/ListLiteralEmptyNotType.txt | 1 + .../tests/type-errors/unit/ListLiteralNotType.txt | 1 + .../type-errors/unit/ListLiteralTypesNotMatch.txt | 1 + .../unit/MergeAlternativeHasNoHandler.txt | 1 + .../type-errors/unit/MergeAnnotationMismatch.txt | 1 + .../type-errors/unit/MergeAnnotationNotType.txt | 1 + .../unit/MergeEmptyNeedsDirectAnnotation1.txt | 1 + .../unit/MergeEmptyNeedsDirectAnnotation2.txt | 1 + .../unit/MergeEmptyWithoutAnnotation.txt | 1 + .../tests/type-errors/unit/MergeHandlerFreeVar.txt | 1 + .../type-errors/unit/MergeHandlerNotFunction.txt | 1 + .../type-errors/unit/MergeHandlerNotInUnion.txt | 1 + .../unit/MergeHandlerNotMatchAlternativeType.txt | 1 + .../unit/MergeHandlersWithDifferentType.txt | 1 + dhall/tests/type-errors/unit/MergeLhsNotRecord.txt | 1 + .../type-errors/unit/MergeMissingHandler1.txt | 1 + .../type-errors/unit/MergeMissingHandler2.txt | 1 + dhall/tests/type-errors/unit/MergeRhsNotUnion.txt | 1 + .../type-errors/unit/NaturalSubtractNotNatural.txt | 1 + .../tests/type-errors/unit/OperatorAndNotBool.txt | 1 + .../type-errors/unit/OperatorEqualNotBool.txt | 1 + .../unit/OperatorListConcatenateLhsNotList.txt | 1 + .../unit/OperatorListConcatenateListsNotMatch.txt | 1 + .../OperatorListConcatenateNotListsButMatch.txt | 1 + .../unit/OperatorListConcatenateRhsNotList.txt | 1 + .../type-errors/unit/OperatorNotEqualNotBool.txt | 1 + dhall/tests/type-errors/unit/OperatorOrNotBool.txt | 1 + .../type-errors/unit/OperatorPlusNotNatural.txt | 1 + .../unit/OperatorTextConcatenateLhsNotText.txt | 1 + .../unit/OperatorTextConcatenateRhsNotText.txt | 1 + .../type-errors/unit/OperatorTimesNotNatural.txt | 1 + .../unit/OptionalDeprecatedSyntaxAbsent.txt | 1 + .../unit/OptionalDeprecatedSyntaxPresent.txt | 1 + .../type-errors/unit/RecordLitDuplicateFields.txt | 1 + dhall/tests/type-errors/unit/RecordMixedKinds3.txt | 1 + .../type-errors/unit/RecordProjectionEmpty.txt | 1 + .../unit/RecordProjectionNotPresent.txt | 1 + .../type-errors/unit/RecordProjectionNotRecord.txt | 1 + .../type-errors/unit/RecordSelectionEmpty.txt | 1 + .../type-errors/unit/RecordSelectionNotPresent.txt | 1 + .../type-errors/unit/RecordSelectionNotRecord.txt | 1 + .../unit/RecordSelectionTypeNotUnionType.txt | 1 + .../type-errors/unit/RecordTypeDuplicateFields.txt | 1 + .../type-errors/unit/RecordTypeValueMember.txt | 1 + .../unit/RecursiveRecordMergeLhsNotRecord.txt | 1 + .../unit/RecursiveRecordMergeOverlapping.txt | 1 + .../unit/RecursiveRecordMergeRhsNotRecord.txt | 1 + .../RecursiveRecordTypeMergeLhsNotRecordType.txt | 1 + .../unit/RecursiveRecordTypeMergeOverlapping.txt | 1 + .../RecursiveRecordTypeMergeRhsNotRecordType.txt | 1 + .../unit/RightBiasedRecordMergeLhsNotRecord.txt | 1 + .../unit/RightBiasedRecordMergeMixedKinds2.txt | 1 + .../unit/RightBiasedRecordMergeMixedKinds3.txt | 1 + .../unit/RightBiasedRecordMergeRhsNotRecord.txt | 1 + dhall/tests/type-errors/unit/SomeNotType.txt | 1 + dhall/tests/type-errors/unit/Sort.txt | 1 + .../unit/TextLiteralInterpolateNotText.txt | 1 + .../tests/type-errors/unit/TypeAnnotationWrong.txt | 1 + .../unit/UnionConstructorFieldNotPresent.txt | 1 + .../unit/UnionDeprecatedConstructorsKeyword.txt | 1 + .../unit/UnionTypeDuplicateVariants1.txt | 1 + .../unit/UnionTypeDuplicateVariants2.txt | 1 + .../tests/type-errors/unit/UnionTypeMixedKinds.txt | 1 + .../type-errors/unit/UnionTypeMixedKinds2.txt | 1 + .../type-errors/unit/UnionTypeMixedKinds3.txt | 1 + dhall/tests/type-errors/unit/UnionTypeNotType.txt | 1 + dhall/tests/type-errors/unit/VariableFree.txt | 1 + 89 files changed, 150 insertions(+), 8 deletions(-) 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 diff --git a/dhall/build.rs b/dhall/build.rs index c7d339c..337480f 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -394,5 +394,34 @@ fn main() -> std::io::Result<()> { }, )?; + make_test_module( + &mut file, + TestFeature { + module_name: "type_error", + directory: spec_tests_dir.join("type-inference/failure/"), + variant: "TypeError", + path_filter: |path: &str| { + false + // TODO: Enable imports in typecheck tests + || path == "importBoundary" + || path == "customHeadersUsingBoundVariable" + // TODO: projection by expression + || path == "unit/RecordProjectionByTypeFieldTypeMismatch" + || path == "unit/RecordProjectionByTypeNotPresent" + // TODO: toMap + || path == "unit/EmptyToMap" + || path == "unit/HeterogenousToMap" + || path == "unit/MistypedToMap1" + || path == "unit/MistypedToMap2" + || path == "unit/MistypedToMap3" + || path == "unit/MistypedToMap4" + || path == "unit/NonRecordToMap" + || path == "unit/ToMapWrongKind" + }, + input_type: FileType::Text, + output_type: None, + }, + )?; + Ok(()) } diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index b98489f..9790b95 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -21,7 +21,7 @@ right: `{}`"#, } use std::fs::File; -use std::io::Read; +use std::io::{Read, Write}; use std::path::PathBuf; use crate::error::{Error, Result}; @@ -40,6 +40,7 @@ pub enum Test<'a> { ImportFailure(&'a str), TypeInferenceSuccess(&'a str, &'a str), TypeInferenceFailure(&'a str), + TypeError(&'a str), Normalization(&'a str, &'a str), AlphaNormalization(&'a str, &'a str), } @@ -144,13 +145,38 @@ pub fn run_test(test: Test<'_>) -> Result<()> { assert_eq_display!(ty, expected); } TypeInferenceFailure(file_path) => { - let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck(); - match res { - Err(_) => {} - // If e did typecheck, check that it doesn't have a type - Ok(e) => { - e.get_type().unwrap_err(); - } + let mut res = + parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + if let Ok(e) = &res { + // If e did typecheck, check that get_type fails + res = e.get_type(); + } + res.unwrap_err(); + } + TypeError(file_path) => { + let mut res = + parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + let file_path = PathBuf::from(file_path); + let error_file_path = file_path + .strip_prefix("../dhall-lang/tests/type-inference/failure/") + .unwrap(); + let error_file_path = + PathBuf::from("tests/type-errors/").join(error_file_path); + let error_file_path = error_file_path.with_extension("txt"); + if let Ok(e) = &res { + // If e did typecheck, check that get_type fails + res = e.get_type(); + } + let err: Error = res.unwrap_err().into(); + + if error_file_path.is_file() { + let expected_msg = std::fs::read_to_string(error_file_path)?; + let msg = format!("{}\n", err); + assert_eq_pretty!(msg, expected_msg); + } else { + std::fs::create_dir_all(error_file_path.parent().unwrap())?; + let mut file = File::create(error_file_path)?; + writeln!(file, "{}", err)?; } } Normalization(expr_file_path, expected_file_path) => { 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/src/error/mod.rs | 61 +++++++--------------- dhall/tests/type-errors/hurkensParadox.txt | 2 +- dhall/tests/type-errors/mixedUnions.txt | 2 +- dhall/tests/type-errors/recordOfKind.txt | 2 +- .../unit/AnnotationRecordWrongFieldName.txt | 2 +- .../unit/AnnotationRecordWrongFieldType.txt | 2 +- dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 2 +- .../type-errors/unit/AssertNotEquivalence.txt | 2 +- .../type-errors/unit/AssertTriviallyFalse.txt | 2 +- .../type-errors/unit/EquivalenceNotSameType.txt | 2 +- .../tests/type-errors/unit/EquivalenceNotTerms.txt | 2 +- .../unit/FunctionApplicationArgumentNotMatch.txt | 2 +- .../unit/FunctionApplicationIsNotFunction.txt | 2 +- .../unit/FunctionArgumentTypeNotAType.txt | 2 +- .../unit/FunctionTypeArgumentTypeNotAType.txt | 2 +- .../type-errors/unit/FunctionTypeKindSort.txt | 2 +- .../type-errors/unit/FunctionTypeTypeSort.txt | 2 +- .../tests/type-errors/unit/IfBranchesNotMatch.txt | 2 +- dhall/tests/type-errors/unit/IfBranchesNotType.txt | 2 +- dhall/tests/type-errors/unit/IfNotBool.txt | 2 +- .../type-errors/unit/LetWithWrongAnnotation.txt | 2 +- .../type-errors/unit/ListLiteralEmptyNotType.txt | 2 +- .../tests/type-errors/unit/ListLiteralNotType.txt | 2 +- .../type-errors/unit/ListLiteralTypesNotMatch.txt | 2 +- .../unit/MergeAlternativeHasNoHandler.txt | 2 +- .../type-errors/unit/MergeAnnotationMismatch.txt | 2 +- .../type-errors/unit/MergeAnnotationNotType.txt | 2 +- .../unit/MergeEmptyNeedsDirectAnnotation1.txt | 2 +- .../unit/MergeEmptyNeedsDirectAnnotation2.txt | 2 +- .../unit/MergeEmptyWithoutAnnotation.txt | 2 +- .../tests/type-errors/unit/MergeHandlerFreeVar.txt | 2 +- .../type-errors/unit/MergeHandlerNotFunction.txt | 2 +- .../type-errors/unit/MergeHandlerNotInUnion.txt | 2 +- .../unit/MergeHandlerNotMatchAlternativeType.txt | 2 +- .../unit/MergeHandlersWithDifferentType.txt | 2 +- dhall/tests/type-errors/unit/MergeLhsNotRecord.txt | 2 +- .../type-errors/unit/MergeMissingHandler1.txt | 2 +- .../type-errors/unit/MergeMissingHandler2.txt | 2 +- dhall/tests/type-errors/unit/MergeRhsNotUnion.txt | 2 +- .../type-errors/unit/NaturalSubtractNotNatural.txt | 2 +- .../tests/type-errors/unit/OperatorAndNotBool.txt | 2 +- .../type-errors/unit/OperatorEqualNotBool.txt | 2 +- .../unit/OperatorListConcatenateLhsNotList.txt | 2 +- .../unit/OperatorListConcatenateListsNotMatch.txt | 2 +- .../OperatorListConcatenateNotListsButMatch.txt | 2 +- .../unit/OperatorListConcatenateRhsNotList.txt | 2 +- .../type-errors/unit/OperatorNotEqualNotBool.txt | 2 +- dhall/tests/type-errors/unit/OperatorOrNotBool.txt | 2 +- .../type-errors/unit/OperatorPlusNotNatural.txt | 2 +- .../unit/OperatorTextConcatenateLhsNotText.txt | 2 +- .../unit/OperatorTextConcatenateRhsNotText.txt | 2 +- .../type-errors/unit/OperatorTimesNotNatural.txt | 2 +- .../unit/OptionalDeprecatedSyntaxAbsent.txt | 2 +- .../unit/OptionalDeprecatedSyntaxPresent.txt | 2 +- .../type-errors/unit/RecordLitDuplicateFields.txt | 2 +- dhall/tests/type-errors/unit/RecordMixedKinds3.txt | 2 +- .../type-errors/unit/RecordProjectionEmpty.txt | 2 +- .../unit/RecordProjectionNotPresent.txt | 2 +- .../type-errors/unit/RecordProjectionNotRecord.txt | 2 +- .../type-errors/unit/RecordSelectionEmpty.txt | 2 +- .../type-errors/unit/RecordSelectionNotPresent.txt | 2 +- .../type-errors/unit/RecordSelectionNotRecord.txt | 2 +- .../unit/RecordSelectionTypeNotUnionType.txt | 2 +- .../type-errors/unit/RecordTypeDuplicateFields.txt | 2 +- .../type-errors/unit/RecordTypeValueMember.txt | 2 +- .../unit/RecursiveRecordMergeLhsNotRecord.txt | 2 +- .../unit/RecursiveRecordMergeOverlapping.txt | 2 +- .../unit/RecursiveRecordMergeRhsNotRecord.txt | 2 +- .../RecursiveRecordTypeMergeLhsNotRecordType.txt | 2 +- .../unit/RecursiveRecordTypeMergeOverlapping.txt | 2 +- .../RecursiveRecordTypeMergeRhsNotRecordType.txt | 2 +- .../unit/RightBiasedRecordMergeLhsNotRecord.txt | 2 +- .../unit/RightBiasedRecordMergeMixedKinds2.txt | 2 +- .../unit/RightBiasedRecordMergeMixedKinds3.txt | 2 +- .../unit/RightBiasedRecordMergeRhsNotRecord.txt | 2 +- dhall/tests/type-errors/unit/SomeNotType.txt | 2 +- dhall/tests/type-errors/unit/Sort.txt | 2 +- .../unit/TextLiteralInterpolateNotText.txt | 2 +- .../tests/type-errors/unit/TypeAnnotationWrong.txt | 2 +- .../unit/UnionConstructorFieldNotPresent.txt | 2 +- .../unit/UnionDeprecatedConstructorsKeyword.txt | 2 +- .../unit/UnionTypeDuplicateVariants1.txt | 2 +- .../unit/UnionTypeDuplicateVariants2.txt | 2 +- .../tests/type-errors/unit/UnionTypeMixedKinds.txt | 2 +- .../type-errors/unit/UnionTypeMixedKinds2.txt | 2 +- .../type-errors/unit/UnionTypeMixedKinds3.txt | 2 +- dhall/tests/type-errors/unit/UnionTypeNotType.txt | 2 +- dhall/tests/type-errors/unit/VariableFree.txt | 2 +- 88 files changed, 105 insertions(+), 130 deletions(-) diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 6d4e120..5338e2d 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -41,7 +41,7 @@ pub enum EncodeError { /// A structured type error that includes context #[derive(Debug)] pub struct TypeError { - type_message: TypeMessage, + message: TypeMessage, context: TypecheckContext, } @@ -90,58 +90,33 @@ pub(crate) enum TypeMessage { impl TypeError { pub(crate) fn new( context: &TypecheckContext, - type_message: TypeMessage, + message: TypeMessage, ) -> Self { TypeError { context: context.clone(), - type_message, + message, } } } -impl std::error::Error for TypeMessage { - fn description(&self) -> &str { +impl std::fmt::Display for TypeError { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { use TypeMessage::*; - match *self { - // UnboundVariable => "Unbound variable", - InvalidInputType(_) => "Invalid function input", - InvalidOutputType(_) => "Invalid function output", - NotAFunction(_) => "Not a function", - TypeMismatch(_, _, _) => "Wrong type of function argument", - _ => "Unhandled error", - } + let msg = match self.message { + UnboundVariable(_) => "Unbound variable".to_string(), + InvalidInputType(_) => "Invalid function input".to_string(), + InvalidOutputType(_) => "Invalid function output".to_string(), + NotAFunction(_) => "Not a function".to_string(), + TypeMismatch(_, _, _) => { + "Wrong type of function argument".to_string() + } + _ => "Unhandled error".to_string(), + }; + write!(f, "{}", msg) } } -impl std::fmt::Display for TypeMessage { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - match self { - // UnboundVariable(_) => { - // f.write_str(include_str!("errors/UnboundVariable.txt")) - // } - // TypeMismatch(e0, e1, e2) => { - // let template = include_str!("errors/TypeMismatch.txt"); - // let s = template - // .replace("$txt0", &format!("{}", e0.as_expr())) - // .replace("$txt1", &format!("{}", e1.as_expr())) - // .replace("$txt2", &format!("{}", e2.as_expr())) - // .replace( - // "$txt3", - // &format!( - // "{}", - // e2.get_type() - // .unwrap() - // .as_normalized() - // .unwrap() - // .as_expr() - // ), - // ); - // f.write_str(&s) - // } - _ => f.write_str("Unhandled error message"), - } - } -} +impl std::error::Error for TypeError {} impl std::fmt::Display for Error { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -151,7 +126,7 @@ impl std::fmt::Display for Error { Error::Decode(err) => write!(f, "{:?}", err), Error::Encode(err) => write!(f, "{:?}", err), Error::Resolve(err) => write!(f, "{:?}", err), - Error::Typecheck(err) => write!(f, "{:?}", err), + Error::Typecheck(err) => write!(f, "Type error: {}", err), } } } 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 0e4f4c5af67b4075174ace5a1c7800dae60a9d11 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 10:52:57 +0000 Subject: Move Span definition to its own file And prepare for more variants --- dhall_syntax/src/core/expr.rs | 35 ---------------------------------- dhall_syntax/src/core/mod.rs | 2 ++ dhall_syntax/src/core/span.rs | 44 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 46 insertions(+), 35 deletions(-) create mode 100644 dhall_syntax/src/core/span.rs diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs index 2ad3ba8..70ce1dc 100644 --- a/dhall_syntax/src/core/expr.rs +++ b/dhall_syntax/src/core/expr.rs @@ -1,4 +1,3 @@ -use std::rc::Rc; use crate::map::{DupTreeMap, DupTreeSet}; use crate::visitor::{self, ExprFMutVisitor, ExprFVisitor}; @@ -15,40 +14,6 @@ pub fn trivial_result(x: Result) -> T { } } -/// A location in the source text -#[derive(Debug, Clone)] -pub struct Span { - input: Rc, - /// # Safety - /// - /// Must be a valid character boundary index into `input`. - start: usize, - /// # Safety - /// - /// Must be a valid character boundary index into `input`. - end: usize, -} - -impl Span { - pub(crate) fn make(input: Rc, sp: pest::Span) -> Self { - Span { - input, - start: sp.start(), - end: sp.end(), - } - } - /// Takes the union of the two spans. Assumes that the spans come from the same input. - /// This will also capture any input between the spans. - pub fn union(&self, other: &Span) -> Self { - use std::cmp::{max, min}; - Span { - input: self.input.clone(), - start: min(self.start, other.start), - end: max(self.start, other.start), - } - } -} - /// Double with bitwise equality #[derive(Debug, Copy, Clone)] pub struct NaiveDouble(f64); diff --git a/dhall_syntax/src/core/mod.rs b/dhall_syntax/src/core/mod.rs index fe2c0be..66bf229 100644 --- a/dhall_syntax/src/core/mod.rs +++ b/dhall_syntax/src/core/mod.rs @@ -4,6 +4,8 @@ mod import; pub use import::*; mod label; pub use label::*; +mod span; +pub use span::*; mod text; pub use text::*; pub mod context; diff --git a/dhall_syntax/src/core/span.rs b/dhall_syntax/src/core/span.rs new file mode 100644 index 0000000..ad5a3a9 --- /dev/null +++ b/dhall_syntax/src/core/span.rs @@ -0,0 +1,44 @@ +use std::rc::Rc; + +/// A location in the source text +#[derive(Debug, Clone)] +pub struct ParsedSpan { + input: Rc, + /// # Safety + /// + /// Must be a valid character boundary index into `input`. + start: usize, + /// # Safety + /// + /// Must be a valid character boundary index into `input`. + end: usize, +} + +/// A location in the source text +#[derive(Debug, Clone)] +pub enum Span { + Parsed(ParsedSpan), +} + +impl Span { + pub(crate) fn make(input: Rc, sp: pest::Span) -> Self { + Span::Parsed(ParsedSpan { + input, + start: sp.start(), + end: sp.end(), + }) + } + /// Takes the union of the two spans. Assumes that the spans come from the same input. + /// This will also capture any input between the spans. + pub fn union(&self, other: &Span) -> Self { + use std::cmp::{max, min}; + use Span::*; + match (self, other) { + (Parsed(x), Parsed(y)) => Span::Parsed(ParsedSpan { + input: x.input.clone(), + start: min(x.start, y.start), + end: max(x.start, y.start), + }), + } + } +} -- cgit v1.2.3 From a8cb6926cbafb2ac806f7bec27a29b0528ed5056 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 10:53:29 +0000 Subject: Fix typo --- dhall_syntax/src/core/span.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dhall_syntax/src/core/span.rs b/dhall_syntax/src/core/span.rs index ad5a3a9..f0eb89a 100644 --- a/dhall_syntax/src/core/span.rs +++ b/dhall_syntax/src/core/span.rs @@ -37,7 +37,7 @@ impl Span { (Parsed(x), Parsed(y)) => Span::Parsed(ParsedSpan { input: x.input.clone(), start: min(x.start, y.start), - end: max(x.start, y.start), + end: max(x.end, y.end), }), } } -- cgit v1.2.3 From b68c3af578d1f6b0d1e32e7d88ef57774fb468d8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 11:20:32 +0000 Subject: Capture absence of span in Span itself --- dhall/src/core/valuef.rs | 3 ++- dhall/src/phase/binary.rs | 10 ++++++++-- dhall/src/phase/typecheck.rs | 6 +++++- dhall_syntax/src/core/expr.rs | 18 ++++-------------- dhall_syntax/src/core/span.rs | 13 +++++++++++-- dhall_syntax/src/parser.rs | 14 +++++--------- 6 files changed, 35 insertions(+), 29 deletions(-) diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 4e457e6..e5d0807 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -1,12 +1,13 @@ use std::collections::HashMap; use dhall_syntax::{ - rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, + Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, }; use crate::core::value::{ToExprOptions, Value}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::phase::typecheck::rc; use crate::phase::{Normalized, NormalizedExpr}; /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index 8c98f77..b4f18da 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -5,8 +5,9 @@ use std::vec; use dhall_syntax::map::DupTreeMap; use dhall_syntax::{ - rc, Expr, ExprF, FilePath, FilePrefix, Hash, Import, ImportLocation, - ImportMode, Integer, InterpolatedText, Label, Natural, Scheme, URL, V, + Expr, ExprF, FilePath, FilePrefix, Hash, Import, ImportLocation, + ImportMode, Integer, InterpolatedText, Label, Natural, RawExpr, Scheme, + Span, URL, V, }; use crate::error::{DecodeError, EncodeError}; @@ -24,6 +25,11 @@ pub(crate) fn encode(expr: &Expr) -> Result, EncodeError> { .map_err(|e| EncodeError::CBORError(e)) } +// Should probably rename this +pub fn rc(x: RawExpr) -> Expr { + Expr::new(x, Span::Decoded) +} + fn cbor_value_to_dhall(data: &cbor::Value) -> Result { use cbor::Value::*; use dhall_syntax::{BinOp, Builtin, Const}; diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 9013c1f..4d8c7d3 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -2,7 +2,7 @@ use std::cmp::max; use std::collections::HashMap; use dhall_syntax::{ - rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, + Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span, }; use crate::core::context::TypecheckContext; @@ -142,6 +142,10 @@ pub(crate) fn const_to_value(c: Const) -> Value { } } +pub fn rc(x: RawExpr) -> Expr { + Expr::new(x, Span::Artificial) +} + // Ad-hoc macro to help construct the types of builtins macro_rules! make_type { (Type) => { ExprF::Const(Const::Type) }; diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs index 70ce1dc..750b58b 100644 --- a/dhall_syntax/src/core/expr.rs +++ b/dhall_syntax/src/core/expr.rs @@ -1,4 +1,3 @@ - use crate::map::{DupTreeMap, DupTreeSet}; use crate::visitor::{self, ExprFMutVisitor, ExprFVisitor}; use crate::*; @@ -143,7 +142,7 @@ pub enum Builtin { // Each node carries an annotation. #[derive(Debug, Clone)] -pub struct Expr(Box<(RawExpr, Option)>); +pub struct Expr(Box<(RawExpr, Span)>); pub type RawExpr = ExprF, Embed>; @@ -299,16 +298,12 @@ impl Expr { pub fn as_mut(&mut self) -> &mut RawExpr { &mut self.0.as_mut().0 } - pub fn span(&self) -> Option { + pub fn span(&self) -> Span { self.0.as_ref().1.clone() } - pub(crate) fn new(x: RawExpr, n: Span) -> Self { - Expr(Box::new((x, Some(n)))) - } - - pub fn from_expr_no_span(x: RawExpr) -> Self { - Expr(Box::new((x, None))) + pub fn new(x: RawExpr, n: Span) -> Self { + Expr(Box::new((x, n))) } pub fn rewrap(&self, x: RawExpr) -> Expr { @@ -353,11 +348,6 @@ impl Expr { } } -// Should probably rename this -pub fn rc(x: RawExpr) -> Expr { - Expr::from_expr_no_span(x) -} - /// Add an isize to an usize /// Panics on over/underflow fn add_ui(u: usize, i: isize) -> Option { diff --git a/dhall_syntax/src/core/span.rs b/dhall_syntax/src/core/span.rs index f0eb89a..fc8de6e 100644 --- a/dhall_syntax/src/core/span.rs +++ b/dhall_syntax/src/core/span.rs @@ -14,10 +14,14 @@ pub struct ParsedSpan { end: usize, } -/// A location in the source text #[derive(Debug, Clone)] pub enum Span { + /// A location in the source text Parsed(ParsedSpan), + /// For expressions obtained from decoding binary + Decoded, + /// For expressions constructed during normalization/typecheck + Artificial, } impl Span { @@ -28,17 +32,22 @@ impl Span { end: sp.end(), }) } + /// Takes the union of the two spans. Assumes that the spans come from the same input. /// This will also capture any input between the spans. pub fn union(&self, other: &Span) -> Self { use std::cmp::{max, min}; use Span::*; match (self, other) { - (Parsed(x), Parsed(y)) => Span::Parsed(ParsedSpan { + (Parsed(x), Parsed(y)) => Parsed(ParsedSpan { input: x.input.clone(), start: min(x.start, y.start), end: max(x.end, y.end), }), + _ => panic!( + "Tried to union incompatible spans: {:?} and {:?}", + self, other + ), } } } diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs index 83f62ee..eaded50 100644 --- a/dhall_syntax/src/parser.rs +++ b/dhall_syntax/src/parser.rs @@ -650,7 +650,7 @@ impl DhallParser { final_expr, |acc, x| { spanned_union( - acc.span().unwrap(), + acc.span(), x.3, Let(x.0, x.1, x.2, acc) ) @@ -717,11 +717,7 @@ impl DhallParser { r => Err(op.error(format!("Rule {:?} isn't an operator", r)))?, }; - Ok(spanned_union( - l.span().unwrap(), - r.span().unwrap(), - BinOp(op, l, r), - )) + Ok(spanned_union(l.span(), r.span(), BinOp(op, l, r))) } fn Some_(_input: ParseInput) -> ParseResult<()> { @@ -739,8 +735,8 @@ impl DhallParser { first, |acc, e| { spanned_union( - acc.span().unwrap(), - e.span().unwrap(), + acc.span(), + e.span(), App(acc, e) ) } @@ -778,7 +774,7 @@ impl DhallParser { first, |acc, e| { spanned_union( - acc.span().unwrap(), + acc.span(), e.1, match e.0 { Either::Left(l) => Field(acc, l), -- cgit v1.2.3 From 5d5a356b8eb36e277c312e5550d1cb0a2f82e9fa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 11:34:29 +0000 Subject: Store a `Span` in `Value` --- dhall/src/core/value.rs | 23 +++++++++++++++++++---- dhall/src/phase/typecheck.rs | 14 ++++++++++---- dhall_syntax/src/core/span.rs | 3 +++ 3 files changed, 32 insertions(+), 8 deletions(-) diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index b4b6b08..b6c156e 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -1,7 +1,7 @@ use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; -use dhall_syntax::{Builtin, Const}; +use dhall_syntax::{Builtin, Const, Span}; use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; @@ -36,6 +36,7 @@ struct ValueInternal { value: ValueF, /// This is None if and only if `value` is `Sort` (which doesn't have a type) ty: Option, + span: Span, } /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, @@ -69,18 +70,21 @@ impl ValueInternal { form: Unevaled, value: ValueF::Const(Const::Type), ty: None, + span: Span::Artificial, }, |vint| match (&vint.form, &vint.ty) { (Unevaled, Some(ty)) => ValueInternal { form: WHNF, value: normalize_whnf(vint.value, &ty), ty: vint.ty, + span: vint.span, }, // `value` is `Sort` (Unevaled, None) => ValueInternal { form: NF, value: ValueF::Const(Const::Sort), ty: None, + span: vint.span, }, // Already in WHNF (WHNF, _) | (NF, _) => vint, @@ -113,11 +117,12 @@ impl ValueInternal { } impl Value { - fn new(value: ValueF, form: Form, ty: Value) -> Value { + fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value { ValueInternal { form, value, ty: Some(ty), + span, } .into_value() } @@ -126,14 +131,22 @@ impl Value { form: NF, value: ValueF::Const(Const::Sort), ty: None, + span: Span::Artificial, } .into_value() } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { - Value::new(v, Unevaled, t) + Value::new(v, Unevaled, t, Span::PlaceHolder) + } + pub(crate) fn from_valuef_and_type_and_span( + v: ValueF, + t: Value, + span: Span, + ) -> Value { + Value::new(v, Unevaled, t, span) } pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value { - Value::new(v, WHNF, t) + Value::new(v, WHNF, t, Span::PlaceHolder) } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) @@ -258,6 +271,7 @@ impl Shift for ValueInternal { form: self.form, value: self.value.shift(delta, var)?, ty: self.ty.shift(delta, var)?, + span: self.span.clone(), }) } } @@ -285,6 +299,7 @@ impl Subst for ValueInternal { form: Unevaled, value: self.value.subst_shift(var, val), ty: self.ty.subst_shift(var, val), + span: self.span.clone(), } } } diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 4d8c7d3..63f5157 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -304,6 +304,7 @@ fn type_with( e: Expr, ) -> Result { use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; + let span = e.span(); Ok(match e.as_ref() { Lam(var, annot, body) => { @@ -348,7 +349,7 @@ fn type_with( |e| type_with(ctx, e.clone()), |_, _| unreachable!(), )?; - type_last_layer(ctx, expr)? + type_last_layer(ctx, expr, span)? } }) } @@ -358,6 +359,7 @@ fn type_with( fn type_last_layer( ctx: &TypecheckContext, e: ExprF, + span: Span, ) -> Result { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; @@ -584,6 +586,7 @@ fn type_last_layer( l.get_type()?, r.get_type()?, ), + Span::PlaceHolder, )?), BinOp(RecursiveRecordTypeMerge, l, r) => { use crate::phase::normalize::merge_maps; @@ -619,6 +622,7 @@ fn type_last_layer( l.clone(), r.clone(), ), + Span::PlaceHolder, ) }, )?; @@ -786,9 +790,11 @@ fn type_last_layer( }; Ok(match ret { - RetTypeOnly(typ) => { - Value::from_valuef_and_type(ValueF::PartialExpr(e), typ) - } + RetTypeOnly(typ) => Value::from_valuef_and_type_and_span( + ValueF::PartialExpr(e), + typ, + span, + ), RetWhole(v) => v, }) } diff --git a/dhall_syntax/src/core/span.rs b/dhall_syntax/src/core/span.rs index fc8de6e..fa89c30 100644 --- a/dhall_syntax/src/core/span.rs +++ b/dhall_syntax/src/core/span.rs @@ -22,6 +22,9 @@ pub enum Span { Decoded, /// For expressions constructed during normalization/typecheck Artificial, + /// For when there should be a span but it's not done yet + /// TODO: properly handle spans + PlaceHolder, } impl Span { -- 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/src/error/mod.rs | 8 +++---- dhall/src/phase/typecheck.rs | 2 +- dhall/src/tests.rs | 25 +++++++++++++++++++++- dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 7 +++++- .../unit/UnionDeprecatedConstructorsKeyword.txt | 7 +++++- dhall/tests/type-errors/unit/VariableFree.txt | 7 +++++- dhall_syntax/src/core/span.rs | 14 ++++++++++++ 7 files changed, 61 insertions(+), 9 deletions(-) diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 5338e2d..efbd578 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -1,6 +1,6 @@ use std::io::Error as IOError; -use dhall_syntax::{BinOp, Import, Label, ParseError, V}; +use dhall_syntax::{BinOp, Import, Label, ParseError, Span}; use crate::core::context::TypecheckContext; use crate::core::value::Value; @@ -48,7 +48,7 @@ pub struct TypeError { /// The specific type error #[derive(Debug)] pub(crate) enum TypeMessage { - UnboundVariable(V