Merge pull request #98 from Nadrieril/catchup-spec

Catchup spec

16 files changed, 146 insertions, 131 deletions

diff --git a/dhall-lang b/dhall-lang
-Subproject 9f259cd68870b912fbf2f2a08cd63dc3ccba9dc
+Subproject fb1c41ddec1d35dadd89a70780698e1a73e179b
diff --git a/dhall/build.rs b/dhall/build.rs
index b6df3d0..8b23dd9 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -94,8 +94,12 @@ fn main() -> std::io::Result<()> {
         // Too slow in debug mode
         path == "success/largeExpression"
             // TODO: Inline headers
-            || path == "success/unit/import/parenthesizeUsing"
             || path == "success/unit/import/inlineUsing"
+            || path == "success/unit/import/Headers"
+            || path == "success/unit/import/HeadersDoubleHash"
+            || path == "success/unit/import/HeadersDoubleHashPrecedence"
+            || path == "success/unit/import/HeadersHashPrecedence"
+            || path == "success/unit/import/HeadersInteriorHash"
             // TODO: projection by expression
             || path == "success/recordProjectionByExpression"
             || path == "success/RecordProjectionByType"
@@ -117,6 +121,7 @@ fn main() -> std::io::Result<()> {
             || path == "success/largeExpression"
             // TODO: Inline headers
             || path == "success/unit/import/inlineUsing"
+            || path == "success/unit/import/Headers"
             // TODO: projection by expression
             || path == "success/recordProjectionByExpression"
             || path == "success/RecordProjectionByType"
@@ -140,13 +145,13 @@ fn main() -> std::io::Result<()> {
             path.starts_with("failure/")
             // Too slow in debug mode
             || path == "success/largeExpression"
-            // Too much of a pain to implement; shouldn't make a difference
-            // since lets disappear on normalization.
-            || path == "success/multilet"
             // See https://github.com/pyfisch/cbor/issues/109
             || path == "success/double"
+            || path == "success/unit/DoubleLitExponentNoDot"
+            || path == "success/unit/DoubleLitSecretelyInt"
             // TODO: Inline headers
             || path == "success/unit/import/inlineUsing"
+            || path == "success/unit/import/Headers"
             // TODO: projection by expression
             || path == "success/recordProjectionByExpression"
             || path == "success/RecordProjectionByType"
@@ -199,7 +204,7 @@ fn main() -> std::io::Result<()> {
             || path == "success/unit/EmptyToMap"
             || path == "success/unit/ToMap"
             || path == "success/unit/ToMapWithType"
-            // Normalize field selection further by inspecting the argument
+            // TODO: Normalize field selection further by inspecting the argument
             || path == "success/simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection0"
             || path == "success/simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection1"
             || path == "success/simplifications/rightBiasedMergeWithinRecursiveRecordMergeWithinFieldselection"
@@ -208,9 +213,12 @@ fn main() -> std::io::Result<()> {
             || path == "success/unit/RecursiveRecordMergeWithinFieldSelection0"
             || path == "success/unit/RecursiveRecordMergeWithinFieldSelection1"
             || path == "success/unit/RecursiveRecordMergeWithinFieldSelection2"
+            || path == "success/unit/RecursiveRecordMergeWithinFieldSelection3"
             || path == "success/unit/RightBiasedMergeWithinFieldSelection0"
             || path == "success/unit/RightBiasedMergeWithinFieldSelection1"
             || path == "success/unit/RightBiasedMergeWithinFieldSelection2"
+            || path == "success/unit/RightBiasedMergeWithinFieldSelection3"
+            || path == "success/unit/RightBiasedMergeEquivalentArguments"
         },
     )?;
 
@@ -229,7 +237,10 @@ fn main() -> std::io::Result<()> {
         "Typecheck",
         |path| {
             false
+            // TODO: Enable imports in typecheck tests
             || path == "failure/importBoundary"
+            // Too slow
+            || path == "success/prelude"
             // TODO: Inline headers
             || path == "failure/customHeadersUsingBoundVariable"
             // TODO: projection by expression
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 5c569e1..5bc25f2 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -221,6 +221,10 @@ impl TypeThunk {
         self.0.to_type()
     }
 
+    pub fn to_typed(&self) -> Typed {
+        self.0.clone()
+    }
+
     pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
         self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
     }
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index d7b9149..26568b5 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -47,7 +47,7 @@ pub enum Value {
     DoubleLit(NaiveDouble),
     EmptyOptionalLit(TypeThunk),
     NEOptionalLit(Thunk),
-    // EmptyListLit(t) means `[] : List t`
+    // EmptyListLit(t) means `[] : List t`, not `[] : t`
     EmptyListLit(TypeThunk),
     NEListLit(Vec<Thunk>),
     RecordLit(HashMap<Label, Thunk>),
@@ -58,6 +58,7 @@ pub enum Value {
     // Invariant: this must not contain interpolations that are themselves TextLits, and
     // contiguous text values must be merged.
     TextLit(Vec<InterpolatedTextContents<Thunk>>),
+    Equivalence(TypeThunk, TypeThunk),
     // Invariant: this must not contain a value captured by one of the variants above.
     PartialExpr(ExprF<Thunk, X>),
 }
@@ -196,6 +197,11 @@ impl Value {
                         .collect(),
                 ))
             }
+            Value::Equivalence(x, y) => rc(ExprF::BinOp(
+                dhall_syntax::BinOp::Equivalence,
+                x.normalize_to_expr_maybe_alpha(alpha),
+                y.normalize_to_expr_maybe_alpha(alpha),
+            )),
             Value::PartialExpr(e) => {
                 rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha)))
             }
