Repository: tweag/nickel
Pull request #2078 (2024-10-23 17:27:43)

Add a type parameter to TypeF for contracts
The TypeF recursion scheme is parametrized by a number of (Rust) types: the type of Nickel types, the type of enum rows and the type of record rows. There is one more Rust type that can be stored in a TypeF: a contract. It's currently hardcoded to be a `RichTerm`, which is fine because we never want to use another Rust type to store something else

With the development of the experimental bytecode interpreter, we are changing the representation of terms. Because we want to keep mailine Nickel operational during the transition, we have to copy paste all the `typ` module somewhere else, replacing `RichTerm` with the type of the new AST.

There is an alternative: as `TypeF` is already parametrized by a bunch of things, why not also parametrize the type of what's stored inside `TypeF::Contract`? This adds a bit more complexity, and requires an additional closure when mapping on or recursing into a `Type`. But the price doesn't seem too high, and we can reuse the same implementation for both mainline Nickel and bytecode Nickel.

There is an unexpected benefit: in fact, we do store something else than a `RichTerm`! During typechecking, we need to store an additional environment alongside a contract in order to properly compute contract equality. This led to having an additional constructor `GenericUnifType::Contract`, that must be handled separately from concrete types. When converting from a `Type` to a `UnifType`, the node `TypeF::Flat` is converted to`GenericUnifType::Contract`, and all typechecking functions then assume the invariant that they will never encounter a `TypeF::Flat`. But the Rust type system can't guarantee it. There's also a bespoke runtime error for that (although we're pretty sure it can't happen), a bunch of `debug_assert`, etc.

We can thus kill two birds with one stone: by parametrizing `TypeF`, we can now instantiate it with `(RichTerm, Environment)` for unification types. No need for runtime invariants or ad-hoc treatment anymore.

Doing so, we also rename `TypeF::Flat` to `TypeF::Contract`, the former being a historical but bad name.

github-actions[bot]: <h2><a href="https://bencher.dev/perf/nickel/reports/418003bf-ed16-4c08-b1b2-3b8d75a5309f?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/2078-merge?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">2078/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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=3cfaf19e-c9c5-4341-95cd-703456d0fc9f&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>485,120.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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=95048806-9bf2-49e4-88f2-dbcd66cbf68a&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&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,672,000.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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=15373c31-496e-4f43-bbb4-466ef49fdd87&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&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,539,000.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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=87746452-c4df-48ea-b5e9-8d66f82ca556&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&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,994,000.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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=7f141ea0-9fbb-4305-bb63-78f163e546d6&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>61,529,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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=8c154d79-dc68-4d93-abb3-83183a62f6a2&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>45,141,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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=6d0222f6-0b85-4eaf-8c5c-e8957c522ef9&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&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,011,400.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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=be0d3f87-d089-4b81-af44-3bbc6e831697&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&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,316,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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=2946df33-45e4-4282-b749-040582021fe3&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>754,850.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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=5be25c57-d46f-4b48-b6f0-dee01b84220a&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&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,171,000.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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=7178a975-b548-4e78-8c84-4f3802668825&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&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,486,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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=6884f292-8796-44a8-a30c-d3cb2ed987f6&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&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,977,500.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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=2f5f7f6a-4e54-4542-aa09-da5671953fbb&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>823,230.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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=211bb66a-58f8-488b-97e4-7ea032870038&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&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,512,100.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=0d6aad48-6762-4872-9841-6309a5ace532&heads=d53838f8-8327-4057-a977-0856295d2dd1&testbeds=66263ed0-9556-4385-9f30-26466ee26211&benchmarks=3f1710c5-ce75-4dfb-aadb-1435fed8a093&measures=2b5b9371-696f-422d-b1a5-262ce8157b6b&start_time=1727113190000&end_time=1729705190000&report=418003bf-ed16-4c08-b1b2-3b8d75a5309f&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=nickel">view plot</a><br/>⚠️ NO THRESHOLD</td><td>810,840.00</td></tr></tbody></table></details><a href="https://bencher.dev/perf/nickel/reports/418003bf-ed16-4c08-b1b2-3b8d75a5309f?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/2078-merge/ubuntu-latest/rust_criterion"></div>

Patch:
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/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/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/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> {