summaryrefslogtreecommitdiff
path: root/dhall/tests/type-inference/failure/hurkensParadox.txt
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/tests/type-inference/failure/hurkensParadox.txt')
-rw-r--r--dhall/tests/type-inference/failure/hurkensParadox.txt8
1 files changed, 4 insertions, 4 deletions
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
- --> <current file>:6:23
+ --> <current file>: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`