@@ -282,6 +288,10 @@ impl Value {
                     }
                 }
             }
+            Value::Equivalence(x, y) => {
+                x.normalize_mut();
+                y.normalize_mut();
+            }
             Value::PartialExpr(e) => {
                 // TODO: need map_mut_simple
                 e.map_ref_simple(|v| {
@@ -418,6 +428,9 @@ impl Shift for Value {
                     })
                     .collect::<Result<_, _>>()?,
             ),
+            Value::Equivalence(x, y) => {
+                Value::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
+            }
             Value::PartialExpr(e) => Value::PartialExpr(
                 e.traverse_ref_with_special_handling_of_binders(
                     |v| Ok(v.shift(delta, var)?),
@@ -533,6 +546,10 @@ impl Subst<Typed> for Value {
                     })
                     .collect(),
             ),
+            Value::Equivalence(x, y) => Value::Equivalence(
+                x.subst_shift(var, val),
+                y.subst_shift(var, val),
+            ),
         }
     }
 }
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index a0ee30a..3c00017 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -68,7 +68,6 @@ pub(crate) enum TypeMessage {
     MissingRecordField(Label, Typed),
     MissingUnionField(Label, Normalized),
     BinOpTypeMismatch(BinOp, Typed),
-    NoDependentTypes(Normalized, Normalized),
     InvalidTextInterpolation(Typed),
     Merge1ArgMustBeRecord(Typed),
     Merge2ArgMustBeUnion(Typed),
@@ -86,7 +85,10 @@ pub(crate) enum TypeMessage {
     RecordTypeMergeRequiresRecordType(Type),
     RecordTypeMismatch(Type, Type, Type, Type),
     UnionTypeDuplicateField,
-    // Unimplemented,
+    EquivalenceArgumentMustBeTerm(bool, Typed),
+    EquivalenceTypeMismatch(Typed, Typed),
+    AssertMismatch(Typed, Typed),
+    AssertMustTakeEquivalence,
 }
 
 impl TypeError {
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 5e7eb40..f4a9cc1 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -119,6 +119,7 @@ fn cbor_value_to_dhall(
                     9 => RightBiasedRecordMerge,
                     10 => RecursiveRecordTypeMerge,
                     11 => ImportAlt,
+                    12 => Equivalence,
                     _ => {
                         Err(DecodeError::WrongFormatError("binop".to_owned()))?
                     }
@@ -177,6 +178,19 @@ fn cbor_value_to_dhall(
                 let l = Label::from(l.as_str());
                 Field(x, l)
             }
+            [U64(10), x, rest..] => {
+                let x = cbor_value_to_dhall(&x)?;
+                let labels = rest
+                    .iter()
+                    .map(|s| match s {
+                        String(s) => Ok(Label::from(s.as_str())),
+                        _ => Err(DecodeError::WrongFormatError(
+                            "projection".to_owned(),
+                        )),
+                    })
+                    .collect::<Result<_, _>>()?;
+                Projection(x, labels)
+            }
             [U64(11), Object(map)] => {
                 let map = cbor_map_to_dhall_opt_map(map)?;
                 UnionType(map)
@@ -211,6 +225,10 @@ fn cbor_value_to_dhall(
                         .collect::<Result<_, _>>()?,
                 )))
             }
+            [U64(19), t] => {
+                let t = cbor_value_to_dhall(&t)?;
+                Assert(t)
+            }
             [U64(24), hash, U64(mode), U64(scheme), rest..] => {
                 let mode = match mode {
                     0 => ImportMode::Code,
@@ -504,6 +522,7 @@ where
             )
         }
         Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)),
