summaryrefslogtreecommitdiff
path: root/dhall/tests
diff options
context:
space:
mode:
authorNadrieril2020-02-02 15:02:23 +0000
committerNadrieril2020-02-02 15:06:39 +0000
commit92bbea48f9a0380a614f2687c73d55a67ff9294e (patch)
tree03dff980cafa1103d03ca6ad27ad729eda5901ec /dhall/tests
parent70eede4fd012f49dfab0e2e27fb3a4e4bbff6325 (diff)
More nice errors plus some refactor
Diffstat (limited to 'dhall/tests')
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt4
-rw-r--r--dhall/tests/type-errors/unit/AssertAlphaTrap.txt7
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt4
-rw-r--r--dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt8
-rw-r--r--dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt8
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt4
-rw-r--r--dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt4
-rw-r--r--dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt7
-rw-r--r--dhall/tests/type-errors/unit/VariableFree.txt7
9 files changed, 40 insertions, 13 deletions
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 10bb9a4..e06c4b2 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1,4 +1,4 @@
-Type error: Unhandled error: error: function annot mismatch
+Type error: Unhandled error: error: Wrong type of function argument
--> <current file>:6:23
|
1 | let bottom : Type = ∀(any : Type) → any
@@ -8,7 +8,7 @@ Type error: Unhandled error: error: function annot mismatch
...
10 | : pow (pow U) → U
11 | = λ(t : pow (pow U))
- | ^^^^^ function annot mismatch
+ | ^^^^^ Wrong type of function argument
| --- help: this expects an argument of type: Kind
| - help: but this has type: Sort
|
diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
index 87cf48e..e4584f5 100644
--- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
+++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: unbound variable
+Type error: Unhandled error: error: unbound variable ``_``
+ --> <current file>:1:46
+ |
+1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
+ | ^ not found in this scope
+ |
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
index 7aa2281..776b14e 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1,8 +1,8 @@
-Type error: Unhandled error: error: function annot mismatch
+Type error: Unhandled error: error: Wrong type of function argument
--> <current file>:1:1
|
1 | (λ(_ : Natural) → _) True
- | ^^^^^^^^^^^^^^^^^^^^^^^^ function annot mismatch
+ | ^^^^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument
| ------------------ help: this expects an argument of type: Natural
| ---- help: but this has type: Bool
|
diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
index a13fb3a..3fc1652 100644
--- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
+++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
@@ -1 +1,7 @@
-[unknown location] Type error: Invalid function input
+Type error: Unhandled error: error: Invalid input type: `Natural`
+ --> <current file>:1:6
+ |
+1 | λ(_ : 1) → _
+ | ^ this has type: `Natural`
+ |
+ = help: The input type of a function must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
index a13fb3a..948c6c7 100644
--- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
+++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -1 +1,7 @@
-[unknown location] Type error: Invalid function input
+Type error: Unhandled error: error: Invalid input type: `Natural`
+ --> <current file>:1:0
+ |
+1 | 2 → _
+ | ^ this has type: `Natural`
+ |
+ = help: The input type of a function must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
index 3673338..125cc87 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1,8 +1,8 @@
-Type error: Unhandled error: error: function annot mismatch
+Type error: Unhandled error: error: Wrong type of function argument
--> <current file>:1:5
|
1 | [] : List Type
- | ^^^^^^^^^ function annot mismatch
+ | ^^^^^^^^^ Wrong type of function argument
| ---- help: this expects an argument of type: Type
| ---- help: but this has type: Kind
|
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
index 795c97c..5ee2a11 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1,8 +1,8 @@
-Type error: Unhandled error: error: function annot mismatch
+Type error: Unhandled error: error: Wrong type of function argument
--> <current file>:1:0
|
1 | Natural/subtract True True
- | ^^^^^^^^^^^^^^^^^^^^^ function annot mismatch
+ | ^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument
| ---------------- help: this expects an argument of type: Natural
| ---- help: but this has type: Bool
|
diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
index 87cf48e..a234f9f 100644
--- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
+++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: unbound variable
+Type error: Unhandled error: error: unbound variable `constructors`
+ --> <current file>:1:0
+ |
+1 | constructors < Left : Natural | Right : Bool >
+ | ^^^^^^^^^^^^ not found in this scope
+ |
diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt
index 87cf48e..52baa7f 100644
--- a/dhall/tests/type-errors/unit/VariableFree.txt
+++ b/dhall/tests/type-errors/unit/VariableFree.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: unbound variable
+Type error: Unhandled error: error: unbound variable `x`
+ --> <current file>:1:0
+ |
+1 | x
+ | ^ not found in this scope
+ |