summaryrefslogtreecommitdiff
path: root/dhall/tests/type-errors/hurkensParadox.txt
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt15
1 files changed, 14 insertions, 1 deletions
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 4dfdcf5..10bb9a4 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1 +1,14 @@
-Type error: Unhandled error: function annot mismatch: (U : Sort) : Kind
+Type error: Unhandled error: error: function annot mismatch
+ --> <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))
+ | ^^^^^ function annot mismatch
+ | --- help: this expects an argument of type: Kind
+ | - help: but this has type: Sort
+ |