summaryrefslogtreecommitdiff
path: root/dhall/tests
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/tests/import/failure/cycle.txt2
-rw-r--r--dhall/tests/import/failure/importBoundary.txt8
-rw-r--r--dhall/tests/type-inference/failure/SortInLet.txt7
-rw-r--r--dhall/tests/type-inference/failure/hurkensParadox.txt8
-rw-r--r--dhall/tests/type-inference/failure/recordOfKind.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt5
-rw-r--r--dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt5
-rw-r--r--dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt5
-rw-r--r--dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt5
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/Sort.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt4
26 files changed, 103 insertions, 37 deletions
diff --git a/dhall/tests/import/failure/cycle.txt b/dhall/tests/import/failure/cycle.txt
index 0a20503..4e9488e 100644
--- a/dhall/tests/import/failure/cycle.txt
+++ b/dhall/tests/import/failure/cycle.txt
@@ -1 +1 @@
-Recursive(Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "cycle.dhall"] }), hash: None }, Resolve(Recursive(Import { mode: Code, location: Local(Parent, FilePath { file_path: ["failure", "cycle.dhall"] }), hash: None }, Resolve(ImportCycle([Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "cycle.dhall"] }), hash: None }, Import { mode: Code, location: Local(Parent, FilePath { file_path: ["failure", "cycle.dhall"] }), hash: None }], Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "cycle.dhall"] }), hash: None })))))
+ImportCycle([Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "cycle.dhall"] }), hash: None }, Import { mode: Code, location: Local(Parent, FilePath { file_path: ["failure", "cycle.dhall"] }), hash: None }], Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "cycle.dhall"] }), hash: None })
diff --git a/dhall/tests/import/failure/importBoundary.txt b/dhall/tests/import/failure/importBoundary.txt
index 8f78e48..6f0615d 100644
--- a/dhall/tests/import/failure/importBoundary.txt
+++ b/dhall/tests/import/failure/importBoundary.txt
@@ -1 +1,7 @@
-Recursive(Import { mode: Code, location: Local(Parent, FilePath { file_path: ["data", "importBoundary.dhall"] }), hash: None }, Typecheck(TypeError { message: Custom("error: unbound variable `x`\n --> <current file>:1:0\n |\n...\n3 | x\n | ^ not found in this scope\n |") }))
+Type error: error: unbound variable `x`
+ --> <current file>:1:0
+ |
+...
+3 | x
+ | ^ not found in this scope
+ |
diff --git a/dhall/tests/type-inference/failure/SortInLet.txt b/dhall/tests/type-inference/failure/SortInLet.txt
index 5b88ff7..19bd26d 100644
--- a/dhall/tests/type-inference/failure/SortInLet.txt
+++ b/dhall/tests/type-inference/failure/SortInLet.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:8
+ |
+1 | let x = Sort in 0
+ | ^^^^ Sort does not have a type
+ |
diff --git a/dhall/tests/type-inference/failure/hurkensParadox.txt b/dhall/tests/type-inference/failure/hurkensParadox.txt
index 6b99615..5aacb80 100644
--- a/dhall/tests/type-inference/failure/hurkensParadox.txt
+++ b/dhall/tests/type-inference/failure/hurkensParadox.txt
@@ -1,15 +1,15 @@
Type error: error: wrong type of function argument
- --> <current file>:6:23
+ --> <current file>:6:15
|
1 | let bottom : Type = ∀(any : Type) → any
2 |
3 | in let not : Type → Type = λ(p : Type) → p → bottom
4 |
...
+ 9 | in let tau
10 | : pow (pow U) → U
-11 | = λ(t : pow (pow U))
- | ^^^ this expects an argument of type: Kind
- | ^ but this has type: Sort
+ | ^^^ this expects an argument of type: Kind
+ | ^ but this has type: Sort
|
= note: expected type `Kind`
found type `Sort`
diff --git a/dhall/tests/type-inference/failure/recordOfKind.txt b/dhall/tests/type-inference/failure/recordOfKind.txt
index 5b88ff7..653fe0b 100644
--- a/dhall/tests/type-inference/failure/recordOfKind.txt
+++ b/dhall/tests/type-inference/failure/recordOfKind.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+ |
+1 | { a = Kind }
+ | ^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
index 2a754fc..a39a0fb 100644
--- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
+++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural }
+Type error: error: annot mismatch: { x : Natural } != { y : Natural }
--> <current file>:1:0
|
1 | { x = 1 } : { y : Natural }
- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ({ x = 1 } : { x : Natural }) : { y : Natural }
+ | ^^^^^^^^^ annot mismatch: { x : Natural } != { y : Natural }
|
diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
index e67edb8..9ecc2a4 100644
--- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
+++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text }
+Type error: error: annot mismatch: { x : Natural } != { x : Text }
--> <current file>:1:0
|
1 | { x = 1 } : { x : Text }
- | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ({ x = 1 } : { x : Natural }) : { x : Text }
+ | ^^^^^^^^^ annot mismatch: { x : Natural } != { x : Text }
|
diff --git a/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt b/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
index d0a9a01..7a4a12c 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionMissingRequiredField.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural } != { id : Optional Natural, name : Text }
--> <current file>:1:4
|
...
6 | in Example::{=}
- | ^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural }) : { id : Optional Natural, name : Text }
+ | ^^^^^^^^^^^^ annot mismatch: { id : Optional Natural } != { id : Optional Natural, name : Text }
|
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
index d4639e9..9235ed4 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongDefaultType.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
--> <current file>:1:4
|
...
6 | in Example::{=}
- | ^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ {=} : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+ | ^^^^^^^^^^^^ annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
|
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
index 0839742..6a6cd1e 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongFieldName.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ { nam = "John Doe" } : { id : Optional Natural, nam : Text, name : Text }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural, nam : Text, name : Text } != { id : Optional Natural, name : Text }
--> <current file>:1:4
|
...
6 | in Example::{ nam = "John Doe" }
- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ { nam = "John Doe" } : { id : Optional Natural, nam : Text, name : Text }) : { id : Optional Natural, name : Text }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { id : Optional Natural, nam : Text, name : Text } != { id : Optional Natural, name : Text }
|
diff --git a/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt b/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
index 7edef95..b4fe726 100644
--- a/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
+++ b/dhall/tests/type-inference/failure/unit/CompletionWithWrongOverridenType.txt
@@ -1,7 +1,7 @@
-Type error: error: annot mismatch: (Example.default ⫽ { name = True } : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+Type error: error: annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
--> <current file>:1:4
|
...
6 | in Example::{ name = True }
- | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: (Example.default ⫽ { name = True } : { id : Optional Natural, name : Bool }) : { id : Optional Natural, name : Text }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { id : Optional Natural, name : Bool } != { id : Optional Natural, name : Text }
|
diff --git a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
index e84eb15..ca5bbcd 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
@@ -1,7 +1,7 @@
-Type error: error: Invalid input type: `Natural`
+Type error: error: Expected a type, found: `1`
--> <current file>:1:6
|
1 | λ(_ : 1) → _
| ^ this has type: `Natural`
|
- = help: The input type of a function must have type `Type`, `Kind` or `Sort`
+ = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
index 4aa0f4f..168ebb9 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -1,7 +1,7 @@
-Type error: error: Invalid input type: `Natural`
+Type error: error: Expected a type, found: `2`
--> <current file>:1:0
|
1 | 2 → _
| ^ this has type: `Natural`
|
- = help: The input type of a function must have type `Type`, `Kind` or `Sort`
+ = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
index 5b88ff7..6f26607 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:7
+ |
+1 | Kind → Sort
+ | ^^^^ Sort does not have a type
+ |
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
index 5b88ff7..169014b 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:7
+ |
+1 | Type → Sort
+ | ^^^^ Sort does not have a type
+ |
diff --git a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
index 5ba4b35..51279f2 100644
--- a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
+++ b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: (True : Bool) : Natural
- --> <current file>:1:8
+Type error: error: annot mismatch: Bool != Natural
+ --> <current file>:1:18
|
1 | let x : Natural = True in True
- | ^^^^^^^ annot mismatch: (True : Bool) : Natural
+ | ^^^^ annot mismatch: Bool != Natural
|
diff --git a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
index 5332fcb..0cc4bba 100644
--- a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
+++ b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: ([1] : List Natural) : Optional Natural
+Type error: error: annot mismatch: List Natural != Optional Natural
--> <current file>:1:0
|
1 | [ 1 ] : Optional Natural
- | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: ([1] : List Natural) : Optional Natural
+ | ^^^^^ annot mismatch: List Natural != Optional Natural
|
diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
index 5b88ff7..146018f 100644
--- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+ |
+1 | { x = Type, y = Kind }
+ | ^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
index f74e839..02cf64f 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt
@@ -1 +1,6 @@
Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+ |
+1 | True ∧ {=}
+ | ^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
index f74e839..202a3e5 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt
@@ -1 +1,6 @@
Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+ |
+1 | { x = True } ∧ { x = False }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
index f74e839..a0b4676 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt
@@ -1 +1,6 @@
Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+ |
+1 | {=} ∧ True
+ | ^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
index f74e839..769712b 100644
--- a/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
+++ b/dhall/tests/type-inference/failure/unit/RecursiveRecordTypeMergeOverlapping.txt
@@ -1 +1,6 @@
Type error: error: RecordTypeMergeRequiresRecordType
+ --> <current file>:1:0
+ |
+1 | { x : Bool } ⩓ { x : Natural }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
index 5b88ff7..521ae05 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:15
+ |
+1 | { x = Bool } ⫽ { x = Kind }
+ | ^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
index 5b88ff7..3abf62c 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: InvalidFieldType
+ --> <current file>:1:14
+ |
+1 | { x = {=} } ⫽ { x = Kind }
+ | ^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/Sort.txt b/dhall/tests/type-inference/failure/unit/Sort.txt
index 5b88ff7..e402127 100644
--- a/dhall/tests/type-inference/failure/unit/Sort.txt
+++ b/dhall/tests/type-inference/failure/unit/Sort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:0
+ |
+1 | Sort
+ | ^^^^ Sort does not have a type
+ |
diff --git a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
index 7360e68..dffadb1 100644
--- a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
+++ b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
@@ -1,6 +1,6 @@
-Type error: error: annot mismatch: (1 : Natural) : Bool
+Type error: error: annot mismatch: Natural != Bool
--> <current file>:1:0
|
1 | 1 : Bool
- | ^^^^^^^^ annot mismatch: (1 : Natural) : Bool
+ | ^ annot mismatch: Natural != Bool
|