From 8abb6c24cd26b64d708a74faaa28cc9294dc3466 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 17:47:58 +0000
Subject: Move ui outputs to a sensible place

---
 dhall/tests/type-inference/failure/hurkensParadox.txt | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 dhall/tests/type-inference/failure/hurkensParadox.txt

(limited to 'dhall/tests/type-inference/failure/hurkensParadox.txt')

diff --git a/dhall/tests/type-inference/failure/hurkensParadox.txt b/dhall/tests/type-inference/failure/hurkensParadox.txt
new file mode 100644
index 0000000..6b99615
--- /dev/null
+++ b/dhall/tests/type-inference/failure/hurkensParadox.txt
@@ -0,0 +1,15 @@
+Type 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`
-- 
cgit v1.2.3