From 70eede4fd012f49dfab0e2e27fb3a4e4bbff6325 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 1 Feb 2020 22:04:34 +0000 Subject: Implement once nice error using annotate_snippets --- dhall/src/semantics/nze/value.rs | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'dhall/src/semantics/nze') 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() } -- cgit v1.3.1 From 92bbea48f9a0380a614f2687c73d55a67ff9294e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 2 Feb 2020 15:02:23 +0000 Subject: More nice errors plus some refactor --- dhall/src/error/builder.rs | 169 +++++++++++------ dhall/src/error/mod.rs | 9 - dhall/src/semantics/nze/value.rs | 3 - dhall/src/semantics/tck/env.rs | 6 +- dhall/src/semantics/tck/typecheck.rs | 204 +++++++++++---------- dhall/tests/type-errors/hurkensParadox.txt | 4 +- dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 7 +- .../unit/FunctionApplicationArgumentNotMatch.txt | 4 +- .../unit/FunctionArgumentTypeNotAType.txt | 8 +- .../unit/FunctionTypeArgumentTypeNotAType.txt | 8 +- .../type-errors/unit/ListLiteralEmptyNotType.txt | 4 +- .../type-errors/unit/NaturalSubtractNotNatural.txt | 4 +- .../unit/UnionDeprecatedConstructorsKeyword.txt | 7 +- dhall/tests/type-errors/unit/VariableFree.txt | 7 +- tests_buffer | 2 + 15 files changed, 272 insertions(+), 174 deletions(-) (limited to 'dhall/src/semantics/nze') 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, + footer: Vec, + /// 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, } #[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("".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 { - 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(x: S) -> Result { 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 { 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 --> :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 ``_`` + --> :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 --> :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` + --> :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` + --> :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 --> :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 --> :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` + --> :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` + --> :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 -- cgit v1.3.1 From d8c3ced0f1acb1924c801fadbfd3077dede9b0dd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 2 Feb 2020 17:22:27 +0000 Subject: More errors --- dhall/src/error/builder.rs | 40 ++++++----- dhall/src/semantics/nze/value.rs | 3 + dhall/src/semantics/tck/typecheck.rs | 84 ++++++++++++++++++++-- dhall/tests/type-errors/hurkensParadox.txt | 4 +- .../unit/FunctionApplicationArgumentNotMatch.txt | 4 +- .../unit/FunctionApplicationIsNotFunction.txt | 8 ++- .../type-errors/unit/ListLiteralEmptyNotType.txt | 4 +- .../type-errors/unit/MergeHandlerNotFunction.txt | 10 ++- .../unit/MergeHandlerNotMatchAlternativeType.txt | 10 ++- .../type-errors/unit/NaturalSubtractNotNatural.txt | 4 +- serde_dhall/src/lib.rs | 2 +- serde_dhall/src/serde.rs | 2 +- 12 files changed, 140 insertions(+), 35 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/error/builder.rs b/dhall/src/error/builder.rs index 22b0d77..29d0d35 100644 --- a/dhall/src/error/builder.rs +++ b/dhall/src/error/builder.rs @@ -70,10 +70,11 @@ impl ErrorBuilder { builder } - pub fn span_err( + 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 { @@ -83,33 +84,38 @@ impl ErrorBuilder { self.annotations.push(SpannedAnnotation { span: span.clone(), message: message.to_string(), - annotation_type: AnnotationType::Error, + annotation_type, }); self } - pub fn span_help( + pub fn footer_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: span.clone(), + self.footer.push(FreeAnnotation { message: message.to_string(), - annotation_type: AnnotationType::Help, + 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.push(FreeAnnotation { - message: message.to_string(), - annotation_type: AnnotationType::Help, - }); - self + self.footer_annot(message, AnnotationType::Help) } // TODO: handle multiple files diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index bb3e3c0..d97b8c4 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -174,6 +174,9 @@ 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/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index e642b8f..d99f549 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -293,14 +293,14 @@ fn type_one_layer( &span, format!("Wrong type of function argument"), ) - .span_help( + .span_err( &f.span(), format!( "this expects an argument of type: {}", annot.to_expr_tyenv(env), ), ) - .span_help( + .span_err( &arg.span(), format!( "but this has type: {}", @@ -314,7 +314,23 @@ fn type_one_layer( let arg_nf = arg.eval(env.as_nzenv()); closure.apply(arg_nf) } - _ => return mkerr(format!("apply to not Pi")), + _ => { + return mkerr( + ErrorBuilder::new(format!( + "Trying to apply an argument \ + to a value that is not a function" + )) + .span_err( + &f.span(), + format!( + "this has type: `{}`", + f.get_type()?.to_expr_tyenv(env) + ), + ) + .help("only functions can be applied to") + .format(), + ) + } }, ExprKind::BoolIf(x, y, z) => { if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) { @@ -483,14 +499,72 @@ 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 `{}` 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) + ), + ) + .help("only functions can be applied to") + .format(), + ); } closure.remove_binder().or_else(|()| { mkerr("MergeReturnTypeIsDependent") })? } - _ => return mkerr("NotAFunction"), + _ => + return mkerr( + ErrorBuilder::new(format!( + "Handler is not a function" + )) + .span_err( + &span, + format!( + "in this merge expression", + ), + ) + .span_err( + &record.span(), + format!( + "the handler `{}` had 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(), diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index e06c4b2..5241517 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -9,6 +9,6 @@ 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 - | --- help: this expects an argument of type: Kind - | - help: but this has type: Sort + | ^^^ this expects an argument of type: Kind + | ^ but this has type: Sort | diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 776b14e..d8811c2 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -3,6 +3,6 @@ Type error: Unhandled error: error: Wrong type of function argument | 1 | (λ(_ : Natural) → _) True | ^^^^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument - | ------------------ help: this expects an argument of type: Natural - | ---- help: but this has type: Bool + | ^^^^^^^^^^^^^^^^^^ this expects an argument of type: Natural + | ^^^^ but this has type: Bool | diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt index a72e120..0732d1c 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -1 +1,7 @@ -Type error: Unhandled error: apply to not Pi +Type error: Unhandled error: error: Trying to apply an argument to a value that is not a function + --> :1:0 + | +1 | True True + | ^^^^ this has type: `Bool` + | + = 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 125cc87..1459ca1 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -3,6 +3,6 @@ Type error: Unhandled error: error: Wrong type of function argument | 1 | [] : List Type | ^^^^^^^^^ Wrong type of function argument - | ---- help: this expects an argument of type: Type - | ---- help: but this has type: Kind + | ^^^^ this expects an argument of type: Type + | ^^^^ but this has type: Kind | diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt index f1cdf92..16931a8 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: Handler is not a function + --> :1:0 + | +1 | merge { x = True } (< x : Bool >.x True) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression + | ^^^^^^^^ the handler `x` had 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..1762a7c 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -1 +1,9 @@ -Type error: Unhandled error: MergeHandlerTypeMismatch +Type error: Unhandled error: error: Wrong handler input type + --> :1:0 + | +1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression + | ^^^^^^^^^^^^^^^^^^^ the handler `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 5ee2a11..a35b9ab 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -3,6 +3,6 @@ Type error: Unhandled error: error: Wrong type of function argument | 1 | Natural/subtract True True | ^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument - | ---------------- help: this expects an argument of type: Natural - | ---- help: but this has type: Bool + | ^^^^^^^^^^^^^^^^ this expects an argument of type: Natural + | ^^^^ but this has type: Bool | 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; -- cgit v1.3.1 From b6625eccbf3f2d1bcfe1a88f4d556439281e91de Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 2 Feb 2020 17:49:49 +0000 Subject: Use Spans consistently by value --- dhall/src/error/builder.rs | 10 +++++----- dhall/src/semantics/nze/value.rs | 6 +++--- dhall/src/semantics/tck/tyexpr.rs | 4 ++-- dhall/src/semantics/tck/typecheck.rs | 16 ++++++++-------- dhall/src/syntax/text/parser.rs | 6 +----- 5 files changed, 19 insertions(+), 23 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/error/builder.rs b/dhall/src/error/builder.rs index 29d0d35..8c7eef3 100644 --- a/dhall/src/error/builder.rs +++ b/dhall/src/error/builder.rs @@ -63,7 +63,7 @@ impl ErrorBuilder { consumed: false, } } - pub fn new_span_err(span: &Span, message: impl ToString) -> 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.span_err(span, message); @@ -72,7 +72,7 @@ impl ErrorBuilder { pub fn span_annot( &mut self, - span: &Span, + span: Span, message: impl ToString, annotation_type: AnnotationType, ) -> &mut Self { @@ -82,7 +82,7 @@ impl ErrorBuilder { _ => return self, }; self.annotations.push(SpannedAnnotation { - span: span.clone(), + span, message: message.to_string(), annotation_type, }); @@ -102,14 +102,14 @@ impl ErrorBuilder { pub fn span_err( &mut self, - span: &Span, + span: Span, message: impl ToString, ) -> &mut Self { self.span_annot(span, message, AnnotationType::Error) } pub fn span_help( &mut self, - span: &Span, + span: Span, message: impl ToString, ) -> &mut Self { self.span_annot(span, message, AnnotationType::Help) diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index d97b8c4..1143781 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -174,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 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 { match &self.ty { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 48794a8..7518e90 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -76,7 +76,7 @@ fn type_one_layer( annot.get_type()?.to_expr_tyenv(env), )) .span_err( - &annot.span(), + annot.span(), format!( "this has type: `{}`", annot.get_type()?.to_expr_tyenv(env) @@ -503,11 +503,11 @@ fn type_one_layer( "Wrong handler input type" )) .span_err( - &span, + span, format!("in this merge expression",), ) .span_err( - &record.span(), + record.span(), format!( "the handler `{}` expects a value \ of type: `{}`", @@ -516,7 +516,7 @@ fn type_one_layer( ), ) .span_err( - &union.span(), + union.span(), format!( "but the corresponding variant \ has type: `{}`", @@ -538,11 +538,11 @@ fn type_one_layer( "Handler is not a function" )) .span_err( - &span, + span, format!("in this merge expression",), ) .span_err( - &record.span(), + record.span(), format!( "the handler `{}` had type: `{}`", x, @@ -550,7 +550,7 @@ fn type_one_layer( ), ) .span_help( - &union.span(), + union.span(), format!( "the corresponding variant has type: \ `{}`", @@ -647,7 +647,7 @@ pub(crate) fn type_with( None => { return mkerr( ErrorBuilder::new(format!("unbound variable `{}`", var)) - .span_err(&expr.span(), "not found in this scope") + .span_err(expr.span(), "not found in this scope") .format(), ) } diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs index ceae2cd..8d571c0 100644 --- a/dhall/src/syntax/text/parser.rs +++ b/dhall/src/syntax/text/parser.rs @@ -82,11 +82,7 @@ fn input_to_span(input: ParseInput) -> Span { fn spanned(input: ParseInput, x: UnspannedExpr) -> Expr { Expr::new(x, input_to_span(input)) } -fn spanned_union( - span1: Span, - span2: Span, - x: UnspannedExpr, -) -> Expr { +fn spanned_union(span1: Span, span2: Span, x: UnspannedExpr) -> Expr { Expr::new(x, span1.union(&span2)) } -- cgit v1.3.1