Check bare row arguments through the shared instantiation relation

Author: biuld

crates/psrs-core/src/tests/instantiation.rs

@@ -234,3 +234,167 @@ fn row_evidence_retains_residuals_without_an_arena_node() {
     assert_eq!(evidence.constructor(variable), None);
     assert_eq!(evidence.row(TypeVariableId(41)).map(|row| row.fields), None);
 }
+
+fn row(types: &mut Vec<Type>, fields: &[(&str, TypeId)], tail: TypeId) -> TypeId {
+    fields.iter().rev().fold(tail, |tail, (label, ty)| {
+        let id = TypeId(types.len() as u32);
+        types.push(Type::RowExtend {
+            label: (*label).into(),
+            ty: *ty,
+            tail,
+        });
+        id
+    })
+}
+
+#[test]
+fn nominal_row_arguments_preserve_checked_residuals_and_label_order_independence() {
+    let variable = TypeVariableId(40);
+    let mut types = vec![
+        Type::Constructor(TypeConstructor::Int),
+        Type::Constructor(TypeConstructor::Boolean),
+        Type::RowEmpty,
+        Type::Variable(variable),
+    ];
+    let generic_row = row(&mut types, &[("y", TypeId(0))], TypeId(3));
+    let generic = nominal(&mut types, 1, generic_row);
+    let concrete_row = row(
+        &mut types,
+        &[("a", TypeId(0)), ("b", TypeId(1)), ("y", TypeId(0))],
+        TypeId(2),
+    );
+    let concrete = nominal(&mut types, 1, concrete_row);
+    let reordered_row = row(
+        &mut types,
+        &[("y", TypeId(0)), ("b", TypeId(1)), ("a", TypeId(0))],
+        TypeId(2),
+    );
+    let reordered = nominal(&mut types, 1, reordered_row);
+    let generic_arrow = arrow(&mut types, generic, generic);
+    let consistent_arrow = arrow(&mut types, concrete, reordered);
+    let different_row = row(
+        &mut types,
+        &[("y", TypeId(0)), ("b", TypeId(0)), ("a", TypeId(0))],
+        TypeId(2),
+    );
+    let different = nominal(&mut types, 1, different_row);
+    let inconsistent_arrow = arrow(&mut types, concrete, different);
+    let missing_row = row(&mut types, &[("a", TypeId(0))], TypeId(2));
+    let missing = nominal(&mut types, 1, missing_row);
+    let duplicate_row = row(&mut types, &[("y", TypeId(0)), ("y", TypeId(0))], TypeId(2));
+    let duplicate = nominal(&mut types, 1, duplicate_row);
+    let module = bare(types);
+    let evidence = module
+        .checked_instantiation(generic_arrow, &[variable], consistent_arrow)
+        .unwrap();
+    let mut residual = evidence.row(variable).unwrap();
+    residual.fields.sort_by(|left, right| left.0.cmp(&right.0));
+    assert_eq!(
+        residual.fields,
+        vec![("a".into(), TypeId(0)), ("b".into(), TypeId(1))]
+    );
+    assert_eq!(residual.tail, None);
+    assert!(
+        module
+            .checked_instantiation(concrete, &[], reordered)
+            .is_some()
+    );
+    assert!(
+        module
+            .checked_instantiation(generic_arrow, &[variable], inconsistent_arrow)
+            .is_none()
+    );
+    assert!(
+        module
+            .checked_instantiation(generic, &[], concrete)
+            .is_none(),
+        "rigid tails cannot absorb fields"
+    );
+    assert!(
+        module
+            .checked_instantiation(generic, &[variable], missing)
+            .is_none()
+    );
+    let duplicate_evidence = module
+        .checked_instantiation(generic, &[variable], duplicate)
+        .unwrap();
+    assert_eq!(
+        duplicate_evidence.row(variable).unwrap().fields,
+        vec![("y".into(), TypeId(0))]
+    );
+}
+
+#[test]
+fn nominal_row_arguments_preserve_duplicate_label_occurrence_order() {
+    let variable = TypeVariableId(41);
+    let mut types = vec![
+        Type::Constructor(TypeConstructor::Int),
+        Type::Constructor(TypeConstructor::Boolean),
+        Type::RowEmpty,
+        Type::Variable(variable),
+    ];
+    let scheme_row = row(&mut types, &[("a", TypeId(0)), ("a", TypeId(1))], TypeId(3));
+    let scheme = nominal(&mut types, 1, scheme_row);
+    let matching_row = row(
+        &mut types,
+        &[("z", TypeId(0)), ("a", TypeId(0)), ("a", TypeId(1))],
+        TypeId(2),
+    );
+    let matching = nominal(&mut types, 1, matching_row);
+    let reversed_row = row(
+        &mut types,
+        &[("a", TypeId(1)), ("a", TypeId(0)), ("z", TypeId(0))],
+        TypeId(2),
+    );
+    let reversed = nominal(&mut types, 1, reversed_row);
+    let module = bare(types);
+    let evidence = module
+        .checked_instantiation(scheme, &[variable], matching)
+        .unwrap();
+    assert_eq!(
+        evidence.row(variable).unwrap().fields,
+        vec![("z".into(), TypeId(0))]
+    );
+    assert!(
+        module
+            .checked_instantiation(scheme, &[variable], reversed)
+            .is_none()
+    );
+}
+
+#[test]
+fn repeated_residual_fields_use_the_checked_relation_for_nested_row_arguments() {
+    let variable = TypeVariableId(42);
+    let mut types = vec![
+        Type::Constructor(TypeConstructor::Int),
+        Type::Constructor(TypeConstructor::Boolean),
+        Type::RowEmpty,
+        Type::Variable(variable),
+    ];
+    let nested_left = row(&mut types, &[("a", TypeId(0)), ("b", TypeId(1))], TypeId(2));
+    let nested_left = nominal(&mut types, 2, nested_left);
+    let nested_right = row(&mut types, &[("b", TypeId(1)), ("a", TypeId(0))], TypeId(2));
+    let nested_right = nominal(&mut types, 2, nested_right);
+    let scheme_row = row(&mut types, &[("y", TypeId(0))], TypeId(3));
+    let scheme = nominal(&mut types, 1, scheme_row);
+    let scheme = arrow(&mut types, scheme, scheme);
+    let domain_row = row(
+        &mut types,
+        &[("x", nested_left), ("y", TypeId(0))],
+        TypeId(2),
+    );
+    let domain = nominal(&mut types, 1, domain_row);
+    let codomain_row = row(
+        &mut types,
+        &[("y", TypeId(0)), ("x", nested_right)],
+        TypeId(2),
+    );
+    let codomain = nominal(&mut types, 1, codomain_row);
+    let instance = arrow(&mut types, domain, codomain);
+    let module = bare(types);
+    assert!(
+        module
+            .checked_instantiation(scheme, &[variable], instance)
+            .is_some()
+    );
+}

