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

@@ -913,32 +913,41 @@ pub type RowConstr = HashMap<VarId, HashSet<Ident>>;
 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<Ident>,
+        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))

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 }) : _)
+

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 }) : _)
+

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 }) : _)
+