Repository: tweag/nickel
Pull request #491 (2021-12-08 15:50:42)

Recursive overriding
Implement the recursive overriding of records, as detailed in #330 and along the lines of #103. This doesn't add merge priorities, merge functions, etc., but just implement the call-by-name semantics when merging recursive records:

```
({foo | default = 0, bar = foo + 1} & {foo = 2}).bar // Equals 3 after this PR
```

## Overview

This PR implements the following changes:
1. Add a `LetRev` node to the AST. `LetRev` acts as a normal `Let`, excepted that it allocates a revertible thunk when evaluated. The share normal form pass generates those `LetRev` instead of normal `Let` precisely for the fields of recursive records.

    To be honest, it's becoming clear at this point that we need to have at least two different ASTs, one straight out of the parser, and one for runtime, as those "syntax-only" and "runtime-only" constructs start to accumulate in the current single AST. However, it is out of scope for this issue. Also, `LetRev` is not so bad as for anything else but evaluation, it is strictly equivalent to a `Let`, so most changes are mechanical.
2. When merging two records, revert all the thunks inside the fields of the operands before performing the usual recursive merging. Once done, `merge` returns a `RecRecord` instead of a standard `Record`, such that when evaluated, the abstract machine builds a fresh recursive environment again (tying the knot).
3. Incidentally, I had to implement a simple optimization for `colsurize` that has been on the plate for a long time. It avoids dumbly generating nested closures when unnecessary. It is required for overriding as the indirections introduced by those nested closures mess with the creation of the recursive environment of `RecRecord`s generated by `merge`.



Patch:
diff --git a/examples/config-gcc/config-gcc.ncl b/examples/config-gcc/config-gcc.ncl
index a944eba9..238c166c 100644
--- a/examples/config-gcc/config-gcc.ncl
+++ b/examples/config-gcc/config-gcc.ncl
@@ -4,7 +4,7 @@ let GccFlag =
   // We only allow the following flags
   let available = ["W", "c", "S", "e", "o"] in
   fun label value =>
-  if builtins.is_str value then
+  if builtins.isStr value then
     if strings.length value > 0 &&
       lists.any (fun x => x == strings.substring 0 1 value) available then
       value
@@ -27,7 +27,7 @@ let GccFlag =
 let Path =
   let pattern = m#"^(.+)/([^/]+)$"#m in
   fun label value =>
-    if builtins.is_str value then
+    if builtins.isStr value then
       if strings.is_match pattern value then
         value
       else
@@ -36,7 +36,7 @@ let Path =
       contracts.blame_with "not a string" label in
 
 let SharedObjectFile = fun label value =>
-  if builtins.is_str value then
+  if builtins.isStr value then
     if strings.is_match m#"\.so$"#m value then
       value
     else
