Implement once nice error using annotate_snippets

11 files changed, 216 insertions, 27 deletions

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..e293220
--- /dev/null
+++ b/dhall/src/error/builder.rs
@@ -0,0 +1,100 @@
+use annotate_snippets::{
+    display_list::DisplayList,
+    formatter::DisplayListFormatter,
+    snippet::{Annotation, AnnotationType, Slice, Snippet, SourceAnnotation},
+};
+
+use crate::syntax::Span;
+
+#[derive(Debug, Clone)]
+pub struct ErrorBuilder {
+    message: String,
+    annotation_type: AnnotationType,
+    annotations: Vec<BuilderAnnotation>,
+}
+
+#[derive(Debug, Clone)]
+struct BuilderAnnotation {
+    span: Span,
+    message: String,
+    annotation_type: AnnotationType,
+}
+
+/// 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 {
+        ErrorBuilder {
+            message,
+            annotation_type: AnnotationType::Error,
+            annotations: Vec::new(),
+        }
+    }
+    pub fn span_err(span: &Span, message: String) -> Self {
+        let mut builder = Self::new(message.clone());
+        builder.annotate_err(span, message);
+        builder
+    }
+
+    pub fn annotate_err(&mut self, span: &Span, message: String) {
+        self.annotations.push(BuilderAnnotation {
+            span: span.clone(),
+            message,
+            annotation_type: AnnotationType::Error,
+        })
+    }
+    pub fn annotate_info(&mut self, span: &Span, message: String) {
+        self.annotations.push(BuilderAnnotation {
+            span: span.clone(),
+            message,
+            annotation_type: AnnotationType::Help,
+        })
+    }
+
+    // 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),
+        };
+
+        let snippet = Snippet {
+            title: Some(Annotation {
+                label: Some(self.message),
+                id: None,
+                annotation_type: self.annotation_type,
+            }),
+            footer: vec![],
+            slices: vec![Slice {
+                source: input,
+                line_start: 1, // TODO
+                origin: Some("<current file>".to_string()),
+                fold: true,
+                annotations,
+            }],
+        };
+        let dl = DisplayList::from(snippet);
+        let dlf = DisplayListFormatter::new(true, false);
+        format!("{}", dlf.format(&dl))
+    }
+}
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 4df018d..5b7693e 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -5,6 +5,9 @@ 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)]
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index ae06942..d97b8c4 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};
@@ -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/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 20076cd..a652663 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,
@@ -57,6 +57,7 @@ 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!(
@@ -252,27 +253,35 @@ fn type_one_layer(
             }
             t
         }
-        ExprKind::App(f, arg) => {
-            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),
-                        ));
-                    }
-
-                    let arg_nf = arg.eval(env.as_nzenv());
-                    closure.apply(arg_nf)
+        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),
+                        ),
+                    );
+                    builder.annotate_info(
+                        &arg.span(),
+                        format!(
+                            "but this has type: {}",
+                            arg.get_type()?.to_expr_tyenv(env),
+                        ),
+                    );
+                    return mkerr(builder.format());
                 }
-                _ => return mkerr(format!("apply to not Pi")),
+
+                let arg_nf = arg.eval(env.as_nzenv());
+                closure.apply(arg_nf)
             }
-        }
+            _ => return mkerr(format!("apply to not Pi")),
+        },
         ExprKind::BoolIf(x, y, z) => {
             if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return mkerr("InvalidPredicate");
@@ -323,7 +332,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 +356,7 @@ fn type_one_layer(
                             tx.to_tyexpr(env.as_varenv()),
                             ty.to_tyexpr(env.as_varenv()),
                         ),
+                        Span::Artificial,
                     )?;
                 }
             }
@@ -588,7 +598,7 @@ pub(crate) fn type_with(
         }
         ekind => {
             let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
-            let ty = type_one_layer(env, &ekind)?;
+            let ty = type_one_layer(env, &ekind, expr.span())?;
             (TyExprKind::Expr(ekind), Some(ty))
         }
     };
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/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 4dfdcf5..10bb9a4 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1 +1,14 @@
-Type error: Unhandled error: function annot mismatch: (U : Sort) : Kind
+Type error: Unhandled error: error: function annot mismatch
+  --> <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))
+   |                        ^^^^^ function annot mismatch
+   |                        --- help: this expects an argument of type: Kind
+   |                            - help: but this has type: Sort
+   |
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
index 8d101c3..7aa2281 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1 +1,8 @@
-Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
+Type error: Unhandled error: error: function annot mismatch
+ --> <current file>:1:1
+  |
+1 | (λ(_ : Natural) → _) True
+  |  ^^^^^^^^^^^^^^^^^^^^^^^^ function annot mismatch
+  |  ------------------ help: this expects an argument of type: Natural
+  |                      ---- help: but this has type: Bool
+  |
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
index 070e461..3673338 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1 +1,8 @@
-Type error: Unhandled error: function annot mismatch: (Type : Kind) : Type
+Type error: Unhandled error: error: function annot mismatch
+ --> <current file>:1:5
+  |
+1 | [] : List Type
+  |      ^^^^^^^^^ function annot mismatch
+  |      ---- 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 8d101c3..795c97c 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1 +1,8 @@
-Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
+Type error: Unhandled error: error: function annot mismatch
+ --> <current file>:1:0
+  |
+1 | Natural/subtract True True
+  | ^^^^^^^^^^^^^^^^^^^^^ function annot mismatch
+  | ---------------- help: this expects an argument of type: Natural
+  |                  ---- help: but this has type: Bool
+  |