Repository: tweag/nickel
Pull request #2007 (2024-07-25 12:22:54)

Add record constructor to subtyping

yannham: > Do you know how to reconstruct a GenericUnifType from GenericUnifRecordRows.

The best is, if those record rows are coming from destructuring a unif type to begin with, is to keep the original `var_levels` around so that you can reconstruct the original type.

If this type is modified, or generated, or coming from some type inference transformation, you can just use `UnifType::concrete` (or `GenericUnifType::concrete`), the method with a lowercase `c` (and not the constructor `Concrete`), which takes care of updating and filling the levels accordingly.
Eckaos: The commit `58af17d` break stuff about record. 
Left to do : 
- [ ] Comments
- [ ] Fix the problem about records
- [ ] Remove subsumption function in `typecheck/mod.rs`
Eckaos: - [ ]  Add documentation
Eckaos: To de-duplicate the code between `is_subsumed_by` and `unify`, we can just call `unify` where we need in `is_subsumed_by`. The cost will be the cost of pattern matching + function call (depends on what optimization the rust compiler will do). Or we could abstract cases that are the same in `is_subsumed_by` and `unify` into another function. The cost will be pattern matching + function call in the two functions (depends on what optimization the rust compiler will do). @yannham 
yannham: > To de-duplicate the code between is_subsumed_by and unify, we can just call unify where we need in is_subsumed_by. 

I'm not sure to understand what you mean here. For example, when subsuming record types, we do the same general work but we still recursively calls `is_subsumed_by` on each component, so we can't just replace the whole case by a call to `unify`. Indeed, I think we need to have a core function that is generic how it calls itself recursively. It's certainly doable, but we can do that in a second step.

P.S: it could be good to have tests for more complicated record types: types with tails, record types with subsumption acting on several components, etc.
Eckaos: I was talking about cases where we do exactly the same work (with Constant and UnifVar etc...). In those cases, we can call `unify` from `is_subsumed_by`.
The other alternative was to factor out a function which does only cases where it is the same result for `unify` and `is_subsumed_by` and then call it from `unify` and `is_subsumed_by` when needed.
github-actions[bot]: <h1><a href="https://bencher.dev/"><img src="https://bencher.dev/favicon.svg" width="32" height="32" alt="🐰" /></a>Bencher</h1><table><tr><td>Report</td><td>Tue, August  6, 2024 at 13:33:40 UTC</td></tr><tr><td>Project</td><td><a href="https://bencher.dev/perf/nickel">nickel</a></td></tr><tr><td>Branch</td><td>2007/merge</td></tr><tr><td>Testbed</td><td>ubuntu-latest</td></tr></table><blockquote><p><b>⚠️ WARNING:</b> The following Measure does not have a Threshold. Without a Threshold, no Alerts will ever be generated!</p><ul><li>Latency (latency)</li></ul><p><a href="https://bencher.dev/console/projects/nickel/thresholds/add">Click here to create a new Threshold</a><br />For more information, see <a href="https://bencher.dev/docs/explanation/thresholds/">the Threshold documentation</a>.<br />To only post results if a Threshold exists, set <a href="https://bencher.dev/docs/explanation/bencher-run/#--ci-only-thresholds">the <code lang="rust">--ci-only-thresholds</code> CLI flag</a>.</p></blockquote><details><summary>Click to view all benchmark results</summary><table><tr><th>Benchmark</th><th>Latency</th><th>Latency Results<br/>nanoseconds (ns)</th></tr><tr><td>fibonacci 10</td><td>➖ (<a href="https://bencher.dev/perf/nickel?branches=fb353459-5cf8-4533-8561-d01d1eea11ba&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=3cfaf19e-c9c5-4341-95cd-703456d0fc9f&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1720359220000&end_time=1722951220000">view plot</a>)</td><td>495,190.00</td></tr><tr><td>pidigits 100</td><td>➖ (<a href="https://bencher.dev/perf/nickel?branches=fb353459-5cf8-4533-8561-d01d1eea11ba&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=5be25c57-d46f-4b48-b6f0-dee01b84220a&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1720359220000&end_time=1722951220000">view plot</a>)</td><td>3,162,200.00</td></tr><tr><td>product 30</td><td>➖ (<a href="https://bencher.dev/perf/nickel?branches=fb353459-5cf8-4533-8561-d01d1eea11ba&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=2f5f7f6a-4e54-4542-aa09-da5671953fbb&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1720359220000&end_time=1722951220000">view plot</a>)</td><td>803,740.00</td></tr><tr><td>scalar 10</td><td>➖ (<a href="https://bencher.dev/perf/nickel?branches=fb353459-5cf8-4533-8561-d01d1eea11ba&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=211bb66a-58f8-488b-97e4-7ea032870038&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1720359220000&end_time=1722951220000">view plot</a>)</td><td>1,483,200.00</td></tr><tr><td>sum 30</td><td>➖ (<a href="https://bencher.dev/perf/nickel?branches=fb353459-5cf8-4533-8561-d01d1eea11ba&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=3f1710c5-ce75-4dfb-aadb-1435fed8a093&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1720359220000&end_time=1722951220000">view plot</a>)</td><td>798,300.00</td></tr></table></details><br/><small><a href="https://bencher.dev">Bencher - Continuous Benchmarking</a></small><br/><small><a href="https://bencher.dev/perf/nickel">View Public Perf Page</a></small><br/><small><a href="https://bencher.dev/docs/">Docs</a> | <a href="https://bencher.dev/repo/">Repo</a> | <a href="https://bencher.dev/chat/">Chat</a> | <a href="https://bencher.dev/help/">Help</a></small><div id="bencher.dev/projects/nickel/id/2007-merge/ubuntu-latest/rust_criterion"></div>

Patch:
diff --git a/.github/workflows/continuous-integration.yml b/.github/workflows/continuous-integration.yml
index ba181c6e..0b962b6f 100644
--- a/.github/workflows/continuous-integration.yml
+++ b/.github/workflows/continuous-integration.yml
@@ -83,3 +83,18 @@ jobs:
 
     - name: Typecheck benchmarks
       run: find core/benches -type f -name "*.ncl" -print0 | xargs -0 -I file nix run . -- typecheck file
