Repository: tweag/nickel
Pull request #2072 (2024-10-16 17:09:46)

[RFC007] First step: AST representation
# New AST representation for the (future) bytecode compiler

This is an implementation of the first step of RFC007: define the first AST representation, supposed to be output by the parser.

The whole RFC007 is a big chunk of work; we don't want to implement it all at once and make it the default. This PR creates a new `bytecode` module, which is only enabled under the `bytecode-experimental` feature, so that mainline Nickel is left unchanged, and we can experiment step by step on the side.

## Content

This PR is concerned with the AST design part. It defines a new immutable, arena-allocated AST, that has been cleaned from any runtime concern - this should be the AST as produced by the parser in the future.

Any subpart of `term::Term` that relies explicitely on the `RichTerm` representation has been copied, cleaned and adapted: mostly the patterns, record and array satellite datatypes.

Finally, this PR introduces a `bytecode::compat` module that converts from  the current mainline AST to the new AST, to make sure we haven't overlooked any part and that we have enough methods to build any ast node. This part isn't tested yet but this PR is already huge so we left this for future work.

## AST design guideline

**Important**: this PR doesn't set anything in stone. The size of the AST hasn't been checked or hardcore optimized yet, and we'll probably have to update the representation as we re-implement typechecking, etc. It's rather a first draft, trying to follow a systematic approach.

The AST is designed to be compact and adapted for processing by various analysis phases (mostly typechecking, code analysis by the LSP and compilation by the future bytecode compiler). Thus we've replaced any `Box`/`Rc` by plain immutable references, where the content has been allocated in a centralized arena (actually several ones of them).

For `struct`s, we have no reason to use references - for example, if `struct Foo` has a field `bar: Bar`, there is no good reason to add an indirection `bar: &'ast Bar`. Thus struct fields use owned data as much as possible.

This is the converse for `enum`s: to avoid size bloat, we add reference indirection for any variant where the arguments takes up more than a few words.

