diff options
author | Nadrieril | 2020-02-01 22:04:34 +0000 |
---|---|---|
committer | Nadrieril | 2020-02-01 22:04:34 +0000 |
commit | 70eede4fd012f49dfab0e2e27fb3a4e4bbff6325 (patch) | |
tree | f9b4a75b5ffc878f6d5e5a40bd7c13c8de94a9f9 /dhall/src/semantics/tck | |
parent | 72a6fef65bb3d34be1f501a1f6de66fb8a54fa04 (diff) |
Implement once nice error using annotate_snippets
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 54 |
1 files changed, 32 insertions, 22 deletions
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)) } }; |