summaryrefslogtreecommitdiff
path: root/dhall/tests
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/tests')
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt16
-rw-r--r--dhall/tests/type-errors/unit/AssertAlphaTrap.txt7
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt10
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt7
-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.txt10
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt10
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt9
-rw-r--r--dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt10
-rw-r--r--dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt7
-rw-r--r--dhall/tests/type-errors/unit/VariableFree.txt7
12 files changed, 97 insertions, 12 deletions
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 4dfdcf5..522e1a2 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1 +1,15 @@
-Type error: Unhandled error: function annot mismatch: (U : Sort) : Kind
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:6:23
+ |
+ 1 | let bottom : Type = ∀(any : Type) → any
+ 2 |
+ 3 | in let not : Type → Type = λ(p : Type) → p → bottom
+ 4 |
+...
+10 | : pow (pow U) → U
+11 | = λ(t : pow (pow U))
+ | ^^^ 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-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 8d101c3..01facbc 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:1:1
+ |
+1 | (λ(_ : Natural) → _) True
+ | ^^^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
+ | ^^^^ but this has type: Bool
+ |
+ = note: expected type `Natural`
+ found type `Bool`
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
index a72e120..f779fd6 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: apply to not Pi
+Type error: Unhandled error: error: expected function, found `Bool`
+ --> <current file>:1:0
+ |
+1 | True True
+ | ^^^^ function application requires a function
+ |
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 070e461..aa7c8c5 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: function annot mismatch: (Type : Kind) : Type
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:1:5
+ |
+1 | [] : List Type
+ | ^^^^ this expects an argument of type: Type
+ | ^^^^ but this has type: Kind
+ |
+ = note: expected type `Type`
+ found type `Kind`
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
index f1cdf92..053a054 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: merge handler is not a function
+ --> <current file>:1:0
+ |
+1 | merge { x = True } (< x : Bool >.x True)
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression
+ | ^^^^^^^^^^^^ the handler for `x` has 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..faca63a 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -1 +1,8 @@
-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 for `x` expects a value of type: `Bool`
+ | ^^^^^^^^^^^^^^^^^^^ but the corresponding variant has type: `Natural`
+ |
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
index 8d101c3..7e410c4 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:1:0
+ |
+1 | Natural/subtract True True
+ | ^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
+ | ^^^^ but this has type: Bool
+ |
+ = note: expected type `Natural`
+ found 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
+ |