+        Assert(x) => ser_seq!(ser; tag(19), expr(x)),
         SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)),
         EmptyListLit(x) => match x.as_ref() {
             App(f, a) => match f.as_ref() {
@@ -541,6 +560,7 @@ where
                 RightBiasedRecordMerge => 9,
                 RecursiveRecordTypeMerge => 10,
                 ImportAlt => 11,
+                Equivalence => 12,
             };
             ser_seq!(ser; tag(3), U64(op), expr(x), expr(y))
         }
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 395cf28..405677a 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -54,6 +54,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                 }
                 (NaturalLit(0), b) => Ok((r, b.clone())),
                 (_, NaturalLit(0)) => Ok((r, NaturalLit(0))),
+                _ if a == b => Ok((r, NaturalLit(0))),
                 _ => Err(()),
             }
         }
@@ -508,9 +509,9 @@ where
 
 fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
     use BinOp::{
-        BoolAnd, BoolEQ, BoolNE, BoolOr, ListAppend, NaturalPlus, NaturalTimes,
-        RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge,
-        TextAppend,
+        BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
+        NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
+        RightBiasedRecordMerge, TextAppend,
     };
     use Value::{
         BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
@@ -626,6 +627,11 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
             Ret::Value(RecordType(kvs))
         }
 
+        (Equivalence, _, _) => Ret::Value(Value::Equivalence(
+            TypeThunk::from_thunk(x.clone()),
+            TypeThunk::from_thunk(y.clone()),
+        )),
+
         _ => return None,
     })
 }
@@ -641,6 +647,7 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
         ExprF::Embed(_) => unreachable!(),
         ExprF::Var(_) => unreachable!(),
         ExprF::Annot(x, _) => Ret::Thunk(x),
+        ExprF::Assert(_) => Ret::Expr(expr),
         ExprF::Lam(x, t, e) => {
             Ret::Value(Lam(x.into(), TypeThunk::from_thunk(t), e))
         }
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 2e4642c..297a096 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -60,18 +60,7 @@ fn tck_pi_type(
         }
     };
 
-    let k = match function_check(ka, kb) {
-        Ok(k) => k,
-        Err(()) => {
-            return Err(TypeError::new(
-                ctx,
-                NoDependentTypes(
-                    tx.to_normalized(),
-                    te.get_type()?.to_normalized(),
-                ),
-            ))
-        }
-    };
+    let k = function_check(ka, kb);
 
     Ok(Typed::from_thunk_and_type(
         Value::Pi(x.into(), TypeThunk::from_type(tx), TypeThunk::from_type(te))
@@ -164,14 +153,13 @@ fn tck_union_type(
     ))
 }
 