crates/psrs-core/src/verify/types/matching/invariant.rs

@@ -164,22 +164,8 @@ impl TypeMatcher<'_> {
                     )
                 }
             }
-            (Type::RowEmpty, Type::RowEmpty) => true,
-            (
-                Type::RowExtend {
-                    label: left_label,
-                    ty: left_ty,
-                    tail: left_tail,
-                },
-                Type::RowExtend {
-                    label: right_label,
-                    ty: right_ty,
-                    tail: right_tail,
-                },
-            ) => {
-                left_label == right_label
-                    && self.relate(*left_ty, *right_ty, Variance::Invariant, false)
-                    && self.relate(*left_tail, *right_tail, Variance::Invariant, false)
+            (Type::RowEmpty | Type::RowExtend { .. }, Type::RowEmpty | Type::RowExtend { .. }) => {
+                self.relate_rows(source, target, Variance::Invariant)
             }
             _ => false,
         };

crates/psrs-core/src/verify/types/matching/mod.rs

@@ -363,22 +363,8 @@ impl TypeMatcher<'_> {
                     self.relate(actual, expected, Variance::Invariant, false)
                 }
             }
-            (Type::RowEmpty, Type::RowEmpty) => true,
-            (
-                Type::RowExtend {
-                    label: actual_label,
-                    ty: actual_ty,
-                    tail: actual_tail,
-                },
-                Type::RowExtend {
-                    label: expected_label,
-                    ty: expected_ty,
-                    tail: expected_tail,
-                },
-            ) => {
-                actual_label == expected_label
-                    && self.relate(*actual_ty, *expected_ty, Variance::Subsumption, true)
-                    && self.relate(*actual_tail, *expected_tail, Variance::Invariant, false)
+            (Type::RowEmpty | Type::RowExtend { .. }, Type::RowEmpty | Type::RowExtend { .. }) => {
+                self.relate_rows(actual, expected, Variance::Invariant)
             }
             _ => false,
         };

crates/psrs-core/src/verify/types/matching/rows.rs

@@ -1,4 +1,3 @@
-use super::super::types_compatible;
 use super::helpers::collect_free_variables;
 use super::{TypeMatcher, Variance};
 use crate::{Type, TypeId, record_row};
@@ -31,30 +30,68 @@ impl TypeMatcher<'_> {
         ) else {
             return false;
         };