Because everything is immutable and shareable, and that we want to avoid heap allocation as much as possible for performance reason (arena allocation should be faster), we don't use `Vec<T>` but `&'ast [T]` instead, which is the immutable equivalent.

We've tried to reduce the variation of the same constructs: while the original AST has two `Let` and `LetPattern`, `Fun` and `FunPattern`, `Record` and `RecRecord`, and so on, this AST merges all those cases. Whilie we take a small size hit for the simplest cases (a `let x = y` now has one indirection, and store the size of a 1 element slice in a fat pointer), this makes the definition and the code consuming it arguably much simpler, and we won't pay this price at runtime since the AST will be compiled away.

Similarly, there's no difference anymore between `UnaryOp`, `BinaryOp`, and `NAryOp` and the corresponding `Op1`, `Op2`, `OpN`: there is only one `PrimOp` type, and one `PrimOpApp` node taking a slice of arguments. Function application is also made multi-ary, which is a more efficient representation for application to multiple arguments and can also help give better error messages during typechecking for over or under-application.

`Type` is the only satellite data that hasn't be replicated. It's a problem because it includes a `Contract` constructor that still refer to the old representation (a `RichTerm`). We can also wonder if we we'd like to arena-allocate the `Type` AST as well, but this is non trivial work and we left it for a follow-up PR.

## Reviewing

The diff is really big, but keep in mind that a lot of code needed to be copy pasted and almost mechanically adapted. I've also added  even more documentation (such as the arguments on primops).

The most interesting is probably type definitions: `Node`, `Ast`, `Pattern`, `PrimOp`, etc. The rest is mostly type-guided implementation.

github-actions[bot]: <h2><a href="https://bencher.dev/perf/nickel/reports/3138e630-e82c-4238-bb29-351c5979f875?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel"><img src="https://bencher.dev/favicon.svg" width="24" height="24" alt="🐰" /> Bencher Report</a></h2><table><tr><td>Branch</td><td><a href="https://bencher.dev/perf/nickel/branches/2072-merge?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">2072/merge</a></td></tr><tr><td>Testbed</td><td><a href="https://bencher.dev/perf/nickel/testbeds/ubuntu-latest?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">ubuntu-latest</a></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><a href="https://bencher.dev/perf/nickel/measures/latency?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">Latency</a></li></ul><p><a href="https://bencher.dev/console/projects/nickel/thresholds/add?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">Click here to create a new Threshold</a><br/>For more information, see <a href="https://bencher.dev/docs/explanation/thresholds/?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">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?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">the <code lang="rust">--ci-only-thresholds</code> CLI flag</a>.</p></blockquote><details><summary>Click to view all benchmark results</summary><br/><table><thead><tr><th>Benchmark</th><th><a href="https://bencher.dev/perf/nickel/measures/latency?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">Latency</a></th><th>nanoseconds (ns)</th></tr></thead><tbody><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/fibonacci-10?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">fibonacci 10</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=3cfaf19e-c9c5-4341-95cd-703456d0fc9f&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>496,090.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/foldl-arrays-50?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">foldl arrays 50</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=95048806-9bf2-49e4-88f2-dbcd66cbf68a&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>1,723,200.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/foldl-arrays-500?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">foldl arrays 500</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=15373c31-496e-4f43-bbb4-466ef49fdd87&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>6,638,100.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/foldr-strings-50?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">foldr strings 50</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=87746452-c4df-48ea-b5e9-8d66f82ca556&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>7,060,100.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/foldr-strings-500?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">foldr strings 500</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=7f141ea0-9fbb-4305-bb63-78f163e546d6&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>62,039,000.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/generate-normal-250?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">generate normal 250</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=8c154d79-dc68-4d93-abb3-83183a62f6a2&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>46,795,000.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/generate-normal-50?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">generate normal 50</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=6d0222f6-0b85-4eaf-8c5c-e8957c522ef9&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>2,050,100.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/generate-normal-unchecked-1000?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">generate normal unchecked 1000</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=be0d3f87-d089-4b81-af44-3bbc6e831697&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>3,264,600.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/generate-normal-unchecked-200?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">generate normal unchecked 200</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=2946df33-45e4-4282-b749-040582021fe3&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>748,800.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/pidigits-100?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">pidigits 100</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=5be25c57-d46f-4b48-b6f0-dee01b84220a&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>3,231,100.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/pipe-normal-20?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">pipe normal 20</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=7178a975-b548-4e78-8c84-4f3802668825&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>1,517,700.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/pipe-normal-200?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">pipe normal 200</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=6884f292-8796-44a8-a30c-d3cb2ed987f6&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>9,971,900.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/product-30?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">product 30</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=2f5f7f6a-4e54-4542-aa09-da5671953fbb&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>836,320.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/scalar-10?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">scalar 10</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=211bb66a-58f8-488b-97e4-7ea032870038&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>1,532,300.00</td></tr><tr><td><a href="https://bencher.dev/perf/nickel/benchmarks/sum-30?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">sum 30</a></td><td>📈 <a href="https://bencher.dev/perf/nickel?branches=0cb58b20-e391-408c-8989-dfcb38a3e42e&heads=1480bd9d-64af-447c-bc37-2377439d3623&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=3f1710c5-ce75-4dfb-aadb-1435fed8a093&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1726507960000&end_time=1729099960000&report=3138e630-e82c-4238-bb29-351c5979f875&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>834,720.00</td></tr></tbody></table></details><a href="https://bencher.dev/perf/nickel/reports/3138e630-e82c-4238-bb29-351c5979f875?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">🐰 View full continuous benchmarking report in Bencher</a><div id="bencher.dev/projects/nickel/id/2072-merge/ubuntu-latest/rust_criterion"></div>
aspiwack: For my understanding, do you actually intent the flat AST to be an output of the parser?
jneem: If I understood this correctly, there's no flat AST: just a tree AST and a bytecode format. This PR is the simplified tree AST produced by the parser. It's simplified compared to current nickel because it doesn't have to support evaluation.
aspiwack: Ah. That's the point I'd missed. Thanks @jneem .

Patch:
diff --git a/Cargo.lock b/Cargo.lock
index 9720d0ed..98138b69 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -307,9 +307,9 @@ dependencies = [
 
 [[package]]
 name = "bumpalo"
-version = "3.15.4"
+version = "3.16.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7ff69b9dd49fd426c69a0db9fc04dd934cdb6645ff000864d98f7e2af8830eaa"
+checksum = "79296716171880943b8470b5f8d03aa55eb2e645a4874bdbb28adb49162e012c"
 
 [[package]]
 name = "bytemuck"
@@ -1840,6 +1840,7 @@ version = "0.9.0"
 dependencies = [
  "ansi_term",
  "assert_matches",
+ "bumpalo",
  "clap 4.5.2",
  "codespan",
  "codespan-reporting",
diff --git a/Cargo.toml b/Cargo.toml
index 0c0026ef..8c13d089 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -98,6 +98,7 @@ toml = "0.8"
 typed-arena = "2.0.2"
 unicode-segmentation = "1.10.1"
 void = "1"
+bumpalo = "3.16.0"
 
 metrics = "0.21"
 metrics-util = "0.15"
diff --git a/cli/src/typecheck.rs b/cli/src/typecheck.rs
index 76d05900..eed375da 100644
--- a/cli/src/typecheck.rs
+++ b/cli/src/typecheck.rs
@@ -1,3 +1,5 @@
+use nickel_lang_core::typecheck::TypecheckMode;
+
 use crate::{
     cli::GlobalOptions,
     customize::NoCustomizeMode,
@@ -9,11 +11,32 @@ use crate::{
 pub struct TypecheckCommand {
     #[command(flatten)]
     inputs: InputOptions<NoCustomizeMode>,
+
+    /// Start the type-checker in strict mode, so that the entire input is treated as a typed block.
+    #[arg(long, global = true)]
+    pub strict_typechecking: bool,
 }
 
 impl TypecheckCommand {
     pub fn run(self, global: GlobalOptions) -> CliResult<()> {
+        if self.strict_typechecking {
+            // In strict mode we run *both* forms of typechecking, because in
+            // fact neither one is more strict than the other. For example,
+            // given the input
+            //
+            // let x = (1 + 1) in (x + 1 : Number)
+            //
+            // typechecking in "enforce" mode will succeed because it will infer
+            // `x: Number`, while typechecking in walk mode will fail because it
+            // will treat `x` as `Dyn` and then try to typecheck `x + 1`.
+            let mut program = self.inputs.prepare(&global)?;
+            program
+                .typecheck(TypecheckMode::Enforce)
+                .report_with_program(program)?;
+        }
         let mut program = self.inputs.prepare(&global)?;
-        program.typecheck().report_with_program(program)
+        program
+            .typecheck(TypecheckMode::Walk)
+            .report_with_program(program)
     }
 }
diff --git a/core/Cargo.toml b/core/Cargo.toml
index 8d636e29..783f3664 100644
--- a/core/Cargo.toml
+++ b/core/Cargo.toml
@@ -27,6 +27,7 @@ doc = ["dep:comrak"]
 format = ["dep:topiary-core", "dep:topiary-queries", "dep:tree-sitter-nickel"]
 metrics = ["dep:metrics"]
 nix-experimental = [ "dep:cxx", "dep:cxx-build", "dep:pkg-config" ]
+bytecode-experimental = ["dep:bumpalo"]
 spanned-deser = ["dep:serde-untagged"]
 benchmark-ci = []
 
@@ -85,6 +86,8 @@ tree-sitter-nickel = { workspace = true, optional = true }
 metrics = { workspace = true, optional = true }
 strsim = "0.10.0"
 
+bumpalo = { workspace = true, optional = true }
+
 [dev-dependencies]
 pretty_assertions.workspace = true
 assert_matches.workspace = true
diff --git a/core/src/bytecode/ast/compat.rs b/core/src/bytecode/ast/compat.rs
new file mode 100644
index 00000000..5ae1b6b9
--- /dev/null
+++ b/core/src/bytecode/ast/compat.rs
@@ -0,0 +1,541 @@
+//! Compatibility with the current stable Nickel version.
+//!
+//! This module defines a trait for converting from the representation used in stable Nickel to the
+//! new AST representation of the bytecode compiler, and implements it for the types defined in
+//! [crate::bytecode::ast].
+
+use super::{primop::PrimOp, *};
+use crate::term;
+
+/// Convert from the mainline Nickel representation to the new AST representation. This trait is
+/// mostly `From` with an additional argument for the allocator.
+///
+/// # Parameters
+///
+/// - `'ast`: the lifetime of the AST nodes, tied to the allocator
+/// - `'a`: the lifetime of the reference to the mainline Nickel object, which doesn't need to be
+///   related to `'ast` (we will copy any required data into the allocator)
+/// - `T`: the type of the mainline Nickel object ([term::Term], [term::pattern::Pattern], etc.)
+pub trait FromMainline<'ast, T> {
+    fn from_mainline(alloc: &'ast AstAlloc, mainline: &T) -> Self;
+}
+
+impl<'ast> FromMainline<'ast, term::pattern::Pattern> for &'ast Pattern<'ast> {
+    fn from_mainline(
+        alloc: &'ast AstAlloc,
+        pattern: &term::pattern::Pattern,
+    ) -> &'ast Pattern<'ast> {
+        alloc.move_pattern(pattern.to_ast(alloc))
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::pattern::Pattern> for Pattern<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, pattern: &term::pattern::Pattern) -> Self {
+        Pattern {
+            data: pattern.data.to_ast(alloc),
+            alias: pattern.alias,
+            pos: pattern.pos,
+        }
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::pattern::PatternData> for PatternData<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, data: &term::pattern::PatternData) -> Self {
+        match data {
+            term::pattern::PatternData::Wildcard => PatternData::Wildcard,
+            term::pattern::PatternData::Any(id) => PatternData::Any(*id),
+            term::pattern::PatternData::Record(record_pattern) => record_pattern.to_ast(alloc),
+            term::pattern::PatternData::Array(array_pattern) => array_pattern.to_ast(alloc),
+            term::pattern::PatternData::Enum(enum_pattern) => enum_pattern.to_ast(alloc),
+            term::pattern::PatternData::Constant(constant_pattern) => {
+                constant_pattern.to_ast(alloc)
+            }
+            term::pattern::PatternData::Or(or_pattern) => or_pattern.to_ast(alloc),
+        }
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::pattern::RecordPattern> for PatternData<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, record_pat: &term::pattern::RecordPattern) -> Self {
+        let patterns = record_pat
+            .patterns
+            .iter()
+            .map(|field_pattern| field_pattern.to_ast(alloc));
+
+        let tail = match record_pat.tail {
+            term::pattern::TailPattern::Empty => TailPattern::Empty,
+            term::pattern::TailPattern::Open => TailPattern::Open,
+            term::pattern::TailPattern::Capture(id) => TailPattern::Capture(id),
+        };
+
+        PatternData::Record(alloc.record_pattern(patterns, tail, record_pat.pos))
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::pattern::FieldPattern> for FieldPattern<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, field_pat: &term::pattern::FieldPattern) -> Self {
+        let pattern = field_pat.pattern.to_ast(alloc);
+
+        let default = field_pat.default.as_ref().map(|term| term.to_ast(alloc));
+
+        let annotation = field_pat.annotation.to_ast(alloc);
+
+        FieldPattern {
+            matched_id: field_pat.matched_id,
+            annotation,
+            default,
+            pattern,
+            pos: field_pat.pos,
+        }
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::pattern::ArrayPattern> for PatternData<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, array_pat: &term::pattern::ArrayPattern) -> Self {
+        let patterns = array_pat.patterns.iter().map(|pat| pat.to_ast(alloc));
+
+        let tail = match array_pat.tail {
+            term::pattern::TailPattern::Empty => TailPattern::Empty,
+            term::pattern::TailPattern::Open => TailPattern::Open,
+            term::pattern::TailPattern::Capture(id) => TailPattern::Capture(id),
+        };
+
+        PatternData::Array(alloc.array_pattern(patterns, tail, array_pat.pos))
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::pattern::EnumPattern> for PatternData<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, enum_pat: &term::pattern::EnumPattern) -> Self {
+        let pattern = enum_pat.pattern.as_ref().map(|pat| (**pat).to_ast(alloc));
+        PatternData::Enum(alloc.enum_pattern(enum_pat.tag, pattern, enum_pat.pos))
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::pattern::ConstantPattern> for PatternData<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, pattern: &term::pattern::ConstantPattern) -> Self {
+        let data = match &pattern.data {
+            term::pattern::ConstantPatternData::Bool(b) => ConstantPatternData::Bool(*b),
+            term::pattern::ConstantPatternData::Number(n) => {
+                ConstantPatternData::Number(alloc.generic_arena.alloc(n.clone()))
+            }
+            term::pattern::ConstantPatternData::String(s) => {
+                ConstantPatternData::String(alloc.generic_arena.alloc_str(s))
+            }
+            term::pattern::ConstantPatternData::Null => ConstantPatternData::Null,
+        };
+
+        PatternData::Constant(alloc.constant_pattern(data, pattern.pos))
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::pattern::OrPattern> for PatternData<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, pattern: &term::pattern::OrPattern) -> Self {
+        let patterns = pattern
+            .patterns
+            .iter()
+            .map(|pat| pat.to_ast(alloc))
+            .collect::<Vec<_>>();
+
+        PatternData::Or(alloc.or_pattern(patterns, pattern.pos))
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::TypeAnnotation> for Annotation<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, annot: &term::TypeAnnotation) -> Self {
+        let typ = annot.typ.as_ref().map(|typ| typ.typ.clone());
+
+        let contracts = alloc
+            .type_arena
+            .alloc_extend(annot.contracts.iter().map(|contract| contract.typ.clone()));
+
+        Annotation { typ, contracts }
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::record::Field> for record::Field<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, field: &term::record::Field) -> Self {
+        record::Field {
+            value: field.value.as_ref().map(|term| term.to_ast(alloc)),
+            metadata: field.metadata.to_ast(alloc),
+        }
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::record::FieldMetadata> for record::FieldMetadata<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, metadata: &term::record::FieldMetadata) -> Self {
+        let doc = metadata.doc.as_ref().map(|doc| rc::Rc::from(doc.as_str()));
+
+        record::FieldMetadata {
+            doc,
+            annotation: metadata.annotation.to_ast(alloc),
+            opt: metadata.opt,
+            not_exported: metadata.not_exported,
+            priority: metadata.priority.clone(),
+        }
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::Term> for &'ast Node<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, term: &term::Term) -> Self {
+        use term::Term;
+
+        match term {
+            Term::Null => alloc.null(),
+            Term::Bool(b) => alloc.bool(*b),
+            Term::Num(n) => alloc.number(n.clone()),
+            Term::Str(s) => alloc.string(s),
+            Term::StrChunks(chunks) => alloc.str_chunks(
+                chunks
+                    .iter()
+                    .map(|chunk| match chunk {
+                        term::StrChunk::Literal(s) => StrChunk::Literal(s.clone()),
+                        term::StrChunk::Expr(expr, indent) => {
+                            StrChunk::Expr(expr.to_ast(alloc), *indent)
+                        }
+                    })
+                    .rev(),
+            ),
+            Term::Fun(id, body) => alloc.fun(
+                alloc.generic_arena.alloc(Pattern::any(*id)),
+                body.to_ast(alloc),
+            ),
+            Term::FunPattern(pat, body) => alloc.fun(pat.to_ast(alloc), body.to_ast(alloc)),
+            Term::Let(bindings, body, attrs) => alloc.let_binding(
+                bindings
+                    .iter()
+                    .map(|(id, term)| (Pattern::any(*id), term.to_ast(alloc))),
+                body.to_ast(alloc),
+                attrs.rec,
+            ),
+            Term::LetPattern(bindings, body, attrs) => alloc.let_binding(
+                bindings
+                    .iter()
+                    .map(|(pat, term)| (pat.to_ast(alloc), term.to_ast(alloc))),
+                body.to_ast(alloc),
+                attrs.rec,
+            ),
+            Term::App(fun, arg) => {
+                match fun.as_ref() {
+                    // We have to special-case if-then-else, which is encoded as a primop application
+                    // of the unary operator if-then-else to the condition, followed by two normal
+                    // applications for the if and else branches, which is a bit painful to match.
+                    Term::App(fun_inner, arg_inner)
+                        if matches!(
+                            fun_inner.as_ref(),
+                            Term::Op1(term::UnaryOp::IfThenElse, _)
+                        ) =>
+                    {
+                        if let Term::Op1(term::UnaryOp::IfThenElse, cond) = fun_inner.as_ref() {
+                            return alloc.if_then_else(
+                                cond.to_ast(alloc),
+                                arg_inner.to_ast(alloc),
+                                arg.to_ast(alloc),
+                            );
+                        }
+                    }
+                    _ => (),
+                };
+
+                let mut args = vec![arg.to_ast(alloc)];
+                let mut maybe_next_app = fun.as_ref();
+
+                while let Term::App(next_fun, next_arg) = maybe_next_app {
+                    args.push(next_arg.to_ast(alloc));
+                    maybe_next_app = next_fun.as_ref();
+                }
+
+                alloc.app(fun.to_ast(alloc), args.into_iter().rev())
+            }
+            Term::Var(id) => alloc.var(*id),
+            Term::Enum(id) => alloc.enum_variant(*id, None),
+            Term::EnumVariant { tag, arg, attrs: _ } => {
+                alloc.enum_variant(*tag, Some(arg.to_ast(alloc)))
+            }
+            Term::RecRecord(data, dyn_fields, _deps) => {
+                let stat_fields = alloc.generic_arena.alloc_slice_fill_iter(
+                    data.fields
+                        .iter()
+                        .map(|(id, field)| (*id, field.to_ast(alloc))),
+                );
+
+                let dyn_fields = alloc.generic_arena.alloc_slice_fill_iter(
+                    dyn_fields
+                        .iter()
+                        .map(|(expr, field)| (expr.to_ast(alloc), field.to_ast(alloc))),
+                );
+
+                let open = data.attrs.open;
+
+                alloc.record(Record {
+                    stat_fields,
+                    dyn_fields,
+                    open,
+                })
+            }
+            Term::Record(data) => {
+                let stat_fields = alloc.generic_arena.alloc_slice_fill_iter(
+                    data.fields
+                        .iter()
+                        .map(|(id, field)| (*id, field.to_ast(alloc))),
+                );
+
+                let open = data.attrs.open;
+
+                alloc.record(Record {
+                    stat_fields,
+                    dyn_fields: alloc
+                        .generic_arena
+                        .alloc_slice_fill_iter(std::iter::empty()),
+                    open,
+                })
+            }
+            Term::Match(data) => {
+                let branches = data.branches.iter().map(|branch| MatchBranch {
+                    pattern: branch.pattern.to_ast(alloc),
+                    guard: branch.guard.as_ref().map(|term| term.to_ast(alloc)),
+                    body: branch.body.to_ast(alloc),
+                });
+
+                alloc.match_expr(branches)
+            }
+            Term::Array(data, _attrs) => {
+                // We should probably make array's iterator an ExactSizeIterator. But for now, we
+                // don't care about the translation's performance so it's simpler to just collect
+                // them in a vec locally.
+                let elts = data
+                    .iter()
+                    .map(|term| term.to_ast(alloc))
+                    .collect::<Vec<_>>();
+                alloc.array(elts)
+            }
+            Term::Op1(op, arg) => {
+                alloc.prim_op(PrimOp::from(op), std::iter::once(arg.to_ast(alloc)))
+            }
+            Term::Op2(op, arg1, arg2) => {
+                // [^primop-argument-order]: Some primops have had exotic arguments order for
+                // historical reasons. The new AST tries to follow the stdlib argument order
+                // whenever possible, which means we have to swap the arguments for a few primops.
+
+                let op = PrimOp::from(op);
+                let mut args = [arg1.to_ast(alloc), arg2.to_ast(alloc)];
+
+                if matches!(op, PrimOp::ArrayAt | PrimOp::StringContains) {
+                    args.swap(0, 1);
+                }
+
+                alloc.prim_op(op, args)
+            }
+            Term::OpN(op, args) => {
+                // See [^primop-argument-order].
+                let op = PrimOp::from(op);
+                let mut args: Vec<_> = args.iter().map(|arg| arg.to_ast(alloc)).collect();
+                if let PrimOp::StringSubstr = op {
+                    debug_assert_eq!(args.len(), 3);
+                    // The original order is: the string, then start and end.
+                    // The target order is: start, end and then the string.
+                    args.swap(0, 1);
+                    args.swap(1, 2);
+                }
+
+                alloc.prim_op(op, args)
+            }
+            Term::SealingKey(_) => panic!("didn't expect a sealing key at the first stage"),
+            Term::Sealed(..) => panic!("didn't expect a sealed term at the first stage"),
+            Term::Annotated(annot, term) => {
+                alloc.annotated(annot.to_ast(alloc), term.to_ast(alloc))
+            }
+            Term::Import { path, format } => alloc.import(path.clone(), *format),
+            Term::ResolvedImport(_) => panic!("didn't expect a resolved import at parsing stage"),
+            Term::Type { typ, .. } => alloc.typ(typ.clone()),
+            Term::CustomContract(_) => panic!("didn't expect a custom contract at parsing stage"),
+            Term::ParseError(error) => alloc.parse_error(error.clone()),
+            Term::RuntimeError(_) => panic!("didn't expect a runtime error at parsing stage"),
+            Term::Closure(_) => panic!("didn't expect a closure at parsing stage"),
+            Term::ForeignId(_) => panic!("didn't expect a foreign id at parsing stage"),
+            _ => unimplemented!(),
+        }
+    }
+}
+
+impl<'ast> FromMainline<'ast, term::RichTerm> for Ast<'ast> {
+    fn from_mainline(alloc: &'ast AstAlloc, rterm: &term::RichTerm) -> Self {
+        alloc.ast(rterm.as_ref().to_ast(alloc), rterm.pos)
+    }
+}
+
+/// Symmetric to `FromMainline`, as `Into` is to `From`.
+pub trait ToAst<'ast, T> {
+    fn to_ast(&self, alloc: &'ast AstAlloc) -> T;
+}
+
+impl<'ast, S, T> ToAst<'ast, T> for S
+where
+    T: FromMainline<'ast, S>,
+{
+    fn to_ast(&self, alloc: &'ast AstAlloc) -> T {
+        T::from_mainline(alloc, self)
+    }
+}
+
+// Primops don't need any heap allocation, so we can implement `From` directly.
+impl From<&term::UnaryOp> for PrimOp {
+    fn from(op: &term::UnaryOp) -> Self {
+        match op {
+            term::UnaryOp::IfThenElse => {
+                panic!("if-then-else should have been handed separately by special casing")
+            }
+            term::UnaryOp::Typeof => PrimOp::Typeof,
+            term::UnaryOp::BoolAnd => PrimOp::BoolAnd,
+            term::UnaryOp::BoolOr => PrimOp::BoolOr,
+            term::UnaryOp::BoolNot => PrimOp::BoolNot,
+            term::UnaryOp::Blame => PrimOp::Blame,
+            term::UnaryOp::EnumEmbed(loc_ident) => PrimOp::EnumEmbed(*loc_ident),
+            term::UnaryOp::RecordAccess(loc_ident) => PrimOp::RecordStatAccess(*loc_ident),
+            term::UnaryOp::ArrayMap => PrimOp::ArrayMap,
+            term::UnaryOp::RecordMap => PrimOp::RecordMap,
+            term::UnaryOp::LabelFlipPol => PrimOp::LabelFlipPol,
+            term::UnaryOp::LabelPol => PrimOp::LabelPol,
+            term::UnaryOp::LabelGoDom => PrimOp::LabelGoDom,
+            term::UnaryOp::LabelGoCodom => PrimOp::LabelGoCodom,
+            term::UnaryOp::LabelGoArray => PrimOp::LabelGoArray,
+            term::UnaryOp::LabelGoDict => PrimOp::LabelGoDict,
+            term::UnaryOp::Seq => PrimOp::Seq,
+            term::UnaryOp::DeepSeq => PrimOp::DeepSeq,
+            term::UnaryOp::ArrayLength => PrimOp::ArrayLength,
+            term::UnaryOp::ArrayGen => PrimOp::ArrayGen,
+            term::UnaryOp::RecordFields(record_op_kind) => {
+                PrimOp::RecordFields((*record_op_kind).into())
+            }
+            term::UnaryOp::RecordValues => PrimOp::RecordValues,
+            term::UnaryOp::StringTrim => PrimOp::StringTrim,
+            term::UnaryOp::StringChars => PrimOp::StringChars,
+            term::UnaryOp::StringUppercase => PrimOp::StringUppercase,
+            term::UnaryOp::StringLowercase => PrimOp::StringLowercase,
+            term::UnaryOp::StringLength => PrimOp::StringLength,
+            term::UnaryOp::ToString => PrimOp::ToString,
+            term::UnaryOp::NumberFromString => PrimOp::NumberFromString,
+            term::UnaryOp::EnumFromString => PrimOp::EnumFromString,
+            term::UnaryOp::StringIsMatch => PrimOp::StringIsMatch,
+            term::UnaryOp::StringFind => PrimOp::StringFind,
+            term::UnaryOp::StringFindAll => PrimOp::StringFindAll,
+            term::UnaryOp::Force {
+                ignore_not_exported,
+            } => PrimOp::Force {
+                ignore_not_exported: *ignore_not_exported,
+            },
+            term::UnaryOp::RecordEmptyWithTail => PrimOp::RecordEmptyWithTail,
+            term::UnaryOp::Trace => PrimOp::Trace,
+            term::UnaryOp::LabelPushDiag => PrimOp::LabelPushDiag,
+            #[cfg(feature = "nix-experimental")]
+            term::UnaryOp::EvalNix => PrimOp::EvalNix,
+            term::UnaryOp::EnumGetArg => PrimOp::EnumGetArg,
+            term::UnaryOp::EnumMakeVariant => PrimOp::EnumMakeVariant,
+            term::UnaryOp::EnumIsVariant => PrimOp::EnumIsVariant,
+            term::UnaryOp::EnumGetTag => PrimOp::EnumGetTag,
+            term::UnaryOp::ContractCustom => PrimOp::ContractCustom,
+            term::UnaryOp::NumberArcCos => PrimOp::NumberArcCos,
+            term::UnaryOp::NumberArcSin => PrimOp::NumberArcSin,
+            term::UnaryOp::NumberArcTan => PrimOp::NumberArcTan,
+            term::UnaryOp::NumberCos => PrimOp::NumberCos,
+            term::UnaryOp::NumberSin => PrimOp::NumberSin,
+            term::UnaryOp::NumberTan => PrimOp::NumberTan,
+
+            op @ (term::UnaryOp::TagsOnlyMatch { .. }
+            | term::UnaryOp::ChunksConcat
+            | term::UnaryOp::StringIsMatchCompiled(_)
+            | term::UnaryOp::StringFindCompiled(_)
+            | term::UnaryOp::StringFindAllCompiled(_)
+            | term::UnaryOp::RecDefault
+            | term::UnaryOp::RecForce
+            | term::UnaryOp::PatternBranch
+            | term::UnaryOp::ContractPostprocessResult) => {
+                panic!("didn't expect {op} at the parsing stage")
+            }
+        }
+    }
+}
+
+impl From<&term::BinaryOp> for PrimOp {
+    fn from(op: &term::BinaryOp) -> Self {
+        match op {
+            term::BinaryOp::Plus => PrimOp::Plus,
+            term::BinaryOp::Sub => PrimOp::Sub,
+            term::BinaryOp::Mult => PrimOp::Mult,
+            term::BinaryOp::Div => PrimOp::Div,
+            term::BinaryOp::Modulo => PrimOp::Modulo,
+            term::BinaryOp::NumberArcTan2 => PrimOp::NumberArcTan2,
+            term::BinaryOp::NumberLog => PrimOp::NumberLog,
+            term::BinaryOp::Pow => PrimOp::Pow,
+            term::BinaryOp::StringConcat => PrimOp::StringConcat,
+            term::BinaryOp::Eq => PrimOp::Eq,
+            term::BinaryOp::LessThan => PrimOp::LessThan,
+            term::BinaryOp::LessOrEq => PrimOp::LessOrEq,
+            term::BinaryOp::GreaterThan => PrimOp::GreaterThan,
+            term::BinaryOp::GreaterOrEq => PrimOp::GreaterOrEq,
+            term::BinaryOp::ContractApply => PrimOp::ContractApply,
+            term::BinaryOp::ContractCheck => PrimOp::ContractCheck,
+            term::BinaryOp::LabelWithErrorData => PrimOp::LabelWithErrorData,
+            term::BinaryOp::LabelGoField => PrimOp::LabelGoField,
+            // This corresponds to a call to `%record/insert%` from the source language. Other
+            // forms are introduced by the evaluator, e.g. when evaluating a recursive record to a
+            // record.
+            term::BinaryOp::RecordInsert {
+                metadata,
+                pending_contracts,
+                ext_kind,
+                op_kind,
+            } if metadata.is_empty()
+                && pending_contracts.is_empty()
+                && *ext_kind == term::RecordExtKind::WithValue =>
+            {
+                PrimOp::RecordInsert((*op_kind).into())
+            }
+            term::BinaryOp::RecordRemove(record_op_kind) => {
+                PrimOp::RecordRemove((*record_op_kind).into())
+            }
+            term::BinaryOp::RecordGet => PrimOp::RecordGet,
+            term::BinaryOp::RecordHasField(record_op_kind) => {
+                PrimOp::RecordHasField((*record_op_kind).into())
+            }
+            term::BinaryOp::RecordFieldIsDefined(record_op_kind) => {
+                PrimOp::RecordFieldIsDefined((*record_op_kind).into())
+            }
+            term::BinaryOp::RecordSplitPair => PrimOp::RecordSplitPair,
+            term::BinaryOp::RecordDisjointMerge => PrimOp::RecordDisjointMerge,
+            term::BinaryOp::ArrayConcat => PrimOp::ArrayConcat,
+            term::BinaryOp::ArrayAt => PrimOp::ArrayAt,
+            term::BinaryOp::Merge(merge_label) => PrimOp::Merge(merge_label.kind),
+            term::BinaryOp::Hash => PrimOp::Hash,
+            term::BinaryOp::Serialize => PrimOp::Serialize,
+            term::BinaryOp::Deserialize => PrimOp::Deserialize,
+            term::BinaryOp::StringSplit => PrimOp::StringSplit,
+            term::BinaryOp::StringContains => PrimOp::StringContains,
+            term::BinaryOp::StringCompare => PrimOp::StringCompare,
+            term::BinaryOp::ContractArrayLazyApp => PrimOp::ContractArrayLazyApp,
+            term::BinaryOp::ContractRecordLazyApp => PrimOp::ContractRecordLazyApp,
+            term::BinaryOp::LabelWithMessage => PrimOp::LabelWithMessage,
+            term::BinaryOp::LabelWithNotes => PrimOp::LabelWithNotes,
+            term::BinaryOp::LabelAppendNote => PrimOp::LabelAppendNote,
+            term::BinaryOp::LabelLookupTypeVar => PrimOp::LabelLookupTypeVar,
+
+            op @ (term::BinaryOp::RecordInsert { .. }
+            | term::BinaryOp::Unseal
+            | term::BinaryOp::Seal) => panic!("didn't expect {op} at the parsing stage"),
+        }
+    }
+}
+
+impl From<&term::NAryOp> for PrimOp {
+    fn from(op: &term::NAryOp) -> Self {
+        match op {
+            term::NAryOp::StringReplace => PrimOp::StringReplace,
+            term::NAryOp::StringReplaceRegex => PrimOp::StringReplaceRegex,
+            term::NAryOp::StringSubstr => PrimOp::StringSubstr,
+            term::NAryOp::MergeContract => PrimOp::MergeContract,
+            term::NAryOp::RecordSealTail => PrimOp::RecordSealTail,
+            term::NAryOp::RecordUnsealTail => PrimOp::RecordUnsealTail,
+            term::NAryOp::LabelInsertTypeVar => PrimOp::LabelInsertTypeVar,
+            term::NAryOp::ArraySlice => PrimOp::ArraySlice,
+        }
+    }
+}
diff --git a/core/src/bytecode/ast/mod.rs b/core/src/bytecode/ast/mod.rs
new file mode 100644
index 00000000..8479ee31
--- /dev/null
+++ b/core/src/bytecode/ast/mod.rs
@@ -0,0 +1,521 @@
+//! The Nickel AST, as ingested by the bytecode compiler.
+//!
+//! Since the AST is built once for each Nickel expression and is then compiled away to bytecode,
+//! the number nodes ever allocated should be reasonably bounded by the input program size. Thus,
+//! for performance reasons, we allocate notes using an arena and keep them alive until the end of
+//! compilation. In return, we get fast allocation and de-allocation, and we can easily reference
+//! other nodes and data structures using native references.
+//!
+//! The corresponding lifetime of all the nodes - and thus of the arena as well - is consistently
+//! called `'ast`.
+
+use std::{ffi::OsString, rc};
+
+use pattern::Pattern;
+use record::Record;
+
+use crate::{
+    cache::InputFormat, error::ParseError, identifier::LocIdent, position::TermPos, typ::Type,
+};
+
+// For now, we reuse those types from the term module.
+pub use crate::term::{Number, StrChunk};
+
+use bumpalo::Bump;
+
+pub mod compat;
+pub mod pattern;
+pub mod primop;
+pub mod record;
+
+use pattern::*;
+use primop::PrimOp;
+
+/// A Nickel AST. Contains a root node and a span.
+///
+/// Both members are references so that `Ast` is cheap to clone - it's in fact `Copy` - and to
+/// store. Additionally, we don't expect to access the span much on the happy path, so the
+/// indirection should be ok.
+#[derive(Clone, Copy, Debug, PartialEq)]
+pub struct Ast<'ast> {
+    node: &'ast Node<'ast>,
+    pos: &'ast TermPos,
+}
+
+/// A node of the Nickel AST.
+///
+/// Nodes are built by the parser and then mostly traversed immutably. Such nodes are optimized for
+/// sharing (hence immutability) and for size, as the size of an enum can grow quite quickly in
+/// Rust. In particular, any data that is bigger than a few words isn't usually owned but rather a
+/// reference to some arena-allocated data
+///
+/// Using an arena has another advantage: the data is allocated in the same order as the AST is
+/// built. This means that even if there are reference indirections, the children of a node are
+/// most likely close to the node itself in memory, which should be good for cache locality.
+#[derive(Clone, Debug, PartialEq, Default)]
+pub enum Node<'ast> {
+    /// The null value.
+    #[default]
+    Null,
+
+    /// A boolean value.
+    Bool(bool),
+
+    /// A number.
+    ///
+    /// A number is an arbitrary-precision rational in Nickel. It's not small and thus we put it
+    /// behind a reference to avoid size bloat.
+    Number(&'ast Number),
+
+    /// A string literal.
+    String(&'ast str),
+
+    /// A string containing interpolated expressions, represented as a list of either literals or
+    /// expressions.
+    ///
+    /// As opposed to [crate::term::Term::StrChunks], the chunks are stored in the original order:
+    /// `"hello%{var}"` will give `["hello", var]`.
+    StrChunks(&'ast [StrChunk<Ast<'ast>>]),
+
+    /// A function.
+    Fun(&'ast Pattern<'ast>, Ast<'ast>),
+
+    /// A let-binding.
+    Let {
+        bindings: &'ast [(Pattern<'ast>, Ast<'ast>)],
+        body: Ast<'ast>,
+        rec: bool,
+    },
+
+    /// An application to one or more arguments.
+    App {
+        fun: Ast<'ast>,
+        args: &'ast [Ast<'ast>],
+    },
+
+    /// A variable.
+    Var(LocIdent),
+
+    /// An enum variant (an algebraic datatype).
+    ///
+    /// Variants have at most one argument: variants with no arguments are often called simply
+    /// enum tags. Note that one can just use a record as an argument to emulate variants with
+    /// multiple arguments.
+    EnumVariant {
+        tag: LocIdent,
+        arg: Option<Ast<'ast>>,
+    },
+
+    /// A record.
+    Record(&'ast Record<'ast>),
+
+    /// An if-then-else expression.
+    IfThenElse {
+        cond: Ast<'ast>,
+        then_branch: Ast<'ast>,
+        else_branch: Ast<'ast>,
+    },
+
+    /// A match expression. This expression is still to be applied to an argument to match on.
+    Match(Match<'ast>),
+
+    /// An array.
+    Array(&'ast [Ast<'ast>]),
+
+    /// An n-ary primitive operation application. As opposed to a traditional function application:
+    ///
+    /// 1. The function part is necessarily a primitive operation.
+    /// 2. The arguments are forced before entering the
+    PrimOpApp {
+        op: &'ast PrimOp,
+        args: &'ast [Ast<'ast>],
+    },
+
+    /// A term with a type and/or contract annotation.
+    Annotated {
+        annot: &'ast Annotation<'ast>,
+        inner: Ast<'ast>,
+    },
+
+    /// An import.
+    Import {
+        path: &'ast OsString,
+        format: InputFormat,
+    },
+
+    /// A type in term position, such as in `let my_contract = Number -> Number in ...`.
+    ///
+    /// During evaluation, this will get turned into a contract.
+    Type(&'ast Type),
+
+    /// A term that couldn't be parsed properly. Used by the LSP to handle partially valid
+    /// programs.
+    ParseError(&'ast ParseError),
+}
+
+/// A flavor for record operations. By design, we want empty optional values to be transparent for
+/// record operations, because they would otherwise make many operations fail spuriously (e.g.
+/// trying to map over such an empty value). So they are most of the time silently ignored.
+///
+/// However, it's sometimes useful and even necessary to take them into account. This behavior is
+/// controlled by [RecordOpKind].
+#[derive(Clone, Debug, PartialEq, Eq, Copy, Default)]
+pub enum RecordOpKind {
+    #[default]
+    IgnoreEmptyOpt,
+    ConsiderAllFields,
+}
+
+/// A branch of a match expression.
+#[derive(Debug, PartialEq, Clone)]
+pub struct MatchBranch<'ast> {
+    /// The pattern on the left hand side of `=>`.
+    pub pattern: Pattern<'ast>,
+    /// A potential guard, which is an additional side-condition defined as `if cond`. The value
+    /// stored in this field is the boolean condition itself.
+    pub guard: Option<Ast<'ast>>,
+    /// The body of the branch, on the right hand side of `=>`.
+    pub body: Ast<'ast>,
+}
+
+/// Content of a match expression.
+#[derive(Debug, PartialEq, Clone, Copy)]
+pub struct Match<'ast> {
+    /// Branches of the match expression, where the first component is the pattern on the left hand
+    /// side of `=>` and the second component is the body of the branch.
+    pub branches: &'ast [MatchBranch<'ast>],
+}
+
+/// A type and/or contract annotation.
+#[derive(Debug, PartialEq, Clone, Default)]
+pub struct Annotation<'ast> {
+    /// The type annotation (using `:`).
+    pub typ: Option<Type>,
+
+    /// The contract annotations (using `|`).
+    pub contracts: &'ast [Type],
+}
+
+impl<'ast> Annotation<'ast> {
+    /// Returns the main annotation, which is either the type annotation if any, or the first
+    /// contract annotation.
+    pub fn first(&'ast self) -> Option<&'ast Type> {
+        self.typ.as_ref().or(self.contracts.iter().next())
+    }
+
+    /// Iterates over the annotations, starting by the type and followed by the contracts.
+    pub fn iter(&'ast self) -> impl Iterator<Item = &'ast Type> {
+        self.typ.iter().chain(self.contracts.iter())
+    }
+
+    /// Returns a string representation of the contracts (without the static type annotation) as a
+    /// comma-separated list.
+    pub fn contracts_to_string(&self) -> Option<String> {
+        (!self.contracts.is_empty()).then(|| {
+            self.contracts
+                .iter()
+                .map(|typ| format!("{typ}"))
+                .collect::<Vec<_>>()
+                .join(",")
+        })
+    }
+
+    /// Returns `true` if this annotation is empty, i.e. hold neither a type annotation nor
+    /// contracts annotations.
+    pub fn is_empty(&self) -> bool {
+        self.typ.is_none() && self.contracts.is_empty()
+    }
+}
+
+/// Owns the arenas required to allocate new AST nodes and provide builder methods to create them.
+///
+/// # Drop and arena allocation
+///
+/// The most popular choice for arena is the `bumpalo` crate, which is a fast bump allocator that
+/// can handle heterogeneous data. However, it doesn't support destructors, which is a problem
+/// because some of the nodes in the AST owns heap allocated data and needs to be de-allocated
+/// (`Number`, `Type` and parse errors currently).
+///
+/// Another choice is `typed-arena` and derivatives, which do run destructors, but can only store
+/// one type of values. As the number of types that need to be dropped is relatively small, we use
+/// a general `bumpalo` arena by default, and specialized typed arenas for stuff that need to be
+/// dropped.
+pub struct AstAlloc {
+    generic_arena: Bump,
+    type_arena: typed_arena::Arena<Type>,
+    number_arena: typed_arena::Arena<Number>,
+    error_arena: typed_arena::Arena<ParseError>,
+}
+
+impl AstAlloc {
+    /// Create a new ast allocator.
+    pub fn new() -> Self {
+        Self {
+            generic_arena: Bump::new(),
+            type_arena: typed_arena::Arena::new(),
+            number_arena: typed_arena::Arena::new(),
+            error_arena: typed_arena::Arena::new(),
+        }
+    }
+
+    pub fn null(&self) -> &Node<'_> {
+        self.generic_arena.alloc(Node::Null)
+    }
+
+    pub fn bool(&self, value: bool) -> &Node<'_> {
+        self.generic_arena.alloc(Node::Bool(value))
+    }
+
+    pub fn number(&self, number: Number) -> &Node<'_> {
+        let number = self.number_arena.alloc(number);
+        self.generic_arena.alloc(Node::Number(number))
+    }
+
+    pub fn string<'ast>(&'ast self, s: &str) -> &'ast Node<'ast> {
+        let s = self.generic_arena.alloc_str(s);
+        self.generic_arena.alloc(Node::String(s))
+    }
+
+    pub fn str_chunks<'ast, I>(&'ast self, chunks: I) -> &'ast Node<'ast>
+    where
+        I: IntoIterator<Item = StrChunk<Ast<'ast>>>,
+        I::IntoIter: ExactSizeIterator,
+    {
+        let chunks = self.generic_arena.alloc_slice_fill_iter(chunks);
+        self.generic_arena.alloc(Node::StrChunks(chunks))
+    }
+
+    pub fn fun<'ast>(&'ast self, pat: &'ast Pattern<'ast>, body: Ast<'ast>) -> &'ast Node<'ast> {
+        self.generic_arena.alloc(Node::Fun(pat, body))
+    }
+
+    pub fn let_binding<'ast, I>(
+        &'ast self,
+        bindings: I,
+        body: Ast<'ast>,
+        rec: bool,
+    ) -> &'ast Node<'ast>
+    where
+        I: IntoIterator<Item = (Pattern<'ast>, Ast<'ast>)>,
+        I::IntoIter: ExactSizeIterator,
+    {
+        let bindings = self.generic_arena.alloc_slice_fill_iter(bindings);
+        self.generic_arena.alloc(Node::Let {
+            bindings,
+            body,
+            rec,
+        })
+    }
+
+    pub fn app<'ast, I>(&'ast self, fun: Ast<'ast>, args: I) -> &'ast Node<'ast>
+    where
+        I: IntoIterator<Item = Ast<'ast>>,
+        I::IntoIter: ExactSizeIterator,
+    {
+        let args = self.generic_arena.alloc_slice_fill_iter(args);
+        self.generic_arena.alloc(Node::App { fun, args })
+    }
+
+    pub fn var(&self, ident: LocIdent) -> &Node<'_> {
+        self.generic_arena.alloc(Node::Var(ident))
+    }
+
+    pub fn enum_variant<'ast>(
+        &'ast self,
+        tag: LocIdent,
+        arg: Option<Ast<'ast>>,
+    ) -> &'ast Node<'ast> {
+        self.generic_arena.alloc(Node::EnumVariant { tag, arg })
+    }
+
+    pub fn record<'ast>(&'ast self, record: Record<'ast>) -> &'ast Node<'ast> {
+        let record = self.generic_arena.alloc(record);
+        self.generic_arena.alloc(Node::Record(record))
+    }
+
+    pub fn record_data<'ast, Ss, Ds>(
+        &'ast self,
+        stat_fields: Ss,
+        dyn_fields: Ds,
+        open: bool,
+    ) -> &'ast Record<'ast>
+    where
+        Ss: IntoIterator<Item = (LocIdent, record::Field<'ast>)>,
+        Ds: IntoIterator<Item = (Ast<'ast>, record::Field<'ast>)>,
+        Ss::IntoIter: ExactSizeIterator,
+        Ds::IntoIter: ExactSizeIterator,
+    {
+        let stat_fields = self.generic_arena.alloc_slice_fill_iter(stat_fields);
+        let dyn_fields = self.generic_arena.alloc_slice_fill_iter(dyn_fields);
+        self.generic_arena.alloc(Record {
+            stat_fields,
+            dyn_fields,
+            open,
+        })
+    }
+
+    pub fn if_then_else<'ast>(
+        &'ast self,
+        cond: Ast<'ast>,
+        then_branch: Ast<'ast>,
+        else_branch: Ast<'ast>,
+    ) -> &'ast Node<'ast> {
+        self.generic_arena.alloc(Node::IfThenElse {
+            cond,
+            then_branch,
+            else_branch,
+        })
+    }
+
+    pub fn match_expr<'ast, I>(&'ast self, branches: I) -> &'ast Node<'ast>
+    where
+        I: IntoIterator<Item = MatchBranch<'ast>>,
+        I::IntoIter: ExactSizeIterator,
+    {
+        let branches = self.generic_arena.alloc_slice_fill_iter(branches);
+        self.generic_arena.alloc(Node::Match(Match { branches }))
+    }
+
+    pub fn array<'ast, I>(&'ast self, elts: I) -> &'ast Node<'ast>
+    where
+        I: IntoIterator<Item = Ast<'ast>>,
+        I::IntoIter: ExactSizeIterator,
+    {
+        let elts = self.generic_arena.alloc_slice_fill_iter(elts);
+        self.generic_arena.alloc(Node::Array(elts))
+    }
+
+    pub fn prim_op<'ast, I>(&'ast self, op: PrimOp, args: I) -> &'ast Node<'ast>
+    where
+        I: IntoIterator<Item = Ast<'ast>>,
+        I::IntoIter: ExactSizeIterator,
+    {
+        let op = self.generic_arena.alloc(op);
+        let args = self.generic_arena.alloc_slice_fill_iter(args);
+        self.generic_arena.alloc(Node::PrimOpApp { op, args })
+    }
+
+    pub fn annotated<'ast>(
+        &'ast self,
+        annot: Annotation<'ast>,
+        inner: Ast<'ast>,
+    ) -> &'ast Node<'ast> {
+        let annot = self.generic_arena.alloc(annot);
+        self.generic_arena.alloc(Node::Annotated { annot, inner })
+    }
+
+    pub fn import(&self, path: OsString, format: InputFormat) -> &Node<'_> {
+        let path = self.generic_arena.alloc(path);
+        self.generic_arena.alloc(Node::Import { path, format })
+    }
+
+    pub fn typ(&self, typ: Type) -> &Node<'_> {
+        let typ = self.type_arena.alloc(typ);
+        self.generic_arena.alloc(Node::Type(typ))
+    }
+
+    pub fn parse_error(&self, error: ParseError) -> &Node<'_> {
+        let error = self.error_arena.alloc(error);
+        self.generic_arena.alloc(Node::ParseError(error))
+    }
+
+    pub fn ast<'ast>(&'ast self, node: &'ast Node<'ast>, pos: TermPos) -> Ast<'ast> {
+        let pos = self.generic_arena.alloc(pos);
+        Ast { node, pos }
+    }
+
+    pub fn pattern<'ast>(
+        &'ast self,
+        data: PatternData<'ast>,
+        alias: Option<LocIdent>,
+        pos: TermPos,
+    ) -> &'ast Pattern<'ast> {
+        self.generic_arena.alloc(Pattern { data, alias, pos })
+    }
+
+    pub fn move_pattern<'ast>(&'ast self, pattern: Pattern<'ast>) -> &'ast Pattern<'ast> {
+        self.generic_arena.alloc(pattern)
+    }
+
+    pub fn enum_pattern<'ast>(
+        &'ast self,
+        tag: LocIdent,
+        pattern: Option<Pattern<'ast>>,
+        pos: TermPos,
+    ) -> &'ast EnumPattern<'ast> {
+        self.generic_arena.alloc(EnumPattern { tag, pattern, pos })
+    }
+
+    pub fn field_pattern<'ast>(
+        &'ast self,
+        matched_id: LocIdent,
+        annotation: Annotation<'ast>,
+        default: Option<Ast<'ast>>,
+        pattern: Pattern<'ast>,
+        pos: TermPos,
+    ) -> &'ast FieldPattern<'ast> {
+        self.generic_arena.alloc(FieldPattern {
+            matched_id,
+            annotation,
+            default,
+            pattern,
+            pos,
+        })
+    }
+
+    pub fn record_pattern<'ast, I>(
+        &'ast self,
+        patterns: I,
+        tail: TailPattern,
+        pos: TermPos,
+    ) -> &'ast RecordPattern<'ast>
+    where
+        I: IntoIterator<Item = FieldPattern<'ast>>,
+        I::IntoIter: ExactSizeIterator,
+    {
+        let patterns = self.generic_arena.alloc_slice_fill_iter(patterns);
+
+        self.generic_arena.alloc(RecordPattern {
+            patterns,
+            tail,
+            pos,
+        })
+    }
+
+    pub fn array_pattern<'ast, I>(
+        &'ast self,
+        patterns: I,
+        tail: TailPattern,
+        pos: TermPos,
+    ) -> &'ast ArrayPattern<'ast>
+    where
+        I: IntoIterator<Item = Pattern<'ast>>,
+        I::IntoIter: ExactSizeIterator,
+    {
+        let patterns = self.generic_arena.alloc_slice_fill_iter(patterns);
+
+        self.generic_arena.alloc(ArrayPattern {
+            patterns,
+            tail,
+            pos,
+        })
+    }
+
+    pub fn constant_pattern<'ast>(
+        &'ast self,
+        data: ConstantPatternData<'ast>,
+        pos: TermPos,
+    ) -> &'ast ConstantPattern<'ast> {
+        self.generic_arena.alloc(ConstantPattern { data, pos })
+    }
+
+    pub fn or_pattern<'ast, I>(&'ast self, patterns: I, pos: TermPos) -> &'ast OrPattern<'ast>
+    where
+        I: IntoIterator<Item = Pattern<'ast>>,
+        I::IntoIter: ExactSizeIterator,
+    {
+        let patterns = self.generic_arena.alloc_slice_fill_iter(patterns);
+
+        self.generic_arena.alloc(OrPattern { patterns, pos })
+    }
+}
diff --git a/core/src/bytecode/ast/pattern/bindings.rs b/core/src/bytecode/ast/pattern/bindings.rs
new file mode 100644
index 00000000..ee473e33
--- /dev/null
+++ b/core/src/bytecode/ast/pattern/bindings.rs
@@ -0,0 +1,181 @@
+//! Pattern analysis. The trait defined here is mostly used by the LSP.
+
+use crate::{
+    bytecode::ast::{pattern::*, record::Field},
+    identifier::LocIdent,
+};
+
+pub trait Bindings<'ast> {
+    /// Returns a list of all variables bound by this pattern, together with the path to the field
+    /// they match and the associated extra annotations.
+    ///
+    /// # Example
+    ///
+    /// For a pattern `{a = x @ {foo, bar | Number = z, ..rest}, d = e}`, the result of this function
+    /// contains:
+    ///
+    /// - `(["a"], "x", empty field)` for the `x` variable
+    /// - `(["a"], "rest", empty field)` for the `rest` variable
+    /// - `(["a", "foo"], "foo", empty field)` for the `foo` variable
+    /// - `(["a", "bar"], "z", field with Number contract)` for the `z` variable
+    /// - `(["d"], "e", empty field)` for the `e` variable
+    fn bindings(&self) -> Vec<(Vec<LocIdent>, LocIdent, Field<'ast>)>;
+}
+
+trait InjectBindings<'ast> {
+    /// Same as [Bindings::bindings], but work relative to a current path inside a pattern and
+    /// injects the bindings into a working vector instead of returning the result. This method is
+    /// mostly used internally and is the one performing the actual work.
+    ///
+    /// Other modules of the LSP should use [Bindings::bindings] directly.
+    ///
+    /// # Parameters
+    ///
+    /// - `bindings`: the vector to inject the bindings into.
+    /// - `path`: the field path to the sub-pattern being analysed.
+    /// - `parent_extra`: the extra annotations associated with a potential parent field pattern.
+    ///   For example, when injecting the bindings of `{foo ? 5 = x @ y @ z}`, all the introduced
+    ///   variables should refer to default annotation of `foo`. This annotation is thus passed
+    ///   along when calling to the sub-patterns' [Self::inject_bindings].
+    fn inject_bindings(
+        &self,
+        bindings: &mut Vec<(Vec<LocIdent>, LocIdent, Field<'ast>)>,
+        path: Vec<LocIdent>,
+        parent_extra: Option<&Field<'ast>>,
+    );
+}
+
+impl<'ast> Bindings<'ast> for Pattern<'ast> {
+    fn bindings(&self) -> Vec<(Vec<LocIdent>, LocIdent, Field<'ast>)> {
+        let mut bindings = Vec::new();
+        self.inject_bindings(&mut bindings, Vec::new(), None);
+        bindings
+    }
+}
+
+impl<'ast> InjectBindings<'ast> for Pattern<'ast> {
+    fn inject_bindings(
+        &self,
+        bindings: &mut Vec<(Vec<LocIdent>, LocIdent, Field<'ast>)>,
+        path: Vec<LocIdent>,
+        parent_deco: Option<&Field<'ast>>,
+    ) {
+        if let Some(alias) = self.alias {
+            bindings.push((
+                path.clone(),
+                alias,
+                parent_deco.cloned().unwrap_or_default(),
+            ));
+        }
+
+        self.data.inject_bindings(bindings, path, parent_deco);
+    }
+}
+
+impl<'ast> InjectBindings<'ast> for PatternData<'ast> {
+    fn inject_bindings(
+        &self,
+        bindings: &mut Vec<(Vec<LocIdent>, LocIdent, Field<'ast>)>,
+        path: Vec<LocIdent>,
+        parent_deco: Option<&Field<'ast>>,
+    ) {
+        match self {
+            PatternData::Any(id) => {
+                bindings.push((path, *id, parent_deco.cloned().unwrap_or_default()))
+            }
+            PatternData::Record(record_pat) => {
+                record_pat.inject_bindings(bindings, path, parent_deco)
+            }
+            PatternData::Array(array_pat) => array_pat.inject_bindings(bindings, path, parent_deco),
+            PatternData::Enum(evariant_pat) => {
+                evariant_pat.inject_bindings(bindings, path, parent_deco)
+            }
+            PatternData::Or(or_pat) => or_pat.inject_bindings(bindings, path, parent_deco),
+            // Wildcard and constant patterns don't bind any variable
+            PatternData::Wildcard | PatternData::Constant(_) => (),
+        }
+    }
+}
+
+impl<'ast> InjectBindings<'ast> for RecordPattern<'ast> {
+    fn inject_bindings(
+        &self,
+        bindings: &mut Vec<(Vec<LocIdent>, LocIdent, Field<'ast>)>,
+        path: Vec<LocIdent>,
+        parent_extra: Option<&Field<'ast>>,
+    ) {
+        for field_pat in self.patterns.iter() {
+            // Field patterns have their own annotation, so there's no need to propagate
+            // `parent_extra` any further
+            field_pat.inject_bindings(bindings, path.clone(), None);
+        }
+
+        if let TailPattern::Capture(rest) = self.tail {
+            // If a contract is attached to the whole record pattern in the enclosing pattern, the
+            // rest doesn't exactly match this contract: there are some fields missing. Still, it
+            // sounds more useful to keep the whole metadata - including documentation - for
+            // autocompletion and the like, even if it's an over-approximation.
+            bindings.push((path, rest, parent_extra.cloned().unwrap_or_default()));
+        }
+    }
+}
+
+impl<'ast> InjectBindings<'ast> for ArrayPattern<'ast> {
+    fn inject_bindings(
+        &self,
+        bindings: &mut Vec<(Vec<LocIdent>, LocIdent, Field<'ast>)>,
+        path: Vec<LocIdent>,
+        _parent_extra: Option<&Field<'ast>>,
+    ) {
+        for subpat in self.patterns.iter() {
+            // Array elements shouldn't inherit the annotation from their parent (for once, they
+            // are of a different type), so we reset `parent_extra` to `None`.
+            subpat.inject_bindings(bindings, path.clone(), None);
+        }
+
+        if let TailPattern::Capture(rest) = self.tail {
+            bindings.push((path, rest, Default::default()));
+        }
+    }
+}
+
+impl<'ast> InjectBindings<'ast> for FieldPattern<'ast> {
+    fn inject_bindings(
+        &self,
+        bindings: &mut Vec<(Vec<LocIdent>, LocIdent, Field<'ast>)>,
+        mut path: Vec<LocIdent>,
+        _parent_extra: Option<&Field<'ast>>,
+    ) {
+        path.push(self.matched_id);
+        self.pattern
+            .inject_bindings(bindings, path, Some(&Field::from(self.annotation.clone())));
+    }
+}
+
+impl<'ast> InjectBindings<'ast> for EnumPattern<'ast> {
+    fn inject_bindings(
+        &self,
+        bindings: &mut Vec<(Vec<LocIdent>, LocIdent, Field<'ast>)>,
+        path: Vec<LocIdent>,
+        _parent_extra: Option<&Field<'ast>>,
+    ) {
+        //TODO: I'm not sure we should just transparently forward to the variant's argument. Maybe
+        //we need a more complex notion of path here, that knows when we enter an enum variant?
+        if let Some(ref arg_pat) = self.pattern {
+            arg_pat.inject_bindings(bindings, path, None);
+        }
+    }
+}
+
+impl<'ast> InjectBindings<'ast> for OrPattern<'ast> {
+    fn inject_bindings(
+        &self,
+        bindings: &mut Vec<(Vec<LocIdent>, LocIdent, Field<'ast>)>,
+        path: Vec<LocIdent>,
+        parent_extra: Option<&Field<'ast>>,
+    ) {
+        for subpat in self.patterns.iter() {
+            subpat.inject_bindings(bindings, path.clone(), parent_extra);
+        }
+    }
+}
diff --git a/core/src/bytecode/ast/pattern/mod.rs b/core/src/bytecode/ast/pattern/mod.rs
new file mode 100644
index 00000000..abd23adb
--- /dev/null
+++ b/core/src/bytecode/ast/pattern/mod.rs
@@ -0,0 +1,232 @@
+//! Pattern matching and destructuring of Nickel values.
+use std::collections::{hash_map::Entry, HashMap};
+
+use super::{Annotation, Ast, Number};
+
+use crate::{identifier::LocIdent, parser::error::ParseError, position::TermPos};
+
+pub mod bindings;
+
+#[derive(Debug, PartialEq, Clone)]
+pub enum PatternData<'ast> {
+    /// A wildcard pattern, matching any value. As opposed to any, this pattern doesn't bind any
+    /// variable.
+    Wildcard,
+    /// A simple pattern consisting of an identifier. Match anything and bind the result to the
+    /// corresponding identifier.
+    Any(LocIdent),
+    /// A record pattern as in `{ a = { b, c } }`
+    Record(&'ast RecordPattern<'ast>),
+    /// An array pattern as in `[a, b, c]`
+    Array(&'ast ArrayPattern<'ast>),
+    /// An enum pattern as in `'Foo x` or `'Foo`
+    Enum(&'ast EnumPattern<'ast>),
+    /// A constant pattern as in `42` or `true`.
+    Constant(&'ast ConstantPattern<'ast>),
+    /// A sequence of alternative patterns as in `'Foo _ or 'Bar _ or 'Baz _`.
+    Or(&'ast OrPattern<'ast>),
+}
+
+/// A generic pattern, that can appear in a match expression (not yet implemented) or in a
+/// destructuring let-binding.
+#[derive(Debug, PartialEq, Clone)]
+pub struct Pattern<'ast> {
+    /// The content of this pattern
+    pub data: PatternData<'ast>,
+    /// A potential alias for this pattern, capturing the whole matched value. In the source
+    /// language, an alias is introduced by `x @ <pattern>`, where `x` is an arbitrary identifier.
+    pub alias: Option<LocIdent>,
+    /// The position of the pattern in the source.
+    pub pos: TermPos,
+}
+
+/// An enum pattern, including both an enum tag and an enum variant.
+#[derive(Debug, PartialEq, Clone)]
+pub struct EnumPattern<'ast> {
+    pub tag: LocIdent,
+    pub pattern: Option<Pattern<'ast>>,
+    pub pos: TermPos,
+}
+
+/// A field pattern inside a record pattern. Every field can be annotated with a type, contracts or
+/// with a default value.
+#[derive(Debug, PartialEq, Clone)]
+pub struct FieldPattern<'ast> {
+    /// The name of the matched field. For example, in `{..., foo = {bar, baz}, ...}`, the matched
+    /// identifier is `foo`.
+    pub matched_id: LocIdent,
+    /// Type and contract annotations of this field.
+    pub annotation: Annotation<'ast>,
+    /// Potential default value, set with the `? value` syntax.
+    pub default: Option<Ast<'ast>>,
+    /// The pattern on the right-hand side of the `=`. A pattern like `{foo, bar}`, without the `=`
+    /// sign, is parsed as `{foo=foo, bar=bar}`. In this case, `pattern.data` will be
+    /// [PatternData::Any].
+    pub pattern: Pattern<'ast>,
+    pub pos: TermPos,
+}
+
+/// The last match in a data structure pattern. This can either be a normal match, or an ellipsis
+/// which can capture the rest of the data structure. The type parameter `P` is the type of the
+/// pattern of the data structure: currently, ellipsis matches are only supported for record, but
+/// we'll probably support them for arrays as well.
+///
+/// This enum is mostly used during parsing.
+///
+/// # Example
+///
+/// - In `{foo={}, bar}`, the last match is an normal match.
+/// - In `{foo={}, bar, ..}`, the last match is a non-capturing ellipsis.
+/// - In `{foo={}, bar, ..rest}`, the last match is a capturing ellipsis.
+#[derive(Debug, PartialEq, Clone)]
+pub enum LastPattern<'ast, P> {
+    /// The last field is a normal match. In this case the pattern is "closed" so every record
+    /// fields should be matched.
+    Normal(&'ast P),
+    /// The pattern is "open" `, ..}`. Optionally you can bind a record containing the remaining
+    /// fields to an `Identifier` using the syntax `, ..y}`.
+    Ellipsis(Option<LocIdent>),
+}
+
+/// A record pattern.
+#[derive(Debug, PartialEq, Clone)]
+pub struct RecordPattern<'ast> {
+    /// The patterns for each field in the record.
+    pub patterns: &'ast [FieldPattern<'ast>],
+    /// The tail of the pattern, indicating if the pattern is open, i.e. if it ended with an
+    /// ellipsis, capturing the rest or not.
+    pub tail: TailPattern,
+    pub pos: TermPos,
+}
+
+/// An array pattern.
+#[derive(Debug, PartialEq, Clone)]
+pub struct ArrayPattern<'ast> {
+    /// The patterns of the elements of the array.
+    pub patterns: &'ast [Pattern<'ast>],
+    /// The tail of the pattern, indicating if the pattern is open, i.e. if it ended with an
+    /// ellipsis, capturing the rest or not.
+    pub tail: TailPattern,
+    pub pos: TermPos,
+}
+
+impl<'ast> ArrayPattern<'ast> {
+    /// Check if this record contract is open, meaning that it accepts additional fields to be
+    /// present, whether the rest is captured or not.
+    pub fn is_open(&self) -> bool {
+        self.tail.is_open()
+    }
+}
+
+/// A constant pattern, matching a constant value.
+#[derive(Debug, PartialEq, Clone)]
+pub struct ConstantPattern<'ast> {
+    pub data: ConstantPatternData<'ast>,
+    pub pos: TermPos,
+}
+
+#[derive(Debug, PartialEq, Clone)]
+pub enum ConstantPatternData<'ast> {
+    Bool(bool),
+    Number(&'ast Number),
+    String(&'ast str),
+    Null,
+}
+
+#[derive(Debug, PartialEq, Clone)]
+pub struct OrPattern<'ast> {
+    pub patterns: &'ast [Pattern<'ast>],
+    pub pos: TermPos,
+}
+
+/// The tail of a data structure pattern (record or array) which might capture the rest of said
+/// data structure.
+#[derive(Debug, PartialEq, Clone)]
+pub enum TailPattern {
+    /// The pattern is closed, i.e. it doesn't allow more fields. For example, `{foo, bar}`.
+    Empty,
+    /// The pattern ends with an ellipsis, making it open. For example, `{foo, bar, ..}`.
+    Open,
+    /// The pattern ends with an ellispis and a variable capturing the rest of the record. For
+    /// example, `{foo, bar, ..rest}`.
+    Capture(LocIdent),
+}
+
+impl<'ast> Pattern<'ast> {
+    pub fn any(id: LocIdent) -> Self {
+        let pos = id.pos;
+
+        Pattern {
+            data: PatternData::Any(id),
+            alias: None,
+            pos,
+        }
+    }
+}
+
+impl TailPattern {
+    /// Check if this tail pattern makes the enclosing data structure pattern open, meaning that it
+    /// accepts additional fields or elements to be present, whether the rest is captured or not.
+    pub fn is_open(&self) -> bool {
+        matches!(self, TailPattern::Open | TailPattern::Capture(_))
+    }
+}
+
+impl<'ast> RecordPattern<'ast> {
+    /// Check the matches for duplication, and raise an error if any occurs.
+    ///
+    /// Note that for backwards-compatibility reasons this function _only_
+    /// checks top-level matches. In Nickel 1.0, this code panicked:
+    ///
+    /// ```text
+    /// let f = fun { x, x, .. } => x in f { x = 1 }
+    /// ```
+    ///
+    /// However this "works", even though the binding to `y` is duplicated.
+    ///
+    /// ```text
+    /// let f =
+    ///   fun { x = { y }, z = { y }, .. } => y
+    /// in f { x = { y = 1 }, z = { y = 2 } }
+    /// # evaluates to 1
+    /// ```
+    ///
+    /// This function aims to raise errors in the first case, but maintain the
+    /// behaviour in the second case.
+    pub fn check_dup(&self) -> Result<(), ParseError> {
+        let mut bindings = HashMap::new();
+
+        for pat in self.patterns.iter() {
+            let binding = pat.matched_id;
+            let label = binding.label().to_owned();
+            match bindings.entry(label) {
+                Entry::Occupied(occupied_entry) => {
+                    return Err(ParseError::DuplicateIdentInRecordPattern {
+                        ident: binding,
+                        prev_ident: occupied_entry.remove_entry().1,
+                    })
+                }
+                Entry::Vacant(vacant_entry) => {
+                    vacant_entry.insert(binding);
+                }
+            }
+        }
+
+        Ok(())
+    }
+
+    /// Check if this record contract is open, meaning that it accepts additional fields to be
+    /// present, whether the rest is captured or not.
+    pub fn is_open(&self) -> bool {
+        self.tail.is_open()
+    }
+}
+
+//TODO: restore Pretty and Display.
+//impl_display_from_pretty!(PatternData);
+//impl_display_from_pretty!(Pattern);
+//impl_display_from_pretty!(ConstantPatternData);
+//impl_display_from_pretty!(ConstantPattern);
+//impl_display_from_pretty!(RecordPattern);
+//impl_display_from_pretty!(EnumPattern);
+//impl_display_from_pretty!(ArrayPattern);
diff --git a/core/src/bytecode/ast/primop.rs b/core/src/bytecode/ast/primop.rs
new file mode 100644
index 00000000..a5a6ed68
--- /dev/null
+++ b/core/src/bytecode/ast/primop.rs
@@ -0,0 +1,1151 @@
+//! Primitive operations of the source language (there exists additional primops that are used at
+//! runtime but can't be expressed in Nickel code).
+
+use std::fmt;
+
+use crate::{identifier::LocIdent, label::MergeKind, term};
+
+use super::RecordOpKind;
+
+/// Nickel primitive operations.
+#[derive(Copy, Clone, Debug, PartialEq, Eq)]
+pub enum PrimOp {
+    /// Unary operators or operator that are eager only in their first argument.
+
+    /// Return an enum tag representing the type of the term.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The term to get the type of.
+    Typeof,
+
+    /// Boolean AND operator.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left condition.
+    /// 2. (Lazy) The right condition.
+    BoolAnd,
+
+    /// Boolean OR operator.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left condition.
+    /// 2. (Lazy) The right condition.
+    BoolOr,
+
+    /// Boolean NOT operator.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left condition.
+    /// 2. (Lazy) The right condition.
+    BoolNot,
+
+    /// Raise a blame, which stops the execution and prints an error according to the label
+    /// argument.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label to blame.
+    Blame,
+
+    /// Typecast an enum to a larger enum type.
+    ///
+    /// [Self::EnumEmbed] is used to upcast enums. For example, if a value `x` has enum type `[|
+    /// 'a, 'b |]`, then `%enum/embed% c 'x` will have enum type `[| 'a, 'b, 'c |]`. It only
+    /// affects typechecking as at runtime `%enum/embed% x` acts like the identity function.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The enum to embed in a larger type.
+    EnumEmbed(LocIdent),
+
+    /// Static record access.
+    ///
+    /// Static means that the field identifier is a statically known string inside the source. This
+    /// is how `record.field` is represented in the AST.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The record to access.
+    RecordStatAccess(LocIdent),
+
+    /// Map a function on each element of an array.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The array to map on.
+    /// 2. (Lazy) The function to map.
+    ArrayMap,
+
+    /// Map a function on a record.
+    ///
+    /// The mapped function must take two arguments, the name of the field as a string, and the
+    /// content of the field. [Self::RecordMap] then replaces the content of each field by the
+    /// result of the function: i.e., `%record/map% { a = 2} f` evaluates to `{ a = f "a" 2 }`.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The record to map on.
+    /// 2. (Lazy) The function to map.
+    RecordMap,
+
+    /// Inverse the polarity of a label.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label.
+    LabelFlipPol,
+
+    /// Get the polarity of a label.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label.
+    LabelPol,
+
+    /// Go to the domain in the type path of a label.
+    ///
+    /// If the argument is a label with a [type path][crate::label::TyPath) representing some
+    /// subtype of the type of the original contract, as in:
+    ///
+    /// ```text
+    /// (Num -> Num) -> Num
+    ///  ^^^^^^^^^^ type path
+    /// ------------------- original type
+    /// ```
+    ///
+    /// Then `GoDom` evaluates to a copy of this label, where the path has gone forward into the
+    /// domain:
+    ///
+    /// ```text
+    /// (Num -> Num) -> Num
+    ///  ^^^ new type path
+    /// ------------------- original type
+    /// ```
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label.
+    LabelGoDom,
+
+    /// Go to the codomain in the type path of a label.
+    ///
+    /// See `GoDom`.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label.
+    LabelGoCodom,
+
+    /// Go to the array in the type path of a label.
+    ///
+    /// See `GoDom`.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label.
+    LabelGoArray,
+
+    /// Go to the type ascribed to every field in a dictionary.
+    ///
+    /// See `GoDom`.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label.
+    LabelGoDict,
+
+    /// Force the evaluation of its argument and proceed with the second.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The term to force.
+    /// 2. (Lazy) The term to proceed with (the continuation).
+    Seq,
+
+    /// Recursively force the evaluation of its first argument then returns the second.
+    ///
+    /// Recursive here means that the evaluation does not stop at a WHNF, but the content of arrays
+    /// and records is also recursively forced.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The term to force.
+    /// 2. (Lazy) The term to proceed with (the continuation).
+    DeepSeq,
+
+    /// Return the length of an array.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The array to get the length of.
+    ArrayLength,
+
+    /// Generate an array of a given length by mapping a `Num -> Num` function onto `[1,..,n]`.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The length of the array.
+    /// 2. (Lazy) The generating function.
+    ArrayGen,
+
+    /// Return the names of the fields of a record as a string array.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The record to get the fields of.
+    RecordFields(RecordOpKind),
+
+    /// Return the values of the fields of a record as an array.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The record to get the values of the fields of.
+    RecordValues,
+
+    /// Remove heading and trailing spaces from a string.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The string to trim.
+    StringTrim,
+
+    /// Return the array of characters of a string.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The string to get the characters of.
+    StringChars,
+
+    /// Transform a string to uppercase.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The string to transform.
+    StringUppercase,
+
+    /// Transform a string to lowercase.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The string to transform.
+    StringLowercase,
+
+    /// Return the length of a string.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The string to get the length of.
+    StringLength,
+
+    /// Transform a data to a string.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The data to transform.
+    ToString,
+
+    /// Transform a string to a number.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The string to transform.
+    NumberFromString,
+
+    /// Transform a string to an enum.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The string to transform.
+    EnumFromString,
+
+    /// Test if a regex matches a string.
+    ///
+    /// Like [Self::StringFind], this is a unary operator because we would like a way to share the
+    /// same "compiled regex" for many matching calls. This is done by returning a closure which
+    /// store the compiled regex and can then be applied to many arguments with recompilation.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The regex to match.
+    /// 2. (Lazy) The string to match.
+    StringIsMatch,
+
+    /// Match a regex on a string, and returns the captured groups together, the index of the
+    /// match, etc.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The regex to match.
+    /// 2. (Lazy) The string to match.
+    StringFind,
+
+    /// Returns all matches of a regex on a string, as an array of matches. Each
+    /// match contains the match groups, the starting index of the match and the
+    /// matched string.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The regex to match.
+    /// 2. (Lazy) The string to match.
+    StringFindAll,
+
+    /// Force full evaluation of a term and return it.
+    ///
+    /// This primop has been added in the context of lazy array contracts, to make serialization
+    /// work with lazy array contracts in general.
+    ///
+    /// # `Force` vs. `DeepSeq`
+    ///
+    /// [Self::Force] updates at the indices containing arrays with a new version where the lazy
+    /// contracts have all been applied, whereas [Self::DeepSeq] evaluates the same expressions,
+    /// but it never updates at the index of an array with lazy contracts with an array where those
+    /// contracts have been applied. In a way, the result of lazy contract application in arrays is
+    /// "lost" in [Self::DeepSeq], while it's returned in [Self::Force].
+    ///
+    /// This means we can observe different results between `deep_seq x x` and `force x`, in some
+    /// cases.
+    ///
+    /// It's also worth noting that [Self::DeepSeq] should be, in principle, more efficient that
+    /// [Self::Force] as it does less cloning.
+    ///
+    /// # About `ignore_not_exported`
+    ///
+    /// When exporting a Nickel term, we first apply `Force` to the term to evaluate it. If there
+    /// are record fields that have been marked `not_exported`, they would still be evaluated
+    /// ordinarily, see [#1230](https://github.com/tweag/nickel/issues/1230). To stop this from
+    /// happening, we introduce the `for_export` parameter here. When `for_export` is `true`, the
+    /// evaluation of `Force` will skip fields that are marked as `not_exported`. When `for_export`
+    /// is `false`, these fields are evaluated.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The term to force.
+    Force { ignore_not_exported: bool },
+
+    /// Creates an "empty" record with a sealed tail copied from its record argument.
+    ///
+    /// Used in the `$record` contract implementation to ensure that we can define a `field_diff`
+    /// function that preserves the sealed polymorphic tail of its argument.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The model record to take the tail from.
+    RecordEmptyWithTail,
+
+    /// Print a message when encountered during evaluation and proceed with the evaluation of the
+    /// argument on the top of the stack. Operationally the same as the identity function
+    ///
+    /// # Arguments
+    ///
+    /// 1. The term to trace.
+    /// 2. (Lazy) The term to proceed with (the continuation).
+    Trace,
+
+    /// Push a new, fresh diagnostic on the diagnostic stack of a contract label. This has the
+    /// effect of saving the current diagnostic, as following calls to primops that modify the
+    /// label's current diagnostic will modify the fresh one, instead of the one being stacked.
+    /// This primop shouldn't be used directly by user a priori, but is used internally during e.g.
+    /// contract application.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label to push the diagnostic on.
+    LabelPushDiag,
+
+    /// Evaluate a string of nix code into a resulting nickel value. Currently completely
+    /// (strictly) evaluates the nix code, and must result in a value serializable into JSON.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The nix code to evaluate.
+    #[cfg(feature = "nix-experimental")]
+    EvalNix,
+
+    /// Retrieve the argument from an enum variant: `%enum/get_arg% ('Foo t) := t`
+    ///
+    /// # Arguments
+    ///
+    /// 1. The enum variant to get the argument from.
+    EnumGetArg,
+    /// Create an enum variant from a tag and an argument.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The tag of the variant.
+    /// 2. (Lazy) The argument of the variant.
+    EnumMakeVariant,
+    /// Return true if the given parameter is an enum variant.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The enum to check.
+    EnumIsVariant,
+    /// Extract the tag from an enum tag or an enum variant.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The enum to get the tag from.
+    EnumGetTag,
+
+    /// Wrap a contract implementation as a custom contract. You can think of this primop as a type
+    /// constructor for custom contracts.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The contract implementation (a function).
+    ContractCustom,
+
+    /// The cosinus function.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The numeral argument.
+    NumberArcCos,
+
+    /// The sinus function.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The numeral argument.
+    NumberArcSin,
+
+    /// The tangent function.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The numeral argument.
+    NumberArcTan,
+
+    /// The cosinus function.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The numeral argument.
+    NumberCos,
+
+    /// The sinus function.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The numeral argument.
+    NumberSin,
+
+    /// The tangent function.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The numeral argument.
+    NumberTan,
+
+    /// Binary operators or multi-ary operators that are eager in their two first arguments.
+
+    /// Addition of numerals.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left numeral.
+    /// 2. The right numeral.
+    Plus,
+
+    /// Subtraction of numerals.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left numeral.
+    /// 2. The right numeral.
+    Sub,
+
+    /// Multiplication of numerals.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left numeral.
+    /// 2. The right numeral.
+    Mult,
+
+    /// Rational division of numerals.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The dividend.
+    /// 2. The divisor.
+    Div,
+
+    /// Modulo of numerals.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left numeral.
+    /// 2. The right numeral.
+    Modulo,
+
+    /// Give the four quadrant arctangent of y and x.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The first numeral.
+    /// 2. The second numeral.
+    NumberArcTan2,
+
+    /// Give the logarithm of a number.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The first numeral.
+    /// 2. The second numeral.
+    NumberLog,
+
+    /// Raise a number to a power.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The first numeral.
+    /// 2. The second numeral.
+    Pow,
+
+    /// Concatenation of strings.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left string.
+    /// 2. The right string.
+    StringConcat,
+
+    /// Polymorphic equality.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left value.
+    /// 2. The right value.
+    Eq,
+
+    /// Strictly less than comparison operator.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left numeral.
+    /// 2. The right numeral.
+    LessThan,
+
+    /// Less than or equal comparison operator.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left numeral.
+    /// 2. The right numeral.
+    LessOrEq,
+
+    /// Strictly greater than comparison operator.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left numeral.
+    /// 2. The right numeral.
+    GreaterThan,
+
+    /// Greater than or equal comparison operator.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left numeral.
+    /// 2. The right numeral.
+    GreaterOrEq,
+
+    /// Apply a contract to a label and a value. The value is is stored on the stack unevaluated,
+    /// while the contract and the label are the strict arguments to this operator.
+    /// [Self::ContractApply] also accepts contracts as records, which are translated to a function
+    /// that merge said contract with its argument. Finally, this operator marks the location of
+    /// the contract argument on the stack for better error reporting.
+    ///
+    /// Either the contract raises a blame error, or the primop evaluates to the value returned by
+    /// the contract that can be used in place of the original value.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The contract to apply.
+    /// 2. The label.
+    /// 3. (Lazy) The argument to the contract.
+    ContractApply,
+
+    /// Variant of [Self::ContractApply] which also applies an arbitrary contract to a label and a
+    /// value, but instead of either blaming or returning the value, it has the same return value
+    /// as contract built via [Self::ContractCustom], that is `[| 'Ok Dyn, 'Error {..}|]`. The
+    /// value returned through `'Ok` can still have lazy blame expressions inside, of course.
+    ///
+    /// Put differently, `%contract/check% (%contract/custom% custom) label value` is equivalent to
+    /// `custom label value`, modulo argument tracking. [Self::ContractCheck] doesn't only work on
+    /// custom contracts, but on builtin contracts as well.
+    ///
+    /// This operation is useful for contract composition, that is when calling a contract from
+    /// another contract. In theory, one could use [Self::ContractApply], but the caller then needs
+    /// to wrap the result in `'Ok`, and much more importantly, `%contract/apply%` converts all
+    /// immediate errors returned as `'Error` into blame errors. This is not desirable, as blame
+    /// errors can't be caught, which artificially makes the called contract entirely delayed. This
+    /// typically wouldn't play very well with boolean combinators. On the other hand,
+    /// [Self::ContractCheck] preserves the immediate/delayed part of the called contract.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The contract to apply.
+    /// 2. The label.
+    /// 3. (Lazy) The argument to the contract.
+    ContractCheck,
+
+    /// Take a record of type `{message | String | optional, notes | String | optional}`, a label,
+    /// and return the label with the diagnostic set accordingly.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The error diagnostic as a record.
+    /// 2. The label.
+    LabelWithErrorData,
+
+    /// Go to a specific field in the type path of a label.
+    ///
+    /// See [Self::LabelGoDom].
+    ///
+    /// # Arguments
+    ///
+    /// 1. The field (as a string)
+    /// 2. The label.
+    LabelGoField,
+
+    /// Insert a new field into a record. Fail if the field already exists.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The field name.
+    /// 2. The record.
+    /// 3. (Lazy) The value to insert.
+    RecordInsert(RecordOpKind),
+
+    /// Remove a field from a record. The field name is given as an argument.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The field name.
+    /// 2. The record.
+    RecordRemove(RecordOpKind),
+
+    /// Dynamically access a field of record. The field name is given as an argument which should
+    /// evaluate to a string. This is how `record."%{field}"` is represented in the AST.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The field name.
+    /// 2. The record.
+    RecordGet,
+
+    /// Test if a record has a specific field.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The field name.
+    /// 2. The record.
+    RecordHasField(RecordOpKind),
+
+    /// Test if the field of a record exists and has a definition.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The field name.
+    /// 2. The record.
+    RecordFieldIsDefined(RecordOpKind),
+
+    /// Take a pair of records and split them into four separate records:
+    ///
+    /// - `left_only`: fields of the left argument but not in the right
+    /// - `left_center`: fields of the left argument that happens to also be in the right (but the
+    ///   value and the metadata are taken from the left)
+    /// - `right_center`: fields of the right argument that happens to also be in the left (but the
+    ///   value and the metadata are taken from the right)
+    /// - `right_only`: fields of the right argument but not in the left
+    ///
+    /// As opposed to an equivalent user-defined implementation, this primop has better performance
+    /// and is able to preserve field metadata.
+    ///
+    /// If `left` (resp. `right`) is open or has a sealed tail, then `left_only` (resp.
+    /// `right_only`) will inherit the same properties. `left_center` (resp. `right_center`) is
+    /// always closed and without a sealed tail.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left record.
+    /// 2. The right record.
+    RecordSplitPair,
+
+    /// Take a pair of disjoint records (i.e. records with no common field) and combine them into
+    /// one. It's a form of merging, but based on the assumption that the records are disjoint and
+    /// thus non-conflicting, it's simpler and more efficient than a general merge.
+    ///
+    /// As for merge, this raises a blame error if one of the arguments has a sealed tail.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left record.
+    /// 2. The right record.
+    RecordDisjointMerge,
+
+    /// Concatenate two arrays.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left array.
+    /// 2. The right array.
+    ArrayConcat,
+
+    /// Access the n-th element of an array.
+    ///
+    /// Warning: the arguments are swapped compared to [crate::term::BinaryOp::ArrayAt].
+    ///
+    /// # Arguments
+    ///
+    /// 1. The index.
+    /// 2. The array.
+    ArrayAt,
+
+    /// The merge operator (see [crate::eval::merge]). `Merge` is parametrized by a
+    /// [crate::label::MergeKind] flavour, which carries additional information for error-reporting
+    /// purpose.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The first argument.
+    /// 2. The second argument.
+    Merge(MergeKind),
+
+    /// Hash a string.
+    ///
+    /// # Arguments
+    ///
+    /// 1. An enum representing the hash function to use (`'Md5, `Sha256`, etc.). See Nickel's
+    ///    stdlib documentation for `std.hash`.
+    /// 2. The string to hash.
+    Hash,
+
+    /// Serialize a value to a string.
+    ///
+    /// # Arguments
+    ///
+    /// 1. An enum representing the serialization format (`'Json`, `'Yaml`, etc.). See Nickel's
+    ///    stdlib documentation for `std.serialize`.
+    /// 2. The value to serialize.
+    Serialize,
+
+    /// Deserialize a string to a value.
+    ///
+    /// # Arguments
+    ///
+    /// 1. An enum representing the serialization format (`'Json`, `'Yaml`, etc.). See Nickel's
+    ///    stdlib documentation for `std.deserialize`.
+    /// 2. The string to deserialize.
+    Deserialize,
+
+    /// Split a string into an array.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The string to split.
+    /// 2. The separator.
+    StringSplit,
+
+    /// Determine if a string is a substring of another one.
+    ///
+    /// Warning: the arguments are swapped compared to [crate::term::BinaryOp::StringContains].
+    ///
+    /// # Arguments
+    ///
+    /// 1. The substring.
+    /// 2. The string.
+    StringContains,
+
+    /// Compare two strings lexicographically.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The left string.
+    /// 2. The right string.
+    StringCompare,
+
+    /// Lazily apply a contract to an Array.
+    ///
+    /// This simply inserts a contract into the array attributes.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label.
+    /// 2. The array.
+    /// 3. (Lazy) The contract to apply.
+    ContractArrayLazyApp,
+
+    /// Lazily map contracts over a record. The arguments are a label and a function which takes
+    /// the name of the field as a parameter and returns the corresponding contract.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label.
+    /// 2. The record.
+    /// 3. (Lazy) The contract parametrized by field names.
+    ContractRecordLazyApp,
+
+    /// Set the message of the current diagnostic of a label.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The message.
+    /// 2. The label.
+    LabelWithMessage,
+
+    /// Set the notes of the current diagnostic of a label.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The notes (an array of evaluated string). Important: the notes must be forced before
+    ///    calling to this primop.
+    /// 2. The label.
+    LabelWithNotes,
+
+    /// Append a note to the current diagnostic of a label.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The note (a string).
+    /// 2. The label.
+    LabelAppendNote,
+
+    /// Look up the [`crate::label::TypeVarData`] associated with a sealing key in the type
+    /// environment of a [label](crate::label::Label).
+    ///
+    /// # Arguments
+    ///
+    /// 1. The sealing key.
+    /// 2. The label.
+    LabelLookupTypeVar,
+
+    /// N-ary primops for `n > 2`.
+
+    /// Replace a substring by another one in a string.
+    ///
+    /// # Arguments
+    ///
+    /// 1. String to replace in.
+    /// 2. The string to replace.
+    /// 3. The replacement.
+    StringReplace,
+
+    /// Replace all substrings matching a pattern by a given string.
+    ///
+    /// # Arguments
+    ///
+    /// 1. String to replace in.
+    /// 2. The pattern to replace.
+    /// 3. The replacement.
+    StringReplaceRegex,
+
+    /// Return a substring of an original string.
+    ///
+    /// Warning: the argument order is different than [crate::term::NAryOp::StringSubstr].
+    ///
+    /// # Arguments
+    ///
+    /// 1. Start index of the substring (included).
+    /// 2. End index of the substring (excluded).
+    /// 3. The string to slice.
+    StringSubstr,
+
+    /// The merge operator in contract mode (see [crate::eval::merge]).
+    ///
+    /// # Arguments
+    ///
+    /// 1. The label.
+    /// 2. The record to check against the contract.
+    /// 3. The record contract.
+    MergeContract,
+
+    /// Seals one record into the tail of another. Used to ensure that functions using polymorphic
+    /// record contracts do not violate parametricity.
+    ///
+    /// # Arguments
+    ///
+    /// 1. A sealing key, which must be provided later to unseal the tail.
+    /// 2. A label, which will be used to assign blame correctly tail access
+    ///    is attempted.
+    /// 3. A record, which is the record we wish to seal the tail into.
+    /// 4. The record that we wish to seal.
+    RecordSealTail,
+
+    /// Unseals a term from the tail of a record and returns it.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The sealing key, which was used to seal the tail.
+    /// 2. A label which will be used to assign blame correctly if
+    ///     something goes wrong while unsealing.
+    /// 3. The record whose tail we wish to unseal.
+    RecordUnsealTail,
+
+    /// Insert type variable data into the `type_environment` of a [`crate::label::Label`]
+    ///
+    /// # Arguments
+    ///
+    /// 1. The sealing key assigned to the type variable.
+    /// 2. The introduction polarity](crate::label::Polarity) of the type variable
+    /// 3. The [kind](crate::typ::VarKind) of the type variable
+    /// 4. A label on which to operate.
+    LabelInsertTypeVar,
+
+    /// Return a sub-array corresponding to a range. Given that Nickel uses array slices under the
+    /// hood, as long as the array isn't modified later, this operation is constant in time and
+    /// memory. However, it will currently retain the original in memory until the slice becomes
+    /// dead.
+    ///
+    /// # Arguments
+    ///
+    /// 1. The start index of the slice (included).
+    /// 2. The end index of the slice (excluded).
+    /// 3. The array to slice.
+    ArraySlice,
+}
+
+impl fmt::Display for PrimOp {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        use PrimOp::*;
+
+        match self {
+            Typeof => write!(f, "typeof"),
+            BoolAnd => write!(f, "(&&)"),
+            BoolOr => write!(f, "(||)"),
+            BoolNot => write!(f, "bool/not"),
+            Blame => write!(f, "blame"),
+            EnumEmbed(_) => write!(f, "enum/embed"),
+            RecordStatAccess(_) => write!(f, "record/access"),
+            ArrayMap => write!(f, "array/map"),
+            RecordMap => write!(f, "record/map"),
+            LabelFlipPol => write!(f, "label/flip_polarity"),
+            LabelPol => write!(f, "label/polarity"),
+            LabelGoDom => write!(f, "label/go_dom"),
+            LabelGoCodom => write!(f, "label/go_codom"),
+            LabelGoArray => write!(f, "label/go_array"),
+            LabelGoDict => write!(f, "label/go_dict"),
+            Seq => write!(f, "seq"),
+            DeepSeq => write!(f, "deep_seq"),
+            ArrayLength => write!(f, "array/length"),
+            ArrayGen => write!(f, "array/generate"),
+            RecordFields(RecordOpKind::IgnoreEmptyOpt) => write!(f, "record/fields"),
+            RecordFields(RecordOpKind::ConsiderAllFields) => write!(f, "record/fields_with_opts"),
+            RecordValues => write!(f, "record/values"),
+            StringTrim => write!(f, "string/trim"),
+            StringChars => write!(f, "string/chars"),
+            StringUppercase => write!(f, "string/uppercase"),
+            StringLowercase => write!(f, "string/lowercase"),
+            StringLength => write!(f, "string/length"),
+            ToString => write!(f, "to_string"),
+            NumberFromString => write!(f, "number/from_string"),
+            EnumFromString => write!(f, "enum/from_string"),
+            StringIsMatch => write!(f, "string/is_match"),
+            StringFind => write!(f, "string/find"),
+            StringFindAll => write!(f, "string/find_all"),
+            Force { .. } => write!(f, "force"),
+            RecordEmptyWithTail => write!(f, "record/empty_with_tail"),
+            Trace => write!(f, "trace"),
+            LabelPushDiag => write!(f, "label/push_diag"),
+
+            #[cfg(feature = "nix-experimental")]
+            EvalNix => write!(f, "eval_nix"),
+
+            EnumGetArg => write!(f, "enum/get_arg"),
+            EnumMakeVariant => write!(f, "enum/make_variant"),
+            EnumIsVariant => write!(f, "enum/is_variant"),
+            EnumGetTag => write!(f, "enum/get_tag"),
+
+            ContractCustom => write!(f, "contract/custom"),
+
+            NumberArcCos => write!(f, "number/arccos"),
+            NumberArcSin => write!(f, "number/arcsin"),
+            NumberArcTan => write!(f, "number/arctan"),
+            NumberCos => write!(f, "number/cos"),
+            NumberSin => write!(f, "number/sin"),
+            NumberTan => write!(f, "number/tan"),
+
+            Plus => write!(f, "(+)"),
+            Sub => write!(f, "(-)"),
+            Mult => write!(f, "(*)"),
+            Div => write!(f, "(/)"),
+            Modulo => write!(f, "(%)"),
+            NumberArcTan2 => write!(f, "number/arctan2"),
+            NumberLog => write!(f, "number/log"),
+            Pow => write!(f, "pow"),
+            StringConcat => write!(f, "string/concat"),
+            Eq => write!(f, "(==)"),
+            LessThan => write!(f, "(<)"),
+            LessOrEq => write!(f, "(<=)"),
+            GreaterThan => write!(f, "(>)"),
+            GreaterOrEq => write!(f, "(>=)"),
+            ContractApply => write!(f, "contract/apply"),
+            ContractCheck => write!(f, "contract/check"),
+            LabelWithErrorData => write!(f, "label/with_error_data"),
+            LabelGoField => write!(f, "label/go_field"),
+            RecordInsert(RecordOpKind::IgnoreEmptyOpt) => write!(f, "record/insert"),
+            RecordInsert(RecordOpKind::ConsiderAllFields) => write!(f, "record/insert_with_opts"),
+            RecordRemove(RecordOpKind::IgnoreEmptyOpt) => write!(f, "record/remove"),
+            RecordRemove(RecordOpKind::ConsiderAllFields) => write!(f, "record/remove_with_opts"),
+            RecordGet => write!(f, "record/get"),
+            RecordHasField(RecordOpKind::IgnoreEmptyOpt) => write!(f, "record/has_field"),
+            RecordHasField(RecordOpKind::ConsiderAllFields) => {
+                write!(f, "record/has_field_with_opts")
+            }
+            RecordFieldIsDefined(RecordOpKind::IgnoreEmptyOpt) => {
+                write!(f, "record/field_is_defined")
+            }
+            RecordFieldIsDefined(RecordOpKind::ConsiderAllFields) => {
+                write!(f, "record/field_is_defined_with_opts")
+            }
+            Self::RecordSplitPair => write!(f, "record/split_pair"),
+            Self::RecordDisjointMerge => write!(f, "record/disjoint_merge"),
+            ArrayConcat => write!(f, "(@)"),
+            ArrayAt => write!(f, "array/at"),
+            Merge(_) => write!(f, "(&)"),
+            Hash => write!(f, "hash"),
+            Serialize => write!(f, "serialize"),
+            Deserialize => write!(f, "deserialize"),
+            StringSplit => write!(f, "string/split"),
+            StringContains => write!(f, "string/contains"),
+            StringCompare => write!(f, "string/compare"),
+            ContractArrayLazyApp => write!(f, "contract/array_lazy_apply"),
+            ContractRecordLazyApp => write!(f, "contract/record_lazy_apply"),
+            LabelWithMessage => write!(f, "label/with_message"),
+            LabelWithNotes => write!(f, "label/with_notes"),
+            LabelAppendNote => write!(f, "label/append_note"),
+            LabelLookupTypeVar => write!(f, "label/lookup_type_variable"),
+
+            StringReplace => write!(f, "string/replace"),
+            StringReplaceRegex => write!(f, "string/replace_regex"),
+            StringSubstr => write!(f, "string/substr"),
+            MergeContract => write!(f, "record/merge_contract"),
+            RecordSealTail => write!(f, "record/seal_tail"),
+            RecordUnsealTail => write!(f, "record/unseal_tail"),
+            LabelInsertTypeVar => write!(f, "label/insert_type_variable"),
+            ArraySlice => write!(f, "array/slice"),
+        }
+    }
+}
+
+impl PrimOp {
+    /// Returns the arity of the primop, i.e. the number of forced arguments it takes as a primop
+    /// application. Additional lazy arguments aren't counted here, and would be part of an outer
+    /// standard function application.
+    pub fn arity(&self) -> usize {
+        use PrimOp::*;
+
+        match self {
+            Typeof
+            | BoolAnd
+            | BoolOr
+            | BoolNot
+            | Blame
+            | EnumEmbed(_)
+            | RecordStatAccess(_)
+            | ArrayMap
+            | RecordMap
+            | LabelFlipPol
+            | LabelPol
+            | LabelGoDom
+            | LabelGoCodom
+            | LabelGoArray
+            | LabelGoDict
+            | Seq
+            | DeepSeq
+            | ArrayLength
+            | ArrayGen
+            | RecordFields(_)
+            | RecordValues
+            | StringTrim
+            | StringChars
+            | StringUppercase
+            | StringLowercase
+            | StringLength
+            | ToString
+            | NumberFromString
+            | EnumFromString
+            | StringIsMatch
+            | StringFind
+            | StringFindAll
+            | Force { .. }
+            | RecordEmptyWithTail
+            | Trace
+            | LabelPushDiag
+            | EnumGetArg
+            | EnumMakeVariant
+            | EnumIsVariant
+            | EnumGetTag
+            | ContractCustom
+            | NumberArcCos
+            | NumberArcSin
+            | NumberArcTan
+            | NumberCos
+            | NumberSin
+            | NumberTan => 1,
+            #[cfg(feature = "nix-experimental")]
+            EvalNix => 1,
+
+            Plus
+            | Sub
+            | Mult
+            | Div
+            | Modulo
+            | NumberArcTan2
+            | NumberLog
+            | Pow
+            | StringConcat
+            | Eq
+            | LessThan
+            | LessOrEq
+            | GreaterThan
+            | GreaterOrEq
+            | ContractApply
+            | ContractCheck
+            | LabelWithErrorData
+            | LabelGoField
+            | RecordInsert(_)
+            | RecordRemove(_)
+            | RecordGet
+            | RecordHasField(_)
+            | RecordFieldIsDefined(_)
+            | Self::RecordSplitPair
+            | Self::RecordDisjointMerge
+            | ArrayConcat
+            | ArrayAt
+            | Merge(_)
+            | Hash
+            | Serialize
+            | Deserialize
+            | StringSplit
+            | StringContains
+            | StringCompare
+            | ContractArrayLazyApp
+            | ContractRecordLazyApp
+            | LabelWithMessage
+            | LabelWithNotes
+            | LabelAppendNote
+            | LabelLookupTypeVar => 2,
+
+            StringReplace | StringReplaceRegex | StringSubstr | MergeContract
+            | RecordUnsealTail | ArraySlice => 3,
+
+            RecordSealTail | LabelInsertTypeVar => 4,
+        }
+    }
+}
+
+impl From<term::RecordOpKind> for RecordOpKind {
+    fn from(op: term::RecordOpKind) -> Self {
+        match op {
+            term::RecordOpKind::IgnoreEmptyOpt => RecordOpKind::IgnoreEmptyOpt,
+            term::RecordOpKind::ConsiderAllFields => RecordOpKind::ConsiderAllFields,
+        }
+    }
+}
diff --git a/core/src/bytecode/ast/record.rs b/core/src/bytecode/ast/record.rs
new file mode 100644
index 00000000..b05333af
--- /dev/null
+++ b/core/src/bytecode/ast/record.rs
@@ -0,0 +1,111 @@
+use super::{Annotation, Ast};
+
+use crate::{combine::Combine, identifier::LocIdent, term::MergePriority};
+
+use std::rc::Rc;
+
+/// Additional attributes for record.
+#[derive(Debug, Default, Eq, PartialEq, Copy, Clone)]
+pub struct RecordAttrs {
+    /// If the record is an open record, ie ending with `..`. Open records have a different
+    /// behavior when used as a record contract: they allow additional fields to be present.
+    pub open: bool,
+}
+
+impl Combine for RecordAttrs {
+    fn combine(left: Self, right: Self) -> Self {
+        RecordAttrs {
+            open: left.open || right.open,
+        }
+    }
+}
+
+/// The metadata attached to record fields.
+#[derive(Debug, PartialEq, Clone, Default)]
+pub struct FieldMetadata<'ast> {
+    /// The documentation of the field. This is allocated once and for all and shared through a
+    /// reference-counted pointer.
+    pub doc: Option<Rc<str>>,
+    /// Potential type and contract annotations.
+    pub annotation: Annotation<'ast>,
+    /// If the field is optional.
+    pub opt: bool,
+    /// If the field should be skipped during serialization.
+    pub not_exported: bool,
+    /// The merge priority.
+    pub priority: MergePriority,
+}
+
+impl<'ast> FieldMetadata<'ast> {
+    pub fn new() -> Self {
+        Default::default()
+    }
+
+    pub fn is_empty(&self) -> bool {
+        self.doc.is_none()
+            && self.annotation.is_empty()
+            && !self.opt
+            && !self.not_exported
+            && matches!(self.priority, MergePriority::Neutral)
+    }
+}
+
+impl<'ast> From<Annotation<'ast>> for FieldMetadata<'ast> {
+    fn from(annotation: Annotation<'ast>) -> Self {
+        FieldMetadata {
+            annotation,
+            ..Default::default()
+        }
+    }
+}
+
+/// A record field with its metadata.
+#[derive(Clone, Default, PartialEq, Debug)]
+pub struct Field<'ast> {
+    /// The value is optional because record field may not have a definition (e.g. optional fields).
+    pub value: Option<Ast<'ast>>,
+    /// The metadata attached to the field.
+    pub metadata: FieldMetadata<'ast>,
+}
+
+impl<'ast> From<Ast<'ast>> for Field<'ast> {
+    fn from(ast: Ast<'ast>) -> Self {
+        Field {
+            value: Some(ast),
+            ..Default::default()
+        }
+    }
+}
+
+impl<'ast> From<Annotation<'ast>> for Field<'ast> {
+    fn from(ann: Annotation<'ast>) -> Self {
+        Field::from(FieldMetadata::from(ann))
+    }
+}
+
+impl<'ast> From<FieldMetadata<'ast>> for Field<'ast> {
+    fn from(metadata: FieldMetadata<'ast>) -> Self {
+        Field {
+            metadata,
+            ..Default::default()
+        }
+    }
+}
+
+/// The base structure of a Nickel record.
+#[derive(Clone, Debug, Default, PartialEq)]
+pub struct Record<'ast> {
+    /// Fields whose names are known statically.
+    pub stat_fields: &'ast [(LocIdent, Field<'ast>)],
+    /// Fields whose names is a Nickel expression computed at runtime.
+    pub dyn_fields: &'ast [(Ast<'ast>, Field<'ast>)],
+    /// If the record is open, i.e. if it ended with `..`.
+    pub open: bool,
+}
+
+impl<'ast> Record<'ast> {
+    /// A record with no fields and the default set of attributes.
+    pub fn empty() -> Self {
+        Default::default()
+    }
+}
diff --git a/core/src/bytecode/mod.rs b/core/src/bytecode/mod.rs
new file mode 100644
index 00000000..b65bb35b
--- /dev/null
+++ b/core/src/bytecode/mod.rs
@@ -0,0 +1,6 @@
+//! Experimental bytecode compiler, virtual machine, and their intermediate representations.
+//!
+//! This implementation is under construction; it's currently not usable and it's not available by
+//! default in mainline Nickel.
+
+pub mod ast;
diff --git a/core/src/cache.rs b/core/src/cache.rs
index e07dcb3d..29920174 100644
--- a/core/src/cache.rs
+++ b/core/src/cache.rs
@@ -14,7 +14,7 @@ use crate::term::record::{Field, RecordData};
 use crate::term::{RichTerm, SharedTerm, Term};
 use crate::transform::import_resolution;
 use crate::typ::UnboundTypeVariableError;
