From ac7e39a752c41c06155e27e84404c67c1341065d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 25 Jun 2020 14:28:48 +0100
Subject: spec!: remove Optional/build and Optional/fold

---
 .../failure/unit/LetWithNonterminatingAnnotation.txt         | 12 ++++++++++++
 .../failure/unit/RemovedBuiltinOptionalBuild.txt             |  6 ++++++
 .../failure/unit/RemovedBuiltinOptionalFold.txt              |  6 ++++++
 3 files changed, 24 insertions(+)
 create mode 100644 dhall/tests/type-inference/failure/unit/LetWithNonterminatingAnnotation.txt
 create mode 100644 dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalBuild.txt
 create mode 100644 dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalFold.txt

(limited to 'dhall/tests/type-inference/failure/unit')

diff --git a/dhall/tests/type-inference/failure/unit/LetWithNonterminatingAnnotation.txt b/dhall/tests/type-inference/failure/unit/LetWithNonterminatingAnnotation.txt
new file mode 100644
index 0000000..6e360da
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/LetWithNonterminatingAnnotation.txt
@@ -0,0 +1,12 @@
+Type error: error: expected function, found `Natural`
+  --> <current file>:6:25
+   |
+ 1 | -- When you check if an inferred type is equivalent to an annotation,
+ 2 | -- you must alpha-beta-normalize both sides first.  But it is not safe
+ 3 | -- to beta-normalise an expression which hasn't first been
+ 4 | -- typechecked.
+...
+10 | let a
+11 |     : (λ(x : Natural) → x x) (λ(x : Natural) → x x)
+   |                         ^ function application requires a function
+   |
diff --git a/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalBuild.txt b/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalBuild.txt
new file mode 100644
index 0000000..e4e285c
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalBuild.txt
@@ -0,0 +1,6 @@
+Type error: error: unbound variable ``Optional/build``
+ --> <current file>:1:1
+  |
+1 | Optional/build
+  | ^^^^^^^^^^^^^^ not found in this scope
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalFold.txt b/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalFold.txt
new file mode 100644
index 0000000..3d6c6aa
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalFold.txt
@@ -0,0 +1,6 @@
+Type error: error: unbound variable ``Optional/fold``
+ --> <current file>:1:1
+  |
+1 | Optional/fold
+  | ^^^^^^^^^^^^^ not found in this scope
+  |
-- 
cgit v1.2.3