-fn function_check(a: Const, b: Const) -> Result<Const, ()> {
-    use dhall_syntax::Const::*;
-    match (a, b) {
-        (_, Type) => Ok(Type),
-        (Kind, Kind) => Ok(Kind),
-        (Sort, Sort) => Ok(Sort),
-        (Sort, Kind) => Ok(Sort),
-        _ => Err(()),
+fn function_check(a: Const, b: Const) -> Const {
+    use dhall_syntax::Const::Type;
+    use std::cmp::max;
+    if b == Type {
+        Type
+    } else {
+        max(a, b)
     }
 }
 
@@ -403,6 +391,19 @@ fn type_last_layer(
             );
             Ok(RetTypeOnly(x.get_type()?.into_owned()))
         }
+        Assert(t) => {
+            match t.to_value() {
+                Value::Equivalence(x, y) if x == y => {}
+                Value::Equivalence(x, y) => {
+                    return Err(mkerr(AssertMismatch(
+                        x.to_typed(),
+                        y.to_typed(),
+                    )))
+                }
+                _ => return Err(mkerr(AssertMustTakeEquivalence)),
+            }
+            Ok(RetTypeOnly(t.to_type()))
+        }
         BoolIf(x, y, z) => {
             ensure_equal!(
                 x.get_type()?,
@@ -807,6 +808,24 @@ fn type_last_layer(
 
             Ok(RetTypeOnly(l.get_type()?.into_owned()))
         }
+        BinOp(Equivalence, l, r) => {
+            ensure_simple_type!(
+                l.get_type()?,
+                mkerr(EquivalenceArgumentMustBeTerm(true, l.clone())),
+            );
+            ensure_simple_type!(
+                r.get_type()?,
+                mkerr(EquivalenceArgumentMustBeTerm(false, r.clone())),
+            );
+
+            ensure_equal!(
+                l.get_type()?,
+                r.get_type()?,
+                mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()))
+            );
+
+            Ok(RetTypeOnly(Type::from_const(dhall_syntax::Const::Type)))
+        }
         BinOp(o, l, r) => {
             let t = builtin_to_type(match o {
                 BoolAnd => Bool,
@@ -821,6 +840,7 @@ fn type_last_layer(
                 RecursiveRecordMerge => unreachable!(),
                 RecursiveRecordTypeMerge => unreachable!(),
                 ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"),
+                Equivalence => unreachable!(),
             })?;
 
             ensure_equal!(
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 9784eec..15bc97a 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -107,6 +107,7 @@ pub fn run_test(
 
             match feature {
                 Parser => {
+                    // This exercices both parsing and binary decoding
                     // Compare parse/decoded
                     let expected_file_path = base_path + "B.dhallb";
                     let expected_file_path = PathBuf::from(&expected_file_path);
diff --git a/dhall_generated_parser/build.rs b/dhall_generated_parser/build.rs
index 74210bf..48605b6 100644
--- a/dhall_generated_parser/build.rs
+++ b/dhall_generated_parser/build.rs
@@ -67,6 +67,7 @@ fn main() -> std::io::Result<()> {
           | merge ~ whsp1 ~ import_expression ~ whsp1 ~ import_expression ~ whsp ~ ^":" ~ whsp1 ~ application_expression
           | empty_list_literal
           | toMap ~ whsp1 ~ import_expression ~ whsp ~ ^":" ~ whsp1 ~ application_expression
+          | assert ~ whsp ~ ^":" ~ whsp1 ~ expression
           | annotated_expression
     }}"#
     )?;
diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility
index de6dc8d..44a52c1 100644
--- a/dhall_generated_parser/src/dhall.pest.visibility
+++ b/dhall_generated_parser/src/dhall.pest.visibility
@@ -46,6 +46,7 @@ missing
 NaN
 Some_
 toMap
+assert
 # keyword
 builtin
 Optional
@@ -85,6 +86,7 @@ Location
 # Text_show
 # combine
 # combine_types
+# equivalent
 # prefer
 lambda
 forall
@@ -154,6 +156,7 @@ combine_types_expression
 times_expression
 equal_expression
 not_equal_expression
+equivalent_expression
 application_expression
 first_application_expression
 # import_expression
diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index b293357..6522cb1 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -44,7 +44,7 @@ impl From<NaiveDouble> for f64 {
 }
 
 /// Constants for a pure type system
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
 pub enum Const {
     Type,
     Kind,
@@ -99,6 +99,8 @@ pub enum BinOp {
     BoolEQ,
     /// `x != y`
     BoolNE,
+    /// x === y
+    Equivalence,
 }
 
 /// Built-ins
@@ -175,6 +177,8 @@ pub enum ExprF<SubExpr, Embed> {
     Let(Label, Option<SubExpr>, SubExpr, SubExpr),
     ///  `x : t`
     Annot(SubExpr, SubExpr),
+    ///  `assert : t`
+    Assert(SubExpr),
     /// Built-in values
     Builtin(Builtin),
     // Binary operations
diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs
index 68ad956..18f76d9 100644
--- a/dhall_syntax/src/core/visitor.rs
+++ b/dhall_syntax/src/core/visitor.rs
@@ -148,6 +148,7 @@ where
             ),
             Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
             Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
+            Assert(e) => Assert(v.visit_subexpr(e)?),
             Embed(a) => return v.visit_embed_squash(a),
         })
     }
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 72dfcdd..9ae6dc8 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -311,6 +311,7 @@ fn can_be_shortcutted(rule: Rule) -> bool {
         | times_expression
         | equal_expression
         | not_equal_expression
+        | equivalent_expression
         | application_expression
         | first_application_expression
         | selector_expression
@@ -744,6 +745,7 @@ make_parser! {
     token_rule!(forall<()>);
     token_rule!(arrow<()>);
     token_rule!(merge<()>);
+    token_rule!(assert<()>);
     token_rule!(if_<()>);
     token_rule!(in_<()>);
 
@@ -777,6 +779,9 @@ make_parser! {
         [merge(()), expression(x), expression(y), expression(z)] => {
             spanned(span, Merge(x, y, Some(z)))
         },
+        [assert(()), expression(x)] => {
+            spanned(span, Assert(x))
+        },
         [expression(e)] => e,
     ));
 
@@ -875,6 +880,13 @@ make_parser! {
             rest.fold(first, |acc, e| unspanned(BinOp(o, acc, e)))
         },
     ));
+    rule!(equivalent_expression<ParsedSubExpr> as expression; children!(
+        [expression(e)] => e,
+        [expression(first), expression(rest)..] => {
+            let o = crate::BinOp::Equivalence;
+            rest.fold(first, |acc, e| unspanned(BinOp(o, acc, e)))
+        },
+    ));
 
     rule!(annotated_expression<ParsedSubExpr> as expression; span; children!(
         [expression(e)] => e,
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 1d6c113..70b224e 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -44,6 +44,9 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
             Annot(a, b) => {
                 write!(f, "{} : {}", a, b)?;
             }
+            Assert(a) => {
+                write!(f, "assert : {}", a)?;
+            }
             ExprF::BinOp(op, a, b) => {
                 write!(f, "{} {} {}", a, op, b)?;
             }
@@ -286,6 +289,7 @@ impl Display for BinOp {
             ImportAlt => "?",
             RightBiasedRecordMerge => "⫽",
             ListAppend => "#",
+            Equivalence => "≡",
         })
     }
 }
diff --git a/tests_buffer b/tests_buffer
index ca578e4..c6366ba 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -2,90 +2,15 @@ parser:
 ./a%20b
 ./"a%20b"
 text interpolation and escapes
-remove `double`
-remove imports/parenthesizeUsing
-remove multilet
-selection by expression unit tests
-split aslocation test into actual unit tests
+projection by expression unit tests
 success/
-    imports/
-        Missing missing
-        Headers https://example.com/foo using ./headers
-        HeadersInteriorHash https://example.com/foo using (./headers sha256:0000000000000000000000000000000000000000000000000000000000000000)
-        HeadersExteriorHash (https://example.com/foo using ./headers) sha256:0000000000000000000000000000000000000000000000000000000000000000
-        HeadersHashPrecedence https://example.com/foo using ./headers sha256:0000000000000000000000000000000000000000000000000000000000000000
-        HeadersDoubleHashPrecedence https://example.com/foo using ./headers sha256:0000000000000000000000000000000000000000000000000000000000000000 sha256:1111111111111111111111111111111111111111111111111111111111111111
-    DoubleLitPositive 1.23
-    DoubleLitNegative -1.23
-    DoubleLitExponent 1.23e4
-    DoubleLitExponentNoDot 1e4
-    DoubleLitExponentNegative 1.23e-4
-    DoubleLitInfinity Infinity
-    DoubleLitNegInfinity -Infinity
-    DoubleLitNaN NaN
-    DoubleLitSecretelyInt 1.0
-    DoubleLitZero 0.0
-    BuiltinListBuild List/Build
-    FunctionApplicationOneArg f x
-    FunctionApplicationMultipleArgs f x y z
-    Annotation x : T
-    ListLitNonEmpty [x, y]
-    ListLitNonEmptyAnnotated [x, y] : List T
-    OptionalLitEmpty []: Optional T
-    OptionalLitNonEmpty [x]: Optional T
-    Field r.x
-    FieldBuiltinName r.List
-    FieldQuoted r.`x`
-    Projection r.{x, y, z}
-    Let let x: T = v in e
-    LetNested let x: T = v in let y: U = w in e
-    LetMulti let x: T = v let y: U = w in e
-    LambdaUnicode λ(x : T) -> y
-    FunctionTypePi forall(x: T) -> U
-    FunctionTypePiUnicode ∀(x: T) -> U
-    FunctionTypePiNested forall(x: T) -> ∀(y: U) -> V
-    FunctionTypePiUnderscore forall(_: T) -> U
-    FunctionTypeArrow T -> U
-    RecordLit { x = 1, y = 2 }
-    RecordType { x: T, y: U }
     operators/
-        ImportAlt x ? y
-        ImportAltAssoc w ? x ? y ? z
-        BoolOr x || y
-        BoolOrAssoc w || x || y || z
-        NaturalPlus x + y
-        NaturalPlusAssoc w + x + y + z
-        TextAppend x ++ y
-        TextAppendAssoc w ++ x ++ y ++ z
-        ListAppend x # y
-        ListAppendAssoc w # x # y # z
-        BoolAnd x && y
-        BoolAndAssoc w && x && y && z
-        NaturalTimes x * y
-        NaturalTimesAssoc w * x * y * z
-        BoolEQ x == y
-        BoolEQAssoc w == x == y == z
-        BoolNE x != y
-        BoolNEAssoc w != x != y != z
-        RecursiveRecordMerge x //\\ y
-        RecursiveRecordMergeAssoc w //\\ x //\\ y //\\ z
-        RecursiveRecordTypeMerge x /\ y
-        RecursiveRecordTypeMergeAssoc w /\ x /\ y /\ z
-        RightBiasedRecordMerge x // y
-        RightBiasedRecordMergeAssoc w // x // y // z
-        RecursiveRecordMergeUnicode x ∧ y
-        RecursiveRecordMergeUnicodeAssoc w ∧ x /\ y ∧ z
-        RightBiasedRecordMergeUnicode x ⫽ y
-        RightBiasedRecordMergeUnicodeAssoc w ⫽ x // y ⫽ z
-        RecursiveRecordTypeMergeUnicode x ⩓ y
-        RecursiveRecordTypeMergeUnicodeAssoc w ⩓ x //\\ y ⩓ z
         PrecedenceAll1 a ? b || c + d ++ e # f && g ∧ h ⫽ i ⩓ j * k == l != m n.o
         PrecedenceAll2 a b != c == d * e ⩓ f ⫽ g ∧ h && i # j ++ k + l || m ? n
-        PrecedenceNat a + b * d + e f * (g + h)
-        PrecedenceBool a && b || c d == e || f != g && h || i
-        PrecedenceRecord a // b c /\ d ⫽ e.{x} ∧ f
+    LetNoAnnot let x = y in e
+    LetAnnot let x: T = y in e
 failure/
-    ProjectionByExpressionNeedsParens r.{ x: T }
+    AssertNoAnnotation assert
 
 binary decoding:
 decode old-style optional literals ?
@@ -99,39 +24,22 @@ failure/
 
 normalization:
 variables across import boundaries
-Text/show ""
-Double/show -1.5e-10
+    Text/show ""
     TextLitNested1 "${""}${x}"
     TextLitNested2 "${"${x}"}"
     TextLitNested3 "${"${""}"}${x}"
-    EquivalenceDouble if b then NaN else NaN
-    EquivalenceAlpha if b then \(x: T) -> x else \(y: T) -> y
 
 typecheck:
 something that involves destructuring a recordtype after merge
 add some of the more complicated Prelude tests back, like List/enumerate
 failure on old-style optional literal
-success/
-    MergeEmptyAlternative merge { x = 1 } < x >.x
-    MergeTrickyShadowing let _ = Bool in merge {_ = \(x: _) -> x} (<_: Bool>._ True)
-    EquivalenceAlpha \(TODO: forall(x: Type) -> x) -> TODO : forall(y: Type) -> y
 failure/
-    MergeEmptyNeedsDirectAnnotation1 \(x: <>) -> (merge {=} x) : Bool
-    MergeEmptyNeedsDirectAnnotation2 \(x: <>) -> let y: Bool = merge {=} x in 1
-    MergeBoolIsNotUnion merge x True
-    MergeOptionalIsNotUnion merge x (Some 1)
-    MergeMissingHandler1 merge {=} < x >.x
-    MergeMissingHandler2 merge {x=...,} <x|y>.x
     merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
     merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
     merge { x = True, y = 1 } < x | y >.x
     merge {x=...,y=...} <x>.x
     merge {x=...,y=...} <x:T>.x
-    MergeHandlerFreeVar merge { x = None } < x = Bool >
-    UnionTypeDuplicateVariants1 <x, x>
-    UnionTypeDuplicateVariants2 <x, x:T>
-    UnionLitDuplicateVariants <x=1|x:T>
-    RecordLitDuplicateFields { x: T, x: T }
-    EquivalenceAlphaTrap \(TODO: forall(_: Type) -> _) -> TODO : forall(x: Type) -> _
+    MergeBoolIsNotUnion merge x True
+    MergeOptionalIsNotUnion merge x (Some 1)
 
 equivalence: