Repository: tweag/nickel
Pull request #2013 (2024-07-26 16:25:04)

[Optimization] Cache contract generation and pre-compile some match expression
This PR is guided by the metrics gathered for some run of Nickel on large codebases, which showed that some contracts were generated again and again, while coming from one initial annotation. While it's expected that an annotation might give raise to many runtime evaluations (a contract in the body of a function, typically), it's wasteful that we _generate_ the code at runtime many times (contract generation is a form of compilation from a static type to a Nickel expression, and it shouldn't happen all the time during execution).

The issue is that we now store types directly in the AST and consider them weak head normal form. So, each time we apply such a contract, `contract/apply` get a `typ::Type`, and need to make a contract out of it: generation happens again and again. This PR adds a new field to `Term::Type`, `contract: RichTerm`, which is populated at parsing time with the contract generated from the type (which is close to the behavior before the introduction of `Term::Type`). Doing so, we should only generate one contract for each user annotation in the code.

Metrics indeed show that in some big examples, the worst case was generating ~1700 times the same contract, which is brought down to one. We also tried to closurize the generated contract, so that it doesn't have to be evaluated several time, but this showed no improvement whatsoever, while it increases the number of allocated thunks, so it's been reverted.

Additionally, in the same spirit of "generating more statically, and don't do it again at runtime", we precompile the match expression generated when converting an enum contract, so that it's not recompiled again and again each time the contract is applied. This showed a reduction of around 25 to 30% of the total number of compilation of match expressions on the private benchmark.

The concrete time again aren't spectacular, as it's saving mostly Rust function calls, and not Nickel, the latter being of course the dominant cost, but there is still a small improvement.

aspiwack: What are the estimate performance gains from this PR?
yannham: > What are the estimate performance gains from this PR?

As a disclaimer, the improvement is hard to measure properly with the micro benchmarks (aka it doesn't show), in particular because we don't really benchmark using the same contract again and again (which does happen in real life as measurements show, probably because of merging, array contracts, etc.), and I feel a micro benchmark on that would be rather artificial. The only example where it can show measurable effects is a 120kLoC real code base, which takes around 20sec to evaluate, which starts to be long running enough to see some differences.

I see a reduction of around 2% on several runs in user time (but system time, which is the predominant cost, is varying quite a bit, making the final result potentially less, at least on my very volatile laptop). Could be interesting to ask the original users, which are moreover using OsX, if they see something different in their setup.

What motivated this PR originally is:

- a few commits earlier, master was atrociously slower than latest stable release on said example. The contract system rework was of course an important factor, but adding a type node to the AST is another thing we implemented after 1.7. In some sense, this PR is trying to do something closer to how it worked in 1.7, with the idea of closing the gap.
- This PR only decreases strictly all the stuff that we measure at the level of the interpreter (thunks allocation, environment creation/size/cloning, all primop application, contract generation, etc.), so at the macro level, it should be a strict improvement. We're not changing the AST layout (that is, the size and alignement of the `Term` structure), which is already a big enum with larger variants. Of course it doesn't preclude memory layout effects that could indeed negate any potential benefit of this change, but I suppose it still limits the possibility.

I intend to do a larger rework of the AST after the next (imminent) release of 1.8 anyway, so this change might not be very impactful on the long term. It's more of a "back to 1.7 perf" band-aid. However it's not hugely impactful even now, so I'm fine ditching it if others think it's not worth it.

Patch:
diff --git a/.github/workflows/benchmark-master.yaml b/.github/workflows/benchmark-master.yaml
new file mode 100644
index 00000000..7e317448
--- /dev/null
+++ b/.github/workflows/benchmark-master.yaml
@@ -0,0 +1,29 @@
+name: benchmark master
+on:
+  push:
+    branches: master
+jobs:
+  benchmark-master:
+    name: benchmark master
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - uses: cachix/install-nix-action@V27
+        name: "Installing Nix"
+        with:
+          extra_nix_config: |
+            experimental-features = nix-command flakes
+            accept-flake-config = true
+          nix_path: "nixpkgs=channel:nixos-unstable"
+      - uses: bencherdev/bencher@main
+      - name: Track benchmarks on master
+        run: |
+          bencher run \
+          --project nickel \
+          --token '${{ secrets.BENCHER_API_TOKEN }}' \
+          --branch master \
+          --testbed ubuntu-latest \
+          --adapter rust_criterion \
+          nix develop --command cargo bench --package nickel-lang-core --bench numeric
diff --git a/.github/workflows/benchmark-pr.yaml b/.github/workflows/benchmark-pr.yaml
new file mode 100644
index 00000000..37add156
--- /dev/null
+++ b/.github/workflows/benchmark-pr.yaml
@@ -0,0 +1,44 @@
+# This is the part of the benchmark runner that runs on pull requests.
+# It's separate from the master runner for two reasons:
+# - to track it differently on bencher.dev, because we only want to use master as
+#   the historical baseline for comparison
+# - because it might want to run on PRs from forks, and those don't get access to the
+#   bencher API key.
+#
+# See the [bencher docs] for more details.
+#
+# [bencher docs]:  https://bencher.dev/docs/how-to/github-actions/#benchmark-fork-pr-and-upload-from-default-branch
+
+name: benchmark pull requests
+on:
+  pull_request:
+    types: [opened, reopened, edited, synchronize]
+
+jobs:
+  benchmark-pr:
+    name: benchmark pr
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - uses: cachix/install-nix-action@V27
+        name: "Installing Nix"
+        with:
+          extra_nix_config: |
+            experimental-features = nix-command flakes
+            accept-flake-config = true
+          nix_path: "nixpkgs=channel:nixos-unstable"
+      - name: run benchmarks
+        run: |
+          nix develop --command cargo bench --package nickel-lang-core --bench numeric > criterion-output.txt
+      - name: upload results
+        uses: actions/upload-artifact@v4
+        with:
+          name: criterion-output
+          path: criterion-output.txt
+      - name: Upload GitHub Pull Request Event
+        uses: actions/upload-artifact@v4
+        with:
+          name: event.json
+          path: ${{ github.event_path }}
diff --git a/.github/workflows/release-artifacts.yaml b/.github/workflows/release-artifacts.yaml
index d9cee164..b9eb3e7d 100644
--- a/.github/workflows/release-artifacts.yaml
+++ b/.github/workflows/release-artifacts.yaml
@@ -1,4 +1,4 @@
-name: Upload release artifacts
+name: Test Docker manifest
 on:
   release:
     types: [published]
diff --git a/.github/workflows/run-benchmark.yaml b/.github/workflows/run-benchmark.yaml
deleted file mode 100644
index b1a0ee3a..00000000
--- a/.github/workflows/run-benchmark.yaml
+++ /dev/null
@@ -1,17 +0,0 @@
-name: benchmark pull requests
-on:
-  pull_request:
-    types: [labeled]
-jobs:
-  runBenchmark:
-    if: ${{ github.event.label.name == 'run-benchmark' && github.event_name == 'pull_request' }}
-    name: run benchmark
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          fetch-depth: 0
-      - uses: jasonwilliams/criterion-compare-action@move_to_actions
-        with:
-          branchName: ${{ github.base_ref }}
-          token: ${{ secrets.GITHUB_TOKEN }}
diff --git a/.github/workflows/upload-pr-benchmarks.yaml b/.github/workflows/upload-pr-benchmarks.yaml
new file mode 100644
index 00000000..7694b882
--- /dev/null
+++ b/.github/workflows/upload-pr-benchmarks.yaml
@@ -0,0 +1,72 @@
+name: Track Benchmarks with Bencher
+
+on:
+  workflow_run:
+    workflows: [benchmark pull requests]
+    types: [completed]
+
+jobs:
+  track_fork_pr_branch:
+    name: track pr benchmarks
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
+    runs-on: ubuntu-latest
+    env:
+      BENCHMARK_RESULTS: criterion-output
+      PR_EVENT: event.json
+    steps:
+      - name: Download Benchmark Results
+        uses: actions/github-script@v6
+        with:
+          script: |
+            async function downloadArtifact(artifactName) {
+              let allArtifacts = await github.rest.actions.listWorkflowRunArtifacts({
+                owner: context.repo.owner,
+                repo: context.repo.repo,
+                run_id: context.payload.workflow_run.id,
+              });
+              let matchArtifact = allArtifacts.data.artifacts.filter((artifact) => {
+                return artifact.name == artifactName
+              })[0];
+              if (!matchArtifact) {
+                core.setFailed(`Failed to find artifact: ${artifactName}`);
+              }
+              let download = await github.rest.actions.downloadArtifact({
+                owner: context.repo.owner,
+                repo: context.repo.repo,
+                artifact_id: matchArtifact.id,
+                archive_format: 'zip',
+              });
+              let fs = require('fs');
+              fs.writeFileSync(`${process.env.GITHUB_WORKSPACE}/${artifactName}.zip`, Buffer.from(download.data));
+            }
+            await downloadArtifact(process.env.BENCHMARK_RESULTS);
+            await downloadArtifact(process.env.PR_EVENT);
+      - name: Unzip Benchmark Results
+        run: |
+          unzip $BENCHMARK_RESULTS.zip
+          unzip $PR_EVENT.zip
+      - name: Export PR Event Data
+        uses: actions/github-script@v6
+        with:
+          script: |
+            let fs = require('fs');
+            let prEvent = JSON.parse(fs.readFileSync(process.env.PR_EVENT, {encoding: 'utf8'}));
+            core.exportVariable("PR_HEAD", `${prEvent.number}/merge`);
+            core.exportVariable("PR_BASE", prEvent.pull_request.base.ref);
+            core.exportVariable("PR_BASE_SHA", prEvent.pull_request.base.sha);
+            core.exportVariable("PR_NUMBER", prEvent.number);
+      - uses: bencherdev/bencher@main
+      - name: Track Benchmarks with Bencher
+        run: |
+          bencher run \
+          --project nickel \
+          --token '${{ secrets.BENCHER_API_TOKEN }}' \
+          --branch '${{ env.PR_HEAD }}' \
+          --branch-start-point '${{ env.PR_BASE }}' \
+          --branch-start-point-hash '${{ env.PR_BASE_SHA }}' \
+          --testbed ubuntu-latest \
+          --adapter rust_criterion \
+          --err \
+          --github-actions '${{ secrets.GITHUB_TOKEN }}' \
+          --ci-number '${{ env.PR_NUMBER }}' \
+          --file "$BENCHMARK_RESULTS.txt"
diff --git a/core/benches/nixpkgs/lists.ncl b/core/benches/nixpkgs/lists.ncl
index d8d886cd..040ac812 100644
--- a/core/benches/nixpkgs/lists.ncl
+++ b/core/benches/nixpkgs/lists.ncl
@@ -525,9 +525,8 @@
             @ (toporest | { result : Array Dyn }).result
         } : { _ : Array Dyn },
 
-  #TODO: can it be statically typed?
   sort
-    | forall a. (a -> a -> Bool) -> Array a -> Array a
+    : forall a. (a -> a -> Bool) -> Array a -> Array a
     | doc m%"
       Sort a list based on a comparator function which compares two
      elements and returns true if the first argument is strictly below
diff --git a/core/src/closurize.rs b/core/src/closurize.rs
index 62f7ef7f..7eec2d42 100644
--- a/core/src/closurize.rs
+++ b/core/src/closurize.rs
@@ -289,9 +289,10 @@ pub fn should_share(t: &Term) -> bool {
         | Term::Var(_)
         | Term::Enum(_)
         | Term::Fun(_, _)
+        | Term::Closure(_)
+        | Term::Type { .. }
         // match acts like a function, and is a WHNF
-        | Term::Match {..}
-        | Term::Type(_) => false,
+        | Term::Match {..} => false,
         _ => true,
     }
 }
