Merge pull request #129 from Nadrieril/missing-features

Implement some missing features

14 files changed, 361 insertions, 106 deletions

diff --git a/dhall/build.rs b/dhall/build.rs
index 9cc07ea..83c154e 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -258,31 +258,22 @@ fn generate_tests() -> std::io::Result<()> {
                     || path == "unit/RecordProjectionByTypeEmpty"
                     || path == "unit/RecordProjectionByTypeNonEmpty"
                     || path == "unit/RecordProjectionByTypeNormalizeProjection"
+                    || path == "unit/RecordProjectionByTypeWithinFieldSelection"
+                    || path == "unit/RecursiveRecordMergeWithinFieldSelection1"
+                    || path == "unit/NestedRecordProjectionByType"
                     // TODO: fix Double/show
                     || path == "prelude/JSON/number/1"
-                    // TODO: toMap
-                    || path == "unit/EmptyToMap"
-                    || path == "unit/ToMap"
-                    || path == "unit/ToMapWithType"
-                    // TODO: Further record simplifications
+                    // TODO: doesn't typecheck
+                    || path == "unit/RightBiasedRecordMergeWithinRecordProjection"
+                    // // TODO: Further record simplifications
                     || path == "simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection0"
                     || path == "simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection1"
                     || path == "simplifications/rightBiasedMergeWithinRecursiveRecordMergeWithinFieldselection"
                     || path == "simplifications/issue661"
-                    || path == "unit/RecordProjectionByTypeWithinFieldSelection"
                     || path == "unit/RecordProjectionWithinFieldSelection"
                     || path == "unit/RecursiveRecordMergeWithinFieldSelection0"
-                    || path == "unit/RecursiveRecordMergeWithinFieldSelection1"
                     || path == "unit/RecursiveRecordMergeWithinFieldSelection2"
                     || path == "unit/RecursiveRecordMergeWithinFieldSelection3"
-                    || path == "unit/RightBiasedMergeWithinFieldSelection0"
-                    || path == "unit/RightBiasedMergeWithinFieldSelection1"
-                    || path == "unit/RightBiasedMergeWithinFieldSelection2"
-                    || path == "unit/RightBiasedMergeWithinFieldSelection3"
-                    || path == "unit/RightBiasedRecordMergeWithinRecordProjection"
-                    || path == "unit/RightBiasedMergeEquivalentArguments"
-                    || path == "unit/NestedRecordProjection"
-                    || path == "unit/NestedRecordProjectionByType"
                     // TODO: record completion
                     || path == "simple/completion"
                     || path == "unit/Completion"
@@ -309,18 +300,6 @@ fn generate_tests() -> std::io::Result<()> {
                 false
                     // Too slow
                     || path == "prelude"
-                    // TODO: projection by expression
-                    || path == "unit/RecordProjectionByType"
-                    || path == "unit/RecordProjectionByTypeEmpty"
-                    || path == "unit/RecordProjectionByTypeJudgmentalEquality"
-                    // TODO: toMap
-                    || path == "unit/ToMap"
-                    || path == "unit/ToMapAnnotated"
-                    || path == "unit/ToMapInferTypeFromRecord"
-                    || path == "simple/toMapEmptyNormalizeAnnotation"
-                    // TODO: record completion
-                    || path == "simple/completion"
-                    || path == "unit/Completion"
             }),
             input_type: FileType::Text,
             output_type: Some(FileType::Text),
