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/tck/typecheck.rs | 54 +++++++++++++++++++++---------------
1 file changed, 32 insertions(+), 22 deletions(-)
(limited to 'dhall/src/semantics/tck')
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<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!(
@@ -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/tck/env.rs | 6 +-
dhall/src/semantics/tck/typecheck.rs | 204 +++++++++++++++++++----------------
2 files changed, 113 insertions(+), 97 deletions(-)
(limited to 'dhall/src/semantics/tck')
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 812ca7a..1fc711c 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, TyExprKind, Type, Value};
+use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, Value};
use crate::syntax::{Label, V};
/// Environment for indexing variables.
@@ -116,9 +116,9 @@ impl TyEnv {
items: self.items.insert_value(e),
}
}
- pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> {
+ pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
let var = self.names.unlabel_var(var)?;
let ty = self.items.lookup_ty(&var);
- Some((TyExprKind::Var(var), ty))
+ Some((var, ty))
}
}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a652663..e642b8f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -35,19 +35,6 @@ fn function_check(a: Const, b: Const) -> Const {
}
}
-fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> {
- let ks = match src.as_const() {
- Some(k) => k,
- _ => return Err(TypeError::new(TypeMessage::InvalidInputType(src))),
- };
- let kt = match tgt.as_const() {
- Some(k) => k,
- _ => return Err(TypeError::new(TypeMessage::InvalidOutputType(tgt))),
- };
-
- Ok(Value::from_const(function_check(ks, kt)))
-}
-
fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
Err(TypeError::new(TypeMessage::Custom(x.to_string())))
}
@@ -64,12 +51,55 @@ fn type_one_layer(
"There should remain no imports in a resolved expression"
),
ExprKind::Var(..)
- | ExprKind::Lam(..)
- | ExprKind::Pi(..)
- | ExprKind::Let(..)
| ExprKind::Const(Const::Sort)
| ExprKind::Embed(..) => unreachable!(), // Handled in type_with
+ ExprKind::Lam(binder, annot, body) => {
+ let body_ty = body.get_type()?;
+ let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
+ let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
+ let pi_ty = type_one_layer(env, &pi_ekind, Span::Artificial)?;
+ let ty = TyExpr::new(
+ TyExprKind::Expr(pi_ekind),
+ Some(pi_ty),
+ Span::Artificial,
+ );
+ ty.eval(env.as_nzenv())
+ }
+ ExprKind::Pi(_, annot, body) => {
+ let ks = match annot.get_type()?.as_const() {
+ Some(k) => k,
+ _ => {
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "Invalid input type: `{}`",
+ annot.get_type()?.to_expr_tyenv(env),
+ ))
+ .span_err(
+ &annot.span(),
+ format!(
+ "this has type: `{}`",
+ annot.get_type()?.to_expr_tyenv(env)
+ ),
+ )
+ .help(
+ format!(
+ "The input type of a function must have type `Type`, `Kind` or `Sort`",
+ ),
+ )
+ .format(),
+ );
+ }
+ };
+ let kt = match body.get_type()?.as_const() {
+ Some(k) => k,
+ _ => return mkerr("Invalid output type"),
+ };
+
+ Value::from_const(function_check(ks, kt))
+ }
+ ExprKind::Let(_, _, _, body) => body.get_type()?,
+
ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
ExprKind::Builtin(b) => {
@@ -202,10 +232,12 @@ fn type_one_layer(
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => {
- let pi_ty = type_of_function(
- ty.get_type()?,
- scrut.get_type()?,
- )?;
+ // Can't fail because uniontypes must have type Const(_).
+ let kt = scrut.get_type()?.as_const().unwrap();
+ // The type of the field must be Const smaller than `kt`, thus the
+ // function type has type `kt`.
+ let pi_ty = Value::from_const(kt);
+
Value::from_kind_and_type(
ValueKind::PiClosure {
binder: Binder::new(x.clone()),
@@ -256,25 +288,27 @@ fn type_one_layer(
ExprKind::App(f, arg) => match f.get_type()?.kind() {
ValueKind::PiClosure { annot, closure, .. } => {
if arg.get_type()? != *annot {
- let mut builder = ErrorBuilder::span_err(
- &span,
- format!("function annot mismatch",),
- );
- builder.annotate_info(
- &f.span(),
- format!(
- "this expects an argument of type: {}",
- annot.to_expr_tyenv(env),
- ),
+ return mkerr(
+ ErrorBuilder::new_span_err(
+ &span,
+ format!("Wrong type of function argument"),
+ )
+ .span_help(
+ &f.span(),
+ format!(
+ "this expects an argument of type: {}",
+ annot.to_expr_tyenv(env),
+ ),
+ )
+ .span_help(
+ &arg.span(),
+ format!(
+ "but this has type: {}",
+ arg.get_type()?.to_expr_tyenv(env),
+ ),
+ )
+ .format(),
);
- builder.annotate_info(
- &arg.span(),
- format!(
- "but this has type: {}",
- arg.get_type()?.to_expr_tyenv(env),
- ),
- );
- return mkerr(builder.format());
}
let arg_nf = arg.eval(env.as_nzenv());
@@ -534,62 +568,15 @@ pub(crate) fn type_with(
) -> Result<TyExpr, TypeError> {
let (tyekind, ty) = match expr.as_ref() {
ExprKind::Var(var) => match env.lookup(&var) {
- Some((k, ty)) => (k, Some(ty)),
- None => return mkerr("unbound variable"),
+ Some((v, ty)) => (TyExprKind::Var(v), Some(ty)),
+ None => {
+ return mkerr(
+ ErrorBuilder::new(format!("unbound variable `{}`", var))
+ .span_err(&expr.span(), "not found in this scope")
+ .format(),
+ )
+ }
},
- ExprKind::Lam(binder, annot, body) => {
- let annot = type_with(env, annot)?;
- let annot_nf = annot.eval(env.as_nzenv());
- let body_env = env.insert_type(&binder, annot_nf.clone());
- let body = type_with(&body_env, body)?;
- let body_ty = body.get_type()?;
- let ty = TyExpr::new(
- TyExprKind::Expr(ExprKind::Pi(
- binder.clone(),
- annot.clone(),
- body_ty.to_tyexpr(body_env.as_varenv()),
- )),
- Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
- Span::Artificial,
- );
- let ty = ty.eval(env.as_nzenv());
- (
- TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
- Some(ty),
- )
- }
- ExprKind::Pi(binder, annot, body) => {
- let annot = type_with(env, annot)?;
- let annot_nf = annot.eval(env.as_nzenv());
- let body =
- type_with(&env.insert_type(binder, annot_nf.clone()), body)?;
- let ty = type_of_function(annot.get_type()?, body.get_type()?)?;
- (
- TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)),
- Some(ty),
- )
- }
- ExprKind::Let(binder, annot, val, body) => {
- let val = if let Some(t) = annot {
- t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
- } else {
- val.clone()
- };
-
- let val = type_with(env, &val)?;
- let val_nf = val.eval(&env.as_nzenv());
- let body = type_with(&env.insert_value(&binder, val_nf), body)?;
- let body_ty = body.get_type().ok();
- (
- TyExprKind::Expr(ExprKind::Let(
- binder.clone(),
- None,
- val,
- body,
- )),
- body_ty,
- )
- }
ExprKind::Const(Const::Sort) => {
(TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
}
@@ -597,7 +584,36 @@ pub(crate) fn type_with(
return Ok(p.clone().into_value().to_tyexpr_noenv())
}
ekind => {
- let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
+ let ekind = match ekind {
+ ExprKind::Lam(binder, annot, body) => {
+ let annot = type_with(env, annot)?;
+ let annot_nf = annot.eval(env.as_nzenv());
+ let body_env = env.insert_type(binder, annot_nf);
+ let body = type_with(&body_env, body)?;
+ ExprKind::Lam(binder.clone(), annot, body)
+ }
+ ExprKind::Pi(binder, annot, body) => {
+ let annot = type_with(env, annot)?;
+ let annot_nf = annot.eval(env.as_nzenv());
+ let body_env = env.insert_type(binder, annot_nf);
+ let body = type_with(&body_env, body)?;
+ ExprKind::Pi(binder.clone(), annot, body)
+ }
+ ExprKind::Let(binder, annot, val, body) => {
+ let val = if let Some(t) = annot {
+ t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
+ } else {
+ val.clone()
+ };
+ let val = type_with(env, &val)?;
+ let val_nf = val.eval(&env.as_nzenv());
+ let body_env = env.insert_value(&binder, val_nf);
+ let body = type_with(&body_env, body)?;
+ ExprKind::Let(binder.clone(), None, val, body)
+ }
+ _ => ekind.traverse_ref(|e| type_with(env, e))?,
+ };
+
let ty = type_one_layer(env, &ekind, expr.span())?;
(TyExprKind::Expr(ekind), Some(ty))
}
--
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/tck/typecheck.rs | 84 +++++++++++++++++++++++++++++++++---
1 file changed, 79 insertions(+), 5 deletions(-)
(limited to 'dhall/src/semantics/tck')
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/tck')
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/tck/tyexpr.rs | 4 ++--
dhall/src/semantics/tck/typecheck.rs | 16 ++++++++--------
2 files changed, 10 insertions(+), 10 deletions(-)
(limited to 'dhall/src/semantics/tck')
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 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/tck')
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