From 6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:53:55 +0000 Subject: Remove most TyExpr from normalization --- .../type-inference/failure/unit/AnnotationRecordWrongFieldName.txt | 4 ++-- .../type-inference/failure/unit/AnnotationRecordWrongFieldType.txt | 4 ++-- .../type-inference/failure/unit/CompletionMissingRequiredField.txt | 4 ++-- .../type-inference/failure/unit/CompletionWithWrongDefaultType.txt | 4 ++-- .../type-inference/failure/unit/CompletionWithWrongFieldName.txt | 4 ++-- .../type-inference/failure/unit/CompletionWithWrongOverridenType.txt | 4 ++-- dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt | 4 ++-- .../type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt | 4 ++-- dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt | 4 ++-- 9 files changed, 18 insertions(+), 18 deletions(-) (limited to 'dhall/tests') diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt index 2a754fc..01a1f32 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 } --> :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..5c10467 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 } --> :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 } --> :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 } --> :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 } --> :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 } --> :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/LetWithWrongAnnotation.txt b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt index 5ba4b35..2f75196 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 +Type error: error: annot mismatch: Bool != Natural --> :1:8 | 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..066e4a3 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 --> :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/TypeAnnotationWrong.txt b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt index 7360e68..e203d22 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 --> :1:0 | 1 | 1 : Bool - | ^^^^^^^^ annot mismatch: (1 : Natural) : Bool + | ^^^^^^^^ annot mismatch: Natural != Bool | -- cgit v1.2.3 From a709c65eb28f1b6a666f15bfc2255da7bc7105ab Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 21:38:37 +0000 Subject: Resolve variables alongside import resolution --- dhall/tests/import/failure/cycle.txt | 2 +- dhall/tests/import/failure/importBoundary.txt | 8 +++++++- 2 files changed, 8 insertions(+), 2 deletions(-) (limited to 'dhall/tests') 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 --> :1:0\n |\n...\n3 | x\n | ^ not found in this scope\n |") })) +Type error: error: unbound variable `x` + --> :1:0 + | +... +3 | x + | ^ not found in this scope + | -- cgit v1.2.3 From f29a40fb55b898b3a3cc51f198e8522eaecf0777 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 20:17:41 +0000 Subject: Simplify conversions to/from TyExpr --- .../type-inference/failure/unit/RecursiveRecordMergeLhsNotRecord.txt | 5 +++++ .../type-inference/failure/unit/RecursiveRecordMergeOverlapping.txt | 5 +++++ .../type-inference/failure/unit/RecursiveRecordMergeRhsNotRecord.txt | 5 +++++ .../failure/unit/RecursiveRecordTypeMergeOverlapping.txt | 5 +++++ 4 files changed, 20 insertions(+) (limited to 'dhall/tests') 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 + --> :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 + --> :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 + --> :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 + --> :1:0 + | +1 | { x : Bool } ⩓ { x : Natural } + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeMergeRequiresRecordType + | -- cgit v1.2.3 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 From 130de8cea49c848a06174c61c747d9414a5c71b7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 16 Feb 2020 19:06:23 +0000 Subject: Start requiring Universe to build a Type --- .../type-inference/failure/unit/FunctionArgumentTypeNotAType.txt | 4 ++-- .../type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'dhall/tests') 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` --> :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` --> :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` -- cgit v1.2.3 From c451c18103b871e563b12c524bc3feec5451154c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 16 Feb 2020 19:48:35 +0000 Subject: Avoid recomputing universes in tck --- dhall/tests/type-inference/failure/recordOfKind.txt | 7 ++++++- dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt | 7 ++++++- .../failure/unit/RightBiasedRecordMergeMixedKinds2.txt | 7 ++++++- .../failure/unit/RightBiasedRecordMergeMixedKinds3.txt | 7 ++++++- 4 files changed, 24 insertions(+), 4 deletions(-) (limited to 'dhall/tests') diff --git a/dhall/tests/type-inference/failure/recordOfKind.txt b/dhall/tests/type-inference/failure/recordOfKind.txt index a5d2465..653fe0b 100644 --- a/dhall/tests/type-inference/failure/recordOfKind.txt +++ b/dhall/tests/type-inference/failure/recordOfKind.txt @@ -1 +1,6 @@ -Type error: error: Sort does not have a type +Type error: error: InvalidFieldType + --> :1:0 + | +1 | { a = Kind } + | ^^^^^^^^^^^^ InvalidFieldType + | diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt index a5d2465..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: error: Sort does not have a type +Type error: error: InvalidFieldType + --> :1:0 + | +1 | { x = Type, y = Kind } + | ^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType + | diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt index a5d2465..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: error: Sort does not have a type +Type error: error: InvalidFieldType + --> :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 a5d2465..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: error: Sort does not have a type +Type error: error: InvalidFieldType + --> :1:14 + | +1 | { x = {=} } ⫽ { x = Kind } + | ^^^^^^^^^^^^ InvalidFieldType + | -- cgit v1.2.3