Repository: tweag/nickel
Pull request #2130 (2024-12-23 15:16:27)

[RFC007] Extract runtime contract equality out of typecheck
This PR continues the preparation work to migrate the typechecker to the new AST. One current blocker is that  `typecheck::eq` is used both by the typechecker and at runtime for contract deduplication. We need to get rid of this module when switching the typechecker implementation, while still needing to perform contract deduplication at runtime (until the landing of the bytecode virtual machine).

This PR extracts the code from `typecheck::eq` for contract deduplication in a new module, so that the runtime isn't dependent on `typecheck` anymore. The code is specialized (as it doesn't need to handle static contract equality), and in order to eliminate the dependence on `UnifType`, we drop the ability to compare polymorphic types. The latter is the only reason `typecheck::eq` operated on `UnifType` instead of `Type` (which makes it dependent on the old typechecker), but the motivation is not very convincing: how many times do we encounter a type annotation, itself inside a contract annotation, such that annotation is a polymorphic type AND it happens to be a candidate for deduplication? Our intuition would be: zero.

This hypothesis has been validated on our working benchmarks, as `--metrics` show detailed data on contract deduplication - including the total count of deduplicated contracts - which doesn't change between this PR and master.

github-actions[bot]: <h2><a href="https://bencher.dev/perf/nickel/reports/3b4c07d9-70c4-4396-bac0-f3fac877771b?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel"><img src="https://bencher.dev/favicon.svg" width="24" height="24" alt="🐰" /> Bencher Report</a></h2><table><tr><td>Branch</td><td><a href="https://bencher.dev/perf/nickel/branches/rfc007-extract-contract-dedup?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">rfc007/extract-contract-dedup</a></td></tr><tr><td>Testbed</td><td><a href="https://bencher.dev/perf/nickel/testbeds/ubuntu-latest?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">ubuntu-latest</a></td></tr></table><details><summary>Click to view all benchmark results</summary><br /><table><thead><tr><th>Benchmark</th><th><a href="https://bencher.dev/perf/nickel/measures/latency?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">Latency</a></th><th>nanoseconds (ns)</th></tr></thead><tbody><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/fibonacci-10?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">fibonacci 10</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=3cfaf19e-c9c5-4341-95cd-703456d0fc9f&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>502.61</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/foldl-arrays-50?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">foldl arrays 50</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=95048806-9bf2-49e4-88f2-dbcd66cbf68a&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>1,700.20</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/foldl-arrays-500?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">foldl arrays 500</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=15373c31-496e-4f43-bbb4-466ef49fdd87&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>6,780.20</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/foldr-strings-50?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">foldr strings 50</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=87746452-c4df-48ea-b5e9-8d66f82ca556&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>7,030.70</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/foldr-strings-500?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">foldr strings 500</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=7f141ea0-9fbb-4305-bb63-78f163e546d6&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>61,974.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/generate-normal-250?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">generate normal 250</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=8c154d79-dc68-4d93-abb3-83183a62f6a2&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>44,668.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/generate-normal-50?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">generate normal 50</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=6d0222f6-0b85-4eaf-8c5c-e8957c522ef9&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>1,940.60</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/generate-normal-unchecked-1000?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">generate normal unchecked 1000</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=be0d3f87-d089-4b81-af44-3bbc6e831697&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>3,339.70</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/generate-normal-unchecked-200?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">generate normal unchecked 200</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=2946df33-45e4-4282-b749-040582021fe3&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>761.66</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/pidigits-100?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">pidigits 100</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=5be25c57-d46f-4b48-b6f0-dee01b84220a&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>3,200.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/pipe-normal-20?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">pipe normal 20</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=7178a975-b548-4e78-8c84-4f3802668825&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>1,508.70</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/pipe-normal-200?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">pipe normal 200</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=6884f292-8796-44a8-a30c-d3cb2ed987f6&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>10,019.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/product-30?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">product 30</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=2f5f7f6a-4e54-4542-aa09-da5671953fbb&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>849.41</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/scalar-10?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">scalar 10</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=211bb66a-58f8-488b-97e4-7ea032870038&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>1,552.90</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/sum-30?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">sum 30</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=b6a69b2a-f3f5-49a8-b1b2-d1ebb1f301fc&heads=0d35e763-f708-4f60-a811-edb64e1e1d6a&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=3f1710c5-ce75-4dfb-aadb-1435fed8a093&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1732375835000&end_time=1734967835000&report=3b4c07d9-70c4-4396-bac0-f3fac877771b">view plot</a><br />🚷 <a href="https://bencher.dev/perf/nickel/thresholds/33127262-00b8-4370-8dd1-838c28dec7b3?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">view threshold</a></td><td>832.91</td></tr></tbody></table></details><a href="https://bencher.dev/perf/nickel/reports/3b4c07d9-70c4-4396-bac0-f3fac877771b?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr%2Bcomments&utm_term=nickel">🐰 View full continuous benchmarking report in Bencher</a><div id="bencher.dev/projects/nickel/id/rfc007-extract-contract-dedup/ubuntu-latest/rust_criterion"></div>