diff --git a/lsp/nls/src/linearization.rs b/lsp/nls/src/linearization.rs
index 37e5df03..2c143d1c 100644
--- a/lsp/nls/src/linearization.rs
+++ b/lsp/nls/src/linearization.rs
@@ -373,7 +373,7 @@ impl Linearizer<BuildingResource, (UnifTable, HashMap<usize, Ident>)> for Analys
 
         let id = id_gen.get();
         match term {
-            Term::Let(ident, _, _) | Term::Fun(ident, _) => {
+            Term::Let(ident, _, _, _) | Term::Fun(ident, _) => {
                 self.env
                     .insert(ident.to_owned(), lin.state.resource.linearization.len());
                 lin.push(LinearizationItem {
@@ -442,12 +442,10 @@ impl Linearizer<BuildingResource, (UnifTable, HashMap<usize, Ident>)> for Analys
                 self.record_fields =
                     Some((id + 1, field_names.into_iter().enumerate().rev().collect()));
             }
-
             Term::Op1(UnaryOp::StaticAccess(ident), _) => {
                 let x = self.access.get_or_insert(Vec::with_capacity(1));
                 x.push(ident.to_owned())
             }
-
             Term::MetaValue(meta) => {
                 // Notice 1: No push to lin
                 // Notice 2: we discard the encoded value as anything we
@@ -485,7 +483,6 @@ impl Linearizer<BuildingResource, (UnifTable, HashMap<usize, Ident>)> for Analys
                     })
                 }
             }
-
             other => {
                 debug!("Add wildcard item: {:?}", other);
 
diff --git a/src/eval.rs b/src/eval.rs
index 05ec7354..ff4c0426 100644
--- a/src/eval.rs
+++ b/src/eval.rs
@@ -96,7 +96,7 @@ use crate::{
     position::RawSpan,
     position::TermPos,
     stack::Stack,
-    term::{make as mk_term, BinaryOp, MetaValue, RichTerm, StrChunk, Term, UnaryOp},
+    term::{make as mk_term, BinaryOp, BindingType, MetaValue, RichTerm, StrChunk, Term, UnaryOp},
 };
 use codespan::FileId;
 use std::cell::{Ref, RefCell, RefMut};
@@ -127,13 +127,13 @@ pub struct ThunkData {
 
 /// The part of [ThunkData] responsible for storing the closure itself. It can either be:
 /// - A standard thunk, that is destructively updated once and for all
-/// - A reversible thunk, that can be restored to its original expression. Used to implement
+/// - A revertible thunk, that can be restored to its original expression. Used to implement
 /// recursive merging of records and overriding (see the [RFC
 /// overriding](https://github.com/tweag/nickel/pull/330))
 #[derive(Clone, Debug, PartialEq)]
 pub enum InnerThunkData {
     Standard(Closure),
-    Reversible {
+    Revertible {
         orig: Rc<Closure>,
         cached: Rc<Closure>,
     },
@@ -148,12 +148,12 @@ impl ThunkData {
         }
     }
 
-    /// Create new reversible thunk data.
+    /// Create new revertible thunk data.
     pub fn new_rev(orig: Closure) -> Self {
         let rc = Rc::new(orig);
 
         ThunkData {
-            inner: InnerThunkData::Reversible {
+            inner: InnerThunkData::Revertible {
                 orig: rc.clone(),
                 cached: rc,
             },
@@ -165,7 +165,7 @@ impl ThunkData {
     pub fn closure(&self) -> &Closure {
         match self.inner {
             InnerThunkData::Standard(ref closure) => closure,
-            InnerThunkData::Reversible { ref cached, .. } => cached,
+            InnerThunkData::Revertible { ref cached, .. } => cached,
         }
     }
 
@@ -173,7 +173,7 @@ impl ThunkData {
     pub fn closure_mut(&mut self) -> &mut Closure {
         match self.inner {
             InnerThunkData::Standard(ref mut closure) => closure,
-            InnerThunkData::Reversible { ref mut cached, .. } => Rc::make_mut(cached),
+            InnerThunkData::Revertible { ref mut cached, .. } => Rc::make_mut(cached),
         }
     }
 
@@ -181,7 +181,7 @@ impl ThunkData {
     pub fn into_closure(self) -> Closure {
         match self.inner {
             InnerThunkData::Standard(closure) => closure,
-            InnerThunkData::Reversible { orig, cached } => {
+            InnerThunkData::Revertible { orig, cached } => {
                 std::mem::drop(orig);
                 Rc::try_unwrap(cached).unwrap_or_else(|rc| (*rc).clone())
             }
@@ -192,27 +192,24 @@ impl ThunkData {
     pub fn update(&mut self, new: Closure) {
         match self.inner {
             InnerThunkData::Standard(ref mut closure) => *closure = new,
-            InnerThunkData::Reversible { ref mut cached, .. } => *cached = Rc::new(new),
+            InnerThunkData::Revertible { ref mut cached, .. } => *cached = Rc::new(new),
         }
 
         self.state = ThunkState::Evaluated;
     }
 
-    /// Create fresh unevaluated thunk data from `self`, restored to its original state before the
-    /// first update. For standard thunk data, the content is unchanged and the state is conserved: in
-    /// this case, `restore()` is the same as `clone()`.
-    pub fn restore(&self) -> Self {
+    /// Create fresh unevaluated thunk data from `self`, reverted to its original state before the
+    /// first update. For standard thunk data, the content is unchanged and the state is conserved:
+    /// in this case, `revert()` is the same as `clone()`.
+    pub fn revert(&self) -> Self {
         match self.inner {
-            InnerThunkData::Standard(ref closure) => ThunkData {
-                inner: InnerThunkData::Standard(closure.clone()),
-                state: self.state,
-            },
-            InnerThunkData::Reversible { ref orig, .. } => ThunkData {
-                inner: InnerThunkData::Reversible {
+            InnerThunkData::Standard(_) => self.clone(),
+            InnerThunkData::Revertible { ref orig, .. } => ThunkData {
+                inner: InnerThunkData::Revertible {
                     orig: Rc::clone(orig),
                     cached: Rc::clone(orig),
                 },
-                state: self.state,
+                state: ThunkState::Suspended,
             },
         }
     }
@@ -223,9 +220,9 @@ impl ThunkData {
 /// A thunk is a shared suspended computation. It is the primary device for the implementation of
 /// lazy evaluation.
 ///
-/// For the implementation of recursive merging, some thunks need to be reversible, in the sense
-/// that we must be able to restore the original expression before update. Those are called
-/// reversible thunks. Most expressions don't need reversible thunks as their evaluation will
+/// For the implementation of recursive merging, some thunks need to be revertible, in the sense
+/// that we must be able to revert to the original expression before update. Those are called
+/// revertible thunks. Most expressions don't need revertible thunks as their evaluation will
 /// always give the same result, but some others, such as the ones containing recursive references
 /// inside a record may be invalidated by merging, and thus need to store the unaltered original
 /// expression. Those aspects are mainly handled in [InnerThunkData].
@@ -248,7 +245,7 @@ impl Thunk {
         }
     }
 
-    /// Create a new reversible thunk.
+    /// Create a new revertible thunk.
     pub fn new_rev(closure: Closure, ident_kind: IdentKind) -> Self {
         Thunk {
             data: Rc::new(RefCell::new(ThunkData::new_rev(closure))),
@@ -308,12 +305,12 @@ impl Thunk {
         }
     }
 
-    /// Create a fresh unevaluated thunk from `self`, restored to its original state before the
+    /// Create a fresh unevaluated thunk from `self`, reverted to its original state before the
     /// first update. For a standard thunk, the content is unchanged and the state is conserved: in
-    /// this case, `restore()` is the same as `clone()`.
-    pub fn restore(&self) -> Self {
+    /// this case, `revert()` is the same as `clone()`.
+    pub fn revert(&self) -> Self {
         Thunk {
-            data: Rc::new(RefCell::new(self.data.borrow().restore())),
+            data: Rc::new(RefCell::new(self.data.borrow().revert())),
             ident_kind: self.ident_kind,
         }
     }
@@ -665,29 +662,6 @@ pub fn eval_full<R>(
     global_env: &Environment,
     resolver: &mut R,
 ) -> Result<RichTerm, EvalError>
-where
-    R: ImportResolver,
-{
-    eval_deep_closure(t0, global_env, resolver).map(|(term, env)| subst(term, global_env, &env))
-}
-
-/// Fully evaluates a Nickel term like `eval_full`, but does not substitute all variables.
-pub fn eval_deep<R>(
-    t0: RichTerm,
-    global_env: &Environment,
-    resolver: &mut R,
-) -> Result<RichTerm, EvalError>
-where
-    R: ImportResolver,
-{
-    eval_deep_closure(t0, global_env, resolver).map(|(term, _)| term)
-}
-
-fn eval_deep_closure<R>(
-    t0: RichTerm,
-    global_env: &Environment,
-    resolver: &mut R,
-) -> Result<(RichTerm, Environment), EvalError>
 where
     R: ImportResolver,
 {
@@ -704,6 +678,7 @@ where
         ),
     );
     eval_closure(Closure::atomic_closure(wrapper), global_env, resolver, true)
+        .map(|(term, env)| subst(term, global_env, &env))
 }
 
 /// Evaluate a Nickel Term, stopping when a meta value is encountered at the top-level without
@@ -826,12 +801,18 @@ where
                 );
                 Closure { body: t1, env }
             }
-            Term::Let(x, s, t) => {
+            Term::Let(x, s, t, btype) => {
                 let closure = Closure {
                     body: s,
                     env: env.clone(),
                 };
-                env.insert(x, Thunk::new(closure, IdentKind::Let));
+
+                let thunk = match btype {
+                    BindingType::Normal => Thunk::new(closure, IdentKind::Let),
+                    BindingType::Revertible => Thunk::new_rev(closure, IdentKind::Let),
+                };
+
+                env.insert(x, thunk);
                 Closure { body: t, env }
             }
             Term::Switch(exp, cases, default) => {
@@ -1182,11 +1163,11 @@ pub fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichT
             | v @ Term::Enum(_)
             | v @ Term::Import(_)
             | v @ Term::ResolvedImport(_) => RichTerm::new(v, pos),
-            Term::Let(id, t1, t2) => {
+            Term::Let(id, t1, t2, btype) => {
                 let t1 = subst_(t1, global_env, env, Cow::Borrowed(bound.as_ref()));
                 let t2 = subst_(t2, global_env, env, bound);
 
-                RichTerm::new(Term::Let(id, t1, t2), pos)
+                RichTerm::new(Term::Let(id, t1, t2, btype), pos)
             }
             p @ Term::LetPattern(..) => panic!("Pattern {:?} has not been transformed before evaluation", p),
             Term::App(t1, t2) => {
diff --git a/src/identifier.rs b/src/identifier.rs
index c9e5f16e..200e7346 100644
--- a/src/identifier.rs
+++ b/src/identifier.rs
@@ -11,6 +11,10 @@ pub struct Ident {
     pub pos: TermPos,
 }
 
+/// Special character used for generating fresh identifiers. It must be syntactically impossible to
+/// use to write in a standard Nickel program, to avoid name clashes.
+pub const GEN_PREFIX: char = '%';
+
 impl PartialOrd for Ident {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
         self.label.partial_cmp(&other.label)
@@ -63,6 +67,6 @@ impl Into<String> for Ident {
 
 impl Ident {
     pub fn is_generated(&self) -> bool {
-        self.label.starts_with('%')
+        self.label.starts_with(GEN_PREFIX)
     }
 }
diff --git a/src/merge.rs b/src/merge.rs
index 0b297428..6fe4fc2a 100644
--- a/src/merge.rs
+++ b/src/merge.rs
@@ -52,8 +52,7 @@
 //! - *Contract check*: merging a `Contract` or a `ContractDefault` with a simple value `t`
 //! evaluates to a contract check, that is an `Assume(..., t)`
 use crate::error::EvalError;
-use crate::eval::CallStack;
-use crate::eval::{Closure, Environment};
+use crate::eval::{CallStack, Closure, Environment};
 use crate::label::Label;
 use crate::position::TermPos;
 use crate::term::{make as mk_term, BinaryOp, Contract, MetaValue, RecordAttrs, RichTerm, Term};
@@ -85,9 +84,9 @@ impl Default for MergeMode {
 /// contract. It is important as `merge` is not commutative in this mode.
 pub fn merge(
     t1: RichTerm,
-    env1: Environment,
+    mut env1: Environment,
     t2: RichTerm,
-    env2: Environment,
+    mut env2: Environment,
     pos_op: TermPos,
     mode: MergeMode,
 ) -> Result<Closure, EvalError> {
@@ -322,7 +321,7 @@ pub fn merge(
         }
         // Merge put together the fields of records, and recursively merge
         // fields that are present in both terms
-        (Term::Record(m1, attrs1), Term::Record(m2, attrs2)) => {
+        (Term::Record(mut m1, attrs1), Term::Record(mut m2, attrs2)) => {
             /* Terms inside m1 and m2 may capture variables of resp. env1 and env2.  Morally, we
              * need to store closures, or a merge of closures, inside the resulting record.  We use
              * the same trick as in the evaluation of the operator DynExtend, and replace each such
@@ -330,7 +329,9 @@ pub fn merge(
              */
             let mut m = HashMap::new();
             let mut env = Environment::new();
-            let (mut left, mut center, mut right) = hashmap::split(m1, m2);
+            rev_thunks(m1.values_mut(), &mut env1);
+            rev_thunks(m2.values_mut(), &mut env2);
+            let (left, center, right) = hashmap::split(m1, m2);
 
             match mode {
                 MergeMode::Contract(mut lbl) if !attrs2.open && !left.is_empty() => {
@@ -343,15 +344,15 @@ pub fn merge(
                 _ => (),
             };
 
-            for (field, t) in left.drain() {
+            for (field, t) in left.into_iter() {
                 m.insert(field, t.closurize(&mut env, env1.clone()));
             }
 
-            for (field, t) in right.drain() {
+            for (field, t) in right.into_iter() {
                 m.insert(field, t.closurize(&mut env, env2.clone()));
             }
 
-            for (field, (t1, t2)) in center.drain() {
+            for (field, (t1, t2)) in center.into_iter() {
                 m.insert(
                     field,
                     merge_closurize(&mut env, t1, env1.clone(), t2, env2.clone()),
@@ -360,7 +361,7 @@ pub fn merge(
 
             Ok(Closure {
                 body: RichTerm::new(
-                    Term::Record(m, RecordAttrs::merge(attrs1, attrs2)),
+                    Term::RecRecord(m, Vec::new(), RecordAttrs::merge(attrs1, attrs2)),
                     pos_op.into_inherited(),
                 ),
                 env,
@@ -432,6 +433,22 @@ fn merge_closurize(
     body.closurize(env, local_env)
 }
 
+fn rev_thunks<'a, I: Iterator<Item = &'a mut RichTerm>>(map: I, env: &mut Environment) {
+    use crate::transformations::fresh_var;
+
+    for rt in map {
+        if let Term::Var(id) = rt.as_ref() {
+            // This create a fresh variable which is bound to a reverted copy of the original thunk
+            let reverted = env.get(&id).unwrap().revert();
+            let fresh_id = fresh_var();
+            env.insert(fresh_id.clone(), reverted);
+            *rt.term = Term::Var(fresh_id);
+        }
+        // Otherwise, if it is not a variable after the share normal form transformations, it
+        // should be a constant and we don't need to revert anything
+    }
+}
+
 pub mod hashmap {
     use std::collections::HashMap;
 
diff --git a/src/program.rs b/src/program.rs
index f111672a..5050b827 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -89,12 +89,6 @@ impl Program {
         eval::eval_full(t, &global_env, &mut self.cache).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, global_env) = self.prepare_eval()?;
-        eval::eval_deep(t, &global_env, &mut self.cache).map_err(|e| e.into())
-    }
-
     /// Wrapper for [`query`](./fn.query.html).
     pub fn query(&mut self, path: Option<String>) -> Result<Term, Error> {
         let global_env = self.cache.prepare_stdlib()?;
diff --git a/src/term.rs b/src/term.rs
index ee6982d9..4d91ff4d 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -63,7 +63,8 @@ pub enum Term {
 
     /// A let binding.
     #[serde(skip)]
-    Let(Ident, RichTerm, RichTerm),
+    Let(Ident, RichTerm, RichTerm, BindingType),
+    /// A destructuring let-binding.
     #[serde(skip)]
     LetPattern(Option<Ident>, Destruct, RichTerm, RichTerm),
     /// An application.
@@ -155,6 +156,21 @@ impl From<MetaValue> for Term {
     }
 }
 
+/// Type of let-binding. This only affects run-time behavior. Revertible bindings introduce
+/// revertible thunks at evaluation, which are devices used for the implementation of recursive
+/// records merging. See the [`merge`] and [`eval`] modules for more details.
+#[derive(Debug, Eq, PartialEq, Copy, Clone)]
+pub enum BindingType {
+    Normal,
+    Revertible,
+}
+
+impl Default for BindingType {
+    fn default() -> Self {
+        BindingType::Normal
+    }
+}
+
 #[derive(Debug, Default, Eq, PartialEq, Copy, Clone)]
 pub struct RecordAttrs {
     pub open: bool,
@@ -333,7 +349,7 @@ impl Term {
                     });
                 meta.value.iter_mut().for_each(func);
             }
-            Let(_, ref mut t1, ref mut t2)
+            Let(_, ref mut t1, ref mut t2, _)
             | LetPattern(_, _, ref mut t1, ref mut t2)
             | App(ref mut t1, ref mut t2)
             | Op2(_, ref mut t1, ref mut t2) => {
@@ -370,8 +386,8 @@ impl Term {
             Term::Sym(_) => Some("Sym"),
             Term::Wrapped(_, _) => Some("Wrapped"),
             Term::MetaValue(_) => Some("Metavalue"),
-            Term::Let(_, _, _)
-            | Term::LetPattern(_, _, _, _)
+            Term::Let(..)
+            | Term::LetPattern(..)
             | Term::App(_, _)
             | Term::Var(_)
             | Term::Switch(..)
@@ -446,8 +462,8 @@ impl Term {
             }
             Term::Var(id) => id.to_string(),
             Term::ParseError => String::from("<parse error>"),
-            Term::Let(_, _, _)
-            | Term::LetPattern(_, _, _, _)
+            Term::Let(..)
+            | Term::LetPattern(..)
             | Term::App(_, _)
             | Term::Switch(..)
             | Term::Op1(_, _)
@@ -498,8 +514,8 @@ impl Term {
             | Term::Record(..)
             | Term::List(_)
             | Term::Sym(_) => true,
-            Term::Let(_, _, _)
-            | Term::LetPattern(_, _, _, _)
+            Term::Let(..)
+            | Term::LetPattern(..)
             | Term::App(_, _)
             | Term::Var(_)
             | Term::Switch(..)
@@ -534,8 +550,8 @@ impl Term {
             | Term::Lbl(_)
             | Term::Enum(_)
             | Term::Sym(_) => true,
-            Term::Let(_, _, _)
-            | Term::LetPattern(_, _, _, _)
+            Term::Let(..)
+            | Term::LetPattern(..)
             | Term::Record(..)
             | Term::List(_)
             | Term::Fun(_, _)
@@ -921,11 +937,11 @@ impl RichTerm {
                     pos,
                 }
             }
-            Term::Let(id, t1, t2) => {
+            Term::Let(id, t1, t2, btype) => {
                 let t1 = t1.traverse(f, state, method)?;
                 let t2 = t2.traverse(f, state, method)?;
                 RichTerm {
-                    term: Box::new(Term::Let(id, t1, t2)),
+                    term: Box::new(Term::Let(id, t1, t2, btype)),
                     pos,
                 }
             }
@@ -1225,7 +1241,7 @@ pub mod make {
         T2: Into<RichTerm>,
         I: Into<Ident>,
     {
-        Term::Let(id.into(), t1.into(), t2.into()).into()
+        Term::Let(id.into(), t1.into(), t2.into(), BindingType::Normal).into()
     }
 
     pub fn let_pat<I, D, T1, T2>(id: Option<I>, pat: D, t1: T1, t2: T2) -> RichTerm
diff --git a/src/transformations.rs b/src/transformations.rs
index bfb3c9ba..2e84f774 100644
--- a/src/transformations.rs
+++ b/src/transformations.rs
@@ -33,8 +33,7 @@ pub mod desugar_destructuring {
     use super::{Ident, RichTerm, Term};
     use crate::destruct::{Destruct, Match};
     use crate::term::make::{op1, op2};
-    use crate::term::MetaValue;
-    use crate::term::{BinaryOp::DynRemove, UnaryOp::StaticAccess};
+    use crate::term::{BinaryOp::DynRemove, BindingType, MetaValue, UnaryOp::StaticAccess};
 
     /// Wrap the desugarized term in a meta value containing the "Record contract" needed to check
     /// the pattern exaustivity and also fill the default values (`?` operator) if not presents in the record.
@@ -73,6 +72,7 @@ pub mod desugar_destructuring {
                     x.clone(),
                     t_,
                     destruct_term(x.clone(), &pat, bind_open_field(x, &pat, body)),
+                    BindingType::Normal,
                 ),
                 pos,
             )
@@ -101,6 +101,7 @@ pub mod desugar_destructuring {
                 }
             }),
             body,
+            BindingType::Normal,
         )
         .into()
     }
@@ -116,6 +117,7 @@ pub mod desugar_destructuring {
                         id.clone(),
                         op1(StaticAccess(id.clone()), Term::Var(x.clone())),
                         t,
+                        BindingType::Normal,
                     ),
                     pos,
                 ),
@@ -167,7 +169,7 @@ pub mod share_normal_form {
     use super::fresh_var;
     use crate::identifier::Ident;
     use crate::position::TermPos;
-    use crate::term::{MetaValue, RichTerm, Term};
+    use crate::term::{BindingType, MetaValue, RichTerm, Term};
 
     /// Transform the top-level term of an AST to a share normal form, if it can.
     ///
@@ -197,7 +199,7 @@ pub mod share_normal_form {
                     })
                     .collect();
 
-                with_bindings(Term::Record(map, attrs), bindings, pos)
+                with_bindings(Term::Record(map, attrs), bindings, pos, BindingType::Normal)
             }
             Term::RecRecord(map, dyn_fields, attrs) => {
                 // When a recursive record is evaluated, all fields need to be turned to closures
@@ -206,11 +208,21 @@ pub mod share_normal_form {
                 // other constructors: it is not only about sharing, but also about the future
                 // evaluation of recursive records. Only constant are not required to be
                 // closurized.
+                //
+                // In theory, the variable case is one exception: if the field is already a bare
+                // variable, it seems useless to add one more indirection through a generated
+                // variable. However, it is currently fundamental for recursive record merging that
+                // the sare normal form transformation ensure the following post-condition: the
+                // fields of recursive records contain either a constant or a *generated* variable,
+                // but never a user-supplied variable directly (the former starts with a special
+                // marker). See comments inside [`RichTerm::closurize`] for more details.
                 let mut bindings = Vec::with_capacity(map.len());
 
                 let map = map
                     .into_iter()
                     .map(|(id, t)| {
+                        // CHANGE THIS CONDITION CAREFULLY. Doing so can break the post-condition
+                        // explained above.
                         if !t.as_ref().is_constant() {
                             let fresh_var = fresh_var();
                             let pos_t = t.pos;
@@ -236,7 +248,14 @@ pub mod share_normal_form {
                     })
                     .collect();
 
-                with_bindings(Term::RecRecord(map, dyn_fields, attrs), bindings, pos)
+                // Recursive records are the reason why we need revertible thunks, since when
+                // merged, we may have to revert the fields back to their original expression.
+                with_bindings(
+                    Term::RecRecord(map, dyn_fields, attrs),
+                    bindings,
+                    pos,
+                    BindingType::Revertible,
+                )
             }
             Term::List(ts) => {
                 let mut bindings = Vec::with_capacity(ts.len());
@@ -255,7 +274,7 @@ pub mod share_normal_form {
                     })
                     .collect();
 
-                with_bindings(Term::List(ts), bindings, pos)
+                with_bindings(Term::List(ts), bindings, pos, BindingType::Normal)
             }
             Term::MetaValue(mut meta @ MetaValue { value: Some(_), .. }) => {
                 if meta.value.as_ref().map(|t| should_share(&t.term)).unwrap() {
@@ -264,7 +283,7 @@ pub mod share_normal_form {
                     meta.value
                         .replace(RichTerm::new(Term::Var(fresh_var.clone()), t.pos));
                     let inner = RichTerm::new(Term::MetaValue(meta), pos);
-                    RichTerm::new(Term::Let(fresh_var, t, inner), pos)
+                    RichTerm::new(Term::Let(fresh_var, t, inner, BindingType::Normal), pos)
                 } else {
                     RichTerm::new(Term::MetaValue(meta), pos)
                 }
@@ -298,14 +317,17 @@ pub mod share_normal_form {
     /// Given the term `body` and bindings of identifiers to terms represented as a list of pairs
     /// `(id_1, term_1), .., (id_n, term_n)`, return the new term `let id_n = term_n in ... let
     /// id_1 = term_1 in body`.
-    fn with_bindings(body: Term, bindings: Vec<(Ident, RichTerm)>, pos: TermPos) -> RichTerm {
-        bindings.into_iter().fold(
-            RichTerm {
-                term: Box::new(body),
-                pos: pos.into_inherited(),
-            },
-            |acc, (id, t)| RichTerm::new(Term::Let(id, t, acc), pos),
-        )
+    fn with_bindings(
+        body: Term,
+        bindings: Vec<(Ident, RichTerm)>,
+        pos: TermPos,
+        btype: BindingType,
+    ) -> RichTerm {
+        bindings
+            .into_iter()
+            .fold(RichTerm::new(body, pos.into_inherited()), |acc, (id, t)| {
+                RichTerm::new(Term::Let(id, t, acc, btype), pos)
+            })
     }
 }
 
@@ -474,7 +496,9 @@ where
 
 /// Generate a new fresh variable which do not clash with user-defined variables.
 pub fn fresh_var() -> Ident {
-    format!("%{}", FreshVarCounter::next()).into()
+    use crate::identifier::GEN_PREFIX;
+
+    format!("{}{}", GEN_PREFIX, FreshVarCounter::next()).into()
 }
 
 /// Structures which can be packed together with their environment as a closure.
@@ -494,14 +518,67 @@ impl Closurizable for RichTerm {
     /// Generate a fresh variable, bind it to the corresponding closure `(t,with_env)` in `env`,
     /// and return this variable as a fresh term.
     fn closurize(self, env: &mut Environment, with_env: Environment) -> RichTerm {
+        // If the term is already a variable, we don't have to create a useless intermediate
+        // closure. We just transfer the original thunk to the new environment. This is not only an
+        // optimization: this is relied upon by recursive record merging when computing the
+        // fixpoint.
+        //
+        // More specifically, the evaluation of a recursive record patches the environment of each
+        // field with the thunks recursively referring to the other fields of the record. `eval`
+        // assumes that a recursive record field is either a constant or a generated variable whose
+        // thunks *immediately* contain the original unevaluated expression (both properties are
+        // true after the share normal form transformation and maintained when reverting thunks
+        // before merging recursive records).
+        //
+        // To maintain this invariant, `closurize` must NOT introduce an indirection through a
+        // variable, such as transforming:
+        //
+        // ```
+        // {foo = %1, bar = 1} in env %1 <- 1 + bar
+        // ```
+        //
+        // to:
+        //
+        // ```
+        // {foo = %2, bar = 1} in env %2 <- (%1 in env %1 <- 1 + bar)
+        // ```
+        //
+        // In this case, the evaluation of the recursive records will patch the outer environment
+        // instead of the inner one, giving:
+        //
+        // ```
+        // {foo = %2, bar = 1} in env %2 <- (%1 in env %1 <- 1 + bar), bar <- 1
+        // ```
+        //
+        // Then, evaluating `foo` would unduly raise an unbound identifier error.
+        //
+        //
+        // We currently only do this optimization for generated variables (introduced by the share
+        // normal form). We could do it for non-generated identifiers as well, but be we would be
+        // renaming user-supplied variables by gibberish generated names. It may hamper error
+        // reporting, so for the time being, we restrict ourselves to generated identifiers. Note
+        // that performing or not performing this optimization for user-supplied variables doesn't
+        // affect the invariant mentioned above, because the share normal form must ensure that the
+        // fields of a record all contain generated variables (or constant), but never
+        // user-supplied variables.
         let var = fresh_var();
         let pos = self.pos;
-        let closure = Closure {
-            body: self,
-            env: with_env,
+
+        let thunk = match self.as_ref() {
+            Term::Var(id) if id.is_generated() => with_env.get(&id).expect(&format!(
+                "Internal error(closurize) : generated identifier {} not found in the environment",
+                id
+            )),
+            _ => {
+                let closure = Closure {
+                    body: self,
+                    env: with_env,
+                };
+                Thunk::new(closure, IdentKind::Record)
+            }
         };
-        env.insert(var.clone(), Thunk::new(closure, IdentKind::Record));
 
+        env.insert(var.clone(), thunk);
         RichTerm::new(Term::Var(var), pos.into_inherited())
     }
 }
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index e2d85e52..a15536a4 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -628,7 +628,7 @@ fn type_check_<S, E>(
             unify(state, strict, ty, mk_typewrapper::dynamic())
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
-        Term::Let(x, re, rt) => {
+        Term::Let(x, re, rt, _) => {
             let ty_let = binding_type(re.as_ref(), &envs, state.table, strict);
             linearizer.retype_ident(lin, x, ty_let.clone());
             type_check_(


Test patch:
diff --git a/tests/examples.rs b/tests/examples.rs
index 0139b106..4b5ed2e7 100644
--- a/tests/examples.rs
+++ b/tests/examples.rs
@@ -8,7 +8,7 @@ fn eval_file(file: &str) -> Result<RichTerm, Error> {
     let mut path = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
     path.push(format!("examples/{}", file));
     let mut p = Program::new_from_file(path).expect("could not load file as a program");
-    p.eval_deep()
+    p.eval()
 }
 
 #[test]
diff --git a/tests/pass.rs b/tests/pass.rs
index df1970cd..ed813665 100644
--- a/tests/pass.rs
+++ b/tests/pass.rs
@@ -112,3 +112,8 @@ fn annot_parsing() {
 fn importing() {
     check_file("import.ncl");
 }
+
+#[test]
+fn overriding() {
+    check_file("overriding.ncl");
+}
diff --git a/tests/pass/overriding.ncl b/tests/pass/overriding.ncl
new file mode 100644
index 00000000..f05240ff
--- /dev/null
+++ b/tests/pass/overriding.ncl
@@ -0,0 +1,74 @@
+let Assert = contracts.from_predicate functions.id in
+
+[
+  {foo | default = 1} & {foo = 2} == {foo = 2},
+  {foo = 1 + 1, bar = foo + 1} == {foo = 2, bar = 3},
+
+  let r = {foo | default = 1 + 1, bar = foo + 1} in
+  builtins.deep_seq (r & {foo = 3}) r == {foo = 2, bar = 3},
+
+  let r = {foo | default = 1 + 1, bar = foo + 1} in
+  (r & {foo = 3}) == {foo = 3, bar = 4},
+
+  let r = {foo | default = 1 + 1, bar = foo + 1} in
+  builtins.deep_seq r (r & {foo = 3}) == {foo = 3, bar = 4},
+
+  let ext = 0 + 1 in
+  let r = {
+    foo | default = 1 + 1,
+    a = let inner = 0 in foo + ext + inner,
+    b = let inner = 1 in a + ext + inner,
+    c = let inner = 2 in b + ext + inner,
+  } in
+  builtins.deep_seq (r & {foo = 1 - 1}) r
+    == {foo = 2, a = 3, b = 5, c = 8},
+
+  let ext = 0 + 1 in
+  let r = {
+    foo | default = 1 + 1,
+    a = let inner = 0 in foo + ext + inner,
+    b = let inner = 1 in a + ext + inner,
+    c = let inner = 2 in b + ext + inner,
+  } in
+  builtins.deep_seq r (r & {foo = 1 - 1})
+    == {foo = 0, a = 1, b = 3, c = 6},
+
+  let nested = {
+    foo.bar.baz | default = 0,
+    some.nested = {
+      stuff = foo.bar.baz + 1,
+      other = stuff + 1,
+    },
+  } in
+  builtins.deep_seq (nested & {foo.bar.baz = 1}) nested
+    == {foo.bar.baz = 0, some.nested.stuff = 1, some.nested.other = 2},
+
+  let nested = {
+    foo.bar.baz | default = 0,
+    some.nested = {
+      stuff = foo.bar.baz + 1,
+      other = stuff + 1,
+    },
+  } in
+  builtins.deep_seq nested (nested & {foo.bar.baz = 1})
+    == {foo.bar.baz = 1, some.nested.stuff = 2, some.nested.other = 3},
+
+  let base = {foo | default = "a", bar = foo ++ "b"} in
+  let ext1 = base & {foo = "1"} in
+  let ext2 = base & {foo = "A"} in
+  (base.bar == "ab"
+  && ext1.bar == "1b"
+  && ext2.bar == "Ab")
+  |> builtins.deep_seq base
+  |> builtins.deep_seq ext1
+  |> builtins.deep_seq ext2,
+
+  // Test that the evaluation of a recursive record patches the right
+  // environment in some edge cases (when fields only contains a variable)
+  let foo = 1 in
+  let y = foo in
+  {bar = y, foo = 2}.bar == 1,
+  ({foo | default = 1, bar = foo} & {foo = 2}).bar == 2,
+  ({foo | default = 1, bar = foo, baz = bar} & {foo = 2}).baz == 2,
+]
+|> lists.foldl (fun next acc => (next | #Assert) && acc) true