From 6243a302d22c4723e945289c50ed74a80e41ffd3 Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Fri, 20 Nov 2020 15:36:17 +0100 Subject: [PATCH] Handle dynamic row tails in the typechecker --- src/error.rs | 33 ++++++++++++++++++++++++++++++ src/typecheck.rs | 52 ++++++++++++++++++++++++++++++++++++++++++------ src/types.rs | 3 ++- 3 files changed, 81 insertions(+), 7 deletions(-) diff --git a/src/error.rs b/src/error.rs index 34e8a876..b02cdb89 100644 --- a/src/error.rs +++ b/src/error.rs @@ -87,6 +87,12 @@ pub enum TypecheckError { /* the inferred/annotated type */ Types, Option, ), + /// A dynamic tail was expected to be in the type of an expression, but was not. + MissingDynTail( + /* the expected type */ Types, + /* the inferred/annotated type */ Types, + Option, + ), /// A specific row was not expected to be in the type of an expression. ExtraRow( Ident, @@ -94,6 +100,13 @@ pub enum TypecheckError { /* the inferred/annotated type */ Types, Option, ), + /// A additional dynamic tail was not expected to be in the type of an expression. + ExtraDynTail( + /* the expected type */ Types, + /* the inferred/annotated type */ Types, + Option, + ), + /// An unbound type variable was referenced. UnboundTypeVariable(Ident, Option), /// The actual (inferred or annotated) type of an expression is incompatible with its expected @@ -956,6 +969,16 @@ impl ToDiagnostic for TypecheckError { format!("The type of the expression was inferred to be `{}`, which does not contain the field `{}`", actual, ident), ])] , + TypecheckError::MissingDynTail(expd, actual, span_opt) => + vec![Diagnostic::error() + .with_message(String::from("Type error: missing dynamic tail `| Dyn`")) + .with_labels(mk_expr_label(span_opt)) + .with_notes(vec![ + format!("The type of the expression was expected to be `{}` which contains the tail `| Dyn`", expd), + format!("The type of the expression was inferred to be `{}`, which does not contain the tail `| Dyn`", actual), + ])] + , + TypecheckError::ExtraRow(Ident(ident), expd, actual, span_opt) => vec![Diagnostic::error() .with_message(format!("Type error: extra row `{}`", ident)) @@ -965,6 +988,16 @@ impl ToDiagnostic for TypecheckError { format!("Tye type of the expression was inferred to be `{}`, which contains the extra field `{}`", actual, ident), ])] , + TypecheckError::ExtraDynTail(expd, actual, span_opt) => + vec![Diagnostic::error() + .with_message(String::from("Type error: extra dynamic tail `| Dyn`")) + .with_labels(mk_expr_label(span_opt)) + .with_notes(vec![ + format!("The type of the expression was expected to be `{}`, which does not contain the tail `| Dyn`", expd), + format!("Tye type of the expression was inferred to be `{}`, which contains the extra tail `| Dyn`", actual), + ])] + , + TypecheckError::UnboundTypeVariable(Ident(ident), span_opt) => vec![Diagnostic::error() .with_message(String::from("Unbound type variable")) diff --git a/src/typecheck.rs b/src/typecheck.rs index b0a63a2e..44b7e219 100644 --- a/src/typecheck.rs +++ b/src/typecheck.rs @@ -55,17 +55,21 @@ use std::collections::{HashMap, HashSet}; pub enum RowUnifError { /// The LHS had a binding that was missing in the RHS. MissingRow(Ident), + /// The LHS had a `Dyn` tail that was missing in the RHS. + MissingDynTail(), /// The RHS had a binding that was not in the LHS. ExtraRow(Ident), + /// The RHS had a additional `Dyn` tail. + ExtraDynTail(), /// There were two incompatible definitions for the same row. RowMismatch(Ident, UnifError), /// Tried to unify an enum row and a record row. RowKindMismatch(Ident, Option, Option), - /// One of the row was ill-formed (typically, a tail was neither a row nor a variable). + /// One of the row was ill-formed (typically, a tail was neither a row, a variable nor `Dyn`). /// /// This should probably not happen with proper restrictions on the parser and a correct - /// typechecking algorithm. We let it as an error for now, but it could be removed and turned - /// into a panic! in the future. + /// typechecking algorithm. We let it as an error for now, but it could be removed in the + /// future. IllformedRow(TypeWrapper), /// A [row constraint](./type.RowConstr.html) was violated. UnsatConstr(Ident, Option), @@ -88,7 +92,9 @@ impl RowUnifError { pub fn to_unif_err(self, left: TypeWrapper, right: TypeWrapper) -> UnifError { match self { RowUnifError::MissingRow(id) => UnifError::MissingRow(id, left, right), + RowUnifError::MissingDynTail() => UnifError::MissingDynTail(left, right), RowUnifError::ExtraRow(id) => UnifError::ExtraRow(id, left, right), + RowUnifError::ExtraDynTail() => UnifError::ExtraDynTail(left, right), RowUnifError::RowKindMismatch(id, tyw1, tyw2) => { UnifError::RowKindMismatch(id, tyw1, tyw2) } @@ -116,8 +122,12 @@ pub enum UnifError { ConstMismatch(usize, usize), /// Tried to unify two rows, but an identifier of the LHS was absent from the RHS. MissingRow(Ident, TypeWrapper, TypeWrapper), + /// Tried to unify two rows, but the `Dyn` tail of the RHS was absent from the LHS. + MissingDynTail(TypeWrapper, TypeWrapper), /// Tried to unify two rows, but an identifier of the RHS was absent from the LHS. ExtraRow(Ident, TypeWrapper, TypeWrapper), + /// Tried to unify two rows, but the `Dyn` tail of the RHS was absent from the LHS. + ExtraDynTail(TypeWrapper, TypeWrapper), /// A row was ill-formed. IllformedRow(TypeWrapper), /// Tried to unify a unification variable with a row type violating the [row @@ -216,12 +226,23 @@ impl UnifError { reporting::to_type(state, names, tyw2), pos_opt, ), + UnifError::MissingDynTail(tyw1, tyw2) => TypecheckError::MissingDynTail( + reporting::to_type(state, names, tyw1), + reporting::to_type(state, names, tyw2), + pos_opt, + ), + UnifError::ExtraRow(id, tyw1, tyw2) => TypecheckError::ExtraRow( id, reporting::to_type(state, names, tyw1), reporting::to_type(state, names, tyw2), pos_opt, ), + UnifError::ExtraDynTail(tyw1, tyw2) => TypecheckError::ExtraDynTail( + reporting::to_type(state, names, tyw1), + reporting::to_type(state, names, tyw2), + pos_opt, + ), UnifError::IllformedRow(tyw) => { TypecheckError::IllformedType(reporting::to_type(state, names, tyw)) } @@ -545,7 +566,7 @@ fn type_check_( }; if let TypeWrapper::Concrete(AbsType::DynRecord(rec_ty)) = root_ty.clone() { - // Checking for an dynamic record + // Checking for a dynamic record stat_map .into_iter() .try_for_each(|(_, t)| -> Result<(), TypecheckError> { @@ -850,7 +871,9 @@ fn row_add( r = get_root(state.table, p); } match r { - TypeWrapper::Concrete(AbsType::RowEmpty()) => Err(RowUnifError::MissingRow(id.clone())), + TypeWrapper::Concrete(AbsType::RowEmpty()) | TypeWrapper::Concrete(AbsType::Dyn()) => { + Err(RowUnifError::MissingRow(id.clone())) + } TypeWrapper::Concrete(AbsType::RowExtend(id2, ty2, r2)) => { if *id == id2 { Ok((ty2, *r2)) @@ -1035,8 +1058,12 @@ pub fn unify_rows( t2: AbsType>, ) -> Result<(), RowUnifError> { match (t1, t2) { - (AbsType::RowEmpty(), AbsType::RowEmpty()) => Ok(()), + (AbsType::RowEmpty(), AbsType::RowEmpty()) | (AbsType::Dyn(), AbsType::Dyn()) => Ok(()), + (AbsType::RowEmpty(), AbsType::Dyn()) => Err(RowUnifError::ExtraDynTail()), + (AbsType::Dyn(), AbsType::RowEmpty()) => Err(RowUnifError::MissingDynTail()), (AbsType::RowEmpty(), AbsType::RowExtend(ident, _, _)) + | (AbsType::Dyn(), AbsType::RowExtend(ident, _, _)) + | (AbsType::RowExtend(ident, _, _), AbsType::Dyn()) | (AbsType::RowExtend(ident, _, _), AbsType::RowEmpty()) => { Err(RowUnifError::ExtraRow(ident)) } @@ -2189,4 +2216,17 @@ mod tests { ); assert_row_conflict(res); } + + #[test] + fn dynamic_row_tail() { + parse_and_typecheck("let r = Assume({a: Num | Dyn}, {a = 1; b = 2}) in Promise(Num, r.a)") + .unwrap(); + parse_and_typecheck("Promise({a: Num | Dyn}, Assume({a: Num | Dyn}, {a = 1; b = 2}))") + .unwrap(); + // Currently, typechecking is conservative wrt the dynamic row type, meaning it can + parse_and_typecheck("Promise({a: Num | Dyn}, {a = 1; b = 2})").unwrap_err(); + parse_and_typecheck("Promise({a: Num | Dyn}, {a = 1})").unwrap_err(); + parse_and_typecheck("Promise({a: Num}, Assume({a: Num | Dyn}, {a = 1}))").unwrap_err(); + parse_and_typecheck("Promise({a: Num | Dyn}, {a = 1})").unwrap_err(); + } } diff --git a/src/types.rs b/src/types.rs index 583bed07..6a8e4e3e 100644 --- a/src/types.rs +++ b/src/types.rs @@ -137,7 +137,7 @@ impl AbsType { /// Determine if a type is a row type. pub fn is_row_type(&self) -> bool { match self { - AbsType::RowExtend(_, _, _) | AbsType::RowEmpty() => true, + AbsType::RowExtend(_, _, _) | AbsType::RowEmpty() | AbsType::Dyn() => true, _ => false, } } @@ -351,6 +351,7 @@ impl fmt::Display for Types { match tail.0 { AbsType::RowEmpty() => write!(f, "{}", tail), AbsType::Var(_) => write!(f, " | {}", tail), + AbsType::Dyn() => write!(f, " | Dyn"), _ => write!(f, ", {}", tail), } }