From 5b4a0213dbd165f03b61bd4fc70c0a42ed50133c Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Thu, 21 Sep 2023 12:22:52 +0200
Subject: [PATCH 01/14] Duplicate contrat elision: first tentative

---
 core/src/eval/merge.rs     |  5 ++++-
 core/src/eval/operation.rs | 16 ++++++++++++----
 core/src/term/mod.rs       | 15 +++++++++++++++
 core/src/typecheck/eq.rs   | 10 ++++------
 4 files changed, 35 insertions(+), 11 deletions(-)

diff --git a/core/src/eval/merge.rs b/core/src/eval/merge.rs
index fdbe960e49..d48e0dd024 100644
--- a/core/src/eval/merge.rs
+++ b/core/src/eval/merge.rs
@@ -410,7 +410,10 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a LocIdent> + Clon
     };
 
     let mut pending_contracts = pending_contracts1.revert_closurize(cache, env_final, env1.clone());
-    pending_contracts.extend(pending_contracts2.revert_closurize(cache, env_final, env2.clone()));
+
+    for ctr2 in pending_contracts2.revert_closurize(cache, env_final, env2.clone()) {
+        RuntimeContract::push_elide(&mut pending_contracts, ctr2, &env1, &env2);
+    }
 
     Ok(Field {
         metadata: FieldMetadata {
diff --git a/core/src/eval/operation.rs b/core/src/eval/operation.rs
index 9c3857600a..1748662577 100644
--- a/core/src/eval/operation.rs
+++ b/core/src/eval/operation.rs
@@ -2113,6 +2113,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                             // due to a limitation of `match_sharedterm`: see the macro's
                             // documentation
                             let mut record_data = record_data;
+                            let term_original_env = env2.clone();
 
                             let mut contract_at_field = |id: LocIdent| {
                                 let pos = contract_term.pos;
@@ -2125,10 +2126,17 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                             };
 
                             for (id, field) in record_data.fields.iter_mut() {
-                                field.pending_contracts.push(RuntimeContract {
-                                    contract: contract_at_field(*id),
-                                    label: label.clone(),
-                                });
+                                let runtime_ctr = RuntimeContract {
+                                        contract: contract_at_field(*id),
+                                        label: label.clone(),
+                                    };
+
+                                crate::term::RuntimeContract::push_elide(
+                                    &mut field.pending_contracts,
+                                    runtime_ctr,
+                                    &term_original_env,
+                                    &contract_env,
+                                );
                             }
 
                             // IMPORTANT: here, we revert the record back to a `RecRecord`. The
diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs
index 0cf5d2c5de..75f62845fa 100644
--- a/core/src/term/mod.rs
+++ b/core/src/term/mod.rs
@@ -319,6 +319,21 @@ impl RuntimeContract {
     {
         contracts.fold(rt, |acc, ctr| ctr.apply(acc, pos))
     }
+
+    pub fn push_elide(
+        contracts: &mut Vec<RuntimeContract>,
+        ctr: Self,
+        env1: &crate::eval::Environment,
+        env2: &crate::eval::Environment,
+    ) {
+        for c in contracts.iter() {
+            if crate::typecheck::eq::contract_eq(0, &c.contract, env1, &ctr.contract, env2) {
+                return;
+            }
+        }
+
+        contracts.push(ctr);
+    }
 }
 
 impl Traverse<RichTerm> for RuntimeContract {
diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index 4d3d0479bb..3f902c8f75 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -52,7 +52,7 @@ use crate::{
 /// The maximal number of variable links we want to unfold before abandoning the check. It should
 /// stay low, but has been fixed arbitrarily: feel fee to increase reasonably if it turns out
 /// legitimate type equalities between simple contracts are unduly rejected in practice.
-pub const MAX_GAS: u8 = 8;
+pub const MAX_GAS: u8 = 20;
 
 /// Abstract over the term environment, which is represented differently in the typechecker and
 /// during evaluation.
@@ -105,19 +105,17 @@ impl std::iter::FromIterator<(Ident, (RichTerm, SimpleTermEnvironment))> for Sim
     }
 }
 
-/*
-impl<C: Cache> TermEnvironment for eval::Environment {
-    fn get_then<F, T>(&self, id: &Ident, f: F) -> T
+impl TermEnvironment for eval::Environment {
+    fn get_then<F, T>(&self, id: Ident, f: F) -> T
     where
         F: FnOnce(Option<(&RichTerm, &eval::Environment)>) -> T,
     {
-        match self.get(id).map(eval::lazy::Thunk::borrow) {
+        match self.get(&id).map(eval::cache::lazy::Thunk::borrow) {
             Some(closure_ref) => f(Some((&closure_ref.body, &closure_ref.env))),
             None => f(None),
         }
     }
 }
-*/
 
 pub trait FromEnv<C: Cache> {
     fn from_env(eval_env: eval::Environment, cache: &C) -> Self;

From b3bb861f2fdbe50a97ed2bcbe10e97e0f3356d32 Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Fri, 22 Sep 2023 11:36:09 +0200
Subject: [PATCH 02/14] Fix contract deduplication

The previous attempt wasn't fruitful, because we don't pass the initial
environment to the contract equality checker. This commit thread the
initial environment through the virtual machine and various functions to
make it available to the contract deduplicator
---
 core/src/eval/merge.rs     |   5 +-
 core/src/eval/mod.rs       |  52 ++++++-----
 core/src/eval/operation.rs |   5 +-
 core/src/program.rs        |  38 ++++----
 core/src/repl/mod.rs       |   8 +-
 core/src/term/mod.rs       |  15 ++-
 core/src/typecheck/eq.rs   | 182 ++++++++++++++++++++++++-------------
 core/src/typecheck/mod.rs  |   8 +-
 core/src/typecheck/unif.rs |   2 +-
 9 files changed, 194 insertions(+), 121 deletions(-)

diff --git a/core/src/eval/merge.rs b/core/src/eval/merge.rs
index d48e0dd024..cee32a9eaa 100644
--- a/core/src/eval/merge.rs
+++ b/core/src/eval/merge.rs
@@ -67,6 +67,7 @@ impl From<MergeMode> for MergeLabel {
 #[allow(clippy::too_many_arguments)] // TODO: Is it worth to pack the inputs in an ad-hoc struct?
 pub fn merge<C: Cache>(
     cache: &mut C,
+    initial_env: &Environment,
     t1: RichTerm,
     env1: Environment,
     t2: RichTerm,
@@ -307,6 +308,7 @@ pub fn merge<C: Cache>(
                     id,
                     merge_fields(
                         cache,
+                        initial_env,
                         merge_label,
                         field1,
                         env1.clone(),
@@ -357,6 +359,7 @@ pub fn merge<C: Cache>(
 #[allow(clippy::too_many_arguments)]
 fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a LocIdent> + Clone>(
     cache: &mut C,
+    initial_env: &Environment,
     merge_label: MergeLabel,
     field1: Field,
     env1: Environment,
@@ -412,7 +415,7 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a LocIdent> + Clon
     let mut pending_contracts = pending_contracts1.revert_closurize(cache, env_final, env1.clone());
 
     for ctr2 in pending_contracts2.revert_closurize(cache, env_final, env2.clone()) {
-        RuntimeContract::push_elide(&mut pending_contracts, ctr2, &env1, &env2);
+        RuntimeContract::push_elide(initial_env, &mut pending_contracts, &env_final, ctr2, &env_final);
     }
 
     Ok(Field {
diff --git a/core/src/eval/mod.rs b/core/src/eval/mod.rs
index 62ed6af29d..9dec90f432 100644
--- a/core/src/eval/mod.rs
+++ b/core/src/eval/mod.rs
@@ -122,6 +122,8 @@ pub struct VirtualMachine<R: ImportResolver, C: Cache> {
     import_resolver: R,
     // The evaluation cache.
     pub cache: C,
+    // The initial environment containing stdlib and builtin functions accessible from anywhere
+    initial_env: Environment,
     // The stream for writing trace output.
     trace: Box<dyn Write>,
 }
@@ -133,6 +135,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
             call_stack: Default::default(),
             stack: Stack::new(),
             cache: Cache::new(),
+            initial_env: Environment::new(),
             trace: Box::new(trace),
         }
     }
@@ -144,6 +147,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
             stack: Stack::new(),
             cache,
             trace: Box::new(trace),
+            initial_env: Environment::new(),
         }
     }
 
@@ -164,8 +168,8 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
 
     /// Evaluate a Nickel term. Wrapper around [VirtualMachine::eval_closure] that starts from an
     /// empty local environment and drops the final environment.
-    pub fn eval(&mut self, t0: RichTerm, initial_env: &Environment) -> Result<RichTerm, EvalError> {
-        self.eval_closure(Closure::atomic_closure(t0), initial_env)
+    pub fn eval(&mut self, t: RichTerm) -> Result<RichTerm, EvalError> {
+        self.eval_closure(Closure::atomic_closure(t))
             .map(|(term, _)| term)
     }
 
@@ -174,45 +178,50 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
     pub fn eval_full(
         &mut self,
         t0: RichTerm,
-        initial_env: &Environment,
     ) -> Result<RichTerm, EvalError> {
-        self.eval_deep_closure(t0, initial_env, false)
-            .map(|(term, env)| subst(&self.cache, term, initial_env, &env))
+        self.eval_full_closure(Closure::atomic_closure(t0)).map(|(term, _)| term)
+    }
+
+    pub fn eval_full_closure(
+        &mut self,
+        t0: Closure,
+    ) -> Result<(RichTerm, Environment), EvalError> {
+        self.eval_deep_closure(t0, false)
+            .map(|(term, env)| (subst(&self.cache, term, &self.initial_env, &env), env))
     }
 
     /// Like `eval_full`, but skips evaluating record fields marked `not_exported`.
     pub fn eval_full_for_export(
         &mut self,
         t0: RichTerm,
-        initial_env: &Environment,
     ) -> Result<RichTerm, EvalError> {
-        self.eval_deep_closure(t0, initial_env, true)
-            .map(|(term, env)| subst(&self.cache, term, initial_env, &env))
+        self.eval_deep_closure(Closure::atomic_closure(t0), true)
+            .map(|(term, env)| subst(&self.cache, term, &self.initial_env, &env))
     }
 
     /// Fully evaluates a Nickel term like `eval_full`, but does not substitute all variables.
     pub fn eval_deep(
         &mut self,
         t0: RichTerm,
-        initial_env: &Environment,
     ) -> Result<RichTerm, EvalError> {
-        self.eval_deep_closure(t0, initial_env, false)
+        self.eval_deep_closure(Closure::atomic_closure(t0), false)
             .map(|(term, _)| term)
     }
 
     fn eval_deep_closure(
         &mut self,
-        rt: RichTerm,
-        initial_env: &Environment,
+        mut closure: Closure,
         for_export: bool,
     ) -> Result<(RichTerm, Environment), EvalError> {
-        let wrapper = mk_term::op1(
+
+        closure.body = mk_term::op1(
             UnaryOp::Force {
                 ignore_not_exported: for_export,
             },
-            rt,
+            closure.body,
         );
-        self.eval_closure(Closure::atomic_closure(wrapper), initial_env)
+
+        self.eval_closure(closure)
     }
 
     /// Query the value and the metadata of a record field in an expression.
@@ -228,7 +237,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
         initial_env: &Environment,
     ) -> Result<Field, EvalError> {
         let mut prev_pos = t.pos;
-        let (rt, mut env) = self.eval_closure(Closure::atomic_closure(t), initial_env)?;
+        let (rt, mut env) = self.eval_closure(Closure::atomic_closure(t))?;
 
         let mut field: Field = rt.into();
 
@@ -272,8 +281,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                     Closure {
                                         body: value_with_ctr,
                                         env: env.clone(),
-                                    },
-                                    initial_env,
+                                    }
                                 )?;
                                 env = new_env;
 
@@ -329,7 +337,6 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
     pub fn eval_closure(
         &mut self,
         mut clos: Closure,
-        initial_env: &Environment,
     ) -> Result<(RichTerm, Environment), EvalError> {
         loop {
             let Closure {
@@ -383,7 +390,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                 Term::Var(x) => {
                     let mut idx = env
                         .get(&x.ident())
-                        .or_else(|| initial_env.get(&x.ident()))
+                        .or_else(|| self.initial_env.get(&x.ident()))
                         .cloned()
                         .ok_or(EvalError::UnboundIdentifier(*x, pos))?;
                     std::mem::drop(env); // idx may be a 1RC pointer
@@ -820,13 +827,14 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
 }
 
 impl<C: Cache> VirtualMachine<ImportCache, C> {
-    pub fn prepare_eval(&mut self, main_id: FileId) -> Result<(RichTerm, Environment), Error> {
+    pub fn prepare_eval(&mut self, main_id: FileId) -> Result<RichTerm, Error> {
         let Envs {
             eval_env,
             type_ctxt,
         }: Envs = self.import_resolver.prepare_stdlib(&mut self.cache)?;
         self.import_resolver.prepare(main_id, &type_ctxt)?;
-        Ok((self.import_resolver().get(main_id).unwrap(), eval_env))
+        self.initial_env = eval_env;
+        Ok(self.import_resolver().get(main_id).unwrap())
     }
 
     pub fn prepare_stdlib(&mut self) -> Result<Envs, Error> {
diff --git a/core/src/eval/operation.rs b/core/src/eval/operation.rs
index 1748662577..c4fab4ef4a 100644
--- a/core/src/eval/operation.rs
+++ b/core/src/eval/operation.rs
@@ -1881,6 +1881,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
             },
             BinaryOp::Merge(merge_label) => merge::merge(
                 &mut self.cache,
+                &self.initial_env,
                 RichTerm {
                     term: t1,
                     pos: pos1,
@@ -2132,9 +2133,10 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                     };
 
                                 crate::term::RuntimeContract::push_elide(
+                                    &self.initial_env,
                                     &mut field.pending_contracts,
-                                    runtime_ctr,
                                     &term_original_env,
+                                    runtime_ctr,
                                     &contract_env,
                                 );
                             }
@@ -2471,6 +2473,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                         Term::Lbl(lbl) => {
                             merge::merge(
                                 &mut self.cache,
+                                &self.initial_env,
                                 RichTerm {
                                     term: t2,
                                     pos: pos2,
diff --git a/core/src/program.rs b/core/src/program.rs
index 2c0383f570..4105ec3297 100644
--- a/core/src/program.rs
+++ b/core/src/program.rs
@@ -22,8 +22,7 @@
 //! Each such value is added to the initial environment before the evaluation of the program.
 use crate::{
     cache::*,
-    error::{report, ColorOpt, Error, EvalError, IOError, IntoDiagnostics, ParseError},
-    eval,
+    error::{report, ColorOpt, Error, IntoDiagnostics, ParseError, EvalError, IOError},
     eval::{cache::Cache as EvalCache, VirtualMachine},
     identifier::LocIdent,
     label::Label,
@@ -237,7 +236,7 @@ impl<EC: EvalCache> Program<EC> {
 
     /// Retrieve the parsed term and typecheck it, and generate a fresh initial environment. Return
     /// both.
-    fn prepare_eval(&mut self) -> Result<(RichTerm, eval::Environment), Error> {
+    fn prepare_eval(&mut self) -> Result<RichTerm, Error> {
         // If there are no overrides, we avoid the boilerplate of creating an empty record and
         // merging it with the current program
         if self.overrides.is_empty() {
@@ -258,7 +257,7 @@ impl<EC: EvalCache> Program<EC> {
                 .value(Term::ResolvedImport(value_file_id));
         }
 
-        let (t, initial_env) = self.vm.prepare_eval(self.main_id)?;
+        let t = self.vm.prepare_eval(self.main_id)?;
         let built_record = record.build();
         // For now, we can't do much better than using `Label::default`, but this is
         // hazardous. `Label::default` was originally written for tests, and although it
@@ -267,22 +266,21 @@ impl<EC: EvalCache> Program<EC> {
         // generate a dummy file id).
         // We'll have to adapt `Label` and `MergeLabel` to be generated programmatically,
         // without referring to any source position.
-        let wrapper = mk_term::op2(BinaryOp::Merge(Label::default().into()), t, built_record);
-        Ok((wrapper, initial_env))
+        Ok(mk_term::op2(BinaryOp::Merge(Label::default().into()), t, built_record))
     }
 
     /// Parse if necessary, typecheck and then evaluate the program.
     pub fn eval(&mut self) -> Result<RichTerm, Error> {
-        let (t, initial_env) = self.prepare_eval()?;
+        let t = self.prepare_eval()?;
         self.vm.reset();
-        self.vm.eval(t, &initial_env).map_err(|e| e.into())
+        self.vm.eval(t).map_err(|e| e.into())
     }
 
     /// Same as `eval`, but proceeds to a full evaluation.
     pub fn eval_full(&mut self) -> Result<RichTerm, Error> {
-        let (t, initial_env) = self.prepare_eval()?;
+        let t = self.prepare_eval()?;
         self.vm.reset();
-        self.vm.eval_full(t, &initial_env).map_err(|e| e.into())
+        self.vm.eval_full(t).map_err(|e| e.into())
     }
 
     /// Same as `eval`, but proceeds to a full evaluation. Optionally take a set of overrides that
@@ -299,18 +297,18 @@ impl<EC: EvalCache> Program<EC> {
     ///   an import referring to the corresponding isolated value. This stub is finally merged with
     ///   the current program before being evaluated for import.
     pub fn eval_full_for_export(&mut self) -> Result<RichTerm, Error> {
-        let (t, initial_env) = self.prepare_eval()?;
+        let t = self.prepare_eval()?;
         self.vm.reset();
         self.vm
-            .eval_full_for_export(t, &initial_env)
+            .eval_full_for_export(t)
             .map_err(|e| e.into())
     }
 
     /// Same as `eval_full`, but does not substitute all variables.
     pub fn eval_deep(&mut self) -> Result<RichTerm, Error> {
-        let (t, initial_env) = self.prepare_eval()?;
+        let t = self.prepare_eval()?;
         self.vm.reset();
-        self.vm.eval_deep(t, &initial_env).map_err(|e| e.into())
+        self.vm.eval_deep(t).map_err(|e| e.into())
     }
 
     /// Wrapper for [`query`].
@@ -424,7 +422,7 @@ impl<EC: EvalCache> Program<EC> {
         use crate::match_sharedterm;
         use crate::term::{record::RecordData, RuntimeContract};
 
-        let (t, initial_env) = self.prepare_eval()?;
+        let t = self.prepare_eval()?;
 
         // Eval pending contracts as well, in order to extract more information from potential
         // record contract fields.
@@ -432,13 +430,12 @@ impl<EC: EvalCache> Program<EC> {
             vm: &mut VirtualMachine<Cache, EC>,
             mut pending_contracts: Vec<RuntimeContract>,
             current_env: Environment,
-            initial_env: &Environment,
         ) -> Result<Vec<RuntimeContract>, Error> {
             vm.reset();
 
             for ctr in pending_contracts.iter_mut() {
                 let rt = ctr.contract.clone();
-                ctr.contract = do_eval(vm, rt, current_env.clone(), initial_env)?;
+                ctr.contract = do_eval(vm, rt, current_env.clone())?;
             }
 
             Ok(pending_contracts)
@@ -448,7 +445,6 @@ impl<EC: EvalCache> Program<EC> {
             vm: &mut VirtualMachine<Cache, EC>,
             t: RichTerm,
             current_env: Environment,
-            initial_env: &Environment,
         ) -> Result<RichTerm, Error> {
             vm.reset();
             let result = vm.eval_closure(
@@ -456,7 +452,6 @@ impl<EC: EvalCache> Program<EC> {
                     body: t.clone(),
                     env: current_env,
                 },
-                initial_env,
             );
 
             // We expect to hit `MissingFieldDef` errors. When a configuration
@@ -484,13 +479,12 @@ impl<EC: EvalCache> Program<EC> {
                                     Field {
                                         value: field
                                             .value
-                                            .map(|rt| do_eval(vm, rt, env.clone(), initial_env))
+                                            .map(|rt| do_eval(vm, rt, env.clone()))
                                             .transpose()?,
                                         pending_contracts: eval_contracts(
                                             vm,
                                             field.pending_contracts,
                                             env.clone(),
-                                            initial_env
                                         )?,
                                         ..field
                                     },
@@ -506,7 +500,7 @@ impl<EC: EvalCache> Program<EC> {
             }
         }
 
-        do_eval(&mut self.vm, t, Environment::new(), &initial_env)
+        do_eval(&mut self.vm, t, Environment::new())
     }
 
     /// Extract documentation from the program
diff --git a/core/src/repl/mod.rs b/core/src/repl/mod.rs
index 2ec5966101..2db08cdfa8 100644
--- a/core/src/repl/mod.rs
+++ b/core/src/repl/mod.rs
@@ -168,9 +168,9 @@ impl<EC: EvalCache> ReplImpl<EC> {
     fn eval_(&mut self, exp: &str, eval_full: bool) -> Result<EvalResult, Error> {
         self.vm.reset();
         let eval_function = if eval_full {
-            eval::VirtualMachine::eval_full
+            eval::VirtualMachine::eval_full_closure
         } else {
-            eval::VirtualMachine::eval
+            eval::VirtualMachine::eval_closure
         };
 
         let file_id = self.vm.import_resolver_mut().add_string(
@@ -189,7 +189,7 @@ impl<EC: EvalCache> ReplImpl<EC> {
         match term {
             ExtendedTerm::RichTerm(t) => {
                 let t = self.prepare(None, t)?;
-                Ok(eval_function(&mut self.vm, t, &self.env.eval_env)?.into())
+                Ok(eval_function(&mut self.vm, Closure { body: t, env: self.env.eval_env.clone() })?.0.into())
             }
             ExtendedTerm::ToplevelLet(id, t) => {
                 let t = self.prepare(Some(id), t)?;
@@ -225,7 +225,7 @@ impl<EC: EvalCache> Repl for ReplImpl<EC> {
 
         let (term, new_env) = self
             .vm
-            .eval_closure(Closure::atomic_closure(term), &self.env.eval_env)?;
+            .eval_closure(Closure { body: term, env: self.env.eval_env.clone()})?;
 
         if !matches!(term.as_ref(), Term::Record(..) | Term::RecRecord(..)) {
             return Err(Error::EvalError(EvalError::Other(
diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs
index 75f62845fa..a97fc213dc 100644
--- a/core/src/term/mod.rs
+++ b/core/src/term/mod.rs
@@ -25,6 +25,8 @@ use crate::{
     match_sharedterm,
     position::TermPos,
     typ::{Type, UnboundTypeVariableError},
+    eval::Environment,
+    typecheck::eq::{contract_eq, EvalEnvs},
 };
 
 use codespan::FileId;
@@ -321,13 +323,20 @@ impl RuntimeContract {
     }
 
     pub fn push_elide(
+        initial_env: &Environment,
         contracts: &mut Vec<RuntimeContract>,
+        env1: &Environment,
         ctr: Self,
-        env1: &crate::eval::Environment,
-        env2: &crate::eval::Environment,
+        env2: &Environment,
     ) {
+        eprintln!("push_elide: ({})", ctr.contract);
+        let envs1 = EvalEnvs { eval_env: env1, initial_env};
+
         for c in contracts.iter() {
-            if crate::typecheck::eq::contract_eq(0, &c.contract, env1, &ctr.contract, env2) {
+            eprintln!("- comparing against ({})", c.contract);
+            let envs = EvalEnvs { eval_env: env2, initial_env};
+            if contract_eq::<EvalEnvs>(0, &c.contract, envs1, &ctr.contract, envs) {
+                eprintln!("  -> found equal contract, eliding");
                 return;
             }
         }
diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index 3f902c8f75..03a2f6198b 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -49,6 +49,8 @@ use crate::{
     term::{self, record::Field, IndexMap, UnaryOp},
 };
 
+use std::fmt::Debug;
+
 /// The maximal number of variable links we want to unfold before abandoning the check. It should
 /// stay low, but has been fixed arbitrarily: feel fee to increase reasonably if it turns out
 /// legitimate type equalities between simple contracts are unduly rejected in practice.
@@ -63,9 +65,15 @@ pub const MAX_GAS: u8 = 20;
 /// `TermEnvironment::get_then` has to take a closure representing the continuation of the task to
 /// do with the result instead of merely returning it.
 pub trait TermEnvironment: Clone {
-    fn get_then<F, T>(&self, id: Ident, f: F) -> T
+    type Owned : Clone + PartialEq + Debug;
+    type Ref<'a> : Copy;
+
+    fn get_then<F, T>(env: Self::Ref<'_>, id: Ident, f: F) -> T
     where
-        F: FnOnce(Option<(&RichTerm, &Self)>) -> T;
+        F: FnOnce(Option<(&RichTerm, Self::Ref<'_>)>) -> T;
+
+    fn owned_to_ref(&self) -> Self::Ref<'_>;
+    fn ref_to_owned(env: Self::Ref<'_>) -> Self::Owned;
 }
 
 /// A simple term environment, as a mapping from identifiers to a tuple of a term and an
@@ -86,11 +94,28 @@ impl Default for SimpleTermEnvironment {
 }
 
 impl TermEnvironment for SimpleTermEnvironment {
-    fn get_then<F, T>(&self, id: Ident, f: F) -> T
+    type Owned = Self;
+    type Ref<'a> = &'a Self;
+
+    fn get_then<F, T>(env: &Self, id: Ident, f: F) -> T
     where
         F: FnOnce(Option<(&RichTerm, &SimpleTermEnvironment)>) -> T,
     {
-        f(self.0.get(&id).map(|(rt, env)| (rt, env)))
+        f(env.0.get(&id).map(|(rt, env)| (rt, env)))
+    }
+
+    fn owned_to_ref(&self) -> Self::Ref<'_> {
+        self
+    }
+
+    fn ref_to_owned(env: &Self) -> Self::Owned {
+        env.clone()
+    }
+}
+
+impl<'a> AsRef<SimpleTermEnvironment> for &'a SimpleTermEnvironment {
+    fn as_ref(&self) -> &SimpleTermEnvironment {
+        self
     }
 }
 
@@ -105,16 +130,47 @@ impl std::iter::FromIterator<(Ident, (RichTerm, SimpleTermEnvironment))> for Sim
     }
 }
 
-impl TermEnvironment for eval::Environment {
-    fn get_then<F, T>(&self, id: Ident, f: F) -> T
+#[derive(Clone, Copy)]
+pub struct EvalEnvs<'a> {
+    pub eval_env: &'a eval::Environment,
+    pub initial_env:  &'a eval::Environment,
+}
+
+#[derive(Clone, PartialEq, Debug)]
+pub struct EvalEnvsOwned {
+    pub eval_env: eval::Environment,
+    pub initial_env:  eval::Environment,
+}
+
+impl<'a> TermEnvironment for EvalEnvs<'a> {
+    type Ref<'b> = EvalEnvs<'b>;
+    type Owned = EvalEnvsOwned;
+
+    fn get_then<F, T>(env: EvalEnvs<'_>, id: Ident, f: F) -> T
     where
-        F: FnOnce(Option<(&RichTerm, &eval::Environment)>) -> T,
+        F: FnOnce(Option<(&RichTerm, EvalEnvs<'_>)>) -> T,
     {
-        match self.get(&id).map(eval::cache::lazy::Thunk::borrow) {
-            Some(closure_ref) => f(Some((&closure_ref.body, &closure_ref.env))),
+        debug_assert!(env.eval_env.get(&id).or(env.initial_env.get(&id)).is_some(), "unbound variable `{}`", id);
+
+        match env.eval_env.get(&id).or(env.initial_env.get(&id)).map(eval::cache::lazy::Thunk::borrow) {
+            Some(closure_ref) => f(Some((&closure_ref.body, EvalEnvs { eval_env: &closure_ref.env, initial_env: env.initial_env }))),
             None => f(None),
         }
     }
+
+    fn owned_to_ref(&self) -> Self::Ref<'_> {
+        EvalEnvs {
+            eval_env: self.eval_env,
+            initial_env: self.initial_env,
+        }
+    }
+
+    fn ref_to_owned(env: EvalEnvs) -> Self::Owned {
+        EvalEnvsOwned {
+            eval_env: env.eval_env.clone(),
+            initial_env: env.initial_env.clone(),
+        }
+    }
 }
 
 pub trait FromEnv<C: Cache> {
@@ -185,24 +241,24 @@ impl State {
 ///
 /// - `env`: an environment mapping variables to their definition (the second placeholder in a
 ///   `let _ = _ in _`)
-pub fn contract_eq<E: TermEnvironment>(
+pub fn contract_eq<'env, 'a: 'env, E: TermEnvironment>(
     var_uid: usize,
-    t1: &RichTerm,
-    env1: &E,
-    t2: &RichTerm,
-    env2: &E,
+    t1: &'a RichTerm,
+    env1: E::Ref<'env>,
+    t2: &'a RichTerm,
+    env2: E::Ref<'env>,
 ) -> bool {
-    contract_eq_bounded(&mut State::new(var_uid), t1, env1, t2, env2)
+    contract_eq_bounded::<E>(&mut State::new(var_uid), t1, env1, t2, env2)
 }
 
 /// Decide type equality on contracts in their respective environment and given the remaining gas
 /// `gas`.
-fn contract_eq_bounded<E: TermEnvironment>(
+fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
     state: &mut State,
-    t1: &RichTerm,
-    env1: &E,
-    t2: &RichTerm,
-    env2: &E,
+    t1: &'a RichTerm,
+    env1: E::Ref<'env>,
+    t2: &'a RichTerm,
+    env2: E::Ref<'env>,
 ) -> bool {
     use Term::*;
 
@@ -221,7 +277,7 @@ fn contract_eq_bounded<E: TermEnvironment>(
         (Enum(id1), Enum(id2)) => id1 == id2,
         (SealingKey(s1), SealingKey(s2)) => s1 == s2,
         (Sealed(key1, inner1, _), Sealed(key2, inner2, _)) => {
-            key1 == key2 && contract_eq_bounded(state, inner1, env1, inner2, env2)
+            key1 == key2 && contract_eq_bounded::<E>(state, inner1, env1, inner2, env2)
         }
         // We only compare string chunks when they represent a plain string (they don't contain any
         // interpolated expression), as static string may be currently parsed as such. We return
@@ -237,8 +293,8 @@ fn contract_eq_bounded<E: TermEnvironment>(
                     })
         }
         (App(head1, arg1), App(head2, arg2)) => {
-            contract_eq_bounded(state, head1, env1, head2, env2)
-                && contract_eq_bounded(state, arg1, env1, arg2, env2)
+            contract_eq_bounded::<E>(state, head1, env1, head2, env2)
+                && contract_eq_bounded::<E>(state, arg1, env1, arg2, env2)
         }
         // All variables must be bound at this stage. This is checked by the typechecker when
         // walking annotations. However, we may assume that `env` is a local environment (that it
@@ -246,8 +302,8 @@ fn contract_eq_bounded<E: TermEnvironment>(
         // if they have the same identifier: whatever global environment the term will be put in,
         // free variables are not redefined locally and will be bound to the same value in any case.
         (Var(id1), Var(id2)) => {
-            env1.get_then(id1.ident(), |binding1| {
-                env2.get_then(id2.ident(), |binding2| {
+            <E as TermEnvironment>::get_then(env1, id1.ident(), |binding1| {
+                <E as TermEnvironment>::get_then(env2, id2.ident(), |binding2| {
                     match (binding1, binding2) {
                         (None, None) => id1 == id2,
                         (Some((t1, env1)), Some((t2, env2))) => {
@@ -256,7 +312,7 @@ fn contract_eq_bounded<E: TermEnvironment>(
                             // still return false if gas was already at zero.
                             let had_gas = state.use_gas();
                             state.use_gas();
-                            had_gas && contract_eq_bounded(state, t1, env1, t2, env2)
+                            had_gas && contract_eq_bounded::<E>(state, t1, env1, t2, env2)
                         }
                         _ => false,
                     }
@@ -265,23 +321,23 @@ fn contract_eq_bounded<E: TermEnvironment>(
         }
         (Var(id), _) => {
             state.use_gas()
-                && env1.get_then(id.ident(), |binding| {
+                && <E as TermEnvironment>::get_then(env1, id.ident(), |binding| {
                     binding
-                        .map(|(t1, env1)| contract_eq_bounded(state, t1, env1, t2, env2))
+                        .map(|(t1, env1)| contract_eq_bounded::<E>(state, t1, env1, t2, env2))
                         .unwrap_or(false)
                 })
         }
         (_, Var(id)) => {
             state.use_gas()
-                && env2.get_then(id.ident(), |binding| {
+                && <E as TermEnvironment>::get_then(env2, id.ident(), |binding| {
                     binding
-                        .map(|(t2, env2)| contract_eq_bounded(state, t1, env1, t2, env2))
+                        .map(|(t2, env2)| contract_eq_bounded::<E>(state, t1, env1, t2, env2))
                         .unwrap_or(false)
                 })
         }
         (Record(r1), Record(r2)) => {
-            map_eq(
-                contract_eq_fields,
+            map_eq::<_, _, E>(
+                contract_eq_fields::<E>,
                 state,
                 &r1.fields,
                 env1,
@@ -295,8 +351,8 @@ fn contract_eq_bounded<E: TermEnvironment>(
         {
             dyn_fields1.is_empty()
                 && dyn_fields2.is_empty()
-                && map_eq(
-                    contract_eq_fields,
+                && map_eq::<_, _, E>(
+                    contract_eq_fields::<E>,
                     state,
                     &r1.fields,
                     env1,
@@ -310,13 +366,13 @@ fn contract_eq_bounded<E: TermEnvironment>(
                 && ts1
                     .iter()
                     .zip(ts2.iter())
-                    .all(|(t1, t2)| contract_eq_bounded(state, t1, env1, t2, env2))
+                    .all(|(t1, t2)| contract_eq_bounded::<E>(state, t1, env1, t2, env2))
                 && attrs1 == attrs2
         }
         // We must compare the inner values as well as the corresponding contracts or type
         // annotations.
         (Annotated(annot1, t1), Annotated(annot2, t2)) => {
-            let value_eq = contract_eq_bounded(state, t1, env1, t2, env2);
+            let value_eq = contract_eq_bounded::<E>(state, t1, env1, t2, env2);
 
             // TODO:
             // - does it really make sense to compare the annotations?
@@ -335,9 +391,9 @@ fn contract_eq_bounded<E: TermEnvironment>(
                 (None, None) => true,
                 (Some(ctr1), Some(ctr2)) => type_eq_bounded(
                     state,
-                    &GenericUnifType::from_type(ctr1.typ.clone(), env1),
+                    &GenericUnifType::<E>::from_type(ctr1.typ.clone(), env1),
                     env1,
-                    &GenericUnifType::from_type(ctr2.typ.clone(), env2),
+                    &GenericUnifType::<E>::from_type(ctr2.typ.clone(), env2),
                     env2,
                 ),
                 _ => false,
@@ -346,7 +402,7 @@ fn contract_eq_bounded<E: TermEnvironment>(
             value_eq && ty_eq
         }
         (Op1(UnaryOp::StaticAccess(id1), t1), Op1(UnaryOp::StaticAccess(id2), t2)) => {
-            id1 == id2 && contract_eq_bounded(state, t1, env1, t2, env2)
+            id1 == id2 && contract_eq_bounded::<E>(state, t1, env1, t2, env2)
         }
         // We don't treat imports, parse errors, nor pairs of terms that don't have the same shape
         _ => false,
@@ -354,16 +410,16 @@ fn contract_eq_bounded<E: TermEnvironment>(
 }
 
 /// Compute the equality between two hashmaps holding either types or terms.
-fn map_eq<V, F, E>(
+fn map_eq<'env, 'a: 'env, V, F, E: TermEnvironment>(
     mut f: F,
     state: &mut State,
-    map1: &IndexMap<LocIdent, V>,
-    env1: &E,
-    map2: &IndexMap<LocIdent, V>,
-    env2: &E,
+    map1: &'a IndexMap<LocIdent, V>,
+    env1: E::Ref<'env>,
+    map2: &'a IndexMap<LocIdent, V>,
+    env2: E::Ref<'env>,
 ) -> bool
 where
-    F: FnMut(&mut State, &V, &E, &V, &E) -> bool,
+    F: FnMut(&mut State, &'a V, E::Ref<'env>, &'a V, E::Ref<'env>) -> bool,
 {
     map1.len() == map2.len()
         && map1.iter().all(|(id, v1)| {
@@ -412,16 +468,16 @@ fn rows_as_set(erows: &UnifEnumRows) -> Option<HashSet<LocIdent>> {
 
 /// Check for contract equality between record fields. Fields are equal if they are both without a
 /// definition, or are both defined and their values are equal.
-fn contract_eq_fields<E: TermEnvironment>(
+fn contract_eq_fields<'env, 'a: 'env, E: TermEnvironment>(
     state: &mut State,
-    field1: &Field,
-    env1: &E,
-    field2: &Field,
-    env2: &E,
+    field1: &'a Field,
+    env1: E::Ref<'env>,
+    field2: &'a Field,
+    env2: E::Ref<'env>,
 ) -> bool {
     match (&field1.value, &field2.value) {
         (Some(ref value1), Some(ref value2)) => {
-            contract_eq_bounded(state, value1, env1, value2, env2)
+            contract_eq_bounded::<E>(state, value1, env1, value2, env2)
         }
         (None, None) => true,
         _ => false,
@@ -438,12 +494,12 @@ fn contract_eq_fields<E: TermEnvironment>(
 /// the rigid type variables encountered have been introduced by `type_eq_bounded` itself. This is
 /// why we don't need unique identifiers that are distinct from the one used during typechecking,
 /// and we can just start from `0`.
-fn type_eq_bounded<E: TermEnvironment>(
+fn type_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
     state: &mut State,
-    ty1: &GenericUnifType<E>,
-    env1: &E,
-    ty2: &GenericUnifType<E>,
-    env2: &E,
+    ty1: &'a GenericUnifType<E>,
+    env1: E::Ref<'env>,
+    ty2: &'a GenericUnifType<E>,
+    env2: E::Ref<'env>,
 ) -> bool {
     match (ty1, ty2) {
         (GenericUnifType::Concrete { typ: s1, .. }, GenericUnifType::Concrete { typ: s2, .. }) => {
@@ -477,12 +533,12 @@ fn type_eq_bounded<E: TermEnvironment>(
                     rows1.is_some() && rows2.is_some() && rows1 == rows2
                 }
                 (TypeF::Record(uty1), TypeF::Record(uty2)) => {
-                    fn type_eq_bounded_wrapper<E: TermEnvironment>(
+                    fn type_eq_bounded_wrapper<'env, 'a: 'env, E: TermEnvironment>(
                         state: &mut State,
-                        uty1: &&GenericUnifType<E>,
-                        env1: &E,
-                        uty2: &&GenericUnifType<E>,
-                        env2: &E,
+                        uty1: &'a &'a GenericUnifType<E>,
+                        env1: E::Ref<'env>,
+                        uty2: &'a &'a GenericUnifType<E>,
+                        env2: E::Ref<'env>,
                     ) -> bool {
                         type_eq_bounded(state, *uty1, env1, *uty2, env2)
                     }
@@ -492,12 +548,12 @@ fn type_eq_bounded<E: TermEnvironment>(
 
                     map1.zip(map2)
                         .map(|(m1, m2)| {
-                            map_eq(type_eq_bounded_wrapper, state, &m1, env1, &m2, env2)
+                            map_eq::<_, _, E>(type_eq_bounded_wrapper, state, &m1, env1, &m2, env2)
                         })
                         .unwrap_or(false)
                 }
                 (TypeF::Flat(t1), TypeF::Flat(t2)) => {
-                    contract_eq_bounded(state, t1, env1, t2, env2)
+                    contract_eq_bounded::<E>(state, t1, env1, t2, env2)
                 }
                 (
                     TypeF::Forall {
diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs
index 1e43aa55c0..e13cded5e5 100644
--- a/core/src/typecheck/mod.rs
+++ b/core/src/typecheck/mod.rs
@@ -329,7 +329,7 @@ pub enum GenericUnifType<E: TermEnvironment> {
     /// 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),
+    Contract(RichTerm, E::Owned),
     /// A rigid type constant which cannot be unified with anything but itself.
     Constant(VarId),
     /// A unification variable.
@@ -478,7 +478,7 @@ 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.
-    pub fn from_record_rows(rrows: RecordRows, env: &E) -> Self {
+    pub fn from_record_rows(rrows: RecordRows, env: E::Ref<'_>) -> Self {
         let f_rrow = |ty: Box<Type>| Box::new(GenericUnifType::from_type(*ty, env));
         let f_rrows =
             |rrows: Box<RecordRows>| Box::new(GenericUnifRecordRows::from_record_rows(*rrows, env));
@@ -820,9 +820,9 @@ 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.
-    pub fn from_type(ty: Type, env: &E) -> Self {
+    pub fn from_type(ty: Type, env: E::Ref<'_>) -> Self {
         match ty.typ {
-            TypeF::Flat(t) => GenericUnifType::Contract(t, env.clone()),
+            TypeF::Flat(t) => GenericUnifType::Contract(t, <E as TermEnvironment>::ref_to_owned(env)),
             ty => GenericUnifType::concrete(ty.map(
                 |ty_| Box::new(GenericUnifType::from_type(*ty_, env)),
                 |rrows| GenericUnifRecordRows::from_record_rows(rrows, env),
diff --git a/core/src/typecheck/unif.rs b/core/src/typecheck/unif.rs
index 8d575a8a3b..1c284fdc7b 100644
--- a/core/src/typecheck/unif.rs
+++ b/core/src/typecheck/unif.rs
@@ -1124,7 +1124,7 @@ impl Unify for UnifType {
                 Err(UnifError::WithConst(VarKindDiscriminant::Type, i, ty))
             }
             (UnifType::Contract(t1, env1), UnifType::Contract(t2, env2))
-                if eq::contract_eq(state.table.max_uvars_count(), &t1, &env1, &t2, &env2) =>
+                if eq::contract_eq::<SimpleTermEnvironment>(state.table.max_uvars_count(), &t1, &env1, &t2, &env2) =>
             {
                 Ok(())
             }

From bfa5cdeab05900010a4de6ef6347c871cb2c2cf8 Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Tue, 26 Sep 2023 12:46:22 +0200
Subject: [PATCH 03/14] Use contract deduplication for annotations as well

Use a special contract deduplication to avoid pretty printing many many
identical type annotations when evaluating. The actual contract
applications were already elided as far as evaluation is concerned, but
contracts annotations were still accumulated without deduplication.
---
 core/src/eval/merge.rs     |  12 +-
 core/src/eval/mod.rs       |  76 +++++-----
 core/src/eval/tests.rs     |  19 ++-
 core/src/program.rs        |  48 ++-----
 core/src/repl/mod.rs       |  27 +++-
 core/src/serialize.rs      |   7 +-
 core/src/term/mod.rs       |  46 +++++-
 core/src/typecheck/eq.rs   | 286 +++++++++++++++++++++++++------------
 core/src/typecheck/mod.rs  |   4 +-
 core/src/typecheck/unif.rs |   8 +-
 utils/src/bench.rs         |   8 +-
 11 files changed, 342 insertions(+), 199 deletions(-)

diff --git a/core/src/eval/merge.rs b/core/src/eval/merge.rs
index cee32a9eaa..9257988eb8 100644
--- a/core/src/eval/merge.rs
+++ b/core/src/eval/merge.rs
@@ -32,7 +32,7 @@ use crate::label::{Label, MergeLabel};
 use crate::position::TermPos;
 use crate::term::{
     record::{self, Field, FieldDeps, FieldMetadata, RecordAttrs, RecordData},
-    BinaryOp, IndexMap, RichTerm, Term,
+    BinaryOp, IndexMap, RichTerm, Term, TypeAnnotation,
 };
 use crate::transform::Closurizable;
 
@@ -415,13 +415,19 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a LocIdent> + Clon
     let mut pending_contracts = pending_contracts1.revert_closurize(cache, env_final, env1.clone());
 
     for ctr2 in pending_contracts2.revert_closurize(cache, env_final, env2.clone()) {
-        RuntimeContract::push_elide(initial_env, &mut pending_contracts, &env_final, ctr2, &env_final);
+        RuntimeContract::push_elide(
+            initial_env,
+            &mut pending_contracts,
+            &env_final,
+            ctr2,
+            &env_final,
+        );
     }
 
     Ok(Field {
         metadata: FieldMetadata {
             doc: merge_doc(metadata1.doc, metadata2.doc),
-            annotation: Combine::combine(metadata1.annotation, metadata2.annotation),
+            annotation: TypeAnnotation::combine_elide(metadata1.annotation, metadata2.annotation),
             // If one of the record requires this field, then it musn't be optional. The
             // resulting field is optional iff both are.
             opt: metadata1.opt && metadata2.opt,
diff --git a/core/src/eval/mod.rs b/core/src/eval/mod.rs
index 9dec90f432..20ef42b3ed 100644
--- a/core/src/eval/mod.rs
+++ b/core/src/eval/mod.rs
@@ -175,45 +175,43 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
 
     /// Fully evaluate a Nickel term: the result is not a WHNF but to a value with all variables
     /// substituted.
-    pub fn eval_full(
-        &mut self,
-        t0: RichTerm,
-    ) -> Result<RichTerm, EvalError> {
-        self.eval_full_closure(Closure::atomic_closure(t0)).map(|(term, _)| term)
+    pub fn eval_full(&mut self, t0: RichTerm) -> Result<RichTerm, EvalError> {
+        self.eval_full_closure(Closure::atomic_closure(t0))
+            .map(|(term, _)| term)
     }
 
-    pub fn eval_full_closure(
-        &mut self,
-        t0: Closure,
-    ) -> Result<(RichTerm, Environment), EvalError> {
+    pub fn eval_full_closure(&mut self, t0: Closure) -> Result<(RichTerm, Environment), EvalError> {
         self.eval_deep_closure(t0, false)
             .map(|(term, env)| (subst(&self.cache, term, &self.initial_env, &env), env))
     }
 
     /// Like `eval_full`, but skips evaluating record fields marked `not_exported`.
-    pub fn eval_full_for_export(
-        &mut self,
-        t0: RichTerm,
-    ) -> Result<RichTerm, EvalError> {
+    pub fn eval_full_for_export(&mut self, t0: RichTerm) -> Result<RichTerm, EvalError> {
         self.eval_deep_closure(Closure::atomic_closure(t0), true)
             .map(|(term, env)| subst(&self.cache, term, &self.initial_env, &env))
     }
 
     /// Fully evaluates a Nickel term like `eval_full`, but does not substitute all variables.
-    pub fn eval_deep(
-        &mut self,
-        t0: RichTerm,
-    ) -> Result<RichTerm, EvalError> {
+    pub fn eval_deep(&mut self, t0: RichTerm) -> Result<RichTerm, EvalError> {
         self.eval_deep_closure(Closure::atomic_closure(t0), false)
             .map(|(term, _)| term)
     }
 
+    /// Use a specific initial environment for evaluation. Usually, [VirtualMachine::prepare_eval]
+    /// is populating the initial environment. But in some cases, such as testing or benchmarks, we
+    /// might want to use a different one.
+    ///
+    /// Return the new virtual machine with the updated initial environment.
+    pub fn with_initial_env(mut self, env: Environment) -> Self {
+        self.initial_env = env;
+        self
+    }
+
     fn eval_deep_closure(
         &mut self,
         mut closure: Closure,
         for_export: bool,
     ) -> Result<(RichTerm, Environment), EvalError> {
-
         closure.body = mk_term::op1(
             UnaryOp::Force {
                 ignore_not_exported: for_export,
@@ -230,14 +228,15 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
     /// `baz`. The content of `baz` is evaluated as well, and variables are substituted, in order
     /// to obtain a value that can be printed. The metadata and the evaluated value are returned as
     /// a new field.
-    pub fn query(
-        &mut self,
-        t: RichTerm,
-        path: QueryPath,
-        initial_env: &Environment,
-    ) -> Result<Field, EvalError> {
-        let mut prev_pos = t.pos;
-        let (rt, mut env) = self.eval_closure(Closure::atomic_closure(t))?;
+    pub fn query(&mut self, t: RichTerm, path: QueryPath) -> Result<Field, EvalError> {
+        self.query_closure(Closure::atomic_closure(t), path)
+    }
+
+    /// Same as [VirtualMachine::query], but starts from a closure instead of a term in an empty
+    /// environment.
+    pub fn query_closure(&mut self, closure: Closure, path: QueryPath) -> Result<Field, EvalError> {
+        let mut prev_pos = closure.body.pos;
+        let (rt, mut env) = self.eval_closure(closure)?;
 
         let mut field: Field = rt.into();
 
@@ -277,12 +276,10 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                     pending_contracts.into_iter(),
                                     prev_pos,
                                 );
-                                let (new_value, new_env) = self.eval_closure(
-                                    Closure {
-                                        body: value_with_ctr,
-                                        env: env.clone(),
-                                    }
-                                )?;
+                                let (new_value, new_env) = self.eval_closure(Closure {
+                                    body: value_with_ctr,
+                                    env: env.clone(),
+                                })?;
                                 env = new_env;
 
                                 Ok(new_value)
@@ -827,18 +824,29 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
 }
 
 impl<C: Cache> VirtualMachine<ImportCache, C> {
+    /// Prepare the underlying program for evaluation (load the stdlib, typecheck, transform,
+    /// etc.). Sets the initial environment of the virtual machine.
     pub fn prepare_eval(&mut self, main_id: FileId) -> Result<RichTerm, Error> {
         let Envs {
             eval_env,
             type_ctxt,
-        }: Envs = self.import_resolver.prepare_stdlib(&mut self.cache)?;
+        } = self.import_resolver.prepare_stdlib(&mut self.cache)?;
         self.import_resolver.prepare(main_id, &type_ctxt)?;
         self.initial_env = eval_env;
         Ok(self.import_resolver().get(main_id).unwrap())
     }
 
+    /// Prepare the stdlib for evaluation. Sets the initial environment of the virtual machine. As
+    /// opposed to [VirtualMachine::prepare_eval], [VirtualMachine::prepare_stdlib] doesn't prepare
+    /// the main program yet (typechecking, transformations, etc.).
+    ///
+    /// # Returns
+    ///
+    /// The initial evaluation and typing environments, containing the stdlib items.
     pub fn prepare_stdlib(&mut self) -> Result<Envs, Error> {
-        self.import_resolver.prepare_stdlib(&mut self.cache)
+        let envs = self.import_resolver.prepare_stdlib(&mut self.cache)?;
+        self.initial_env = envs.eval_env.clone();
+        Ok(envs)
     }
 }
 
diff --git a/core/src/eval/tests.rs b/core/src/eval/tests.rs
index a2f971825e..8877f0bb14 100644
--- a/core/src/eval/tests.rs
+++ b/core/src/eval/tests.rs
@@ -14,7 +14,7 @@ use codespan::Files;
 /// Evaluate a term without import support.
 fn eval_no_import(t: RichTerm) -> Result<Term, EvalError> {
     VirtualMachine::<_, CacheImpl>::new(DummyResolver {}, std::io::sink())
-        .eval(t, &Environment::new())
+        .eval(t)
         .map(Term::from)
 }
 
@@ -169,9 +169,7 @@ fn imports() {
     let mk_import_two = mk_import("x", "two", mk_term::var("x"), &mut vm).unwrap();
     vm.reset();
     assert_eq!(
-        vm.eval(mk_import_two, &Environment::new(),)
-            .map(RichTerm::without_pos)
-            .unwrap(),
+        vm.eval(mk_import_two).map(RichTerm::without_pos).unwrap(),
         mk_term::integer(2)
     );
 
@@ -187,9 +185,7 @@ fn imports() {
     );
     vm.reset();
     assert_eq!(
-        vm.eval(mk_import_lib.unwrap(), &Environment::new(),)
-            .map(Term::from)
-            .unwrap(),
+        vm.eval(mk_import_lib.unwrap()).map(Term::from).unwrap(),
         Term::Bool(true)
     );
 }
@@ -269,7 +265,8 @@ fn initial_env() {
     let t = mk_term::let_in("x", mk_term::integer(2), mk_term::var("x"));
     assert_eq!(
         VirtualMachine::new_with_cache(DummyResolver {}, eval_cache.clone(), std::io::sink())
-            .eval(t, &initial_env)
+            .with_initial_env(initial_env.clone())
+            .eval(t)
             .map(RichTerm::without_pos),
         Ok(mk_term::integer(2))
     );
@@ -277,7 +274,8 @@ fn initial_env() {
     let t = mk_term::let_in("x", mk_term::integer(2), mk_term::var("g"));
     assert_eq!(
         VirtualMachine::new_with_cache(DummyResolver {}, eval_cache.clone(), std::io::sink())
-            .eval(t, &initial_env)
+            .with_initial_env(initial_env.clone())
+            .eval(t)
             .map(RichTerm::without_pos),
         Ok(mk_term::integer(1))
     );
@@ -286,7 +284,8 @@ fn initial_env() {
     let t = mk_term::let_in("g", mk_term::integer(2), mk_term::var("g"));
     assert_eq!(
         VirtualMachine::new_with_cache(DummyResolver {}, eval_cache.clone(), std::io::sink())
-            .eval(t, &initial_env)
+            .with_initial_env(initial_env.clone())
+            .eval(t)
             .map(RichTerm::without_pos),
         Ok(mk_term::integer(2))
     );
diff --git a/core/src/program.rs b/core/src/program.rs
index 4105ec3297..1d15f6f13b 100644
--- a/core/src/program.rs
+++ b/core/src/program.rs
@@ -234,7 +234,7 @@ impl<EC: EvalCache> Program<EC> {
             .clone())
     }
 
-    /// Retrieve the parsed term and typecheck it, and generate a fresh initial environment. Return
+    /// Retrieve the parsed term, typecheck it, and generate a fresh initial environment. Return
     /// both.
     fn prepare_eval(&mut self) -> Result<RichTerm, Error> {
         // If there are no overrides, we avoid the boilerplate of creating an empty record and
@@ -299,9 +299,7 @@ impl<EC: EvalCache> Program<EC> {
     pub fn eval_full_for_export(&mut self) -> Result<RichTerm, Error> {
         let t = self.prepare_eval()?;
         self.vm.reset();
-        self.vm
-            .eval_full_for_export(t)
-            .map_err(|e| e.into())
+        self.vm.eval_full_for_export(t).map_err(|e| e.into())
     }
 
     /// Same as `eval_full`, but does not substitute all variables.
@@ -313,9 +311,10 @@ impl<EC: EvalCache> Program<EC> {
 
     /// Wrapper for [`query`].
     pub fn query(&mut self, path: Option<String>) -> Result<Field, Error> {
-        let initial_env = self.vm.prepare_stdlib()?;
+        let rt = self.prepare_eval()?;
         let query_path = QueryPath::parse_opt(self.vm.import_resolver_mut(), path)?;
-        query(&mut self.vm, self.main_id, &initial_env, query_path)
+
+        Ok(self.vm.query(rt, query_path)?)
     }
 
     /// Load, parse, and typecheck the program and the standard library, if not already done.
@@ -447,12 +446,10 @@ impl<EC: EvalCache> Program<EC> {
             current_env: Environment,
         ) -> Result<RichTerm, Error> {
             vm.reset();
-            let result = vm.eval_closure(
-                Closure {
-                    body: t.clone(),
-                    env: current_env,
-                },
-            );
+            let result = vm.eval_closure(Closure {
+                body: t.clone(),
+                env: current_env,
+            });
 
             // We expect to hit `MissingFieldDef` errors. When a configuration
             // contains undefined record fields they most likely will be used
@@ -524,7 +521,7 @@ impl<EC: EvalCache> Program<EC> {
         out: &mut impl std::io::Write,
         apply_transforms: bool,
     ) -> Result<(), Error> {
-        use crate::pretty::*;
+        use crate::{pretty::*, transform::transform};
         use pretty::BoxAllocator;
 
         let Program {
@@ -534,7 +531,7 @@ impl<EC: EvalCache> Program<EC> {
 
         let rt = vm.import_resolver().parse_nocache(*main_id)?.0;
         let rt = if apply_transforms {
-            crate::transform::transform(rt, None).map_err(EvalError::from)?
+            transform(rt, None).map_err(EvalError::from)?
         } else {
             rt
         };
@@ -545,29 +542,6 @@ impl<EC: EvalCache> Program<EC> {
     }
 }
 
-/// Query the metadata of a path of a term in the cache.
-///
-/// The path is a list of dot separated identifiers. For example, querying `{a = {b  = ..}}` (call
-/// it `exp`) with path `a.b` will evaluate `exp.a` and retrieve the `b` field. `b` is forced as
-/// well, in order to print its value (note that forced just means evaluated to a WHNF, it isn't
-/// deeply - or recursively - evaluated).
-//TODO: also gather type information, such that `query a.b.c <<< '{ ... } : {a: {b: {c: Num}}}`
-//would additionally report `type: Num` for example. Maybe use the LSP infrastructure?
-//TODO: not sure where this should go. It seems to embed too much logic to be in `Cache`, but is
-//common to both `Program` and `Repl`. Leaving it here as a stand-alone function for now
-pub fn query<EC: EvalCache>(
-    vm: &mut VirtualMachine<Cache, EC>,
-    file_id: FileId,
-    initial_env: &Envs,
-    path: QueryPath,
-) -> Result<Field, Error> {
-    vm.import_resolver_mut()
-        .prepare(file_id, &initial_env.type_ctxt)?;
-
-    let rt = vm.import_resolver().get_owned(file_id).unwrap();
-    Ok(vm.query(rt, path, &initial_env.eval_env)?)
-}
-
 #[cfg(feature = "doc")]
 mod doc {
     use crate::error::{Error, ExportError, IOError};
diff --git a/core/src/repl/mod.rs b/core/src/repl/mod.rs
index 2db08cdfa8..cc9d1d48e1 100644
--- a/core/src/repl/mod.rs
+++ b/core/src/repl/mod.rs
@@ -189,7 +189,15 @@ impl<EC: EvalCache> ReplImpl<EC> {
         match term {
             ExtendedTerm::RichTerm(t) => {
                 let t = self.prepare(None, t)?;
-                Ok(eval_function(&mut self.vm, Closure { body: t, env: self.env.eval_env.clone() })?.0.into())
+                Ok(eval_function(
+                    &mut self.vm,
+                    Closure {
+                        body: t,
+                        env: self.env.eval_env.clone(),
+                    },
+                )?
+                .0
+                .into())
             }
             ExtendedTerm::ToplevelLet(id, t) => {
                 let t = self.prepare(Some(id), t)?;
@@ -223,9 +231,10 @@ impl<EC: EvalCache> Repl for ReplImpl<EC> {
 
         let term = self.prepare(None, term)?;
 
-        let (term, new_env) = self
-            .vm
-            .eval_closure(Closure { body: term, env: self.env.eval_env.clone()})?;
+        let (term, new_env) = self.vm.eval_closure(Closure {
+            body: term,
+            env: self.env.eval_env.clone(),
+        })?;
 
         if !matches!(term.as_ref(), Term::Record(..) | Term::RecRecord(..)) {
             return Err(Error::EvalError(EvalError::Other(
@@ -295,8 +304,6 @@ impl<EC: EvalCache> Repl for ReplImpl<EC> {
     }
 
     fn query(&mut self, path: String) -> Result<Field, Error> {
-        use crate::program;
-
         let mut query_path = QueryPath::parse(self.vm.import_resolver_mut(), path)?;
 
         // remove(): this is safe because there is no such thing as an empty field path. If `path`
@@ -309,7 +316,13 @@ impl<EC: EvalCache> Repl for ReplImpl<EC> {
             .import_resolver_mut()
             .replace_string(SourcePath::ReplQuery, target.label().into());
 
-        program::query(&mut self.vm, file_id, &self.env, query_path)
+        Ok(self.vm.query_closure(
+            Closure {
+                body: self.vm.import_resolver().get_owned(file_id).unwrap(),
+                env: self.env.eval_env.clone(),
+            },
+            query_path,
+        )?)
     }
 
     fn cache_mut(&mut self) -> &mut Cache {
diff --git a/core/src/serialize.rs b/core/src/serialize.rs
index b9a4c30c0b..9b86e85da4 100644
--- a/core/src/serialize.rs
+++ b/core/src/serialize.rs
@@ -281,7 +281,7 @@ mod tests {
     use super::*;
     use crate::cache::resolvers::DummyResolver;
     use crate::eval::cache::CacheImpl;
-    use crate::eval::{Environment, VirtualMachine};
+    use crate::eval::VirtualMachine;
     use crate::program::Program;
     use crate::term::{make as mk_term, BinaryOp};
     use serde_json::json;
@@ -306,10 +306,7 @@ mod tests {
     fn assert_nickel_eq(term: RichTerm, expected: RichTerm) {
         assert_eq!(
             VirtualMachine::<_, CacheImpl>::new(DummyResolver {}, std::io::stderr())
-                .eval(
-                    mk_term::op2(BinaryOp::Eq(), term, expected),
-                    &Environment::new(),
-                )
+                .eval(mk_term::op2(BinaryOp::Eq(), term, expected))
                 .map(Term::from),
             Ok(Term::Bool(true))
         )
diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs
index a97fc213dc..ff49b1fc60 100644
--- a/core/src/term/mod.rs
+++ b/core/src/term/mod.rs
@@ -20,13 +20,13 @@ use string::NickelString;
 use crate::{
     destructuring::RecordPattern,
     error::{EvalError, ParseError},
+    eval::Environment,
     identifier::LocIdent,
     label::{Label, MergeLabel},
     match_sharedterm,
     position::TermPos,
     typ::{Type, UnboundTypeVariableError},
-    eval::Environment,
-    typecheck::eq::{contract_eq, EvalEnvs},
+    typecheck::eq::{contract_eq, type_eq_noenv, EvalEnvs},
 };
 
 use codespan::FileId;
@@ -322,6 +322,9 @@ impl RuntimeContract {
         contracts.fold(rt, |acc, ctr| ctr.apply(acc, pos))
     }
 
+    /// Push a pending contract to a vector of contracts if the contract to add isn't already
+    /// present in the vector, according to the notion of contract equality defined in
+    /// [crate::typecheck::eq].
     pub fn push_elide(
         initial_env: &Environment,
         contracts: &mut Vec<RuntimeContract>,
@@ -329,14 +332,20 @@ impl RuntimeContract {
         ctr: Self,
         env2: &Environment,
     ) {
-        eprintln!("push_elide: ({})", ctr.contract);
-        let envs1 = EvalEnvs { eval_env: env1, initial_env};
+        // eprintln!("push_elide: ({})", ctr.contract);
+        let envs1 = EvalEnvs {
+            eval_env: env1,
+            initial_env,
+        };
 
         for c in contracts.iter() {
-            eprintln!("- comparing against ({})", c.contract);
-            let envs = EvalEnvs { eval_env: env2, initial_env};
+            // eprintln!("- comparing against ({})", c.contract);
+            let envs = EvalEnvs {
+                eval_env: env2,
+                initial_env,
+            };
             if contract_eq::<EvalEnvs>(0, &c.contract, envs1, &ctr.contract, envs) {
-                eprintln!("  -> found equal contract, eliding");
+                // eprintln!("  -> found equal contract, eliding");
                 return;
             }
         }
@@ -600,6 +609,29 @@ impl TypeAnnotation {
     pub fn is_empty(&self) -> bool {
         self.typ.is_none() && self.contracts.is_empty()
     }
+
+    /// Same as [`Combine::combine`], but eliminate duplicate contracts. As there's no notion of
+    /// environment when combining annotations, we use an unsound contract equality checking, which
+    /// just compares things syntactically.
+    pub fn combine_elide(left: Self, right: Self) -> Self {
+        let mut contracts = left.contracts;
+
+        let typ = match (left.typ, right.typ) {
+            (left_ty @ Some(_), Some(right_ty)) => {
+                contracts.push(right_ty);
+                left_ty
+            }
+            (left_ty, right_ty) => left_ty.or(right_ty),
+        };
+
+        for ctr in right.contracts.into_iter() {
+            if !contracts.iter().any(|c| type_eq_noenv(0, &c.typ, &ctr.typ)) {
+                contracts.push(ctr);
+            }
+        }
+
+        TypeAnnotation { typ, contracts }
+    }
 }
 
 impl From<TypeAnnotation> for LetMetadata {
diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index 03a2f6198b..ef0856f32d 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -54,26 +54,35 @@ use std::fmt::Debug;
 /// The maximal number of variable links we want to unfold before abandoning the check. It should
 /// stay low, but has been fixed arbitrarily: feel fee to increase reasonably if it turns out
 /// legitimate type equalities between simple contracts are unduly rejected in practice.
-pub const MAX_GAS: u8 = 20;
+pub const MAX_GAS: u8 = 10;
+
+/// Like `std::borrow::ToOwned`, but defined as a local trait for convenience and to be implemented
+/// on the reference type directly. Beside the slightly different signature, the blanket
+/// implementations of `ToOwned` would interfere with our own.
+pub trait ToOwnedEnv<Owned> {
+    fn to_owned_env(self) -> Owned;
+}
 
 /// Abstract over the term environment, which is represented differently in the typechecker and
 /// during evaluation.
 ///
-/// The evaluation environment holds [crate::eval::cache::CacheIndex]es,
-/// while the term environment used during typechecking is just maps identifiers to
-/// a pair `(RichTerm, Environment)`. To have an interface that works with both,
-/// `TermEnvironment::get_then` has to take a closure representing the continuation of the task to
-/// do with the result instead of merely returning it.
+/// The evaluation environment holds [crate::eval::cache::CacheIndex]es, while the term environment
+/// used during typechecking is just maps identifiers to a pair `(RichTerm, Environment)`. To have
+/// an interface that works with both, `TermEnvironment::get_then` has to take a closure
+/// representing the continuation of the task to do with the result instead of merely returning it.
 pub trait TermEnvironment: Clone {
-    type Owned : Clone + PartialEq + Debug;
-    type Ref<'a> : Copy;
+    /// The representation of the environment is different during typechecking and evaluation. In
+    /// particular, the evaluation's environment is actually a pair of environments (the initial
+    /// environment and the local environment), and thus the notion of owned environment of the
+    /// environment and of reference to it are not necessarily the obvious `Self` and `&Self`
+    /// respectively.
+    /// The trait abstract over it by defining a reference type and an owned type.
+    type Owned: Clone + PartialEq + Debug;
+    type Ref<'a>: Copy + ToOwnedEnv<Self::Owned>;
 
     fn get_then<F, T>(env: Self::Ref<'_>, id: Ident, f: F) -> T
     where
         F: FnOnce(Option<(&RichTerm, Self::Ref<'_>)>) -> T;
-
-    fn owned_to_ref(&self) -> Self::Ref<'_>;
-    fn ref_to_owned(env: Self::Ref<'_>) -> Self::Owned;
 }
 
 /// A simple term environment, as a mapping from identifiers to a tuple of a term and an
@@ -93,6 +102,12 @@ impl Default for SimpleTermEnvironment {
     }
 }
 
+impl<'a, E: Clone> ToOwnedEnv<E> for &'a E {
+    fn to_owned_env(self) -> E {
+        self.clone()
+    }
+}
+
 impl TermEnvironment for SimpleTermEnvironment {
     type Owned = Self;
     type Ref<'a> = &'a Self;
@@ -103,14 +118,6 @@ impl TermEnvironment for SimpleTermEnvironment {
     {
         f(env.0.get(&id).map(|(rt, env)| (rt, env)))
     }
-
-    fn owned_to_ref(&self) -> Self::Ref<'_> {
-        self
-    }
-
-    fn ref_to_owned(env: &Self) -> Self::Owned {
-        env.clone()
-    }
 }
 
 impl<'a> AsRef<SimpleTermEnvironment> for &'a SimpleTermEnvironment {
@@ -133,13 +140,22 @@ impl std::iter::FromIterator<(Ident, (RichTerm, SimpleTermEnvironment))> for Sim
 #[derive(Clone, Copy)]
 pub struct EvalEnvs<'a> {
     pub eval_env: &'a eval::Environment,
-    pub initial_env:  &'a eval::Environment,
+    pub initial_env: &'a eval::Environment,
 }
 
 #[derive(Clone, PartialEq, Debug)]
 pub struct EvalEnvsOwned {
     pub eval_env: eval::Environment,
-    pub initial_env:  eval::Environment,
+    pub initial_env: eval::Environment,
+}
+
+impl<'a> ToOwnedEnv<EvalEnvsOwned> for EvalEnvs<'a> {
+    fn to_owned_env(self) -> EvalEnvsOwned {
+        EvalEnvsOwned {
+            eval_env: self.eval_env.clone(),
+            initial_env: self.initial_env.clone(),
+        }
+    }
 }
 
 impl<'a> TermEnvironment for EvalEnvs<'a> {
@@ -150,27 +166,28 @@ impl<'a> TermEnvironment for EvalEnvs<'a> {
     where
         F: FnOnce(Option<(&RichTerm, EvalEnvs<'_>)>) -> T,
     {
-        debug_assert!(env.eval_env.get(&id).or(env.initial_env.get(&id)).is_some(), "unbound variable `{}`", id);
-
-        match env.eval_env.get(&id).or(env.initial_env.get(&id)).map(eval::cache::lazy::Thunk::borrow) {
-            Some(closure_ref) => f(Some((&closure_ref.body, EvalEnvs { eval_env: &closure_ref.env, initial_env: env.initial_env }))),
+        debug_assert!(
+            env.eval_env.get(&id).or(env.initial_env.get(&id)).is_some(),
+            "unbound variable `{}`",
+            id
+        );
+
+        match env
+            .eval_env
+            .get(&id)
+            .or(env.initial_env.get(&id))
+            .map(eval::cache::lazy::Thunk::borrow)
+        {
+            Some(closure_ref) => f(Some((
+                &closure_ref.body,
+                EvalEnvs {
+                    eval_env: &closure_ref.env,
+                    initial_env: env.initial_env,
+                },
+            ))),
             None => f(None),
         }
     }
-
-    fn owned_to_ref(&self) -> Self::Ref<'_> {
-        EvalEnvs {
-            eval_env: self.eval_env,
-            initial_env: self.initial_env,
-        }
-    }
-
-    fn ref_to_owned(env: EvalEnvs) -> Self::Owned {
-        EvalEnvsOwned {
-            eval_env: env.eval_env.clone(),
-            initial_env: env.initial_env.clone(),
-        }
-    }
 }
 
 pub trait FromEnv<C: Cache> {
@@ -192,6 +209,26 @@ impl<C: Cache> FromEnv<C> for SimpleTermEnvironment {
     }
 }
 
+/// Dummy environment used in conjunction with [VarEq::Direct] to compare variables by name.
+///
+/// **Warning**: calling `get_then` on this environment will panic, as it has no way to generate a
+/// term from a variable. It must only be used in conjunction with [VarEq::Direct], which doesn't
+/// access the environment.
+#[derive(Copy, Clone, Debug, PartialEq)]
+pub struct NoEnvironment;
+
+impl TermEnvironment for NoEnvironment {
+    type Owned = Self;
+    type Ref<'a> = &'a Self;
+
+    fn get_then<F, T>(_env: &Self, id: Ident, _f: F) -> T
+    where
+        F: FnOnce(Option<(&RichTerm, &NoEnvironment)>) -> T,
+    {
+        panic!("contract equality checking: cannot get variable `{id}` from no environment")
+    }
+}
+
 /// State threaded through the type equality computation.
 #[derive(Copy, Clone, Default)]
 struct State {
@@ -235,30 +272,66 @@ impl State {
     }
 }
 
-/// Compute the equality between two flat types (contracts).
+/// Different possible behavior for variables comparison variables.
+#[derive(Copy, Clone, PartialEq, Eq)]
+enum VarEq {
+    /// Use the environment to fetch the content of variables and compare them.
+    Environment,
+    /// Don't use an environment and simply compare variables by name. This is unsound, and should
+    /// only be used to deduplicate annotations for pretty-printing.
+    Direct,
+}
+
+/// Compute equality between two contracts.
 ///
 /// # Parameters
 ///
 /// - `env`: an environment mapping variables to their definition (the second placeholder in a
 ///   `let _ = _ in _`)
-pub fn contract_eq<'env, 'a: 'env, E: TermEnvironment>(
+pub fn contract_eq<E: TermEnvironment>(
     var_uid: usize,
-    t1: &'a RichTerm,
-    env1: E::Ref<'env>,
-    t2: &'a RichTerm,
-    env2: E::Ref<'env>,
+    t1: &RichTerm,
+    env1: E::Ref<'_>,
+    t2: &RichTerm,
+    env2: E::Ref<'_>,
 ) -> bool {
-    contract_eq_bounded::<E>(&mut State::new(var_uid), t1, env1, t2, env2)
+    contract_eq_bounded::<E>(
+        &mut State::new(var_uid),
+        VarEq::Environment,
+        t1,
+        env1,
+        t2,
+        env2,
+    )
+}
+
+/// **Warning**: this function isn't computing a sound contract equality (it could equate contracts
+/// that aren't actually the same). It is used to deduplicate type and contract annotations for
+/// pretty-printing, where there is no notion of environment and the only thing that matters is
+/// that they are printed the same or not.
+///
+/// Compute equality between two contracts, considering that two variables with the same name are
+/// equal.
+pub fn type_eq_noenv(var_uid: usize, t1: &Type, t2: &Type) -> bool {
+    type_eq_bounded::<NoEnvironment>(
+        &mut State::new(var_uid),
+        VarEq::Direct,
+        &GenericUnifType::<NoEnvironment>::from_type(t1.clone(), &NoEnvironment),
+        &NoEnvironment,
+        &GenericUnifType::<NoEnvironment>::from_type(t2.clone(), &NoEnvironment),
+        &NoEnvironment,
+    )
 }
 
 /// Decide type equality on contracts in their respective environment and given the remaining gas
 /// `gas`.
-fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
+fn contract_eq_bounded<E: TermEnvironment>(
     state: &mut State,
-    t1: &'a RichTerm,
-    env1: E::Ref<'env>,
-    t2: &'a RichTerm,
-    env2: E::Ref<'env>,
+    var_eq: VarEq,
+    t1: &RichTerm,
+    env1: E::Ref<'_>,
+    t2: &RichTerm,
+    env2: E::Ref<'_>,
 ) -> bool {
     use Term::*;
 
@@ -277,7 +350,7 @@ fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
         (Enum(id1), Enum(id2)) => id1 == id2,
         (SealingKey(s1), SealingKey(s2)) => s1 == s2,
         (Sealed(key1, inner1, _), Sealed(key2, inner2, _)) => {
-            key1 == key2 && contract_eq_bounded::<E>(state, inner1, env1, inner2, env2)
+            key1 == key2 && contract_eq_bounded::<E>(state, var_eq, inner1, env1, inner2, env2)
         }
         // We only compare string chunks when they represent a plain string (they don't contain any
         // interpolated expression), as static string may be currently parsed as such. We return
@@ -293,9 +366,10 @@ fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
                     })
         }
         (App(head1, arg1), App(head2, arg2)) => {
-            contract_eq_bounded::<E>(state, head1, env1, head2, env2)
-                && contract_eq_bounded::<E>(state, arg1, env1, arg2, env2)
+            contract_eq_bounded::<E>(state, var_eq, head1, env1, head2, env2)
+                && contract_eq_bounded::<E>(state, var_eq, arg1, env1, arg2, env2)
         }
+        (Var(id1), Var(id2)) if var_eq == VarEq::Direct => id1 == id2,
         // All variables must be bound at this stage. This is checked by the typechecker when
         // walking annotations. However, we may assume that `env` is a local environment (that it
         // doesn't include the stdlib). In that case, free variables (unbound) may be deemed equal
@@ -312,18 +386,23 @@ fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
                             // still return false if gas was already at zero.
                             let had_gas = state.use_gas();
                             state.use_gas();
-                            had_gas && contract_eq_bounded::<E>(state, t1, env1, t2, env2)
+                            had_gas && contract_eq_bounded::<E>(state, var_eq, t1, env1, t2, env2)
                         }
                         _ => false,
                     }
                 })
             })
         }
+        // If one term is a variable and not the other, and we don't have access to an environment, the
+        // term are considered unequal
+        (Var(_), _) | (_, Var(_)) if var_eq == VarEq::Direct => false,
         (Var(id), _) => {
             state.use_gas()
                 && <E as TermEnvironment>::get_then(env1, id.ident(), |binding| {
                     binding
-                        .map(|(t1, env1)| contract_eq_bounded::<E>(state, t1, env1, t2, env2))
+                        .map(|(t1, env1)| {
+                            contract_eq_bounded::<E>(state, var_eq, t1, env1, t2, env2)
+                        })
                         .unwrap_or(false)
                 })
         }
@@ -331,7 +410,9 @@ fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
             state.use_gas()
                 && <E as TermEnvironment>::get_then(env2, id.ident(), |binding| {
                     binding
-                        .map(|(t2, env2)| contract_eq_bounded::<E>(state, t1, env1, t2, env2))
+                        .map(|(t2, env2)| {
+                            contract_eq_bounded::<E>(state, var_eq, t1, env1, t2, env2)
+                        })
                         .unwrap_or(false)
                 })
         }
@@ -339,6 +420,7 @@ fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
             map_eq::<_, _, E>(
                 contract_eq_fields::<E>,
                 state,
+                var_eq,
                 &r1.fields,
                 env1,
                 &r2.fields,
@@ -354,6 +436,7 @@ fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
                 && map_eq::<_, _, E>(
                     contract_eq_fields::<E>,
                     state,
+                    var_eq,
                     &r1.fields,
                     env1,
                     &r2.fields,
@@ -366,13 +449,13 @@ fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
                 && ts1
                     .iter()
                     .zip(ts2.iter())
-                    .all(|(t1, t2)| contract_eq_bounded::<E>(state, t1, env1, t2, env2))
+                    .all(|(t1, t2)| contract_eq_bounded::<E>(state, var_eq, t1, env1, t2, env2))
                 && attrs1 == attrs2
         }
         // We must compare the inner values as well as the corresponding contracts or type
         // annotations.
         (Annotated(annot1, t1), Annotated(annot2, t2)) => {
-            let value_eq = contract_eq_bounded::<E>(state, t1, env1, t2, env2);
+            let value_eq = contract_eq_bounded::<E>(state, var_eq, t1, env1, t2, env2);
 
             // TODO:
             // - does it really make sense to compare the annotations?
@@ -391,6 +474,7 @@ fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
                 (None, None) => true,
                 (Some(ctr1), Some(ctr2)) => type_eq_bounded(
                     state,
+                    var_eq,
                     &GenericUnifType::<E>::from_type(ctr1.typ.clone(), env1),
                     env1,
                     &GenericUnifType::<E>::from_type(ctr2.typ.clone(), env2),
@@ -402,29 +486,38 @@ fn contract_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
             value_eq && ty_eq
         }
         (Op1(UnaryOp::StaticAccess(id1), t1), Op1(UnaryOp::StaticAccess(id2), t2)) => {
-            id1 == id2 && contract_eq_bounded::<E>(state, t1, env1, t2, env2)
+            id1 == id2 && contract_eq_bounded::<E>(state, var_eq, t1, env1, t2, env2)
         }
+        (Type(ty1), Type(ty2)) => type_eq_bounded(
+            state,
+            var_eq,
+            &GenericUnifType::<E>::from_type(ty1.clone(), env1),
+            env1,
+            &GenericUnifType::<E>::from_type(ty2.clone(), env2),
+            env2,
+        ),
         // We don't treat imports, parse errors, nor pairs of terms that don't have the same shape
         _ => false,
     }
 }
 
 /// Compute the equality between two hashmaps holding either types or terms.
-fn map_eq<'env, 'a: 'env, V, F, E: TermEnvironment>(
+fn map_eq<V, F, E: TermEnvironment>(
     mut f: F,
     state: &mut State,
-    map1: &'a IndexMap<LocIdent, V>,
-    env1: E::Ref<'env>,
-    map2: &'a IndexMap<LocIdent, V>,
-    env2: E::Ref<'env>,
+    var_eq: VarEq,
+    map1: &IndexMap<LocIdent, V>,
+    env1: E::Ref<'_>,
+    map2: &IndexMap<LocIdent, V>,
+    env2: E::Ref<'_>,
 ) -> bool
 where
-    F: FnMut(&mut State, &'a V, E::Ref<'env>, &'a V, E::Ref<'env>) -> bool,
+    F: FnMut(&mut State, VarEq, &V, E::Ref<'_>, &V, E::Ref<'_>) -> bool,
 {
     map1.len() == map2.len()
         && map1.iter().all(|(id, v1)| {
             map2.get(id)
-                .map(|v2| f(state, v1, env1, v2, env2))
+                .map(|v2| f(state, var_eq, v1, env1, v2, env2))
                 .unwrap_or(false)
         })
 }
@@ -468,16 +561,17 @@ fn rows_as_set(erows: &UnifEnumRows) -> Option<HashSet<LocIdent>> {
 
 /// Check for contract equality between record fields. Fields are equal if they are both without a
 /// definition, or are both defined and their values are equal.
-fn contract_eq_fields<'env, 'a: 'env, E: TermEnvironment>(
+fn contract_eq_fields<E: TermEnvironment>(
     state: &mut State,
-    field1: &'a Field,
-    env1: E::Ref<'env>,
-    field2: &'a Field,
-    env2: E::Ref<'env>,
+    var_eq: VarEq,
+    field1: &Field,
+    env1: E::Ref<'_>,
+    field2: &Field,
+    env2: E::Ref<'_>,
 ) -> bool {
     match (&field1.value, &field2.value) {
         (Some(ref value1), Some(ref value2)) => {
-            contract_eq_bounded::<E>(state, value1, env1, value2, env2)
+            contract_eq_bounded::<E>(state, var_eq, value1, env1, value2, env2)
         }
         (None, None) => true,
         _ => false,
@@ -494,12 +588,13 @@ fn contract_eq_fields<'env, 'a: 'env, E: TermEnvironment>(
 /// the rigid type variables encountered have been introduced by `type_eq_bounded` itself. This is
 /// why we don't need unique identifiers that are distinct from the one used during typechecking,
 /// and we can just start from `0`.
-fn type_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
+fn type_eq_bounded<E: TermEnvironment>(
     state: &mut State,
-    ty1: &'a GenericUnifType<E>,
-    env1: E::Ref<'env>,
-    ty2: &'a GenericUnifType<E>,
-    env2: E::Ref<'env>,
+    var_eq: VarEq,
+    ty1: &GenericUnifType<E>,
+    env1: E::Ref<'_>,
+    ty2: &GenericUnifType<E>,
+    env2: E::Ref<'_>,
 ) -> bool {
     match (ty1, ty2) {
         (GenericUnifType::Concrete { typ: s1, .. }, GenericUnifType::Concrete { typ: s2, .. }) => {
@@ -519,13 +614,13 @@ fn type_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
                         type_fields: uty2,
                         flavour: attrs2,
                     },
-                ) if attrs1 == attrs2 => type_eq_bounded(state, uty1, env1, uty2, env2),
+                ) if attrs1 == attrs2 => type_eq_bounded(state, var_eq, uty1, env1, uty2, env2),
                 (TypeF::Array(uty1), TypeF::Array(uty2)) => {
-                    type_eq_bounded(state, uty1, env1, uty2, env2)
+                    type_eq_bounded(state, var_eq, uty1, env1, uty2, env2)
                 }
                 (TypeF::Arrow(s1, t1), TypeF::Arrow(s2, t2)) => {
-                    type_eq_bounded(state, s1, env1, s2, env2)
-                        && type_eq_bounded(state, t1, env1, t2, env2)
+                    type_eq_bounded(state, var_eq, s1, env1, s2, env2)
+                        && type_eq_bounded(state, var_eq, t1, env1, t2, env2)
                 }
                 (TypeF::Enum(uty1), TypeF::Enum(uty2)) => {
                     let rows1 = rows_as_set(uty1);
@@ -533,14 +628,15 @@ fn type_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
                     rows1.is_some() && rows2.is_some() && rows1 == rows2
                 }
                 (TypeF::Record(uty1), TypeF::Record(uty2)) => {
-                    fn type_eq_bounded_wrapper<'env, 'a: 'env, E: TermEnvironment>(
+                    fn type_eq_bounded_wrapper<E: TermEnvironment>(
                         state: &mut State,
-                        uty1: &'a &'a GenericUnifType<E>,
-                        env1: E::Ref<'env>,
-                        uty2: &'a &'a GenericUnifType<E>,
-                        env2: E::Ref<'env>,
+                        var_eq: VarEq,
+                        uty1: &&GenericUnifType<E>,
+                        env1: E::Ref<'_>,
+                        uty2: &&GenericUnifType<E>,
+                        env2: E::Ref<'_>,
                     ) -> bool {
-                        type_eq_bounded(state, *uty1, env1, *uty2, env2)
+                        type_eq_bounded(state, var_eq, *uty1, env1, *uty2, env2)
                     }
 
                     let map1 = rows_as_map(uty1);
@@ -548,12 +644,20 @@ fn type_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
 
                     map1.zip(map2)
                         .map(|(m1, m2)| {
-                            map_eq::<_, _, E>(type_eq_bounded_wrapper, state, &m1, env1, &m2, env2)
+                            map_eq::<_, _, E>(
+                                type_eq_bounded_wrapper,
+                                state,
+                                var_eq,
+                                &m1,
+                                env1,
+                                &m2,
+                                env2,
+                            )
                         })
                         .unwrap_or(false)
                 }
                 (TypeF::Flat(t1), TypeF::Flat(t2)) => {
-                    contract_eq_bounded::<E>(state, t1, env1, t2, env2)
+                    contract_eq_bounded::<E>(state, var_eq, t1, env1, t2, env2)
                 }
                 (
                     TypeF::Forall {
@@ -591,7 +695,7 @@ fn type_eq_bounded<'env, 'a: 'env, E: TermEnvironment>(
                         ),
                     };
 
-                    type_eq_bounded(state, &uty1_subst, env1, &uty2_subst, env2)
+                    type_eq_bounded(state, var_eq, &uty1_subst, env1, &uty2_subst, env2)
                 }
                 // We can't compare type variables without knowing what they are instantiated to,
                 // and all type variables should have been substituted at this point, so we bail
diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs
index e13cded5e5..8ef7d6c5a7 100644
--- a/core/src/typecheck/mod.rs
+++ b/core/src/typecheck/mod.rs
@@ -89,7 +89,7 @@ pub mod mk_uniftype;
 pub mod eq;
 pub mod unif;
 
-use eq::{SimpleTermEnvironment, TermEnvironment};
+use eq::{SimpleTermEnvironment, TermEnvironment, ToOwnedEnv};
 use error::*;
 use indexmap::IndexMap;
 use operation::{get_bop_type, get_nop_type, get_uop_type};
@@ -822,7 +822,7 @@ impl<E: TermEnvironment + Clone> GenericUnifType<E> {
     /// checking type equality involving contracts.
     pub fn from_type(ty: Type, env: E::Ref<'_>) -> Self {
         match ty.typ {
-            TypeF::Flat(t) => GenericUnifType::Contract(t, <E as TermEnvironment>::ref_to_owned(env)),
+            TypeF::Flat(t) => GenericUnifType::Contract(t, env.to_owned_env()),
             ty => GenericUnifType::concrete(ty.map(
                 |ty_| Box::new(GenericUnifType::from_type(*ty_, env)),
                 |rrows| GenericUnifRecordRows::from_record_rows(rrows, env),
diff --git a/core/src/typecheck/unif.rs b/core/src/typecheck/unif.rs
index 1c284fdc7b..cdbef5fa4c 100644
--- a/core/src/typecheck/unif.rs
+++ b/core/src/typecheck/unif.rs
@@ -1124,7 +1124,13 @@ impl Unify for UnifType {
                 Err(UnifError::WithConst(VarKindDiscriminant::Type, i, ty))
             }
             (UnifType::Contract(t1, env1), UnifType::Contract(t2, env2))
-                if eq::contract_eq::<SimpleTermEnvironment>(state.table.max_uvars_count(), &t1, &env1, &t2, &env2) =>
+                if eq::contract_eq::<SimpleTermEnvironment>(
+                    state.table.max_uvars_count(),
+                    &t1,
+                    &env1,
+                    &t2,
+                    &env2,
+                ) =>
             {
                 Ok(())
             }
diff --git a/utils/src/bench.rs b/utils/src/bench.rs
index 4e107f81c7..b3fb3e0f59 100644
--- a/utils/src/bench.rs
+++ b/utils/src/bench.rs
@@ -121,12 +121,14 @@ pub fn bench_terms<'r>(rts: Vec<Bench<'r>>) -> Box<dyn Fn(&mut Criterion) + 'r>
                             c_local.typecheck(id, &type_ctxt).unwrap();
                         } else {
                             c_local.prepare(id, &type_ctxt).unwrap();
+
                             VirtualMachine::new_with_cache(
                                 c_local,
                                 eval_cache.clone(),
                                 std::io::sink(),
                             )
-                            .eval(t, &eval_env)
+                            .with_initial_env(eval_env.clone())
+                            .eval(t)
                             .unwrap();
                         }
                     },
@@ -201,12 +203,14 @@ macro_rules! ncl_bench_group {
                                 c_local.typecheck(id, &type_ctxt).unwrap();
                             } else {
                                 c_local.prepare(id, &type_ctxt).unwrap();
+
                                 VirtualMachine::new_with_cache(
                                     c_local,
                                     eval_cache.clone(),
                                     std::io::sink()
                                 )
-                                .eval(t, &eval_env)
+                                .with_initial_env(eval_env.clone())
+                                .eval(t)
                                 .unwrap();
                             }
                         },

From d4172bd8aa0a208b686bfdade4d5de624e42cb79 Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Tue, 26 Sep 2023 18:27:17 +0200
Subject: [PATCH 04/14] Rename elision->dedup which is better descriptive

---
 core/src/eval/merge.rs     |  4 ++--
 core/src/eval/operation.rs |  2 +-
 core/src/term/mod.rs       | 16 +++++++++-------
 3 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/core/src/eval/merge.rs b/core/src/eval/merge.rs
index 9257988eb8..503f3a6a74 100644
--- a/core/src/eval/merge.rs
+++ b/core/src/eval/merge.rs
@@ -415,7 +415,7 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a LocIdent> + Clon
     let mut pending_contracts = pending_contracts1.revert_closurize(cache, env_final, env1.clone());
 
     for ctr2 in pending_contracts2.revert_closurize(cache, env_final, env2.clone()) {
-        RuntimeContract::push_elide(
+        RuntimeContract::push_dedup(
             initial_env,
             &mut pending_contracts,
             &env_final,
@@ -427,7 +427,7 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a LocIdent> + Clon
     Ok(Field {
         metadata: FieldMetadata {
             doc: merge_doc(metadata1.doc, metadata2.doc),
-            annotation: TypeAnnotation::combine_elide(metadata1.annotation, metadata2.annotation),
+            annotation: TypeAnnotation::combine_dedup(metadata1.annotation, metadata2.annotation),
             // If one of the record requires this field, then it musn't be optional. The
             // resulting field is optional iff both are.
             opt: metadata1.opt && metadata2.opt,
diff --git a/core/src/eval/operation.rs b/core/src/eval/operation.rs
index c4fab4ef4a..47736e2647 100644
--- a/core/src/eval/operation.rs
+++ b/core/src/eval/operation.rs
@@ -2132,7 +2132,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                         label: label.clone(),
                                     };
 
-                                crate::term::RuntimeContract::push_elide(
+                                crate::term::RuntimeContract::push_dedup(
                                     &self.initial_env,
                                     &mut field.pending_contracts,
                                     &term_original_env,
diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs
index ff49b1fc60..9e072652c2 100644
--- a/core/src/term/mod.rs
+++ b/core/src/term/mod.rs
@@ -325,27 +325,24 @@ impl RuntimeContract {
     /// Push a pending contract to a vector of contracts if the contract to add isn't already
     /// present in the vector, according to the notion of contract equality defined in
     /// [crate::typecheck::eq].
-    pub fn push_elide(
+    pub fn push_dedup(
         initial_env: &Environment,
         contracts: &mut Vec<RuntimeContract>,
         env1: &Environment,
         ctr: Self,
         env2: &Environment,
     ) {
-        // eprintln!("push_elide: ({})", ctr.contract);
         let envs1 = EvalEnvs {
             eval_env: env1,
             initial_env,
         };
 
         for c in contracts.iter() {
-            // eprintln!("- comparing against ({})", c.contract);
             let envs = EvalEnvs {
                 eval_env: env2,
                 initial_env,
             };
             if contract_eq::<EvalEnvs>(0, &c.contract, envs1, &ctr.contract, envs) {
-                // eprintln!("  -> found equal contract, eliding");
                 return;
             }
         }
@@ -610,10 +607,15 @@ impl TypeAnnotation {
         self.typ.is_none() && self.contracts.is_empty()
     }
 
+    /// **Warning**: the contract equality check used in this function behaves like syntactic
+    /// equality, and doesn't take the environment into account. It's unsound for execution (it
+    /// could equate contracts that are actually totally distinct), but we use it only to trim
+    /// accumulated contracts before pretty-printing. Do not use prior to any form of evaluation.
+    ///
     /// Same as [`Combine::combine`], but eliminate duplicate contracts. As there's no notion of
-    /// environment when combining annotations, we use an unsound contract equality checking, which
-    /// just compares things syntactically.
-    pub fn combine_elide(left: Self, right: Self) -> Self {
+    /// environment when considering mere annotations, we use an unsound contract equality checking
+    /// which correspond to compares contracts syntactically.
+    pub fn combine_dedup(left: Self, right: Self) -> Self {
         let mut contracts = left.contracts;
 
         let typ = match (left.typ, right.typ) {

From 11e1458a5a05090ee2843795fa3942ca1353b527 Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Tue, 26 Sep 2023 18:32:57 +0200
Subject: [PATCH 05/14] Fix clippy warning

---
 core/src/eval/merge.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/core/src/eval/merge.rs b/core/src/eval/merge.rs
index 503f3a6a74..72f8568b3f 100644
--- a/core/src/eval/merge.rs
+++ b/core/src/eval/merge.rs
@@ -418,9 +418,9 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a LocIdent> + Clon
         RuntimeContract::push_dedup(
             initial_env,
             &mut pending_contracts,
-            &env_final,
+            env_final,
             ctr2,
-            &env_final,
+            env_final,
         );
     }
 

From e0f846b0c2f3da42b47c1017bab5907b18795c58 Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Tue, 26 Sep 2023 18:49:42 +0200
Subject: [PATCH 06/14] Fix cargo doc warnings

---
 core/src/program.rs      | 2 +-
 core/src/term/mod.rs     | 6 +++---
 core/src/typecheck/eq.rs | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/core/src/program.rs b/core/src/program.rs
index 1d15f6f13b..43d5452f57 100644
--- a/core/src/program.rs
+++ b/core/src/program.rs
@@ -309,7 +309,7 @@ impl<EC: EvalCache> Program<EC> {
         self.vm.eval_deep(t).map_err(|e| e.into())
     }
 
-    /// Wrapper for [`query`].
+    /// Prepare for evaluation, then query the program for a field.
     pub fn query(&mut self, path: Option<String>) -> Result<Field, Error> {
         let rt = self.prepare_eval()?;
         let query_path = QueryPath::parse_opt(self.vm.import_resolver_mut(), path)?;
diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs
index 9e072652c2..8daf72aa18 100644
--- a/core/src/term/mod.rs
+++ b/core/src/term/mod.rs
@@ -612,9 +612,9 @@ impl TypeAnnotation {
     /// could equate contracts that are actually totally distinct), but we use it only to trim
     /// accumulated contracts before pretty-printing. Do not use prior to any form of evaluation.
     ///
-    /// Same as [`Combine::combine`], but eliminate duplicate contracts. As there's no notion of
-    /// environment when considering mere annotations, we use an unsound contract equality checking
-    /// which correspond to compares contracts syntactically.
+    /// Same as [`crate::combine::Combine`], but eliminate duplicate contracts. As there's no
+    /// notion of environment when considering mere annotations, we use an unsound contract
+    /// equality checking which correspond to compares contracts syntactically.
     pub fn combine_dedup(left: Self, right: Self) -> Self {
         let mut contracts = left.contracts;
 
diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index ef0856f32d..1f3f1fabc0 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -274,7 +274,7 @@ impl State {
 
 /// Different possible behavior for variables comparison variables.
 #[derive(Copy, Clone, PartialEq, Eq)]
-enum VarEq {
+pub enum VarEq {
     /// Use the environment to fetch the content of variables and compare them.
     Environment,
     /// Don't use an environment and simply compare variables by name. This is unsound, and should

From ca8e8b3789383c5d8d58c6fbe6fe2d914991e1af Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Tue, 26 Sep 2023 19:39:46 +0200
Subject: [PATCH 07/14] Cosmetic improvements

---
 core/src/term/mod.rs     |  9 +++++----
 core/src/typecheck/eq.rs | 35 +++++++++++++++++++----------------
 2 files changed, 24 insertions(+), 20 deletions(-)

diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs
index 8daf72aa18..bec643d2c7 100644
--- a/core/src/term/mod.rs
+++ b/core/src/term/mod.rs
@@ -26,7 +26,7 @@ use crate::{
     match_sharedterm,
     position::TermPos,
     typ::{Type, UnboundTypeVariableError},
-    typecheck::eq::{contract_eq, type_eq_noenv, EvalEnvs},
+    typecheck::eq::{contract_eq, type_eq_noenv, EvalEnvsRef},
 };
 
 use codespan::FileId;
@@ -332,17 +332,18 @@ impl RuntimeContract {
         ctr: Self,
         env2: &Environment,
     ) {
-        let envs1 = EvalEnvs {
+        let envs1 = EvalEnvsRef {
             eval_env: env1,
             initial_env,
         };
 
         for c in contracts.iter() {
-            let envs = EvalEnvs {
+            let envs = EvalEnvsRef {
                 eval_env: env2,
                 initial_env,
             };
-            if contract_eq::<EvalEnvs>(0, &c.contract, envs1, &ctr.contract, envs) {
+
+            if contract_eq::<EvalEnvsRef>(0, &c.contract, envs1, &ctr.contract, envs) {
                 return;
             }
         }
diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index 1f3f1fabc0..8856d03b04 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -67,16 +67,17 @@ pub trait ToOwnedEnv<Owned> {
 /// during evaluation.
 ///
 /// The evaluation environment holds [crate::eval::cache::CacheIndex]es, while the term environment
-/// used during typechecking is just maps identifiers to a pair `(RichTerm, Environment)`. To have
-/// an interface that works with both, `TermEnvironment::get_then` has to take a closure
-/// representing the continuation of the task to do with the result instead of merely returning it.
+/// used during typechecking just maps identifiers to a pair `(RichTerm, Environment)`. To have an
+/// interface that works with both, [TermEnvironment] provides [TermEnvironment::get_then], which
+/// has to take a closure representing the continuation of the task to do with the result instead
+/// of merely returning it.
 pub trait TermEnvironment: Clone {
     /// The representation of the environment is different during typechecking and evaluation. In
     /// particular, the evaluation's environment is actually a pair of environments (the initial
-    /// environment and the local environment), and thus the notion of owned environment of the
-    /// environment and of reference to it are not necessarily the obvious `Self` and `&Self`
+    /// environment and the local environment), and thus the notion of owned environment and
+    /// reference to the environment don't always map to the obvious `Self` and `&Self`
     /// respectively.
-    /// The trait abstract over it by defining a reference type and an owned type.
+    /// The trait abstract over thos notions by defining a reference type and an owned type.
     type Owned: Clone + PartialEq + Debug;
     type Ref<'a>: Copy + ToOwnedEnv<Self::Owned>;
 
@@ -138,7 +139,7 @@ impl std::iter::FromIterator<(Ident, (RichTerm, SimpleTermEnvironment))> for Sim
 }
 
 #[derive(Clone, Copy)]
-pub struct EvalEnvs<'a> {
+pub struct EvalEnvsRef<'a> {
     pub eval_env: &'a eval::Environment,
     pub initial_env: &'a eval::Environment,
 }
@@ -149,7 +150,7 @@ pub struct EvalEnvsOwned {
     pub initial_env: eval::Environment,
 }
 
-impl<'a> ToOwnedEnv<EvalEnvsOwned> for EvalEnvs<'a> {
+impl<'a> ToOwnedEnv<EvalEnvsOwned> for EvalEnvsRef<'a> {
     fn to_owned_env(self) -> EvalEnvsOwned {
         EvalEnvsOwned {
             eval_env: self.eval_env.clone(),
@@ -158,13 +159,13 @@ impl<'a> ToOwnedEnv<EvalEnvsOwned> for EvalEnvs<'a> {
     }
 }
 
-impl<'a> TermEnvironment for EvalEnvs<'a> {
-    type Ref<'b> = EvalEnvs<'b>;
+impl<'a> TermEnvironment for EvalEnvsRef<'a> {
+    type Ref<'b> = EvalEnvsRef<'b>;
     type Owned = EvalEnvsOwned;
 
-    fn get_then<F, T>(env: EvalEnvs<'_>, id: Ident, f: F) -> T
+    fn get_then<F, T>(env: EvalEnvsRef<'_>, id: Ident, f: F) -> T
     where
-        F: FnOnce(Option<(&RichTerm, EvalEnvs<'_>)>) -> T,
+        F: FnOnce(Option<(&RichTerm, EvalEnvsRef<'_>)>) -> T,
     {
         debug_assert!(
             env.eval_env.get(&id).or(env.initial_env.get(&id)).is_some(),
@@ -180,7 +181,7 @@ impl<'a> TermEnvironment for EvalEnvs<'a> {
         {
             Some(closure_ref) => f(Some((
                 &closure_ref.body,
-                EvalEnvs {
+                EvalEnvsRef {
                     eval_env: &closure_ref.env,
                     initial_env: env.initial_env,
                 },
@@ -272,13 +273,15 @@ impl State {
     }
 }
 
-/// Different possible behavior for variables comparison variables.
-#[derive(Copy, Clone, PartialEq, Eq)]
+/// Different possible behavior for variables comparison.
+#[derive(Copy, Clone, PartialEq, Eq, Default)]
 pub enum VarEq {
+    #[default]
     /// Use the environment to fetch the content of variables and compare them.
     Environment,
     /// Don't use an environment and simply compare variables by name. This is unsound, and should
-    /// only be used to deduplicate annotations for pretty-printing.
+    /// only be used to deduplicate annotations for pretty-printing. In this case, use
+    /// [NoEnvironment] as an environment.
     Direct,
 }
 

From bf0dc06612944eeef05d86140a8fdf1d5f3f9c66 Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Tue, 26 Sep 2023 20:00:55 +0200
Subject: [PATCH 08/14] Mention idempotency assumption in the manual

---
 doc/manual/contracts.md | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/doc/manual/contracts.md b/doc/manual/contracts.md
index 6a90167083..a43aa8c140 100644
--- a/doc/manual/contracts.md
+++ b/doc/manual/contracts.md
@@ -58,6 +58,29 @@ are available. `Dyn` is a contract that never fails.
 
 ## User-defined contracts
 
+### Preamble: idempotency
+
+As you will see in this section, Nickel contracts are more than mere boolean
+validators. They can sometimes modify the checked value for valid reasons
+exposed below. However, it's hard (if not impossible) to rightfully limit the
+expressive power of contracts to be *reasonable* with respect to modifications.
+
+For Nickel, the notion of reasonable modification is practically defined by
+idempotency. An idempotent contract is a contract which gives the same result if
+applied once or many times to the same value. That is, for any value,
+`MyContract` is idempotent if `value | MyContract` and `value | MyContract |
+MyContract` gives the same result. Idempotency sounds like a reasonable property
+for a contract, even if it can perform some normalization.
+
+**Nickel makes the assumption that all contracts - including user-defined
+contracts - are idempotent**, because the converse would be surprising for
+consumers of the contract and because this assumption enables important
+optimizations such as contract deduplication. **While non-idempotent contracts
+shouldn't wreak havoc on your program, they might lead to surprising results**,
+such as a change in behavior e.g. when refactoring a program to a new version
+that should be identical, typically because the deduplication optimization
+doesn't fire anymore.
+
 ### By hand
 
 The ability to check arbitrary properties is where run-time contracts really

From f0ef02802d2600f3ba7e6a98e46e7481b9bbb1c8 Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Wed, 27 Sep 2023 10:45:13 +0200
Subject: [PATCH 09/14] Update core/src/typecheck/eq.rs

Co-authored-by: Taeer Bar-Yam <Radvendii@users.noreply.github.com>
---
 core/src/typecheck/eq.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index 8856d03b04..5047dc6250 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -122,7 +122,7 @@ impl TermEnvironment for SimpleTermEnvironment {
 }
 
 impl<'a> AsRef<SimpleTermEnvironment> for &'a SimpleTermEnvironment {
-    fn as_ref(&self) -> &SimpleTermEnvironment {
+    fn as_ref(&self) -> &Self {
         self
     }
 }

From 455bfc078a883b07de2e56be70de6633b851fe12 Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Wed, 27 Sep 2023 11:07:03 +0200
Subject: [PATCH 10/14] Fix REPL query not working anymore

---
 core/src/repl/mod.rs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/core/src/repl/mod.rs b/core/src/repl/mod.rs
index cc9d1d48e1..51d46160d0 100644
--- a/core/src/repl/mod.rs
+++ b/core/src/repl/mod.rs
@@ -167,6 +167,7 @@ impl<EC: EvalCache> ReplImpl<EC> {
 
     fn eval_(&mut self, exp: &str, eval_full: bool) -> Result<EvalResult, Error> {
         self.vm.reset();
+
         let eval_function = if eval_full {
             eval::VirtualMachine::eval_full_closure
         } else {
@@ -304,6 +305,8 @@ impl<EC: EvalCache> Repl for ReplImpl<EC> {
     }
 
     fn query(&mut self, path: String) -> Result<Field, Error> {
+        self.vm.reset();
+
         let mut query_path = QueryPath::parse(self.vm.import_resolver_mut(), path)?;
 
         // remove(): this is safe because there is no such thing as an empty field path. If `path`
@@ -316,6 +319,10 @@ impl<EC: EvalCache> Repl for ReplImpl<EC> {
             .import_resolver_mut()
             .replace_string(SourcePath::ReplQuery, target.label().into());
 
+        self.vm
+            .import_resolver_mut()
+            .prepare(file_id, &self.env.type_ctxt)?;
+
         Ok(self.vm.query_closure(
             Closure {
                 body: self.vm.import_resolver().get_owned(file_id).unwrap(),

From 8612019e92d81f5f16e15199418284f4a87298ef Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Wed, 27 Sep 2023 11:49:02 +0200
Subject: [PATCH 11/14] Update core/src/typecheck/eq.rs

Co-authored-by: jneem <joeneeman@gmail.com>
---
 core/src/typecheck/eq.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index 5047dc6250..b5e94a41de 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -327,7 +327,7 @@ pub fn type_eq_noenv(var_uid: usize, t1: &Type, t2: &Type) -> bool {
 }
 
 /// Decide type equality on contracts in their respective environment and given the remaining gas
-/// `gas`.
+/// in `state`.
 fn contract_eq_bounded<E: TermEnvironment>(
     state: &mut State,
     var_eq: VarEq,

From 69cff47513db52a0edb29b02e97a992198ddc1d7 Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Wed, 27 Sep 2023 13:52:12 +0200
Subject: [PATCH 12/14] Formatting

---
 core/src/program.rs | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/core/src/program.rs b/core/src/program.rs
index 43d5452f57..5efb054094 100644
--- a/core/src/program.rs
+++ b/core/src/program.rs
@@ -22,7 +22,7 @@
 //! Each such value is added to the initial environment before the evaluation of the program.
 use crate::{
     cache::*,
-    error::{report, ColorOpt, Error, IntoDiagnostics, ParseError, EvalError, IOError},
+    error::{report, ColorOpt, Error, EvalError, IOError, IntoDiagnostics, ParseError},
     eval::{cache::Cache as EvalCache, VirtualMachine},
     identifier::LocIdent,
     label::Label,
@@ -266,7 +266,11 @@ impl<EC: EvalCache> Program<EC> {
         // generate a dummy file id).
         // We'll have to adapt `Label` and `MergeLabel` to be generated programmatically,
         // without referring to any source position.
-        Ok(mk_term::op2(BinaryOp::Merge(Label::default().into()), t, built_record))
+        Ok(mk_term::op2(
+            BinaryOp::Merge(Label::default().into()),
+            t,
+            built_record,
+        ))
     }
 
     /// Parse if necessary, typecheck and then evaluate the program.

From 76b188de0bfbde6a618a7f83ff689e124393e61e Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Wed, 27 Sep 2023 13:53:41 +0200
Subject: [PATCH 13/14] Fix clippy error

---
 core/src/typecheck/eq.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/core/src/typecheck/eq.rs b/core/src/typecheck/eq.rs
index b5e94a41de..1f20f8465e 100644
--- a/core/src/typecheck/eq.rs
+++ b/core/src/typecheck/eq.rs
@@ -122,7 +122,7 @@ impl TermEnvironment for SimpleTermEnvironment {
 }
 
 impl<'a> AsRef<SimpleTermEnvironment> for &'a SimpleTermEnvironment {
-    fn as_ref(&self) -> &Self {
+    fn as_ref(&self) -> Self {
         self
     }
 }

From b0469a75fe583849da14656fbd423fd48e51c746 Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@tweag.io>
Date: Thu, 28 Sep 2023 18:00:12 +0200
Subject: [PATCH 14/14] Update core/src/program.rs

Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>
---
 core/src/program.rs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/core/src/program.rs b/core/src/program.rs
index 5efb054094..b90234afae 100644
--- a/core/src/program.rs
+++ b/core/src/program.rs
@@ -234,8 +234,7 @@ impl<EC: EvalCache> Program<EC> {
             .clone())
     }
 
-    /// Retrieve the parsed term, typecheck it, and generate a fresh initial environment. Return
-    /// both.
+    /// Retrieve the parsed term, typecheck it, and generate a fresh initial environment.
     fn prepare_eval(&mut self) -> Result<RichTerm, Error> {
         // If there are no overrides, we avoid the boilerplate of creating an empty record and
         // merging it with the current program