spec!: remove Optional/build and Optional/fold

8 files changed, 29 insertions, 48 deletions

diff --git a/CHANGELOG.md b/CHANGELOG.md
index dd042c3..8854a31 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,7 @@
 
 #### [Unreleased]
 
+- BREAKING CHANGE: Remove Optional/build and Optional/fold
 - BREAKING CHANGE: Remove the ability to quote paths in URLs
 - Allow quoted labels to be empty
 - Support Dhall v16.0.0
diff --git a/dhall-lang b/dhall-lang
-Subproject 9358ffa9c8241b0d8446d46010318758b0df38c
+Subproject 549470527dcc0ee59253708c6ac23c0cee45509
diff --git a/dhall/src/builtins.rs b/dhall/src/builtins.rs
index 67929a0..16d656f 100644
--- a/dhall/src/builtins.rs
+++ b/dhall/src/builtins.rs
@@ -42,8 +42,6 @@ pub enum Builtin {
     ListLast,
     ListIndexed,
     ListReverse,
-    OptionalFold,
-    OptionalBuild,
     TextShow,
 }
 
@@ -79,8 +77,6 @@ impl Builtin {
             "List/last" => Some(ListLast),
             "List/indexed" => Some(ListIndexed),
             "List/reverse" => Some(ListReverse),
-            "Optional/fold" => Some(OptionalFold),
-            "Optional/build" => Some(OptionalBuild),
             "Text/show" => Some(TextShow),
             _ => None,
         }
@@ -245,22 +241,6 @@ pub fn type_of_builtin(b: Builtin) -> Hir {
             forall (a: Type) -> (List a) -> List a
         ),
 
-        OptionalBuild => make_type!(
-            forall (a: Type) ->
-            (forall (optional: Type) ->
-                forall (just: a -> optional) ->
-                forall (nothing: optional) ->
-                optional) ->
-            Optional a
-        ),
-        OptionalFold => make_type!(
-            forall (a: Type) ->
-            (Optional a) ->
-            forall (optional: Type) ->
-            forall (just: a -> optional) ->
-            forall (nothing: optional) ->
-            optional
-        ),
         OptionalNone => make_type!(
             forall (A: Type) -> Optional A
         ),
@@ -510,27 +490,6 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
             }
             _ => Ret::DoneAsIs,
         },
-        (Builtin::OptionalBuild, [t, f]) => {
-            let optional_t =
-                Nir::from_builtin(Builtin::Optional).app(t.clone());
-            Ret::Nir(
-                f.app(optional_t)
-                    .app(
-                        make_closure(make_closure!(
-                            λ(T : Type) ->
-                            λ(a : var(T)) ->
-                            Some(var(a))
-                        ))
-                        .app(t.clone()),
-                    )
-                    .app(EmptyOptionalLit(t.clone()).into_nir()),
-            )
-        }
-        (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
-            EmptyOptionalLit(_) => Ret::Nir(nothing.clone()),
-            NEOptionalLit(x) => Ret::Nir(just.app(x.clone())),
-            _ => Ret::DoneAsIs,
-        },
         (Builtin::NaturalBuild, [f]) => Ret::Nir(
             f.app(Nir::from_builtin(Builtin::Natural))
                 .app(make_closure(make_closure!(
@@ -600,8 +559,6 @@ impl std::fmt::Display for Builtin {
             ListLast => "List/last",
             ListIndexed => "List/indexed",
             ListReverse => "List/reverse",
-            OptionalFold => "Optional/fold",
-            OptionalBuild => "Optional/build",
             TextShow => "Text/show",
         })
     }
diff --git a/dhall/src/syntax/text/dhall.abnf b/dhall/src/syntax/text/dhall.abnf
index 173209c..37ec43b 100644
--- a/dhall/src/syntax/text/dhall.abnf
+++ b/dhall/src/syntax/text/dhall.abnf
@@ -387,6 +387,9 @@ keyword =
     / forall-keyword

     / with

 

+; Note that there is a corresponding parser test in

+; `tests/parser/success/builtinsA.dhall`. Please update it when

+; you modify this `builtin` rule.

 builtin =

       Natural-fold

     / Natural-build

@@ -408,8 +411,6 @@ builtin =
     / List-last

     / List-indexed

     / List-reverse

-    / Optional-fold

-    / Optional-build

     / Text-show

     / Bool

     / True

@@ -462,8 +463,6 @@ List-head         = %x4c.69.73.74.2f.68.65.61.64
 List-last         = %x4c.69.73.74.2f.6c.61.73.74

 List-indexed      = %x4c.69.73.74.2f.69.6e.64.65.78.65.64

 List-reverse      = %x4c.69.73.74.2f.72.65.76.65.72.73.65

-Optional-fold     = %x4f.70.74.69.6f.6e.61.6c.2f.66.6f.6c.64

-Optional-build    = %x4f.70.74.69.6f.6e.61.6c.2f.62.75.69.6c.64

 Text-show         = %x54.65.78.74.2f.73.68.6f.77

 

 ; Operators

diff --git a/dhall/tests/parser/success/builtinsB.txt b/dhall/tests/parser/success/builtinsB.txt
index 4e3ed79..1005949 100644
--- a/dhall/tests/parser/success/builtinsB.txt
+++ b/dhall/tests/parser/success/builtinsB.txt
@@ -1 +1 @@
-λ(x : { field0 : Bool, field1 : Optional (Optional Bool), field2 : Natural, field3 : Integer, field4 : Double, field5 : Text, field6 : List (List Bool) }) → { field00 = Natural/fold, field01 = Natural/build, field02 = Natural/isZero, field03 = Natural/even, field04 = Natural/odd, field05 = Natural/toInteger, field06 = Natural/show, field07 = Integer/show, field08 = Double/show, field09 = List/build, field10 = List/fold, field11 = List/length, field12 = List/head, field13 = List/last, field14 = List/indexed, field15 = List/reverse, field16 = Optional/fold, field17 = Optional/build, field18 = True, field19 = False, field20 = None }
+[Natural/fold, Natural/build, Natural/isZero, Natural/even, Natural/odd, Natural/toInteger, Natural/show, Integer/toDouble, Integer/show, Integer/negate, Integer/clamp, Natural/subtract, Double/show, List/build, List/fold, List/length, List/head, List/last, List/indexed, List/reverse, Text/show, Bool, True, False, Optional, None, Natural, Integer, Double, Text, List, Type, Kind, Sort]
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
+  |