-use crate::typecheck::{self, type_check, Wildcards};
+use crate::typecheck::{self, type_check, TypecheckMode, Wildcards};
 use crate::{eval, parser, transform};
 
 use codespan::{FileId, Files};
@@ -638,6 +638,7 @@ impl Cache {
         &mut self,
         file_id: FileId,
         initial_ctxt: &typecheck::Context,
+        initial_mode: TypecheckMode,
     ) -> Result<CacheOp<()>, CacheError<TypecheckError>> {
         match self.terms.get(&file_id) {
             Some(TermEntry { state, .. }) if *state >= EntryState::Typechecked => {
@@ -645,13 +646,13 @@ impl Cache {
             }
             Some(TermEntry { term, state, .. }) if *state >= EntryState::Parsed => {
                 if *state < EntryState::Typechecking {
-                    let wildcards = type_check(term, initial_ctxt.clone(), self)?;
+                    let wildcards = type_check(term, initial_ctxt.clone(), self, initial_mode)?;
                     self.update_state(file_id, EntryState::Typechecking);
                     self.wildcards.insert(file_id, wildcards);
 
                     if let Some(imports) = self.imports.get(&file_id).cloned() {
                         for f in imports.into_iter() {
-                            self.typecheck(f, initial_ctxt)?;
+                            self.typecheck(f, initial_ctxt, initial_mode)?;
                         }
                     }
 
@@ -1005,10 +1006,13 @@ impl Cache {
             result = CacheOp::Done(());
         }
 
-        let typecheck_res = self.typecheck(file_id, initial_ctxt).map_err(|cache_err| {
-            cache_err
-                .unwrap_error("cache::prepare(): expected source to be parsed before typechecking")
-        })?;
+        let typecheck_res = self
+            .typecheck(file_id, initial_ctxt, TypecheckMode::Walk)
+            .map_err(|cache_err| {
+                cache_err.unwrap_error(
+                    "cache::prepare(): expected source to be parsed before typechecking",
+                )
+            })?;
         if typecheck_res == CacheOp::Done(()) {
             result = CacheOp::Done(());
         };
@@ -1052,7 +1056,7 @@ impl Cache {
             resolved_ids: pending,
         } = import_resolution::strict::resolve_imports(term, self)?;
 
-        let wildcards = type_check(&term, initial_ctxt.clone(), self)?;
+        let wildcards = type_check(&term, initial_ctxt.clone(), self, TypecheckMode::Walk)?;
         let term = transform::transform(term, Some(&wildcards))
             .map_err(|err| Error::ParseErrors(err.into()))?;
         Ok((term, pending))
@@ -1291,7 +1295,7 @@ impl Cache {
         if let Some(ids) = self.stdlib_ids.as_ref().cloned() {
             ids.iter()
                 .try_fold(CacheOp::Cached(()), |cache_op, (_, file_id)| {
-                    match self.typecheck(*file_id, initial_ctxt)? {
+                    match self.typecheck(*file_id, initial_ctxt, TypecheckMode::Walk)? {
                         done @ CacheOp::Done(()) => Ok(done),
                         _ => Ok(cache_op),
                     }
diff --git a/core/src/error/mod.rs b/core/src/error/mod.rs
index fca69a1d..12d9af8a 100644
--- a/core/src/error/mod.rs
+++ b/core/src/error/mod.rs
@@ -346,26 +346,17 @@ pub enum TypecheckError {
         cause: Box<TypecheckError>,
         pos: TermPos,
     },
-    /// This error should mostly not happen: contracts (flat types) are now properly checked for
-    /// equality. This error is raised when flat types are encountered during unification, but flat
-    /// types should all have been converted to `typecheck::UnifType::Contract` at this point.
-    /// Consider this as an internal, unexpected error.
-    IncomparableFlatTypes {
-        expected: RichTerm,
-        inferred: RichTerm,
-        pos: TermPos,
-    },
     /// Within statically typed code, the typechecker must reject terms containing nonsensical
     /// contracts such as `let C = { foo : (4 + 1) } in ({ foo = 5 } | C)`, which will fail at
     /// runtime.
     ///
     /// The typechecker is currently quite conservative and simply forbids to store any custom
-    /// contract (flat type) in a type that appears in term position. Note that this restriction
+    /// contract in a type that appears in term position. Note that this restriction
     /// doesn't apply to annotations, which aren't considered part of the statically typed block.
     /// For example, `{foo = 5} | {foo : (4 + 1)}` is accepted by the typechecker.
-    FlatTypeInTermPosition {
+    CtrTypeInTermPos {
         /// The term that was in a flat type (the `(4 + 1)` in the example above).
-        flat: RichTerm,
+        contract: RichTerm,
         /// The position of the entire type (the `{foo : 5}` in the example above).
         pos: TermPos,
     },
@@ -2245,13 +2236,13 @@ impl IntoDiagnostics<FileId> for TypecheckError {
                 pos,
             } => {
                 fn addendum(ty: &Type) -> &str {
-                    if ty.typ.is_flat() {
+                    if ty.typ.is_contract() {
                         " (a contract)"
                     } else {
                         ""
                     }
                 }
-                let last_note = if expected.typ.is_flat() ^ inferred.typ.is_flat() {
+                let last_note = if expected.typ.is_contract() ^ inferred.typ.is_contract() {
                     "Static types and contracts are not compatible"
                 } else {
                     "These types are not compatible"
@@ -2525,20 +2516,6 @@ impl IntoDiagnostics<FileId> for TypecheckError {
 
                 diags
             }
-            TypecheckError::IncomparableFlatTypes {
-                expected,
-                inferred,
-                pos,
-            } => {
-                vec![Diagnostic::error()
-                    .with_message("internal error: can't compare unconverted flat types")
-                    .with_labels(mk_expr_label(&pos))
-                    .with_notes(vec![
-                        format!("{} (contract)", mk_expected_msg(&expected.to_string()),),
-                        format!("{} (contract)", mk_inferred_msg(&inferred.to_string()),),
-                        String::from(INTERNAL_ERROR_MSG),
-                    ])]
-            }
             TypecheckError::ForallParametricityViolation {
                 kind,
                 tail,
@@ -2561,7 +2538,7 @@ impl IntoDiagnostics<FileId> for TypecheckError {
                             .to_owned(),
                     ])]
             }
-            TypecheckError::FlatTypeInTermPosition { flat, pos } => {
+            TypecheckError::CtrTypeInTermPos { contract, pos } => {
                 vec![Diagnostic::error()
                     .with_message(
                         "types containing user-defined contracts cannot be converted into contracts"
@@ -2572,7 +2549,7 @@ impl IntoDiagnostics<FileId> for TypecheckError {
                                 primary(&span).with_message("This type (in contract position)")
                             })
                             .into_iter()
-                            .chain(flat.pos.into_opt().map(|span| {
+                            .chain(contract.pos.into_opt().map(|span| {
                                 secondary(&span).with_message("contains this user-defined contract")
                             }))
                             .collect(),
diff --git a/core/src/eval/merge.rs b/core/src/eval/merge.rs
index d0418d73..b072ae8f 100644
--- a/core/src/eval/merge.rs
+++ b/core/src/eval/merge.rs
@@ -229,7 +229,7 @@ pub fn merge<C: Cache>(
             );
 
             let label = Label {
-                typ: Rc::new(TypeF::Flat(contract_for_display).into()),
+                typ: Rc::new(TypeF::Contract(contract_for_display).into()),
                 span: MergeLabel::from(mode).span,
                 ..Default::default()
             }
diff --git a/core/src/lib.rs b/core/src/lib.rs
index e1785af7..32ecbe27 100644
--- a/core/src/lib.rs
+++ b/core/src/lib.rs
@@ -1,3 +1,5 @@
+#[cfg(feature = "bytecode-experimental")]
+pub mod bytecode;
 pub mod cache;
 pub mod closurize;
 pub mod combine;
diff --git a/core/src/parser/uniterm.rs b/core/src/parser/uniterm.rs
index bcef7fc9..58ac8296 100644
--- a/core/src/parser/uniterm.rs
+++ b/core/src/parser/uniterm.rs
@@ -110,7 +110,7 @@ impl TryFrom<UniTerm> for Type {
                     return Err(ParseError::InvalidContract(ut.pos.unwrap()));
                 }
 
-                Type::from(TypeF::Flat(rt))
+                Type::from(TypeF::Contract(rt))
             }
         };
 
@@ -128,7 +128,7 @@ impl TryFrom<UniTerm> for RichTerm {
             UniTermNode::Record(r) => RichTerm::try_from(r)?,
             UniTermNode::Type(mut typ) => {
                 typ.fix_type_vars(pos.unwrap())?;
-                if let TypeF::Flat(rt) = typ.typ {
+                if let TypeF::Contract(rt) = typ.typ {
                     rt.with_pos(pos)
                 } else {
                     let contract = typ
@@ -538,7 +538,7 @@ impl TryFrom<UniRecord> for Type {
             let pos = ur.pos;
             ur.clone().into_type_strict().or_else(|_| {
                 RichTerm::try_from(ur).map(|rt| Type {
-                    typ: TypeF::Flat(rt),
+                    typ: TypeF::Contract(rt),
                     pos,
                 })
             })
@@ -619,7 +619,7 @@ impl VarKindCell {
 pub(super) trait FixTypeVars {
     /// Post-process a type at the right hand side of an annotation by replacing each unbound type
     /// variable `TypeF::Var(id)` by a term variable with the same identifier seen as a custom
-    /// contract `TypeF::Flat(Term::Var(id))`.
+    /// contract `TypeF::Contract(Term::Var(id))`.
     ///
     /// Additionally, this passes determine the kind of a variable introduced by a forall binder.
     ///
@@ -702,7 +702,7 @@ impl FixTypeVars for Type {
             | TypeF::String
             | TypeF::ForeignId
             | TypeF::Symbol
-            | TypeF::Flat(_)
+            | TypeF::Contract(_)
             // We don't fix type variables inside a dictionary contract. A dictionary contract
             // should not be considered as a static type, but instead work as a contract. In
             // particular mustn't be allowed to capture type variables from the enclosing type: see
@@ -723,7 +723,7 @@ impl FixTypeVars for Type {
                         })?;
                 } else {
                     let id = LocIdent::from(sym).with_pos(self.pos);
-                    self.typ = TypeF::Flat(RichTerm::new(Term::Var(id), id.pos));
+                    self.typ = TypeF::Contract(RichTerm::new(Term::Var(id), id.pos));
                 }
                 Ok(())
             }
diff --git a/core/src/pretty.rs b/core/src/pretty.rs
index d094db88..a4492145 100644
--- a/core/src/pretty.rs
+++ b/core/src/pretty.rs
@@ -136,7 +136,7 @@ fn contains_carriage_return<T>(chunks: &[StrChunk<T>]) -> bool {
 /// example when said term is a function function. This function precisely determines if the given
 /// type is such a term.
 fn needs_parens_in_type_pos(typ: &Type) -> bool {
-    if let TypeF::Flat(term) = &typ.typ {
+    if let TypeF::Contract(term) = &typ.typ {
         matches!(
             term.as_ref(),
             Term::Fun(..)
@@ -1248,7 +1248,7 @@ impl<'a> Pretty<'a, Allocator> for &Type {
             .group(),
             ForeignId => allocator.text("ForeignId"),
             Symbol => allocator.text("Symbol"),
-            Flat(t) => t.pretty(allocator),
+            Contract(t) => t.pretty(allocator),
             Var(var) => allocator.as_string(var),
             Forall { var, ref body, .. } => {
                 let mut curr = body.as_ref();
diff --git a/core/src/program.rs b/core/src/program.rs
index 4f2d6a81..cab770e2 100644
--- a/core/src/program.rs
+++ b/core/src/program.rs
@@ -36,6 +36,7 @@ use crate::{
         record::Field,
         BinaryOp, MergePriority, RichTerm, Term,
     },
+    typecheck::TypecheckMode,
 };
 
 use clap::ColorChoice;
@@ -531,7 +532,7 @@ impl<EC: EvalCache> Program<EC> {
     }
 
     /// Load, parse, and typecheck the program and the standard library, if not already done.
-    pub fn typecheck(&mut self) -> Result<(), Error> {
+    pub fn typecheck(&mut self, initial_mode: TypecheckMode) -> Result<(), Error> {
         self.vm
             .import_resolver_mut()
             .parse(self.main_id, InputFormat::Nickel)?;
@@ -548,7 +549,7 @@ impl<EC: EvalCache> Program<EC> {
             })?;
         self.vm
             .import_resolver_mut()
-            .typecheck(self.main_id, &initial_env)
+            .typecheck(self.main_id, &initial_env, initial_mode)
             .map_err(|cache_err| {
                 cache_err.unwrap_error("program::typecheck(): expected source to be parsed")
             })?;
@@ -1186,7 +1187,7 @@ mod tests {
                     TermPos::None,
                 ))
             })?;
-        p.typecheck()
+        p.typecheck(TypecheckMode::Walk)
     }
 
     #[test]
diff --git a/core/src/repl/mod.rs b/core/src/repl/mod.rs
index 28ef952f..b7c35d10 100644
--- a/core/src/repl/mod.rs
+++ b/core/src/repl/mod.rs
@@ -20,6 +20,7 @@ use crate::term::TraverseOrder;
 use crate::term::{record::Field, RichTerm, Term, Traverse};
 use crate::transform::import_resolution;
 use crate::typ::Type;
+use crate::typecheck::TypecheckMode;
 use crate::{eval, transform, typecheck};
 use codespan::FileId;
 use simple_counter::*;
@@ -129,8 +130,12 @@ impl<EC: EvalCache> ReplImpl<EC> {
                 })?;
         }
 
-        let wildcards =
-            typecheck::type_check(&t, self.env.type_ctxt.clone(), self.vm.import_resolver())?;
+        let wildcards = typecheck::type_check(
+            &t,
+            self.env.type_ctxt.clone(),
+            self.vm.import_resolver(),
+            TypecheckMode::Walk,
+        )?;
 
         if let Some(id) = id {
             typecheck::env_add(
@@ -150,7 +155,7 @@ impl<EC: EvalCache> ReplImpl<EC> {
         for id in &pending {
             self.vm
                 .import_resolver_mut()
-                .typecheck(*id, &self.initial_type_ctxt)
+                .typecheck(*id, &self.initial_type_ctxt, TypecheckMode::Walk)
                 .map_err(|cache_err| {
                     cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
                 })?;
@@ -293,8 +298,12 @@ impl<EC: EvalCache> Repl for ReplImpl<EC> {
             self.vm.import_resolver_mut().resolve_imports(*id).unwrap();
         }
 
-        let wildcards =
-            typecheck::type_check(&term, self.env.type_ctxt.clone(), self.vm.import_resolver())?;
+        let wildcards = typecheck::type_check(
+            &term,
+            self.env.type_ctxt.clone(),
+            self.vm.import_resolver(),
+            TypecheckMode::Walk,
+        )?;
         // Substitute the wildcard types for their inferred types We need to `traverse` the term, in
         // case the type depends on inner terms that also contain wildcards
         let term = term
diff --git a/core/src/term/pattern/mod.rs b/core/src/term/pattern/mod.rs
index d1880321..bef1463d 100644
--- a/core/src/term/pattern/mod.rs
+++ b/core/src/term/pattern/mod.rs
@@ -14,8 +14,6 @@ use crate::{
 pub mod bindings;
 pub mod compile;
 
-/// A small helper to generate a
-
 #[derive(Debug, PartialEq, Clone)]
 pub enum PatternData {
     /// A wildcard pattern, matching any value. As opposed to any, this pattern doesn't bind any
diff --git a/core/src/transform/free_vars.rs b/core/src/transform/free_vars.rs
index cecf9ca8..e2c1f034 100644
--- a/core/src/transform/free_vars.rs
+++ b/core/src/transform/free_vars.rs
@@ -227,7 +227,7 @@ impl CollectFreeVars for Type {
                 ty1.as_mut().collect_free_vars(set);
                 ty2.as_mut().collect_free_vars(set);
             }
-            TypeF::Flat(ref mut rt) => rt.collect_free_vars(set),
+            TypeF::Contract(ref mut rt) => rt.collect_free_vars(set),
         }
     }
 }
diff --git a/core/src/typ.rs b/core/src/typ.rs
index 2939b12f..04a80060 100644
--- a/core/src/typ.rs
+++ b/core/src/typ.rs
@@ -254,11 +254,12 @@ pub enum DictTypeFlavour {
 ///
 /// ## Type parameters
 ///
-/// Here, `TypeF` also takes two additional type parameters for the recursive unfolding of record
-/// rows and enum rows. We have other, distinct recursive subcomponents (or subtrees) in our
-/// complete definition, but the approach is unchanged.
+/// - `Ty`: the recursive unfolding of Nickel types
+/// - `RRows`: the recursive unfolding of record rows
+/// - `ERows`: the recursive unfolding of enum rows
+/// - `Te`: the type of a term (used to store contracts)
 #[derive(Clone, PartialEq, Debug)]
-pub enum TypeF<Ty, RRows, ERows> {
+pub enum TypeF<Ty, RRows, ERows, Te> {
     /// The dynamic type, or unitype. Assigned to values whose actual type is not statically known
     /// or checked.
     Dyn,
@@ -275,7 +276,7 @@ pub enum TypeF<Ty, RRows, ERows> {
     /// The type of `Term::ForeignId`.
     ForeignId,
     /// A type created from a user-defined contract.
-    Flat(RichTerm),
+    Contract(Te),
     /// A function.
     Arrow(Ty, Ty),
     /// A type variable.
@@ -324,7 +325,7 @@ pub struct RecordRows(pub RecordRowsF<Box<Type>, Box<RecordRows>>);
 /// Concrete, recursive type for a Nickel type.
 #[derive(Clone, PartialEq, Debug)]
 pub struct Type {
-    pub typ: TypeF<Box<Type>, RecordRows, EnumRows>,
+    pub typ: TypeF<Box<Type>, RecordRows, EnumRows, RichTerm>,
     pub pos: TermPos,
 }
 
@@ -512,7 +513,7 @@ impl<Ty, ERows> EnumRowsF<Ty, ERows> {
     }
 }
 
-impl<Ty, RRows, ERows> TypeF<Ty, RRows, ERows> {
+impl<Ty, RRows, ERows, Te> TypeF<Ty, RRows, ERows, Te> {
     /// Map functions over the children nodes of a type, when seen as a tree. The mutable state (
     /// `S`) is threaded through the calls to the mapped functions. Functions are fallible and may
     /// return an error `E`, which causes `try_map_state` to return early with the same error.
@@ -531,17 +532,19 @@ impl<Ty, RRows, ERows> TypeF<Ty, RRows, ERows> {
     ///
     /// Since `TypeF` may contain record rows and enum rows as well, `f_rrows` and `f_erows` are
     /// required to know how to map on record and enum types respectively.
-    pub fn try_map_state<TyO, RRowsO, ERowsO, FTy, FRRows, FERows, S, E>(
+    pub fn try_map_state<TyO, RRowsO, ERowsO, TeO, FTy, FRRows, FERows, FTe, S, E>(
         self,
         mut f: FTy,
         mut f_rrows: FRRows,
         mut f_erows: FERows,
+        mut f_ctr: FTe,
         state: &mut S,
-    ) -> Result<TypeF<TyO, RRowsO, ERowsO>, E>
+    ) -> Result<TypeF<TyO, RRowsO, ERowsO, TeO>, E>
     where
         FTy: FnMut(Ty, &mut S) -> Result<TyO, E>,
         FRRows: FnMut(RRows, &mut S) -> Result<RRowsO, E>,
         FERows: FnMut(ERows, &mut S) -> Result<ERowsO, E>,
+        FTe: FnMut(Te, &mut S) -> Result<TeO, E>,
     {
         match self {
             TypeF::Dyn => Ok(TypeF::Dyn),
@@ -550,7 +553,7 @@ impl<Ty, RRows, ERows> TypeF<Ty, RRows, ERows> {
             TypeF::String => Ok(TypeF::String),
             TypeF::ForeignId => Ok(TypeF::ForeignId),
             TypeF::Symbol => Ok(TypeF::Symbol),
-            TypeF::Flat(t) => Ok(TypeF::Flat(t)),
+            TypeF::Contract(t) => Ok(TypeF::Contract(f_ctr(t, state)?)),
             TypeF::Arrow(dom, codom) => Ok(TypeF::Arrow(f(dom, state)?, f(codom, state)?)),
             TypeF::Var(i) => Ok(TypeF::Var(i)),
             TypeF::Forall {
@@ -577,70 +580,102 @@ impl<Ty, RRows, ERows> TypeF<Ty, RRows, ERows> {
     }
 
     /// Variant of `try_map_state` without threaded state.
-    pub fn try_map<TyO, RRowsO, ERowsO, FTy, FRRows, FERows, E>(
+    pub fn try_map<TyO, RRowsO, ERowsO, TeO, FTy, FRRows, FERows, FTe, E>(
         self,
         mut f: FTy,
         mut f_rrows: FRRows,
         mut f_erows: FERows,
-    ) -> Result<TypeF<TyO, RRowsO, ERowsO>, E>
+        mut f_ctr: FTe,
+    ) -> Result<TypeF<TyO, RRowsO, ERowsO, TeO>, E>
     where
         FTy: FnMut(Ty) -> Result<TyO, E>,
         FRRows: FnMut(RRows) -> Result<RRowsO, E>,
         FERows: FnMut(ERows) -> Result<ERowsO, E>,
+        FTe: FnMut(Te) -> Result<TeO, E>,
     {
         let f_lifted = |ty: Ty, _: &mut ()| -> Result<TyO, E> { f(ty) };
         let f_rrows_lifted = |rrows: RRows, _: &mut ()| -> Result<RRowsO, E> { f_rrows(rrows) };
         let f_erows_lifted = |erows: ERows, _: &mut ()| -> Result<ERowsO, E> { f_erows(erows) };
-
-        self.try_map_state(f_lifted, f_rrows_lifted, f_erows_lifted, &mut ())
+        let f_ctr_lifted = |ctr: Te, _: &mut ()| -> Result<TeO, E> { f_ctr(ctr) };
+
+        self.try_map_state(
+            f_lifted,
+            f_rrows_lifted,
+            f_erows_lifted,
+            f_ctr_lifted,
+            &mut (),
+        )
     }
 
     /// Variant of `try_map_state` with infallible functions.
-    pub fn map_state<TyO, RRowsO, ERowsO, FTy, FRRows, FERows, S>(
+    pub fn map_state<TyO, RRowsO, ERowsO, TeO, FTy, FRRows, FERows, FTe, S>(
         self,
         mut f: FTy,
         mut f_rrows: FRRows,
         mut f_erows: FERows,
+        mut f_ctr: FTe,
         state: &mut S,
-    ) -> TypeF<TyO, RRowsO, ERowsO>
+    ) -> TypeF<TyO, RRowsO, ERowsO, TeO>
     where
         FTy: FnMut(Ty, &mut S) -> TyO,
         FRRows: FnMut(RRows, &mut S) -> RRowsO,
         FERows: FnMut(ERows, &mut S) -> ERowsO,
+        FTe: FnMut(Te, &mut S) -> TeO,
     {
-        let f_lifted = |ty: Ty, state: &mut S| -> Result<TyO, ()> { Ok(f(ty, state)) };
-        let f_rrows_lifted =
-            |rrows: RRows, state: &mut S| -> Result<RRowsO, ()> { Ok(f_rrows(rrows, state)) };
-        let f_erows_lifted =
-            |erows: ERows, state: &mut S| -> Result<ERowsO, ()> { Ok(f_erows(erows, state)) };
-        self.try_map_state(f_lifted, f_rrows_lifted, f_erows_lifted, state)
-            .unwrap()
+        let f_lifted = |ty: Ty, state: &mut S| -> Result<TyO, Infallible> { Ok(f(ty, state)) };
+        let f_rrows_lifted = |rrows: RRows, state: &mut S| -> Result<RRowsO, Infallible> {
+            Ok(f_rrows(rrows, state))
+        };
+        let f_erows_lifted = |erows: ERows, state: &mut S| -> Result<ERowsO, Infallible> {
+            Ok(f_erows(erows, state))
+        };
+        let f_ctr_lifted =
+            |ctr: Te, state: &mut S| -> Result<TeO, Infallible> { Ok(f_ctr(ctr, state)) };
+
+        self.try_map_state(
+            f_lifted,
+            f_rrows_lifted,
+            f_erows_lifted,
+            f_ctr_lifted,
+            state,
+        )
+        .unwrap()
     }
 
     /// Variant of `try_map_state` without threaded state and with infallible functions.
-    pub fn map<TyO, RRowsO, ERowsO, FTy, FRRows, FERows>(
+    pub fn map<TyO, RRowsO, ERowsO, TeO, FTy, FRRows, FERows, FTe>(
         self,
         mut f: FTy,
         mut f_rrows: FRRows,
         mut f_erows: FERows,
-    ) -> TypeF<TyO, RRowsO, ERowsO>
+        mut f_ctr: FTe,
+    ) -> TypeF<TyO, RRowsO, ERowsO, TeO>
     where
         FTy: FnMut(Ty) -> TyO,
         FRRows: FnMut(RRows) -> RRowsO,
         FERows: FnMut(ERows) -> ERowsO,
+        FTe: FnMut(Te) -> TeO,
     {
         let f_lifted = |ty: Ty, _: &mut ()| -> TyO { f(ty) };
         let f_rrows_lifted = |rrows: RRows, _: &mut ()| -> RRowsO { f_rrows(rrows) };
         let f_erows_lifted = |erows: ERows, _: &mut ()| -> ERowsO { f_erows(erows) };
-        self.map_state(f_lifted, f_rrows_lifted, f_erows_lifted, &mut ())
+        let f_ctr_lifted = |ctr: Te, _: &mut ()| -> TeO { f_ctr(ctr) };
+
+        self.map_state(
+            f_lifted,
+            f_rrows_lifted,
+            f_erows_lifted,
+            f_ctr_lifted,
+            &mut (),
+        )
     }
 
     pub fn is_wildcard(&self) -> bool {
         matches!(self, TypeF::Wildcard(_))
     }
 
-    pub fn is_flat(&self) -> bool {
-        matches!(self, TypeF::Flat(_))
+    pub fn is_contract(&self) -> bool {
+        matches!(self, TypeF::Contract(_))
     }
 }
 
@@ -857,7 +892,7 @@ impl Subcontract for Type {
             //
             // However, in the case of a contract embedded in a type, we don't want to do the
             // additional wrapping, as `t` should already be a fully constructed contract.
-            TypeF::Flat(ref t) => return Ok(t.clone()),
+            TypeF::Contract(ref t) => return Ok(t.clone()),
             TypeF::Var(id) => get_var_contract(&vars, id, self.pos)?,
             TypeF::Forall {
                 ref var,
@@ -1482,8 +1517,8 @@ impl Subcontract for RecordRows {
     }
 }
 
-impl From<TypeF<Box<Type>, RecordRows, EnumRows>> for Type {
-    fn from(typ: TypeF<Box<Type>, RecordRows, EnumRows>) -> Self {
+impl From<TypeF<Box<Type>, RecordRows, EnumRows, RichTerm>> for Type {
+    fn from(typ: TypeF<Box<Type>, RecordRows, EnumRows, RichTerm>) -> Self {
         Type {
             typ,
             pos: TermPos::None,
@@ -1568,15 +1603,15 @@ impl Type {
             | TypeF::Var(_)
             | TypeF::Record(_)
             | TypeF::Enum(_) => true,
-            TypeF::Flat(rt) if rt.as_ref().is_atom() => true,
+            TypeF::Contract(rt) if rt.as_ref().is_atom() => true,
             _ => false,
         }
     }
 
-    /// Searches for a `TypeF::Flat`. If one is found, returns the term it contains.
-    pub fn find_flat(&self) -> Option<RichTerm> {
+    /// Searches for a `TypeF::Contract`. If one is found, returns the term it contains.
+    pub fn find_contract(&self) -> Option<RichTerm> {
         self.find_map(|ty: &Type| match &ty.typ {
-            TypeF::Flat(f) => Some(f.clone()),
+            TypeF::Contract(f) => Some(f.clone()),
             _ => None,
         })
     }
@@ -1756,6 +1791,7 @@ impl Traverse<Type> for Type {
             |ty, f| Ok(Box::new(ty.traverse(f, order)?)),
             |rrows, f| rrows.traverse(f, order),
             |erows, _| Ok(erows),
+            |ctr, _| Ok(ctr),
             f,
         )?;
 
@@ -1794,7 +1830,7 @@ impl Traverse<Type> for Type {
             | TypeF::Var(_)
             | TypeF::Enum(_)
             | TypeF::Wildcard(_) => None,
-            TypeF::Flat(rt) => rt.traverse_ref(f, state),
+            TypeF::Contract(rt) => rt.traverse_ref(f, state),
             TypeF::Arrow(t1, t2) => t1
                 .traverse_ref(f, state)
                 .or_else(|| t2.traverse_ref(f, state)),
@@ -1813,9 +1849,9 @@ impl Traverse<RichTerm> for Type {
     {
         self.traverse(
             &mut |ty: Type| match ty.typ {
-                TypeF::Flat(t) => t
+                TypeF::Contract(t) => t
                     .traverse(f, order)
-                    .map(|t| Type::from(TypeF::Flat(t)).with_pos(ty.pos)),
+                    .map(|t| Type::from(TypeF::Contract(t)).with_pos(ty.pos)),
                 _ => Ok(ty),
             },
             order,
@@ -1829,7 +1865,7 @@ impl Traverse<RichTerm> for Type {
     ) -> Option<U> {
         self.traverse_ref(
             &mut |ty: &Type, s: &S| match &ty.typ {
-                TypeF::Flat(t) => {
+                TypeF::Contract(t) => {
                     if let Some(ret) = t.traverse_ref(f, s) {
                         TraverseControl::Return(ret)
                     } else {
diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index e9835b28..42092946 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -1,4 +1,4 @@
-//! Computation of type equality for contracts (flat types).
+//! Computation of type equality for contracts.
 //!
 //! Determine if two contracts are equal as opaque types. Used to decide if two contract should
 //! unify.
@@ -702,7 +702,7 @@ fn type_eq_bounded<E: TermEnvironment>(
                         })
                         .unwrap_or(false)
                 }
-                (TypeF::Flat(t1), TypeF::Flat(t2)) => {
+                (TypeF::Contract((t1, env1)), TypeF::Contract((t2, env2))) => {
                     contract_eq_bounded(state, t1, env1, t2, env2)
                 }
                 (
@@ -757,9 +757,6 @@ fn type_eq_bounded<E: TermEnvironment>(
             id1 == id2
         }
         (GenericUnifType::Constant(i1), GenericUnifType::Constant(i2)) => i1 == i2,
-        (GenericUnifType::Contract(t1, env2), GenericUnifType::Contract(t2, env1)) => {
-            contract_eq_bounded(state, t1, env1, t2, env2)
-        }
         _ => false,
     }
 }
diff --git a/core/src/typecheck/error.rs b/core/src/typecheck/error.rs
index 52c6b3fc..9a9f24a4 100644
--- a/core/src/typecheck/error.rs
+++ b/core/src/typecheck/error.rs
@@ -8,7 +8,6 @@ use crate::{
     identifier::LocIdent,
     label::ty_path,
     position::TermPos,
-    term::RichTerm,
     typ::{TypeF, VarKindDiscriminant},
 };
 
@@ -231,12 +230,6 @@ pub enum UnifError {
         expected_const_id: VarId,
         inferred: UnifType,
     },
-    /// A flat type, which is an opaque type corresponding to custom contracts, contained a Nickel
-    /// term different from a variable. Only a variables is a legal inner term of a flat type.
-    IncomparableFlatTypes {
-        expected: RichTerm,
-        inferred: RichTerm,
-    },
     /// An unbound type variable was referenced.
     UnboundTypeVariable(LocIdent),
     /// An error occurred when unifying the domains of two arrows.
@@ -353,13 +346,6 @@ impl UnifError {
                 violating_type: inferred.to_type(names_reg, state.table),
                 pos,
             },
-            UnifError::IncomparableFlatTypes { expected, inferred } => {
-                TypecheckError::IncomparableFlatTypes {
-                    expected,
-                    inferred,
-                    pos,
-                }
-            }
             UnifError::MissingRow {
                 id,
                 expected,
diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs
index 5088f8e8..def31528 100644
--- a/core/src/typecheck/mod.rs
+++ b/core/src/typecheck/mod.rs
@@ -17,9 +17,10 @@
 //!   typecheck. Walk mode also stores the annotations of bound identifiers in the environment. This
 //!   is implemented by the `walk` function.
 //!
-//! The algorithm starts in walk mode. A typed block (an expression annotated with a type) switches
-//! to enforce mode, and is switched back to walk mode when entering an expression annotated with a
-//! contract. Type and contract annotations thus serve as a switch for the typechecking mode.
+//! The algorithm usually starts in walk mode, although this can be configured. A typed block
+//! (an expression annotated with a type) switches to enforce mode, and is switched back to walk
+//! mode when entering an expression annotated with a contract. Type and contract annotations thus
+//! serve as a switch for the typechecking mode.
 //!
 //! Note that the static typing part (enforce mode) is based on the bidirectional typing framework,
 //! which defines two different modes. Thus, the enforce mode is itself divided again into
@@ -95,6 +96,15 @@ 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;
 
+/// The typechecker has two modes, one for statically typed code and one for dynamically type code.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum TypecheckMode {
+    /// In `Walk` mode, the typechecker traverses the AST looking for typed blocks.
+    Walk,
+    /// In `Enforce` mode, the typechecker checks types.
+    Enforce,
+}
+
 /// The typing environment.
 pub type Environment = GenericEnvironment<Ident, UnifType>;
 
@@ -218,7 +228,7 @@ impl<E: TermEnvironment> VarLevelUpperBound for GenericUnifType<E> {
                 var_levels_data, ..
             } => var_levels_data.upper_bound,
             GenericUnifType::UnifVar { init_level, .. } => *init_level,
-            GenericUnifType::Contract(..) | GenericUnifType::Constant(_) => VarLevel::NO_VAR,
+            GenericUnifType::Constant(_) => VarLevel::NO_VAR,
         }
     }
 }
@@ -241,12 +251,7 @@ impl<E: TermEnvironment> VarLevelUpperBound for GenericUnifTypeUnrolling<E> {
             TypeF::Record(rrows) => rrows.var_level_upper_bound(),
             TypeF::Dict { type_fields, .. } => type_fields.var_level_upper_bound(),
             TypeF::Array(ty_elts) => ty_elts.var_level_upper_bound(),
-            TypeF::Wildcard(_) | TypeF::Var(_) => VarLevel::NO_VAR,
-            // This should be unreachable, but let's not panic in release mode nonetheless
-            TypeF::Flat(_) => {
-                debug_assert!(false, "unexpected Flat type in var_level_upper_bound");
-                VarLevel::NO_VAR
-            }
+            TypeF::Wildcard(_) | TypeF::Var(_) | TypeF::Contract(_) => VarLevel::NO_VAR,
         }
     }
 }
@@ -330,10 +335,6 @@ pub enum GenericUnifType<E: TermEnvironment> {
         /// Additional metadata related to unification variable levels update. See [VarLevelsData].
         var_levels_data: VarLevelsData,
     },
-    /// A contract, seen as an opaque type. In order to compute type equality between contracts or
-    /// between a contract and a type, we need to carry an additional environment. This is why we
-    /// don't reuse the variant from [`crate::typ::TypeF`].
-    Contract(RichTerm, E),
     /// A rigid type constant which cannot be unified with anything but itself.
     Constant(VarId),
     /// A unification variable.
@@ -358,7 +359,7 @@ pub enum GenericUnifType<E: TermEnvironment> {
 }
 
 type GenericUnifTypeUnrolling<E> =
-    TypeF<Box<GenericUnifType<E>>, GenericUnifRecordRows<E>, GenericUnifEnumRows<E>>;
+    TypeF<Box<GenericUnifType<E>>, GenericUnifRecordRows<E>, GenericUnifEnumRows<E>, (RichTerm, E)>;
 
 impl<E: TermEnvironment> GenericUnifType<E> {
     /// Create a concrete generic unification type. Compute the variable levels data from the
@@ -438,23 +439,17 @@ impl<E: TermEnvironment + Clone> std::convert::TryInto<Type> for GenericUnifType
     fn try_into(self) -> Result<Type, ()> {
         match self {
             GenericUnifType::Concrete { typ, .. } => {
-                let converted: TypeF<Box<Type>, RecordRows, EnumRows> = typ.try_map(
+                let converted: TypeF<Box<Type>, RecordRows, EnumRows, RichTerm> = typ.try_map(
                     |uty_boxed| {
                         let ty: Type = (*uty_boxed).try_into()?;
                         Ok(Box::new(ty))
                     },
                     GenericUnifRecordRows::try_into,
                     GenericUnifEnumRows::try_into,
+                    |(term, _env)| Ok(term),
                 )?;
                 Ok(Type::from(converted))
             }
-            GenericUnifType::Contract(t, _) => {
-                let pos = t.pos;
-                Ok(Type {
-                    typ: TypeF::Flat(t),
-                    pos,
-                })
-            }
             _ => Err(()),
         }
     }
@@ -481,9 +476,7 @@ impl<E: TermEnvironment> GenericUnifEnumRows<E> {
 }
 
 impl<E: TermEnvironment + Clone> GenericUnifRecordRows<E> {
-    /// Create `GenericUnifRecordRows` from `RecordRows`. Contracts are represented as the separate
-    /// variant [`GenericUnifType::Contract`] which also stores a term environment, required for
-    /// checking type equality involving contracts.
+    /// Create `GenericUnifRecordRows` from `RecordRows`.
     pub fn from_record_rows(rrows: RecordRows, env: &E) -> Self {
         let f_rrow = |ty: Box<Type>| Box::new(GenericUnifType::from_type(*ty, env));
         let f_rrows =
@@ -552,6 +545,8 @@ impl<E: TermEnvironment> Subst<GenericUnifType<E>> for GenericUnifType<E> {
                             *upper_bound = max(*upper_bound, new_ub);
                             new_erows
                         },
+                        // Substitution doesn't cross the contract boundaries
+                        |ctr, _upper_bound| ctr,
                         &mut upper_bound,
                     ),
                     var_levels_data: VarLevelsData {
@@ -677,6 +672,7 @@ impl<E: TermEnvironment> Subst<GenericUnifRecordRows<E>> for GenericUnifType<E>
                         *upper_bound = max(*upper_bound, new_ub);
                         new_erows
                     },
+                    |ctr, _upper_bound| ctr,
                     &mut upper_bound,
                 );
 
@@ -806,6 +802,7 @@ impl<E: TermEnvironment> Subst<GenericUnifEnumRows<E>> for GenericUnifType<E> {
                         *upper_bound = max(*upper_bound, new_ub);
                         new_erows
                     },
+                    |ctr, _upper_bound| ctr,
                     &mut upper_bound,
                 );
 
@@ -920,18 +917,14 @@ impl<E: TermEnvironment> Subst<GenericUnifEnumRows<E>> for GenericUnifEnumRows<E
 }
 
 impl<E: TermEnvironment + Clone> GenericUnifType<E> {
-    /// Create a [`GenericUnifType`] from a [`Type`]. Contracts are represented as the separate
-    /// variant [`GenericUnifType::Contract`] which also stores a term environment, required for
-    /// checking type equality involving contracts.
+    /// Create a [`GenericUnifType`] from a [`Type`].
     pub fn from_type(ty: Type, env: &E) -> Self {
-        match ty.typ {
-            TypeF::Flat(t) => GenericUnifType::Contract(t, env.clone()),
-            ty => GenericUnifType::concrete(ty.map(
-                |ty_| Box::new(GenericUnifType::from_type(*ty_, env)),
-                |rrows| GenericUnifRecordRows::from_record_rows(rrows, env),
-                |erows| GenericUnifEnumRows::from_enum_rows(erows, env),
-            )),
-        }
+        GenericUnifType::concrete(ty.typ.map(
+            |ty_| Box::new(GenericUnifType::from_type(*ty_, env)),
+            |rrows| GenericUnifRecordRows::from_record_rows(rrows, env),
+            |erows| GenericUnifEnumRows::from_enum_rows(erows, env),
+            |term| (term, env.clone()),
+        ))
     }
 }
 
@@ -1050,10 +1043,10 @@ impl UnifType {
                     |btyp| Box::new(btyp.into_type(table)),
                     |urrows| urrows.into_rrows(table),
                     |uerows| uerows.into_erows(table),
+                    |(term, _env)| term,
                 );
                 Type::from(mapped)
             }
-            UnifType::Contract(t, _) => Type::from(TypeF::Flat(t)),
         }
     }
 
@@ -1067,12 +1060,8 @@ impl UnifType {
     }
 }
 
-// This implementation assumes that `TypeF::Flat` is not possible. If a [`UnifType`] has been
-// correctly created from a type using `from_type`, this must be the case.
 impl From<UnifTypeUnrolling> for UnifType {
     fn from(typ: UnifTypeUnrolling) -> Self {
-        debug_assert!(!matches!(typ, TypeF::Flat(_)));
-
         let var_level_max = typ.var_level_upper_bound();
 
         UnifType::Concrete {
@@ -1382,8 +1371,10 @@ pub fn type_check(
     t: &RichTerm,
     initial_ctxt: Context,
     resolver: &impl ImportResolver,
+    initial_mode: TypecheckMode,
 ) -> Result<Wildcards, TypecheckError> {
-    type_check_with_visitor(t, initial_ctxt, resolver, &mut ()).map(|tables| tables.wildcards)
+    type_check_with_visitor(t, initial_ctxt, resolver, &mut (), initial_mode)
+        .map(|tables| tables.wildcards)
 }
 
 /// Typecheck a term while providing the type information to a visitor.
@@ -1392,6 +1383,7 @@ pub fn type_check_with_visitor<V>(
     initial_ctxt: Context,
     resolver: &impl ImportResolver,
     visitor: &mut V,
+    initial_mode: TypecheckMode,
 ) -> Result<TypeTables, TypecheckError>
 where
     V: TypecheckVisitor,
@@ -1408,7 +1400,12 @@ where
             wildcard_vars: &mut wildcard_vars,
         };
 
-        walk(&mut state, initial_ctxt, visitor, t)?;
+        if initial_mode == TypecheckMode::Enforce {
+            let uty = state.table.fresh_type_uvar(initial_ctxt.var_level);
+            check(&mut state, initial_ctxt, visitor, t, uty)?;
+        } else {
+            walk(&mut state, initial_ctxt, visitor, t)?;
+        }
     }
 
     let result = wildcard_vars_to_type(wildcard_vars.clone(), &table);
@@ -1475,7 +1472,7 @@ fn walk<V: TypecheckVisitor>(
             walk(state, ctxt, visitor, t)
         }
         Term::FunPattern(pat, t) => {
-            let PatternTypeData { bindings: pat_bindings, ..} = pat.pattern_types(state, &ctxt, pattern::TypecheckMode::Walk)?;
+            let PatternTypeData { bindings: pat_bindings, ..} = pat.pattern_types(state, &ctxt, TypecheckMode::Walk)?;
             ctxt.type_env.extend(pat_bindings.into_iter().map(|(id, typ)| (id.ident(), typ)));
 
             walk(state, ctxt, visitor, t)
@@ -1552,7 +1549,7 @@ fn walk<V: TypecheckVisitor>(
                 //
                 // The use of start_ctxt here looks like it might be wrong for let rec, but in fact
                 // it's unused in TypecheckMode::Walk anyway.
-                let PatternTypeData {bindings: pat_bindings, ..} = pat.data.pattern_types(state, &start_ctxt, pattern::TypecheckMode::Walk)?;
+                let PatternTypeData {bindings: pat_bindings, ..} = pat.data.pattern_types(state, &start_ctxt, TypecheckMode::Walk)?;
 
                 for (id, typ) in pat_bindings {
                     visitor.visit_ident(&id, typ.clone());
@@ -1574,7 +1571,7 @@ fn walk<V: TypecheckVisitor>(
         Term::Match(data) => {
             data.branches.iter().try_for_each(|MatchBranch { pattern, guard, body }| {
                 let mut local_ctxt = ctxt.clone();
-                let PatternTypeData { bindings: pat_bindings, .. } = pattern.data.pattern_types(state, &ctxt, pattern::TypecheckMode::Walk)?;
+                let PatternTypeData { bindings: pat_bindings, .. } = pattern.data.pattern_types(state, &ctxt, TypecheckMode::Walk)?;
 
                 if let Some(alias) = &pattern.alias {
                     visitor.visit_ident(alias, mk_uniftype::dynamic());
@@ -1660,8 +1657,8 @@ fn walk<V: TypecheckVisitor>(
    }
 }
 
-/// Same as [`walk`] but operate on a type, which can contain terms as contracts (`TypeF::Flat`),
-/// instead of a term.
+/// Same as [`walk`] but operate on a type, which can contain terms as contracts
+/// ([crate::typ::TypeF::Contract]), instead of a term.
 fn walk_type<V: TypecheckVisitor>(
     state: &mut State,
     ctxt: Context,
@@ -1678,7 +1675,8 @@ fn walk_type<V: TypecheckVisitor>(
        // Currently, the parser can't generate unbound type variables by construction. Thus we
        // don't check here for unbound type variables again.
        | TypeF::Var(_)
-       // An enum type can't contain a flat type inside.
+       // An enum type can't contain a contract.
+       // TODO: the assertion above isn't true anymore (ADTs). Need fixing?
        | TypeF::Enum(_)
        | TypeF::Wildcard(_) => Ok(()),
        TypeF::Arrow(ty1, ty2) => {
@@ -1686,7 +1684,7 @@ fn walk_type<V: TypecheckVisitor>(
            walk_type(state, ctxt, visitor, ty2.as_ref())
        }
        TypeF::Record(rrows) => walk_rrows(state, ctxt, visitor, rrows),
-       TypeF::Flat(t) => walk(state, ctxt, visitor, t),
+       TypeF::Contract(t) => walk(state, ctxt, visitor, t),
        TypeF::Dict { type_fields: ty2, .. }
        | TypeF::Array(ty2)
        | TypeF::Forall {body: ty2, ..} => walk_type(state, ctxt, visitor, ty2),
@@ -1916,9 +1914,9 @@ fn check<V: TypecheckVisitor>(
         }
         Term::FunPattern(pat, t) => {
             // See [^separate-alias-treatment].
-            let pat_types =
-                pat.data
-                    .pattern_types(state, &ctxt, pattern::TypecheckMode::Enforce)?;
+            let pat_types = pat
+                .data
+                .pattern_types(state, &ctxt, TypecheckMode::Enforce)?;
             // In the destructuring case, there's no alternative pattern, and we must thus
             // immediately close all the row types.
             pattern::close_all_enums(pat_types.enum_open_tails, state);
@@ -2036,8 +2034,7 @@ fn check<V: TypecheckVisitor>(
             let start_ctxt = ctxt.clone();
             for (pat, re) in bindings {
                 // See [^separate-alias-treatment].
-                let pat_types =
-                    pat.pattern_types(state, &start_ctxt, pattern::TypecheckMode::Enforce)?;
+                let pat_types = pat.pattern_types(state, &start_ctxt, TypecheckMode::Enforce)?;
 
                 // In the destructuring case, there's no alternative pattern, and we must thus
                 // immediatly close all the row types.
@@ -2109,11 +2106,9 @@ fn check<V: TypecheckVisitor>(
                 .map(|branch| -> Result<_, TypecheckError> {
                     Ok((
                         branch,
-                        branch.pattern.pattern_types(
-                            state,
-                            &ctxt,
-                            pattern::TypecheckMode::Enforce,
-                        )?,
+                        branch
+                            .pattern
+                            .pattern_types(state, &ctxt, TypecheckMode::Enforce)?,
                     ))
                 })
                 .collect::<Result<Vec<(&MatchBranch, PatternTypeData<_>)>, _>>()?;
@@ -2425,8 +2420,11 @@ fn check<V: TypecheckVisitor>(
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Type { typ, contract: _ } => {
-            if let Some(flat) = typ.find_flat() {
-                Err(TypecheckError::FlatTypeInTermPosition { flat, pos: *pos })
+            if let Some(contract) = typ.find_contract() {
+                Err(TypecheckError::CtrTypeInTermPos {
+                    contract,
+                    pos: *pos,
+                })
             } else {
                 Ok(())
             }
@@ -2760,7 +2758,6 @@ fn replace_wildcards_with_var(
 
     match ty.typ {
         TypeF::Wildcard(i) => get_wildcard_var(table, ctxt.var_level, wildcard_vars, i),
-        TypeF::Flat(t) => UnifType::Contract(t, ctxt.term_env.clone()),
         _ => UnifType::concrete(ty.typ.map_state(
             |ty, (table, wildcard_vars)| {
                 Box::new(replace_wildcards_with_var(table, ctxt, wildcard_vars, *ty))
@@ -2768,6 +2765,7 @@ fn replace_wildcards_with_var(
             |rrows, (table, wildcard_vars)| replace_rrows(table, ctxt, wildcard_vars, rrows),
             // Enum rows contain neither wildcards nor contracts
             |erows, (table, wildcard_vars)| replace_erows(table, ctxt, wildcard_vars, erows),
+            |ctr, _| (ctr, ctxt.term_env.clone()),
             &mut (table, wildcard_vars),
         )),
     }
diff --git a/core/src/typecheck/operation.rs b/core/src/typecheck/operation.rs
index 0d5ed874..dfad9955 100644
--- a/core/src/typecheck/operation.rs
+++ b/core/src/typecheck/operation.rs
@@ -643,16 +643,7 @@ pub fn custom_contract_type() -> UnifType {
 /// |]
 /// ```
 pub fn custom_contract_ret_type() -> UnifType {
-    mk_uty_enum!(
-        ("Ok", mk_uniftype::dynamic()),
-        // /!\ IMPORTANT
-        //
-        // During typechecking, `TypeF::Flat` all have been transformed to `UnifType::Contract(..)`
-        // with their associated environment. Generating a `TypeF::Flat` at this point will panic
-        // in the best case (we should catch that), or have incorrect behavior in the worst case.
-        // Do not turn this into `UnifType::concrete(TypeF::Flat(..))`.
-        ("Error", error_data_type())
-    )
+    mk_uty_enum!(("Ok", mk_uniftype::dynamic()), ("Error", error_data_type()))
 }
 
 /// The type of error data that can be returned by a custom contract:
@@ -686,5 +677,8 @@ fn error_data_type() -> UnifType {
         .optional()
         .no_value();
 
-    UnifType::Contract(error_data.build(), SimpleTermEnvironment::new())
+    UnifType::concrete(TypeF::Contract((
+        error_data.build(),
+        SimpleTermEnvironment::new(),
+    )))
 }
diff --git a/core/src/typecheck/pattern.rs b/core/src/typecheck/pattern.rs
index ace9c93a..5dbfd544 100644
--- a/core/src/typecheck/pattern.rs
+++ b/core/src/typecheck/pattern.rs
@@ -8,12 +8,6 @@ use crate::{
 
 use super::*;
 
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
-pub(super) enum TypecheckMode {
-    Walk,
-    Enforce,
-}
-
 /// A list of pattern variables and their associated type.
 pub type TypeBindings = Vec<(LocIdent, UnifType)>;
 
diff --git a/core/src/typecheck/reporting.rs b/core/src/typecheck/reporting.rs
index af1a4a06..e95f7599 100644
--- a/core/src/typecheck/reporting.rs
+++ b/core/src/typecheck/reporting.rs
@@ -156,11 +156,11 @@ impl ToType for UnifType {
                     |btyp, reg| Box::new(btyp.to_type(reg, table)),
                     |rrows, reg| rrows.to_type(reg, table),
                     |erows, reg| erows.to_type(reg, table),
+                    |(ctr, _env), _reg| ctr,
                     reg,
                 );
                 Type::from(mapped)
             }
-            UnifType::Contract(t, _) => Type::from(TypeF::Flat(t)),
         }
     }
 }
diff --git a/core/src/typecheck/unif.rs b/core/src/typecheck/unif.rs
index 648eee86..2f2b2ad4 100644
--- a/core/src/typecheck/unif.rs
+++ b/core/src/typecheck/unif.rs
@@ -439,6 +439,7 @@ impl UnifTable {
                 |uty, table| Box::new(update_utype_with_lvl(table, *uty, level)),
                 |rrows, table| update_rrows_with_lvl(table, rrows, level),
                 |erows, table| update_erows_with_lvl(table, erows, level),
+                |ctr, _| ctr,
                 table,
             )
         }
@@ -535,7 +536,7 @@ impl UnifTable {
                         },
                     }
                 }
-                UnifType::Constant(_) | UnifType::Contract(..) | UnifType::Concrete { .. } => uty,
+                UnifType::Constant(_) | UnifType::Concrete { .. } => uty,
             }
         }
 
@@ -613,9 +614,7 @@ impl UnifTable {
                 //
                 // Note that this type might still contain other pending updates deeper inside, but
                 // those are registered as pending updates and will be processed in any case.
-                UnifType::Constant(_) | UnifType::Contract(..) | UnifType::Concrete { .. } => {
-                    (uty, false)
-                }
+                UnifType::Constant(_) | UnifType::Concrete { .. } => (uty, false),
             }
         }
 
@@ -679,6 +678,7 @@ impl UnifTable {
                         |uty, table| Box::new(update_utype_with_lvl(table, *uty, level)),
                         |rrows, table| update_rrows_with_lvl(table, rrows, level),
                         |erows, table| update_erows_with_lvl(table, erows, level),
+                        |ctr, _| ctr,
                         table,
                     );
 
@@ -688,7 +688,7 @@ impl UnifTable {
                         var_levels_data,
                     }
                 }
-                UnifType::UnifVar { .. } | UnifType::Constant(_) | UnifType::Contract(..) => utype,
+                UnifType::UnifVar { .. } | UnifType::Constant(_) => utype,
             }
         }
 
@@ -870,6 +870,7 @@ impl UnifTable {
                         |uty, table| Box::new(update_utype_with_lvl(table, *uty, level)),
                         |rrows, table| update_rrows_with_lvl(table, rrows, level),
                         |erows, table| update_erows_with_lvl(table, erows, level),
+                        |ctr, _| ctr,
                         table,
                     );
 
@@ -879,7 +880,7 @@ impl UnifTable {
                         var_levels_data,
                     }
                 }
-                UnifType::UnifVar { .. } | UnifType::Constant(_) | UnifType::Contract(..) => utype,
+                UnifType::UnifVar { .. } | UnifType::Constant(_) => utype,
             }
         }
 
@@ -1227,8 +1228,10 @@ impl Unify for UnifType {
                             cause: Box::new(err),
                         })
                 }
-                (TypeF::Flat(expected), TypeF::Flat(inferred)) => {
-                    Err(UnifError::IncomparableFlatTypes { expected, inferred })
+                (TypeF::Contract((t1, env1)), TypeF::Contract((t2, env2)))
+                    if eq::contract_eq(state.table.max_uvars_count(), &t1, &env1, &t2, &env2) =>
+                {
+                    Ok(())
                 }
                 (TypeF::Enum(erows1), TypeF::Enum(erows2)) => erows1
                     .clone()
@@ -1332,17 +1335,6 @@ impl Unify for UnifType {
                     inferred: ty,
                 })
             }
-            (UnifType::Contract(t1, env1), UnifType::Contract(t2, env2))
-                if eq::contract_eq(state.table.max_uvars_count(), &t1, &env1, &t2, &env2) =>
-            {
-                Ok(())
-            }
-            (uty1 @ UnifType::Contract(..), uty2) | (uty1, uty2 @ UnifType::Contract(..)) => {
-                Err(UnifError::TypeMismatch {
-                    expected: uty1,
-                    inferred: uty2,
-                })
-            }
         }
     }
 }
diff --git a/lsp/nls/src/cache.rs b/lsp/nls/src/cache.rs
index 5b3c788f..e774b4b8 100644
--- a/lsp/nls/src/cache.rs
+++ b/lsp/nls/src/cache.rs
@@ -70,6 +70,7 @@ impl CacheExt for Cache {
                 initial_ctxt.clone(),
                 self,
                 &mut collector,
+                typecheck::TypecheckMode::Walk,
             )
             .map_err(|err| vec![Error::TypecheckError(err)])?;
 
diff --git a/lsp/nls/src/field_walker.rs b/lsp/nls/src/field_walker.rs
index 0b0eecf6..90fc92b5 100644
--- a/lsp/nls/src/field_walker.rs
+++ b/lsp/nls/src/field_walker.rs
@@ -482,7 +482,7 @@ impl<'a> FieldResolver<'a> {
             TypeF::Record(rows) => vec![Container::RecordType(rows.clone())],
             TypeF::Dict { type_fields, .. } => vec![Container::Dict(type_fields.as_ref().clone())],
             TypeF::Array(elt_ty) => vec![Container::Array(elt_ty.as_ref().clone())],
-            TypeF::Flat(rt) => self.resolve_container(rt),
+            TypeF::Contract(rt) => self.resolve_container(rt),
             _ => Default::default(),
         }
     }
diff --git a/rfcs/006-package-management.md b/rfcs/006-package-management.md
new file mode 100644
index 00000000..94755432
--- /dev/null
+++ b/rfcs/006-package-management.md
@@ -0,0 +1,584 @@
+---
+feature: package management
+start-date: 2024-06-28
+author: Joe Neeman
+---
+
+# Package management
+
+People want to reuse code, but Nickel doesn't currently have a good way to do
+it. We should have a way to fetch packages and make them easily available to
+Nickel code. The mechanism needs to be predictable (it should fetch the code
+that the user expects to fetch) and reliable (if it works on my machine it
+should work on your machine).
+
+Explicit non-goals are:
+
+- Management of system (or other non-Nickel) dependencies. You can use Nix for
+  that.
+- Any sort of processing or compilation. Nickel is an interpreted language, so
+  package management is only in charge of distributing unmodified source files.
+- Integration with other language ecosystems; this is only for Nickel code.
+  Anyone integrating Nickel with other languages should use a polyglot build
+  system like Bazel. (However, providing integration points for other tools *is*
+  in scope. More detail on that below.)
+
+## The manifest file
+
+We will require a manifest file in order to import packages. Manifest files
+must be named `electroplate.ncl`, and they are found by searching up from the
+file being evaluated. That is, when the user invokes `nickel export path/to/
+foo.ncl`, we look for a manifest at `path/to/electroplate.ncl` and then at
+`path/electroplate.ncl`, and so on.
+
+The manifest file format is defined by the contract `std.package.Manifest`,
+which is defined as
+
+```nickel
+{
+  name | String,
+  version | Semver,
+  nickel-version
+    | Semver,
+    | doc "The minimum version of nickel supported by this package",
+
+
+  dependencies
+    | { _:
+      [|
+        'Path String,
+        'Git { url | String, branch | optional | String, rev | optional | String },
+        'Index { name | String, version | SemverConstraint },
+      |]
+      }
+    | default
+    = {},
+}
+```
+
+So an example manifest might look like
+
+```nickel
+{
+  name = "demo",
+  version = "0.1.0",
+  nickel-version = "1.0",
+  dependencies = {
+    foo = 'Index { package = "github/tweag/foo", version = "1.2.0" },
+    bar = 'Path "../my-bar",
+  }
+} | std.package.Manifest
+```
+
+### Alternative: inline dependencies
+
+Nix and Dhall allow for importing dependencies dynamically, using things like
+`fetchGit`. There was some discussion
+[here](https://github.com/tweag/nickel/issues/329#issuecomment-967372858)
+on the advantages and disadvantages of inline imports.
+
+### Alternative: toml manifest
+
+Maybe the manifest should be in some plain-data format like toml. This would
+be easier to modify programmatically, and it would prevent people from putting
+lots of complicated code in their manifest files.
+The disadvantage of a plain-data format is that you don't get a nice contract
+for it and you can't use ADTs for the dependencies.
+
+We discussed this point in office hours, and the general sentiment was that
+it's ok to allow the manifest to be interpreted. If someone wants to use
+that power to create a ridiculously complicated manifest, that's their problem.
+
+### Alternative: shorthand for registry imports
+
+Cargo allows a shorthand like
+
+```toml
+    "github/tweag/foo" = "1.2.0"
+```
+
+instead of
+
+```nickel
+    foo = 'Index { package = "github/tweag/foo", version = "1.2.0" }
+```
+
+Since we expect registry imports to be the common case, maybe it's worth having
+a shorthand?
+
+### Alternative: manifest file name
+
+Bikeshed the name "electroplate.ncl".
+
+## Import statements
+
+The manifest file assigns a name to each dependency; to import the dependency
+named `foo` you simply write `import foo`. That is, an `import` statement either
+takes a string in quotes -- in which case it imports a path -- or an identifier
+without quote -- in which case it imports a package.
+
+The `import foo` expression evaluates to the contents of `main.ncl` in `foo`'s
+root directory.
+
+### Alternative: specify the entrypoint in the manifest
+
+Since the package manifest is a nickel file, it could contain an arbitrary nickel
+expression as its entrypoint. That is, the `import foo` expression could evaluate
+to `(import "<path-to-foo>/electroplate.ncl").entrypoint`, and we could provide
+a default `entrypoint | default = import "main.ncl"` manifest entry. It might
+require some care to avoid looking for the "main.ncl" file if it doesn't exist.
+
+### Alternative: other entry points
+
+We've hardcoded `main.ncl` as the entry point of every package, but what if
+they want to expose multiple entry points? For example, node allows a package's
+manifest to specify the entry point(s). This is probably not very important to
+support, as you can just put
+
+```nickel
+{
+  other = import "./other.ncl",
+  blah = import "./blah.ncl",
+}
+```
+
+in your package's `main.ncl`, to provide "other" and "blah" as other entry points.
+
+### Alternative: entry points are top-level files
+
+Instead of hardcoding `main.ncl`, we could say that every file in the package's
+top-level directory is publicly accessible. Package authors could keep implementation
+details private by putting code in subdirectories. The import syntax would
+need to change somehow to specify the entry point.
+
+### Alternative: namespace the import tool
+
+Our initial intention for packaging was to allow for the usage of multiple
+different package management tools. This RFC only proposes one such tool, but
+maybe the import syntax could be designed with other tools in mind. For example,
+it could be `import foo from electroplate` with the idea that future nickel
+versions might add, say, `import foo from nix-flake`.
+
+One problem with this approach is that even if you switch package managers, you
+still want to import the same packages. So probably it doesn't make sense to
+include the name of the package manager in the nickel source.
+
+## CLI interface
+
+We will build package management straight into the nickel CLI. There will
+be a `nickel package` subcommand. This command will start by searching for an
+`electroplate.ncl` file. If one is found, we will evaluate it. We will then
+search for a lock-file. If one is found, it will be used to guide dependency
+resolution; if not, we will do dependency resolution from scratch and write out
+the generated lock-file.
+
+Once dependencies are resolved, they will be downloaded if necessary
+(git dependencies will need to be downloaded during resolution), and then
+cached.
+
+Other nickel commands like
+`nickel eval` and `nickel export` will read the lockfile before the actual
+evaluation.
+
+### Alternative: do the package management updates automatically
+
+We could do the main package management steps automatically when running
+commands like `nickel eval` and `nickel export`. This would ensure that
+the lock-file is never stale: if you update the manifest and then run
+`nickel eval`, it will take manifest changes into account. This automatic
+package management step is similar to how `cargo` works, whereas `poetry`
+and `npm` require an explicit package-management command.
+
+There will be command line flags to fine-tune this behavior. For example, there
+could be a `--locked` flag that triggers a failure if the lock-file is not
+present and up-to-date, or an `--offline` flag that triggers a failure if the
+dependencies aren't already available. There could also be a flag (`--no-electroplate`?)
+to disable package-management altogether.
+
+The main concern with this approach is performance: we need to check on
+each invocation whether the manifest is up-to-date. After initial implementation,
+we can measure the performance and decide whether we want to do things
+automatically.
+
+### Alternative: a separate CLI tool
+
+We could add a new CLI tool (called `plate`) that wraps the nickel CLI and
+adds package management. It would offer a superset of the nickel CLI's commands
+and arguments. For example, `plate eval foo.ncl` is the same as `nickel eval
+foo.ncl`, except that it reads the manifest file, prepares the dependencies, and
+makes them available to the nickel interpreter before evaluating. This would
+allow package-management to be opt-in.
+
+### Alternative: two-stage interface
+
+Rather than wrapping the original `nickel` CLI, the `plate` command could
+*prepare* the packages for `nickel`, which would be in charge of loading
+them. The workflow would then be `plate install` followed by `nickel eval foo.ncl`.
+This would be more like how `npm` or `poetry` work (whereas the wrapping
+interface is more similar to `cargo`).
+
+## Kinds of dependencies
+
+Where can dependencies come from? Dhall allows imports from arbitrary urls. Nix
+supports fetching from a variety of VCSs, paths, and archive formats.
+
+We'll support dependencies from
+
+- a central registry, that can identify packages by name and version number.
+  This should be the most common method of importing packages, like `crates.io`
+  in rust.
+- git repositories (either from HEAD, or from branches, tags, and revisions
+  specified by hashes). This allows for easy use of unpublished packages,
+  including in-development versions.
+- paths (relative or absolute). This allows for easy use of different packages
+  within the same repository, or for temporary patching of published packages.
+
+We require packages to have their own manifest file (at the package root), even
+if they don't import dependencies.
+
+## Lock files
+
+In order to ensure reproducibility across time and across machines, we build
+a lock-file (if there isn't yet one) when running `nickel eval` or `nickel
+export`. The lock-file specifies the exact versions of all (transitive)
+dependencies, allowing those identical versions to be used every time.
+
+- For a git dependency, the manifest might not specify the exact revision (it
+  might specify a branch or tag, or just default to HEAD). The lock-file will
+  record the exact revision.
+- For a repository dependency, the version specifier might allow for a range of
+  versions. The lock-file will record the exact version used.
+- For a path dependency, the lock-file will record that there was a path
+  dependency, but it won't record anything about it and it will ignore recursive
+  dependencies. This is because path dependencies can change at any time, so
+  they can't be meaningfully locked.
+
+## Restrictions on path dependencies
+
+Path dependencies can be problematic for reproducibility, because they require
+something to be present at a given path. In order to mitigate this:
+
+- Packages imported from the index are not allowed to have path dependencies.
+- Packages imported from git can have path dependencies, but only if they point
+  within the same git repo. The lock-file treats these path dependencies as though
+  they were git dependencies.
+
+Therefore your dependency tree can have a few path-dependency subtrees, but only
+at the root.
+
+## Stale lock files
+
+What happens if there's a lock-file, but someone modifies the manifest? The
+lock-file might need to be regenerated: certainly it might need some new
+entries, but also there might be new version conflicts that require a different
+resolution. In this case, we treat the lock-file as a suggestion instead of a
+hard constraint: during resolving, when choosing the next package version to
+try, we try to pick the locked version first. But if we run into a resolution
+conflict, we allow a different version to be chosen (and notify the user
+that a package was changed).
+
+This behavior is similar to what cargo does. It has the advantage that if the
+new manifest is compatible with the old lock-file, nothing will be changed.
+
+### Alternative: interactive prompt
+
+Instead of merely notifying the user that the lock-file changed, we could
+require them to approve the changes.
+
+### Alternative: explicit regeneration
+
+Instead of automatically updating the lock-file when the manifest changes,
+we could update it only on explicit commands: `plate eval` would use an
+old lock-file if it exists, while `plate lock` would read the manifest
+and update the lock-file. This alternative is potentially more efficient
+(as `plate eval` wouldn't need to re-read the manifest, and the manifests
+of path-dependencies, on every invocation), but makes it easy to accidentally
+use out-of-date packages.
+
+## Version compatibility and resolution
+
+How do we handle a package that gets imported multiple times in the dependency
+tree?
+
+For path and git dependencies, there isn't much choice. Dependencies from the
+registry are the most interesting.  Some languages (e.g. python) insist that
+each package resolves to a single version across the whole dependency tree.
+Other languages allow multiple versions, keeping track of which package in the
+dependency tree needs to import which version of a package.
+
+I think we want to allow multiple versions of a package; the alternative can be
+fragile and annoying. But then we need to figure out how many different versions
+to allow. There's a trade-off: if we allow pulling in a different version
+every time a package gets imported, solving the dependency graph is easy.
+But it increases the chance of getting incompatibilities at runtime: we might
+accidentally get a value from `util@1.1` and try to pass it to an incompatible
+function defined in `util@1.2`. Pulling in too many different versions also
+increases the total number of packages in the dependency graph.
+
+The current prototype uses a strategy similar to cargo: it divides package
+versions into semver-delimited "bins" and allows resolution to choose at most
+one version from each bin. That is, we can have a `util@2.2` and a `util@1.2` in
+the same dependency tree, but not a `util@1.2` and a `util@1.1`.
+
+### Alternative: global snapshots à la Stackage
+
+Maybe we can just avoid version resolution altogether? For example, Stackage
+provides an ecosystem-wide snapshot of packages that are mutually compatible.
+Then users just depend on a single version of Stackage, and all other versions
+are determined from there (with some escape hatches if they need a specific
+version of a specific package). nixpkgs works similarly; a single revision
+of nixpkgs fixes the versions of all the packages in nixpkgs.
+
+We might have some trouble automatically coming up with mutually compatible
+snapshots, though. Haskell gets to use compile-time checks to test compatibility,
+and nixpkgs just does a lot of building and testing to check whether everything
+works. Nickel being dynamic and lazy might make this hard.
+
+It seems like global snapshots are something that can be added after the fact
+(like stackage did), so we can revisit this later.
+
+### Alternative: minimal version selection
+
+Go uses a system called "[minimal version selection]" in which all version
+updates are required to be backwards-compatible: if you want to break some
+API, you have to add the new API at a different path and retain the old API.
+Then version resolution is trivial: just take the oldest version that is
+compatible with all the requirements. Advantages:
+
+- version resolution is trivial
+- version specification is trivial (there are no version ranges, just lower bounds)
+- version resolution is stable over time, even without a lock file; resolving
+  to the oldest compatible version means that we don't change resolution just
+  because a new version became available
+
+I don't have much experience using this method, but it seems like one
+disadvantage is that it puts an extra burden on package maintainers to keep
+backwards compatibility even across "major" version bumps.
+
+[bzlmod] also uses some version of minimal version selection, but they
+do apparently allow for backwards-compatibility breakage. They have
+an extra piece of metadata called "compatibility level" (not encoded in
+the version number). They don't allow a dependency graph to contain different
+compatibility levels of the same module.
+
+[minimal version selection]: https://research.swtch.com/vgo-mvs
+[bzlmod]: https://docs.bazel.build/versions/5.0.0/bzlmod.html
+
+### Some interpolation between MVS and semver
+
+There are some middle grounds between "minimal version selection" and
+cargo-style resolution. We could follow semver and allow multiple incompatible
+versions of packages, while also doing one or both of the following
+
+- preferring to resolve minimal versions instead of maximal versions. This promotes
+  stability in version resolution, at the cost of requiring intervention to bring
+  in bugfixes in dependencies.
+- only allowing `^` version specifications (along with `=` overrides at the top level).
+  This amounts to being opinionated that "the ecosystem is using semver, and your
+  version requirements should comply with semver." It's basically a semver analogue
+  of go's policy of only allowing lower bounds (plus pinning at the top level).
+
+### Question: how to handle pre-1.0 minor versions?
+
+Officially, semver says that pre-1.0 versions are mutually incompatible. If we
+follow this, pre-1.0 versions would never get binned together. `cargo` modifies
+the semver rules, allowing `0.x.y` versions to be binned together if they share
+the same `x`. Should we do the same?
+
+## Yanking packages
+
+What if someone messes up and publishes a package that's incompatible with
+an earlier version? In this case, we allow packages in the registry to be
+"yanked," meaning that they are left there but marked as broken. The resolver
+will ignore yanked packages unless they are already in the lock-file.
+This means that if you're happily using a package version that got yanked
+(maybe you're not using the broken part of the package) then you won't
+get broken by the yank.
+
+Package yanking will be done with the same process as package publishing
+(i.e., probably PRs to the index). See the next section.
+
+### Alternative: allow yanked packages if resolution would otherwise fail
+
+A slightly more permissive alternative would be to ignore yanked packages that
+aren't in the lock-file, but if resolution fails then go back and try allowing
+them. This would allow resolution to succeed, for example, if your manifest
+asks for the latest version of a package *and* that package was yanked *and*
+you don't have a lock-file. But this seems like maybe adding too many corner-cases.
+
+## The registry
+
+How should we manage the global registry? There's a potential for incurring
+substantial maintenance costs here, so we should be careful.
+
+We will provide a git repo, hard-coded to live at `github.com/nickel-lang/nickel-mine`,
+to serve as the registry.
+This repo will contain the "index", but not the actual package contents. It
+will contain one file per package, each of which contains a line per version.
+Each entry specifies the location of the package (currently required to be on
+github) and its git tree hash. This ensures that packages are immutable, but it
+doesn't stop them from disappearing: we don't keep a copy of the actual package
+contents.
+
+The registry index will also contain package metadata: the dependencies (so
+that we can resolve recursive dependencies without fetching the packages),
+and whatever metadata we want to be searchable.
+
+The registry entries are named like "github/\<org\>/\<package\>" (where in the
+future we might support places other than github). This allows us to skip
+registration and authentication: if someone has the github permissions to create
+`jneem/foo` on github, they also have permissions to create and update the
+`github/jneem/foo` nickel package.
+
+Packages will be updated by pull requests to the index. There can be some tooling
+in the nickel CLI to automate the creation of these pull requests. If the volume
+of updates becomes high enough, we can automate the merging.
+
+### Question: should we store a content hash too?
+
+We're storing a git tree hash in the index, but if we ever want to store package
+contents in the future, maybe we should also store a hash of the git tree
+contents? This would allow verification of package tarballs, without needing the
+whole git repo.
+
+## Alternate registries
+
+It's very convenient to have a default global registry, but you might also want
+to get the benefits of a registry without making your code public. Therefore
+we should support alternatives to the global registry. There are at least two
+distinct use-cases:
+
+1. providing an additional registry with private code, to be used alongside
+   the global registry
+2. replacing some registry with an alternative, for example in order to
+   host or cache it locally
+
+The difference between these two settings is that the private code registries
+are configured per-package: when you import the `myorg/foo` package you should
+know that it's coming from the registry hosted by `myorg` and not from
+the global registry. (It's important not to transparently overlay private
+registries on global registries, because this can lead to
+[dependency confusion attacks](https://medium.com/@alex.birsan/dependency-confusion-4a5d60fec610)).
+
+On the other hand, the registry replacements are configured globally, possibly
+on a system-wide level. The main use is to set up, say, an organization-wide mirror
+of the registry so as not to depend on external infrastructure.
+For this global setting, we add a `source-replacement` field to some system-wide
+or project-local nickel configuration file. It takes the form
+
+```nickel
+{
+  source-replacement | {
+    registry | { _ : String },
+    git | { _ : String },
+  },
+}
+```
+
+The idea is that you say
+
+```nickel
+source-replacement.registry."https://github.com/nickel-lang/nickel-mine.git"
+  = "/path/to/a/local/git/repo"
+```
+
+or
+
+```nickel
+source-replacement.registry."https://github.com/nickel-lang/nickel-mine.git"
+  = "https://my-site/nickel-mine"
+```
+
+You can also replace git repository locations, because why not.
+
+For per-package alternate registries (use-case 1 above), we just add a
+`registry` field to the package spec: the contract on `dependencies` becomes
+
+```nickel
+{ _:
+  [|
+    'Path String,
+    'Git { url | String, branch | optional | String, rev | optional | String }
+    'Index { name | String, version | SemverConstraint, registry | optional | String },
+    #                                                  NEW! ^^^
+  |]
+}
+```
+
+This is a bit different from what cargo does (it associates registry names to
+registry urls in global config, then you use only the *name* in the per-package
+part). But since our manifest format is nickel, you can just do that anyway:
+
+```nickel
+let my-repo = "https://github.com/jneem/my-mine" in
+{
+  dependencies = { bar = 'Index { name = "github/foo/bar", version = "0.1.0", registry = my-repo } }
+}
+```
+
+## Integration point: package maps
+
+Other tools (like build systems) may need to (1) consume the dependency resolution
+that we produce, or (2) plug in their own dependencies to the nickel interpreter.
+For (1), they can consume our lock-file, which will be in JSON. This means its
+format needs to be stable.
+
+For (2), we divide the package management implementation into two parts: the
+`nickel_lang_package` crate
+has all the logic for consuming the manifest, fetching packages, and so on.
+The other part is to teach the nickel interpreter about "package maps," which is
+just a map associating a filesystem path to each pair
+`(package filesystem path, package-local name)`. When the nickel interpreter
+is running a file that came from the package at path `/home/jneem/foo`, and that
+file contains `import bar`, the nickel interpreter looks up `(/home/jneem/foo, bar)`
+in the package map to figure out where to import from.
+
+When running `nickel eval` or `nickel export`, by default the nickel CLI will
+first use the `nickel_lang_package` crate to resolve and fetch dependencies.
+Then it provides the interpreter with the correct package map to find them.
+Other CLI commands can split up these steps (e.g., only resolving and printing
+dependencies; or invoking the interpreter with a custom package map that uses,
+say, vendored dependencies).
+
+## CLI support
+
+We'll need some CLI commands for handling common package-management tasks. The
+current prototype has
+
+- a `plate package generate-lockfile` command that updates the lock-file
+- a `plate package debug-resolution` command that prints the full recursive
+  dependency tree
+
+We probably also want
+
+- a command for adding a new dependency to the manifest (checking if it exists,
+  and picking the most recent version)
+- a command for listing (in machine-readable format) the dependency tree and all
+  its relevant metadata (for use in build systems that expect different "fetch"
+  and "build" phases)
+- a command that checks for new dependency versions and updates the manifest
+- a command for automating the pull request necessary for updating your package
+
+Anything else?
+
+## Where do the packages live?
+
+Index and git dependencies need to be downloaded before they are used. We will
+use a single global cache directory for all dependencies. It will use the
+[`directories`](https://docs.rs/directories/latest/directories/struct.ProjectDirs.html#method.cache_dir)
+crate to deduce a platform-appropriate location (`~/.cache/nickel-lang/` on
+linux, unless `$XDG_CACHE_HOME` is set). Within this directory, git checkouts
+will be stored in directories whose name includes the commit hash. So for
+example, the `foo` package could be stored in the `abcdef9876543210-foo`
+directory. If the same checkout of `foo` is used multiple times in different
+nickel projects, those projects will use the same checkout.
+
+The git checkouts will be created atomically (by first creating them under a temporary
+name and then renaming them) and marked read-only, so that multiple nickel processes
+can add cached packages without getting in one another's way.
+
+### Alternative: per-project cache
+
+We could use a per-project cache instead of a system-wide cache. This would have
+better isolation (e.g. if someone messes with the cache, it doesn't cause problems
+for *all* your nickel projects), but it also uses more bandwidth and disk space.
diff --git a/utils/src/bench.rs b/utils/src/bench.rs
index da40fd9a..71fec8a6 100644
--- a/utils/src/bench.rs
+++ b/utils/src/bench.rs
@@ -7,6 +7,7 @@ use nickel_lang_core::{
     },
     term::RichTerm,
     transform::import_resolution,
+    typecheck::TypecheckMode,
 };
 
 use std::path::PathBuf;
@@ -120,7 +121,9 @@ pub fn bench_terms<'r>(rts: Vec<Bench<'r>>) -> Box<dyn Fn(&mut Criterion) + 'r>
                     },
                     |(mut c_local, id, t)| {
                         if bench.eval_mode == EvalMode::TypeCheck {
-                            c_local.typecheck(id, &type_ctxt).unwrap();
+                            c_local
+                                .typecheck(id, &type_ctxt, TypecheckMode::Walk)
+                                .unwrap();
                         } else {
                             c_local.prepare(id, &type_ctxt).unwrap();
 
@@ -187,6 +190,7 @@ macro_rules! ncl_bench_group {
                 cache::{Envs, Cache, ErrorTolerance, ImportResolver, InputFormat},
                 eval::{VirtualMachine, cache::{CacheImpl, Cache as EvalCache}},
                 transform::import_resolution::strict::resolve_imports,
+                typecheck::TypecheckMode,
                 error::report::{report, ColorOpt, ErrorFormat},
             };
 
@@ -214,7 +218,7 @@ macro_rules! ncl_bench_group {
                         },
                         |(mut c_local, id, t)| {
                             if bench.eval_mode == $crate::bench::EvalMode::TypeCheck {
-                                c_local.typecheck(id, &type_ctxt).unwrap();
+                                c_local.typecheck(id, &type_ctxt, TypecheckMode::Walk).unwrap();
                             } else {
                                 c_local.prepare(id, &type_ctxt).unwrap();
 


Test patch:
diff --git a/cli/src/doctest.rs b/cli/src/doctest.rs
index 0bde75a7..7d86cb4f 100644
--- a/cli/src/doctest.rs
+++ b/cli/src/doctest.rs
@@ -18,6 +18,7 @@ use nickel_lang_core::{
         TypeAnnotation,
     },
     typ::{Type, TypeF},
+    typecheck::TypecheckMode,
 };
 use once_cell::sync::Lazy;
 use regex::Regex;
@@ -282,7 +283,7 @@ impl TestCommand {
         program: &mut Program<CacheImpl>,
     ) -> Result<(RichTerm, TestRegistry), CoreError> {
         let mut registry = TestRegistry::default();
-        program.typecheck()?;
+        program.typecheck(TypecheckMode::Walk)?;
         program
             .custom_transform(|cache, rt| doctest_transform(cache, &mut registry, rt))
             .map_err(|e| e.unwrap_error("transforming doctest"))?;
@@ -428,7 +429,7 @@ fn doctest_transform(
                                 ["contract", "Equal"],
                             );
                             let eq = mk_app!(eq, expected_term);
-                            let eq_ty = Type::from(TypeF::Flat(eq));
+                            let eq_ty = Type::from(TypeF::Contract(eq));
                             test_term = Term::Annotated(
                                 TypeAnnotation {
                                     typ: None,
diff --git a/cli/tests/snapshot/inputs/errors/typecheck_strict_mode.ncl b/cli/tests/snapshot/inputs/errors/typecheck_strict_mode.ncl
new file mode 100644
index 00000000..c00be6b2
--- /dev/null
+++ b/cli/tests/snapshot/inputs/errors/typecheck_strict_mode.ncl
@@ -0,0 +1,3 @@
+# capture = 'stderr'
+# command = ['typecheck', '--strict-typechecking']
+1 + "foo"
diff --git a/cli/tests/snapshot/inputs/errors/typedcheck_strict_mode_is_strict.ncl b/cli/tests/snapshot/inputs/errors/typedcheck_strict_mode_is_strict.ncl
new file mode 100644
index 00000000..ff96f27a
--- /dev/null
+++ b/cli/tests/snapshot/inputs/errors/typedcheck_strict_mode_is_strict.ncl
@@ -0,0 +1,3 @@
+# capture = 'stderr'
+# command = ['typecheck', '--strict-typechecking']
+let x = (1 + 1) in (x + 1 : Number)
diff --git a/cli/tests/snapshot/snapshots/snapshot__typecheck_stderr_typecheck_strict_mode.ncl.snap b/cli/tests/snapshot/snapshots/snapshot__typecheck_stderr_typecheck_strict_mode.ncl.snap
new file mode 100644
index 00000000..5e2354de
--- /dev/null
+++ b/cli/tests/snapshot/snapshots/snapshot__typecheck_stderr_typecheck_strict_mode.ncl.snap
@@ -0,0 +1,13 @@
+---
+source: cli/tests/snapshot/main.rs
+expression: err
+---
+error: incompatible types
+  ┌─ [INPUTS_PATH]/errors/typecheck_strict_mode.ncl:3:5
+  │
+3 │ 1 + "foo"
+  │     ^^^^^ this expression
+  │
+  = Expected an expression of type `Number`
+  = Found an expression of type `String`
+  = These types are not compatible
diff --git a/cli/tests/snapshot/snapshots/snapshot__typecheck_stderr_typedcheck_strict_mode_is_strict.ncl.snap b/cli/tests/snapshot/snapshots/snapshot__typecheck_stderr_typedcheck_strict_mode_is_strict.ncl.snap
new file mode 100644
index 00000000..9629b356
--- /dev/null
+++ b/cli/tests/snapshot/snapshots/snapshot__typecheck_stderr_typedcheck_strict_mode_is_strict.ncl.snap
@@ -0,0 +1,13 @@
+---
+source: cli/tests/snapshot/main.rs
+expression: err
+---
+error: incompatible types
+  ┌─ [INPUTS_PATH]/errors/typedcheck_strict_mode_is_strict.ncl:3:21
+  │
+3 │ let x = (1 + 1) in (x + 1 : Number)
+  │                     ^ this expression
+  │
+  = Expected an expression of type `Number`
+  = Found an expression of type `Dyn`
+  = These types are not compatible
diff --git a/core/tests/integration/inputs/lib/import_typecheck_strict.ncl b/core/tests/integration/inputs/lib/import_typecheck_strict.ncl
new file mode 100644
index 00000000..53e748ae
--- /dev/null
+++ b/core/tests/integration/inputs/lib/import_typecheck_strict.ncl
@@ -0,0 +1,4 @@
+# test.type = 'skip'
+
+# This is an auxiliary file used by typechecking tests
+1 + "foo"
diff --git a/core/tests/integration/inputs/typecheck/shallow_type_inference_strict_mode.ncl b/core/tests/integration/inputs/typecheck/shallow_type_inference_strict_mode.ncl
new file mode 100644
index 00000000..949a8b86
--- /dev/null
+++ b/core/tests/integration/inputs/typecheck/shallow_type_inference_strict_mode.ncl
@@ -0,0 +1,3 @@
+# test.type = 'pass'
+# eval = 'typecheck_strict'
+let x = (1 + 1) in (x + 1 : Number)
diff --git a/core/tests/integration/inputs/typecheck/strict_mode.ncl b/core/tests/integration/inputs/typecheck/strict_mode.ncl
new file mode 100644
index 00000000..50bf0342
--- /dev/null
+++ b/core/tests/integration/inputs/typecheck/strict_mode.ncl
@@ -0,0 +1,10 @@
+# test.type = 'error'
+# eval = 'typecheck_strict'
+#
+# [test.metadata]
+# error = 'TypecheckError::TypeMismatch'
+#
+# [test.metadata.expectation]
+# expected = 'Number'
+# inferred = 'String'
+1 + "foo"
diff --git a/core/tests/integration/inputs/typecheck/strict_mode_import.ncl b/core/tests/integration/inputs/typecheck/strict_mode_import.ncl
new file mode 100644
index 00000000..9e53c0f9
--- /dev/null
+++ b/core/tests/integration/inputs/typecheck/strict_mode_import.ncl
@@ -0,0 +1,10 @@
+# test.type = 'error'
+# eval = 'typecheck_strict'
+#
+# [test.metadata]
+# error = 'TypecheckError::TypeMismatch'
+#
+# [test.metadata.expectation]
+# expected = 'Number'
+# inferred = 'String'
+import "../lib/import_typecheck_strict.ncl"
diff --git a/core/tests/integration/inputs/typecheck/type_in_term_position.ncl b/core/tests/integration/inputs/typecheck/type_in_term_position.ncl
index efe0a34f..bb9f5bec 100644
--- a/core/tests/integration/inputs/typecheck/type_in_term_position.ncl
+++ b/core/tests/integration/inputs/typecheck/type_in_term_position.ncl
@@ -2,5 +2,5 @@
 # eval = 'typecheck'
 # 
 # [test.metadata]
-# error = 'TypecheckError::FlatTypeInTermPosition'
+# error = 'TypecheckError::CtrTypeInTermPos'
 (let c = Number -> (4 + 1) in 3): _
diff --git a/core/tests/integration/main.rs b/core/tests/integration/main.rs
index 6aa5b8c4..fceb748a 100644
--- a/core/tests/integration/main.rs
+++ b/core/tests/integration/main.rs
@@ -5,6 +5,7 @@ use nickel_lang_core::{
         Error, EvalError, ExportError, ExportErrorData, ImportError, ParseError, TypecheckError,
     },
     term::Term,
+    typecheck::TypecheckMode,
 };
 use nickel_lang_utils::{
     annotated_test::{read_annotated_test_case, TestCase},
@@ -108,6 +109,8 @@ enum EvalStrategy {
     Standard,
     #[serde(rename = "typecheck")]
     TypeCheck,
+    #[serde(rename = "typecheck_strict")]
+    TypeCheckStrict,
 }
 
 impl EvalStrategy {
@@ -115,7 +118,10 @@ impl EvalStrategy {
         match self {
             EvalStrategy::Full => p.eval_full().map(Term::from),
             EvalStrategy::Standard => p.eval().map(Term::from),
-            EvalStrategy::TypeCheck => p.typecheck().map(|_| Term::Bool(true)),
+            EvalStrategy::TypeCheck => p.typecheck(TypecheckMode::Walk).map(|_| Term::Bool(true)),
+            EvalStrategy::TypeCheckStrict => p
+                .typecheck(TypecheckMode::Enforce)
+                .map(|_| Term::Bool(true)),
         }
         .expect("Expected evaluation to succeed but got an error")
     }
@@ -124,7 +130,8 @@ impl EvalStrategy {
         match self {
             EvalStrategy::Full => p.eval_full().map(|_| ()),
             EvalStrategy::Standard => p.eval().map(|_| ()),
-            EvalStrategy::TypeCheck => p.typecheck(),
+            EvalStrategy::TypeCheck => p.typecheck(TypecheckMode::Walk),
+            EvalStrategy::TypeCheckStrict => p.typecheck(TypecheckMode::Enforce),
         }
         .expect_err("Expected an error but program evaluated successfully")
     }
@@ -202,8 +209,8 @@ enum ErrorExpectation {
     TypecheckMissingDynTail,
     #[serde(rename = "TypecheckError::ArrowTypeMismatch")]
     TypecheckArrowTypeMismatch { cause: Box<ErrorExpectation> },
-    #[serde(rename = "TypecheckError::FlatTypeInTermPosition")]
-    TypecheckFlatTypeInTermPosition,
+    #[serde(rename = "TypecheckError::CtrTypeInTermPos")]
+    TypecheckCtrTypeInTermPos,
     #[serde(rename = "TypecheckError::VarLevelMismatch")]
     TypecheckVarLevelMismatch { type_var: String },
     #[serde(rename = "TypecheckError::OrPatternVarsMismatch")]
@@ -264,8 +271,8 @@ impl PartialEq<Error> for ErrorExpectation {
             )
             | (TypecheckExtraDynTail, Error::TypecheckError(TypecheckError::ExtraDynTail { .. }))
             | (
-                TypecheckFlatTypeInTermPosition,
-                Error::TypecheckError(TypecheckError::FlatTypeInTermPosition { .. }),
+                TypecheckCtrTypeInTermPos,
+                Error::TypecheckError(TypecheckError::CtrTypeInTermPos { .. }),
             )
             | (ImportParseError, Error::ImportError(ImportError::ParseErrors(..)))
             | (ImportIoError, Error::ImportError(ImportError::IOError(..)))
@@ -448,7 +455,7 @@ impl std::fmt::Display for ErrorExpectation {
             TypecheckArrowTypeMismatch { cause } => {
                 format!("TypecheckError::ArrowTypeMismatch({cause})")
             }
-            TypecheckFlatTypeInTermPosition => "TypecheckError::FlatTypeInTermPosition".to_owned(),
+            TypecheckCtrTypeInTermPos => "TypecheckError::CtrTypeInTermPos".to_owned(),
             TypecheckVarLevelMismatch { type_var } => {
                 format!("TypecheckError::VarLevelMismatch({type_var})")
             }
diff --git a/utils/src/test_program.rs b/utils/src/test_program.rs
index 60a9287d..8a076c84 100644
--- a/utils/src/test_program.rs
+++ b/utils/src/test_program.rs
@@ -6,6 +6,7 @@ use nickel_lang_core::{
     parser::{grammar, lexer, ErrorTolerantParser, ExtendedTerm},
     program::Program,
     term::{RichTerm, Term},
+    typecheck::TypecheckMode,
 };
 
 use std::io::Cursor;
@@ -45,7 +46,7 @@ pub fn parse_extended(s: &str) -> Result<ExtendedTerm, ParseError> {
 
 pub fn typecheck_fixture(f: &str) -> Result<(), Error> {
     let mut p: Program<CacheImpl> = program_from_test_fixture(f);
-    p.typecheck()
+    p.typecheck(TypecheckMode::Walk)
 }
 
 fn program_from_test_fixture(f: &str) -> Program<CacheImpl> {