More nice errors plus some refactor

15 files changed, 272 insertions, 174 deletions

diff --git a/dhall/src/error/builder.rs b/dhall/src/error/builder.rs
index e293220..22b0d77 100644
--- a/dhall/src/error/builder.rs
+++ b/dhall/src/error/builder.rs
@@ -4,97 +4,162 @@ use annotate_snippets::{
     snippet::{Annotation, AnnotationType, Slice, Snippet, SourceAnnotation},
 };
 
-use crate::syntax::Span;
+use crate::syntax::{ParsedSpan, Span};
 
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, Default)]
 pub struct ErrorBuilder {
+    title: FreeAnnotation,
+    annotations: Vec<SpannedAnnotation>,
+    footer: Vec<FreeAnnotation>,
+    /// Inducate that the current builder has already been consumed and consuming it again should
+    /// panic.
+    consumed: bool,
+}
+
+#[derive(Debug, Clone)]
+struct SpannedAnnotation {
+    span: ParsedSpan,
     message: String,
     annotation_type: AnnotationType,
-    annotations: Vec<BuilderAnnotation>,
 }
 
 #[derive(Debug, Clone)]
-struct BuilderAnnotation {
-    span: Span,
+struct FreeAnnotation {
     message: String,
     annotation_type: AnnotationType,
 }
 
+impl SpannedAnnotation {
+    fn into_annotation(self) -> SourceAnnotation {
+        SourceAnnotation {
+            label: self.message,
+            annotation_type: self.annotation_type,
+            range: self.span.as_char_range(),
+        }
+    }
+}
+
+impl FreeAnnotation {
+    fn into_annotation(self) -> Annotation {
+        Annotation {
+            label: Some(self.message),
+            id: None,
+            annotation_type: self.annotation_type,
+        }
+    }
+}
+
 /// A builder that uses the annotate_snippets library to display nice error messages about source
 /// code locations.
 impl ErrorBuilder {
-    pub fn new(message: String) -> Self {
+    pub fn new(message: impl ToString) -> Self {
         ErrorBuilder {
-            message,
-            annotation_type: AnnotationType::Error,
+            title: FreeAnnotation {
+                message: message.to_string(),
+                annotation_type: AnnotationType::Error,
+            },
             annotations: Vec::new(),
+            footer: Vec::new(),
+            consumed: false,
         }
     }
-    pub fn span_err(span: &Span, message: String) -> Self {
+    pub fn new_span_err(span: &Span, message: impl ToString) -> Self {
+        let message = message.to_string();
         let mut builder = Self::new(message.clone());
-        builder.annotate_err(span, message);
+        builder.span_err(span, message);
         builder
     }
 
-    pub fn annotate_err(&mut self, span: &Span, message: String) {
-        self.annotations.push(BuilderAnnotation {
+    pub fn span_err(
+        &mut self,
+        span: &Span,
+        message: impl ToString,
+    ) -> &mut Self {
+        // Ignore spans not coming from a source file
+        let span = match span {
+            Span::Parsed(span) => span,
+            _ => return self,
+        };
+        self.annotations.push(SpannedAnnotation {
             span: span.clone(),
-            message,
+            message: message.to_string(),
             annotation_type: AnnotationType::Error,
-        })
+        });
+        self
     }
-    pub fn annotate_info(&mut self, span: &Span, message: String) {
-        self.annotations.push(BuilderAnnotation {
+    pub fn span_help(
+        &mut self,
+        span: &Span,
+        message: impl ToString,
+    ) -> &mut Self {
+        // Ignore spans not coming from a source file
+        let span = match span {
+            Span::Parsed(span) => span,
+            _ => return self,
+        };
+        self.annotations.push(SpannedAnnotation {
             span: span.clone(),
-            message,
+            message: message.to_string(),
+            annotation_type: AnnotationType::Help,
+        });
+        self
+    }
+    pub fn help(&mut self, message: impl ToString) -> &mut Self {
+        self.footer.push(FreeAnnotation {
+            message: message.to_string(),
             annotation_type: AnnotationType::Help,
-        })
+        });
+        self
     }
 
     // TODO: handle multiple files
-    pub fn format(self) -> String {
-        let mut input = None;
-        let annotations = self
-            .annotations
-            .into_iter()
-            .filter_map(|annot| {
-                let span = match annot.span {
-                    Span::Parsed(span) => span,
-                    _ => return None,
-                };
-                if input.is_none() {
-                    input = Some(span.to_input());
-                }
-                Some(SourceAnnotation {
-                    label: annot.message,
-                    annotation_type: annot.annotation_type,
-                    range: span.as_char_range(),
-                })
-            })
-            .collect();
-
-        let input = match input {
-            Some(input) => input,
-            None => return format!("[unknown location] {}", self.message),
-        };
+    pub fn format(&mut self) -> String {
+        if self.consumed {
+            panic!("tried to format the same ErrorBuilder twice")
+        }
+        let this = std::mem::replace(self, ErrorBuilder::default());
+        self.consumed = true;
+        drop(self); // Get rid of the self reference so we don't use it by mistake.
 
-        let snippet = Snippet {
-            title: Some(Annotation {
-                label: Some(self.message),
-                id: None,
-                annotation_type: self.annotation_type,
-            }),
-            footer: vec![],
-            slices: vec![Slice {
+        let slices = if this.annotations.is_empty() {
+            Vec::new()
+        } else {
+            let input = this.annotations[0].span.to_input();
+            let annotations = this
+                .annotations
+                .into_iter()
+                .map(|annot| annot.into_annotation())
+                .collect();
+            vec![Slice {
                 source: input,
                 line_start: 1, // TODO
                 origin: Some("<current file>".to_string()),
                 fold: true,
                 annotations,
-            }],
+            }]
+        };
+        let footer = this
+            .footer
+            .into_iter()
+            .map(|annot| annot.into_annotation())
+            .collect();
+
+        let snippet = Snippet {
+            title: Some(this.title.into_annotation()),
+            slices,
+            footer,
         };
         let dl = DisplayList::from(snippet);
         let dlf = DisplayListFormatter::new(true, false);
         format!("{}", dlf.format(&dl))
     }
 }
+
+impl Default for FreeAnnotation {
+    fn default() -> Self {
+        FreeAnnotation {
+            message: String::new(),
+            annotation_type: AnnotationType::Error,
+        }
+    }
+}
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 5b7693e..6ea7d0c 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -1,7 +1,6 @@
 use std::io::Error as IOError;
 
 use crate::semantics::resolve::ImportStack;
-use crate::semantics::Value;
 use crate::syntax::{Import, ParseError};
 use crate::NormalizedExpr;
 
@@ -49,8 +48,6 @@ pub struct TypeError {
 #[derive(Debug)]
 pub(crate) enum TypeMessage {
     // UnboundVariable(Span),
-    InvalidInputType(Value),
-    InvalidOutputType(Value),
     // NotAFunction(Value),
     // TypeMismatch(Value, Value, Value),
     // AnnotMismatch(Value, Value),
@@ -100,12 +97,6 @@ impl std::fmt::Display for TypeError {
         use TypeMessage::*;
         let msg = match &self.message {
             // UnboundVariable(var) => var.error("Type error: Unbound variable"),
-            InvalidInputType(v) => {
-                v.span().error("Type error: Invalid function input")
-            }
-            InvalidOutputType(v) => {
-                v.span().error("Type error: Invalid function output")
-            }
             // NotAFunction(v) => v.span().error("Type error: Not a function"),
             // TypeMismatch(x, y, z) => {
             //     x.span()
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index d97b8c4..bb3e3c0 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -174,9 +174,6 @@ impl Value {
             _ => None,
         }
     }
-    pub(crate) fn span(&self) -> Span {
-        self.0.span.clone()
-    }
 
     /// This is what you want if you want to pattern-match on the value.
     /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 812ca7a..1fc711c 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, TyExprKind, Type, Value};
+use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, Value};
 use crate::syntax::{Label, V};
 
 /// Environment for indexing variables.
@@ -116,9 +116,9 @@ impl TyEnv {
             items: self.items.insert_value(e),
         }
     }
-    pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> {
+    pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
         let var = self.names.unlabel_var(var)?;
         let ty = self.items.lookup_ty(&var);
-        Some((TyExprKind::Var(var), ty))
+        Some((var, ty))
     }
 }
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a652663..e642b8f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -35,19 +35,6 @@ fn function_check(a: Const, b: Const) -> Const {
     }
 }
 
-fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> {
-    let ks = match src.as_const() {
-        Some(k) => k,
-        _ => return Err(TypeError::new(TypeMessage::InvalidInputType(src))),
-    };
-    let kt = match tgt.as_const() {
-        Some(k) => k,
-        _ => return Err(TypeError::new(TypeMessage::InvalidOutputType(tgt))),
-    };
-
-    Ok(Value::from_const(function_check(ks, kt)))
-}
-
 fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
     Err(TypeError::new(TypeMessage::Custom(x.to_string())))
 }
@@ -64,12 +51,55 @@ fn type_one_layer(
             "There should remain no imports in a resolved expression"
         ),
         ExprKind::Var(..)
-        | ExprKind::Lam(..)
-        | ExprKind::Pi(..)
-        | ExprKind::Let(..)
         | ExprKind::Const(Const::Sort)
         | ExprKind::Embed(..) => unreachable!(), // Handled in type_with
 
+        ExprKind::Lam(binder, annot, body) => {
+            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())
+        }
+        ExprKind::Pi(_, annot, body) => {
+            let ks = match annot.get_type()?.as_const() {
+                Some(k) => k,
+                _ => {
+                    return mkerr(
+                        ErrorBuilder::new(format!(
+                            "Invalid input type: `{}`",
+                            annot.get_type()?.to_expr_tyenv(env),
+                        ))
+                        .span_err(
+                            &annot.span(),
+                            format!(
+                                "this has type: `{}`",
+                                annot.get_type()?.to_expr_tyenv(env)
+                            ),
+                        )
+                        .help(
+                            format!(
+                                "The input type of a function must have type `Type`, `Kind` or `Sort`",
+                            ),
+                        )
+                        .format(),
+                    );
+                }
+            };
+            let kt = match body.get_type()?.as_const() {
+                Some(k) => k,
+                _ => return mkerr("Invalid output type"),
+            };
+
+            Value::from_const(function_check(ks, kt))
+        }
+        ExprKind::Let(_, _, _, body) => body.get_type()?,
+
         ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
         ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
@@ -202,10 +232,12 @@ fn type_one_layer(
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(ty)) => {
-                                let pi_ty = type_of_function(
-                                    ty.get_type()?,
-                                    scrut.get_type()?,
-                                )?;
+                                // Can't fail because uniontypes must have type Const(_).
+                                let kt = scrut.get_type()?.as_const().unwrap();
+                                // The type of the field must be Const smaller than `kt`, thus the
+                                // function type has type `kt`.
+                                let pi_ty = Value::from_const(kt);
+
                                 Value::from_kind_and_type(
                                     ValueKind::PiClosure {
                                         binder: Binder::new(x.clone()),
@@ -256,25 +288,27 @@ fn type_one_layer(
         ExprKind::App(f, arg) => match f.get_type()?.kind() {
             ValueKind::PiClosure { annot, closure, .. } => {
                 if arg.get_type()? != *annot {
-                    let mut builder = ErrorBuilder::span_err(
-                        &span,
-                        format!("function annot mismatch",),
-                    );
-                    builder.annotate_info(
-                        &f.span(),
-                        format!(
-                            "this expects an argument of type: {}",
-                            annot.to_expr_tyenv(env),
-                        ),
+                    return mkerr(
+                        ErrorBuilder::new_span_err(
+                            &span,
+                            format!("Wrong type of function argument"),
+                        )
+                        .span_help(
+                            &f.span(),
+                            format!(
+                                "this expects an argument of type: {}",
+                                annot.to_expr_tyenv(env),
+                            ),
+                        )
+                        .span_help(
+                            &arg.span(),
+                            format!(
+                                "but this has type: {}",
+                                arg.get_type()?.to_expr_tyenv(env),
+                            ),
+                        )
+                        .format(),
                     );
-                    builder.annotate_info(
-                        &arg.span(),
-                        format!(
-                            "but this has type: {}",
-                            arg.get_type()?.to_expr_tyenv(env),
-                        ),
-                    );
-                    return mkerr(builder.format());
                 }
 
                 let arg_nf = arg.eval(env.as_nzenv());
@@ -534,62 +568,15 @@ pub(crate) fn type_with(
 ) -> Result<TyExpr, TypeError> {
     let (tyekind, ty) = match expr.as_ref() {
         ExprKind::Var(var) => match env.lookup(&var) {
-            Some((k, ty)) => (k, Some(ty)),
-            None => return mkerr("unbound variable"),
+            Some((v, ty)) => (TyExprKind::Var(v), Some(ty)),
+            None => {
+                return mkerr(
+                    ErrorBuilder::new(format!("unbound variable `{}`", var))
+                        .span_err(&expr.span(), "not found in this scope")
+                        .format(),
+                )
+            }
         },
-        ExprKind::Lam(binder, annot, body) => {
-            let annot = type_with(env, annot)?;
-            let annot_nf = annot.eval(env.as_nzenv());
-            let body_env = env.insert_type(&binder, annot_nf.clone());
-            let body = type_with(&body_env, body)?;
-            let body_ty = body.get_type()?;
-            let ty = TyExpr::new(
-                TyExprKind::Expr(ExprKind::Pi(
-                    binder.clone(),
-                    annot.clone(),
-                    body_ty.to_tyexpr(body_env.as_varenv()),
-                )),
-                Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
-                Span::Artificial,
-            );
-            let ty = ty.eval(env.as_nzenv());
-            (
-                TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
-                Some(ty),
-            )
-        }
-        ExprKind::Pi(binder, annot, body) => {
-            let annot = type_with(env, annot)?;
-            let annot_nf = annot.eval(env.as_nzenv());
-            let body =
-                type_with(&env.insert_type(binder, annot_nf.clone()), body)?;
-            let ty = type_of_function(annot.get_type()?, body.get_type()?)?;
-            (
-                TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)),
-                Some(ty),
-            )
-        }
-        ExprKind::Let(binder, annot, val, body) => {
-            let val = if let Some(t) = annot {
-                t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
-            } else {
-                val.clone()
-            };
-
-            let val = type_with(env, &val)?;
-            let val_nf = val.eval(&env.as_nzenv());
-            let body = type_with(&env.insert_value(&binder, val_nf), body)?;
-            let body_ty = body.get_type().ok();
-            (
-                TyExprKind::Expr(ExprKind::Let(
-                    binder.clone(),
-                    None,
-                    val,
-                    body,
-                )),
-                body_ty,
-            )
-        }
         ExprKind::Const(Const::Sort) => {
             (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
         }
@@ -597,7 +584,36 @@ pub(crate) fn type_with(
             return Ok(p.clone().into_value().to_tyexpr_noenv())
         }
         ekind => {
-            let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
+            let ekind = match ekind {
+                ExprKind::Lam(binder, annot, body) => {
+                    let annot = type_with(env, annot)?;
+                    let annot_nf = annot.eval(env.as_nzenv());
+                    let body_env = env.insert_type(binder, annot_nf);
+                    let body = type_with(&body_env, body)?;
+                    ExprKind::Lam(binder.clone(), annot, body)
+                }
+                ExprKind::Pi(binder, annot, body) => {
+                    let annot = type_with(env, annot)?;
+                    let annot_nf = annot.eval(env.as_nzenv());
+                    let body_env = env.insert_type(binder, annot_nf);
+                    let body = type_with(&body_env, body)?;
+                    ExprKind::Pi(binder.clone(), annot, body)
+                }
+                ExprKind::Let(binder, annot, val, body) => {
+                    let val = if let Some(t) = annot {
+                        t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
+                    } else {
+                        val.clone()
+                    };
+                    let val = type_with(env, &val)?;
+                    let val_nf = val.eval(&env.as_nzenv());
+                    let body_env = env.insert_value(&binder, val_nf);
+                    let body = type_with(&body_env, body)?;
+                    ExprKind::Let(binder.clone(), None, val, body)
+                }
+                _ => ekind.traverse_ref(|e| type_with(env, e))?,
+            };
+
             let ty = type_one_layer(env, &ekind, expr.span())?;
             (TyExprKind::Expr(ekind), Some(ty))
         }
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 10bb9a4..e06c4b2 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1,4 +1,4 @@
-Type error: Unhandled error: error: function annot mismatch
+Type error: Unhandled error: error: Wrong type of function argument
   --> <current file>:6:23
    |
  1 |     let bottom : Type = ∀(any : Type) → any
@@ -8,7 +8,7 @@ Type error: Unhandled error: error: function annot mismatch
 ...
 10 |         : pow (pow U) → U
 11 |         =   λ(t : pow (pow U))
-   |                        ^^^^^ function annot mismatch
+   |                        ^^^^^ Wrong type of function argument
    |                        --- help: this expects an argument of type: Kind
    |                            - help: but this has type: Sort
    |
diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
index 87cf48e..e4584f5 100644
--- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
+++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: unbound variable
+Type error: Unhandled error: error: unbound variable ``_``
+ --> <current file>:1:46
+  |
+1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
+  |                                               ^ not found in this scope
+  |
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
index 7aa2281..776b14e 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1,8 +1,8 @@
-Type error: Unhandled error: error: function annot mismatch
+Type error: Unhandled error: error: Wrong type of function argument
  --> <current file>:1:1
   |
 1 | (λ(_ : Natural) → _) True
-  |  ^^^^^^^^^^^^^^^^^^^^^^^^ function annot mismatch
+  |  ^^^^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument
   |  ------------------ help: this expects an argument of type: Natural
   |                      ---- help: but this has type: Bool
   |
diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
index a13fb3a..3fc1652 100644
--- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
+++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
@@ -1 +1,7 @@
-[unknown location] Type error: Invalid function input
+Type error: Unhandled error: error: Invalid input type: `Natural`
+ --> <current file>:1:6
+  |
+1 | λ(_ : 1) → _
+  |       ^ this has type: `Natural`
+  |
+  = help: The input type of a function must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
index a13fb3a..948c6c7 100644
--- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
+++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -1 +1,7 @@
-[unknown location] Type error: Invalid function input
+Type error: Unhandled error: error: Invalid input type: `Natural`
+ --> <current file>:1:0
+  |
+1 | 2 → _
+  | ^ this has type: `Natural`
+  |
+  = help: The input type of a function must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
index 3673338..125cc87 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1,8 +1,8 @@
-Type error: Unhandled error: error: function annot mismatch
+Type error: Unhandled error: error: Wrong type of function argument
  --> <current file>:1:5
   |
 1 | [] : List Type
-  |      ^^^^^^^^^ function annot mismatch
+  |      ^^^^^^^^^ Wrong type of function argument
   |      ---- help: this expects an argument of type: Type
   |           ---- help: but this has type: Kind
   |
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
index 795c97c..5ee2a11 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1,8 +1,8 @@
-Type error: Unhandled error: error: function annot mismatch
+Type error: Unhandled error: error: Wrong type of function argument
  --> <current file>:1:0
   |
 1 | Natural/subtract True True
-  | ^^^^^^^^^^^^^^^^^^^^^ function annot mismatch
+  | ^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument
   | ---------------- help: this expects an argument of type: Natural
   |                  ---- help: but this has type: Bool
   |
diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
index 87cf48e..a234f9f 100644
--- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
+++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: unbound variable
+Type error: Unhandled error: error: unbound variable `constructors`
+ --> <current file>:1:0
+  |
+1 | constructors < Left : Natural | Right : Bool >
+  | ^^^^^^^^^^^^ not found in this scope
+  |
diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt
index 87cf48e..52baa7f 100644
--- a/dhall/tests/type-errors/unit/VariableFree.txt
+++ b/dhall/tests/type-errors/unit/VariableFree.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: unbound variable
+Type error: Unhandled error: error: unbound variable `x`
+ --> <current file>:1:0
+  |
+1 | x
+  | ^ not found in this scope
+  |
diff --git a/tests_buffer b/tests_buffer
index 34210a9..87d73ef 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -51,6 +51,8 @@ success/
             let X = 0 in λ(T : Type) → λ(x : T) → 1
             (λ(T : Type) → let foo = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
 failure/
+    \(_: Bool) -> assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
+    \(x: let x = 1 in Sort) -> 0
     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