diff options
Diffstat (limited to '')
22 files changed, 527 insertions, 142 deletions
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..39f8dfb --- /dev/null +++ b/dhall/src/error/builder.rs @@ -0,0 +1,168 @@ +use annotate_snippets::{ + display_list::DisplayList, + formatter::DisplayListFormatter, + snippet::{Annotation, AnnotationType, Slice, Snippet, SourceAnnotation}, +}; + +use crate::syntax::{ParsedSpan, Span}; + +#[derive(Debug, Clone, Default)] +pub struct ErrorBuilder { + title: FreeAnnotation, + annotations: Vec<SpannedAnnotation>, + footer: Vec<FreeAnnotation>, + /// Inducate that the current builder has already been consumed and consuming it again should + /// panic. + consumed: bool, +} + +#[derive(Debug, Clone)] +struct SpannedAnnotation { + span: ParsedSpan, + message: String, + annotation_type: AnnotationType, +} + +#[derive(Debug, Clone)] +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: impl ToString) -> Self { + ErrorBuilder { + title: FreeAnnotation { + message: message.to_string(), + annotation_type: AnnotationType::Error, + }, + annotations: Vec::new(), + footer: Vec::new(), + consumed: false, + } + } + + 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 { + Span::Parsed(span) => span, + _ => return self, + }; + self.annotations.push(SpannedAnnotation { + span, + message: message.to_string(), + annotation_type, + }); + self + } + pub fn footer_annot( + &mut self, + message: impl ToString, + annotation_type: AnnotationType, + ) -> &mut Self { + self.footer.push(FreeAnnotation { + message: message.to_string(), + 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_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 { + 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 slices = if this.annotations.is_empty() { + Vec::new() + } else { + let input = this.annotations[0].span.to_input(); + let annotations = this + .annotations + .into_iter() + .map(|annot| annot.into_annotation()) + .collect(); + vec![Slice { + source: input, + line_start: 1, // TODO + origin: Some("<current file>".to_string()), + fold: true, + annotations, + }] + }; + let footer = this + .footer + .into_iter() + .map(|annot| annot.into_annotation()) + .collect(); + + let snippet = Snippet { + title: Some(this.title.into_annotation()), + slices, + footer, + }; + let dl = DisplayList::from(snippet); + let dlf = DisplayListFormatter::new(true, false); + format!("{}", dlf.format(&dl)) + } +} + +impl Default for FreeAnnotation { + fn default() -> Self { + FreeAnnotation { + message: String::new(), + annotation_type: AnnotationType::Error, + } + } +} diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 4df018d..6ea7d0c 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -1,10 +1,12 @@ use std::io::Error as IOError; use crate::semantics::resolve::ImportStack; -use crate::semantics::Value; use crate::syntax::{Import, ParseError}; use crate::NormalizedExpr; +mod builder; +pub(crate) use builder::*; + pub type Result<T> = std::result::Result<T, Error>; #[derive(Debug)] @@ -46,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), @@ -97,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 ae06942..1143781 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}; @@ -173,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 @@ -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/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/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<Type, TypeError> { match &self.ty { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 20076cd..9a1d0d8 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, @@ -35,19 +35,6 @@ fn function_check(a: Const, b: Const) -> Const { } } -fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> { - let ks = match src.as_const() { - Some(k) => k, - _ => return Err(TypeError::new(TypeMessage::InvalidInputType(src))), - }; - let kt = match tgt.as_const() { - Some(k) => k, - _ => return Err(TypeError::new(TypeMessage::InvalidOutputType(tgt))), - }; - - Ok(Value::from_const(function_check(ks, kt))) -} - fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> { Err(TypeError::new(TypeMessage::Custom(x.to_string()))) } @@ -57,18 +44,61 @@ fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> { fn type_one_layer( env: &TyEnv, kind: &ExprKind<TyExpr, Normalized>, + span: Span, ) -> Result<Type, TypeError> { Ok(match kind { ExprKind::Import(..) => unreachable!( "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) => { @@ -201,10 +231,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,21 +288,47 @@ fn type_one_layer( 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), - )); + 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), + arg.get_type()?.to_expr_tyenv(env), + )) + .format(), + ); } let arg_nf = arg.eval(env.as_nzenv()); closure.apply(arg_nf) } - _ => return mkerr(format!("apply to not Pi")), + _ => return mkerr( + ErrorBuilder::new(format!( + "expected function, found `{}`", + f.get_type()?.to_expr_tyenv(env) + )) + .span_err( + f.span(), + format!("function application requires a function",), + ) + .format(), + ), } } ExprKind::BoolIf(x, y, z) => { @@ -323,7 +381,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 +405,7 @@ fn type_one_layer( tx.to_tyexpr(env.as_varenv()), ty.to_tyexpr(env.as_varenv()), ), + Span::Artificial, )?; } } @@ -439,14 +498,73 @@ 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 for `{}` 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) + ), + ) + .format(), + ); } closure.remove_binder().or_else(|()| { mkerr("MergeReturnTypeIsDependent") })? } - _ => return mkerr("NotAFunction"), + _ => { + return mkerr( + ErrorBuilder::new(format!( + "merge handler is not a function" + )) + .span_err( + span, + format!("in this merge expression"), + ) + .span_err( + record.span(), + format!( + "the handler for `{}` has 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(), @@ -524,62 +642,15 @@ pub(crate) fn type_with( ) -> Result<TyExpr, TypeError> { let (tyekind, ty) = match expr.as_ref() { ExprKind::Var(var) => match env.lookup(&var) { - Some((k, ty)) => (k, Some(ty)), - None => return mkerr("unbound variable"), + Some((v, ty)) => (TyExprKind::Var(v), Some(ty)), + None => { + return mkerr( + ErrorBuilder::new(format!("unbound variable `{}`", var)) + .span_err(expr.span(), "not found in this scope") + .format(), + ) + } }, - ExprKind::Lam(binder, annot, body) => { - let annot = type_with(env, annot)?; - let annot_nf = annot.eval(env.as_nzenv()); - let body_env = env.insert_type(&binder, annot_nf.clone()); - let body = type_with(&body_env, body)?; - let body_ty = body.get_type()?; - let ty = TyExpr::new( - TyExprKind::Expr(ExprKind::Pi( - binder.clone(), - annot.clone(), - body_ty.to_tyexpr(body_env.as_varenv()), - )), - Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?), - Span::Artificial, - ); - let ty = ty.eval(env.as_nzenv()); - ( - TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)), - Some(ty), - ) - } - ExprKind::Pi(binder, annot, body) => { - let annot = type_with(env, annot)?; - let annot_nf = annot.eval(env.as_nzenv()); - let body = - type_with(&env.insert_type(binder, annot_nf.clone()), body)?; - let ty = type_of_function(annot.get_type()?, body.get_type()?)?; - ( - TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)), - Some(ty), - ) - } - ExprKind::Let(binder, annot, val, body) => { - let val = if let Some(t) = annot { - t.rewrap(ExprKind::Annot(val.clone(), t.clone())) - } else { - val.clone() - }; - - let val = type_with(env, &val)?; - let val_nf = val.eval(&env.as_nzenv()); - let body = type_with(&env.insert_value(&binder, val_nf), body)?; - let body_ty = body.get_type().ok(); - ( - TyExprKind::Expr(ExprKind::Let( - binder.clone(), - None, - val, - body, - )), - body_ty, - ) - } ExprKind::Const(Const::Sort) => { (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) } @@ -587,8 +658,37 @@ 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 ty = type_one_layer(env, &ekind)?; + 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/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<E> Expr<E> { span: self.span.clone(), } } + pub fn with_span(self, span: Span) -> Self { + Expr { + kind: self.kind, + span, + } + } pub fn traverse_resolve_mut<Err, F1>( &mut self, diff --git a/dhall/src/syntax/ast/span.rs b/dhall/src/syntax/ast/span.rs index f9c7008..ffdd82c 100644 --- a/dhall/src/syntax/ast/span.rs +++ b/dhall/src/syntax/ast/span.rs @@ -24,6 +24,20 @@ pub enum Span { Artificial, } +impl ParsedSpan { + pub(crate) fn to_input(&self) -> String { + self.input.to_string() + } + /// Convert to a char range for consumption by annotate_snippets. + /// This compensates for https://github.com/rust-lang/annotate-snippets-rs/issues/24 + pub(crate) fn as_char_range(&self) -> (usize, usize) { + ( + char_idx_from_byte_idx(&self.input, self.start), + char_idx_from_byte_idx(&self.input, self.end), + ) + } +} + impl Span { pub(crate) fn make(input: Rc<str>, sp: pest::Span) -> Self { Span::Parsed(ParsedSpan { @@ -79,3 +93,19 @@ impl Span { format!("{}", err) } } + +/// Convert a byte idx into a string into a char idx for consumption by annotate_snippets. +fn char_idx_from_byte_idx(input: &str, idx: usize) -> usize { + let char_idx = input + .char_indices() + .enumerate() + .find(|(_, (i, _))| *i == idx) + .unwrap() + .0; + // Unix-style newlines are counted as two chars (see + // https://github.com/rust-lang/annotate-snippets-rs/issues/24). + let nbr_newlines = input[..idx].chars().filter(|c| *c == '\n').count(); + let nbr_carriage_returns = + input[..idx].chars().filter(|c| *c == '\r').count(); + char_idx + nbr_newlines - nbr_carriage_returns +} diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs index 2ec63e2..8d571c0 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<Normalized>; +type UnspannedExpr = syntax::UnspannedExpr<Normalized>; type ParsedText = InterpolatedText<Expr>; type ParsedTextContents = InterpolatedTextContents<Expr>; type ParseInput<'input> = pest_consume::Node<'input, Rule, Rc<str>>; @@ -78,14 +79,10 @@ 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<Normalized>) -> Expr { +fn spanned(input: ParseInput, x: UnspannedExpr) -> Expr { Expr::new(x, input_to_span(input)) } -fn spanned_union( - span1: Span, - span2: Span, - x: UnspannedExpr<Normalized>, -) -> Expr { +fn spanned_union(span1: Span, span2: Span, x: UnspannedExpr) -> Expr { Expr::new(x, span1.union(&span2)) } @@ -845,25 +842,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<Expr> { - Ok(spanned(input, RecordLit(Default::default()))) + #[alias(record_type_or_literal)] + fn empty_record_literal(input: ParseInput) -> ParseResult<UnspannedExpr> { + Ok(RecordLit(Default::default())) } - #[alias(expression)] - fn empty_record_type(input: ParseInput) -> ParseResult<Expr> { - Ok(spanned(input, RecordType(Default::default()))) + #[alias(record_type_or_literal)] + fn empty_record_type(input: ParseInput) -> ParseResult<UnspannedExpr> { + Ok(RecordType(Default::default())) } - #[alias(expression)] + #[alias(record_type_or_literal)] fn non_empty_record_type_or_literal( input: ParseInput, - ) -> ParseResult<Expr> { - let e = match_nodes!(input.children(); + ) -> ParseResult<UnspannedExpr> { + 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 +873,7 @@ impl DhallParser { map.insert(first_label, first_expr); RecordLit(map) }, - ); - Ok(spanned(input, e)) + )) } fn non_empty_record_type( @@ -910,13 +908,12 @@ impl DhallParser { )) } - #[alias(expression)] - fn union_type(input: ParseInput) -> ParseResult<Expr> { + fn union_type(input: ParseInput) -> ParseResult<UnspannedExpr> { 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/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index 4dfdcf5..522e1a2 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -1 +1,15 @@ -Type error: Unhandled error: function annot mismatch: (U : Sort) : Kind +Type error: Unhandled error: error: wrong type of function argument + --> <current file>:6:23 + | + 1 | let bottom : Type = ∀(any : Type) → any + 2 | + 3 | in let not : Type → Type = λ(p : Type) → p → bottom + 4 | +... +10 | : pow (pow U) → U +11 | = λ(t : pow (pow U)) + | ^^^ 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/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt index 87cf48e..e4584f5 100644 --- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt +++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt @@ -1 +1,6 @@ -Type error: Unhandled error: unbound variable +Type error: Unhandled error: error: unbound variable ``_`` + --> <current file>:1:46 + | +1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _) + | ^ not found in this scope + | diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 8d101c3..01facbc 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -1 +1,9 @@ -Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural +Type error: Unhandled error: error: wrong type of function argument + --> <current file>:1:1 + | +1 | (λ(_ : Natural) → _) True + | ^^^^^^^^^^^^^^^^^^ 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 a72e120..f779fd6 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -1 +1,6 @@ -Type error: Unhandled error: apply to not Pi +Type error: Unhandled error: error: expected function, found `Bool` + --> <current file>:1:0 + | +1 | True True + | ^^^^ function application requires a function + | diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt index a13fb3a..3fc1652 100644 --- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt @@ -1 +1,7 @@ -[unknown location] Type error: Invalid function input +Type error: Unhandled error: error: Invalid input type: `Natural` + --> <current file>:1:6 + | +1 | λ(_ : 1) → _ + | ^ this has type: `Natural` + | + = help: The input type of a function must have type `Type`, `Kind` or `Sort` diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt index a13fb3a..948c6c7 100644 --- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt @@ -1 +1,7 @@ -[unknown location] Type error: Invalid function input +Type error: Unhandled error: error: Invalid input type: `Natural` + --> <current file>:1:0 + | +1 | 2 → _ + | ^ this has type: `Natural` + | + = help: The input type of a function must have type `Type`, `Kind` or `Sort` diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index 070e461..aa7c8c5 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -1 +1,9 @@ -Type error: Unhandled error: function annot mismatch: (Type : Kind) : Type +Type error: Unhandled error: error: wrong type of function argument + --> <current file>:1:5 + | +1 | [] : List Type + | ^^^^ 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 f1cdf92..053a054 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: merge handler is not a function + --> <current file>:1:0 + | +1 | merge { x = True } (< x : Bool >.x True) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression + | ^^^^^^^^^^^^ 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 8b729a4..faca63a 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -1 +1,8 @@ -Type error: Unhandled error: MergeHandlerTypeMismatch +Type error: Unhandled error: error: Wrong handler input type + --> <current file>:1:0 + | +1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression + | ^^^^^^^^^^^^^^^^^^^^^^^ the handler for `x` expects a value of type: `Bool` + | ^^^^^^^^^^^^^^^^^^^ but the corresponding variant has type: `Natural` + | diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index 8d101c3..7e410c4 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -1 +1,9 @@ -Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural +Type error: Unhandled error: error: wrong type of function argument + --> <current file>:1:0 + | +1 | Natural/subtract True True + | ^^^^^^^^^^^^^^^^ 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/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt index 87cf48e..a234f9f 100644 --- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt +++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt @@ -1 +1,6 @@ -Type error: Unhandled error: unbound variable +Type error: Unhandled error: error: unbound variable `constructors` + --> <current file>:1:0 + | +1 | constructors < Left : Natural | Right : Bool > + | ^^^^^^^^^^^^ not found in this scope + | diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt index 87cf48e..52baa7f 100644 --- a/dhall/tests/type-errors/unit/VariableFree.txt +++ b/dhall/tests/type-errors/unit/VariableFree.txt @@ -1 +1,6 @@ -Type error: Unhandled error: unbound variable +Type error: Unhandled error: error: unbound variable `x` + --> <current file>:1:0 + | +1 | x + | ^ not found in this scope + | |