+        for row in [actual_row, expected_row] {
+            let Some((fields, _)) = self.flatten_row(row) else {
+                return false;
+            };
+            let mut labels = HashSet::new();
+            if fields.iter().any(|(label, _)| !labels.insert(label)) {
+                return false;
+            }
+        }
+        self.relate_rows(actual_row, expected_row, variance)
+    }
+
+    /// Bare rows in nominal arguments use the same checked residual relation as
+    /// records. The caller owns variance; nominal row arguments are invariant.
+    pub(super) fn relate_rows(
+        &mut self,
+        actual: TypeId,
+        expected: TypeId,
+        variance: Variance,
+    ) -> bool {
         let (Some((actual_fields, actual_tail)), Some((expected_fields, expected_tail))) =
-            (self.flatten_row(actual_row), self.flatten_row(expected_row))
+            (self.flatten_row(actual), self.flatten_row(expected))
         else {
             return false;
         };
-        let Some(mut expected_fields) = index_fields(expected_fields) else {
-            return false;
-        };
+        let mut expected_fields = expected_fields;
+        let mut actual_fields = actual_fields;
+        // Preserve duplicate-label occurrence order while ignoring the order
+        // of distinct labels. Bare rows may contain duplicates (e.g. Union).
+        actual_fields.sort_by(|left, right| left.0.cmp(&right.0));
+        expected_fields.sort_by(|left, right| left.0.cmp(&right.0));
+        let (mut actual_index, mut expected_index) = (0, 0);
         let mut actual_rest = Vec::new();
-        let mut seen = HashSet::new();
-        for (label, actual_ty) in actual_fields {
-            if !seen.insert(label.clone()) {
-                return false;
-            }
-            if let Some(expected_ty) = expected_fields.remove(&label) {
-                let instantiate = variance == Variance::Subsumption;
-                if !self.relate(actual_ty, expected_ty, variance, instantiate) {
-                    return false;
+        let mut expected_rest = Vec::new();
+        while actual_index < actual_fields.len() && expected_index < expected_fields.len() {
+            let actual_field = &actual_fields[actual_index];
+            let expected_field = &expected_fields[expected_index];
+            match actual_field.0.cmp(&expected_field.0) {
+                std::cmp::Ordering::Equal => {
+                    if !self.relate(
+                        actual_field.1,
+                        expected_field.1,
+                        variance,
+                        variance == Variance::Subsumption,
+                    ) {
+                        return false;
+                    }
+                    actual_index += 1;
+                    expected_index += 1;
+                }
+                std::cmp::Ordering::Less => {
+                    actual_rest.push(actual_field.clone());
+                    actual_index += 1;
+                }
+                std::cmp::Ordering::Greater => {
+                    expected_rest.push(expected_field.clone());
+                    expected_index += 1;
                 }
-            } else {
-                actual_rest.push((label, actual_ty));
             }
         }
-        let expected_rest = expected_fields.into_iter().collect::<Vec<_>>();
+        actual_rest.extend(actual_fields[actual_index..].iter().cloned());
+        expected_rest.extend(expected_fields[expected_index..].iter().cloned());
         self.finish_row(actual_rest, actual_tail, expected_rest, expected_tail)
     }
 
@@ -189,15 +226,7 @@ impl TypeMatcher<'_> {
     }
 
     fn types_equal(&mut self, left: TypeId, right: TypeId) -> bool {
-        let mut alpha = self.alpha.clone();
-        types_compatible(left, right, self.module, &mut HashSet::new(), &mut alpha)
-            && types_compatible(
-                right,
-                left,
-                self.module,
-                &mut HashSet::new(),
-                &mut self.alpha.clone(),
-            )
+        self.relate(left, right, Variance::Invariant, false)
     }
 
     fn flatten_row(&self, mut row: TypeId) -> Option<RowShape> {
@@ -257,16 +286,6 @@ impl TypeMatcher<'_> {
     }
 }
 
-fn index_fields(fields: Vec<(String, TypeId)>) -> Option<HashMap<String, TypeId>> {
-    let mut indexed = HashMap::new();
-    for (label, ty) in fields {
-        if indexed.insert(label, ty).is_some() {
-            return None;
-        }
-    }
-    Some(indexed)
-}
-
 fn same_labels(left: &[(String, TypeId)], right: &[(String, TypeId)]) -> bool {
     let mut left = left.to_vec();
     let mut right = right.to_vec();

docs/design/frontend/type-system/rows-and-records.md

@@ -103,6 +103,16 @@ Row equality is independent of source label order; matched fields have equal che
 
 P5 receives kind-checked row expressions and resolved record operations from HIR. It supplies type equations and evidence to [type inference](type-inference.md) and emits verified THIR. Row normalization and the primitive row relations are internal to P5 and share the kind and evidence contracts of [kinds](kinds.md) and [classes](classes-and-evidence.md); a later stage receives only checked row types. The backend chooses record and variant representation only after Core lowering.
 
+Core checks bare rows inside nominal type arguments with the same label-based
+row relation as record rows. Nominal arguments stay invariant: fields must have
+matching types, repeated bare-row labels retain their occurrence order, closed
+rows must have the same label occurrences, and rigid tails cannot
+absorb extra fields. Only quantified flexible tails receive checked residual
+substitutions. Those residuals remain in instantiation evidence even when no
+existing type-arena node represents them; later local-row materialization uses
+that evidence rather than reconstructing the match.
+
+
 ## Open questions and future work
 
 Use official tests to pin down duplicate-label diagnostics, record-update edge cases, and primitive row improvement order; [primitives](prim.md) owns the rules those tests exercise. [DEC-04](../../../decision/DEC-04-official-test-suite-roadmap.md) tracks implementation coverage.