summaryrefslogtreecommitdiff
path: root/dhall/tests
diff options
context:
space:
mode:
authorNadrieril2020-02-02 17:22:27 +0000
committerNadrieril2020-02-02 17:22:27 +0000
commitd8c3ced0f1acb1924c801fadbfd3077dede9b0dd (patch)
tree1884b1c33faf2c104c6b71ea8a6fd2472826da48 /dhall/tests
parent92bbea48f9a0380a614f2687c73d55a67ff9294e (diff)
More errors
Diffstat (limited to 'dhall/tests')
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt4
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt4
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt8
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt4
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt10
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt10
-rw-r--r--dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt4
7 files changed, 33 insertions, 11 deletions
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
+ --> <current file>: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
+ --> <current file>: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
+ --> <current file>: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
|