From 70eede4fd012f49dfab0e2e27fb3a4e4bbff6325 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 1 Feb 2020 22:04:34 +0000
Subject: Implement once nice error using annotate_snippets

---
 dhall/tests/type-errors/hurkensParadox.txt | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

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

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
+   |
-- 
cgit v1.2.3