Merge pull request #127 from Nadrieril/nicer-type-errors

Enable multiple locations for type errors

27 files changed, 539 insertions, 144 deletions

diff --git a/.rustfmt.toml b/.rustfmt.toml
index ee91dbd..0a0f30e 100644
--- a/.rustfmt.toml
+++ b/.rustfmt.toml
@@ -1,3 +1,4 @@
 edition = "2018"
 max_width = 80
 # error_on_line_overflow = true
+format_strings = true
diff --git a/Cargo.lock b/Cargo.lock
index c737e52..450a1da 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -19,6 +19,11 @@ dependencies = [
 ]
 
 [[package]]
+name = "annotate-snippets"
+version = "0.6.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
 name = "ansi_term"
 version = "0.11.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -87,6 +92,7 @@ name = "dhall"
 version = "0.2.1"
 dependencies = [
  "abnf_to_pest 0.2.0",
+ "annotate-snippets 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
  "hex 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
  "itertools 0.8.2 (registry+https://github.com/rust-lang/crates.io-index)",
  "lazy_static 1.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
@@ -511,6 +517,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 
 [metadata]
 "checksum abnf 0.6.0 (registry+https://github.com/rust-lang/crates.io-index)" = "e065019cf2f9438a593954cc8e774925656b86701b72720b82ec3141e682ac14"
+"checksum annotate-snippets 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)" = "c7021ce4924a3f25f802b2cccd1af585e39ea1a363a1aa2e72afe54b67a3a7a7"
 "checksum ansi_term 0.11.0 (registry+https://github.com/rust-lang/crates.io-index)" = "ee49baf6cb617b853aa8d93bf420db2383fab46d314482ca2803b40d5fde979b"
 "checksum arrayvec 0.4.12 (registry+https://github.com/rust-lang/crates.io-index)" = "cd9fd44efafa8690358b7408d253adf110036b88f55672a933f01d616ad9b1b9"
 "checksum autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "1d49d90015b3c36167a20fe2810c5cd875ad504b39cff3d4eae7977e6b7c1cb2"
diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml
index 2fbfb23..3281e4a 100644
--- a/dhall/Cargo.toml
+++ b/dhall/Cargo.toml
@@ -10,10 +10,11 @@ edition = "2018"
 build = "build.rs"
 
 [dependencies]
+annotate-snippets = "0.6.1"
 itertools = "0.8.0"
 hex = "0.3.2"
 lazy_static = "1.4.0"
- once_cell = "1.3.1"
+once_cell = "1.3.1"
 percent-encoding = "2.1.0"
 pest = "2.1"
 pest_consume = "1.0"
diff --git a/dhall/src/error/builder.rs b/dhall/src/error/builder.rs
new file mode 100644
index 0000000..39f8dfb
--- /dev/null
+++ b/dhall/src/error/builder.rs
@@ -0,0 +1,168 @@
+use annotate_snippets::{
+    display_list::DisplayList,
+    formatter::DisplayListFormatter,
+    snippet::{Annotation, AnnotationType, Slice, Snippet, SourceAnnotation},
+};
+
+use crate::syntax::{ParsedSpan, Span};
+
+#[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,
+}
+
+#[derive(Debug, Clone)]
+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: impl ToString) -> Self {
+        ErrorBuilder {
+            title: FreeAnnotation {
+                message: message.to_string(),
+                annotation_type: AnnotationType::Error,
+            },
+            annotations: Vec::new(),
+            footer: Vec::new(),
+            consumed: false,
+        }
+    }
+
+    pub fn span_annot(
+        &mut self,
+        span: Span,
+        message: impl ToString,
+        annotation_type: AnnotationType,
+    ) -> &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,
+            message: message.to_string(),
+            annotation_type,
+        });
+        self
+    }
+    pub fn footer_annot(
+        &mut self,
+        message: impl ToString,
+        annotation_type: AnnotationType,
+    ) -> &mut Self {
+        self.footer.push(FreeAnnotation {
+            message: message.to_string(),
+            annotation_type,
+        });
+        self
+    }
+
+    pub fn span_err(
+        &mut self,
+        span: Span,
+        message: impl ToString,
+    ) -> &mut Self {
+        self.span_annot(span, message, AnnotationType::Error)
+    }
+    pub fn span_help(
+        &mut self,
+        span: Span,
+        message: impl ToString,
+    ) -> &mut Self {
+        self.span_annot(span, message, AnnotationType::Help)
+    }
+    pub fn help(&mut self, message: impl ToString) -> &mut Self {
+        self.footer_annot(message, AnnotationType::Help)
+    }
+    pub fn note(&mut self, message: impl ToString) -> &mut Self {
+        self.footer_annot(message, AnnotationType::Note)
+    }
+
+    // TODO: handle multiple files
+    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 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 4df018d..6ea7d0c 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -1,10 +1,12 @@
 use std::io::Error as IOError;
 
 use crate::semantics::resolve::ImportStack;
