Merge pull request #171 from Nadrieril/catchup-spec

62 files changed, 246 insertions, 226 deletions

diff --git a/dhall/build.rs b/dhall/build.rs
index 4fc8545..22f0e8f 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -15,7 +15,6 @@ fn convert_abnf_to_pest() -> std::io::Result<()> {
 
     let mut data = read_to_string(abnf_path)?;
     data.push('\n');
-    let data = data.replace('∀', ""); // TODO: waiting for abnf 0.6.1
 
     let mut rules = abnf_to_pest::parse_abnf(&data)?;
     for line in BufReader::new(File::open(visibility_path)?).lines() {
@@ -95,7 +94,7 @@ fn convert_abnf_to_pest() -> std::io::Result<()> {
             bool_or |
             import_alt
         }}
-        operator_expression = {{ with_expression ~ (whsp ~ operator ~ whsp ~ with_expression)* }}
+        operator_expression = {{ application_expression ~ (whsp ~ operator ~ whsp ~ application_expression)* }}
     "##
     )?;
 
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/operations/kind.rs b/dhall/src/operations/kind.rs
index 5415637..0ee9671 100644
--- a/dhall/src/operations/kind.rs
+++ b/dhall/src/operations/kind.rs
@@ -6,6 +6,8 @@ use crate::syntax::{trivial_result, Label};
 // pretty-printing to work correctly
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum BinOp {
+    /// x === y
+    Equivalence,
     /// `x ? y`
     ImportAlt,
     /// `x || y`
@@ -30,8 +32,6 @@ pub enum BinOp {
     BoolEQ,
     /// `x != y`
     BoolNE,
-    /// x === y
-    Equivalence,
 }
 
 /// Operations
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 361e1b4..d21c7ce 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -137,30 +137,20 @@ fn type_one_layer(
             Type::from_const(k)
         }
         ExprKind::UnionType(kts) => {
-            // Check that all types are the same const
-            let mut k = None;
+            // An empty union type has type Type;
+            // an union type with only unary variants also has type Type
+            let mut k = Const::Type;
             for t in kts.values() {
                 if let Some(t) = t {
-                    let c = match t.ty().as_const() {
-                        Some(c) => c,
+                    match t.ty().as_const() {
+                        Some(c) => k = max(k, c),
                         None => {
                             return mk_span_err(t.span(), "InvalidVariantType")
                         }
-                    };
-                    match k {
-                        None => k = Some(c),
-                        Some(k) if k == c => {}
-                        _ => {
-                            return mk_span_err(t.span(), "InvalidVariantType")
-                        }
                     }
                 }
             }
 
-            // An empty union type has type Type;
-            // an union type with only unary variants also has type Type
-            let k = k.unwrap_or(Const::Type);
-
             Type::from_const(k)
         }
         ExprKind::Op(op) => typecheck_operation(env, span, op)?,
diff --git a/dhall/src/syntax/ast/span.rs b/dhall/src/syntax/ast/span.rs
index e250602..ab3279b 100644
--- a/dhall/src/syntax/ast/span.rs
+++ b/dhall/src/syntax/ast/span.rs
@@ -66,6 +66,12 @@ impl Span {
                     end: max(x.end, y.end),
                 })
             }