+
+  build-and-test-windows:
+    name: "build-and-test (windows-latest, stable)"
+    runs-on: windows-latest
+    continue-on-error: true
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
+
+      - name: Build
+        run: cargo build --all-targets --package nickel-lang-*
+
+      - name: Test
+        run: cargo test --package nickel-lang-*
diff --git a/Cargo.lock b/Cargo.lock
index 6a2d9254..6b838fbb 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1774,7 +1774,6 @@ dependencies = [
  "nickel-lang-utils",
  "once_cell",
  "pkg-config",
- "pprof",
  "pretty",
  "pretty_assertions",
  "regex",
@@ -1848,6 +1847,7 @@ dependencies = [
  "codespan",
  "criterion",
  "nickel-lang-core",
+ "pprof",
  "serde",
  "toml",
 ]
diff --git a/core/Cargo.toml b/core/Cargo.toml
index de696370..4c2fa3df 100644
--- a/core/Cargo.toml
+++ b/core/Cargo.toml
@@ -86,8 +86,7 @@ strsim = "0.10.0"
 pretty_assertions.workspace = true
 assert_matches.workspace = true
 criterion.workspace = true
-pprof = { workspace = true, features = ["criterion", "flamegraph"] }
-nickel-lang-utils.workspace = true
+nickel-lang-utils = { workspace = true, features = ["pprof"] }
 similar.workspace = true
 test-generator.workspace = true
 
diff --git a/core/benches/arrays.rs b/core/benches/arrays.rs
index 70d16e8e..9c8d36bf 100644
--- a/core/benches/arrays.rs
+++ b/core/benches/arrays.rs
@@ -1,12 +1,11 @@
 use std::rc::Rc;
 
-use criterion::{criterion_main, Criterion};
+use criterion::criterion_main;
 use nickel_lang_core::term::{
     array::{Array, ArrayAttrs},
     Number, RichTerm, Term,
 };
-use nickel_lang_utils::{bench::EvalMode, ncl_bench_group};
-use pprof::criterion::{Output, PProfProfiler};
+use nickel_lang_utils::{bench::criterion_config, bench::EvalMode, ncl_bench_group};
 use pretty::{BoxAllocator, DocBuilder, Pretty};
 
 /// Generates a pseaudo-random Nickel array as a string.
@@ -35,7 +34,7 @@ fn ncl_random_array(len: usize) -> String {
 
 ncl_bench_group! {
 name = benches;
-config = Criterion::default().with_profiler(PProfProfiler::new(100, Output::Flamegraph(None)));
+config = criterion_config();
 {
         name = "foldr strings 50",
         path = "arrays/fold",
diff --git a/core/benches/functions.rs b/core/benches/functions.rs
index 28cd5f19..3635bb25 100644
--- a/core/benches/functions.rs
+++ b/core/benches/functions.rs
@@ -1,10 +1,9 @@
-use criterion::{criterion_main, Criterion};
-use nickel_lang_utils::ncl_bench_group;
-use pprof::criterion::{Output, PProfProfiler};
+use criterion::criterion_main;
+use nickel_lang_utils::{bench::criterion_config, ncl_bench_group};
 
 ncl_bench_group! {
     name = benches;
-    config = Criterion::default().with_profiler(PProfProfiler::new(100, Output::Flamegraph(None)));
+    config = criterion_config();
     {
         name = "church 3",
         path = "functions/church",
diff --git a/core/benches/mantis.rs b/core/benches/mantis.rs
index 1fff0ef2..636c5b6f 100644
--- a/core/benches/mantis.rs
+++ b/core/benches/mantis.rs
@@ -1,10 +1,9 @@
-use criterion::{criterion_main, Criterion};
-use nickel_lang_utils::{bench::EvalMode, ncl_bench_group};
-use pprof::criterion::{Output, PProfProfiler};
+use criterion::criterion_main;
+use nickel_lang_utils::{bench::criterion_config, bench::EvalMode, ncl_bench_group};
 
 ncl_bench_group! {
     name = benches;
-    config = Criterion::default().with_profiler(PProfProfiler::new(100, Output::Flamegraph(None)));
+    config = criterion_config();
     {
         name = "mantis",
         path = "mantis/run",
diff --git a/core/benches/numeric.rs b/core/benches/numeric.rs
index d413c95e..a72c6900 100644
--- a/core/benches/numeric.rs
+++ b/core/benches/numeric.rs
@@ -1,10 +1,9 @@
-use criterion::{criterion_main, Criterion};
-use nickel_lang_utils::ncl_bench_group;
-use pprof::criterion::{Output, PProfProfiler};
+use criterion::criterion_main;
+use nickel_lang_utils::{bench::criterion_config, ncl_bench_group};
 
 ncl_bench_group! {
     name = benches;
-    config = Criterion::default().with_profiler(PProfProfiler::new(100, Output::Flamegraph(None)));
+    config = criterion_config();
     {
         name = "fibonacci 10",
         path = "numeric/fibonacci",
diff --git a/core/benches/records.rs b/core/benches/records.rs
index d3157d9c..a2edaeab 100644
--- a/core/benches/records.rs
+++ b/core/benches/records.rs
@@ -1,10 +1,9 @@
-use criterion::{criterion_main, Criterion};
-use nickel_lang_utils::{bench::EvalMode, ncl_bench_group};
-use pprof::criterion::{Output, PProfProfiler};
+use criterion::criterion_main;
+use nickel_lang_utils::{bench::criterion_config, bench::EvalMode, ncl_bench_group};
 
 ncl_bench_group! {
     name = benches;
-    config = Criterion::default().with_profiler(PProfProfiler::new(100, Output::Flamegraph(None)));
+    config = criterion_config();
     {
             name = "countLetters",
             path = "records/countLetters",
diff --git a/core/benches/serialization.rs b/core/benches/serialization.rs
index d823b9fa..2c6f26c4 100644
--- a/core/benches/serialization.rs
+++ b/core/benches/serialization.rs
@@ -1,10 +1,9 @@
-use criterion::{criterion_main, Criterion};
-use nickel_lang_utils::ncl_bench_group;
-use pprof::criterion::{Output, PProfProfiler};
+use criterion::criterion_main;
+use nickel_lang_utils::{bench::criterion_config, ncl_bench_group};
 
 ncl_bench_group! {
     name = benches;
-    config = Criterion::default().with_profiler(PProfProfiler::new(100, Output::Flamegraph(None)));
+    config = criterion_config();
     {
         name = "round_trip",
         path = "serialization/main",
diff --git a/core/benches/stdlib.rs b/core/benches/stdlib.rs
index e442199f..c15d4b8f 100644
--- a/core/benches/stdlib.rs
+++ b/core/benches/stdlib.rs
@@ -1,7 +1,7 @@
 use criterion::{criterion_group, criterion_main, Criterion};
-use pprof::criterion::{Output, PProfProfiler};
 
 use nickel_lang_core::cache::{Cache, ErrorTolerance};
+use nickel_lang_utils::bench::criterion_config;
 
 pub fn typecheck_stdlib(c: &mut Criterion) {
     let mut cache = Cache::new(ErrorTolerance::Strict);
@@ -18,7 +18,7 @@ pub fn typecheck_stdlib(c: &mut Criterion) {
 
 criterion_group!(
 name = benches;
-config = Criterion::default().with_profiler(PProfProfiler::new(100, Output::Flamegraph(None)));
+config = criterion_config();
 targets = typecheck_stdlib
 );
 criterion_main!(benches);
diff --git a/core/benches/typecheck-nixpkgs-lib.rs b/core/benches/typecheck-nixpkgs-lib.rs
index ea282109..d7181eb4 100644
--- a/core/benches/typecheck-nixpkgs-lib.rs
+++ b/core/benches/typecheck-nixpkgs-lib.rs
@@ -1,10 +1,9 @@
-use criterion::{criterion_main, Criterion};
-use nickel_lang_utils::{bench::EvalMode, ncl_bench_group};
-use pprof::criterion::{Output, PProfProfiler};
+use criterion::criterion_main;
+use nickel_lang_utils::{bench::criterion_config, bench::EvalMode, ncl_bench_group};
 
 ncl_bench_group! {
     name = benches;
-    config = Criterion::default().with_profiler(PProfProfiler::new(100, Output::Flamegraph(None)));
+    config = criterion_config();
     {
         name = "nixpkgs lists",
         path = "nixpkgs/lists",
diff --git a/core/src/identifier.rs b/core/src/identifier.rs
index d24a5e38..c44a3b74 100644
--- a/core/src/identifier.rs
+++ b/core/src/identifier.rs
@@ -33,6 +33,14 @@ impl Ident {
     pub fn into_label(self) -> String {
         self.label().to_owned()
     }
+
+    /// Create a new fresh identifier. This identifier is unique and is guaranteed not to collide
+    /// with any identifier defined before. Generated identifiers start with a special prefix that
+    /// can't be used by normal, user-defined identifiers.
+    pub fn fresh() -> Self {
+        increment!("Ident::fresh");
+        Self::new(format!("{}{}", GEN_PREFIX, GeneratedCounter::next()))
+    }
 }
 
 impl fmt::Display for Ident {
@@ -122,12 +130,9 @@ impl LocIdent {
         LocIdent { pos, ..self }
     }
 
-    /// Create a new fresh identifier. This identifier is unique and is guaranteed not to collide
-    /// with any identifier defined before. Generated identifiers start with a special prefix that
-    /// can't be used by normal, user-defined identifiers.
+    /// Create a fresh identifier with no position. See [Ident::fresh].
     pub fn fresh() -> Self {
-        increment!("LocIdent::fresh");
-        Self::new(format!("{}{}", GEN_PREFIX, GeneratedCounter::next()))
+        Ident::fresh().into()
     }
 
     /// Return the identifier without its position.
diff --git a/core/src/serialize.rs b/core/src/serialize.rs
index ee147858..16eafe02 100644
--- a/core/src/serialize.rs
+++ b/core/src/serialize.rs
@@ -47,6 +47,8 @@ impl fmt::Display for ExportFormat {
     }
 }
 
+// TODO: This type is publicly exposed, but never constructed.
+#[allow(dead_code)]
 #[derive(Clone, Eq, PartialEq, Debug)]
 pub struct ParseFormatError(String);
 
diff --git a/core/src/stdlib.rs b/core/src/stdlib.rs
index 2b238c5a..e7c77931 100644
--- a/core/src/stdlib.rs
+++ b/core/src/stdlib.rs
@@ -92,6 +92,7 @@ pub mod internals {
     generate_accessor!(record_contract);
     generate_accessor!(record_type);
     generate_accessor!(forall_record_tail);
+    generate_accessor!(forall_record_tail_excluded_only);
     generate_accessor!(dyn_tail);
     generate_accessor!(empty_tail);
 
diff --git a/core/src/typ.rs b/core/src/typ.rs
index 1370272f..1b8318a6 100644
--- a/core/src/typ.rs
+++ b/core/src/typ.rs
@@ -951,6 +951,73 @@ impl EnumRows {
             ty: std::marker::PhantomData,
         }
     }
+
+    /// Simplify enum rows for contract generation when the rows are part of a static type
+    /// annotation. See [Type::contract_static].
+    ///
+    /// The following simplification are applied:
+    ///
+    /// - the type of the argument of each enum variant is simplified as well
+    /// - if the polarity is positive and the rows are composed entirely of enum tags and enum variants whose argument's simplified type is `Dyn`, the entire rows are elided by returning `None`
+    /// - a tail variable in tail position is currently left unchanged, because it doesn't give
+    /// rise to any sealing at runtime currently (see documentation of `$forall_enum_tail` in the
+    /// internals module of the stdlib)
+    fn simplify(
+        self,
+        contract_env: &mut Environment<Ident, RichTerm>,
+        simplify_vars: SimplifyVars,
+        polarity: Polarity,
+    ) -> Option<Self> {
+        // Actual simplification logic. We can elide the initial enum row type if **each**
+        // individual row can be elided and this enum has an empty tail. Thus, when making
+        // recursive calls, we can't just return `None` when some subrows can be elided, as we
+        // might still need them. Instead, `do_simplify` returns a tuple of the simplified rows and
+        // a boolean indicating if this part can be elided.
+        fn do_simplify(
+            rows: EnumRows,
+            contract_env: &mut Environment<Ident, RichTerm>,
+            simplify_vars: SimplifyVars,
+            polarity: Polarity,
+        ) -> (EnumRows, bool) {
+            match rows {
+                EnumRows(EnumRowsF::Empty) => (EnumRows(EnumRowsF::Empty), true),
+                // Currently, we could actually return `true` here, because the tail contract for
+                // enums doesn't do anything (see documentation of `$forall_enum_tail` in the
+                // `internals` module of the stdlib). However, if we ever fix this shortcoming of
+                // enum tail contracts and actually enforce parametricity, returning `true` would
+                // become incorrect. So let's be future proof.
+                EnumRows(EnumRowsF::TailVar(id)) => (EnumRows(EnumRowsF::TailVar(id)), false),
+                EnumRows(EnumRowsF::Extend { row, tail }) => {
+                    let (tail, mut elide) =
+                        do_simplify(*tail, contract_env, simplify_vars.clone(), polarity);
+
+                    let typ = row.typ.map(|mut typ| {
+                        *typ = typ.simplify(contract_env, simplify_vars, polarity);
+                        elide = elide && matches!(typ.typ, TypeF::Dyn);
+                        typ
+                    });
+
+                    let row = EnumRowF { id: row.id, typ };
+
+                    (
+                        EnumRows(EnumRowsF::Extend {
+                            row,
+                            tail: Box::new(tail),
+                        }),
+                        elide,
+                    )
+                }
+            }
+        }
+
+        let (result, elide) = do_simplify(self, contract_env, simplify_vars, polarity);
+
+        if matches!((elide, polarity), (true, Polarity::Positive)) {
+            None
+        } else {
+            Some(result)
+        }
+    }
 }
 
 impl Subcontract for EnumRows {
@@ -1141,6 +1208,233 @@ impl RecordRows {
             ty: std::marker::PhantomData,
         }
     }
+
+    /// Simplify record rows for contract generation when the rows are part of a static type
+    /// annotation. See [Type::contract_static].
+    ///
+    /// The following simplifications are applied:
+    ///
+    /// - the type of each field is simplified
+    /// - if the polarity is positive and the tail is known to be simplified to `Dyn`, any field
+    ///   whose simplified type is `Dyn` is entirely elided from the final result. That is, `{foo :
+    ///   Number, bar : Number -> Number}` in positive position is simplified to `{bar : Number ->
+    ///   Dyn; Dyn}`. `{foo : Number, bar : Dyn}` is simplified to `{; Dyn}` which is simplified
+    ///   further to `Dyn` by [Type::simplify].
+    ///
+    ///   We can't do that when the tail can't be simplified to `Dyn` (this is the case when the
+    ///   tail variable has been introduced by a forall in negative position).
+    /// - The case of a tail variable is a bit more complex and is detailed below.
+    ///
+    /// # Simplification of tail variable
+    ///
+    /// The following paragraphs distinguish between a tail variable (and thus an enclosing record
+    /// type) in positive position and a tail variable in negative position (the polarity of the
+    /// introducing forall is yet another dimension, covered in each paragraph).
+    ///
+    /// ## Negative polarity
+    ///
+    /// The simplification of record row variables is made harder by the presence of excluded
+    /// fields. It's tempting to replace all `r` in tail position by `Dyn` if the introducing
+    /// `forall r` was in positive position, as we do for regular type variables, but it's
+    /// unfortunately not sound. For example:
+    ///
+    /// ```nickel
+    /// inject_meta: forall r. {; r} -> {meta : String; r}
+    /// ```
+    ///
+    /// In this case, the `forall r` is in positive position, but the `r` in `{; r}` in negative
+    /// position can't be entirely elided, because it checks that `meta` isn't already present in
+    /// the original argument. In particular, the original contract rejects `inject_meta {meta =
+    /// "hello"}`, but blindly simplifying the type of `inject_meta` to `{; Dyn} -> {; Dyn}`
+    /// would allow this argument.
+    ///
+    /// We can simplify it to something like `{; $forall_record_tail_excluded_only ["meta"]} -> {;
+    /// Dyn}` (further simplified to `{; $forall_record_tail_excluded_only ["meta"]} -> Dyn` by
+    /// `Type::simplify`). `$forall_record_tail_excluded_only` is a specialized version of the
+    /// record tail contract `$forall_record_tail$ which doesn't seal but still check for the
+    /// absence of excluded fields.
+    ///
+    /// Note that we can't actually put an arbitrary contract in the tail of a record type. This is
+    /// why the `simplify()` methods take a mutable reference to an environment `contract_env`
+    /// which will be passed to the contract generation methods. What we do in practice is to bind
+    /// a fresh record row variable to `$forall_record_tail_excluded_only ["meta"]` in this
+    /// environment and we substitute the tail var for this fresh variable.
+    ///
+    /// On the other hand, in
+    ///
+    /// ```nickel
+    /// update_meta: forall r. {meta : String; r} -> {meta : String; r}
+    /// ```
+    ///
+    /// The contract can be simplified to `{meta : String; Dyn} -> Dyn`. To detect this case, we
+    /// record the set of fields that are present in the current rows and check if this set is
+    /// equal to the excluded fields for this row variable (it's always a subset of the excluded
+    /// fields by definition of row constraints), or if there are some excluded fields left to
+    /// check.
+    ///
+    /// ## Positive polarity
+    ///
+    /// In a positive position, we can replace the tail with `Dyn` if the tail isn't a variable
+    /// introduced in negative position, because a typed term can never violate row constraints.
+    ///
+    /// For a variable introduced by a forall in negative position, we need to keep the unsealing
+    /// operation to make sure the corresponding forall type doesn't blame. But the unsealing
+    /// operation needs prior sealing to work out, so we need to keep the tail even for record
+    /// types in positive position. What's more, _we can't elide any field in this case_. Indeed,
+    /// eliding fields can change what goes in the tail, and can only be done when the tail is
+    /// ensured to be `Dyn`.
+    fn simplify(
+        self,
+        contract_env: &mut Environment<Ident, RichTerm>,
+        simplify_vars: SimplifyVars,
+        polarity: Polarity,
+    ) -> Self {
+        // This helper does a first traversal of record rows in order to peek the tail and check if
+        // it's a variable introduced by a forall in negative position. In this case, the second
+        // component of the result will be `false` and we can't elide any field during the actual
+        // simplification.
+        //
+        // As we will need the set of all fields later, we build during this first traversal as well.
+        fn peek_tail(rrows: &RecordRows, simplify_vars: &SimplifyVars) -> (HashSet<Ident>, bool) {
+            let mut fields = HashSet::new();
+            let mut can_elide = true;
+
+            for row in rrows.iter() {
+                match row {
+                    RecordRowsIteratorItem::Row(row) => {
+                        fields.insert(row.id.ident());
+                    }
+                    RecordRowsIteratorItem::TailVar(id)
+                        if simplify_vars.rrows_vars_elide.get(&id.ident()).is_none() =>
+                    {
+                        can_elide = false;
+                    }
+                    _ => {}
+                }
+            }
+
+            (fields, can_elide)
+        }
+
+        // Actual simplification logic, which additionally remembers if a field has been elided and
+        // if we thus need to change the tail to `Dyn` to account for the elision.
+        fn do_simplify(
+            rrows: RecordRows,
+            contract_env: &mut Environment<Ident, RichTerm>,
+            simplify_vars: SimplifyVars,
+            polarity: Polarity,
+            fields: &HashSet<Ident>,
+            can_elide: bool,
+        ) -> RecordRows {
+            let rrows = match rrows.0 {
+                // Because we may have elided some fields, we always make this record type open
+                // when in positive position, which never hurts
+                RecordRowsF::Empty if matches!(polarity, Polarity::Positive) => {
+                    RecordRowsF::TailDyn
+                }
+                RecordRowsF::Empty => RecordRowsF::Empty,
+                RecordRowsF::Extend { row, tail } => {
+                    let typ_simplified =
+                        row.typ
+                            .simplify(contract_env, simplify_vars.clone(), polarity);
+                    // If we are in a positive position, the simplified type of the field is `Dyn`,
+                    // and we can elide fields given the current tail of these rows, we get rid of
+                    // the whole field.
+                    let elide_field = matches!(
+                        (&typ_simplified.typ, polarity),
+                        (TypeF::Dyn, Polarity::Positive)
+                    ) && can_elide;
+
+                    let row = RecordRow {
+                        id: row.id,
+                        typ: Box::new(typ_simplified),
+                    };
+
+                    let tail = Box::new(do_simplify(
+                        *tail,
+                        contract_env,
+                        simplify_vars,
+                        polarity,
+                        fields,
+                        can_elide,
+                    ));
+
+                    if elide_field {
+                        tail.0
+                    } else {
+                        RecordRowsF::Extend { row, tail }
+                    }
+                }
+                RecordRowsF::TailDyn => RecordRowsF::TailDyn,
+                RecordRowsF::TailVar(id) => {
+                    let excluded = simplify_vars.rrows_vars_elide.get(&id.ident());
+
+                    match (excluded, polarity) {
+                        // If the variable was introduced in positive position, it won't cause any
+                        // (un)sealing. So if we are in positive position as well, we can just get
+                        // rid of the tail
+                        (Some(_), Polarity::Positive) => RecordRowsF::TailDyn,
+                        // If the variable was introduced in negative position, we can't elide the
+                        // unsealing contracts which are in negative position as well, and thus
+                        // neither elide the corresponding sealing contract.
+                        (None, Polarity::Positive | Polarity::Negative) => RecordRowsF::TailVar(id),
+                        // If the variable was introduced by a forall in positive position and we
+                        // are in a negative position, we can do some simplifying and at least get
+                        // rid of the sealing operation, and sometimes of the whole tail contract.
+                        (Some(excluded), Polarity::Negative) => {
+                            // We don't have to check for the absence of fields that appear in this row
+                            // type
+                            let excluded = excluded - fields;
+
+                            // If all the excluded fields are listed in the record type, the
+                            // contract will never blame on the presence of an excluded field, so
+                            // we can get rid of the tail altogether
+                            if excluded.is_empty() {
+                                RecordRowsF::TailDyn
+                            }
+                            // Otherwise, we need to check for the absence of the remaining excluded
+                            // fields with a specialized tail contract which doesn't seal the tail.
+                            else {
+                                let fresh_var = LocIdent::fresh();
+
+                                let excluded_ncl: RichTerm = Term::Array(
+                                    Array::from_iter(
+                                        excluded
+                                            .iter()
+                                            .map(|id| Term::Str(NickelString::from(*id)).into()),
+                                    ),
+                                    Default::default(),
+                                )
+                                .into();
+
+                                contract_env.insert(
+                                    fresh_var.ident(),
+                                    mk_app!(
+                                        internals::forall_record_tail_excluded_only(),
+                                        excluded_ncl
+                                    ),
+                                );
+
+                                RecordRowsF::TailVar(fresh_var)
+                            }
+                        }
+                    }
+                }
+            };
+
+            RecordRows(rrows)
+        }
+
+        let (fields, can_elide) = peek_tail(&self, &simplify_vars);
+        do_simplify(
+            self,
+            contract_env,
+            simplify_vars,
+            polarity,
+            &fields,
+            can_elide,
+        )
+    }
 }
 
 impl Subcontract for RecordRows {
@@ -1228,112 +1522,16 @@ impl Type {
         .unwrap()
     }
 
-    /// Static typing guarantees make some of the contract checks useless, assuming that blame
-    /// safety holds. This function simplifies `self` for contract generation, assuming it is part
-    /// of a static type annotation, by eliding some of these useless subcontracts.
-    ///
-    /// # Simplifications
-    ///
-    /// - `forall`s in positive positions are removed, and the corresponding type variable is
-    ///   substituted for a `Dyn` contract. In consequence, [Self::contract()] will generate
-    ///   optimized contracts as well (for example, `forall a. Array a -> a` becomes `Array Dyn ->
-    ///   Dyn`, where `Array Dyn` will be translated to `$array_dyn` which has a constant-time
-    ///   overhead while `Array a` is linear in the size of the array.
-    /// - All positive occurrences of first order contracts (that is, anything but a function type)
-    /// are turned to `Dyn` contracts.
-    fn optimize_static(self) -> Self {
-        // We use this environment as a shareable HashSet
-        type VarsHashSet = Environment<Ident, ()>;
-
-        trait Optimize {
-            fn optimize(self, vars_elide: VarsHashSet, polarity: Polarity) -> Self;
-        }
-
-        impl Optimize for Type {
-            fn optimize(self, mut vars_elide: VarsHashSet, polarity: Polarity) -> Type {
-                let mut pos = self.pos;
-
-                let optimized = match self.typ {
-                    TypeF::Arrow(dom, codom) => TypeF::Arrow(
-                        Box::new(dom.optimize(vars_elide.clone(), polarity.flip())),
-                        Box::new(codom.optimize(vars_elide, polarity)),
-                    ),
-                    // TODO: don't optimize only VarKind::Type
-                    TypeF::Forall {
-                        var,
-                        var_kind: VarKind::Type,
-                        body,
-                    } if polarity == Polarity::Positive => {
-                        vars_elide.insert(var.ident(), ());
-                        let result = body.optimize(vars_elide, polarity);
-                        // we keep the position of the body, not the one of the forall
-                        pos = result.pos;
-                        result.typ
-                    }
-                    TypeF::Forall {
-                        var,
-                        var_kind,
-                        body,
-                    } => TypeF::Forall {
-                        var,
-                        var_kind,
-                        body: Box::new(body.optimize(vars_elide, polarity)),
-                    },
-                    TypeF::Var(id) if vars_elide.get(&id).is_some() => TypeF::Dyn,
-                    v @ TypeF::Var(_) => v,
-                    // Any first-order type on positive position can be elided
-                    _ if matches!(polarity, Polarity::Positive) => TypeF::Dyn,
-                    // Otherwise, we still recurse into non-primitive types
-                    TypeF::Record(rrows) => TypeF::Record(rrows.optimize(vars_elide, polarity)),
-                    TypeF::Enum(erows) => TypeF::Enum(erows.optimize(vars_elide, polarity)),
-                    TypeF::Dict {
-                        type_fields,
-                        flavour,
-                    } => TypeF::Dict {
-                        type_fields: Box::new(type_fields.optimize(vars_elide, polarity)),
-                        flavour,
-                    },
-                    TypeF::Array(t) => TypeF::Array(Box::new(t.optimize(vars_elide, polarity))),
-                    // All other types don't contain subtypes, it's a base case
-                    t => t,
-                };
-                Type {
-                    typ: optimized,
-                    pos,
-                }
-            }
-        }
-
-        impl Optimize for RecordRows {
-            fn optimize(self, vars_elide: VarsHashSet, polarity: Polarity) -> RecordRows {
-                RecordRows(self.0.map(
-                    |typ| Box::new(typ.optimize(vars_elide.clone(), polarity)),
-                    |rrows| Box::new(rrows.optimize(vars_elide.clone(), polarity)),
-                ))
-            }
-        }
-
-        impl Optimize for EnumRows {
-            fn optimize(self, vars_elide: VarsHashSet, polarity: Polarity) -> EnumRows {
-                EnumRows(self.0.map(
-                    |typ| Box::new(typ.optimize(vars_elide.clone(), polarity)),
-                    |erows| Box::new(erows.optimize(vars_elide.clone(), polarity)),
-                ))
-            }
-        }
-
-        self.optimize(VarsHashSet::new(), Polarity::Positive)
-    }
-
-    /// Return the contract corresponding to a type which appears in a static type annotation. Said
-    /// contract must then be applied using the `ApplyContract` primitive operation.
-    ///
-    /// [Self::contract_static] uses the fact that the checked term has been typechecked to
-    /// optimize the generated contract.
+    /// Variant of [Self::contract] that returns the contract corresponding to a type which appears
+    /// in a static type annotation. [Self::contract_static] uses the fact that the checked term
+    /// has been typechecked to optimize the generated contract thanks to the guarantee of static
+    /// typing.
     pub fn contract_static(self) -> Result<RichTerm, UnboundTypeVariableError> {
         let mut sy = 0;
-        self.optimize_static()
-            .subcontract(Environment::new(), Polarity::Positive, &mut sy)
+        let mut contract_env = Environment::new();
+
+        self.simplify(&mut contract_env, SimplifyVars::new(), Polarity::Positive)
+            .subcontract(contract_env, Polarity::Positive, &mut sy)
     }
 
     /// Return the contract corresponding to a type. Said contract must then be applied using the
@@ -1380,6 +1578,163 @@ impl Type {
             _ => None,
         })
     }
+
+    /// Static typing guarantees make some of the contract checks useless, assuming that blame
+    /// safety holds. This function simplifies `self` for contract generation, assuming it is part
+    /// of a static type annotation, by eliding some of these useless subcontracts.
+    ///
+    /// # Simplifications
+    ///
+    /// - `forall`s of a type variable in positive positions are removed, and the corresponding type
+    ///   variable is substituted for a `Dyn` contract. In consequence, [Self::contract()] will generate
+    ///   simplified contracts as well. For example, `forall a. Array a -> a` becomes `Array Dyn -> Dyn`,
+    ///   and `Array Dyn` will then be specialized to `$array_dyn` which has a constant-time overhead
+    ///   (while `Array a` is linear in the size of the array). The final contract will just check that
+    ///   the argument is an array.
+    /// - `forall`s of a row variable (either record or enum) are removed as well. The substitution of
+    ///   the corresponding row variable is a bit more complex than in the type variable case and depends
+    ///   on the situation. See [RecordRows::simplify] and [EnumRows::simplify] for more details.
+    /// - `forall`s in negative position are left unchanged.
+    /// - All positive occurrences of type constructors that aren't a function type are recursively
+    ///   simplified. If they are simplified to a trivial type, such as `{; Dyn}` for a record or `Array
+    ///   Dyn` for an array, they are further simplified to `Dyn`.
+    ///   are turned to `Dyn` contracts. However, we must be careful here: type constructors might
+    ///   have function types somewhere inside, as in `{foo : Number, bar : Array (String ->
+    ///   String) }`. In this case, we can elide `foo`, but not `bar`.
+    fn simplify(
+        self,
+        contract_env: &mut Environment<Ident, RichTerm>,
+        mut simplify_vars: SimplifyVars,
+        polarity: Polarity,
+    ) -> Self {
+        let mut pos = self.pos;
+
+        let simplified = match self.typ {
+            TypeF::Arrow(dom, codom) => TypeF::Arrow(
+                Box::new(dom.simplify(contract_env, simplify_vars.clone(), polarity.flip())),
+                Box::new(codom.simplify(contract_env, simplify_vars, polarity)),
+            ),
+            TypeF::Forall {
+                var,
+                var_kind: VarKind::Type,
+                body,
+            } if polarity == Polarity::Positive => {
+                // The case of type variables is the simplest: we just replace all of them by
+                // `Dyn`. We don't bother messing with the contract environment and only register
+                // them in `simplify_vars`. Subsequent calls to `simplify` will check the register
+                // and replace the variable by `Dyn` when appropriate.
+                simplify_vars.type_vars_elide.insert(var.ident(), ());
+
+                let result = body.simplify(contract_env, simplify_vars, polarity);
+                // we keep the position of the body, not the one of the forall
+                pos = result.pos;
+                result.typ
+            }
+            TypeF::Forall {
+                var,
+                var_kind: VarKind::RecordRows { excluded },
+                body,
+            } if polarity == Polarity::Positive => {
+                simplify_vars.rrows_vars_elide.insert(var.ident(), excluded);
+
+                let result = body.simplify(contract_env, simplify_vars, polarity);
+                // we keep the position of the body, not the one of the forall
+                pos = result.pos;
+                result.typ
+            }
+            // For enum rows in negative position, we don't any simplification for now because
+            // parametricity isn't enforced. Polymorphic enum row contracts are mostly doing
+            // nothing, and it's fine to keep them as they are. See the documentation of
+            // `$forall_enum_tail` for more details. Even if we do enforce parametricity in the
+            // future, we will be missing an optimization opportunity here but we won't introduce
+            // any unsoundness.
+            //
+            // We don't elide foralls in negative position either.
+            //
+            // In both cases, we still simplify the body of the forall.
+            TypeF::Forall {
+                var,
+                var_kind,
+                body,
+            } => TypeF::Forall {
+                var,
+                var_kind,
+                body: Box::new(body.simplify(contract_env, simplify_vars, polarity)),
+            },
+            TypeF::Var(id) if simplify_vars.type_vars_elide.get(&id).is_some() => TypeF::Dyn,
+            // Any ground type in positive position can be entirely elided
+            TypeF::Number | TypeF::String | TypeF::Bool | TypeF::Symbol | TypeF::ForeignId
+                if matches!(polarity, Polarity::Positive) =>
+            {
+                TypeF::Dyn
+            }
+            // We need to recurse into type constructors, which could contain arrow types inside.
+            TypeF::Record(rrows) => {
+                let rrows_simplified = rrows.simplify(contract_env, simplify_vars, polarity);
+
+                // [^simplify-type-constructor-positive]: if we are in positive position, and the
+                // record type is entirely elided (which means simplified to `{; Dyn}`) or is
+                // empty, we can simplify it further to `Dyn`. This works for other type
+                // constructors as well (arrays, dictionaries, etc.): if there's no negative type
+                // or polymorphic tail somewhere inside, we can get rid of the whole thing.
+                if matches!(
+                    (&rrows_simplified, polarity),
+                    (
+                        RecordRows(RecordRowsF::TailDyn) | RecordRows(RecordRowsF::Empty),
+                        Polarity::Positive
+                    )
+                ) {
+                    TypeF::Dyn
+                } else {
+                    TypeF::Record(rrows_simplified)
+                }
+            }
+            TypeF::Enum(erows) => {
+                let erows = erows.simplify(contract_env, simplify_vars, polarity);
+
+                // See [^simplify-type-constructor-positive]
+                erows.map(TypeF::Enum).unwrap_or(TypeF::Dyn)
+            }
+            TypeF::Dict {
+                type_fields,
+                flavour,
+            } => {
+                let type_fields =
+                    Box::new(type_fields.simplify(contract_env, simplify_vars, polarity));
+
+                // See [^simplify-type-constructor-positive]
+                if matches!(
+                    (&type_fields.typ, polarity),
+                    (TypeF::Dyn, Polarity::Positive)
+                ) {
+                    TypeF::Dyn
+                } else {
+                    TypeF::Dict {
+                        type_fields,
+                        flavour,
+                    }
+                }
+            }
+            TypeF::Array(t) => {
+                let type_elts = t.simplify(contract_env, simplify_vars, polarity);
+
+                // See [^simplify-type-constructor-positive]
+                if matches!((&type_elts.typ, polarity), (TypeF::Dyn, Polarity::Positive)) {
+                    TypeF::Dyn
+                } else {
+                    TypeF::Array(Box::new(type_elts))
+                }
+            }
+            // All the remaining cases are ground types that don't contain subtypes, or they are
+            // type variables that can't be elided. We leave them unchanged
+            t => t,
+        };
+
+        Type {
+            typ: simplified,
+            pos,
+        }
+    }
 }
 
 impl Traverse<Type> for Type {
@@ -1486,6 +1841,25 @@ impl Traverse<RichTerm> for Type {
     }
 }
 
+/// Some context storing various type variables that can be simplified during static contract
+/// simplification (see the various `simplify()` methods).
+#[derive(Clone, Debug, Default)]
+struct SimplifyVars {
+    /// Environment used as a persistent HashSet to record type variables that can be elided
+    /// (replaced by `Dyn`) because they were introduced by a forall in positive position.
+    type_vars_elide: Environment<Ident, ()>,
+    /// Record record rows variables that were introduced by a forall in positive position and
+    /// their corresponding `excluded` field. They will be substituted for different simplified
+    /// contracts depending on where the variable appears and the surrounding record.
+    rrows_vars_elide: Environment<Ident, HashSet<Ident>>,
+}
+
+impl SimplifyVars {
+    fn new() -> Self {
+        Self::default()
+    }
+}
+
 impl_display_from_pretty!(Type);
 impl_display_from_pretty!(EnumRow);
 impl_display_from_pretty!(EnumRows);
@@ -1493,3 +1867,108 @@ impl_display_from_pretty!(RecordRow);
 impl_display_from_pretty!(RecordRows);
 
 impl PrettyPrintCap for Type {}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::parser::{grammar::FixedTypeParser, lexer::Lexer, ErrorTolerantParser};
+
+    /// Parse a type represented as a string.
+    fn parse_type(s: &str) -> Type {
+        use codespan::Files;
+        let id = Files::new().add("<test>", s);
+
+        FixedTypeParser::new()
+            .parse_strict(id, Lexer::new(s))
+            .unwrap()
+    }
+
+    /// Parse a type, simplify it and assert that the result corresponds to the second argument
+    /// (which is parsed and printed again to eliminate formatting differences). This function also
+    /// checks that the contract generation from the simplified version works without an unbound
+    /// type variable error.
+    #[track_caller]
+    fn assert_simplifies_to(orig: &str, target: &str) {
+        let parsed = parse_type(orig);
+
+        parsed.clone().contract_static().unwrap();
+
+        let simplified = parsed.simplify(
+            &mut Environment::new(),
+            SimplifyVars::new(),
+            Polarity::Positive,
+        );
+        let target_typ = parse_type(target);
+
+        assert_eq!(format!("{simplified}"), format!("{target_typ}"));
+    }
+
+    #[test]
+    fn simplify() {
+        assert_simplifies_to("forall a. a -> (a -> a) -> a", "Dyn -> (Dyn -> Dyn) -> Dyn");
+        assert_simplifies_to(
+            "forall b. (forall a. a -> a) -> b",
+            "(forall a. a -> a) -> Dyn",
+        );
+
+        // Big but entirely positive type
+        assert_simplifies_to(
+            "{foo : Array {bar : String, baz : Number}, qux: [| 'Foo, 'Bar, 'Baz Dyn |], pweep: {single : Array Bool}}",
+            "Dyn"
+        );
+        // Mixed type with arrows inside the return value
+        assert_simplifies_to(
+            "Array Number -> Array {foo : Number,  bar : String -> String}",
+            "Array Number -> Array {bar: String -> Dyn; Dyn}",
+        );
+        // Enum with arrows inside
+        assert_simplifies_to(
+            "{single : Array [| 'Foo, 'Bar, 'Baz (Dyn -> Dyn) |] }",
+            "{single : Array [| 'Foo, 'Bar, 'Baz (Dyn -> Dyn) |]; Dyn}",
+        );
+
+        // Polymorphic rows, case without excluded fields to check
+        assert_simplifies_to(
+            "forall r. {meta : String, doc : String; r} -> {meta : String; r}",
+            "{meta : String, doc : String; Dyn} -> Dyn",
+        );
+        // Polymorphic rows in negative position should prevent row elision in positive position
+        assert_simplifies_to(
+            "(forall r. {meta : String, count: Number; r} -> {; r}) -> {meta : String, count: Number}",
+            "(forall r. {meta : Dyn, count : Dyn; r} -> {; r}) -> Dyn",
+        );
+    }
+
+    #[test]
+    fn simplify_dont_elide_record() {
+        use regex::Regex;
+        // The simplified version of the type should contain a generated variable here. We can't
+        // represent a generated variable in normal Nickel syntax, so instead of parsing the
+        // expected result and print it again to eliminate formatting details as in
+        // `assert_simplifies_to`, we will print the simplified version and do a direct string
+        // comparison on the result.
+        let orig = "forall r. {x: Number, y: String; r} -> {z: Array Bool; r}";
+
+        let mut contract_env = Environment::new();
+        let simplified = parse_type(orig)
+            .simplify(&mut contract_env, SimplifyVars::new(), Polarity::Positive)
+            .to_string();
+
+        // Note: because we match on strings directly, we must get the formatting right.
+        let expected = Regex::new(r"\{ x : Number, y : String; (%\d+) \} -> Dyn").unwrap();
+        let caps = expected.captures(&simplified).unwrap();
+
+        // We should have the generated variable in the contract environment bound to
+        // `$forall_enum_tail_excluded_only ["z"]`. Indeed, `x`, `y` and `z` are excluded fields
+        // for the row variable `r`. Because `forall r` is in positive position, we remove the
+        // forall. `{x: Number, y: String; r}` is in negative position, so we still need to check
+        // for excluded fields, but `x` and `y` are already taken care of in the body of the record
+        // type. It only remains to check that `z` isn't present in the input record.
+        let expected_var = Ident::from(caps.get(1).unwrap().as_str());
+
+        assert_eq!(
+            contract_env.get(&expected_var).unwrap().to_string(),
+            "$forall_record_tail_excluded_only [ \"z\" ]"
+        );
+    }
+}
diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs
index a003386d..72918472 100644
--- a/core/src/typecheck/mod.rs
+++ b/core/src/typecheck/mod.rs
@@ -81,6 +81,7 @@ pub mod reporting;
 #[macro_use]
 pub mod mk_uniftype;
 pub mod eq;
+pub mod subtyping;
 pub mod unif;
 
 use eq::{SimpleTermEnvironment, TermEnvironment};
@@ -90,6 +91,8 @@ use operation::{get_bop_type, get_nop_type, get_uop_type};
 use pattern::{PatternTypeData, PatternTypes};
 use unif::*;
 
+use self::subtyping::SubsumedBy;
+
 /// The max depth parameter used to limit the work performed when inferring the type of the stdlib.
 const INFER_RECORD_MAX_DEPTH: u8 = 4;
 
@@ -2166,8 +2169,9 @@ fn check<V: TypecheckVisitor>(
         | Term::Annotated(..) => {
             let inferred = infer(state, ctxt.clone(), visitor, rt)?;
 
-            // We call to `subsumption` to perform the switch from infer mode to checking mode.
-            subsumption(state, ctxt, inferred, ty)
+            // We apply the subsumption rule when switching from infer mode to checking mode.
+            inferred
+                .subsumed_by(ty, state, ctxt)
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Enum(id) => {
@@ -2363,102 +2367,6 @@ fn check<V: TypecheckVisitor>(
     }
 }
 
-/// Change from inference mode to checking mode, and apply a potential subsumption rule.
-///
-/// Currently, there is record/dictionary subtyping, if we are not in this case we fallback to perform
-/// polymorphic type instantiation with unification variable on the left (on the inferred type),
-/// and then simply performs unification (put differently, the subtyping relation when it is not
-/// a record/dictionary subtyping is the equality
-/// relation).
-///
-/// The type instantiation corresponds to the zero-ary case of application in the current
-/// specification (which is based on [A Quick Look at Impredicativity][quick-look], although we
-/// currently don't support impredicative polymorphism).
-///
-/// In the future, this function might implement a other non-trivial subsumption rule.
-///
-/// [quick-look]: https://www.microsoft.com/en-us/research/uploads/prod/2020/01/quick-look-icfp20-fixed.pdf
-pub fn subsumption(
-    state: &mut State,
-    mut ctxt: Context,
-    inferred: UnifType,
-    checked: UnifType,
-) -> Result<(), UnifError> {
-    let inferred_inst = instantiate_foralls(state, &mut ctxt, inferred, ForallInst::UnifVar);
-    let checked = checked.into_root(state.table);
-    match (inferred_inst, checked) {
-        (
-            UnifType::Concrete {
-                typ: TypeF::Record(rrows),
-                ..
-            },
-            UnifType::Concrete {
-                typ:
-                    TypeF::Dict {
-                        type_fields,
-                        flavour,
-                    },
-                var_levels_data,
-            },
-        ) => {
-            for row in rrows.iter() {
-                match row {
-                    GenericUnifRecordRowsIteratorItem::Row(a) => {
-                        subsumption(state, ctxt.clone(), a.typ.clone(), *type_fields.clone())?
-                    }
-                    GenericUnifRecordRowsIteratorItem::TailUnifVar { id, .. } =>
-                    // We don't need to perform any variable level checks when unifying a free
-                    // unification variable with a ground type
-                    // We close the tail because there is no garanty that
-                    // { a : Number, b : Number, _ : a?} <= { _ : Number}
-                    {
-                        state
-                            .table
-                            .assign_rrows(id, UnifRecordRows::concrete(RecordRowsF::Empty))
-                    }
-                    GenericUnifRecordRowsIteratorItem::TailConstant(id) => {
-                        let checked = UnifType::Concrete {
-                            typ: TypeF::Dict {
-                                type_fields: type_fields.clone(),
-                                flavour,
-                            },
-                            var_levels_data,
-                        };
-                        Err(UnifError::WithConst {
-                            var_kind: VarKindDiscriminant::RecordRows,
-                            expected_const_id: id,
-                            inferred: checked,
-                        })?
-                    }
-                    _ => (),
-                }
-            }
-            Ok(())
-        }
-        (
-            UnifType::Concrete {
-                typ: TypeF::Array(a),
-                ..
-            },
-            UnifType::Concrete {
-                typ: TypeF::Array(b),
-                ..
-            },
-        )
-        | (
-            UnifType::Concrete {
-                typ: TypeF::Dict { type_fields: a, .. },
-                ..
-            },
-            UnifType::Concrete {
-                typ: TypeF::Dict { type_fields: b, .. },
-                ..
-            },
-        ) => subsumption(state, ctxt.clone(), *a, *b),
-        (inferred_inst, checked) => checked.unify(inferred_inst, state, &ctxt),
-    }
-}
-
 fn check_field<V: TypecheckVisitor>(
     state: &mut State,
     ctxt: Context,
@@ -2489,7 +2397,9 @@ fn check_field<V: TypecheckVisitor>(
             field.value.as_ref(),
         )?;
 
-        subsumption(state, ctxt, inferred, ty).map_err(|err| err.into_typecheck_err(state, pos))
+        inferred
+            .subsumed_by(ty, state, ctxt)
+            .map_err(|err| err.into_typecheck_err(state, pos))
     }
 }
 
@@ -2573,10 +2483,6 @@ fn infer_with_annot<V: TypecheckVisitor>(
         // An empty value is a record field without definition. We don't check anything, and infer
         // its type to be either the first annotation defined if any, or `Dyn` otherwise.
         // We can only hit this case for record fields.
-        //
-        // TODO: we might have something to do with the visitor to clear the current metadata. It
-        // looks like it may be unduly attached to the next field definition, which is not
-        // critical, but still a bug.
         _ => {
             let inferred = annot
                 .first()
diff --git a/core/src/typecheck/subtyping.rs b/core/src/typecheck/subtyping.rs
new file mode 100644
index 00000000..bbcaa866
--- /dev/null
+++ b/core/src/typecheck/subtyping.rs
@@ -0,0 +1,254 @@
+//! Type subsumption (subtyping)
+//!
+//! Subtyping is a relation between types that allows a value of one type to be used at a place
+//! where another type is expected, because the value's actual type is subsumed by the expected
+//! type.
+//!
+//! The subsumption rule is applied when from inference mode to checking mode, as customary in
+//! bidirectional type checking.
+//!
+//! Currently, there is one core subtyping axiom:
+//!
+//! - Record / Dictionary : `{a1 : T1,...,an : Tn} <: {_ : U}` if for every n `Tn <: U`
+//!
+//! The subtyping relation is extended to a congruence on other type constructors in the obvious
+//! way:
+//!
+//! - `Array T <: Array U` if `T <: U`
+//! - `{_ : T} <: {_ : U}` if `T <: U`
+//! - `{a1 : T1,...,an : Tn} <: {b1 : U1,...,bn : Un}` if for every n `Tn <: Un`
+//!
+//! In all other cases, we fallback to unification (although we instantiate polymorphic types as
+//! needed before). That is, we try to apply reflexivity: `T <: U` if `T = U`.
+//!
+//! The type instantiation corresponds to the zero-ary case of application in the current
+//! specification (which is based on [A Quick Look at Impredicativity][quick-look], although we
+//! currently don't support impredicative polymorphism).
+//!
+//! [quick-look]: https://www.microsoft.com/en-us/research/uploads/prod/2020/01/quick-look-icfp20-fixed.pdf
+use super::*;
+
+pub(super) trait SubsumedBy {
+    type Error;
+
+    /// Checks if `self` is subsumed by `t2`, that is if `self <: t2`. Returns an error otherwise.
+    fn subsumed_by(self, t2: Self, state: &mut State, ctxt: Context) -> Result<(), Self::Error>;
+}
+
+impl SubsumedBy for UnifType {
+    type Error = UnifError;
+
+    fn subsumed_by(
+        self,
+        t2: Self,
+        state: &mut State,
+        mut ctxt: Context,
+    ) -> Result<(), Self::Error> {
+        let inferred = instantiate_foralls(state, &mut ctxt, self, ForallInst::UnifVar);
+        let checked = t2.into_root(state.table);
+
+        match (inferred, checked) {
+            // {a1 : T1,...,an : Tn} <: {_ : U} if for every n `Tn <: U`
+            (
+                UnifType::Concrete {
+                    typ: TypeF::Record(rrows),
+                    ..
+                },
+                UnifType::Concrete {
+                    typ:
+                        TypeF::Dict {
+                            type_fields,
+                            flavour,
+                        },
+                    var_levels_data,
+                },
+            ) => {
+                for row in rrows.iter() {
+                    match row {
+                        GenericUnifRecordRowsIteratorItem::Row(a) => {
+                            a.typ
+                                .clone()
+                                .subsumed_by(*type_fields.clone(), state, ctxt.clone())?
+                        }
+                        GenericUnifRecordRowsIteratorItem::TailUnifVar { id, .. } =>
+                        // We don't need to perform any variable level checks when unifying a free
+                        // unification variable with a ground type
+                        // We close the tail because there is no guarantee that
+                        // { a : Number, b : Number, _ : a?} <= { _ : Number}
+                        {
+                            state
+                                .table
+                                .assign_rrows(id, UnifRecordRows::concrete(RecordRowsF::Empty))
+                        }
+                        GenericUnifRecordRowsIteratorItem::TailConstant(id) => {
+                            let checked = UnifType::Concrete {
+                                typ: TypeF::Dict {
+                                    type_fields: type_fields.clone(),
+                                    flavour,
+                                },
+                                var_levels_data,
+                            };
+                            Err(UnifError::WithConst {
+                                var_kind: VarKindDiscriminant::RecordRows,
+                                expected_const_id: id,
+                                inferred: checked,
+                            })?
+                        }
+                        _ => (),
+                    }
+                }
+                Ok(())
+            }
+            // Array T <: Array U if T <: U
+            (
+                UnifType::Concrete {
+                    typ: TypeF::Array(a),
+                    ..
+                },
+                UnifType::Concrete {
+                    typ: TypeF::Array(b),
+                    ..
+                },
+            )
+            // Dict T <: Dict U if T <: U
+            | (
+                UnifType::Concrete {
+                    typ: TypeF::Dict { type_fields: a, .. },
+                    ..
+                },
+                UnifType::Concrete {
+                    typ: TypeF::Dict { type_fields: b, .. },
+                    ..
+                },
+            ) => a.subsumed_by(*b, state, ctxt),
+            // {a1 : T1,...,an : Tn} <: {b1 : U1,...,bn : Un} if for every n `Tn <: Un`
+            (
+                UnifType::Concrete {
+                    typ: TypeF::Record(rrows1),
+                    ..
+                },
+                UnifType::Concrete {
+                    typ: TypeF::Record(rrows2),
+                    ..
+                },
+            ) => rrows1
+                .clone()
+                .subsumed_by(rrows2.clone(), state, ctxt)
+                .map_err(|err| err.into_unif_err(mk_uty_record!(;rrows2), mk_uty_record!(;rrows1))),
+            // T <: U if T = U
+            (inferred, checked) => checked.unify(inferred, state, &ctxt),
+        }
+    }
+}
+
+impl SubsumedBy for UnifRecordRows {
+    type Error = RowUnifError;
+
+    fn subsumed_by(self, t2: Self, state: &mut State, ctxt: Context) -> Result<(), Self::Error> {
+        // This code is almost taken verbatim fro `unify`, but where some recursive calls are
+        // changed to be `subsumed_by` instead of `unify`. We can surely factorize both into a
+        // generic function, but this is left for future work.
+        let inferred = self.into_root(state.table);
+        let checked = t2.into_root(state.table);
+
+        match (inferred, checked) {
+            (
+                UnifRecordRows::Concrete { rrows: rrows1, .. },
+                UnifRecordRows::Concrete {
+                    rrows: rrows2,
+                    var_levels_data: levels2,
+                },
+            ) => match (rrows1, rrows2) {
+                (RecordRowsF::Extend { row, tail }, rrows2 @ RecordRowsF::Extend { .. }) => {
+                    let urrows2 = UnifRecordRows::Concrete {
+                        rrows: rrows2,
+                        var_levels_data: levels2,
+                    };
+                    let (ty_res, urrows_without_ty_res) = urrows2
+                        .remove_row(&row.id, &row.typ, state, ctxt.var_level)
+                        .map_err(|err| match err {
+                            RemoveRowError::Missing => RowUnifError::MissingRow(row.id),
+                            RemoveRowError::Conflict => {
+                                RowUnifError::RecordRowConflict(row.clone())
+                            }
+                        })?;
+                    if let RemoveRowResult::Extracted(ty) = ty_res {
+                        row.typ
+                            .subsumed_by(ty, state, ctxt.clone())
+                            .map_err(|err| RowUnifError::RecordRowMismatch {
+                                id: row.id,
+                                cause: Box::new(err),
+                            })?;
+                    }
+                    tail.subsumed_by(urrows_without_ty_res, state, ctxt)
+                }
+                (RecordRowsF::TailVar(id), _) | (_, RecordRowsF::TailVar(id)) => {
+                    Err(RowUnifError::UnboundTypeVariable(id))
+                }
+                (RecordRowsF::Empty, RecordRowsF::Empty)
+                | (RecordRowsF::TailDyn, RecordRowsF::TailDyn) => Ok(()),
+                (RecordRowsF::Empty, RecordRowsF::TailDyn)
+                | (RecordRowsF::TailDyn, RecordRowsF::Empty) => Err(RowUnifError::ExtraDynTail),
+                (
+                    RecordRowsF::Empty,
+                    RecordRowsF::Extend {
+                        row: UnifRecordRow { id, .. },
+                        ..
+                    },
+                )
+                | (
+                    RecordRowsF::TailDyn,
+                    RecordRowsF::Extend {
+                        row: UnifRecordRow { id, .. },
+                        ..
+                    },
+                ) => Err(RowUnifError::MissingRow(id)),
+                (
+                    RecordRowsF::Extend {
+                        row: UnifRecordRow { id, .. },
+                        ..
+                    },
+                    RecordRowsF::TailDyn,
+                )
+                | (
+                    RecordRowsF::Extend {
+                        row: UnifRecordRow { id, .. },
+                        ..
+                    },
+                    RecordRowsF::Empty,
+                ) => Err(RowUnifError::ExtraRow(id)),
+            },
+            (UnifRecordRows::UnifVar { id, .. }, urrows)
+            | (urrows, UnifRecordRows::UnifVar { id, .. }) => {
+                if let UnifRecordRows::Constant(cst_id) = urrows {
+                    let constant_level = state.table.get_rrows_level(cst_id);
+                    state.table.force_rrows_updates(constant_level);
+                    if state.table.get_rrows_level(id) < constant_level {
+                        return Err(RowUnifError::VarLevelMismatch {
+                            constant_id: cst_id,
+                            var_kind: VarKindDiscriminant::RecordRows,
+                        });
+                    }
+                }
+                urrows.propagate_constrs(state.constr, id)?;
+                state.table.assign_rrows(id, urrows);
+                Ok(())
+            }
+            (UnifRecordRows::Constant(i1), UnifRecordRows::Constant(i2)) if i1 == i2 => Ok(()),
+            (UnifRecordRows::Constant(i1), UnifRecordRows::Constant(i2)) => {
+                Err(RowUnifError::ConstMismatch {
+                    var_kind: VarKindDiscriminant::RecordRows,
+                    expected_const_id: i2,
+                    inferred_const_id: i1,
+                })
+            }
+            (urrows, UnifRecordRows::Constant(i)) | (UnifRecordRows::Constant(i), urrows) => {
+                Err(RowUnifError::WithConst {
+                    var_kind: VarKindDiscriminant::RecordRows,
+                    expected_const_id: i,
+                    inferred: UnifType::concrete(TypeF::Record(urrows)),
+                })
+            }
+        }
+    }
+}
diff --git a/core/src/typecheck/unif.rs b/core/src/typecheck/unif.rs
index 2ec4cb6f..627ea06a 100644
--- a/core/src/typecheck/unif.rs
+++ b/core/src/typecheck/unif.rs
@@ -1043,7 +1043,7 @@ impl UnifTable {
 /// the map to be rather sparse, we use a `HashMap` instead of a `Vec`.
 pub type RowConstrs = HashMap<VarId, HashSet<Ident>>;
 
-trait PropagateConstrs {
+pub(super) trait PropagateConstrs {
     /// Check that unifying a variable with a type doesn't violate rows constraints, and update the
     /// row constraints of the unified type accordingly if needed.
     ///
@@ -1599,7 +1599,7 @@ impl Unify for UnifRecordRows {
 }
 
 #[derive(Clone, Copy, Debug)]
-enum RemoveRowError {
+pub(super) enum RemoveRowError {
     // The row to add was missing and the row type was closed (no free unification variable in tail
     // position).
     Missing,
@@ -1613,7 +1613,7 @@ pub enum RemoveRowResult<RowContent: Clone> {
     Extended,
 }
 
-trait RemoveRow: Sized {
+pub(super) trait RemoveRow: Sized {
     /// The row data minus the identifier.
     type RowContent: Clone;
 
diff --git a/core/stdlib/internals.ncl b/core/stdlib/internals.ncl
index 280aa6f1..56d0f60f 100644
--- a/core/stdlib/internals.ncl
+++ b/core/stdlib/internals.ncl
@@ -375,6 +375,30 @@
             extra_fields
         ),
 
+  # Specialized version of `$forall_record_tail` for a `forall` introduced in a
+  # positive position and a tail in a negative position which only checks for
+  # excluded fields but doesn't seal the tail. This version is used by the
+  # contract simplifier, when optimizing contracts coming from a static type
+  # annotation.
+  "$forall_record_tail_excluded_only" = fun constr extra_fields label value =>
+    let plural = fun list => if %array/length% list == 1 then "" else "s" in
+
+    # Conflicts happen because a polymorphic record tail might have additional
+    # constraints as to what can actually be in there. See the documentation
+    # of the typechecker for more information.
+    let conflicts =
+      std.array.filter
+        (fun field => std.array.elem field constr)
+        (%record/fields% extra_fields)
+    in
+
+    if conflicts != [] then
+      'Error {
+        message = "field%{plural conflicts} not allowed in tail: `%{std.string.join ", " conflicts}`",
+      }
+    else
+      'Ok value,
+
   # Tail wrapper for a dynamic tail. A dynamic tail doesn't seal anything, so we
   # just add the extra fields back to the returned value. See
   # `$record_type/delayed`.
diff --git a/doc/manual/typing.md b/doc/manual/typing.md
index 68894b21..b964e2c4 100644
--- a/doc/manual/typing.md
+++ b/doc/manual/typing.md
@@ -330,6 +330,24 @@ Subtyping extends to type constructors in the following way:
 
   Here, `{_ : {a : Number}}` is accepted where `{_ : {_ : Number}}` is expected,
   because `{a : Number} <: { _ : Number }`.
+- **Record**: `{a1 : T1, ..., an : Tn} <: {a1 : U1, ..., an : Un}` if for each
+  `i`, `Ti <: Ui`
+
+  Example:
+
+  ```nickel
+  let block : _ =
+    let record_of_records : {a: {b : Number}} = {a = {b = 5}} in
+    let inject_c_in_a : {a : {_ : Number}} -> {a : {_ : Number}}
+      = fun x => {a = std.record.insert "c" 5 (std.record.get "a" x)}
+    in
+
+    inject_c_in_a record_of_records in
+  block
+  ```
+
+  Here, `{a : {b : Number}}` is accepted where `{a : {_ : Number}}` is expected,
+  because `{b : Number} <: { _ : Number }`.
 
 **Remark**: if you've used languages with subtyping before, you might expect the
 presence of a rule for function types, namely that `T -> U <: S -> V` if `S <:
diff --git a/lsp/lsp-harness/src/lib.rs b/lsp/lsp-harness/src/lib.rs
index 5c99a57f..3e70f351 100644
--- a/lsp/lsp-harness/src/lib.rs
+++ b/lsp/lsp-harness/src/lib.rs
@@ -5,7 +5,6 @@ use std::collections::{hash_map::Entry, HashMap};
 
 use assert_cmd::prelude::CommandCargoExt;
 pub use jsonrpc::Server;
-use log::error;
 use lsp_types::{
     notification::{Notification, PublishDiagnostics},
     request::{
@@ -57,23 +56,94 @@ pub struct Requests {
     diagnostic: Option<Vec<Url>>,
 }
 
+/// Produce an absolute filepath `Url` that is safe to use in tests.
+///
+/// The `C:\` prefix on Windows is needed both to avoid `Url::from_file_path` failing due to a
+/// missing drive letter and to avoid invalid filepath errors.
+pub fn file_url_from_path(path: &str) -> Result<Url, String> {
+    assert!(path.starts_with('/'));
+
+    let path = if cfg!(unix) {
+        path.to_owned()
+    } else {
+        format!("C:\\{}", &path[1..])
+    };
+
+    Url::from_file_path(&path).map_err(|()| format!("Unable to convert filepath {path:?} into Url"))
+}
+
+#[cfg(windows)]
+fn modify_requests_uris(mut reqs: Requests) -> Requests {
+    match reqs.request.iter_mut().next() {
+        None => {}
+        Some(rs) => {
+            for req in rs.iter_mut() {
+                modify_request_uri(req);
+            }
+        }
+    }
+    match reqs.diagnostic.iter_mut().next() {
+        None => {}
+        Some(urls) => {
+            for url in urls.iter_mut() {
+                *url = file_url_from_path(url.path()).unwrap();
+            }
+        }
+    };
+    reqs
+}
+
+#[cfg(windows)]
+fn modify_request_uri(req: &mut Request) {
+    fn file_url(url: &Url) -> Url {
+        file_url_from_path(url.path()).unwrap()
+    }
+
+    match req {
+        Request::GotoDefinition(params) => {
+            params.text_document_position_params.text_document.uri =
+                file_url(&params.text_document_position_params.text_document.uri);
+        }
+        Request::References(params) => {
+            params.text_document_position.text_document.uri =
+                file_url(&params.text_document_position.text_document.uri);
+        }
+        Request::Completion(params) => {
+            params.text_document_position.text_document.uri =
+                file_url(&params.text_document_position.text_document.uri);
+        }
+        Request::Formatting(params) => {
+            params.text_document.uri = file_url(&params.text_document.uri);
+        }
+        Request::Hover(params) => {
+            params.text_document_position_params.text_document.uri =
+                file_url(&params.text_document_position_params.text_document.uri);
+        }
+        Request::Rename(params) => {
+            params.text_document_position.text_document.uri =
+                file_url(&params.text_document_position.text_document.uri);
+        }
+        Request::Symbols(params) => {
+            params.text_document.uri = file_url(&params.text_document.uri);
+        }
+    }
+}
+
 impl TestFixture {
-    pub fn parse(s: &str) -> Option<Self> {
+    pub fn parse(s: &str) -> Result<Self, String> {
         let mut header_lines = Vec::new();
         let mut content = String::new();
         let mut files = Vec::new();
         let mut push_file = |header: &[&str], content: &mut String| {
-            if header.len() > 1 {
-                error!("files can only have 1 header line");
-                return None;
-            }
-
-            let uri = Url::from_file_path(header.first()?).ok()?;
+            let uri = match header {
+                &[path] => file_url_from_path(path),
+                _ => Err(format!("Files can only have 1 header line: {header:?}")),
+            }?;
             files.push(TestFile {
                 uri,
                 contents: std::mem::take(content),
             });
-            Some(())
+            Ok::<(), String>(())
         };
 
         for line in s.lines() {
@@ -94,7 +164,7 @@ impl TestFixture {
             // The text fixture ended with a nickel file; there are no lsp
             // requests specified.
             push_file(&header_lines, &mut content)?;
-            Some(TestFixture {
+            Ok(TestFixture {
                 files,
                 reqs: Vec::new(),
                 expected_diags: Vec::new(),
@@ -105,7 +175,10 @@ impl TestFixture {
             // we expect to receive.
             let remaining = header_lines.join("\n");
             let reqs: Requests = toml::from_str(&remaining).unwrap();
-            Some(TestFixture {
+            #[cfg(windows)]
+            let reqs = modify_requests_uris(reqs);
+
+            Ok(TestFixture {
                 files,
                 reqs: reqs.request.unwrap_or_default(),
                 expected_diags: reqs.diagnostic.unwrap_or_default(),
diff --git a/lsp/nls/Cargo.toml b/lsp/nls/Cargo.toml
index 8ddee0d9..62a7bafd 100644
--- a/lsp/nls/Cargo.toml
+++ b/lsp/nls/Cargo.toml
@@ -58,7 +58,7 @@ assert_cmd.workspace = true
 assert_matches.workspace = true
 criterion.workspace = true
 glob = "0.3.1"
-insta.workspace = true
+insta = { workspace = true, features = ["filters"] }
 lsp-harness.workspace = true
 nickel-lang-utils.workspace = true
 pretty_assertions.workspace = true
diff --git a/lsp/nls/benches/main.rs b/lsp/nls/benches/main.rs
index 87bc67ae..21bb147d 100644
--- a/lsp/nls/benches/main.rs
+++ b/lsp/nls/benches/main.rs
@@ -53,7 +53,8 @@ fn test_requests(c: &mut Criterion) {
 fn benchmark_one_test(c: &mut Criterion, path: &str) {
     let full_path = project_root().join(path);
     let contents = std::fs::read_to_string(&full_path).unwrap();
-    let fixture = TestFixture::parse(&contents).unwrap();
+    let fixture =
+        TestFixture::parse(&contents).unwrap_or_else(|s| panic!("Failed parsing {path:?}: {s}"));
     let mut harness = TestHarness::new();
 
     harness.prepare_files(&fixture);
diff --git a/lsp/vscode-extension/yarn.lock b/lsp/vscode-extension/yarn.lock
index 8e8bd1e9..da0eacae 100644
--- a/lsp/vscode-extension/yarn.lock
+++ b/lsp/vscode-extension/yarn.lock
@@ -482,7 +482,7 @@ brace-expansion@^2.0.1:
   dependencies:
     balanced-match "^1.0.0"
 
-braces@^3.0.2, braces@~3.0.2:
+braces@^3.0.3, braces@~3.0.2:
   version "3.0.3"
   resolved "https://registry.yarnpkg.com/braces/-/braces-3.0.3.tgz#490332f40919452272d55a8480adc0c441358789"
   integrity sha512-yQbXgO/OSZVD2IsiLlro+7Hf6Q18EJrKSEsdoMzKePKXct3gvD8oLcOQdIzGupr5Fj+EDe8gO/lxc1BzfMpxvA==
@@ -1443,11 +1443,11 @@ merge2@^1.3.0, merge2@^1.4.1:
   integrity sha512-8q7VEgMJW4J8tcfVPy8g09NcQwZdbwFEqhe/WZkoIzjn/3TGDwtOCYtXGxA3O8tPzpczCCDgv+P2P5y00ZJOOg==
 
 micromatch@^4.0.4:
-  version "4.0.5"
-  resolved "https://registry.yarnpkg.com/micromatch/-/micromatch-4.0.5.tgz#bc8999a7cbbf77cdc89f132f6e467051b49090c6"
-  integrity sha512-DMy+ERcEW2q8Z2Po+WNXuw3c5YaUSFjAO5GsJqfEl7UjvtIuFKO6ZrKvcItdy98dwFI2N1tg3zNIdKaQT+aNdA==
+  version "4.0.8"
+  resolved "https://registry.yarnpkg.com/micromatch/-/micromatch-4.0.8.tgz#d66fa18f3a47076789320b9b1af32bd86d9fa202"
+  integrity sha512-PXwfBhYu0hBCPw8Dn0E+WDYb7af3dSLVWKi3HGv84IdF4TyFoC0ysxFd0Goxw7nSv4T/PzEJQxsYsEiFCKo2BA==
   dependencies:
-    braces "^3.0.2"
+    braces "^3.0.3"
     picomatch "^2.3.1"
 
 mime@^1.3.4:
diff --git a/utils/Cargo.toml b/utils/Cargo.toml
index 299881dd..a9e30bc4 100644
--- a/utils/Cargo.toml
+++ b/utils/Cargo.toml
@@ -13,9 +13,15 @@ repository.workspace = true
 bench = false
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
+[features]
+pprof = ["dep:pprof"]
+
 [dependencies]
 nickel-lang-core.workspace = true
 criterion.workspace = true
 codespan.workspace = true
 serde = { workspace = true, features = ["derive"] }
 toml = { workspace = true, features = ["parse"] }
+
+[target.'cfg(target_family = "unix")'.dependencies]
+pprof = { workspace = true, features = ["criterion", "flamegraph"], optional = true }
diff --git a/utils/src/bench.rs b/utils/src/bench.rs
index b2759491..6179e072 100644
--- a/utils/src/bench.rs
+++ b/utils/src/bench.rs
@@ -71,7 +71,7 @@ impl<'b> Bench<'b> {
 
         let field_path = self.subtest.map(|s| format!(".{s}")).unwrap_or_default();
         let content = format!(
-            "(import \"{}\"){}.run {}",
+            "(import {:?}){}.run {}",
             path.to_string_lossy(),
             field_path,
             self.args
@@ -86,13 +86,15 @@ impl<'b> Bench<'b> {
         } else {
             content
         };
-        parse(&content).unwrap()
+        parse(&content).unwrap_or_else(|err| panic!("Failed parsing {path:?}: {err:?}"))
     }
 
     pub fn path(&self) -> PathBuf {
-        let mut path = PathBuf::from(self.base_dir);
-        path.push(format!("benches/{}.ncl", self.subpath));
-        path
+        PathBuf::from_iter([
+            self.base_dir,
+            "benches",
+            format!("{}.ncl", self.subpath).as_str(),
+        ])
     }
 }
 
@@ -139,6 +141,17 @@ pub fn bench_terms<'r>(rts: Vec<Bench<'r>>) -> Box<dyn Fn(&mut Criterion) + 'r>
     })
 }
 
+/// Create a `Criterion` config. Uses `PProfProfiler` when `pprof` is enabled on Unix systems.
+pub fn criterion_config() -> Criterion {
+    let config = Criterion::default();
+    #[cfg(all(target_family = "unix", feature = "pprof"))]
+    let config = config.with_profiler(pprof::criterion::PProfProfiler::new(
+        100,
+        pprof::criterion::Output::Flamegraph(None),
+    ));
+    config
+}
+
 #[macro_export]
 macro_rules! ncl_bench {
     {


Test patch:
diff --git a/cli/tests/snapshot/main.rs b/cli/tests/snapshot/main.rs
index 3c17bbcb..00b5e962 100644
--- a/cli/tests/snapshot/main.rs
+++ b/cli/tests/snapshot/main.rs
@@ -16,8 +16,9 @@ macro_rules! assert_snapshot_filtered {
             // Since error output includes fully-qualified paths to the source file
             // we need to replace those with something static to avoid snapshots
             // differing across machines.
-            (r"(?:/.+/tests/snapshot/inputs)", "[INPUTS_PATH]"),
-            (r"(?:/.+/tests/snapshot/imports)", "[IMPORTS_PATH]")
+            // Replace filepath backslashes with forward slashes for Windows.
+            (r"(?:(?:.:)?(?:/|\\).+(?:/|\\)tests(?:/|\\)snapshot(?:/|\\)inputs(?:/|\\))([0-9A-Za-z_-]+)(?:/|\\)(.+)", "[INPUTS_PATH]/${1}/${2}"),
+            (r"(?:(?:.:)?(?:/|\\).+(?:/|\\)tests(?:/|\\)snapshot(?:/|\\)imports(?:/|\\))(.+)", "[IMPORTS_PATH]/${1}")
         ]},
         {
             insta::assert_snapshot!($name, $snapshot);
diff --git a/core/tests/integration/inputs/contracts/simplify_doesnt_remove_fields.ncl b/core/tests/integration/inputs/contracts/simplify_doesnt_remove_fields.ncl
new file mode 100644
index 00000000..59b26796
--- /dev/null
+++ b/core/tests/integration/inputs/contracts/simplify_doesnt_remove_fields.ncl
@@ -0,0 +1,8 @@
+# test.type = 'pass'
+
+# Regression test for issue #2014 "Record row polymorphism can be destructive"
+# (https://github.com/tweag/nickel/issues/2014)
+let f : forall tail. { a : Number; tail } -> { a : Number; tail }
+  = fun o => o
+  in
+f { a = 1, b = ".." } == { a = 1, b = ".." }
diff --git a/core/tests/integration/inputs/typecheck/record_subtyping.ncl b/core/tests/integration/inputs/typecheck/record_subtyping.ncl
new file mode 100644
index 00000000..8915cf85
--- /dev/null
+++ b/core/tests/integration/inputs/typecheck/record_subtyping.ncl
@@ -0,0 +1,6 @@
+# test.type = 'pass'
+let test : _ =
+    let test_func : {a : {_ : Number}} -> {a : {_ : Number}} = fun a => a in
+    test_func {a = {foo = 5}}
+in 
+true
diff --git a/core/tests/integration/inputs/typecheck/record_subtyping_multiple_components.ncl b/core/tests/integration/inputs/typecheck/record_subtyping_multiple_components.ncl
new file mode 100644
index 00000000..3940f45d
--- /dev/null
+++ b/core/tests/integration/inputs/typecheck/record_subtyping_multiple_components.ncl
@@ -0,0 +1,6 @@
+# test.type = 'pass'
+let test : _ =
+  let test_func : {a : {_ : Number}, b : {_ : String}} -> {a : {_ : Number}, b : {_ : String}} = fun a => a in 
+  test_func {a = {foo = 5}, b = {a = "test"}}
+in
+true
diff --git a/core/tests/integration/inputs/typecheck/record_subtyping_with_tail.ncl b/core/tests/integration/inputs/typecheck/record_subtyping_with_tail.ncl
new file mode 100644
index 00000000..a24d9516
--- /dev/null
+++ b/core/tests/integration/inputs/typecheck/record_subtyping_with_tail.ncl
@@ -0,0 +1,6 @@
+# test.type = 'pass'
+let test : _ =
+  let test_func : forall b. {a : {_ : Number}; b} -> {a : {_ : Number}; b} = fun a => a in
+  test_func {a = {foo = 5}, b = 5} 
+in
+true
diff --git a/lsp/nls/tests/main.rs b/lsp/nls/tests/main.rs
index 173610e4..1f4ded2d 100644
--- a/lsp/nls/tests/main.rs
+++ b/lsp/nls/tests/main.rs
@@ -3,7 +3,7 @@ use pretty_assertions::assert_eq;
 use serde_json::json;
 use test_generator::test_resources;
 
-use lsp_harness::{TestFixture, TestHarness};
+use lsp_harness::{file_url_from_path, TestFixture, TestHarness};
 
 #[test_resources("lsp/nls/tests/inputs/*.ncl")]
 fn check_snapshots(path: &str) {
@@ -23,7 +23,12 @@ fn check_snapshots(path: &str) {
     harness.drain_diagnostics(fixture.expected_diags.iter().cloned());
     let output = String::from_utf8(harness.out).unwrap();
 
+    insta::with_settings!(
+        {filters => vec![("file:///C:", "file://")]},
+        {
     insta::assert_snapshot!(path, output);
+       }
+    );
 }
 
 #[test]
@@ -31,8 +36,8 @@ fn refresh_missing_imports() {
     let _ = env_logger::try_init();
     let mut harness = TestHarness::new();
 
-    let url = |s: &str| lsp_types::Url::from_file_path(s).unwrap();
-    harness.send_file(url("/test.ncl"), "import \"dep.ncl\"");
+    let test_uri = file_url_from_path("/test.ncl").unwrap();
+    harness.send_file(test_uri.clone(), "import \"dep.ncl\"");
     let diags = harness.wait_for_diagnostics().diagnostics;
     assert_eq!(2, diags.len());
     assert!(diags[0].message.contains("import of dep.ncl failed"));
@@ -43,7 +48,8 @@ fn refresh_missing_imports() {
     assert!(diags[0].message.contains("import of dep.ncl failed"));
 
     // Now provide the import.
-    harness.send_file(url("/dep.ncl"), "42");
+    let dep_uri = file_url_from_path("/dep.ncl").unwrap();
+    harness.send_file(dep_uri.clone(), "42");
 
     // Check that we get back clean diagnostics for both files.
     // (LSP doesn't define the order, but we happen to know it)
@@ -52,7 +58,7 @@ fn refresh_missing_imports() {
     loop {
         let diags = harness.wait_for_diagnostics();
         assert!(diags.diagnostics.is_empty());
-        if diags.uri.path() == "/dep.ncl" {
+        if diags.uri == dep_uri {
             break;
         }
     }
@@ -60,7 +66,7 @@ fn refresh_missing_imports() {
     loop {
         let diags = harness.wait_for_diagnostics();
         assert!(diags.diagnostics.is_empty());
-        if diags.uri.path() == "/test.ncl" {
+        if diags.uri == test_uri {
             break;
         }
     }
@@ -73,17 +79,18 @@ fn reload_broken_imports() {
     let _ = env_logger::try_init();
     let mut harness = TestHarness::new();
 
-    let url = |s: &str| lsp_types::Url::from_file_path(s).unwrap();
-    harness.send_file(url("/dep.ncl"), "{ x }");
+    let dep_uri = file_url_from_path("/dep.ncl").unwrap();
+    harness.send_file(dep_uri.clone(), "{ x }");
 
-    harness.send_file(url("/test.ncl"), "import \"dep.ncl\"");
+    let test_uri = file_url_from_path("/test.ncl").unwrap();
+    harness.send_file(test_uri.clone(), "import \"dep.ncl\"");
     let diags = harness.wait_for_diagnostics();
 
-    assert_eq!("/dep.ncl", diags.uri.path());
+    assert_eq!(diags.uri, dep_uri);
     assert!(diags.diagnostics.is_empty());
 
     let diags = harness.wait_for_diagnostics();
-    assert_eq!("/test.ncl", diags.uri.path());
+    assert_eq!(diags.uri, test_uri);
     assert!(diags.diagnostics.is_empty());
 
     // We expect two more diagnostics coming from background eval.
@@ -91,7 +98,7 @@ fn reload_broken_imports() {
     let _diags = harness.wait_for_diagnostics();
 
     // Introduce an error in the import.
-    harness.send_file(url("/dep.ncl"), "{ `x = 1 }");
+    harness.send_file(dep_uri.clone(), "{ `x = 1 }");
 
     // Check that we get back clean diagnostics for both files.
     // (LSP doesn't define the order, but we happen to know it)
@@ -99,7 +106,7 @@ fn reload_broken_imports() {
     // file (once from synchronous typechecking, once from eval in the background).
     loop {
         let diags = harness.wait_for_diagnostics();
-        if diags.uri.path() == "/dep.ncl" {
+        if diags.uri == dep_uri {
             assert_eq!(diags.diagnostics[0].message, "unexpected token");
             break;
         }
@@ -107,7 +114,7 @@ fn reload_broken_imports() {
 
     loop {
         let diags = harness.wait_for_diagnostics();
-        if diags.uri.path() == "/test.ncl" {
+        if diags.uri == test_uri {
             assert_eq!(diags.diagnostics[0].message, "unexpected token");
             break;
         }
@@ -125,9 +132,9 @@ fn apply_client_options() {
         }
     });
     let mut harness = TestHarness::new_with_options(Some(lsp_options));
-    let url = |s: &str| lsp_types::Url::from_file_path(s).unwrap();
+    let test_uri = file_url_from_path("/test.ncl").unwrap();
     harness.send_file(
-        url("/test.ncl"),
+        test_uri,
         "{ C = fun n => if n == 0 then String else C (n - 1), res = 2 | C 5 }",
     );
 
diff --git a/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__hover_field_typed_block_regression_1574.ncl.snap b/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__hover_field_typed_block_regression_1574.ncl.snap
index 61ad2365..2e9e5234 100644
--- a/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__hover_field_typed_block_regression_1574.ncl.snap
+++ b/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__hover_field_typed_block_regression_1574.ncl.snap
@@ -2,7 +2,9 @@
 source: lsp/nls/tests/main.rs
 expression: output
 ---
-<0:24-0:37>[Applies a function to every element in the given array. That is,
+<0:24-0:37>[```nickel
+(_a -> Number) -> Array _a -> Array Number
+```, Applies a function to every element in the given array. That is,
 `map f [ x1, x2, ..., xn ]` is `[ f x1, f x2, ..., f xn ]`.
 
 # Examples
@@ -13,4 +15,3 @@ std.array.map (fun x => x + 1) [ 1, 2, 3 ] =>
 ```, ```nickel
 forall a b. (a -> b) -> Array a -> Array b
 ```]
-