-use crate::semantics::Value;
 use crate::syntax::{Import, ParseError};
 use crate::NormalizedExpr;
 
+mod builder;
+pub(crate) use builder::*;
+
 pub type Result<T> = std::result::Result<T, Error>;
 
 #[derive(Debug)]
@@ -46,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),
@@ -97,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 ae06942..1143781 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -6,6 +6,7 @@ use crate::semantics::nze::lazy;
 use crate::semantics::Binder;
 use crate::semantics::{
     apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
+    TyEnv,
 };
 use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
 use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
@@ -173,9 +174,9 @@ impl Value {
             _ => None,
         }
     }
-    pub(crate) fn span(&self) -> Span {
-        self.0.span.clone()
-    }
+    // 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
@@ -192,6 +193,9 @@ impl Value {
 
         self.to_tyexpr_noenv().to_expr(opts)
     }
+    pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+        self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
+    }
     pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
         self.kind().clone()
     }
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/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 1a048f9..1886646 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -48,8 +48,8 @@ impl TyExpr {
     pub fn kind(&self) -> &TyExprKind {
         &*self.kind
     }
-    pub fn span(&self) -> &Span {
-        &self.span
+    pub fn span(&self) -> Span {
+        self.span.clone()
     }
     pub fn get_type(&self) -> Result<Type, TypeError> {
         match &self.ty {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 20076cd..9a1d0d8 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
 use std::cmp::max;
 use std::collections::HashMap;
 
-use crate::error::{TypeError, TypeMessage};
+use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::semantics::merge_maps;
 use crate::semantics::{
     type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
@@ -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())))
 }
@@ -57,18 +44,61 @@ fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
 fn type_one_layer(
     env: &TyEnv,
     kind: &ExprKind<TyExpr, Normalized>,
+    span: Span,
 ) -> Result<Type, TypeError> {
     Ok(match kind {
         ExprKind::Import(..) => unreachable!(
             "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) => {
@@ -201,10 +231,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,21 +288,47 @@ fn type_one_layer(
             match f.get_type()?.kind() {
                 ValueKind::PiClosure { annot, closure, .. } => {
                     if arg.get_type()? != *annot {
-                        // return mkerr(format!("function annot mismatch"));
-                        return mkerr(format!(
-                            "function annot mismatch: ({} : {}) : {}",
-                            arg.to_expr_tyenv(env),
-                            arg.get_type()?
-                                .to_tyexpr(env.as_varenv())
-                                .to_expr_tyenv(env),
-                            annot.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
-                        ));
+                        return mkerr(
+                            ErrorBuilder::new(format!(
+                                "wrong type of function argument"
+                            ))
+                            .span_err(
+                                f.span(),
+                                format!(
+                                    "this expects an argument of type: {}",
+                                    annot.to_expr_tyenv(env),
+                                ),
+                            )
+                            .span_err(
+                                arg.span(),
+                                format!(
+                                    "but this has type: {}",
+                                    arg.get_type()?.to_expr_tyenv(env),
+                                ),
+                            )
+                            .note(format!(
+                                "expected type `{}`\n   found type `{}`",
+                                annot.to_expr_tyenv(env),
+                                arg.get_type()?.to_expr_tyenv(env),
+                            ))
+                            .format(),
+                        );
                     }
 
                     let arg_nf = arg.eval(env.as_nzenv());
                     closure.apply(arg_nf)
                 }
-                _ => return mkerr(format!("apply to not Pi")),
+                _ => return mkerr(
+                    ErrorBuilder::new(format!(
+                        "expected function, found `{}`",
+                        f.get_type()?.to_expr_tyenv(env)
+                    ))
+                    .span_err(
+                        f.span(),
+                        format!("function application requires a function",),
+                    )
+                    .format(),
+                ),
             }
         }
         ExprKind::BoolIf(x, y, z) => {
@@ -323,7 +381,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)?;
+            let ty = type_one_layer(env, &ekind, Span::Artificial)?;
             TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
                 .eval(env.as_nzenv())
         }
@@ -347,6 +405,7 @@ fn type_one_layer(
                             tx.to_tyexpr(env.as_varenv()),
                             ty.to_tyexpr(env.as_varenv()),
                         ),
+                        Span::Artificial,
                     )?;
                 }
             }
@@ -439,14 +498,73 @@ fn type_one_layer(
                     Some(Some(variant_type)) => match handler_type.kind() {
                         ValueKind::PiClosure { closure, annot, .. } => {
                             if variant_type != annot {
-                                return mkerr("MergeHandlerTypeMismatch");
+                                return mkerr(
+                                    ErrorBuilder::new(format!(
+                                        "Wrong handler input type"
+                                    ))
+                                    .span_err(
+                                        span,
+                                        format!("in this merge expression",),
+                                    )
+                                    .span_err(
+                                        record.span(),
+                                        format!(
+                                            "the handler for `{}` expects a \
+                                             value of type: `{}`",
+                                            x,
+                                            annot.to_expr_tyenv(env)
+                                        ),
+                                    )
+                                    .span_err(
+                                        union.span(),
+                                        format!(
+                                            "but the corresponding variant \
+                                             has type: `{}`",
+                                            variant_type.to_expr_tyenv(env)
+                                        ),
+                                    )
+                                    .format(),
+                                );
                             }
 
                             closure.remove_binder().or_else(|()| {
                                 mkerr("MergeReturnTypeIsDependent")
                             })?
                         }
-                        _ => return mkerr("NotAFunction"),
+                        _ => {
+                            return mkerr(
+                                ErrorBuilder::new(format!(
+                                    "merge handler is not a function"
+                                ))
+                                .span_err(
+                                    span,
+                                    format!("in this merge expression"),
+                                )
+                                .span_err(
+                                    record.span(),
+                                    format!(
+                                        "the handler for `{}` has type: `{}`",
+                                        x,
+                                        handler_type.to_expr_tyenv(env)
+                                    ),
+                                )
+                                .span_help(
+                                    union.span(),
+                                    format!(
+                                        "the corresponding variant has type: \
+                                         `{}`",
+                                        variant_type.to_expr_tyenv(env)
+                                    ),
+                                )
+                                .help(format!(
+                                    "a handler for this variant must be a \
+                                     function that takes an input of type: \
+                                     `{}`",
+                                    variant_type.to_expr_tyenv(env)
+                                ))
+                                .format(),
+                            )
+                        }
                     },
                     // Union alternative without type
                     Some(None) => handler_type.clone(),
@@ -524,62 +642,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)
         }
