From 4a4825e688c719ebb729837bf192c6e3bc79664c Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Mon, 16 Sep 2024 18:08:55 +0200
Subject: [PATCH] Fix unsound record contract deduplication (#2042)

* Fix contract equality unsound on records

Contract equality code used to flat out ignore all of the metadata of a
fields, including contract annotations, which is obviously entirely
wrong. This means that `{foo | String}` and `{foo | Number}` was deemed
equal and deduplicated as the same contract.

This commit fixes the issue by comparing the metadata as well. Contract
labels are a subtle matter, and they are the only part that is ignored
by the contract equality code.

* Add comparison of label's type_environment for safety

* Update core/src/typecheck/eq.rs

Co-authored-by: jneem <joeneeman@gmail.com>

* Add integration test for contract dedup unsoundness

---------

Co-authored-by: jneem <joeneeman@gmail.com>
---
 core/src/typecheck/eq.rs                      | 53 ++++++++++++++++++-
 .../unsound_dedup_record_contract.ncl         | 49 +++++++++++++++++
 2 files changed, 100 insertions(+), 2 deletions(-)
 create mode 100644 core/tests/integration/inputs/contracts/unsound_dedup_record_contract.ncl

diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index 0cceb9e377..e9835b2806 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -548,6 +548,11 @@ fn erows_as_map<E: TermEnvironment>(
 
 /// Check for contract equality between record fields. Fields are equal if they are both without a
 /// definition, or are both defined and their values are equal.
+///
+/// The attached metadata must be equal as well: most record contracts are written as field with
+/// metadata but without definition. For example, take `{ foo | {bar | Number}}` and `{foo | {bar |
+/// String}}`. Those two record contracts are obviously not equal, but to know that, we have to
+/// look at the contracts of each bar field.
 fn contract_eq_fields<E: TermEnvironment>(
     state: &mut State,
     field1: &Field,
@@ -555,13 +560,57 @@ fn contract_eq_fields<E: TermEnvironment>(
     field2: &Field,
     env2: &E,
 ) -> bool {
-    match (&field1.value, &field2.value) {
+    // Check that the pending contracts are equal.
+    //
+    // [^contract-eq-ignore-label]: We mostly ignore the label here, which doesn't impact the fact
+    // that a contract blame or not. Different labels might lead to different error messages,
+    // though. Note that there is one important exception: the field `type_environment` does impact
+    // the evaluation of the contract. Fortunately, it's a simple datastructure that is easy to
+    // compare, so we do check for equality here.
+    //
+    // Otherwise, comparing the rest of the labels seem rather clumsy (as labels store a wide
+    // variety of static and runtime data) and not very meaningful.
+    let pending_contracts_eq = field1
+        .pending_contracts
+        .iter()
+        .zip(field2.pending_contracts.iter())
+        .all(|(c1, c2)| {
+            c1.label.type_environment == c2.label.type_environment
+                && contract_eq_bounded(state, &c1.contract, env1, &c2.contract, env2)
+        });
+
+    // Check that the type and contrat annotations are equal. [^contract-eq-ignore-label] applies
+    // here as well.
+    let annotations_eq = field1
+        .metadata
+        .annotation
+        .iter()
+        .zip(field2.metadata.annotation.iter())
+        .all(|(t1, t2)| {
+            t1.label.type_environment == t2.label.type_environment
+                && type_eq_bounded(
+                    state,
+                    &GenericUnifType::from_type(t1.typ.clone(), env1),
+                    env1,
+                    &GenericUnifType::from_type(t2.typ.clone(), env2),
+                    env2,
+                )
+        });
+
+    // Check that "scalar" metadata (simple values) are equals
+    let scalar_metadata_eq = field1.metadata.opt == field2.metadata.opt
+        && field1.metadata.not_exported == field2.metadata.not_exported
+        && field1.metadata.priority == field2.metadata.priority;
+
+    let value_eq = match (&field1.value, &field2.value) {
         (Some(ref value1), Some(ref value2)) => {
             contract_eq_bounded(state, value1, env1, value2, env2)
         }
         (None, None) => true,
         _ => false,
-    }
+    };
+
+    pending_contracts_eq && annotations_eq && scalar_metadata_eq && value_eq
 }
 
 /// Perform the type equality comparison on types. Structurally recurse into type constructors and
diff --git a/core/tests/integration/inputs/contracts/unsound_dedup_record_contract.ncl b/core/tests/integration/inputs/contracts/unsound_dedup_record_contract.ncl
new file mode 100644
index 0000000000..beb669e0a7
--- /dev/null
+++ b/core/tests/integration/inputs/contracts/unsound_dedup_record_contract.ncl
@@ -0,0 +1,49 @@
+# test.type = 'error'
+# eval = 'full'
+#
+# [test.metadata]
+# error = 'EvalError::BlameError'
+
+# Regression test for https://github.com/tweag/nickel/issues/1700
+let outer = {
+  spec
+    | {
+      hostAliases | Number,
+      containers | Number,
+    },
+}
+in
+
+let inner = {
+  spec
+    | {
+      hostAliases,
+      containers
+        | Array {
+          ..
+        },
+    },
+}
+in
+
+std.deep_seq
+  (
+    {
+      spec = {
+        hostAliases = "this should fail",
+        containers = [
+          {
+            name = "test",
+            image = "nginx",
+            ports = [
+              {
+                containerPort = 80,
+                name = "http"
+              }
+            ],
+          }
+        ]
+      }
+    } | inner | outer
+  )
+  true