diff options
Diffstat (limited to 'dhall/tests/type-inference/failure')
24 files changed, 95 insertions, 35 deletions
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 | |