@@ -587,8 +658,37 @@ 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 ty = type_one_layer(env, &ekind)?;
+            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/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 28a0aee..b493fdb 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -275,6 +275,12 @@ impl<E> Expr<E> {
             span: self.span.clone(),
         }
     }
+    pub fn with_span(self, span: Span) -> Self {
+        Expr {
+            kind: self.kind,
+            span,
+        }
+    }
 
     pub fn traverse_resolve_mut<Err, F1>(
         &mut self,
diff --git a/dhall/src/syntax/ast/span.rs b/dhall/src/syntax/ast/span.rs
index f9c7008..ffdd82c 100644
--- a/dhall/src/syntax/ast/span.rs
+++ b/dhall/src/syntax/ast/span.rs
@@ -24,6 +24,20 @@ pub enum Span {
     Artificial,
 }
 
+impl ParsedSpan {
+    pub(crate) fn to_input(&self) -> String {
+        self.input.to_string()
+    }
+    /// Convert to a char range for consumption by annotate_snippets.
+    /// This compensates for  https://github.com/rust-lang/annotate-snippets-rs/issues/24
+    pub(crate) fn as_char_range(&self) -> (usize, usize) {
+        (
+            char_idx_from_byte_idx(&self.input, self.start),
+            char_idx_from_byte_idx(&self.input, self.end),
+        )
+    }
+}
+
 impl Span {
     pub(crate) fn make(input: Rc<str>, sp: pest::Span) -> Self {
         Span::Parsed(ParsedSpan {
@@ -79,3 +93,19 @@ impl Span {
         format!("{}", err)
     }
 }
+
+/// Convert a byte idx into a string into a char idx for consumption by annotate_snippets.
+fn char_idx_from_byte_idx(input: &str, idx: usize) -> usize {
+    let char_idx = input
+        .char_indices()
+        .enumerate()
+        .find(|(_, (i, _))| *i == idx)
+        .unwrap()
+        .0;
+    // Unix-style newlines are counted as two chars (see
+    // https://github.com/rust-lang/annotate-snippets-rs/issues/24).
+    let nbr_newlines = input[..idx].chars().filter(|c| *c == '\n').count();
+    let nbr_carriage_returns =
+        input[..idx].chars().filter(|c| *c == '\r').count();
+    char_idx + nbr_newlines - nbr_carriage_returns
+}
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 2ec63e2..8d571c0 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -11,7 +11,7 @@ use crate::syntax::ExprKind::*;
 use crate::syntax::{
     Double, FilePath, FilePrefix, Hash, ImportLocation, ImportMode, Integer,
     InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, Natural,
-    Scheme, Span, UnspannedExpr, URL, V,
+    Scheme, Span, URL, V,
 };
 use crate::Normalized;
 
@@ -21,6 +21,7 @@ use crate::Normalized;
 // are here and hopefully you can figure out how they work.
 
 type Expr = syntax::Expr<Normalized>;
+type UnspannedExpr = syntax::UnspannedExpr<Normalized>;
 type ParsedText = InterpolatedText<Expr>;
 type ParsedTextContents = InterpolatedTextContents<Expr>;
 type ParseInput<'input> = pest_consume::Node<'input, Rule, Rc<str>>;
@@ -78,14 +79,10 @@ impl crate::syntax::Builtin {
 fn input_to_span(input: ParseInput) -> Span {
     Span::make(input.user_data().clone(), input.as_pair().as_span())
 }
-fn spanned(input: ParseInput, x: UnspannedExpr<Normalized>) -> Expr {
+fn spanned(input: ParseInput, x: UnspannedExpr) -> Expr {
     Expr::new(x, input_to_span(input))
 }
-fn spanned_union(
-    span1: Span,
-    span2: Span,
-    x: UnspannedExpr<Normalized>,
-) -> Expr {
+fn spanned_union(span1: Span, span2: Span, x: UnspannedExpr) -> Expr {
     Expr::new(x, span1.union(&span2))
 }
 
@@ -845,25 +842,27 @@ impl DhallParser {
             [integer_literal(n)] => spanned(input, IntegerLit(n)),
             [double_quote_literal(s)] => spanned(input, TextLit(s)),
             [single_quote_literal(s)] => spanned(input, TextLit(s)),
+            [record_type_or_literal(e)] => spanned(input, e),
+            [union_type(e)] => spanned(input, e),
             [expression(e)] => e,
         ))
     }
 
-    #[alias(expression)]
-    fn empty_record_literal(input: ParseInput) -> ParseResult<Expr> {
-        Ok(spanned(input, RecordLit(Default::default())))
+    #[alias(record_type_or_literal)]
+    fn empty_record_literal(input: ParseInput) -> ParseResult<UnspannedExpr> {
+        Ok(RecordLit(Default::default()))
     }
 
-    #[alias(expression)]
-    fn empty_record_type(input: ParseInput) -> ParseResult<Expr> {
-        Ok(spanned(input, RecordType(Default::default())))
+    #[alias(record_type_or_literal)]
+    fn empty_record_type(input: ParseInput) -> ParseResult<UnspannedExpr> {
+        Ok(RecordType(Default::default()))
     }
 
-    #[alias(expression)]
+    #[alias(record_type_or_literal)]
     fn non_empty_record_type_or_literal(
         input: ParseInput,
-    ) -> ParseResult<Expr> {
-        let e = match_nodes!(input.children();
+    ) -> ParseResult<UnspannedExpr> {
+        Ok(match_nodes!(input.children();
             [label(first_label), non_empty_record_type(rest)] => {
                 let (first_expr, mut map) = rest;
                 map.insert(first_label, first_expr);
@@ -874,8 +873,7 @@ impl DhallParser {
                 map.insert(first_label, first_expr);
                 RecordLit(map)
             },
-        );
-        Ok(spanned(input, e))
+        ))
     }
 
     fn non_empty_record_type(
@@ -910,13 +908,12 @@ impl DhallParser {
         ))
     }
 
-    #[alias(expression)]
-    fn union_type(input: ParseInput) -> ParseResult<Expr> {
+    fn union_type(input: ParseInput) -> ParseResult<UnspannedExpr> {
         let map = match_nodes!(input.children();
             [empty_union_type(_)] => Default::default(),
             [union_type_entry(entries)..] => entries.collect(),
         );
-        Ok(spanned(input, UnionType(map)))
+        Ok(UnionType(map))
     }
 
     fn empty_union_type(_input: ParseInput) -> ParseResult<()> {
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 4dfdcf5..522e1a2 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1 +1,15 @@
-Type error: Unhandled error: function annot mismatch: (U : Sort) : Kind
+Type error: Unhandled error: error: wrong type of function argument
+  --> <current file>:6:23
+   |
+ 1 |     let bottom : Type = ∀(any : Type) → any
+ 2 | 
+ 3 | in  let not : Type → Type = λ(p : Type) → p → bottom
+ 4 | 
+...
+10 |         : pow (pow U) → U
+11 |         =   λ(t : pow (pow U))
+   |                        ^^^ this expects an argument of type: Kind
+   |                            ^ but this has type: Sort
+   |
+   = note: expected type `Kind`
+              found 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 8d101c3..01facbc 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:1:1
+  |
+1 | (λ(_ : Natural) → _) True
+  |  ^^^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
+  |                      ^^^^ but this has type: Bool
+  |
+  = note: expected type `Natural`
+             found type `Bool`
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
index a72e120..f779fd6 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: apply to not Pi
+Type error: Unhandled error: error: expected function, found `Bool`
+ --> <current file>:1:0
+  |
+1 | True True
+  | ^^^^ function application requires a function
+  |
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 070e461..aa7c8c5 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: function annot mismatch: (Type : Kind) : Type
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:1:5
+  |
+1 | [] : List Type
+  |      ^^^^ this expects an argument of type: Type
+  |           ^^^^ but this has type: Kind
+  |
+  = note: expected type `Type`
+             found type `Kind`
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
index f1cdf92..053a054 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: NotAFunction
+Type error: Unhandled error: error: merge handler is not a function
+ --> <current file>:1:0
+  |
+1 | merge { x = True } (< x : Bool >.x True)
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression
+  |       ^^^^^^^^^^^^ the handler for `x` has type: `Bool`
+  |                     ------------------- help: the corresponding variant has type: `Bool`
+  |
+  = help: a handler for this variant must be a function that takes an input of type: `Bool`
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
index 8b729a4..faca63a 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -1 +1,8 @@
-Type error: Unhandled error: MergeHandlerTypeMismatch
+Type error: Unhandled error: error: Wrong handler input type
+ --> <current file>:1:0
+  |
+1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1)
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression
+  |       ^^^^^^^^^^^^^^^^^^^^^^^ the handler for `x` expects a value of type: `Bool`
+  |                                ^^^^^^^^^^^^^^^^^^^ but the corresponding variant has type: `Natural`
+  |
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
index 8d101c3..7e410c4 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:1:0
+  |
+1 | Natural/subtract True True
+  | ^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
+  |                  ^^^^ but this has type: Bool
+  |
+  = note: expected type `Natural`
+             found 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/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs
index 0381fec..7bf6d30 100644
--- a/serde_dhall/src/lib.rs
+++ b/serde_dhall/src/lib.rs
@@ -181,8 +181,8 @@ pub use value::Value;
 // A Dhall value.
 #[doc(hidden)]
 pub mod value {
-    use dhall::{Normalized, NormalizedExpr, Parsed};
     use dhall::syntax::Builtin;
+    use dhall::{Normalized, NormalizedExpr, Parsed};
 
     use super::de::{Error, Result};
 
diff --git a/serde_dhall/src/serde.rs b/serde_dhall/src/serde.rs
index 336330a..3e78987 100644
--- a/serde_dhall/src/serde.rs
+++ b/serde_dhall/src/serde.rs
@@ -4,8 +4,8 @@ use serde::de::value::{
     MapAccessDeserializer, MapDeserializer, SeqDeserializer,
 };
 
-use dhall::NormalizedExpr;
 use dhall::syntax::ExprKind;
+use dhall::NormalizedExpr;
 
 use crate::de::{Deserialize, Error, Result};
 use crate::Value;
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