diff --git a/core/src/eval/mod.rs b/core/src/eval/mod.rs
index cd0c4dd3..93c0da04 100644
--- a/core/src/eval/mod.rs
+++ b/core/src/eval/mod.rs
@@ -1165,7 +1165,7 @@ pub fn subst<C: Cache>(
         // We could recurse here, because types can contain terms which would then be subject to
         // substitution. Not recursing should be fine, though, because a type in term position
         // turns into a contract, and we don't substitute inside contracts either currently.
-        | v @ Term::Type(_) => RichTerm::new(v, pos),
+        | v @ Term::Type {..} => RichTerm::new(v, pos),
         Term::EnumVariant { tag, arg, attrs } => {
             let arg = subst(cache, arg, initial_env, env);
 
diff --git a/core/src/eval/operation.rs b/core/src/eval/operation.rs
index 6c8a054f..d6a0fa11 100644
--- a/core/src/eval/operation.rs
+++ b/core/src/eval/operation.rs
@@ -247,7 +247,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     Term::Array(..) => "Array",
                     Term::Record(..) | Term::RecRecord(..) => "Record",
                     Term::Lbl(..) => "Label",
-                    Term::Type(_) => "Type",
+                    Term::Type { .. } => "Type",
                     Term::ForeignId(_) => "ForeignId",
                     _ => "Other",
                 };
@@ -1736,15 +1736,25 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                 }
             }
             BinaryOp::ContractApply | BinaryOp::ContractCheck => {
-                // The translation of a type might return any kind of contract, including e.g. a
-                // record or a custom contract. The result thus needs to be passed to `b_op` again.
-                // In that case, we don't bother tracking the argument and updating the label: this
-                // will be done by the next call to `b_op`.
-                if let Term::Type(typ) = &*t1 {
+                // Doing just one `if let Term::Type` and putting the call to `increment!` there
+                // looks sensible at first, but it's annoying to explain to rustc and clippy that
+                // we match on `typ` but use it only if the `metrics` feature is enabled (we get
+                // unused variable warning otherwise). It's simpler to just make a separate `if`
+                // conditionally included.
+                #[cfg(feature = "metrics")]
+                if let Term::Type { typ, .. } = &*t1 {
                     increment!(format!(
                         "primop:contract/apply:{}",
                         typ.pretty_print_cap(40)
                     ));
+                }
+
+                let t1 = if let Term::Type { typ: _, contract } = &*t1 {
+                    // The contract generation from a static type might return any kind of
+                    // contract, including e.g. a record or a custom contract. The result needs to
+                    // be evaluated first, and then passed to `b_op` again. In that case, we don't
+                    // bother tracking the argument and updating the label: this will be done by
+                    // the next call to `b_op`.
 
                     // We set the stack to represent the evaluation context `<b_op> [.] label` and
                     // proceed to evaluate `<typ.contract()>`
@@ -1765,10 +1775,12 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     );
 
                     return Ok(Closure {
-                        body: typ.contract()?,
+                        body: contract.clone(),
                         env: env1,
                     });
-                }
+                } else {
+                    t1
+                };
 
                 let t2 = t2.into_owned();
 
