From 8c64ae33149db4edaaa89d2d187baf10a2b9f8bf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 13:29:27 +0000 Subject: Make most type errors stringy --- dhall/src/error/mod.rs | 95 +++++++++++---------- dhall/src/semantics/phase/typecheck.rs | 151 ++++++++++++--------------------- 2 files changed, 101 insertions(+), 145 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 850a792..5330c59 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -3,7 +3,7 @@ use std::io::Error as IOError; use crate::semantics::core::value::Value; use crate::semantics::phase::resolve::ImportStack; use crate::semantics::phase::NormalizedExpr; -use crate::syntax::{BinOp, Import, Label, ParseError, Span}; +use crate::syntax::{Import, Label, ParseError, Span}; pub type Result = std::result::Result; @@ -48,41 +48,41 @@ pub(crate) enum TypeMessage { UnboundVariable(Span), InvalidInputType(Value), InvalidOutputType(Value), - NotAFunction(Value), - TypeMismatch(Value, Value, Value), - AnnotMismatch(Value, Value), - InvalidListElement(usize, Value, Value), - InvalidListType(Value), - InvalidOptionalType(Value), - InvalidPredicate(Value), - IfBranchMismatch(Value, Value), - IfBranchMustBeTerm(bool, Value), + // NotAFunction(Value), + // TypeMismatch(Value, Value, Value), + // AnnotMismatch(Value, Value), + // InvalidListElement(usize, Value, Value), + // InvalidListType(Value), + // InvalidOptionalType(Value), + // InvalidPredicate(Value), + // IfBranchMismatch(Value, Value), + // IfBranchMustBeTerm(bool, Value), InvalidFieldType(Label, Value), - NotARecord(Label, Value), - MustCombineRecord(Value), - MissingRecordField(Label, Value), - MissingUnionField(Label, Value), - BinOpTypeMismatch(BinOp, Value), - InvalidTextInterpolation(Value), - Merge1ArgMustBeRecord(Value), - Merge2ArgMustBeUnionOrOptional(Value), - MergeEmptyNeedsAnnotation, - MergeHandlerMissingVariant(Label), - MergeVariantMissingHandler(Label), - MergeAnnotMismatch, - MergeHandlerTypeMismatch, - MergeHandlerReturnTypeMustNotBeDependent, - ProjectionMustBeRecord, - ProjectionMissingEntry, - ProjectionDuplicateField, + // NotARecord(Label, Value), + // MustCombineRecord(Value), + // MissingRecordField(Label, Value), + // MissingUnionField(Label, Value), + // BinOpTypeMismatch(BinOp, Value), + // InvalidTextInterpolation(Value), + // Merge1ArgMustBeRecord(Value), + // Merge2ArgMustBeUnionOrOptional(Value), + // MergeEmptyNeedsAnnotation, + // MergeHandlerMissingVariant(Label), + // MergeVariantMissingHandler(Label), + // MergeAnnotMismatch, + // MergeHandlerTypeMismatch, + // MergeHandlerReturnTypeMustNotBeDependent, + // ProjectionMustBeRecord, + // ProjectionMissingEntry, + // ProjectionDuplicateField, Sort, RecordTypeDuplicateField, - RecordTypeMergeRequiresRecordType(Value), + // RecordTypeMergeRequiresRecordType(Value), UnionTypeDuplicateField, - EquivalenceArgumentMustBeTerm(bool, Value), - EquivalenceTypeMismatch(Value, Value), - AssertMismatch(Value, Value), - AssertMustTakeEquivalence, + // EquivalenceArgumentMustBeTerm(bool, Value), + // EquivalenceTypeMismatch(Value, Value), + // AssertMismatch(Value, Value), + // AssertMustTakeEquivalence, Custom(String), } @@ -103,21 +103,22 @@ impl std::fmt::Display for TypeError { 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() - .error("Type error: Wrong type of function argument") - + "\n" - + &z.span().error(format!( - "This argument has type {:?}", - z.get_type().unwrap() - )) - + "\n" - + &y.span().error(format!( - "But the function expected an argument of type {:?}", - y - )) - } + // NotAFunction(v) => v.span().error("Type error: Not a function"), + // TypeMismatch(x, y, z) => { + // x.span() + // .error("Type error: Wrong type of function argument") + // + "\n" + // + &z.span().error(format!( + // "This argument has type {:?}", + // z.get_type().unwrap() + // )) + // + "\n" + // + &y.span().error(format!( + // "But the function expected an argument of type {:?}", + // y + // )) + // } + Custom(s) => format!("Type error: Unhandled error: {}", s), _ => format!("Type error: Unhandled error: {:?}", self.message), }; write!(f, "{}", msg) diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 0f3754e..44678cd 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -357,8 +357,8 @@ fn type_last_layer( use syntax::Builtin::*; use syntax::Const::Type; use syntax::ExprKind::*; - use TypeMessage::*; - let mkerr = |msg: TypeMessage| Err(TypeError::new(msg)); + let mkerr = + |msg: &str| Err(TypeError::new(TypeMessage::Custom(msg.to_string()))); /// Intermediary return type enum Ret { @@ -381,10 +381,10 @@ fn type_last_layer( let tf_borrow = tf.as_whnf(); let (tx, tb) = match &*tf_borrow { ValueKind::Pi(_, tx, tb) => (tx, tb), - _ => return mkerr(NotAFunction(f.clone())), + _ => return mkerr("NotAFunction"), }; if &a.get_type()? != tx { - return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); + return mkerr("TypeMismatch"); } let ret = tb.subst_shift(&AlphaVar::default(), a); @@ -393,35 +393,33 @@ fn type_last_layer( } Annot(x, t) => { if &x.get_type()? != t { - return mkerr(AnnotMismatch(x.clone(), t.clone())); + return mkerr("AnnotMismatch"); } RetWhole(x.clone()) } Assert(t) => { match &*t.as_whnf() { ValueKind::Equivalence(x, y) if x == y => {} - ValueKind::Equivalence(x, y) => { - return mkerr(AssertMismatch(x.clone(), y.clone())) - } - _ => return mkerr(AssertMustTakeEquivalence), + ValueKind::Equivalence(..) => return mkerr("AssertMismatch"), + _ => return mkerr("AssertMustTakeEquivalence"), } RetTypeOnly(t.clone()) } BoolIf(x, y, z) => { if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) { - return mkerr(InvalidPredicate(x.clone())); + return mkerr("InvalidPredicate"); } if y.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(IfBranchMustBeTerm(true, y.clone())); + return mkerr("IfBranchMustBeTerm"); } if z.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(IfBranchMustBeTerm(false, z.clone())); + return mkerr("IfBranchMustBeTerm"); } if y.get_type()? != z.get_type()? { - return mkerr(IfBranchMismatch(y.clone(), z.clone())); + return mkerr("IfBranchMismatch"); } RetTypeOnly(y.get_type()?) @@ -433,7 +431,7 @@ fn type_last_layer( { args[0].clone() } - _ => return mkerr(InvalidListType(t.clone())), + _ => return mkerr("InvalidListType"), }; RetWhole(Value::from_kind_and_type( ValueKind::EmptyListLit(arg), @@ -443,18 +441,14 @@ fn type_last_layer( NEListLit(xs) => { let mut iter = xs.iter().enumerate(); let (_, x) = iter.next().unwrap(); - for (i, y) in iter { + for (_, y) in iter { if x.get_type()? != y.get_type()? { - return mkerr(InvalidListElement( - i, - x.get_type()?, - y.clone(), - )); + return mkerr("InvalidListElement"); } } let t = x.get_type()?; if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidListType(t)); + return mkerr("InvalidListType"); } RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t)) @@ -462,7 +456,7 @@ fn type_last_layer( SomeLit(x) => { let t = x.get_type()?; if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidOptionalType(t)); + return mkerr("InvalidOptionalType"); } RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t)) @@ -479,48 +473,25 @@ fn type_last_layer( Field(r, x) => { match &*r.get_type()?.as_whnf() { ValueKind::RecordType(kts) => match kts.get(&x) { - Some(tth) => { - RetTypeOnly(tth.clone()) - }, - None => return mkerr(MissingRecordField(x.clone(), - r.clone())), + Some(tth) => RetTypeOnly(tth.clone()), + None => return mkerr("MissingRecordField"), }, // TODO: branch here only when r.get_type() is a Const _ => { match &*r.as_whnf() { ValueKind::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > - Some(Some(t)) => { - RetTypeOnly( - tck_pi_type( - ctx.new_binder(x), - t.clone(), - r.under_binder(), - )? - ) - }, - Some(None) => { - RetTypeOnly(r.clone()) - }, - None => { - return mkerr(MissingUnionField( - x.clone(), - r.clone(), - )) - }, - }, - _ => { - return mkerr(NotARecord( - x.clone(), - r.clone() - )) + Some(Some(t)) => RetTypeOnly(tck_pi_type( + ctx.new_binder(x), + t.clone(), + r.under_binder(), + )?), + Some(None) => RetTypeOnly(r.clone()), + None => return mkerr("MissingUnionField"), }, + _ => return mkerr("NotARecord"), } - } - // _ => mkerr(NotARecord( - // x, - // r?, - // )), + } // _ => mkerr("NotARecord"), } } Const(c) => RetWhole(const_to_value(*c)), @@ -535,7 +506,7 @@ fn type_last_layer( use InterpolatedTextContents::Expr; if let Expr(x) = contents { if x.get_type()? != text_type { - return mkerr(InvalidTextInterpolation(x.clone())); + return mkerr("InvalidTextInterpolation"); } } } @@ -549,14 +520,14 @@ fn type_last_layer( let l_type_borrow = l_type.as_whnf(); let kts_x = match &*l_type_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(MustCombineRecord(l.clone())), + _ => return mkerr("MustCombineRecord"), }; // Extract the RHS record type let r_type_borrow = r_type.as_whnf(); let kts_y = match &*r_type_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(MustCombineRecord(r.clone())), + _ => return mkerr("MustCombineRecord"), }; // Union the two records, prefering @@ -584,18 +555,14 @@ fn type_last_layer( let borrow_l = l.as_whnf(); let kts_x = match &*borrow_l { ValueKind::RecordType(kts) => kts, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) - } + _ => return mkerr("RecordTypeMergeRequiresRecordType"), }; // Extract the RHS record type let borrow_r = r.as_whnf(); let kts_y = match &*borrow_r { ValueKind::RecordType(kts) => kts, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) - } + _ => return mkerr("RecordTypeMergeRequiresRecordType"), }; // Ensure that the records combine without a type error @@ -618,28 +585,28 @@ fn type_last_layer( RetWhole(tck_record_type(kts.into_iter().map(Ok))?) } - BinOp(o @ ListAppend, l, r) => { + BinOp(ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { ValueKind::AppliedBuiltin(List, _, _) => {} - _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), + _ => return mkerr("BinOpTypeMismatch"), } if l.get_type()? != r.get_type()? { - return mkerr(BinOpTypeMismatch(*o, r.clone())); + return mkerr("BinOpTypeMismatch"); } RetTypeOnly(l.get_type()?) } BinOp(Equivalence, l, r) => { if l.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone())); + return mkerr("EquivalenceArgumentMustBeTerm"); } if r.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone())); + return mkerr("EquivalenceArgumentMustBeTerm"); } if l.get_type()? != r.get_type()? { - return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); + return mkerr("EquivalenceTypeMismatch"); } RetWhole(Value::from_kind_and_type( @@ -665,11 +632,11 @@ fn type_last_layer( }); if l.get_type()? != t { - return mkerr(BinOpTypeMismatch(*o, l.clone())); + return mkerr("BinOpTypeMismatch"); } if r.get_type()? != t { - return mkerr(BinOpTypeMismatch(*o, r.clone())); + return mkerr("BinOpTypeMismatch"); } RetTypeOnly(t) @@ -679,7 +646,7 @@ fn type_last_layer( let record_borrow = record_type.as_whnf(); let handlers = match &*record_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(Merge1ArgMustBeRecord(record.clone())), + _ => return mkerr("Merge1ArgMustBeRecord"), }; let union_type = union.get_type()?; @@ -697,9 +664,7 @@ fn type_last_layer( kts.insert("Some".into(), Some(ty.clone())); Cow::Owned(kts) } - _ => { - return mkerr(Merge2ArgMustBeUnionOrOptional(union.clone())) - } + _ => return mkerr("Merge2ArgMustBeUnionOrOptional"), }; let mut inferred_type = None; @@ -711,19 +676,11 @@ fn type_last_layer( let handler_type_borrow = handler_type.as_whnf(); let (tx, tb) = match &*handler_type_borrow { ValueKind::Pi(_, tx, tb) => (tx, tb), - _ => { - return mkerr(NotAFunction( - handler_type.clone(), - )) - } + _ => return mkerr("NotAFunction"), }; if variant_type != tx { - return mkerr(TypeMismatch( - handler_type.clone(), - tx.clone(), - variant_type.clone(), - )); + return mkerr("TypeMismatch"); } // Extract `tb` from under the binder. Fails if the variable was used @@ -731,41 +688,39 @@ fn type_last_layer( match tb.over_binder() { Some(x) => x, None => return mkerr( - MergeHandlerReturnTypeMustNotBeDependent, + "MergeHandlerReturnTypeMustNotBeDependent", ), } } // Union alternative without type Some(None) => handler_type.clone(), - None => { - return mkerr(MergeHandlerMissingVariant(x.clone())) - } + None => return mkerr("MergeHandlerMissingVariant"), }; match &inferred_type { None => inferred_type = Some(handler_return_type), Some(t) => { if t != &handler_return_type { - return mkerr(MergeHandlerTypeMismatch); + return mkerr("MergeHandlerTypeMismatch"); } } } } for x in variants.keys() { if !handlers.contains_key(x) { - return mkerr(MergeVariantMissingHandler(x.clone())); + return mkerr("MergeVariantMissingHandler"); } } match (inferred_type, type_annot.as_ref()) { (Some(t1), Some(t2)) => { if &t1 != t2 { - return mkerr(MergeAnnotMismatch); + return mkerr("MergeAnnotMismatch"); } RetTypeOnly(t1) } (Some(t), None) => RetTypeOnly(t), (None, Some(t)) => RetTypeOnly(t.clone()), - (None, None) => return mkerr(MergeEmptyNeedsAnnotation), + (None, None) => return mkerr("MergeEmptyNeedsAnnotation"), } } ToMap(_, _) => unimplemented!("toMap"), @@ -774,18 +729,18 @@ fn type_last_layer( let record_type_borrow = record_type.as_whnf(); let kts = match &*record_type_borrow { ValueKind::RecordType(kts) => kts, - _ => return mkerr(ProjectionMustBeRecord), + _ => return mkerr("ProjectionMustBeRecord"), }; let mut new_kts = HashMap::new(); for l in labels { match kts.get(l) { - None => return mkerr(ProjectionMissingEntry), + None => return mkerr("ProjectionMissingEntry"), Some(t) => { use std::collections::hash_map::Entry; match new_kts.entry(l.clone()) { Entry::Occupied(_) => { - return mkerr(ProjectionDuplicateField) + return mkerr("ProjectionDuplicateField") } Entry::Vacant(e) => e.insert(t.clone()), } -- cgit v1.2.3