+            (Parsed(_), Parsed(_)) => panic!(
+                "Tried to union incompatible spans: {:?} and {:?}",
+                self, other
+            ),
+            (Parsed(x), _) => Parsed(x.clone()),
+            (_, Parsed(x)) => Parsed(x.clone()),
             _ => panic!(
                 "Tried to union incompatible spans: {:?} and {:?}",
                 self, other
diff --git a/dhall/src/syntax/text/dhall.abnf b/dhall/src/syntax/text/dhall.abnf
index 1c3a980..37ec43b 100644
--- a/dhall/src/syntax/text/dhall.abnf
+++ b/dhall/src/syntax/text/dhall.abnf
@@ -206,7 +206,7 @@ quoted-label-char =
         ; %x60 = '`'

     / %x61-7E

 

-quoted-label = 1*quoted-label-char

+quoted-label = *quoted-label-char

 

 ; NOTE: Dhall does not support Unicode labels, mainly to minimize the potential

 ; for code obfuscation

@@ -370,7 +370,9 @@ NaN                   = %x4e.61.4e
 Some                  = %x53.6f.6d.65

 toMap                 = %x74.6f.4d.61.70

 assert                = %x61.73.73.65.72.74

-forall                = %x2200 / %x66.6f.72.61.6c.6c ; "∀" / "forall"

+forall-keyword        = %x66.6f.72.61.6c.6c ; "forall"

+forall-symbol         = %x2200 ; Unicode FOR ALL

+forall                = forall-symbol / forall-keyword

 with                  = %x77.69.74.68

 

 ; Unused rule that could be used as negative lookahead in the

@@ -382,9 +384,12 @@ keyword =
     / assert / as

     / Infinity / NaN

     / merge / Some / toMap

-    / forall

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

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

     / List-indexed

     / List-reverse

-    / Optional-fold

-    / Optional-build

     / Text-show

     / Bool

     / True

@@ -460,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

@@ -580,7 +581,6 @@ scheme = %x68.74.74.70 [ %x73 ]  ; "http" [ "s" ]
 

 ; NOTE: This does not match the official grammar for a URI.  Specifically:

 ;

-; * path segments may be quoted instead of using percent-encoding

 ; * this does not support fragment identifiers, which have no meaning within

 ;   Dhall expressions and do not affect import resolution

 ; * the characters "(" ")" and "," are not included in the `sub-delims` rule:

@@ -593,13 +593,9 @@ scheme = %x68.74.74.70 [ %x73 ]  ; "http" [ "s" ]
 ;

 ; Reserved characters in quoted path components should be percent-encoded

 ; according to https://tools.ietf.org/html/rfc3986#section-2

-http-raw = scheme "://" authority url-path [ "?" query ]

+http-raw = scheme "://" authority path-abempty [ "?" query ]

 

-; Temporary rule to allow old-style `path-component`s and RFC3986 `segment`s in

-; the same grammar. Eventually we can just use `path-abempty` from the same

-; RFC. See issue #581

-

-url-path = *(path-component / "/" segment)

+path-abempty = *( "/" segment )

 

 ; NOTE: Backtrack if parsing the optional user info prefix fails

 authority = [ userinfo "@" ] host [ ":" port ]

@@ -757,6 +753,11 @@ expression =
     ; NOTE: Backtrack if parsing this alternative fails

     / operator-expression whsp arrow whsp expression

     

+    ; "a with x = b"

+    ;

+    ; NOTE: Backtrack if parsing this alternative fails

+    / with-expression

+    

     ; "merge e1 e2 : t"

     ;

     ; NOTE: Backtrack if parsing this alternative fails since we can't tell

@@ -792,9 +793,16 @@ let-binding = let whsp1 nonreserved-label whsp [ ":" whsp1 expression whsp ] "="
 empty-list-literal =

     "[" whsp [ "," whsp ] "]" whsp ":" whsp1 application-expression

 

-operator-expression = import-alt-expression

+with-expression =

+    import-expression 1*(whsp1 with whsp1 with-clause)

+

+with-clause =

+    any-label-or-some *(whsp "." whsp any-label-or-some) whsp "=" whsp operator-expression

+

+operator-expression = equivalent-expression

 

 ; Nonempty-whitespace to disambiguate `http://a/a?a`

+equivalent-expression    = import-alt-expression    *(whsp equivalent whsp import-alt-expression)

 import-alt-expression    = or-expression            *(whsp "?" whsp1 or-expression)

 or-expression            = plus-expression          *(whsp "||" whsp plus-expression)

 ; Nonempty-whitespace to disambiguate `f +2`

@@ -807,13 +815,7 @@ prefer-expression        = combine-types-expression *(whsp prefer whsp combine-t
 combine-types-expression = times-expression         *(whsp combine-types whsp times-expression)

 times-expression         = equal-expression         *(whsp "*" whsp equal-expression)

 equal-expression         = not-equal-expression     *(whsp "==" whsp not-equal-expression)

-not-equal-expression     = equivalent-expression    *(whsp "!=" whsp equivalent-expression)

-equivalent-expression    = with-expression          *(whsp equivalent whsp with-expression)

-

-with-expression = application-expression *(whsp1 with whsp1 with-clause)

-

-with-clause =

-    any-label-or-some *(whsp "." whsp any-label-or-some) whsp "=" whsp application-expression

+not-equal-expression     = application-expression   *(whsp "!=" whsp application-expression)

 

 

 ; Import expressions need to be separated by some whitespace, otherwise there

@@ -890,11 +892,9 @@ primitive-expression =
 

 record-type-or-literal =

       empty-record-literal

-    / non-empty-record-type-or-literal

-    / empty-record-type

+    / [non-empty-record-type-or-literal]

 

 empty-record-literal = "="

-empty-record-type = ""

 

 non-empty-record-type-or-literal =

     (non-empty-record-type / non-empty-record-literal)

@@ -907,22 +907,18 @@ record-type-entry = any-label-or-some whsp ":" whsp1 expression
 non-empty-record-literal =

     record-literal-entry *(whsp "," whsp record-literal-entry)

 

+; If the `record-literal-normal-entry` is absent, that represents a punned

+; record entry, such as in `{ x }`, which is a short-hand for `{ x = x }`

 record-literal-entry =

-    any-label-or-some (record-literal-normal-entry / record-literal-punned-entry)

+    any-label-or-some [record-literal-normal-entry]

 

 record-literal-normal-entry =

     *(whsp "." whsp any-label-or-some) whsp "=" whsp expression

-record-literal-punned-entry = ""

-

 

+; If the `union-type-entry` is absent, that represents an empty union

+; alternative, such as in `< Heads | Tails >`

 union-type =

-      non-empty-union-type

-    / empty-union-type

-

-empty-union-type = ""

-

-non-empty-union-type =

-    union-type-entry *(whsp "|" whsp union-type-entry)

+    [union-type-entry *(whsp "|" whsp union-type-entry)]

 

 ; x : Natural

 ; x

diff --git a/dhall/src/syntax/text/dhall.pest.visibility b/dhall/src/syntax/text/dhall.pest.visibility
index b2114ce..6de7dd2 100644
--- a/dhall/src/syntax/text/dhall.pest.visibility
+++ b/dhall/src/syntax/text/dhall.pest.visibility
@@ -120,7 +120,7 @@ home_path
 absolute_path
 scheme
 http_raw
-url_path
+path_abempty
 authority
 # userinfo
 # host
@@ -178,19 +178,15 @@ selector
 labels
 # type_selector
 primitive_expression
-# record_type_or_literal
+record_type_or_literal
 empty_record_literal
-empty_record_type
-non_empty_record_type_or_literal
+# non_empty_record_type_or_literal
 non_empty_record_type
 record_type_entry
 non_empty_record_literal
 record_literal_entry
-# record_literal_punned_entry
 # record_literal_normal_entry
 union_type
-empty_union_type
-# non_empty_union_type
 union_type_entry
 non_empty_list_literal
 # complete_expression
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 1e1449c..06c1ac3 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -130,6 +130,7 @@ lazy_static::lazy_static! {
         use Rule::*;
         // In order of precedence
         let operators = vec![
+            equivalent,
             import_alt,
             bool_or,
             natural_plus,
@@ -142,7 +143,6 @@ lazy_static::lazy_static! {
             natural_times,
             bool_eq,
             bool_ne,
-            equivalent,
         ];
         PrecClimber::new(
             operators
@@ -514,14 +514,14 @@ impl DhallParser {
 
     fn http_raw(input: ParseInput) -> ParseResult<URL<Expr>> {
         Ok(match_nodes!(input.into_children();
-            [scheme(sch), authority(auth), url_path(p)] => URL {
+            [scheme(sch), authority(auth), path_abempty(p)] => URL {
                 scheme: sch,
                 authority: auth,
                 path: p,
                 query: None,
                 headers: None,
             },
-            [scheme(sch), authority(auth), url_path(p), query(q)] => URL {
+            [scheme(sch), authority(auth), path_abempty(p), query(q)] => URL {
                 scheme: sch,
                 authority: auth,
                 path: p,
@@ -531,10 +531,10 @@ impl DhallParser {
         ))
     }
 
-    fn url_path(input: ParseInput) -> ParseResult<FilePath> {
+    fn path_abempty(input: ParseInput) -> ParseResult<FilePath> {
         Ok(match_nodes!(input.into_children();
-            [path_component(components)..] => {
-                let mut file_path: Vec<_> = components.collect();
+            [segment(segments)..] => {
+                let mut file_path: Vec<_> = segments.collect();
                 // An empty path normalizes to "/"
                 if file_path.is_empty() {
                     file_path = vec!["".to_owned()];
@@ -548,7 +548,6 @@ impl DhallParser {
         Ok(input.as_str().to_owned())
     }
 
-    #[alias(path_component)]
     fn segment(input: ParseInput) -> ParseResult<String> {
         Ok(input.as_str().to_string())
     }
@@ -909,26 +908,19 @@ impl DhallParser {
         ))
     }
 
-    #[alias(record_type_or_literal)]
-    fn empty_record_literal(input: ParseInput) -> ParseResult<UnspannedExpr> {
-        Ok(RecordLit(Default::default()))
-    }
-
-    #[alias(record_type_or_literal)]
-    fn empty_record_type(input: ParseInput) -> ParseResult<UnspannedExpr> {
-        Ok(RecordType(Default::default()))
-    }
-
-    #[alias(record_type_or_literal)]
-    fn non_empty_record_type_or_literal(
-        input: ParseInput,
-    ) -> ParseResult<UnspannedExpr> {
+    fn record_type_or_literal(input: ParseInput) -> ParseResult<UnspannedExpr> {
         Ok(match_nodes!(input.children();
+            [empty_record_literal(_)] => RecordLit(Default::default()),
             [non_empty_record_type(map)] => RecordType(map),
             [non_empty_record_literal(map)] => RecordLit(map),
+            [] => RecordType(Default::default()),
         ))
     }
 
+    fn empty_record_literal(input: ParseInput) -> ParseResult<()> {
+        Ok(())
+    }
+
     fn non_empty_record_type(
         input: ParseInput,
     ) -> ParseResult<BTreeMap<Label, Expr>> {
@@ -997,8 +989,7 @@ impl DhallParser {
     }
 
     fn union_type(input: ParseInput) -> ParseResult<UnspannedExpr> {
-        let map = match_nodes!(input.children();
-            [empty_union_type(_)] => Default::default(),
+        Ok(match_nodes!(input.children();
             [union_type_entry(entries)..] => {
                 let mut map = BTreeMap::default();
                 for (l, t) in entries {
@@ -1015,14 +1006,9 @@ impl DhallParser {
                         }
                     }
                 }
-                map
+                UnionType(map)
             },
-        );
-        Ok(UnionType(map))
-    }
-
-    fn empty_union_type(_input: ParseInput) -> ParseResult<()> {
-        Ok(())
+        ))
     }
 
     fn union_type_entry(
@@ -1065,7 +1051,7 @@ pub fn parse_expr(input_str: &str) -> ParseResult<Expr> {
 }
 
 #[test]
-#[ignore]
+#[cfg_attr(windows, ignore)]
 // Check that the local copy of the grammar file is in sync with the one from dhall-lang.
 fn test_grammar_files_in_sync() {
     use std::process::Command;
@@ -1079,8 +1065,8 @@ fn test_grammar_files_in_sync() {
         .arg("--ignore-space-change")
         .arg("--color")
         .arg("--")
-        .arg(spec_abnf_path)
         .arg(local_abnf_path)
+        .arg(spec_abnf_path)
         .output()
         .expect("failed to run `git diff` command");
 
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index ccba385..8815d69 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -154,7 +154,9 @@ fn fmt_label(label: &Label, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         | "True" | "False" | "Some" => true,
         _ => Builtin::parse(&s).is_some(),
     };
-    if !is_reserved && s.chars().all(|c| c.is_ascii_alphanumeric()) {
+    if s.is_empty() {
+        write!(f, "``")
+    } else if !is_reserved && s.chars().all(|c| c.is_ascii_alphanumeric()) {
         write!(f, "{}", s)
     } else {
         write!(f, "`{}`", s)
diff --git a/dhall/tests/parser/failure/ProjectionByTypeNeedsParens.txt b/dhall/tests/parser/failure/ProjectionByTypeNeedsParens.txt
index 0586abb..3ce3b45 100644
--- a/dhall/tests/parser/failure/ProjectionByTypeNeedsParens.txt
+++ b/dhall/tests/parser/failure/ProjectionByTypeNeedsParens.txt
@@ -3,4 +3,4 @@
 1 | r.{ x: T }␊
   |     ^---
   |
-  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall
+  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall_keyword
diff --git a/dhall/tests/parser/failure/annotation.txt b/dhall/tests/parser/failure/annotation.txt
index 3390d3e..648ef2b 100644
--- a/dhall/tests/parser/failure/annotation.txt
+++ b/dhall/tests/parser/failure/annotation.txt
@@ -3,4 +3,4 @@
 1 | let a:Natural = 1 in a␊
   |     ^---
   |
-  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall
+  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall_keyword
diff --git a/dhall/tests/parser/failure/spacing/ForallNoSpace.txt b/dhall/tests/parser/failure/spacing/ForallNoSpace.txt
index 697d400..6bd7fbc 100644
--- a/dhall/tests/parser/failure/spacing/ForallNoSpace.txt
+++ b/dhall/tests/parser/failure/spacing/ForallNoSpace.txt
@@ -3,4 +3,4 @@
 1 | forall(x :T) -> x␊
   |        ^---
   |
-  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall
+  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall_keyword
diff --git a/dhall/tests/parser/failure/spacing/LambdaNoSpace.txt b/dhall/tests/parser/failure/spacing/LambdaNoSpace.txt
index adb0f1f..e5d1089 100644
--- a/dhall/tests/parser/failure/spacing/LambdaNoSpace.txt
+++ b/dhall/tests/parser/failure/spacing/LambdaNoSpace.txt
@@ -3,4 +3,4 @@
 1 | \(x :T) -> x␊
   |   ^---
   |
-  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall
+  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall_keyword
diff --git a/dhall/tests/parser/failure/spacing/LetAnnotNoSpace.txt b/dhall/tests/parser/failure/spacing/LetAnnotNoSpace.txt
index 577f157..06aef2d 100644
--- a/dhall/tests/parser/failure/spacing/LetAnnotNoSpace.txt
+++ b/dhall/tests/parser/failure/spacing/LetAnnotNoSpace.txt
@@ -3,4 +3,4 @@
 1 | let x :T = y in e␊
   |     ^---
   |
-  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall
+  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall_keyword
diff --git a/dhall/tests/parser/failure/spacing/MergeNoSpace2.txt b/dhall/tests/parser/failure/spacing/MergeNoSpace2.txt
index 77314e0..0fba8c0 100644
--- a/dhall/tests/parser/failure/spacing/MergeNoSpace2.txt
+++ b/dhall/tests/parser/failure/spacing/MergeNoSpace2.txt
@@ -3,4 +3,4 @@
 1 | merge x(y)␊
   |       ^---
   |
-  = expected missing, non_empty_list_literal, double_quote_literal, single_quote_literal, if_, merge, NaN, Some_, toMap, assert, forall, numeric_double_literal, minus_infinity_literal, plus_infinity_literal, natural_literal, integer_literal, or import_hashed
+  = expected missing, non_empty_list_literal, double_quote_literal, single_quote_literal, if_, merge, NaN, Some_, toMap, assert, forall_keyword, numeric_double_literal, minus_infinity_literal, plus_infinity_literal, natural_literal, integer_literal, or import_hashed
diff --git a/dhall/tests/parser/failure/spacing/RecordTypeNoSpace.txt b/dhall/tests/parser/failure/spacing/RecordTypeNoSpace.txt
index 0e1a879..759dd6f 100644
--- a/dhall/tests/parser/failure/spacing/RecordTypeNoSpace.txt
+++ b/dhall/tests/parser/failure/spacing/RecordTypeNoSpace.txt
@@ -3,4 +3,4 @@
 1 | { x :T }␊
   |   ^---
   |
-  = expected missing, if_, merge, NaN, Some_, toMap, assert, forall, empty_record_literal, or record_type_entry
+  = expected missing, record_type_entry, if_, merge, NaN, Some_, toMap, assert, forall_keyword, or empty_record_literal
diff --git a/dhall/tests/parser/failure/spacing/UnionTypeNoSpace.txt b/dhall/tests/parser/failure/spacing/UnionTypeNoSpace.txt
index 0a83dc8..8ff406c 100644
--- a/dhall/tests/parser/failure/spacing/UnionTypeNoSpace.txt
+++ b/dhall/tests/parser/failure/spacing/UnionTypeNoSpace.txt
@@ -3,4 +3,4 @@
 1 | < x :T >␊
   |   ^---
   |
-  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall
+  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall_keyword
diff --git a/dhall/tests/parser/failure/unit/OldUnionLitSyntax.txt b/dhall/tests/parser/failure/unit/OldUnionLitSyntax.txt
index 8475bb9..552a7c3 100644
--- a/dhall/tests/parser/failure/unit/OldUnionLitSyntax.txt
+++ b/dhall/tests/parser/failure/unit/OldUnionLitSyntax.txt
@@ -3,4 +3,4 @@
 1 | < x = 3 | y : Bool >␊
   |   ^---
   |
-  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall
+  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall_keyword
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword00.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword00.txt
new file mode 100644
index 0000000..9a8747b
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword00.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { if: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword01.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword01.txt
new file mode 100644
index 0000000..d041384
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword01.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { then: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword02.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword02.txt
new file mode 100644
index 0000000..2cdce47
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword02.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { else: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword03.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword03.txt
new file mode 100644
index 0000000..b8dd809
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword03.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { let: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword04.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword04.txt
new file mode 100644
index 0000000..4b2df06
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword04.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { in: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword05.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword05.txt
new file mode 100644
index 0000000..23d4f75
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword05.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { using: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword06.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword06.txt
new file mode 100644
index 0000000..4e715eb
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword06.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { missing: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword07.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword07.txt
new file mode 100644
index 0000000..420dc77
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword07.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { assert: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword08.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword08.txt
new file mode 100644
index 0000000..159e243
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword08.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { as: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword09.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword09.txt
new file mode 100644
index 0000000..f5b7130
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword09.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { Infinity: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword10.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword10.txt
new file mode 100644
index 0000000..dd6f552
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword10.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { NaN: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword11.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword11.txt
new file mode 100644
index 0000000..ccf18aa
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword11.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { merge: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword12.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword12.txt
new file mode 100644
index 0000000..f91f9dd
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword12.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { toMap: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword13.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword13.txt
new file mode 100644
index 0000000..be64d1f
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword13.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { with: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword14.txt b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword14.txt
new file mode 100644
index 0000000..9e2b836
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/RecordFieldMustNotBeKeyword14.txt
@@ -0,0 +1,6 @@
+ --> 1:3
+  |
+1 | { forall: Text }␊
+  |   ^---
+  |
+  = expected any_label_or_some or empty_record_literal
diff --git a/dhall/tests/parser/failure/unit/RecordLitPunDotted.txt b/dhall/tests/parser/failure/unit/RecordLitPunDotted.txt
index 2e0ac22..429aa05 100644
--- a/dhall/tests/parser/failure/unit/RecordLitPunDotted.txt
+++ b/dhall/tests/parser/failure/unit/RecordLitPunDotted.txt
@@ -3,4 +3,4 @@
 1 | { x.y.z }␊
   |       ^---
   |
-  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall
+  = expected missing, if_, merge, NaN, Some_, toMap, assert, or forall_keyword
diff --git a/dhall/tests/parser/failure/unit/UrlWithQuotedPath.txt b/dhall/tests/parser/failure/unit/UrlWithQuotedPath.txt
new file mode 100644
index 0000000..0b51f38
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/UrlWithQuotedPath.txt
@@ -0,0 +1,6 @@
+ --> 1:21
+  |
+1 | https://example.com/"a%20b"/c␊
+  |                     ^---
+  |
+  = expected EOI, import_alt, bool_or, natural_plus, text_append, list_append, bool_and, natural_times, bool_eq, bool_ne, combine, combine_types, equivalent, prefer, or arrow
diff --git a/dhall/tests/parser/failure/unit/WithPrecedence1.txt b/dhall/tests/parser/failure/unit/WithPrecedence1.txt
new file mode 100644
index 0000000..a1dfd31
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/WithPrecedence1.txt
@@ -0,0 +1,6 @@
+ --> 1:24
+  |
+1 | { x = 0 } // { y = 1 } with x = 1␊
+  |                        ^---
+  |
+  = expected EOI, import_alt, bool_or, natural_plus, text_append, list_append, bool_and, natural_times, bool_eq, bool_ne, combine, combine_types, equivalent, prefer, arrow, import_hashed, or primitive_expression
diff --git a/dhall/tests/parser/failure/unit/WithPrecedence2.txt b/dhall/tests/parser/failure/unit/WithPrecedence2.txt
new file mode 100644
index 0000000..fefd172
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/WithPrecedence2.txt
@@ -0,0 +1,6 @@
+ --> 1:15
+  |
+1 | foo { x = 0 } with x = 1␊
+  |               ^---
+  |
+  = expected EOI, import_alt, bool_or, natural_plus, text_append, list_append, bool_and, natural_times, bool_eq, bool_ne, combine, combine_types, equivalent, prefer, arrow, import_hashed, or primitive_expression
diff --git a/dhall/tests/parser/failure/unit/WithPrecedence3.txt b/dhall/tests/parser/failure/unit/WithPrecedence3.txt
new file mode 100644
index 0000000..418c669
--- /dev/null
+++ b/dhall/tests/parser/failure/unit/WithPrecedence3.txt
@@ -0,0 +1,6 @@
+ --> 1:22
+  |
+1 | { x = 0 } with x = 1 : T␊
+  |                      ^---
+  |
+  = expected EOI, import_alt, bool_or, natural_plus, text_append, list_append, bool_and, natural_times, bool_eq, bool_ne, combine, combine_types, equivalent, prefer, import_hashed, or primitive_expression
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/parser/success/quotedLabelB.txt b/dhall/tests/parser/success/quotedLabelB.txt
index 861ae0b..f8175de 100644
--- a/dhall/tests/parser/success/quotedLabelB.txt
+++ b/dhall/tests/parser/success/quotedLabelB.txt
@@ -1 +1 @@
-{ example1 = let `let` = 1 in `let`, example2 = let `:.` = 1 in `:.`, example3 = let `$ref` = 1 in `$ref` }
+{ example1 = let `let` = 1 in `let`, example2 = let `:.` = 1 in `:.`, example3 = let `$ref` = 1 in `$ref`, example4 = let `` = 1 in `` }
diff --git a/dhall/tests/parser/success/quotedRecordLabelB.txt b/dhall/tests/parser/success/quotedRecordLabelB.txt
new file mode 100644
index 0000000..6e5a76b
--- /dev/null
+++ b/dhall/tests/parser/success/quotedRecordLabelB.txt
@@ -0,0 +1 @@
+{ `` = 2, ` ` = 3, foo = 1 }
diff --git a/dhall/tests/parser/success/quotedUnionLabelB.txt b/dhall/tests/parser/success/quotedUnionLabelB.txt
new file mode 100644
index 0000000..1974ec2
--- /dev/null
+++ b/dhall/tests/parser/success/quotedUnionLabelB.txt
@@ -0,0 +1 @@
+< ``: Natural | ` `: Natural | foo: Natural >
diff --git a/dhall/tests/parser/success/unit/DoubleLit16bitB.txt b/dhall/tests/parser/success/unit/DoubleLit16bitB.txt
new file mode 100644
index 0000000..9ad974f
--- /dev/null
+++ b/dhall/tests/parser/success/unit/DoubleLit16bitB.txt
@@ -0,0 +1 @@
+5.5
diff --git a/dhall/tests/parser/success/unit/DoubleLit32bitB.txt b/dhall/tests/parser/success/unit/DoubleLit32bitB.txt
new file mode 100644
index 0000000..f67efa2
--- /dev/null
+++ b/dhall/tests/parser/success/unit/DoubleLit32bitB.txt
@@ -0,0 +1 @@
+5555.5
diff --git a/dhall/tests/parser/success/unit/DoubleLit64bitB.txt b/dhall/tests/parser/success/unit/DoubleLit64bitB.txt
new file mode 100644
index 0000000..f3714c3
--- /dev/null
+++ b/dhall/tests/parser/success/unit/DoubleLit64bitB.txt
@@ -0,0 +1 @@
+55555555555.5
diff --git a/dhall/tests/parser/success/unit/WithPrecedenceB.txt b/dhall/tests/parser/success/unit/WithPrecedence1B.txt
index 5f22335..5f22335 100644
--- a/dhall/tests/parser/success/unit/WithPrecedenceB.txt
+++ b/dhall/tests/parser/success/unit/WithPrecedence1B.txt
diff --git a/dhall/tests/parser/success/unit/WithPrecedence2B.txt b/dhall/tests/parser/success/unit/WithPrecedence2B.txt
new file mode 100644
index 0000000..f945cc9
--- /dev/null
+++ b/dhall/tests/parser/success/unit/WithPrecedence2B.txt
@@ -0,0 +1 @@
+{ x = 0 } ⫽ { x = 1 + 1 }
diff --git a/dhall/tests/parser/success/unit/WithPrecedence3B.txt b/dhall/tests/parser/success/unit/WithPrecedence3B.txt
new file mode 100644
index 0000000..a801b24
--- /dev/null
+++ b/dhall/tests/parser/success/unit/WithPrecedence3B.txt
@@ -0,0 +1 @@
+foo::{ x = 0 } ⫽ { x = 1 }
diff --git a/dhall/tests/parser/success/unit/import/quotedPathsB.txt b/dhall/tests/parser/success/unit/import/quotedPathsB.txt
index 4705ca3..373b872 100644
--- a/dhall/tests/parser/success/unit/import/quotedPathsB.txt
+++ b/dhall/tests/parser/success/unit/import/quotedPathsB.txt
@@ -1 +1 @@
-{ example0 = /foo/bar/"baz qux", example1 = https://example.com/foo/bar%3Fbaz?qux }
+/foo/bar/"baz qux"
diff --git a/dhall/tests/parser/success/unit/import/urls/quotedPathFakeUrlEncodeB.txt b/dhall/tests/parser/success/unit/import/urls/quotedPathFakeUrlEncodeB.txt
deleted file mode 100644
index a8366d2..0000000
--- a/dhall/tests/parser/success/unit/import/urls/quotedPathFakeUrlEncodeB.txt
+++ /dev/null
@@ -1 +0,0 @@
-https://example.com/a%20b/c
diff --git a/dhall/tests/parser/success/unit/operators/PrecedenceEquivalenceB.txt b/dhall/tests/parser/success/unit/operators/PrecedenceEquivalenceB.txt
new file mode 100644
index 0000000..717c108
--- /dev/null
+++ b/dhall/tests/parser/success/unit/operators/PrecedenceEquivalenceB.txt
@@ -0,0 +1 @@
+2 + 3 * 4 ≡ 4 * 3 + 2
diff --git a/dhall/tests/spec.rs b/dhall/tests/spec.rs
index 37df91d..77d2aaa 100644
--- a/dhall/tests/spec.rs
+++ b/dhall/tests/spec.rs
@@ -51,7 +51,7 @@ impl FileType {
         match self {
             FileType::Text => TestFile::Source(file),
             FileType::Binary => TestFile::Binary(file),
-            FileType::Hash => TestFile::Binary(file),
+            FileType::Hash => TestFile::UI(file),
             FileType::UI => TestFile::UI(file),
         }
     }
@@ -413,11 +413,6 @@ fn define_features() -> Vec<TestFeature> {
             directory: "parser/success/",
             variant: SpecTestKind::ParserSuccess,
             too_slow_path: Rc::new(|path: &str| path == "largeExpression"),
-            exclude_path: Rc::new(|path: &str| {
-                false
-                    // Pretty sure the test is incorrect
-                    || path == "unit/import/urls/quotedPathFakeUrlEncode"
-            }),
             output_type: FileType::Binary,
             ..default_feature.clone()
         },
@@ -445,15 +440,6 @@ fn define_features() -> Vec<TestFeature> {
             directory: "parser/success/",
             variant: SpecTestKind::BinaryEncoding,
             too_slow_path: Rc::new(|path: &str| path == "largeExpression"),
-            exclude_path: Rc::new(|path: &str| {
-                false
-                    // Pretty sure the test is incorrect
-                    || path == "unit/import/urls/quotedPathFakeUrlEncode"
-                    // See https://github.com/pyfisch/cbor/issues/109
-                    || path == "double"
-                    || path == "unit/DoubleLitExponentNoDot"
-                    || path == "unit/DoubleLitSecretelyInt"
-            }),
             output_type: FileType::Binary,
             ..default_feature.clone()
         },
@@ -493,6 +479,7 @@ fn define_features() -> Vec<TestFeature> {
                     || path == "noHeaderForwarding"
                     // TODO: git changes newlines on windows
                     || (cfg!(windows) && path == "unit/AsText")
+                    || (cfg!(windows) && path == "unit/QuotedPath")
                     // TODO: paths on windows have backslashes; this breaks all the `as Location` tests
                     // See https://github.com/dhall-lang/dhall-lang/issues/1032
                     || (cfg!(windows) && path.contains("asLocation"))
@@ -518,13 +505,8 @@ fn define_features() -> Vec<TestFeature> {
             directory: "semantic-hash/success/",
             variant: SpecTestKind::SemanticHash,
             exclude_path: Rc::new(|path: &str| {
-                false
-                    // We don't support bignums
-                    || path == "simple/integerToDouble"
-                    // See https://github.com/pyfisch/cbor/issues/109
-                    || path == "prelude/Integer/toDouble/0"
-                    || path == "prelude/Integer/toDouble/1"
-                    || path == "prelude/Natural/toDouble/0"
+                // We don't support bignums
+                path == "simple/integerToDouble"
             }),
             output_type: FileType::Hash,
             ..default_feature.clone()
@@ -559,7 +541,9 @@ fn define_features() -> Vec<TestFeature> {
             module_name: "type_inference_success",
             directory: "type-inference/success/",
             variant: SpecTestKind::TypeInferenceSuccess,
-            too_slow_path: Rc::new(|path: &str| path == "prelude"),
+            // TODO: this fails because of caching shenanigans
+            // too_slow_path: Rc::new(|path: &str| path == "prelude"),
+            exclude_path: Rc::new(|path: &str| path == "prelude"),
             ..default_feature.clone()
         },
         TestFeature {
@@ -614,6 +598,17 @@ fn run_test(test: &SpecTest) -> Result<()> {
     // Set environment variable for import tests.
     env::set_var("DHALL_TEST_VAR", "6 * 7");
 
+    // Configure cache for import tests
+    env::set_var(
+        "XDG_CACHE_HOME",
+        root_dir
+            .join("dhall-lang")
+            .join("tests")
+            .join("import")
+            .join("cache")
+            .as_path(),
+    );
+
     let SpecTest {
         input: expr,
         output: expected,
@@ -662,16 +657,6 @@ fn run_test(test: &SpecTest) -> Result<()> {
             expected.compare_ui(parsed)?;
         }
         ImportSuccess => {
-            // Configure cache for import tests
-            env::set_var(
-                "XDG_CACHE_HOME",
-                root_dir
-                    .join("dhall-lang")
-                    .join("tests")
-                    .join("import")
-                    .join("cache")
-                    .as_path(),
-            );
             let expr = expr.normalize()?;
             expected.compare(expr)?;
         }
diff --git a/dhall/tests/type-inference/failure/mixedUnions.txt b/dhall/tests/type-inference/failure/mixedUnions.txt
deleted file mode 100644
index 2b307d0..0000000
--- a/dhall/tests/type-inference/failure/mixedUnions.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidVariantType
- --> <current file>:1:28
-  |
-1 | < Left : Natural | Right : Type >
-  |                            ^^^^ InvalidVariantType
-  |
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/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
deleted file mode 100644
index a83bb4f..0000000
--- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:17
-  |
-1 | { x = Type, y = Kind }
-  |                 ^^^^ InvalidFieldType
-  |
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
+  |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
deleted file mode 100644
index 6a6da80..0000000
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:22
-  |
-1 | { x = Bool } ⫽ { x = Kind }
-  |                      ^^^^ InvalidFieldType
-  |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
deleted file mode 100644
index 322e7f4..0000000
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:21
-  |
-1 | { x = {=} } ⫽ { x = Kind }
-  |                     ^^^^ InvalidFieldType
-  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt
deleted file mode 100644
index ae6c845..0000000
--- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidVariantType
- --> <current file>:1:18
-  |
-1 | < x : Bool | y : Type >
-  |                  ^^^^ InvalidVariantType
-  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt
deleted file mode 100644
index faf81a9..0000000
--- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidVariantType
- --> <current file>:1:18
-  |
-1 | < x : Kind | y : Type >
-  |                  ^^^^ InvalidVariantType
-  |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt
deleted file mode 100644
index bbfb1f3..0000000
--- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Type error: error: InvalidVariantType
- --> <current file>:1:18
-  |
-1 | < x : Kind | y : Bool >
-  |                  ^^^^ InvalidVariantType
-  |