From d8c3ced0f1acb1924c801fadbfd3077dede9b0dd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 2 Feb 2020 17:22:27 +0000 Subject: More errors --- dhall/tests/type-errors/hurkensParadox.txt | 4 ++-- .../type-errors/unit/FunctionApplicationArgumentNotMatch.txt | 4 ++-- .../type-errors/unit/FunctionApplicationIsNotFunction.txt | 8 +++++++- dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt | 4 ++-- dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt | 10 +++++++++- .../type-errors/unit/MergeHandlerNotMatchAlternativeType.txt | 10 +++++++++- dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt | 4 ++-- 7 files changed, 33 insertions(+), 11 deletions(-) (limited to 'dhall/tests') diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index e06c4b2..5241517 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -9,6 +9,6 @@ Type error: Unhandled error: error: Wrong type of function argument 10 | : pow (pow U) → U 11 | = λ(t : pow (pow U)) | ^^^^^ Wrong type of function argument - | --- help: this expects an argument of type: Kind - | - help: but this has type: Sort + | ^^^ this expects an argument of type: Kind + | ^ but this has type: Sort | diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 776b14e..d8811c2 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -3,6 +3,6 @@ Type error: Unhandled error: error: Wrong type of function argument | 1 | (λ(_ : Natural) → _) True | ^^^^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument - | ------------------ help: this expects an argument of type: Natural - | ---- help: but this has type: Bool + | ^^^^^^^^^^^^^^^^^^ this expects an argument of type: Natural + | ^^^^ but this has type: Bool | diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt index a72e120..0732d1c 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -1 +1,7 @@ -Type error: Unhandled error: apply to not Pi +Type error: Unhandled error: error: Trying to apply an argument to a value that is not a function + --> :1:0 + | +1 | True True + | ^^^^ this has type: `Bool` + | + = help: only functions can be applied to diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index 125cc87..1459ca1 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -3,6 +3,6 @@ Type error: Unhandled error: error: Wrong type of function argument | 1 | [] : List Type | ^^^^^^^^^ Wrong type of function argument - | ---- help: this expects an argument of type: Type - | ---- help: but this has type: Kind + | ^^^^ this expects an argument of type: Type + | ^^^^ but this has type: Kind | diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt index f1cdf92..16931a8 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt @@ -1 +1,9 @@ -Type error: Unhandled error: NotAFunction +Type error: Unhandled error: error: Handler is not a function + --> :1:0 + | +1 | merge { x = True } (< x : Bool >.x True) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression + | ^^^^^^^^ the handler `x` had type: `Bool` + | ----------------- help: the corresponding variant has type: `Bool` + | + = help: a handler for this variant must be a function that takes an input of type: `Bool` diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt index 8b729a4..1762a7c 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -1 +1,9 @@ -Type error: Unhandled error: MergeHandlerTypeMismatch +Type error: Unhandled error: error: Wrong handler input type + --> :1:0 + | +1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression + | ^^^^^^^^^^^^^^^^^^^ the handler `x` expects a value of type: `Bool` + | ^^^^^^^^^^^^^^^^^ but the corresponding variant has type: `Natural` + | + = help: only functions can be applied to diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index 5ee2a11..a35b9ab 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -3,6 +3,6 @@ Type error: Unhandled error: error: Wrong type of function argument | 1 | Natural/subtract True True | ^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument - | ---------------- help: this expects an argument of type: Natural - | ---- help: but this has type: Bool + | ^^^^^^^^^^^^^^^^ this expects an argument of type: Natural + | ^^^^ but this has type: Bool | -- cgit v1.2.3