Patch:
diff --git a/core/src/eval/contract_eq.rs b/core/src/eval/contract_eq.rs
new file mode 100644
index 00000000..ec033194
--- /dev/null
+++ b/core/src/eval/contract_eq.rs
@@ -0,0 +1,518 @@
+//! Computation of contract equality.
+//!
+//! This module is temporary, and has been extracted from the typechecker operating in the legacy
+//! AST (`RichTerm`). It's used by the current tree-walking virtual machine, but will be scrapped
+//! once the bytecode virtual machine (RFC007) is operational. At the time, we won't have the AST
+//! around at runtime anymore, and will use an entirely different technique for contract
+//! deduplication.
+//!
+//! Determine if two contracts are equal at runtime, which is leveraged by the contract
+//! deduplication optimization.
+//!
+//! We first test for physical equality. If the comparison fails, we do a simple structural
+//! recursion, unfolding simple forms and following variables with a limited number of times. For
+//! anything more complex, we return false.
+//!
+//! The terms involved can be arbitrarily complex. Primops applications, `match`, and the like are
+//! quite unlikely to appear inside an annotation (they surely appear inside contract definitions).
+//!
+//! We don't want to compare functions syntactically either. The spirit of this implementation is
+//! to equate aliases or simple constructs that may appear inlined inside an annotation
+//! (applications, records, primitive constants and arrays, mostly) in a structural way, and rely
+//! on physical equality otherwise when two contracts "point" (through maybe variables) to the same
+//! definition.
+//!
+//! ## Recursion
+//!
+//! We must refrain from following all variables links blindly, as there could be cycles in the
+//! graph leading to an infinite loop:
+//!
+//! ```nickel
+//! {
+//!   Foo = Bar,
+//!   Bar = Foo,
+//! }
+//! ```
+//!
+//! Because we just follows variables, and don't apply functions, we can detect cycles while
+//! walking the graph. Still, as it is potentially performed many times during typechecking, type
+//! equality ought to stay reasonably cheap. We choose to just set an arbitrary limit (the gas) on
+//! the number of variable links that the type equality may follow. Doing so, we don't have to
+//! worry about loops anymore.
+use super::{cache::lazy::Thunk, Environment};
+
+use crate::{
+    identifier::LocIdent,
+    term::{self, record::Field, IndexMap, RichTerm, StrChunk, Term, UnaryOp},
+    typ::{
+        EnumRowF, EnumRows, EnumRowsIteratorItem, RecordRowF, RecordRows, RecordRowsIteratorItem,
+        Type, TypeF,
+    },
+};
+
+/// The maximal number of variable links we want to unfold before abandoning the check. It should
+/// stay low, but has been fixed arbitrarily: feel fee to increase reasonably if it turns out
+/// legitimate type equalities between simple contracts are unduly rejected in practice.
+pub const MAX_GAS: u8 = 12;
+
+/// State threaded through the type equality computation.
+#[derive(Copy, Clone, Default)]
+struct State {
+    /// The current gas remaining for variable substitutions. Once it reaches zero and we encounter
+    /// a variable, we abort the computation and return false.
+    gas: u8,
+}
+
+impl State {
+    fn new() -> Self {
+        State { gas: MAX_GAS }
+    }
+
+    /// Try to consume one unit of gas for a variable substitution. Return true in case of success,
+    /// or false if the gas was already at zero.
+    fn use_gas(&mut self) -> bool {
+        if self.gas == 0 {
+            false
+        } else {
+            self.gas -= 1;
+            true
+        }
+    }
+}
+
+/// Compute equality between two contracts.
+///
+/// # Parameters
+///
+/// - `env`: an environment mapping variables to their definition (the second placeholder in a
+///   `let _ = _ in _`)
+pub fn contract_eq(t1: &RichTerm, env1: &Environment, t2: &RichTerm, env2: &Environment) -> bool {
+    contract_eq_bounded(&mut State::new(), t1, env1, t2, env2)
+}
+
+/// **Warning**: this function isn't computing a sound contract equality (it could equate contracts
+/// that aren't actually the same). It is used to deduplicate type and contract annotations for
+/// pretty-printing, where there is no notion of environment and the only thing that matters is
+/// that they are printed the same or not.
+///
+/// Compute equality between two contracts in an empty environment. This means that two variables
+/// with the same name are considered equal.
+pub fn type_eq_noenv(t1: &Type, t2: &Type) -> bool {
+    let empty = Environment::new();
+
+    type_eq_bounded(&mut State::new(), t1, &empty, t2, &empty)
+}
+
+/// Decide type equality on contracts in their respective environment and given the remaining gas
+/// in `state`.
+fn contract_eq_bounded(
+    state: &mut State,
+    t1: &RichTerm,
+    env1: &Environment,
+    t2: &RichTerm,
+    env2: &Environment,
+) -> bool {
+    // Test for physical equality as both an optimization and a way to cheaply equate complex
+    // contracts that happen to point to the same definition (while the purposely limited
+    // structural checks below may reject the equality)
+    if term::SharedTerm::ptr_eq(&t1.term, &t2.term) && Environment::ptr_eq(env1, env2) {
+        return true;
+    }
+
+    match (t1.as_ref(), t2.as_ref()) {
+        (Term::Null, Term::Null) => true,
+        (Term::Bool(b1), Term::Bool(b2)) => b1 == b2,
+        (Term::Num(n1), Term::Num(n2)) => n1 == n2,
+        (Term::Str(s1), Term::Str(s2)) => s1 == s2,
+        (Term::Enum(id1), Term::Enum(id2)) => id1 == id2,
+        (Term::SealingKey(s1), Term::SealingKey(s2)) => s1 == s2,
+        (Term::Sealed(key1, inner1, _), Term::Sealed(key2, inner2, _)) => {
+            key1 == key2 && contract_eq_bounded(state, inner1, env1, inner2, env2)
+        }
+        // We only compare string chunks when they represent a plain string (they don't contain any
+        // interpolated expression), as static string may be currently parsed as such. We return
+        // false for anything more complex.
+        (Term::StrChunks(scs1), Term::StrChunks(scs2)) => {
+            scs1.len() == scs2.len()
+                && scs1
+                    .iter()
+                    .zip(scs2.iter())
+                    .all(|(chunk1, chunk2)| match (chunk1, chunk2) {
+                        (StrChunk::Literal(s1), StrChunk::Literal(s2)) => s1 == s2,
+                        _ => false,
+                    })
+        }
+        (Term::App(head1, arg1), Term::App(head2, arg2)) => {
+            contract_eq_bounded(state, head1, env1, head2, env2)
+                && contract_eq_bounded(state, arg1, env1, arg2, env2)
+        }
+        (Term::Closure(id1), Term::Closure(id2)) if Thunk::ptr_eq(id1, id2) => true,
+        // All variables must be bound at this stage. This is checked by the typechecker when
+        // walking annotations. However, we may assume that `env` is a local environment (that it
+        // doesn't include the stdlib). In that case, free variables (unbound) may be deemed equal
+        // if they have the same identifier: whatever global environment the term will be put in,
+        // free variables are not redefined locally and will be bound to the same value in any case.
+        (Term::Var(id1), Term::Var(id2)) => {
+            match (env1.get(&id1.ident()), env2.get(&id2.ident())) {
+                (Some(idx1), Some(idx2)) => {
+                    // We may end up using one more gas unit if gas was exactly 1. That is
+                    // not very important, and it's simpler to just ignore this case. We
+                    // still return false if gas was already at zero.
+                    let had_gas = state.use_gas();
+                    state.use_gas();
+
+                    let closure1 = idx1.borrow();
+                    let closure2 = idx2.borrow();
+
+                    had_gas
+                        && contract_eq_bounded(
+                            state,
+                            &closure1.body,
+                            &closure1.env,
+                            &closure2.body,
+                            &closure2.env,
+                        )
+                }
+                (None, None) => id1 == id2,
+                _ => false,
+            }
+        }
+        (Term::Closure(idx1), Term::Closure(idx2)) => {
+            // We may end up using one more gas unit if gas was exactly 1. That is
+            // not very important, and it's simpler to just ignore this case. We
+            // still return false if gas was already at zero.
+            let had_gas = state.use_gas();
+            state.use_gas();
+
+            let closure1 = idx1.borrow();
+            let closure2 = idx2.borrow();
+
+            had_gas
+                && contract_eq_bounded(
+                    state,
+                    &closure1.body,
+                    &closure1.env,
+                    &closure2.body,
+                    &closure2.env,
+                )
+        }
+        (Term::Var(id), _) => {
+            state.use_gas()
+                && env1
+                    .get(&id.ident())
+                    .map(|idx| {
+                        let closure = idx.borrow();
+                        contract_eq_bounded(state, &closure.body, &closure.env, t2, env2)
+                    })
+                    .unwrap_or(false)
+        }
+        (_, Term::Var(id)) => {
+            state.use_gas()
+                && env2
+                    .get(&id.ident())
+                    .map(|idx| {
+                        let closure = idx.borrow();
+                        contract_eq_bounded(state, t1, env1, &closure.body, &closure.env)
+                    })
+                    .unwrap_or(false)
+        }
+        (Term::Closure(idx), _) => {
+            let closure = idx.borrow();
+
+            state.use_gas() && contract_eq_bounded(state, &closure.body, &closure.env, t2, env2)
+        }
+        (_, Term::Closure(idx)) => {
+            let closure = idx.borrow();
+
+            state.use_gas() && contract_eq_bounded(state, t1, env1, &closure.body, &closure.env)
+        }
+        (Term::Record(r1), Term::Record(r2)) => {
+            map_eq(
+                contract_eq_fields,
+                state,
+                &r1.fields,
+                env1,
+                &r2.fields,
+                env2,
+            ) && r1.attrs.open == r2.attrs.open
+        }
+        (Term::RecRecord(r1, dyn_fields, _), Term::Record(r2))
+        | (Term::Record(r1), Term::RecRecord(r2, dyn_fields, _)) => {
+            dyn_fields.is_empty()
+                && map_eq(
+                    contract_eq_fields,
+                    state,
+                    &r1.fields,
+                    env1,
+                    &r2.fields,
+                    env2,
+                )
+                && r1.attrs.open == r2.attrs.open
+        }
+        (Term::RecRecord(r1, dyn_fields1, _), Term::RecRecord(r2, dyn_fields2, _)) =>
+        // We only compare records whose field structure is statically known (i.e. without dynamic
+        // fields).
+        {
+            dyn_fields1.is_empty()
+                && dyn_fields2.is_empty()
+                && map_eq(
+                    contract_eq_fields,
+                    state,
+                    &r1.fields,
+                    env1,
+                    &r2.fields,
+                    env2,
+                )
+                && r1.attrs.open == r2.attrs.open
+        }
+        (Term::Array(ts1, attrs1), Term::Array(ts2, attrs2)) => {
+            ts1.len() == ts2.len()
+                && ts1
+                    .iter()
+                    .zip(ts2.iter())
+                    .all(|(t1, t2)| contract_eq_bounded(state, t1, env1, t2, env2))
+                // Ideally we would compare pending contracts, but it's a bit advanced and for now
+                // we only equate arrays without additional contracts
+                && attrs1.pending_contracts.is_empty() && attrs2.pending_contracts.is_empty()
+        }
+        // We must compare the inner values as well as the corresponding contracts or type
+        // annotations.
+        (Term::Annotated(annot1, t1), Term::Annotated(annot2, t2)) => {
+            let value_eq = contract_eq_bounded(state, t1, env1, t2, env2);
+
+            // TODO:
+            // - does it really make sense to compare the annotations?
+            // - does it even happen to have contracts having themselves type annotations?
+            // - and in the latter case, should they be declared unequal because of that?
+            //   The answer to the last question is probably yes, because contracts are
+            //   fundamentally as powerful as function application, so they can change their
+            //   argument.
+
+            // We use the same logic as in the typechecker: the type associated to an annotated
+            // value is either the type annotation, or the first contract annotation.
+            let ty1 = annot1.first();
+            let ty2 = annot2.first();
+
+            let ty_eq = match (ty1, ty2) {
+                (None, None) => true,
+                (Some(ctr1), Some(ctr2)) => {
+                    type_eq_bounded(state, &ctr1.typ, env1, &ctr2.typ, env2)
+                }
+                _ => false,
+            };
+
+            value_eq && ty_eq
+        }
+        (Term::Op1(UnaryOp::RecordAccess(id1), t1), Term::Op1(UnaryOp::RecordAccess(id2), t2)) => {
+            id1 == id2 && contract_eq_bounded(state, t1, env1, t2, env2)
+        }
+        // Contract is just a caching mechanism. `typ` should be the source of truth for equality
+        // (and it's probably easier to prove that type are equal rather than their generated
+        // contract version).
+        (
+            Term::Type {
+                typ: ty1,
+                contract: _,
+            },
+            Term::Type {
+                typ: ty2,
+                contract: _,
+            },
+        ) => type_eq_bounded(state, ty1, env1, ty2, env2),
+        // We don't treat imports, parse errors, nor pairs of terms that don't have the same shape
+        _ => false,
+    }
+}
+
+/// Compute the equality between two hashmaps holding either types or terms.
+fn map_eq<V, F>(
+    mut f: F,
+    state: &mut State,
+    map1: &IndexMap<LocIdent, V>,
+    env1: &Environment,
+    map2: &IndexMap<LocIdent, V>,
+    env2: &Environment,
+) -> bool
+where
+    F: FnMut(&mut State, &V, &Environment, &V, &Environment) -> bool,
+{
+    map1.len() == map2.len()
+        && map1.iter().all(|(id, v1)| {
+            map2.get(id)
+                .map(|v2| f(state, v1, env1, v2, env2))
+                .unwrap_or(false)
+        })
+}
+
+/// Convert record rows to a hashmap.
+///
+/// Require the rows to be closed (i.e. the last element must be `RowEmpty`), otherwise `None` is
+/// returned. `None` is returned as well if a type encountered is not row, or if it is a enum row.
+fn rrows_as_map(erows: &RecordRows) -> Option<IndexMap<LocIdent, &Type>> {
+    let map: Option<IndexMap<LocIdent, _>> = erows
+        .iter()
+        .map(|item| match item {
+            RecordRowsIteratorItem::Row(RecordRowF { id, typ }) => Some((id, typ)),
+            _ => None,
+        })
+        .collect();
+
+    map
+}
+
+/// Convert enum rows to a hashmap.
+///
+/// Require the rows to be closed (i.e. the last element must be `RowEmpty`), otherwise `None` is
+/// returned. `None` is returned as well if a type encountered is not row type, or if it is a
+/// record row.
+fn erows_as_map(erows: &EnumRows) -> Option<IndexMap<LocIdent, Option<&Type>>> {
+    let set: Option<IndexMap<LocIdent, Option<_>>> = erows
+        .iter()
+        .map(|item| match item {
+            EnumRowsIteratorItem::Row(EnumRowF { id, typ }) => Some((id, typ)),
+            _ => None,
+        })
+        .collect();
+
+    set
+}
+
+/// 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(
+    state: &mut State,
+    field1: &Field,
+    env1: &Environment,
+    field2: &Field,
+    env2: &Environment,
+) -> bool {
+    // 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, &t1.typ, env1, &t2.typ.clone(), 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 equality comparison on types. Structurally recurse into type constructors and test that
+/// subtypes or subterms (contracts) are equals.
+fn type_eq_bounded(
+    state: &mut State,
+    ty1: &Type,
+    env1: &Environment,
+    ty2: &Type,
+    env2: &Environment,
+) -> bool {
+    match (&ty1.typ, &ty2.typ) {
+        (TypeF::Wildcard(id1), TypeF::Wildcard(id2)) => id1 == id2,
+        (TypeF::Dyn, TypeF::Dyn)
+        | (TypeF::Number, TypeF::Number)
+        | (TypeF::Bool, TypeF::Bool)
+        | (TypeF::Symbol, TypeF::Symbol)
+        | (TypeF::String, TypeF::String) => true,
+        (
+            TypeF::Dict {
+                type_fields: uty1,
+                flavour: attrs1,
+            },
+            TypeF::Dict {
+                type_fields: uty2,
+                flavour: attrs2,
+            },
+        ) if attrs1 == attrs2 => type_eq_bounded(state, uty1, env1, uty2, env2),
+        (TypeF::Array(uty1), TypeF::Array(uty2)) => type_eq_bounded(state, uty1, env1, uty2, env2),
+        (TypeF::Arrow(s1, t1), TypeF::Arrow(s2, t2)) => {
+            type_eq_bounded(state, s1, env1, s2, env2) && type_eq_bounded(state, t1, env1, t2, env2)
+        }
+        (TypeF::Enum(uty1), TypeF::Enum(uty2)) => {
+            fn type_eq_bounded_wrapper(
+                state: &mut State,
+                uty1: &Option<&Type>,
+                env1: &Environment,
+                uty2: &Option<&Type>,
+                env2: &Environment,
+            ) -> bool {
+                match (uty1, uty2) {
+                    (Some(uty1), Some(uty2)) => type_eq_bounded(state, uty1, env1, uty2, env2),
+                    (None, None) => true,
+                    _ => false,
+                }
+            }
+
+            let map1 = erows_as_map(uty1);
+            let map2 = erows_as_map(uty2);
+
+            map1.zip(map2)
+                .map(|(m1, m2)| map_eq(type_eq_bounded_wrapper, state, &m1, env1, &m2, env2))
+                .unwrap_or(false)
+        }
+        (TypeF::Record(uty1), TypeF::Record(uty2)) => {
+            fn type_eq_bounded_wrapper(
+                state: &mut State,
+                uty1: &&Type,
+                env1: &Environment,
+                uty2: &&Type,
+                env2: &Environment,
+            ) -> bool {
+                type_eq_bounded(state, uty1, env1, uty2, env2)
+            }
+
+            let map1 = rrows_as_map(uty1);
+            let map2 = rrows_as_map(uty2);
+
+            map1.zip(map2)
+                .map(|(m1, m2)| map_eq(type_eq_bounded_wrapper, state, &m1, env1, &m2, env2))
+                .unwrap_or(false)
+        }
+        (TypeF::Contract(t1), TypeF::Contract(t2)) => {
+            contract_eq_bounded(state, t1, env1, t2, env2)
+        }
+        // We don't handle foralls in this temporary module: they are unlikely to appear,
+        // and they require type substitution machinery.
+        _ => false,
+    }
+}
diff --git a/core/src/eval/mod.rs b/core/src/eval/mod.rs
index eb5e2d04..8daa2137 100644
--- a/core/src/eval/mod.rs
+++ b/core/src/eval/mod.rs
@@ -99,6 +99,7 @@ use std::io::Write;
 
 pub mod cache;
 pub mod callstack;
+pub mod contract_eq;
 pub mod fixpoint;
 pub mod merge;
 pub mod operation;
diff --git a/core/src/eval/operation.rs b/core/src/eval/operation.rs
index 4e1a8f8c..aa4d237e 100644
--- a/core/src/eval/operation.rs
+++ b/core/src/eval/operation.rs
@@ -8,6 +8,7 @@
 //! receive evaluated operands and implement the actual semantics of operators.
 use super::{
     cache::lazy::Thunk,
+    contract_eq::contract_eq,
     merge::{self, split, MergeMode},
     stack::StrAccData,
     subst, Cache, Closure, Environment, ImportResolver, VirtualMachine,
@@ -35,7 +36,6 @@ use crate::{
         string::NickelString,
         *,
     },
-    typecheck::eq::contract_eq,
 };
 
 #[cfg(feature = "metrics")]
@@ -2481,7 +2481,6 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                 let twin_index = ctrs_right_sieve.iter().position(|other_ctr| {
                                     other_ctr.as_ref().map_or(false, |other_ctr| {
                                         contract_eq(
-                                            0,
                                             &ctr.contract,
                                             &env1,
                                             &other_ctr.contract,
diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs
index a92b673e..abf7d056 100644
--- a/core/src/term/mod.rs
+++ b/core/src/term/mod.rs
@@ -24,7 +24,7 @@ use crate::{
     cache::InputFormat,
     combine::Combine,
     error::{EvalError, ParseError},
-    eval::{cache::CacheIndex, Environment},
+    eval::{cache::CacheIndex, contract_eq, Environment},
     files::FileId,
     identifier::{Ident, LocIdent},
     impl_display_from_pretty,
@@ -34,7 +34,6 @@ use crate::{
     pretty::PrettyPrintCap,
     traverse::*,
     typ::{Type, UnboundTypeVariableError},
-    typecheck::eq::{contract_eq, type_eq_noenv},
 };
 
 use crate::metrics::increment;
@@ -502,7 +501,7 @@ impl RuntimeContract {
 
     /// Push a pending contract to a vector of contracts if the contract to add isn't already
     /// present in the vector, according to the notion of contract equality defined in
-    /// [crate::typecheck::eq].
+    /// [crate::eval::contract_eq].
     pub fn push_dedup(
         contracts: &mut Vec<RuntimeContract>,
         env1: &Environment,
@@ -512,7 +511,7 @@ impl RuntimeContract {
         for c in contracts.iter() {
             increment!("contracts:equality-checks");
 
-            if contract_eq(0, &c.contract, env1, &ctr.contract, env2) {
+            if contract_eq::contract_eq(&c.contract, env1, &ctr.contract, env2) {
                 increment!("contracts:deduped");
                 return;
             }
@@ -888,7 +887,7 @@ impl TypeAnnotation {
     ///
     /// Same as [`crate::combine::Combine`], but eliminate duplicate contracts. As there's no
     /// notion of environment when considering mere annotations, we use an unsound contract
-    /// equality checking which correspond to compares contracts syntactically.
+    /// equality checking which correspond to comparing contracts syntactically.
     pub fn combine_dedup(left: Self, right: Self) -> Self {
         let mut contracts = left.contracts;
 
@@ -901,7 +900,10 @@ impl TypeAnnotation {
         };
 
         for ctr in right.contracts.into_iter() {
-            if !contracts.iter().any(|c| type_eq_noenv(0, &c.typ, &ctr.typ)) {
+            if !contracts
+                .iter()
+                .any(|c| contract_eq::type_eq_noenv(&c.typ, &ctr.typ))
+            {
                 contracts.push(ctr);
             }
         }
diff --git a/core/stdlib/std.ncl b/core/stdlib/std.ncl
index 91086278..ed5c5af9 100644
--- a/core/stdlib/std.ncl
+++ b/core/stdlib/std.ncl
@@ -3187,7 +3187,7 @@
           # => error
           ```
         "%%
-      = fun field content r => %record/insert% field r content,
+      = fun field content r => %record/insert% field (%record/freeze% r) content,
 
     insert_with_opts
       : forall a. String -> a -> { _ : a } -> { _ : a }
@@ -3221,7 +3221,7 @@
           # => error
           ```
         "%%
-      = fun field content r => %record/insert_with_opts% field r content,
+      = fun field content r => %record/insert_with_opts% field (%record/freeze% r) content,
 
     remove
       : forall a. String -> { _ : a } -> { _ : a }
@@ -3256,7 +3256,7 @@
           # => error
           ```
         "%
-      = fun field r => %record/remove% field r,
+      = fun field r => %record/remove% field (%record/freeze% r),
 
     remove_with_opts
       : forall a. String -> { _ : a } -> { _ : a }
@@ -3284,7 +3284,7 @@
           # => error
           ```
         "%
-      = fun field r => %record/remove_with_opts% field r,
+      = fun field r => %record/remove_with_opts% field (%record/freeze% r),
 
     update
       : forall a. String -> a -> { _ : a } -> { _ : a }
@@ -3327,6 +3327,7 @@
           ```
         "%
       = fun field content r =>
+        let r = %record/freeze% r in
         let r =
           if %record/has_field% field r then
             %record/remove% field r


Test patch:
diff --git a/core/tests/integration/inputs/records/freeze_insert_fails_on_missing.ncl b/core/tests/integration/inputs/records/freeze_insert_fails_on_missing.ncl
new file mode 100644
index 00000000..22dfaa4a
--- /dev/null
+++ b/core/tests/integration/inputs/records/freeze_insert_fails_on_missing.ncl
@@ -0,0 +1,8 @@
+# test.type = 'error'
+#
+# [test.metadata]
+# error = 'EvalError::MissingFieldDef'
+#
+# [test.metadata.expectation]
+# field = 'bar'
+((std.record.insert "bar" 1 { foo = bar + 1, bar | optional }) & { bar | force = 2 }).foo
diff --git a/core/tests/integration/inputs/records/freezing_ops.ncl b/core/tests/integration/inputs/records/freezing_ops.ncl
new file mode 100644
index 00000000..b289ad6e
--- /dev/null
+++ b/core/tests/integration/inputs/records/freezing_ops.ncl
@@ -0,0 +1,15 @@
+# test.type = 'pass'
+[
+  ((std.record.insert "baz" 1 { foo = bar + 1, bar = 0 }) & { bar | force = 2 }) == { foo = 1, bar = 2, baz = 1 },
+  ((std.record.insert_with_opts "baz" 1 { foo = bar + 1, bar = 0 }) & { bar | force = 2 }) == { foo = 1, bar = 2, baz = 1 },
+  (
+    (std.record.remove "to_remove" { foo = bar + 1, bar = 0, to_remove = false, rev_dep = to_remove })
+    & { bar | force = 1, to_remove = true }
+  ) == { foo = 1, bar = 1, to_remove = true, rev_dep = false },
+  (
+    (std.record.remove_with_opts "to_remove" { foo = bar + 1, bar = 0, to_remove = false, rev_dep = to_remove })
+    & { bar | force = 1, to_remove = true }
+  ) == { foo = 1, bar = 1, to_remove = true, rev_dep = false },
+  ((std.record.update "bar" 1 { foo = bar + 1, bar = 0 }) & { bar | force = 2 }) == { foo = 1, bar = 2, },
+]
+|> std.test.assert_all