diff --git a/core/src/parser/uniterm.rs b/core/src/parser/uniterm.rs
index 07b1bb8c..bcef7fc9 100644
--- a/core/src/parser/uniterm.rs
+++ b/core/src/parser/uniterm.rs
@@ -126,12 +126,16 @@ impl TryFrom<UniTerm> for RichTerm {
         let rt = match node {
             UniTermNode::Var(id) => RichTerm::new(Term::Var(id), pos),
             UniTermNode::Record(r) => RichTerm::try_from(r)?,
-            UniTermNode::Type(mut ty) => {
-                ty.fix_type_vars(pos.unwrap())?;
-                if let TypeF::Flat(rt) = ty.typ {
+            UniTermNode::Type(mut typ) => {
+                typ.fix_type_vars(pos.unwrap())?;
+                if let TypeF::Flat(rt) = typ.typ {
                     rt.with_pos(pos)
                 } else {
-                    RichTerm::new(Term::Type(ty), pos)
+                    let contract = typ
+                        .contract()
+                        .map_err(|err| ParseError::UnboundTypeVariables(vec![err.0]))?;
+
+                    RichTerm::new(Term::Type { typ, contract }, pos)
                 }
             }
             UniTermNode::Term(rt) => rt,
@@ -478,7 +482,7 @@ impl TryFrom<UniRecord> for RichTerm {
         let result = if ur.tail.is_some() || (ur.is_record_type() && !ur.fields.is_empty()) {
             let tail_span = ur.tail.as_ref().and_then(|t| t.1.into_opt());
             // We unwrap all positions: at this stage of the parsing, they must all be set
-            let mut ty = ur
+            let mut typ = ur
                 .into_type_strict()
                 .map_err(|cause| ParseError::InvalidRecordType {
                     tail_span,
@@ -486,8 +490,12 @@ impl TryFrom<UniRecord> for RichTerm {
                     cause,
                 })?;
 
-            ty.fix_type_vars(pos.unwrap())?;
-            Ok(RichTerm::new(Term::Type(ty), pos))
+            typ.fix_type_vars(pos.unwrap())?;
+            let contract = typ
+                .contract()
+                .map_err(|err| ParseError::UnboundTypeVariables(vec![err.0]))?;
+
+            Ok(RichTerm::new(Term::Type { typ, contract }, pos))
         } else {
             ur.check_typed_field_without_def()?;
 
diff --git a/core/src/pretty.rs b/core/src/pretty.rs
index 58ac14f9..67d7820f 100644
--- a/core/src/pretty.rs
+++ b/core/src/pretty.rs
@@ -1038,7 +1038,7 @@ where
                 .append(allocator.as_string(f.to_string_lossy()).double_quotes()),
             ResolvedImport(id) => allocator.text(format!("import <file_id: {id:?}>")),
             // This type is in term position, so we don't need to add parentheses.
-            Type(ty) => ty.pretty(allocator),
+            Type { typ, contract: _ } => typ.pretty(allocator),
             ParseError(_) => allocator.text("%<PARSE ERROR>"),
             RuntimeError(_) => allocator.text("%<RUNTIME ERROR>"),
             Closure(idx) => allocator.text(format!("%<closure@{idx:p}>")),
diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs
index acf87974..3e50f8fb 100644
--- a/core/src/term/mod.rs
+++ b/core/src/term/mod.rs
@@ -21,8 +21,7 @@ use string::NickelString;
 
 use crate::{
     error::{EvalError, ParseError},
-    eval::cache::CacheIndex,
-    eval::Environment,
+    eval::{cache::CacheIndex, Environment},
     identifier::LocIdent,
     impl_display_from_pretty,
     label::{Label, MergeLabel},
@@ -217,7 +216,14 @@ pub enum Term {
     ///
     /// During evaluation, this will get turned into a contract.
     #[serde(skip)]
-    Type(Type),
+    Type {
+        /// The static type.
+        typ: Type,
+        /// The conversion of this type to a contract, that is, `typ.contract()?`. This field
+        /// serves as a caching mechanism so we only run the contract generation code once per type
+        /// written by the user.
+        contract: RichTerm,
+    },
 
     /// A custom contract. The content must be a function (or function-like terms like a match
     /// expression) of two arguments: a label and the value to be checked. In particular, it must
@@ -362,7 +368,16 @@ impl PartialEq for Term {
             (Self::Annotated(l0, l1), Self::Annotated(r0, r1)) => l0 == r0 && l1 == r1,
             (Self::Import(l0), Self::Import(r0)) => l0 == r0,
             (Self::ResolvedImport(l0), Self::ResolvedImport(r0)) => l0 == r0,
-            (Self::Type(l0), Self::Type(r0)) => l0 == r0,
+            (
+                Self::Type {
+                    typ: l0,
+                    contract: l1,
+                },
+                Self::Type {
+                    typ: r0,
+                    contract: r1,
+                },
+            ) => l0 == r0 && l1 == r1,
             (Self::ParseError(l0), Self::ParseError(r0)) => l0 == r0,
             (Self::RuntimeError(l0), Self::RuntimeError(r0)) => l0 == r0,
             // We don't compare closure, because we can't, without the evaluation cache at hand.
@@ -948,7 +963,7 @@ impl Term {
             Term::SealingKey(_) => Some("SealingKey".to_owned()),
             Term::Sealed(..) => Some("Sealed".to_owned()),
             Term::Annotated(..) => Some("Annotated".to_owned()),
-            Term::Type(_) => Some("Type".to_owned()),
+            Term::Type { .. } => Some("Type".to_owned()),
             Term::ForeignId(_) => Some("ForeignId".to_owned()),
             Term::CustomContract(_) => Some("CustomContract".to_owned()),
             Term::Let(..)
@@ -998,9 +1013,9 @@ impl Term {
             | Term::EnumVariant {..}
             | Term::Record(..)
             | Term::Array(..)
-            | Term::Type(_)
             | Term::ForeignId(_)
-            | Term::SealingKey(_) => true,
+            | Term::SealingKey(_)
+            | Term::Type {..} => true,
             Term::Let(..)
             | Term::LetPattern(..)
             | Term::FunPattern(..)
@@ -1078,7 +1093,7 @@ impl Term {
             | Term::ResolvedImport(_)
             | Term::StrChunks(_)
             | Term::RecRecord(..)
-            | Term::Type(_)
+            | Term::Type { .. }
             | Term::ParseError(_)
             | Term::EnumVariant { .. }
             | Term::RuntimeError(_) => false,
@@ -1115,6 +1130,7 @@ impl Term {
             | Term::Op1(UnaryOp::BoolOr, _) => true,
             // A number with a minus sign as a prefix isn't a proper atom
             Term::Num(n) if *n >= 0 => true,
+            Term::Type {typ, contract: _} => typ.fmt_is_atom(),
             Term::Let(..)
             | Term::Num(..)
             | Term::EnumVariant {..}
@@ -1131,7 +1147,6 @@ impl Term {
             | Term::Annotated(..)
             | Term::Import(..)
             | Term::ResolvedImport(..)
-            | Term::Type(_)
             | Term::Closure(_)
             | Term::ParseError(_)
             | Term::RuntimeError(_) => false,
@@ -2322,8 +2337,11 @@ impl Traverse<RichTerm> for RichTerm {
                 let term = term.traverse(f, order)?;
                 RichTerm::new(Term::Annotated(annot, term), pos)
             }
-            Term::Type(ty) => {
-                RichTerm::new(Term::Type(ty.traverse(f, order)?), pos)
+            Term::Type { typ, contract } => {
+                let typ = typ.traverse(f, order)?;
+                let contract = contract.traverse(f, order)?;
+
+                RichTerm::new(Term::Type { typ, contract }, pos)
             }
             _ => rt,
         });
@@ -2417,7 +2435,10 @@ impl Traverse<RichTerm> for RichTerm {
             Term::Annotated(annot, t) => t
                 .traverse_ref(f, state)
                 .or_else(|| annot.traverse_ref(f, state)),
-            Term::Type(ty) => ty.traverse_ref(f, state),
+            Term::Type { typ, contract } => {
+                typ.traverse_ref(f, state)?;
+                contract.traverse_ref(f, state)
+            }
         }
     }
 }
@@ -2430,9 +2451,10 @@ impl Traverse<Type> for RichTerm {
         self.traverse(
             &mut |rt: RichTerm| {
                 match_sharedterm!(match (rt.term) {
-                    Term::Type(ty) => ty
-                        .traverse(f, order)
-                        .map(|ty| RichTerm::new(Term::Type(ty), rt.pos)),
+                    Term::Type { typ, contract } => {
+                        let typ = typ.traverse(f, order)?;
+                        Ok(RichTerm::new(Term::Type { typ, contract }, rt.pos))
+                    }
                     _ => Ok(rt),
                 })
             },
@@ -2447,7 +2469,7 @@ impl Traverse<Type> for RichTerm {
     ) -> Option<U> {
         self.traverse_ref(
             &mut |rt: &RichTerm, state: &S| match &*rt.term {
-                Term::Type(ty) => ty.traverse_ref(f, state).into(),
+                Term::Type { typ, contract: _ } => typ.traverse_ref(f, state).into(),
                 _ => TraverseControl::Continue,
             },
             state,
diff --git a/core/src/transform/free_vars.rs b/core/src/transform/free_vars.rs
index 823719c4..e4ab64d3 100644
--- a/core/src/transform/free_vars.rs
+++ b/core/src/transform/free_vars.rs
@@ -180,8 +180,9 @@ impl CollectFreeVars for RichTerm {
 
                 t.collect_free_vars(free_vars);
             }
-            Term::Type(ty) => {
-                ty.collect_free_vars(free_vars);
+            Term::Type { typ, contract } => {
+                typ.collect_free_vars(free_vars);
+                contract.collect_free_vars(free_vars);
             }
             Term::Closure(_) => {
                 unreachable!("should never see closures at the transformation stage");
diff --git a/core/src/typ.rs b/core/src/typ.rs
index a7652c4b..1370272f 100644
--- a/core/src/typ.rs
+++ b/core/src/typ.rs
@@ -51,6 +51,7 @@ use crate::{
     position::TermPos,
     pretty::PrettyPrintCap,
     stdlib::internals,
+    term::pattern::compile::Compile,
     term::{
         array::Array, make as mk_term, record::RecordData, string::NickelString, IndexMap,
         MatchBranch, MatchData, RichTerm, Term, Traverse, TraverseControl, TraverseOrder,
@@ -987,8 +988,8 @@ impl Subcontract for EnumRows {
         // For example, for an enum type [| 'foo, 'bar, 'Baz T |], the function looks like:
         //
         // ```
-        // fun l x =>
-        //   x |> match {
+        // fun label value =>
+        //   value |> match {
         //     'foo => 'Ok x,
         //     'bar => 'Ok x,
         //     'Baz variant_arg => 'Ok ('Baz (%apply_contract% T label_arg variant_arg)),
@@ -1075,7 +1076,9 @@ impl Subcontract for EnumRows {
             body: default,
         });
 
-        let match_expr = mk_app!(Term::Match(MatchData { branches }), mk_term::var(value_arg));
+        // We pre-compile the match expression, so that it's not compiled again and again at each
+        // application of the contract.
+        let match_expr = MatchData { branches }.compile(mk_term::var(value_arg), TermPos::None);
 
         let case = mk_fun!(label_arg, value_arg, match_expr);
         Ok(mk_app!(internals::enumeration(), case))
diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index e6fb49ab..0cceb9e3 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -463,7 +463,19 @@ fn contract_eq_bounded<E: TermEnvironment>(
         (Op1(UnaryOp::RecordAccess(id1), t1), Op1(UnaryOp::RecordAccess(id2), t2)) => {
             id1 == id2 && contract_eq_bounded(state, t1, env1, t2, env2)
         }
-        (Type(ty1), Type(ty2)) => type_eq_bounded(
+        // 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).
+        (
+            Type {
+                typ: ty1,
+                contract: _,
+            },
+            Type {
+                typ: ty2,
+                contract: _,
+            },
+        ) => type_eq_bounded(
             state,
             &GenericUnifType::from_type(ty1.clone(), env1),
             env1,
diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs
index 1d70ac5f..a003386d 100644
--- a/core/src/typecheck/mod.rs
+++ b/core/src/typecheck/mod.rs
@@ -1619,7 +1619,9 @@ fn walk<V: TypecheckVisitor>(
         Term::Annotated(annot, rt) => {
             walk_annotated(state, ctxt, visitor, annot, rt)
         }
-        Term::Type(ty) => walk_type(state, ctxt, visitor, ty),
+        // The contract field is just a caching mechanism, and should be set to `None` at this
+        // point anyway. We can safely ignore it.
+        Term::Type { typ, contract: _ } => walk_type(state, ctxt, visitor, typ),
         Term::Closure(_) => unreachable!("should never see a closure at typechecking time"),
    }
 }
@@ -2350,7 +2352,7 @@ fn check<V: TypecheckVisitor>(
             ty.unify(ty_import, state, &ctxt)
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
-        Term::Type(typ) => {
+        Term::Type { typ, contract: _ } => {
             if let Some(flat) = typ.find_flat() {
                 Err(TypecheckError::FlatTypeInTermPosition { flat, pos: *pos })
             } else {
@@ -2383,6 +2385,7 @@ pub fn subsumption(
     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 {
diff --git a/doc/manual/typing.md b/doc/manual/typing.md
index 8c280bc1..68894b21 100644
--- a/doc/manual/typing.md
+++ b/doc/manual/typing.md
@@ -255,6 +255,90 @@ The following type constructors are available:
   }
   ```
 
+### Subtyping
+
+While distinct types are usually incompatible, some types might actually be
+safely converted to some other types. For example, `{foo = 5}` is inferred to
+have type `{foo : Number}` by default, but is also a valid value of type `{_ :
+Number}`. The latter type is less precise, but might be required for dynamic
+dictionary operations such as `std.record.insert`:
+
+```nickel
+let extended : { _ : Number } =
+  let initial : { foo : Number } = { foo = 5 } in
+  std.record.insert "bar" 5 initial in
+extended
+```
+
+In this example, there is a silent conversion from `{foo : Number}` to `{_ :
+Number}`. This is safe because `foo` is of type `Number`, and it's the only
+field, which means that a value of type `{foo : Number}` is effectively
+dictionary of numbers. In the typing jargon, `{foo : Number}` is said to be a
+*subtype* of `{_ : Number}`. We will write `T <: U` to say that `T` is a subtype
+of `U`: whenever a value of type `U` is expected, we can use a value of type `T`
+as well.
+
+Currently, Nickel supports the following subtyping rule which generalizes the
+example above:
+
+- **Record/Dictionary** subtyping :
+  `{ field1 : T1, ..., fieldn : Tn } <: { _ : T }` if for each `i`, `Ti <: T`
+  That is, a record type is a subtype of a dictionary type if the type of each
+  field is a subtype of the type of dictionary elements.
+
+  Example:
+
+  ```nickel
+  let occurrences : {a : Number, b : Number, c : Number} = {a = 1, b = 3, c = 0} in
+  std.record.map (fun char count => count + 1) occurrences : {_ : Number}
+  ```
+
+Subtyping extends to type constructors in the following way:
+
+- **Equality** : a type is trivially a subtype of itself, that is `T <: T`.
+- **Array**: `Array T <: Array U` if `T <: U`.
+
+  Example:
+
+  ```nickel
+  let block : _ =
+      let array_of_records : Array {a : Number} = [{a = 5}] in
+      let inject_b : Array {_ : Number} -> Array {_ : Number} =
+          std.array.map (fun a => std.record.insert "b" 5 a)
+      in
+
+      inject_b array_of_records
+  in block
+  ```
+
+  Here, `Array {a : Number}` is accepted where `Array {_ : Number}` is expected,
+  because `{a : Number} <: { _ : Number }`.
+- **Dictionary**: similarly, `{ _ : T } <: { _ : U }` if `T <: U`.
+
+  Example:
+
+  ```nickel
+  let block : _ =
+    let dict_of_records : { _ : {a : Number}} = {r = {a = 5}} in
+    let inject_b : { _ : {_ : Number}} -> { _ : {_ : Number}}
+      = std.record.map (fun _ x => std.record.insert "b" 5 x)
+    in
+
+    inject_b dict_of_records in
+  block
+  ```
+
+  Here, `{_ : {a : Number}}` is accepted where `{_ : {_ : Number}}` is expected,
+  because `{a : 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 <:
+T` and `U <: V`. This is not the case in Nickel, for various technical reasons.
+However, you can work around this limitation by expanding a given function:
+If `f` has type `T -> U`, but a value of type `S -> V` is required,
+use `fun x => f x` instead, which has the same runtime behavior
+but isn't typed in the same way.
+
 ### Polymorphism
 
 #### Type polymorphism
diff --git a/lsp/nls/src/field_walker.rs b/lsp/nls/src/field_walker.rs
index b62d68a6..bf5674b8 100644
--- a/lsp/nls/src/field_walker.rs
+++ b/lsp/nls/src/field_walker.rs
@@ -440,7 +440,7 @@ impl<'a> FieldResolver<'a> {
                 let defs = self.resolve_annot(annot);
                 defs.chain(self.resolve_container(term)).collect()
             }
-            Term::Type(typ) => self.resolve_type(typ),
+            Term::Type { typ, contract: _ } => self.resolve_type(typ),
             _ => Default::default(),
         };
 


Test patch:
diff --git a/core/tests/integration/inputs/typecheck/chaining_dictionary_function_record_dictionary_subtyping.ncl b/core/tests/integration/inputs/typecheck/chaining_dictionary_function_record_dictionary_subtyping.ncl
new file mode 100644
index 00000000..a9fa59c1
--- /dev/null
+++ b/core/tests/integration/inputs/typecheck/chaining_dictionary_function_record_dictionary_subtyping.ncl
@@ -0,0 +1,8 @@
+# test.type = 'error'
+# [test.metadata]
+# error = 'EvalError::BlameError'
+let x = {foo = 1, bar = 2} in
+let y = std.record.insert "baz" 5 x in
+let _ = std.record.get "foo" y in
+let z = std.record.remove "foo" y in
+std.record.get "foo" z