From e25b67906ce68e8726e8139c1d1855f3ab2518ce Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 20:45:42 +0000 Subject: Rework annotation and Sort handling --- dhall/tests/type-inference/failure/SortInLet.txt | 7 ++++++- dhall/tests/type-inference/failure/hurkensParadox.txt | 8 ++++---- dhall/tests/type-inference/failure/recordOfKind.txt | 2 +- .../failure/unit/AnnotationRecordWrongFieldName.txt | 2 +- .../failure/unit/AnnotationRecordWrongFieldType.txt | 2 +- dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt | 7 ++++++- dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt | 7 ++++++- .../tests/type-inference/failure/unit/LetWithWrongAnnotation.txt | 4 ++-- .../failure/unit/OptionalDeprecatedSyntaxPresent.txt | 2 +- dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt | 2 +- .../failure/unit/RightBiasedRecordMergeMixedKinds2.txt | 2 +- .../failure/unit/RightBiasedRecordMergeMixedKinds3.txt | 2 +- dhall/tests/type-inference/failure/unit/Sort.txt | 7 ++++++- dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt | 2 +- 14 files changed, 38 insertions(+), 18 deletions(-) (limited to 'dhall/tests') 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 + --> :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 - --> :6:23 + --> :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..a5d2465 100644 --- a/dhall/tests/type-inference/failure/recordOfKind.txt +++ b/dhall/tests/type-inference/failure/recordOfKind.txt @@ -1 +1 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt index 01a1f32..a39a0fb 100644 --- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt +++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt @@ -2,5 +2,5 @@ Type error: error: annot mismatch: { x : Natural } != { y : Natural } --> :1:0 | 1 | { x = 1 } : { y : Natural } - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { 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 5c10467..9ecc2a4 100644 --- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt +++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt @@ -2,5 +2,5 @@ Type error: error: annot mismatch: { x : Natural } != { x : Text } --> :1:0 | 1 | { x = 1 } : { x : Text } - | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { x : Natural } != { x : Text } + | ^^^^^^^^^ annot mismatch: { x : Natural } != { x : Text } | 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 + --> :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 + --> :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 2f75196..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: Bool != Natural - --> :1:8 + --> :1:18 | 1 | let x : Natural = True in True - | ^^^^^^^ annot mismatch: 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 066e4a3..0cc4bba 100644 --- a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt +++ b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt @@ -2,5 +2,5 @@ Type error: error: annot mismatch: List Natural != Optional Natural --> :1:0 | 1 | [ 1 ] : Optional Natural - | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: 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..a5d2465 100644 --- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt +++ b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt @@ -1 +1 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt index 5b88ff7..a5d2465 100644 --- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt +++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt @@ -1 +1 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt index 5b88ff7..a5d2465 100644 --- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt +++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt @@ -1 +1 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type 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 + --> :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 e203d22..dffadb1 100644 --- a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt +++ b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt @@ -2,5 +2,5 @@ Type error: error: annot mismatch: Natural != Bool --> :1:0 | 1 | 1 : Bool - | ^^^^^^^^ annot mismatch: Natural != Bool + | ^ annot mismatch: Natural != Bool | -- cgit v1.2.3