spec!: remove Optional/build and Optional/fold

1 files changed, 12 insertions, 0 deletions

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
+   |