Tweak errors

9 files changed, 63 insertions, 65 deletions

diff --git a/dhall/src/error/builder.rs b/dhall/src/error/builder.rs
index 8c7eef3..39f8dfb 100644
--- a/dhall/src/error/builder.rs
+++ b/dhall/src/error/builder.rs
@@ -63,12 +63,6 @@ impl ErrorBuilder {
             consumed: false,
         }
     }
-    pub fn new_span_err(span: Span, message: impl ToString) -> Self {
-        let message = message.to_string();
-        let mut builder = Self::new(message.clone());
-        builder.span_err(span, message);
-        builder
-    }
 
     pub fn span_annot(
         &mut self,
@@ -117,6 +111,9 @@ impl ErrorBuilder {
     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 {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7518e90..9a1d0d8 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -284,53 +284,53 @@ 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(
-                        ErrorBuilder::new_span_err(
-                            &span,
-                            format!("Wrong type of function argument"),
-                        )
-                        .span_err(
-                            &f.span(),
-                            format!(
-                                "this expects an argument of type: {}",
+        ExprKind::App(f, arg) => {
+            match f.get_type()?.kind() {
+                ValueKind::PiClosure { annot, closure, .. } => {
+                    if arg.get_type()? != *annot {
+                        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),
-                            ),
-                        )
-                        .span_err(
-                            &arg.span(),
-                            format!(
-                                "but this has type: {}",
                                 arg.get_type()?.to_expr_tyenv(env),
-                            ),
-                        )
-                        .format(),
-                    );
-                }
+                            ))
+                            .format(),
+                        );
+                    }
 
-                let arg_nf = arg.eval(env.as_nzenv());
-                closure.apply(arg_nf)
-            }
-            _ => {
-                return mkerr(
+                    let arg_nf = arg.eval(env.as_nzenv());
+                    closure.apply(arg_nf)
+                }
+                _ => return mkerr(
                     ErrorBuilder::new(format!(
-                        "Trying to apply an argument to a value that is not a \
-                         function"
+                        "expected function, found `{}`",
+                        f.get_type()?.to_expr_tyenv(env)
                     ))
                     .span_err(
-                        &f.span(),
-                        format!(
-                            "this has type: `{}`",
-                            f.get_type()?.to_expr_tyenv(env)
-                        ),
+                        f.span(),
+                        format!("function application requires a function",),
                     )
-                    .help("only functions can be applied to")
                     .format(),
-                )
+                ),
             }
-        },
+        }
         ExprKind::BoolIf(x, y, z) => {
             if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return mkerr("InvalidPredicate");
@@ -509,8 +509,8 @@ fn type_one_layer(
                                     .span_err(
                                         record.span(),
                                         format!(
-                                            "the handler `{}` expects a value \
-                                             of type: `{}`",
+                                            "the handler for `{}` expects a \
+                                             value of type: `{}`",
                                             x,
                                             annot.to_expr_tyenv(env)
                                         ),
@@ -523,7 +523,6 @@ fn type_one_layer(
                                             variant_type.to_expr_tyenv(env)
                                         ),
                                     )
-                                    .help("only functions can be applied to")
                                     .format(),
                                 );
                             }
@@ -535,16 +534,16 @@ fn type_one_layer(
                         _ => {
                             return mkerr(
                                 ErrorBuilder::new(format!(
-                                    "Handler is not a function"
+                                    "merge handler is not a function"
                                 ))
                                 .span_err(
                                     span,
-                                    format!("in this merge expression",),
+                                    format!("in this merge expression"),
                                 )
                                 .span_err(
                                     record.span(),
                                     format!(
-                                        "the handler `{}` had type: `{}`",
+                                        "the handler for `{}` has type: `{}`",
                                         x,
                                         handler_type.to_expr_tyenv(env)
                                     ),
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 5241517..522e1a2 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1,4 +1,4 @@
-Type error: Unhandled error: error: Wrong type of function argument
+Type error: Unhandled error: error: wrong type of function argument
   --> <current file>:6:23
    |
  1 |     let bottom : Type = ∀(any : Type) → any
@@ -8,7 +8,8 @@ Type error: Unhandled error: error: Wrong type of function argument
 ...
 10 |         : pow (pow U) → U
 11 |         =   λ(t : pow (pow U))
-   |                        ^^^^^ Wrong type of function argument
    |                        ^^^ 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/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
index d8811c2..01facbc 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1,8 +1,9 @@
-Type error: Unhandled error: error: Wrong type of function argument
+Type error: Unhandled error: error: wrong type of function argument
  --> <current file>:1:1
   |
 1 | (λ(_ : Natural) → _) True
-  |  ^^^^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument
   |  ^^^^^^^^^^^^^^^^^^ 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 0732d1c..f779fd6 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -1,7 +1,6 @@
-Type error: Unhandled error: error: Trying to apply an argument to a value that is not a function
+Type error: Unhandled error: error: expected function, found `Bool`
  --> <current file>:1:0
   |
 1 | True True
-  | ^^^^ this has type: `Bool`
+  | ^^^^ function application requires a function
   |
-  = help: only functions can be applied to
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
index 1459ca1..aa7c8c5 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1,8 +1,9 @@
-Type error: Unhandled error: error: Wrong type of function argument
+Type error: Unhandled error: error: wrong type of function argument
  --> <current file>:1:5
   |
 1 | [] : List Type
-  |      ^^^^^^^^^ Wrong type of function argument
   |      ^^^^ 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 3a12c06..053a054 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
@@ -1,9 +1,9 @@
-Type error: Unhandled error: error: Handler is not a function
+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 `x` had type: `Bool`
+  |       ^^^^^^^^^^^^ 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 2afbc78..faca63a 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -3,7 +3,6 @@ Type error: Unhandled error: error: Wrong handler input type
   |
 1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression
-  |       ^^^^^^^^^^^^^^^^^^^^^^^ the handler `x` expects a value of type: `Bool`
+  |       ^^^^^^^^^^^^^^^^^^^^^^^ the handler for `x` expects a value of type: `Bool`
   |                                ^^^^^^^^^^^^^^^^^^^ but the corresponding variant has type: `Natural`
   |
-  = help: only functions can be applied to
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
index a35b9ab..7e410c4 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1,8 +1,9 @@
-Type error: Unhandled error: error: Wrong type of function argument
+Type error: Unhandled error: error: wrong type of function argument
  --> <current file>:1:0
   |
 1 | Natural/subtract True True
-  | ^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument
   | ^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
   |                  ^^^^ but this has type: Bool
   |
+  = note: expected type `Natural`
+             found type `Bool`