@@ -331,24 +310,6 @@ fn generate_tests() -> std::io::Result<()> {
             variant: "TypeInferenceFailure",
             path_filter: Box::new(|path: &str| {
                 false
-                    // TODO: projection by expression
-                    || path == "unit/RecordProjectionByTypeFieldTypeMismatch"
-                    || path == "unit/RecordProjectionByTypeNotPresent"
-                    // TODO: toMap
-                    || path == "unit/EmptyToMap"
-                    || path == "unit/HeterogenousToMap"
-                    || path == "unit/MistypedToMap1"
-                    || path == "unit/MistypedToMap2"
-                    || path == "unit/MistypedToMap3"
-                    || path == "unit/MistypedToMap4"
-                    || path == "unit/NonRecordToMap"
-                    || path == "unit/ToMapEmptyInvalidAnnotation"
-                    || path == "unit/ToMapWrongKind"
-                    // TODO: record completion
-                    || path == "unit/CompletionMissingRequiredField"
-                    || path == "unit/CompletionWithWrongDefaultType"
-                    || path == "unit/CompletionWithWrongFieldName"
-                    || path == "unit/CompletionWithWrongOverridenType"
                     // TODO: enable free variable checking
                     || path == "unit/MergeHandlerFreeVar"
             }),
@@ -361,24 +322,6 @@ fn generate_tests() -> std::io::Result<()> {
             variant: "TypeError",
             path_filter: Box::new(|path: &str| {
                 false
-                    // TODO: projection by expression
-                    || path == "unit/RecordProjectionByTypeFieldTypeMismatch"
-                    || path == "unit/RecordProjectionByTypeNotPresent"
-                    // TODO: toMap
-                    || path == "unit/EmptyToMap"
-                    || path == "unit/HeterogenousToMap"
-                    || path == "unit/MistypedToMap1"
-                    || path == "unit/MistypedToMap2"
-                    || path == "unit/MistypedToMap3"
-                    || path == "unit/MistypedToMap4"
-                    || path == "unit/NonRecordToMap"
-                    || path == "unit/ToMapEmptyInvalidAnnotation"
-                    || path == "unit/ToMapWrongKind"
-                    // TODO: record completion
-                    || path == "unit/CompletionMissingRequiredField"
-                    || path == "unit/CompletionWithWrongDefaultType"
-                    || path == "unit/CompletionWithWrongFieldName"
-                    || path == "unit/CompletionWithWrongOverridenType"
                     // TODO: enable free variable checking
                     || path == "unit/MergeHandlerFreeVar"
             }),
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index c20fb77..907d449 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -1,5 +1,5 @@
 use crate::semantics::{
-    self, typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv,
+    typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv,
 };
 use crate::syntax::map::DupTreeMap;
 use crate::syntax::Const::Type;
@@ -301,9 +301,7 @@ fn apply_builtin(
             _ => Ret::DoneAsIs,
         },
         (NaturalShow, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::ValueKind(TextLit(
-                semantics::TextLit::from_text(n.to_string()),
-            )),
+            NaturalLit(n) => Ret::Value(Value::from_text(n)),
             _ => Ret::DoneAsIs,
         },
         (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
@@ -322,7 +320,7 @@ fn apply_builtin(
                 } else {
                     format!("+{}", n)
                 };
-                Ret::ValueKind(TextLit(semantics::TextLit::from_text(s)))
+                Ret::Value(Value::from_text(s))
             }
             _ => Ret::DoneAsIs,
         },
@@ -343,9 +341,7 @@ fn apply_builtin(
             _ => Ret::DoneAsIs,
         },
         (DoubleShow, [n]) => match &*n.kind() {
-            DoubleLit(n) => Ret::ValueKind(TextLit(
-                semantics::TextLit::from_text(n.to_string()),
-            )),
+            DoubleLit(n) => Ret::Value(Value::from_text(n)),
             _ => Ret::DoneAsIs,
         },
         (TextShow, [v]) => match &*v.kind() {
@@ -355,8 +351,7 @@ fn apply_builtin(
                     let txt: InterpolatedText<Normalized> =
                         std::iter::once(InterpolatedTextContents::Text(s))
                             .collect();
-                    let s = txt.to_string();
-                    Ret::ValueKind(TextLit(semantics::TextLit::from_text(s)))
+                    Ret::Value(Value::from_text(txt))
                 } else {
                     Ret::DoneAsIs
                 }
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index e9d140b..a00b7ff 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -1,3 +1,4 @@
+use itertools::Itertools;
 use std::collections::HashMap;
 
 use crate::semantics::NzEnv;
@@ -184,6 +185,7 @@ fn apply_binop<'a>(
             }
             Ret::ValueKind(RecordLit(kvs))
         }
