From 459c04245ebebeb095f7c663eb32e7f797633cd3 Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Fri, 1 Sep 2023 12:16:55 +0200 Subject: [PATCH] Fix incomplete check of row constraints In an attempt to free the allocation of the constraints of a record row unification variable that is being assigned to some record rows, the code checking that row constraints are satisfied was removing the constraints from the global state. Since rows are defined as linked list, if the constraint wasn't violated on the first row, this function would recursively call itself. But then the subsequent recursive calls would try to get the constraints from the state again, to only find an empty set constraints, as it has been removed just before. The function thus wouldn't detect constraint violations happening in the tail of the record rows. This patch defines a subfunction which passes the initial constraints along recursive calls, such that they aren't lost during recursion, instead of trying to get them from the state again at each recursive call. --- core/src/typecheck/unif.rs | 37 ++++++++++++------- .../fail/row_conflict_poly_shuffled1.ncl | 20 ++++++++++ .../fail/row_conflict_poly_shuffled2.ncl | 20 ++++++++++ .../fail/row_conflict_poly_shuffled3.ncl | 20 ++++++++++ 4 files changed, 84 insertions(+), 13 deletions(-) create mode 100644 core/tests/integration/typecheck/fail/row_conflict_poly_shuffled1.ncl create mode 100644 core/tests/integration/typecheck/fail/row_conflict_poly_shuffled2.ncl create mode 100644 core/tests/integration/typecheck/fail/row_conflict_poly_shuffled3.ncl diff --git a/core/src/typecheck/unif.rs b/core/src/typecheck/unif.rs index bf20a96d4e..9f8b814e7b 100644 --- a/core/src/typecheck/unif.rs +++ b/core/src/typecheck/unif.rs @@ -913,32 +913,41 @@ pub type RowConstr = HashMap>; pub fn constr_unify_rrows( constr: &mut RowConstr, var_id: VarId, - rrows: &UnifRecordRows, + urrows: &UnifRecordRows, ) -> Result<(), RowUnifError> { - if let Some(p_constr) = constr.remove(&var_id) { + fn do_unify( + constr: &mut RowConstr, + var_id: VarId, + var_constr: HashSet, + rrows: &UnifRecordRows, + ) -> Result<(), RowUnifError> { match rrows { UnifRecordRows::Concrete { rrows: RecordRowsF::Extend { row, .. }, .. - } if p_constr.contains(&row.id.ident()) => Err(RowUnifError::UnsatConstr( + } if var_constr.contains(&row.id.ident()) => Err(RowUnifError::UnsatConstr( row.id, UnifType::concrete(TypeF::Record(rrows.clone())), )), UnifRecordRows::Concrete { rrows: RecordRowsF::Extend { tail, .. }, .. - } => constr_unify_rrows(constr, var_id, tail), + } => do_unify(constr, var_id, var_constr, tail), UnifRecordRows::UnifVar { id, .. } if *id != var_id => { - if let Some(u_constr) = constr.get_mut(id) { - u_constr.extend(p_constr); + if let Some(tail_constr) = constr.get_mut(id) { + tail_constr.extend(var_constr); } else { - constr.insert(*id, p_constr); + constr.insert(*id, var_constr); } Ok(()) } _ => Ok(()), } + } + + if let Some(var_constr) = constr.remove(&var_id) { + do_unify(constr, var_id, var_constr, urrows) } else { Ok(()) } @@ -1386,14 +1395,13 @@ impl RemoveRow for UnifRecordRows { } }, UnifRecordRows::UnifVar { id: var_id, .. } => { - let excluded = state.constr.entry(var_id).or_default(); - - if !excluded.insert(target.ident()) { - return Err(RemoveRRowError::Conflict); - } - let fresh_uvar = state.table.fresh_type_uvar(var_level); let tail_var_id = state.table.fresh_rrows_var_id(var_level); + // We have to manually insert the constraint that `tail_var_id` can't contain a row + // `target`, to avoid producing ill-formed record rows later + state + .constr + .insert(tail_var_id, HashSet::from([target.ident()])); let row_to_insert = UnifRecordRow { id: *target, @@ -1403,11 +1411,14 @@ impl RemoveRow for UnifRecordRows { id: tail_var_id, init_level: var_level, }; + let tail_extended = UnifRecordRows::concrete(RecordRowsF::Extend { row: row_to_insert, tail: Box::new(tail_var.clone()), }); + constr_unify_rrows(state.constr, var_id, &tail_extended) + .map_err(|_| RemoveRRowError::Conflict)?; state.table.assign_rrows(var_id, tail_extended); Ok((fresh_uvar, tail_var)) diff --git a/core/tests/integration/typecheck/fail/row_conflict_poly_shuffled1.ncl b/core/tests/integration/typecheck/fail/row_conflict_poly_shuffled1.ncl new file mode 100644 index 0000000000..c640eb62b2 --- /dev/null +++ b/core/tests/integration/typecheck/fail/row_conflict_poly_shuffled1.ncl @@ -0,0 +1,20 @@ +# test.type = 'error' +# eval = 'typecheck' +# +# [test.metadata] +# error = 'TypecheckError::RowConflict' +# +# [test.metadata.expectation] +# row = 'a' + +# Regression test for issue #1393 (https://github.com/tweag/nickel/issues/1393). +# Ensure that row constraints are properly checked, indepedently of the order of +# row declarations. +let f + | forall r. {; r } -> { a : Number, b : Number; r } + # the implementation doesn't matter, we care about types + = fun r => null + in +let g = fun x => 'a in +g ((f { a = 0, x = 0, y = 0 }) : _) + diff --git a/core/tests/integration/typecheck/fail/row_conflict_poly_shuffled2.ncl b/core/tests/integration/typecheck/fail/row_conflict_poly_shuffled2.ncl new file mode 100644 index 0000000000..c8b2c52766 --- /dev/null +++ b/core/tests/integration/typecheck/fail/row_conflict_poly_shuffled2.ncl @@ -0,0 +1,20 @@ +# test.type = 'error' +# eval = 'typecheck' +# +# [test.metadata] +# error = 'TypecheckError::RowConflict' +# +# [test.metadata.expectation] +# row = 'a' + +# Regression test for issue #1393 (https://github.com/tweag/nickel/issues/1393). +# Ensure that row constraints are properly checked, indepedently of the order of +# row declarations. +let f + | forall r. {; r } -> { a : Number, b : Number; r } + # the implementation doesn't matter, we care about types + = fun r => null + in +let g = fun x => 'a in +g ((f { x = 0, a = 0, y = 0 }) : _) + diff --git a/core/tests/integration/typecheck/fail/row_conflict_poly_shuffled3.ncl b/core/tests/integration/typecheck/fail/row_conflict_poly_shuffled3.ncl new file mode 100644 index 0000000000..bae7e58e10 --- /dev/null +++ b/core/tests/integration/typecheck/fail/row_conflict_poly_shuffled3.ncl @@ -0,0 +1,20 @@ +# test.type = 'error' +# eval = 'typecheck' +# +# [test.metadata] +# error = 'TypecheckError::RowConflict' +# +# [test.metadata.expectation] +# row = 'a' + +# Regression test for issue #1393 (https://github.com/tweag/nickel/issues/1393). +# Ensure that row constraints are properly checked, indepedently of the order of +# row declarations. +let f + | forall r. {; r } -> { a : Number, b : Number; r } + # the implementation doesn't matter, we care about types + = fun r => null + in +let g = fun x => 'a in +g ((f { x = 0, y = 0, a = 0 }) : _) +