summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/error/builder.rs169
-rw-r--r--dhall/src/error/mod.rs9
-rw-r--r--dhall/src/semantics/nze/value.rs3
-rw-r--r--dhall/src/semantics/tck/env.rs6
-rw-r--r--dhall/src/semantics/tck/typecheck.rs204
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt4
-rw-r--r--dhall/tests/type-errors/unit/AssertAlphaTrap.txt7
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt4
-rw-r--r--dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt8
-rw-r--r--dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt8
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt4
-rw-r--r--dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt4
-rw-r--r--dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt7
-rw-r--r--dhall/tests/type-errors/unit/VariableFree.txt7
-rw-r--r--tests_buffer2
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-31 14:58:19 +0000