+        (RightBiasedRecordMerge, _, _) if x == y => Ret::ValueRef(y),
 
         (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
             Ret::ValueRef(x)
@@ -242,9 +244,9 @@ pub(crate) fn normalize_one_layer(
     env: &NzEnv,
 ) -> ValueKind {
     use ValueKind::{
-        BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit,
-        NEOptionalLit, NaturalLit, RecordLit, RecordType, UnionConstructor,
-        UnionLit, UnionType,
+        BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit,
+        NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit,
+        RecordType, UnionConstructor, UnionLit, UnionType,
     };
 
     let ret = match expr {
@@ -271,7 +273,7 @@ pub(crate) fn normalize_one_layer(
         ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
         ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
-            let arg = match &*t.kind() {
+            let arg = match t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
@@ -330,6 +332,13 @@ pub(crate) fn normalize_one_layer(
                     .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
                     .collect(),
             )),
+            PartialExpr(ExprKind::Projection(v2, _)) => {
+                return normalize_one_layer(
+                    ExprKind::Projection(v2.clone(), ls.clone()),
+                    ty,
+                    env,
+                )
+            }
             _ => Ret::Expr(expr),
         },
         ExprKind::Field(ref v, ref l) => match v.kind() {
@@ -342,6 +351,88 @@ pub(crate) fn normalize_one_layer(
                 kts.clone(),
                 v.get_type().unwrap(),
             )),
+            PartialExpr(ExprKind::BinOp(
+                BinOp::RightBiasedRecordMerge,
+                x,
+                y,
+            )) => match (x.kind(), y.kind()) {
+                (_, RecordLit(kvs)) => match kvs.get(l) {
+                    Some(r) => Ret::Value(r.clone()),
+                    None => {
+                        return normalize_one_layer(
+                            ExprKind::Field(x.clone(), l.clone()),
+                            ty,
+                            env,
+                        )
+                    }
+                },
+                (RecordLit(kvs), _) => match kvs.get(l) {
+                    Some(r) => Ret::Expr(ExprKind::Field(
+                        Value::from_kind_and_type(
+                            PartialExpr(ExprKind::BinOp(
+                                BinOp::RightBiasedRecordMerge,
+                                Value::from_kind_and_type(
+                                    RecordLit({
+                                        let mut kvs = HashMap::new();
+                                        kvs.insert(l.clone(), r.clone());
+                                        kvs
+                                    }),
+                                    Value::from_kind_and_type(
+                                        RecordType({
+                                            let mut kvs = HashMap::new();
+                                            kvs.insert(
+                                                l.clone(),
+                                                r.get_type_not_sort(),
+                                            );
+                                            kvs
+                                        }),
+                                        r.get_type_not_sort()
+                                            .get_type_not_sort(),
+                                    ),
+                                ),
+                                y.clone(),
+                            )),
+                            v.get_type_not_sort(),
+                        ),
+                        l.clone(),
+                    )),
+                    None => {
+                        return normalize_one_layer(
+                            ExprKind::Field(y.clone(), l.clone()),
+                            ty,
+                            env,
+                        )
+                    }
+                },
+                _ => Ret::Expr(expr),
+            },
+            PartialExpr(ExprKind::BinOp(
+                BinOp::RecursiveRecordTypeMerge,
+                x,
+                y,
+            )) => match (x.kind(), y.kind()) {
+                (RecordLit(kvs), _) => match kvs.get(l) {
+                    Some(_) => Ret::Expr(expr),
+                    None => {
+                        return normalize_one_layer(
+                            ExprKind::Field(y.clone(), l.clone()),
+                            ty,
+                            env,
+                        )
+                    }
+                },
+                (_, RecordLit(kvs)) => match kvs.get(l) {
+                    Some(_) => Ret::Expr(expr),
+                    None => {
+                        return normalize_one_layer(
+                            ExprKind::Field(x.clone(), l.clone()),
+                            ty,
+                            env,
+                        )
+                    }
+                },
+                _ => Ret::Expr(expr),
+            },
             _ => Ret::Expr(expr),
         },
         ExprKind::ProjectionByExpr(_, _) => {
@@ -373,7 +464,45 @@ pub(crate) fn normalize_one_layer(
                 _ => Ret::Expr(expr),
             }
         }
-        ExprKind::ToMap(_, _) => unimplemented!("toMap"),
+        ExprKind::ToMap(ref v, ref annot) => match v.kind() {
+            RecordLit(kvs) if kvs.is_empty() => {
+                match annot.as_ref().map(|v| v.kind()) {
+                    Some(ValueKind::AppliedBuiltin(BuiltinClosure {
+                        b: Builtin::List,
+                        args,
+                        ..
+                    })) if args.len() == 1 => {
+                        Ret::ValueKind(EmptyListLit(args[0].clone()))
+                    }
+                    _ => Ret::Expr(expr),
+                }
+            }
+            RecordLit(kvs) => Ret::ValueKind(NEListLit(
+                kvs.iter()
+                    .sorted_by_key(|(k, _)| k.clone())
+                    .map(|(k, v)| {
+                        let mut rec = HashMap::new();
+                        let mut rec_ty = HashMap::new();
+                        rec.insert("mapKey".into(), Value::from_text(k));
+                        rec.insert("mapValue".into(), v.clone());
+                        rec_ty.insert(
+                            "mapKey".into(),
+                            Value::from_builtin(Builtin::Text),
+                        );
+                        rec_ty.insert("mapValue".into(), v.get_type_not_sort());
+
+                        Value::from_kind_and_type(
+                            ValueKind::RecordLit(rec),
+                            Value::from_kind_and_type(
+                                ValueKind::RecordType(rec_ty),
+                                Value::from_const(Const::Type),
+                            ),
+                        )
+                    })
+                    .collect(),
+            )),
+            _ => Ret::Expr(expr),
+        },
     };
 
     match ret {
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 1143781..607aa0d 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -167,6 +167,12 @@ impl Value {
             typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(),
         )
     }
+    pub(crate) fn from_text(txt: impl ToString) -> Self {
+        Value::from_kind_and_type(
+            ValueKind::TextLit(TextLit::from_text(txt.to_string())),
+            Value::from_builtin(Builtin::Text),
+        )
+    }
 
     pub(crate) fn as_const(&self) -> Option<Const> {
         match &*self.kind() {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index c3c589b..6817712 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -51,9 +51,9 @@ fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
 /// layer.
 fn type_one_layer(
     env: &TyEnv,
-    kind: &ExprKind<TyExpr, Normalized>,
+    ekind: ExprKind<TyExpr, Normalized>,
     span: Span,
-) -> Result<Type, TypeError> {
+) -> Result<TyExpr, TypeError> {
     let span_err = |msg: &str| {
         mkerr(
             ErrorBuilder::new(msg.to_string())
@@ -62,7 +62,7 @@ fn type_one_layer(
         )
     };
 
-    Ok(match kind {
+    let ty = match &ekind {
         ExprKind::Import(..) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
@@ -74,13 +74,8 @@ fn type_one_layer(
             let body_ty = body.get_type()?;
             let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
             let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
-            let pi_ty = type_one_layer(env, &pi_ekind, Span::Artificial)?;
-            let ty = TyExpr::new(
-                TyExprKind::Expr(pi_ekind),
-                Some(pi_ty),
-                Span::Artificial,
-            );
-            ty.eval(env.as_nzenv())
+            type_one_layer(env, pi_ekind, Span::Artificial)?
+                .eval(env.as_nzenv())
         }
         ExprKind::Pi(_, annot, body) => {
             let ks = match annot.get_type()?.as_const() {
@@ -187,7 +182,7 @@ fn type_one_layer(
             }
 
             let ty = type_of_recordtype(
-                span,
+                span.clone(),
                 kts.iter()
                     .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
             )?;
@@ -206,7 +201,10 @@ fn type_one_layer(
                 };
             }
 
-            type_of_recordtype(span, kts.iter().map(|(_, t)| Cow::Borrowed(t)))?
+            type_of_recordtype(
+                span.clone(),
+                kts.iter().map(|(_, t)| Cow::Borrowed(t)),
+            )?
         }
         ExprKind::UnionType(kts) => {
             use std::collections::hash_map::Entry;
@@ -389,7 +387,7 @@ fn type_one_layer(
 
             // Construct the final record type
             let ty = type_of_recordtype(
-                span,
+                span.clone(),
                 kts.iter()
                     .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
             )?;
@@ -401,9 +399,7 @@ fn type_one_layer(
                 x.get_type()?.to_tyexpr(env.as_varenv()),
                 y.get_type()?.to_tyexpr(env.as_varenv()),
             );
-            let ty = type_one_layer(env, &ekind, Span::Artificial)?;
-            TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
-                .eval(env.as_nzenv())
+            type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv())
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
             let x_val = x.eval(env.as_nzenv());
@@ -420,7 +416,7 @@ fn type_one_layer(
                 if let Some(ty) = kts_y.get(k) {
                     type_one_layer(
                         env,
-                        &ExprKind::BinOp(
+                        ExprKind::BinOp(
                             BinOp::RecursiveRecordTypeMerge,
                             tx.to_tyexpr(env.as_varenv()),
                             ty.to_tyexpr(env.as_varenv()),
@@ -547,9 +543,14 @@ fn type_one_layer(
                                 );
                             }
 
-                            closure.remove_binder().or_else(|()| {
-                                span_err("MergeReturnTypeIsDependent")
-                            })?
+                            match closure.remove_binder() {
+                                Ok(v) => v,
+                                Err(()) => {
+                                    return span_err(
+                                        "MergeReturnTypeIsDependent",
+                                    )
+                                }
+                            }
                         }
                         _ => {
                             return mkerr(
@@ -619,7 +620,85 @@ fn type_one_layer(
                 (None, None) => return span_err("MergeEmptyNeedsAnnotation"),
             }
         }
-        ExprKind::ToMap(_, _) => unimplemented!("toMap"),
+        ExprKind::ToMap(record, annot) => {
+            let record_t = record.get_type()?;
+            let kts = match record_t.kind() {
+                ValueKind::RecordType(kts) => kts,
+                _ => {
+                    return span_err("The argument to `toMap` must be a record")
+                }
+            };
+
+            if kts.is_empty() {
+                let annot = if let Some(annot) = annot {
+                    annot
+                } else {
+                    return span_err(
+                        "`toMap` applied to an empty record requires a type \
+                         annotation",
+                    );
+                };
+                let annot_val = annot.eval(env.as_nzenv());
+
+                let err_msg = "The type of `toMap x` must be of the form \
+                               `List { mapKey : Text, mapValue : T }`";
+                let arg = match annot_val.kind() {
+                    ValueKind::AppliedBuiltin(BuiltinClosure {
+                        b: Builtin::List,
+                        args,
+                        ..
+                    }) if args.len() == 1 => &args[0],
+                    _ => return span_err(err_msg),
+                };
+                let kts = match arg.kind() {
+                    ValueKind::RecordType(kts) => kts,
+                    _ => return span_err(err_msg),
+                };
+                if kts.len() != 2 {
+                    return span_err(err_msg);
+                }
+                match kts.get(&"mapKey".into()) {
+                    Some(t) if *t == Value::from_builtin(Builtin::Text) => {}
+                    _ => return span_err(err_msg),
+                }
+                match kts.get(&"mapValue".into()) {
+                    Some(_) => {}
+                    None => return span_err(err_msg),
+                }
+                annot_val
+            } else {
+                let entry_type = kts.iter().next().unwrap().1.clone();
+                if entry_type.get_type()?.as_const() != Some(Const::Type) {
+                    return span_err(
+                        "`toMap` only accepts records of type `Type`",
+                    );
+                }
+                for (_, t) in kts.iter() {
+                    if *t != entry_type {
+                        return span_err(
+                            "Every field of the record must have the same type",
+                        );
+                    }
+                }
+
+                let mut kts = HashMap::new();
+                kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
+                kts.insert("mapValue".into(), entry_type);
+                let output_type = Value::from_builtin(Builtin::List).app(
+                    Value::from_kind_and_type(
+                        ValueKind::RecordType(kts),
+                        Value::from_const(Const::Type),
+                    ),
+                );
+                if let Some(annot) = annot {
+                    let annot_val = annot.eval(env.as_nzenv());
+                    if output_type != annot_val {
+                        return span_err("Annotation mismatch");
+                    }
+                }
+                output_type
+            }
+        }
         ExprKind::Projection(record, labels) => {
             let record_type = record.get_type()?;
             let kts = match record_type.kind() {
@@ -648,11 +727,61 @@ fn type_one_layer(
                 record_type.get_type()?,
             )
         }
-        ExprKind::ProjectionByExpr(_, _) => {
-            unimplemented!("selection by expression")
+        ExprKind::ProjectionByExpr(record, selection) => {
+            let record_type = record.get_type()?;
+            let rec_kts = match record_type.kind() {
+                ValueKind::RecordType(kts) => kts,
+                _ => return span_err("ProjectionMustBeRecord"),
+            };
+
+            let selection_val = selection.eval(env.as_nzenv());
+            let sel_kts = match selection_val.kind() {
+                ValueKind::RecordType(kts) => kts,
+                _ => return span_err("ProjectionByExprTakesRecordType"),
+            };
+
+            for (l, sel_ty) in sel_kts {
+                match rec_kts.get(l) {
+                    Some(rec_ty) => {
+                        if rec_ty != sel_ty {
+                            return span_err("ProjectionWrongType");
+                        }
+                    }
+                    None => return span_err("ProjectionMissingEntry"),
+                }
+            }
+
+            selection_val
+        }
+        ExprKind::Completion(ty, compl) => {
+            let ty_field_default = type_one_layer(
+                env,
+                ExprKind::Field(ty.clone(), "default".into()),
+                span.clone(),
+            )?;
+            let ty_field_type = type_one_layer(
+                env,
+                ExprKind::Field(ty.clone(), "Type".into()),
+                span.clone(),
+            )?;
+            let merge = type_one_layer(
+                env,
+                ExprKind::BinOp(
+                    BinOp::RightBiasedRecordMerge,
+                    ty_field_default,
+                    compl.clone(),
+                ),
+                span.clone(),
+            )?;
+            return type_one_layer(
+                env,
+                ExprKind::Annot(merge, ty_field_type),
+                span.clone(),
+            );
         }
-        ExprKind::Completion(_, _) => unimplemented!("record completion"),
-    })
+    };
+
+    Ok(TyExpr::new(TyExprKind::Expr(ekind), Some(ty), span))
 }
 
 /// `type_with` typechecks an expressio in the provided environment.
@@ -708,9 +837,7 @@ pub(crate) fn type_with(
                 }
                 _ => ekind.traverse_ref(|e| type_with(env, e))?,
             };
-
-            let ty = type_one_layer(env, &ekind, expr.span())?;
-            (TyExprKind::Expr(ekind), Some(ty))
+            return type_one_layer(env, ekind, expr.span());
         }
     };
 
diff --git a/dhall/tests/type-errors/unit/EmptyToMap.txt b/dhall/tests/type-errors/unit/EmptyToMap.txt
new file mode 100644
index 0000000..000fac7
--- /dev/null
+++ b/dhall/tests/type-errors/unit/EmptyToMap.txt
@@ -0,0 +1,6 @@
+Type error: error: `toMap` applied to an empty record requires a type annotation
+ --> <current file>:1:0
+  |
+1 | toMap {=}
+  | ^^^^^^^^^ `toMap` applied to an empty record requires a type annotation
+  |
diff --git a/dhall/tests/type-errors/unit/HeterogenousToMap.txt b/dhall/tests/type-errors/unit/HeterogenousToMap.txt
new file mode 100644
index 0000000..2f8abf2
--- /dev/null
+++ b/dhall/tests/type-errors/unit/HeterogenousToMap.txt
@@ -0,0 +1,6 @@
+Type error: error: Every field of the record must have the same type
+ --> <current file>:1:0
+  |
+1 | toMap { foo= 1, bar= "Bar" }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Every field of the record must have the same type
+  |
diff --git a/dhall/tests/type-errors/unit/MistypedToMap1.txt b/dhall/tests/type-errors/unit/MistypedToMap1.txt
new file mode 100644
index 0000000..14d9791
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MistypedToMap1.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+  |
+1 | toMap { foo= 1, bar= 4 } : Natural
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+  |
diff --git a/dhall/tests/type-errors/unit/MistypedToMap2.txt b/dhall/tests/type-errors/unit/MistypedToMap2.txt
new file mode 100644
index 0000000..88e303e
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MistypedToMap2.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+  |
+1 | toMap { foo= 1, bar= 4 } : List Natural
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+  |
diff --git a/dhall/tests/type-errors/unit/MistypedToMap3.txt b/dhall/tests/type-errors/unit/MistypedToMap3.txt
new file mode 100644
index 0000000..6b3772d
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MistypedToMap3.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+  |
+1 | toMap { foo= 1, bar= 4 } : List { mapKey : Natural, mapValue : Natural }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+  |
diff --git a/dhall/tests/type-errors/unit/MistypedToMap4.txt b/dhall/tests/type-errors/unit/MistypedToMap4.txt
new file mode 100644
index 0000000..e0cf651
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MistypedToMap4.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+  |
+1 | toMap { foo= 1, bar= 4 } : List { mapKey : Text, mapValue : Text }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+  |
diff --git a/dhall/tests/type-errors/unit/NonRecordToMap.txt b/dhall/tests/type-errors/unit/NonRecordToMap.txt
new file mode 100644
index 0000000..8e83002
--- /dev/null
+++ b/dhall/tests/type-errors/unit/NonRecordToMap.txt
@@ -0,0 +1,6 @@
+Type error: error: The argument to `toMap` must be a record
+ --> <current file>:1:0
+  |
+1 | toMap "text"
+  | ^^^^^^^^^^^^ The argument to `toMap` must be a record
+  |
diff --git a/dhall/tests/type-errors/unit/ToMapEmptyInvalidAnnotation.txt b/dhall/tests/type-errors/unit/ToMapEmptyInvalidAnnotation.txt
new file mode 100644
index 0000000..c28073e
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ToMapEmptyInvalidAnnotation.txt
@@ -0,0 +1,7 @@
+Type error: error: The type of `toMap x` must be of the form `List { mapKey : Text, mapValue : T }`
+ --> <current file>:2:0
+  |
+1 | -- The mapKey must be Text
+2 | toMap {=} : List { mapKey : Bool, mapValue : Text }
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The type of `toMap x` must be of the form `List { mapKey : Text, mapValue : T }`
+  |
diff --git a/dhall/tests/type-errors/unit/ToMapWrongKind.txt b/dhall/tests/type-errors/unit/ToMapWrongKind.txt
new file mode 100644
index 0000000..8158c08
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ToMapWrongKind.txt
@@ -0,0 +1,6 @@
+Type error: error: `toMap` only accepts records of type `Type`
+ --> <current file>:1:0
+  |
+1 | toMap { x = Bool }
+  | ^^^^^^^^^^^^^^^^^^ `toMap` only accepts records of type `Type`
+  |