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 --- Cargo.lock | 7 ++ dhall/Cargo.toml | 3 +- dhall/src/error/builder.rs | 100 +++++++++++++++++++++ dhall/src/error/mod.rs | 3 + dhall/src/semantics/nze/value.rs | 4 + dhall/src/semantics/tck/typecheck.rs | 54 ++++++----- dhall/src/syntax/ast/span.rs | 30 +++++++ dhall/tests/type-errors/hurkensParadox.txt | 15 +++- .../unit/FunctionApplicationArgumentNotMatch.txt | 9 +- .../type-errors/unit/ListLiteralEmptyNotType.txt | 9 +- .../type-errors/unit/NaturalSubtractNotNatural.txt | 9 +- 11 files changed, 216 insertions(+), 27 deletions(-) create mode 100644 dhall/src/error/builder.rs diff --git a/Cargo.lock b/Cargo.lock index c737e52..450a1da 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -18,6 +18,11 @@ dependencies = [ "pretty 0.5.2 (registry+https://github.com/rust-lang/crates.io-index)", ] +[[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" @@ -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, +} + +#[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("".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 = std::result::Result; #[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(x: S) -> Result { fn type_one_layer( env: &TyEnv, kind: &ExprKind, + span: Span, ) -> Result { 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, 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 + --> :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 + --> :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 + --> :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 + --> :1:0 + | +1 | Natural/subtract True True + | ^^^^^^^^^^^^^^^^^^^^^ function annot mismatch + | ---------------- help: this expects an argument of type: Natural + | ---- help: but this has type: Bool + | -- cgit v1.2.3 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(-) 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.2.3 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(-) 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.2.3 From 47167b874179bd6e659f0a596defcfe854369618 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 2 Feb 2020 17:23:20 +0000 Subject: Let rustfmt format string literals --- .rustfmt.toml | 1 + dhall/src/semantics/tck/typecheck.rs | 87 ++++++++++++++++++------------------ 2 files changed, 45 insertions(+), 43 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/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index d99f549..48794a8 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -82,11 +82,10 @@ fn type_one_layer( annot.get_type()?.to_expr_tyenv(env) ), ) - .help( - format!( - "The input type of a function must have type `Type`, `Kind` or `Sort`", - ), - ) + .help(format!( + "The input type of a function must have type \ + `Type`, `Kind` or `Sort`", + )) .format(), ); } @@ -317,8 +316,8 @@ fn type_one_layer( _ => { return mkerr( ErrorBuilder::new(format!( - "Trying to apply an argument \ - to a value that is not a function" + "Trying to apply an argument to a value that is not a \ + function" )) .span_err( &f.span(), @@ -505,14 +504,13 @@ fn type_one_layer( )) .span_err( &span, - format!( - "in this merge expression", - ), + format!("in this merge expression",), ) .span_err( &record.span(), format!( - "the handler `{}` expects a value of type: `{}`", + "the handler `{}` expects a value \ + of type: `{}`", x, annot.to_expr_tyenv(env) ), @@ -520,7 +518,8 @@ fn type_one_layer( .span_err( &union.span(), format!( - "but the corresponding variant has type: `{}`", + "but the corresponding variant \ + has type: `{}`", variant_type.to_expr_tyenv(env) ), ) @@ -533,38 +532,40 @@ fn type_one_layer( mkerr("MergeReturnTypeIsDependent") })? } - _ => - 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(), + _ => { + 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(), -- cgit v1.2.3 From 4f98c23963e82eaf08c9d7291d0988d13571d337 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 2 Feb 2020 17:36:15 +0000 Subject: Fix spans for unions and records --- dhall/src/syntax/ast/expr.rs | 6 ++++ dhall/src/syntax/text/parser.rs | 35 +++++++++++----------- .../type-errors/unit/MergeHandlerNotFunction.txt | 4 +-- .../unit/MergeHandlerNotMatchAlternativeType.txt | 4 +-- 4 files changed, 28 insertions(+), 21 deletions(-) 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 Expr { span: self.span.clone(), } } + pub fn with_span(self, span: Span) -> Self { + Expr { + kind: self.kind, + span, + } + } pub fn traverse_resolve_mut( &mut self, diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs index 2ec63e2..ceae2cd 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; +type UnspannedExpr = syntax::UnspannedExpr; type ParsedText = InterpolatedText; type ParsedTextContents = InterpolatedTextContents; type ParseInput<'input> = pest_consume::Node<'input, Rule, Rc>; @@ -78,13 +79,13 @@ 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) -> Expr { +fn spanned(input: ParseInput, x: UnspannedExpr) -> Expr { Expr::new(x, input_to_span(input)) } fn spanned_union( span1: Span, span2: Span, - x: UnspannedExpr, + x: UnspannedExpr, ) -> Expr { Expr::new(x, span1.union(&span2)) } @@ -845,25 +846,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 { - Ok(spanned(input, RecordLit(Default::default()))) + #[alias(record_type_or_literal)] + fn empty_record_literal(input: ParseInput) -> ParseResult { + Ok(RecordLit(Default::default())) } - #[alias(expression)] - fn empty_record_type(input: ParseInput) -> ParseResult { - Ok(spanned(input, RecordType(Default::default()))) + #[alias(record_type_or_literal)] + fn empty_record_type(input: ParseInput) -> ParseResult { + Ok(RecordType(Default::default())) } - #[alias(expression)] + #[alias(record_type_or_literal)] fn non_empty_record_type_or_literal( input: ParseInput, - ) -> ParseResult { - let e = match_nodes!(input.children(); + ) -> ParseResult { + 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 +877,7 @@ impl DhallParser { map.insert(first_label, first_expr); RecordLit(map) }, - ); - Ok(spanned(input, e)) + )) } fn non_empty_record_type( @@ -910,13 +912,12 @@ impl DhallParser { )) } - #[alias(expression)] - fn union_type(input: ParseInput) -> ParseResult { + fn union_type(input: ParseInput) -> ParseResult { 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/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt index 16931a8..3a12c06 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt @@ -3,7 +3,7 @@ Type error: Unhandled error: error: Handler is not a function | 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` + | ^^^^^^^^^^^^ 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 1762a7c..2afbc78 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -3,7 +3,7 @@ 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` - | ^^^^^^^^^^^^^^^^^ but the corresponding variant has type: `Natural` + | ^^^^^^^^^^^^^^^^^^^^^^^ the handler `x` expects a value of type: `Bool` + | ^^^^^^^^^^^^^^^^^^^ but the corresponding variant has type: `Natural` | = help: only functions can be applied to -- cgit v1.2.3 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(-) 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.2.3 From f3681f7a32ddb78db4d564769b50b697c54ebeac Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 2 Feb 2020 18:03:03 +0000 Subject: Tweak errors --- dhall/src/error/builder.rs | 9 +-- dhall/src/semantics/tck/typecheck.rs | 87 +++++++++++----------- dhall/tests/type-errors/hurkensParadox.txt | 5 +- .../unit/FunctionApplicationArgumentNotMatch.txt | 5 +- .../unit/FunctionApplicationIsNotFunction.txt | 5 +- .../type-errors/unit/ListLiteralEmptyNotType.txt | 5 +- .../type-errors/unit/MergeHandlerNotFunction.txt | 4 +- .../unit/MergeHandlerNotMatchAlternativeType.txt | 3 +- .../type-errors/unit/NaturalSubtractNotNatural.txt | 5 +- 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 --> :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 --> :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` --> :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 --> :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 --> :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 --> :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` -- cgit v1.2.3