From 70eede4fd012f49dfab0e2e27fb3a4e4bbff6325 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 1 Feb 2020 22:04:34 +0000 Subject: Implement once nice error using annotate_snippets --- dhall/src/semantics/nze/value.rs | 4 +++ dhall/src/semantics/tck/typecheck.rs | 54 +++++++++++++++++++++--------------- 2 files changed, 36 insertions(+), 22 deletions(-) (limited to 'dhall/src/semantics') 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)) } }; -- 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/semantics/nze/value.rs | 3 - dhall/src/semantics/tck/env.rs | 6 +- dhall/src/semantics/tck/typecheck.rs | 204 +++++++++++++++++++---------------- 3 files changed, 113 insertions(+), 100 deletions(-) (limited to 'dhall/src/semantics') 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)) } -- 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/semantics/nze/value.rs | 3 ++ dhall/src/semantics/tck/typecheck.rs | 84 +++++++++++++++++++++++++++++++++--- 2 files changed, 82 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics') 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(), -- 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 --- dhall/src/semantics/tck/typecheck.rs | 87 ++++++++++++++++++------------------ 1 file changed, 44 insertions(+), 43 deletions(-) (limited to 'dhall/src/semantics') 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 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/semantics/nze/value.rs | 6 +++--- dhall/src/semantics/tck/tyexpr.rs | 4 ++-- dhall/src/semantics/tck/typecheck.rs | 16 ++++++++-------- 3 files changed, 13 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics') 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(), ) } -- 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/semantics/tck/typecheck.rs | 87 ++++++++++++++++++------------------ 1 file changed, 43 insertions(+), 44 deletions(-) (limited to 'dhall/src/semantics') 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) ), -- cgit v1.2.3