summaryrefslogtreecommitdiff
path: root/dhall/tests
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/tests')
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt2
-rw-r--r--dhall/tests/type-errors/mixedUnions.txt2
-rw-r--r--dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt2
-rw-r--r--dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt2
-rw-r--r--dhall/tests/type-errors/unit/AssertAlphaTrap.txt7
-rw-r--r--dhall/tests/type-errors/unit/EquivalenceNotTerms.txt2
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt2
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt2
-rw-r--r--dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt7
-rw-r--r--dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt7
-rw-r--r--dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt2
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt2
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt22
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt66
-rw-r--r--dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt2
-rw-r--r--dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt2
-rw-r--r--dhall/tests/type-errors/unit/RecordTypeValueMember.txt2
-rw-r--r--dhall/tests/type-errors/unit/TypeAnnotationWrong.txt2
-rw-r--r--dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt7
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt2
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt2
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt2
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeNotType.txt2
-rw-r--r--dhall/tests/type-errors/unit/VariableFree.txt7
25 files changed, 108 insertions, 50 deletions
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 9342fd8..4dfdcf5 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1 +1 @@
-Type error: Unhandled error: TypeMismatch
+Type error: Unhandled error: function annot mismatch: (U : Sort) : Kind
diff --git a/dhall/tests/type-errors/mixedUnions.txt b/dhall/tests/type-errors/mixedUnions.txt
index 30fcdf8..fd4de70 100644
--- a/dhall/tests/type-errors/mixedUnions.txt
+++ b/dhall/tests/type-errors/mixedUnions.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("Right"), Type)
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
index 045eb98..946b296 100644
--- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch
+Type error: Unhandled error: annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural }
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
index 045eb98..89817db 100644
--- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch
+Type error: Unhandled error: annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text }
diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
index 2969c18..87cf48e 100644
--- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
+++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
@@ -1,6 +1 @@
- --> 1:47
- |
-1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)␊
- | ^
- |
- = Type error: Unbound variable
+Type error: Unhandled error: unbound variable
diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
index 7c48d6f..de11e28 100644
--- a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
+++ b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
@@ -1 +1 @@
-Type error: Unhandled error: EquivalenceArgumentMustBeTerm
+Type error: Unhandled error: EquivalenceArgumentsMustBeTerms
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
index 9342fd8..8d101c3 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1 +1 @@
-Type error: Unhandled error: TypeMismatch
+Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
index f1cdf92..13b0819 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -1 +1 @@
-Type error: Unhandled error: NotAFunction
+Type error: Unhandled error: apply to not Pi: AppliedBuiltin(Bool, [], [], NzEnv { items: [] })
diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
index 9e43c33..a13fb3a 100644
--- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
+++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
@@ -1,6 +1 @@
- --> 1:7
- |
-1 | λ(_ : 1) → _␊
- | ^
- |
- = Type error: Invalid function input
+[unknown location] Type error: Invalid function input
diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
index dd2e758..a13fb3a 100644
--- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
+++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -1,6 +1 @@
- --> 1:1
- |
-1 | 2 → _␊
- | ^
- |
- = Type error: Invalid function input
+[unknown location] Type error: Invalid function input
diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
index 045eb98..cae4fea 100644
--- a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
+++ b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch
+Type error: Unhandled error: annot mismatch: (True : Bool) : Natural
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
index 9342fd8..070e461 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1 +1 @@
-Type error: Unhandled error: TypeMismatch
+Type error: Unhandled error: function annot mismatch: (Type : Kind) : Type
diff --git a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt
deleted file mode 100644
index de9e256..0000000
--- a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt
+++ /dev/null
@@ -1 +0,0 @@
-Type error: Unhandled error: MergeHandlerReturnTypeMustNotBeDependent
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
index 9342fd8..77fed39 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -1 +1,21 @@
-Type error: Unhandled error: TypeMismatch
+Type error: Unhandled error: MergeHandlerTypeMismatch: Value@WHNF {
+ value: AppliedBuiltin(
+ Natural,
+ [],
+ [],
+ NzEnv {
+ items: [],
+ },
+ ),
+ type: Type,
+} != Value@WHNF {
+ value: AppliedBuiltin(
+ Bool,
+ [],
+ [],
+ NzEnv {
+ items: [],
+ },
+ ),
+ type: Type,
+}
diff --git a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
index 8b729a4..02d2970 100644
--- a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
@@ -1 +1,65 @@
-Type error: Unhandled error: MergeHandlerTypeMismatch
+Type error: Unhandled error: MergeHandlerTypeMismatch: Value@WHNF {
+ value: AppliedBuiltin(
+ Bool,
+ [],
+ [],
+ NzEnv {
+ items: [
+ Replaced(
+ Value@Unevaled {
+ value: Var(
+ AlphaVar(0),
+ Fresh(
+ 119,
+ ),
+ ),
+ type: Value@WHNF {
+ value: AppliedBuiltin(
+ Bool,
+ [],
+ [],
+ NzEnv {
+ items: [],
+ },
+ ),
+ type: Type,
+ },
+ },
+ ),
+ ],
+ },
+ ),
+ type: Type,
+} != Value@WHNF {
+ value: AppliedBuiltin(
+ Natural,
+ [],
+ [],
+ NzEnv {
+ items: [
+ Replaced(
+ Value@Unevaled {
+ value: Var(
+ AlphaVar(0),
+ Fresh(
+ 120,
+ ),
+ ),
+ type: Value@WHNF {
+ value: AppliedBuiltin(
+ Natural,
+ [],
+ [],
+ NzEnv {
+ items: [],
+ },
+ ),
+ type: Type,
+ },
+ },
+ ),
+ ],
+ },
+ ),
+ type: Type,
+}
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
index 9342fd8..8d101c3 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1 +1 @@
-Type error: Unhandled error: TypeMismatch
+Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
index 045eb98..91d7fb0 100644
--- a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
+++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch
+Type error: Unhandled error: annot mismatch: ([1] : List Natural) : Optional Natural
diff --git a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
index ed3fd6a..fd4de70 100644
--- a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
+++ b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
index 045eb98..52fc94d 100644
--- a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
+++ b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch
+Type error: Unhandled error: annot mismatch: (1 : Natural) : Bool
diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
index 9cc0c19..87cf48e 100644
--- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
+++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
@@ -1,6 +1 @@
- --> 1:1
- |
-1 | constructors < Left : Natural | Right : Bool >␊
- | ^----------^
- |
- = Type error: Unbound variable
+Type error: Unhandled error: unbound variable
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
index 07604ba..fd4de70 100644
--- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("y"), Type)
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
index 07604ba..fd4de70 100644
--- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("y"), Type)
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
index ded0e5c..fd4de70 100644
--- a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("y"), Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/UnionTypeNotType.txt b/dhall/tests/type-errors/unit/UnionTypeNotType.txt
index ed3fd6a..fd4de70 100644
--- a/dhall/tests/type-errors/unit/UnionTypeNotType.txt
+++ b/dhall/tests/type-errors/unit/UnionTypeNotType.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: InvalidFieldType
diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt
index a46aac0..87cf48e 100644
--- a/dhall/tests/type-errors/unit/VariableFree.txt
+++ b/dhall/tests/type-errors/unit/VariableFree.txt
@@ -1,6 +1 @@
- --> 1:1
- |
-1 | x␊
- | ^
- |
- = Type error: Unbound variable
+Type error: Unhandled error: unbound variable