Repository: tweag/nickel
Pull request #1086 (2023-01-30 11:47:07)

[RFC005] Lazy propagation
Follow-up of #990.

Implement the second part of RFC005, namely getting rid of eager cross application of contracts during merging, and implement lazy propagation instead. All the bogus examples from RFC005 now gives the desired result within this PR.

The idea and challenges are in fact quite similar to the ones of lazy array contracts (#809). We probably should use `%force%` instead of `%deep_seq%` even more. We also have the same potential performance issue that contract application aren't cached as long as we don't destruct a record (same happen with arrays):

```nickel
let r = {foo | Num = 1 + 1} in
r.foo + r.foo + r.foo
```

Here, the `Num` contract is applied lazily at each field access, and thus recomputed 3 times (the contract application, not `1 + 1` which is in its own thunk). Somehow, `1 + 1 | Num` doesn't have a proper intermediate thunk to be cached. However, this is not something very hard to solve (namely by introducing this intermediate level of thunk/cache). It's just postponed to future work.

In the end, the net diff is negative, and this PR gets rid of a lot of complexities from the merging function, transformation and the overall pipeline. Retrospectively, beside the user-centric motivations of RFC005, it also seems to be the better choice with respect to maintainability.


Patch:
diff --git a/.github/workflows/continuous-integration.yml b/.github/workflows/continuous-integration.yml
index 544422b3..ff93ed41 100644
--- a/.github/workflows/continuous-integration.yml
+++ b/.github/workflows/continuous-integration.yml
@@ -5,9 +5,6 @@ on:
       - master
   pull_request:
 
-concurrency:
-  group: ci-${{ github.ref }}
-  cancel-in-progress: true
 
 jobs:
   build-and-test:
diff --git a/src/eval/fixpoint.rs b/src/eval/fixpoint.rs
index e9314e79..4f150bb7 100644
--- a/src/eval/fixpoint.rs
+++ b/src/eval/fixpoint.rs
@@ -1,13 +1,56 @@
 //! Compute the fixpoint of a recursive record.
 use super::*;
 use crate::position::TermPos;
-use crate::term::{Traverse, TraverseOrder};
-use crate::types::{TypeF, Types};
+
+// Update the environment of a term by extending it with a recursive environment. In the general
+// case, the term is expected to be a variable pointing to the thunk to be patched. Otherwise, it's
+// considered to have no dependencies and is left untouched.
+//
+// This function achieve the same as `patch_field`, but is somehow lower-level, as it operates on a
+// general `RichTerm` instead of a `Field`. In practice, the patched term is either the value of a
+// field or one of its pending contract.
+fn patch_term<C: Cache>(
+    cache: &mut C,
+    term: &RichTerm,
+    rec_env: &[(Ident, CacheIndex)],
+    env: &Environment,
+) -> Result<(), EvalError> {
+    if let Term::Var(var_id) = &*term.term {
+        // TODO: Shouldn't be mutable, [`CBNCache`] abstraction is leaking.
+        let mut idx = env
+            .get(var_id)
+            .cloned()
+            .ok_or(EvalError::UnboundIdentifier(*var_id, term.pos))?;
+
+        cache.build_cached(&mut idx, rec_env);
+    };
+
+    Ok(())
+}
 
 /// Build a recursive environment from record bindings. For each field, `rec_env` either extracts
 /// the corresponding thunk from the environment in the general case, or create a closure on the
 /// fly if the field is a constant. The resulting environment is to be passed to the
 /// [`patch_field`] function.
+///
+/// # Pending contracts
+///
+/// Since the implementation of RFC005, contract are lazily applied at the level of record fields.
+/// Consider the following example:
+///
+/// ```nickel
+/// let Schema = {bar | default = "hello"} in
+///
+/// {
+///   foo | Schema = {},
+///   baz = foo.bar
+/// }
+/// ```
+///
+/// This program is valid and should output `{foo.bar = "hello", baz = "hello"}`. To make this
+/// happen, we have to ensure the pending contract `Schema` is applied to the recursive occurrence
+/// `foo` used in the definition `baz = foo.bar`. That is, we must apply pending contracts to their
+/// corresponding field when building the recursive environment.
 pub fn rec_env<'a, I: Iterator<Item = (&'a Ident, &'a Field)>, C: Cache>(
     cache: &mut C,
     bindings: I,
@@ -17,13 +60,13 @@ pub fn rec_env<'a, I: Iterator<Item = (&'a Ident, &'a Field)>, C: Cache>(
     bindings
         .map(|(id, field)| {
             if let Some(ref value) = field.value {
-                match value.as_ref() {
+                let idx = match value.as_ref() {
                     Term::Var(ref var_id) => {
                         let idx = env
                             .get(var_id)
                             .cloned()
                             .ok_or(EvalError::UnboundIdentifier(*var_id, value.pos))?;
-                        Ok((*id, idx))
+                        idx
                     }
                     _ => {
                         // If we are in this branch, `rt` must be a constant after the share normal form
@@ -33,12 +76,33 @@ pub fn rec_env<'a, I: Iterator<Item = (&'a Ident, &'a Field)>, C: Cache>(
                             body: value.clone(),
                             env: Environment::new(),
                         };
-                        Ok((
-                            *id,
-                            cache.add(closure, IdentKind::Record, BindingType::Normal),
-                        ))
+
+                        cache.add(closure, IdentKind::Record, BindingType::Normal)
                     }
-                }
+                };
+
+                // We now need to wrap the binding in a value with contracts applied.
+                // Pending contracts might use identifiers from the current record's environment,
+                // so we start from in the environment of the original record.
+                let mut final_env = env.clone();
+                let id_value = Ident::fresh();
+                final_env.insert(id_value, idx);
+
+                let with_ctr_applied = PendingContract::apply_all(
+                    RichTerm::new(Term::Var(id_value), value.pos),
+                    field.pending_contracts.iter().cloned(),
+                    value.pos,
+                );
+
+                let final_closure = Closure {
+                    body: with_ctr_applied,
+                    env: final_env,
+                };
+
+                Ok((
+                    *id,
+                    cache.add(final_closure, IdentKind::Record, BindingType::Normal),
+                ))
             } else {
                 let error = EvalError::MissingFieldDef {
                     id: *id,
@@ -81,23 +145,11 @@ pub fn patch_field<C: Cache>(
     env: &Environment,
 ) -> Result<(), EvalError> {
     if let Some(ref value) = field.value {
-        if let Term::Var(var_id) = &*value.term {
-            // TODO: Shouldn't be mutable, [`CBNCache`] abstraction is leaking.
-            let mut idx = env
-                .get(var_id)
-                .cloned()
-                .ok_or(EvalError::UnboundIdentifier(*var_id, value.pos))?;
-
-            cache.build_cached(&mut idx, rec_env);
-        }
-
-        // Thanks to the share normal form transformation, the content is either a constant or a
-        // variable. In the constant case, the environment is irrelevant and we don't have to do
-        // anything in the `else` case.
+        patch_term(cache, value, rec_env, env)?;
     }
 
-    // We must patch the contracts contained in the fields' metadata as well, since they can depend
-    // recursively on other fields, as in:
+    // We must patch the contracts contained in the fields' pending contracts as well, since they
+    // can depend recursively on other fields, as in:
     //
     // ```
     // let Variant = match {
@@ -113,32 +165,8 @@ pub fn patch_field<C: Cache>(
     // ```
     //
     // Here, `Variant` depends on `tag` recursively.
-    for labeled_ty in field.metadata.annotation.iter() {
-        // It's a bit sad to clone just to be able to call `traverse` here, but it would be also
-        // sad to reimplement the whole traversal just to operate on references. One hope is to
-        // use `Rc` for `Types` one day, instead of `Box`, so that cloning is cheap.
-        labeled_ty.types.clone().traverse(
-            &|ty: Types, cache: &mut C| -> Result<Types, EvalError> {
-                if let TypeF::Flat(contract) = &ty.0 {
-                    if let Term::Var(var_id) = &*contract.term {
-                        // TODO: Shouldn't be mutable, [`CBNCache`] abstraction is leaking.
-                        let mut idx = env
-                            .get(var_id)
-                            .cloned()
-                            .ok_or(EvalError::UnboundIdentifier(*var_id, contract.pos))?;
-
-                        cache.build_cached(&mut idx, rec_env);
-                    };
-                };
-
-                // Thanks to the share normal form transformation, the content is either a constant or a
-                // variable. In the constant case, the environment is irrelevant and we don't have to do
-                // anything in the `else` case.
-                Ok(ty)
-            },
-            cache,
-            TraverseOrder::TopDown,
-        )?;
+    for pending_contract in field.pending_contracts.iter() {
+        patch_term(cache, &pending_contract.contract, rec_env, env)?;
     }
 
     Ok(())
diff --git a/src/eval/merge.rs b/src/eval/merge.rs
index 55e4095d..d4a2bb07 100644
--- a/src/eval/merge.rs
+++ b/src/eval/merge.rs
@@ -56,11 +56,9 @@ use crate::error::{EvalError, IllegalPolymorphicTailAction};
 use crate::label::Label;
 use crate::position::TermPos;
 use crate::term::{
-    make as mk_term,
     record::{self, Field, FieldDeps, FieldMetadata, RecordAttrs, RecordData},
-    BinaryOp, LabeledType, RichTerm, SharedTerm, Term, TypeAnnotation,
+    BinaryOp, RichTerm, SharedTerm, Term, TypeAnnotation,
 };
-use crate::types::{TypeF, Types};
 use std::collections::HashMap;
 
 /// Merging mode. Merging is used both to combine standard data and to apply contracts defined as
@@ -347,69 +345,6 @@ pub fn merge<C: Cache>(
     }
 }
 
-/// Apply a series of contracts to the value of a field as well as the necessary saturation (see
-/// [saturate]) and closurize operations.
-///
-/// Both the contract and the field are saturated, and the result is closurized. The result is
-/// revertible if either the contract or the record is, with the union of their
-/// dependencies.
-///
-/// # Parameters
-///
-/// - the value is given by `value1` in its environment `env1`
-/// - the contracts are given as an iterator `it2` together with their (common) environment `env2`
-fn cross_apply_contracts<'a, 'b, C: Cache, I: DoubleEndedIterator<Item = &'b Ident> + Clone>(
-    cache: &mut C,
-    value1: RichTerm,
-    env1: Environment,
-    mut it2: impl Iterator<Item = &'a LabeledType>,
-    env2: &Environment,
-    deps2: FieldDeps,
-    fields: &I,
-) -> Result<Closure, EvalError> {
-    // The environment of `%assume% ctr1 (%assume% ctr2 (... field)...)`. `ctr` and `field` will be saturated, ie of the form
-    // `%head% field1 .. fieldn`.
-    let mut local_env = Environment::new();
-
-    let pos = value1.pos.into_inherited();
-    let combined_deps = field_deps(cache, &value1, &env1)?.union(deps2);
-
-    // Produce the concrete sequence of application of the `assume` primop to the contract argument.
-    let value_saturated = value1.saturate(cache, &mut local_env, &env1, fields.clone())?;
-    let body = it2.try_fold(value_saturated, |acc, ctr| -> Result<RichTerm, EvalError> {
-        let ty_saturated = ctr
-            .types
-            .clone()
-            .saturate(cache, &mut local_env, env2, fields.clone())
-            .unwrap();
-        Ok(mk_term::assume(ty_saturated, ctr.label.clone(), acc).map(|rt| rt.with_pos(pos))?)
-    })?;
-
-    // We closurize the final result in a new thunk with appropriate dependencies and
-    // revertibility.
-    let closure = Closure {
-        body,
-        env: local_env,
-    };
-    let mut final_env = Environment::new();
-    let fresh_var = Ident::fresh();
-
-    // new_rev takes care of not creating a revertible thunk if the dependencies are empty.
-    final_env.insert(
-        fresh_var,
-        cache.add(
-            closure,
-            IdentKind::Record,
-            BindingType::Revertible(combined_deps),
-        ),
-    );
-
-    Ok(Closure {
-        body: RichTerm::from(Term::Var(fresh_var)),
-        env: final_env,
-    })
-}
-
 /// Take two record fields in their respective environment and combine both their metadata and
 /// values. Apply the required saturate, revert or closurize operation, including on the final
 /// field returned.
@@ -428,102 +363,55 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a Ident> + Clone>(
     let Field {
         metadata: metadata1,
         value: value1,
+        pending_contracts: pending_contracts1,
     } = field1;
     let Field {
         metadata: metadata2,
         value: value2,
+        pending_contracts: pending_contracts2,
     } = field2;
 
-    // Cross-application (in the process of being removed, see RFC005)
-    //
-    // If:
-    // 1. field1 has a value
-    // 2. field2 has a contract
-    // 3. The priorities (or the fact that field2's value is not defined) are such that
-    //    field1's value will be used in the final value
-    //
-    // Then, we apply field2's contracts to field1. This creates a new value and a new
-    // intermediate environment.
-    let (value1, val_env1) = match (value1, metadata2.annotation.first()) {
-        (Some(v1), Some(fst_ctr))
-            if (metadata1.priority >= metadata2.priority || value2.is_none()) =>
-        {
-            let Closure { body, env } = cross_apply_contracts(
-                cache,
-                v1,
-                env1.clone(),
-                metadata2.annotation.iter(),
-                &env2,
-                ty_field_deps(cache, &fst_ctr.types, &env2).unwrap(),
-                &fields,
-            )?;
-            (Some(body), env)
-        }
-        (v1, _) => (v1, env1.clone()),
-    };
-
-    // Cross-application (in the process of being removed, see RFC005)
-    //
-    // Dually, we cross apply meta1's contracts to meta2's value.
-    let (value2, val_env2) = match (value2, metadata1.annotation.first()) {
-        (Some(v2), Some(fst_ctr))
-            if (metadata2.priority >= metadata1.priority || value1.is_none()) =>
-        {
-            let Closure { body, env } = cross_apply_contracts(
-                cache,
-                v2,
-                env2.clone(),
-                metadata1.annotation.iter(),
-                &env1,
-                ty_field_deps(cache, &fst_ctr.types, &env1)?,
-                &fields,
-            )?;
-            (Some(body), env)
-        }
-        (v2, _) => (v2, env2.clone()),
-    };
-
     // Selecting either meta1's value, meta2's value, or the merge of the two values,
     // depending on which is defined and respective priorities.
     let (value, priority) = match (value1, value2) {
         (Some(t1), Some(t2)) if metadata1.priority == metadata2.priority => (
-            Some(
-                fields_merge_closurize(cache, env_final, t1, &val_env1, t2, &val_env2, fields)
-                    .unwrap(),
-            ),
+            Some(fields_merge_closurize(cache, env_final, t1, &env1, t2, &env2, fields).unwrap()),
             metadata1.priority,
         ),
         (Some(t1), _) if metadata1.priority > metadata2.priority => (
-            Some(t1.revert_closurize(cache, env_final, val_env1.clone())),
+            Some(t1.revert_closurize(cache, env_final, env1.clone())),
             metadata1.priority,
         ),
         (Some(t1), None) => (
-            Some(t1.revert_closurize(cache, env_final, val_env1.clone())),
+            Some(t1.revert_closurize(cache, env_final, env1.clone())),
             metadata1.priority,
         ),
         (_, Some(t2)) if metadata2.priority > metadata1.priority => (
-            Some(t2.revert_closurize(cache, env_final, val_env2.clone())),
+            Some(t2.revert_closurize(cache, env_final, env2.clone())),
             metadata2.priority,
         ),
         (None, Some(t2)) => (
-            Some(t2.revert_closurize(cache, env_final, val_env2.clone())),
+            Some(t2.revert_closurize(cache, env_final, env2.clone())),
             metadata2.priority,
         ),
         (None, None) => (None, Default::default()),
         _ => unreachable!(),
     };
 
-    let mut annot1 = metadata1
-        .annotation
-        .revert_closurize(cache, env_final, env1.clone());
-    let mut annot2 = metadata2
-        .annotation
-        .revert_closurize(cache, env_final, env2.clone());
-
-    // If both have type annotations, we arbitrarily choose the first one. At this point we are
-    // evaluating, and types annotations and contracts make no difference operationnally. Even for
-    // a query, it's strange to show multiple static types. So if both are set, we turn types2 to a
-    // contract and keep type1 as the main type annotation.
+    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())
+            .into_iter(),
+    );
+
+    // Annotation aren't used anymore at runtime. We still accumulate them to answer metadata
+    // queries, but we don't need to e.g. closurize or revert them.
+    let mut annot1 = metadata1.annotation;
+    let mut annot2 = metadata2.annotation;
+
+    // If both have type annotations, we arbitrarily choose the first one as the type annotation
+    // for the resulting field. This doesn't make any difference operationally.
     let types = match (annot1.types.take(), annot2.types.take()) {
         (Some(ctr1), Some(ctr2)) => {
             annot1.contracts.push(ctr2);
@@ -537,6 +425,7 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a Ident> + Clone>(
         .into_iter()
         .chain(annot2.contracts.into_iter())
         .collect();
+
     let metadata = FieldMetadata {
         doc: merge_doc(metadata1.doc, metadata2.doc),
         annotation: TypeAnnotation { types, contracts },
@@ -546,7 +435,11 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a Ident> + Clone>(
         priority,
     };
 
-    Ok(Field { metadata, value })
+    Ok(Field {
+        metadata,
+        value,
+        pending_contracts,
+    })
 }
 
 /// Merge two optional documentations.
@@ -555,9 +448,9 @@ fn merge_doc(doc1: Option<String>, doc2: Option<String>) -> Option<String> {
     doc1.or(doc2)
 }
 
-/// See [crate::eval::lazy::Thunk::saturate]. Saturation is a transformation on recursive thunks that is
-/// used when we must combine different values with different recursive dependencies (say, the two
-/// values of fields being merged) into one expression.
+/// See [crate::eval::lazy::Thunk::saturate]. Saturation is a transformation on recursive thunks
+/// that is used when we must combine different values with different recursive dependencies (say,
+/// the two values of fields being merged) into one expression.
 ///
 /// Saturation is first and foremost a transformation of terms, but like
 /// [crate::transform::Closurizable], it can be applied to other types that contain terms, hence
@@ -599,32 +492,6 @@ impl Saturate for RichTerm {
     }
 }
 
-impl Saturate for Types {
-    fn saturate<'a, I: DoubleEndedIterator<Item = &'a Ident> + Clone, C: Cache>(
-        self,
-        cache: &mut C,
-        env: &mut Environment,
-        local_env: &Environment,
-        fields: I,
-    ) -> Result<Types, EvalError> {
-        match self {
-            // Currently, either:
-            // 1. the contract is part of a recursive records and MUST have been closurized as a
-            //    revertible thunk during program transformation:
-            Types(TypeF::Flat(ctr)) if matches!(ctr.as_ref(), Term::Var(id) if id.is_generated()) => {
-                Ok(Types(TypeF::Flat(
-                    ctr.saturate(cache, env, local_env, fields)?,
-                )))
-            }
-            // 2. or it is the contract of a non-recursive record (e.g. the contract generated by
-            //    pattern matching or desugaring `foo.bar.baz = value`) and doesn't need to be
-            //    saturated at all, as it can't be recursive. This contract can still capture
-            //    variables from the environment, so we need to closurize it nontheless
-            ty => Ok(ty.closurize(cache, env, local_env.clone())),
-        }
-    }
-}
-
 /// Return the dependencies of a field when represented as a `RichTerm`.
 fn field_deps<C: Cache>(
     cache: &C,
@@ -641,21 +508,6 @@ fn field_deps<C: Cache>(
     }
 }
 
-/// Return the dependencies of a contract when represented as a `Types`.
-fn ty_field_deps<C: Cache>(
-    cache: &C,
-    ty: &Types,
-    local_env: &Environment,
-) -> Result<FieldDeps, EvalError> {
-    if let Types(TypeF::Flat(ctr)) = ty {
-        field_deps(cache, ctr, local_env)
-    } else {
-        Ok(FieldDeps::empty())
-    }
-}
-
-/// Return the dependencies of a contract when represented as a `Type`.
-
 /// Take the current environment, two fields with their local environment, and return a term which
 /// is the merge of the two fields, closurized in the provided final environment.
 ///
@@ -676,7 +528,7 @@ fn fields_merge_closurize<'a, I: DoubleEndedIterator<Item = &'a Ident> + Clone,
 ) -> Result<RichTerm, EvalError> {
     let mut local_env = Environment::new();
 
-    let combined_deps = field_deps(cache, &t1, env1)?.union(field_deps(cache, &t2, env2).unwrap());
+    let combined_deps = field_deps(cache, &t1, env1)?.union(field_deps(cache, &t2, env2)?);
     let body = RichTerm::from(Term::Op2(
         BinaryOp::Merge(),
         t1.saturate(cache, &mut local_env, env1, fields.clone())?,
@@ -722,7 +574,6 @@ impl RevertClosurize for RichTerm {
         with_env: Environment,
     ) -> RichTerm {
         if let Term::Var(id) = self.as_ref() {
-            //TODO: actually use the cache after rebase
             // This create a fresh variable which is bound to a reverted copy of the original thunk
             let reverted = cache.revert(with_env.get(id).unwrap());
             let fresh_id = Ident::fresh();
@@ -743,83 +594,43 @@ impl RevertClosurize for Field {
         env: &mut Environment,
         with_env: Environment,
     ) -> Field {
-        let metadata = self.metadata.revert_closurize(cache, env, with_env.clone());
         let value = self
             .value
-            .map(|value| value.revert_closurize(cache, env, with_env));
+            .map(|value| value.revert_closurize(cache, env, with_env.clone()));
 
-        Field { metadata, value }
-    }
-}
+        let pending_contracts = self
+            .pending_contracts
+            .revert_closurize(cache, env, with_env);
 
-impl RevertClosurize for Types {
-    fn revert_closurize<C: Cache>(
-        self,
-        cache: &mut C,
-        env: &mut Environment,
-        with_env: Environment,
-    ) -> Types {
-        match self {
-            // Currently, either:
-            // 1. the contract is part of a recursive records and MUST have been closurized as a
-            //    revertible thunk during program transformation:
-            Types(TypeF::Flat(ctr)) if matches!(ctr.as_ref(), Term::Var(id) if id.is_generated()) => {
-                Types(TypeF::Flat(ctr.revert_closurize(cache, env, with_env)))
-            }
-            // 2. or it is the contract of a non-recursive record (e.g. the contract generated by
-            //    pattern matching or desugaring `foo.bar.baz = value`) and doesn't need to be
-            //    saturated at all, as it can't be recursive. This contract can still capture
-            //    variables from the environment, so we need to closurize it nontheless
-            ty => ty.closurize(cache, env, with_env),
+        Field {
+            metadata: self.metadata,
+            value,
+            pending_contracts,
         }
     }
 }
 
-impl RevertClosurize for LabeledType {
+impl RevertClosurize for PendingContract {
     fn revert_closurize<C: Cache>(
         self,
         cache: &mut C,
         env: &mut Environment,
         with_env: Environment,
-    ) -> LabeledType {
-        LabeledType {
-            types: self.types.revert_closurize(cache, env, with_env),
-            label: self.label,
-        }
+    ) -> PendingContract {
+        self.map_contract(|ctr| ctr.revert_closurize(cache, env, with_env))
     }
 }
 
-impl RevertClosurize for TypeAnnotation {
+impl RevertClosurize for Vec<PendingContract> {
     fn revert_closurize<C: Cache>(
         self,
         cache: &mut C,
         env: &mut Environment,
         with_env: Environment,
-    ) -> TypeAnnotation {
-        let types = self
-            .types
-            .map(|ty| ty.revert_closurize(cache, env, with_env.clone()));
-        let contracts = self
-            .contracts
-            .into_iter()
-            .map(|labeled_ty| labeled_ty.revert_closurize(cache, env, with_env.clone()))
-            .collect();
-
-        TypeAnnotation { types, contracts }
-    }
-}
-
-impl RevertClosurize for FieldMetadata {
-    fn revert_closurize<C: Cache>(
-        self,
-        cache: &mut C,
-        env: &mut Environment,
-        with_env: Environment,
-    ) -> FieldMetadata {
-        FieldMetadata {
-            annotation: self.annotation.revert_closurize(cache, env, with_env),
-            ..self
-        }
+    ) -> Vec<PendingContract> {
+        self.into_iter()
+            .map(|pending_contract| pending_contract.revert_closurize(cache, env, with_env.clone()))
+            .collect()
     }
 }
 
diff --git a/src/eval/mod.rs b/src/eval/mod.rs
index 751bdd38..30317d23 100644
--- a/src/eval/mod.rs
+++ b/src/eval/mod.rs
@@ -228,16 +228,24 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     if let Some(Field {
                         metadata: metadata_next,
                         value: mut value_next,
+                        pending_contracts,
                     }) = next_field.take()
                     {
                         // We evaluate the fields' value, either to handle the next ident of the
                         // path, or to show the value if we are treating the last ident of the path
+
                         value_next = value_next
                             .map(|value| -> Result<RichTerm, EvalError> {
+                                let pos_value = value.pos;
+                                let value_with_ctr = PendingContract::apply_all(
+                                    value,
+                                    pending_contracts.into_iter(),
+                                    pos_value,
+                                );
                                 let (new_value, new_env) = self.eval_closure(
                                     Closure {
-                                        body: value,
-                                        env: std::mem::take(&mut env),
+                                        body: value_with_ctr,
+                                        env: env.clone(),
                                     },
                                     initial_env,
                                 )?;
@@ -250,6 +258,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                         field = Field {
                             metadata: metadata_next.clone(),
                             value: value_next,
+                            pending_contracts: Default::default(),
                         };
                     } else {
                         return Err(EvalError::FieldMissing(
@@ -530,11 +539,22 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     //instead of `match` in the main eval loop, if possible
                     let static_part = RichTerm::new(Term::Record(record.clone()), pos);
 
-                    // Transform the static part `{stat1 = val1, ..., statn = valn}` and the dynamic
-                    // part `{exp1 = dyn_val1, ..., expm = dyn_valm}` to a sequence of extensions
-                    // `%record_insert% exp1 (... (%record_insert% expn {stat1 = val1, ..., statn = valn} dyn_valn)) dyn_val1`
-                    // The `dyn_val` are given access to the recursive environment, but the recursive
-                    // environment only contains the static fields, and not the dynamic fields.
+                    // Transform the static part `{stat1 = val1, ..., statn = valn}` and the
+                    // dynamic part `{exp1 = dyn_val1, ..., expm = dyn_valm}` to a sequence of
+                    // extensions
+                    //
+                    // ```
+                    // %record_insert% exp1
+                    //   (...
+                    //     (%record_insert% expn {stat1 = val1, ..., statn = valn} dyn_valn)
+                    //   ...)
+                    //   dyn_val1
+                    //
+                    // ```
+                    //
+                    // The `dyn_val` are given access to the recursive environment, but the
+                    // recursive environment only contains the static fields, and not the dynamic
+                    // fields.
                     let extended = dyn_fields
                         .iter()
                         .try_fold::<_, _, Result<RichTerm, EvalError>>(
@@ -549,10 +569,21 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                 fixpoint::patch_field(&mut self.cache, field, &rec_env, &env)?;
 
                                 let ext_kind = field.extension_kind();
-                                let Field { metadata, value } = field;
+                                let Field {
+                                    metadata,
+                                    value,
+                                    pending_contracts,
+                                } = field;
 
+                                //TODO[LAZYPROP]: we should probably closurize the pending
+                                //contracts. It seems to work currently, but looks a bit fragile
+                                //with respect to refactoring/changes.
                                 let extend = mk_term::op2(
-                                    BinaryOp::DynExtend(metadata.clone(), ext_kind),
+                                    BinaryOp::DynExtend {
+                                        metadata: metadata.clone(),
+                                        pending_contracts: pending_contracts.clone(),
+                                        ext_kind,
+                                    },
                                     name_as_term.clone(),
                                     acc,
                                 );
@@ -574,7 +605,6 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                         env,
                     }
                 }
-                // Unwrapping of enriched terms
                 Term::ResolvedImport(id) => {
                     if let Some(t) = self.import_resolver.get(*id) {
                         Closure::atomic_closure(t)
@@ -640,16 +670,22 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                 }
                 // For now, we simply erase annotations at runtime. They aren't accessible anyway
                 // (as opposed to field metadata) and don't change the operational semantics, as
-                // long as we generate the corresponding contract application at one point
-                // (currently ahead-of-time during program transformations).
+                // long as we generate the corresponding contract application when consuming it.
                 //
                 // The situation could change if we want to implement optimizations such as
                 // avoiding repeated contract application. Annotations could then be a good way of
                 // remembering which contracts have been applied to a value.
-                Term::Annotated(_, inner) => Closure {
-                    body: inner.clone(),
-                    env,
-                },
+                Term::Annotated(annot, inner) => {
+                    let contracts = annot.as_pending_contracts()?;
+                    let pos = inner.pos;
+                    let inner_with_ctr =
+                        PendingContract::apply_all(inner.clone(), contracts.into_iter(), pos);
+
+                    Closure {
+                        body: inner_with_ctr,
+                        env,
+                    }
+                }
                 // Continuation of operations and thunk update
                 _ if self.stack.is_top_idx() || self.stack.is_top_cont() => {
                     clos = Closure {
diff --git a/src/eval/operation.rs b/src/eval/operation.rs
index db68bd5c..e4a937a0 100644
--- a/src/eval/operation.rs
+++ b/src/eval/operation.rs
@@ -28,7 +28,7 @@ use crate::{
         BinaryOp, MergePriority, NAryOp, PendingContract, RecordExtKind, RichTerm, SharedTerm,
         StrChunk, Term, UnaryOp,
     },
-    transform::{apply_contracts::apply_contracts, Closurizable},
+    transform::Closurizable,
 };
 
 use md5::digest::Digest;
@@ -454,25 +454,19 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
             },
             UnaryOp::StaticAccess(id) => {
                 if let Term::Record(record) = &*t {
-                    match record.fields.get(&id) {
-                        Some(Field {
-                            value: Some(value), ..
-                        }) => {
+                    // We have to apply potentially pending contracts. Right now, this
+                    // means that repeated field access will re-apply the contract again
+                    // and again, which is not optimal. The same thing happens with array
+                    // contracts. There are several way to improve this, but this is left
+                    // as future work.
+                    match record
+                        .get_value_with_ctrs(&id)
+                        .map_err(|err| err.into_eval_err(pos, pos_op))?
+                    {
+                        Some(value) => {
                             self.call_stack.enter_field(id, pos, value.pos, pos_op);
-                            Ok(Closure {
-                                body: value.clone(),
-                                env,
-                            })
+                            Ok(Closure { body: value, env })
                         }
-                        Some(Field {
-                            value: None,
-                            metadata,
-                        }) => Err(EvalError::MissingFieldDef {
-                            id,
-                            metadata: metadata.clone(),
-                            pos_record: pos,
-                            pos_access: pos_op,
-                        }),
                         None => Err(EvalError::FieldMissing(
                             id.into_label(),
                             String::from("(.)"),
@@ -559,7 +553,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                             let ts = ts
                                 .into_iter()
                                 .map(|t| {
-                                    let t_with_ctrs = apply_contracts(
+                                    let t_with_ctrs = PendingContract::apply_all(
                                         t,
                                         attrs.pending_contracts.iter().cloned(),
                                         pos.into_inherited(),
@@ -661,7 +655,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                             let f_as_var = f.body.closurize(&mut self.cache, &mut env, f.env);
 
                             // As for `ArrayMap` (see above), we closurize the content of fields
-                            let record = record.map_fields_without_optionals(&mut self.cache, &mut shared_env, &env, |id, t| {
+                            let record = record.map_values_closurize(&mut self.cache, &mut shared_env, &env, |id, t| {
                                 let pos = t.pos.into_inherited();
 
                                 mk_app!(f_as_var.clone(), mk_term::string(id.label()), t)
@@ -718,6 +712,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                         let pos_record = pos;
                         let pos_access = pos_op;
                         let defined = record
+                            // into_iter_without_opts applies pending contracts as well
                             .into_iter_without_opts()
                             .collect::<Result<Vec<_>, _>>()
                             .map_err(|missing_def_err| {
@@ -746,7 +741,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                         let terms =
                             seq_terms(
                                 ts.into_iter().map(|t| {
-                                    let t_with_ctr = apply_contracts(
+                                    let t_with_ctr = PendingContract::apply_all(
                                         t,
                                         attrs.pending_contracts.iter().cloned(),
                                         pos.into_inherited(),
@@ -774,7 +769,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
             UnaryOp::ArrayHead() => {
                 if let Term::Array(ts, attrs) = &*t {
                     if let Some(head) = ts.get(0) {
-                        let head_with_ctr = apply_contracts(
+                        let head_with_ctr = PendingContract::apply_all(
                             head.clone(),
                             attrs.pending_contracts.iter().cloned(),
                             pos.into_inherited(),
@@ -1188,7 +1183,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                         Term::Record(record) if !record.fields.is_empty() => {
                             let mut shared_env = Environment::new();
 
-                            let record = record.map_fields_without_optionals(&mut self.cache, &mut shared_env, &env, |id, t| {
+                            let record = record.map_values_closurize(&mut self.cache, &mut shared_env, &env, |id, t| {
                                 let stack_elem = Some(callstack::StackElem::Field {
                                     id,
                                     pos_record: pos,
@@ -1216,7 +1211,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                 .map(|t| {
                                     mk_term::op1(
                                         UnaryOp::Force(None),
-                                        apply_contracts(
+                                        PendingContract::apply_all(
                                             t,
                                             attrs.pending_contracts.iter().cloned(),
                                             pos.into_inherited(),
@@ -1909,11 +1904,16 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
             BinaryOp::DynAccess() => match_sharedterm! {t1, with {
                     Term::Str(id) => {
                         if let Term::Record(record) = &*t2 {
-                            match record.get_value(&Ident::from(&id)).map_err(|missing_field_err| missing_field_err.into_eval_err(pos2, pos_op))? {
+                            // We have to apply potential pending contracts. Right now, this
+                            // means that repeated field access will re-apply the contract again
+                            // and again, which is not optimal. The same thing happens with array
+                            // contracts. There are several way to improve this, but this is left
+                            // as future work.
+                            match record.get_value_with_ctrs(&Ident::from(&id)).map_err(|missing_field_err| missing_field_err.into_eval_err(pos2, pos_op))? {
                                 Some(value) => {
                                     self.call_stack.enter_field(Ident::from(id), pos2, value.pos, pos_op);
                                     Ok(Closure {
-                                        body: value.clone(),
+                                        body: value,
                                         env: env2,
                                     })
                                 }
@@ -1951,7 +1951,11 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     ))
                 }
             },
-            BinaryOp::DynExtend(metadata, extension_kind) => {
+            BinaryOp::DynExtend {
+                metadata,
+                pending_contracts,
+                ext_kind,
+            } => {
                 if let Term::Str(id) = &*t1 {
                     match_sharedterm! {t2, with {
                             Term::Record(record) => {
@@ -1959,7 +1963,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
 
                                 // If a defined value is expected for this field, it must be
                                 // provided as an additional argument, so we pop it from the stack
-                                let value = if let RecordExtKind::WithValue = extension_kind {
+                                let value = if let RecordExtKind::WithValue = ext_kind {
                                     let (value_closure, _) = self
                                         .stack
                                         .pop_arg(&self.cache)
@@ -1972,10 +1976,10 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                     None
                                 };
 
-                                match fields.insert(Ident::from(id), Field {value, metadata }) {
+                                match fields.insert(Ident::from(id), Field {value, metadata, pending_contracts }) {
                                     //TODO: what to do on insertion where an empty optional field
                                     //exists? Temporary: we fail with existing field exception
-                                    Some(t) => Err(EvalError::Other(format!("insert: tried to extend a record with the field {}, but it already exists", id), pos_op)),
+                                    Some(t) => Err(EvalError::Other(format!("insert: tried to extend a record with the field {id}, but it already exists"), pos_op)),
                                     _ => Ok(Closure {
                                         body: Term::Record(RecordData { fields, ..record }).into(),
                                         env: env2,
@@ -2016,6 +2020,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                     | Some(Field {
                                         value: None,
                                         metadata: FieldMetadata { opt: true, ..},
+                                        ..
                                       }) =>
                                     {
                                         Err(EvalError::FieldMissing(
@@ -2137,12 +2142,12 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                     .filter(|ctr| !ctrs_left.contains(ctr) && !ctrs_common.contains(ctr));
 
                                 ts.extend(ts1.into_iter().map(|t|
-                                    apply_contracts(t, ctrs_left.iter().cloned(), pos1)
+                                    PendingContract::apply_all(t, ctrs_left.iter().cloned(), pos1)
                                     .closurize(&mut self.cache, &mut env, env1.clone())
                                 ));
 
                                 ts.extend(ts2.into_iter().map(|t|
-                                    apply_contracts(t, ctrs_right.clone(), pos2)
+                                    PendingContract::apply_all(t, ctrs_right.clone(), pos2)
                                     .closurize(&mut self.cache, &mut env, env2.clone())
                                 ));
 
@@ -2189,7 +2194,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     } else if *n < 0.0 || n_int >= ts.len() {
                         Err(EvalError::Other(format!("elemAt: index out of bounds. Expected a value between 0 and {}, got {}", ts.len(), n), pos_op))
                     } else {
-                        let elem_with_ctr = apply_contracts(
+                        let elem_with_ctr = PendingContract::apply_all(
                             ts.get(n_int).unwrap().clone(),
                             attrs.pending_contracts.iter().cloned(),
                             pos1.into_inherited(),
@@ -3106,18 +3111,36 @@ fn eq<C: Cache>(
                         (
                             Field {
                                 value: Some(value1),
+                                pending_contracts: pending_contracts1,
                                 ..
                             },
                             Field {
                                 value: Some(value2),
+                                pending_contracts: pending_contracts2,
                                 ..
                             },
-                        ) => Some(Ok((value1, value2))),
+                        ) => {
+                            let pos1 = value1.pos;
+                            let pos2 = value2.pos;
+
+                            let value1_with_ctr = PendingContract::apply_all(
+                                value1,
+                                pending_contracts1.into_iter(),
+                                pos1,
+                            );
+                            let value2_with_ctr = PendingContract::apply_all(
+                                value2,
+                                pending_contracts2.into_iter(),
+                                pos2,
+                            );
+                            Some(Ok((value1_with_ctr, value2_with_ctr)))
+                        }
                         (Field { value: None, .. }, Field { value: None, .. }) => None,
                         (
                             Field {
                                 value: value1 @ None,
                                 metadata,
+                                ..
                             },
                             Field { value: Some(_), .. },
                         )
@@ -3129,6 +3152,7 @@ fn eq<C: Cache>(
                             Field {
                                 value: None,
                                 metadata,
+                                ..
                             },
                         ) => {
                             let pos_record = if value1.is_none() { pos1 } else { pos2 };
@@ -3142,6 +3166,7 @@ fn eq<C: Cache>(
                         }
                     })
                     .collect();
+
                 Ok(gen_eqs(cache, eqs?.into_iter(), env, env1, env2))
             }
         }
@@ -3158,21 +3183,15 @@ fn eq<C: Cache>(
                 .into_iter()
                 .map(|t| {
                     let pos = t.pos.into_inherited();
-                    apply_contracts(t, a1.pending_contracts.iter().cloned(), pos).closurize(
-                        cache,
-                        &mut shared_env1,
-                        env1.clone(),
-                    )
+                    PendingContract::apply_all(t, a1.pending_contracts.iter().cloned(), pos)
+                        .closurize(cache, &mut shared_env1, env1.clone())
                 })
                 .collect::<Vec<_>>()
                 .into_iter()
                 .zip(l2.into_iter().map(|t| {
                     let pos = t.pos.into_inherited();
-                    apply_contracts(t, a2.pending_contracts.iter().cloned(), pos).closurize(
-                        cache,
-                        &mut shared_env2,
-                        env2.clone(),
-                    )
+                    PendingContract::apply_all(t, a2.pending_contracts.iter().cloned(), pos)
+                        .closurize(cache, &mut shared_env2, env2.clone())
                 }))
                 .collect::<Vec<_>>();
 
@@ -3215,8 +3234,17 @@ fn eq<C: Cache>(
     }
 }
 
-trait RecordDataExt {
-    fn map_fields_without_optionals<F, C: Cache>(
+trait RecordDataExt: Sized {
+    /// Returns the record resulting from:
+    ///
+    /// 1. Filtering out any field which is an empty optional
+    /// 2. Appplying the pending contracts to each fields
+    /// 3. Applying the provided function
+    /// 4. Closurizing each result into the shared environment.
+    ///
+    /// Because we applied the pending contracts in 2., they are dropped in the result: all fields
+    /// have an empty set of pending contracts.
+    fn map_values_closurize<F, C: Cache>(
         self,
         cache: &mut C,
         shared_env: &mut Environment,
@@ -3224,19 +3252,11 @@ trait RecordDataExt {
         f: F,
     ) -> Result<Self, record::MissingFieldDefError>
     where
-        F: FnMut(Ident, RichTerm) -> RichTerm,
-        Self: Sized;
+        F: FnMut(Ident, RichTerm) -> RichTerm;
 }
 
 impl RecordDataExt for RecordData {
-    /// Returns the record resulting from applying the provided function
-    /// to each field, and removing any field which is an empty optional
-    /// in the provided environment. The resulting values are then closurized
-    /// into the shared environment.
-    ///
-    /// Note that `f` is taken as `mut` in order to allow it to mutate
-    /// external state while iterating.
-    fn map_fields_without_optionals<F, C: Cache>(
+    fn map_values_closurize<F, C: Cache>(
         self,
         cache: &mut C,
         shared_env: &mut Environment,
@@ -3251,15 +3271,25 @@ impl RecordDataExt for RecordData {
             .into_iter()
             .filter_map(|(id, field)| {
                 (!field.is_empty_optional()).then(|| {
-                    let value = field.value.map(|value| f(id, value)).ok_or(
-                        record::MissingFieldDefError {
+                    let value = field
+                        .value
+                        .map(|value| {
+                            let pos = value.pos;
+                            let value_with_ctrs = PendingContract::apply_all(
+                                value,
+                                field.pending_contracts.iter().cloned(),
+                                pos,
+                            );
+                            f(id, value_with_ctrs)
+                        })
+                        .ok_or(record::MissingFieldDefError {
                             id,
                             metadata: field.metadata.clone(),
-                        },
-                    )?;
+                        })?;
 
                     let field = Field {
                         value: Some(value),
+                        pending_contracts: Vec::new(),
                         ..field
                     }
                     .closurize(cache, shared_env, env.clone());
diff --git a/src/parser/grammar.lalrpop b/src/parser/grammar.lalrpop
index 955a24f0..30c53afe 100644
--- a/src/parser/grammar.lalrpop
+++ b/src/parser/grammar.lalrpop
@@ -58,7 +58,7 @@ use crate::{
     identifier::Ident,
     destruct::{Match, LastMatch, Destruct},
     term::{
-        *, 
+        *,
         record::{RecordAttrs, Field, FieldMetadata},
         array::Array,
         make as mk_term,
@@ -383,7 +383,7 @@ RecordField: FieldDef = {
 
         let field = match (ann, t) {
             (Some(FieldExtAnnot { metadata, rec_force: false, rec_default: false }), None) => {
-                Field { value: None, metadata }
+                Field { value: None, metadata, ..Default::default() }
             }
             (Some(ann), Some(value)) => {
                 ann.attach_term(value)
@@ -487,6 +487,7 @@ DefaultAnnot: Field = "?" <t: Term> => Field {
         ..Default::default()
     },
     value: Some(t),
+    ..Default::default()
 };
 
 Ident: Ident = <l:@L> <i: "identifier"> <r:@R> =>
@@ -590,7 +591,7 @@ MultilineStaticString: String = DelimitedStaticString<"m%\"","\"%"> => {
     let chunks: Vec<StrChunk<RichTerm>> = vec![StrChunk::Literal(<>)];
     match strip_indent(chunks).pop().unwrap() {
         StrChunk::Literal(s) => s,
-        // We build 
+        // We build
         _ => unreachable!(),
     }
 };
@@ -828,10 +829,11 @@ BOpPre: BinaryOp = {
     "pow" => BinaryOp::Pow(),
     "str_split" => BinaryOp::StrSplit(),
     "str_contains" => BinaryOp::StrContains(),
-    "record_insert" => BinaryOp::DynExtend(
-        FieldMetadata::default(),
-        RecordExtKind::WithValue,
-    ),
+    "record_insert" => BinaryOp::DynExtend {
+        ext_kind: RecordExtKind::WithValue,
+        metadata: Default::default(),
+        pending_contracts: Default::default(),
+    },
     "record_remove" => BinaryOp::DynRemove(),
 }
 
diff --git a/src/parser/uniterm.rs b/src/parser/uniterm.rs
index f5969257..9ad67120 100644
--- a/src/parser/uniterm.rs
+++ b/src/parser/uniterm.rs
@@ -191,6 +191,9 @@ impl UniRecord {
                             opt: false,
                             priority: MergePriority::Neutral,
                         },
+                    // At this stage, this field should always be empty. It's a run-time thing, and
+                    // is only filled during program transformation.
+                    pending_contracts: _,
                 } if contracts.is_empty() => Ok(RecordRows(RecordRowsF::Extend {
                     row: RecordRow {
                         id,
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index 2d0f5179..d28e55e8 100644
--- a/src/parser/utils.rs
+++ b/src/parser/utils.rs
@@ -245,6 +245,7 @@ impl AttachTerm<Field> for FieldMetadata {
         Field {
             value: Some(rt),
             metadata: self,
+            pending_contracts: Default::default(),
         }
     }
 }
@@ -303,11 +304,13 @@ pub fn combine_match_annots(
             let Field {
                 value: default_value,
                 metadata: default_metadata,
+                pending_contracts,
             } = default.unwrap_or_default();
 
             Field {
                 value: default_value,
                 metadata: Annot::combine(anns.unwrap_or_default(), default_metadata),
+                pending_contracts,
             }
         }
         (None, None) => {
@@ -370,6 +373,7 @@ impl AttachTerm<Field> for FieldExtAnnot {
         Field {
             value,
             metadata: self.metadata,
+            pending_contracts: Default::default(),
         }
     }
 }
@@ -519,7 +523,13 @@ fn merge_fields(field1: Field, field2: Field) -> Field {
 
     let metadata = FieldMetadata::flatten(field1.metadata, field2.metadata);
 
-    Field { value, metadata }
+    // At this stage, pending contracts aren't filled nor meaningful, and should all be empty.
+    debug_assert!(field1.pending_contracts.is_empty() && field2.pending_contracts.is_empty());
+    Field {
+        value,
+        metadata,
+        pending_contracts: field1.pending_contracts,
+    }
 }
 
 /// Make a span from parser byte offsets.
diff --git a/src/pretty.rs b/src/pretty.rs
index c30e0e9e..42ec8a25 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -315,6 +315,7 @@ where
                 .append(allocator.space())
                 .append(allocator.as_string(id))
                 .append(allocator.space()),
+            Force(_) => allocator.text("%force%").append(allocator.space()),
             op => allocator
                 .text(format!("%{:?}%", op).to_lowercase())
                 .append(allocator.space()),
@@ -385,6 +386,7 @@ where
                                             priority: MergePriority::Bottom,
                                             ..
                                         },
+                                    ..
                                 } => allocator
                                     .text("?")
                                     .append(allocator.space())
diff --git a/src/repl/query_print.rs b/src/repl/query_print.rs
index 37d02ab2..48364a14 100644
--- a/src/repl/query_print.rs
+++ b/src/repl/query_print.rs
@@ -250,6 +250,7 @@ fn write_query_result_<R: QueryPrinter>(
                     ..
                 },
             value: Some(t),
+            ..
         } if selected_attrs.default => {
             renderer.write_metadata(out, "default", &t.as_ref().shallow_repr())?;
             found = true;
@@ -261,6 +262,7 @@ fn write_query_result_<R: QueryPrinter>(
                     ..
                 },
             value: Some(t),
+            ..
         } if selected_attrs.value => {
             renderer.write_metadata(out, "priority", &format!("{}", n))?;
             renderer.write_metadata(out, "value", &t.as_ref().shallow_repr())?;
diff --git a/src/term/mod.rs b/src/term/mod.rs
index 399867ff..be4efdc3 100644
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@@ -237,6 +237,54 @@ impl PendingContract {
     pub fn new(contract: RichTerm, label: Label) -> Self {
         PendingContract { contract, label }
     }
+
+    /// Map a function over the term representing the underlying contract.
+    pub fn map_contract<F>(self, f: F) -> Self
+    where
+        F: FnOnce(RichTerm) -> RichTerm,
+    {
+        PendingContract {
+            contract: f(self.contract),
+            ..self
+        }
+    }
+
+    /// Apply a series of pending contracts to a given term.
+    pub fn apply_all<I>(rt: RichTerm, contracts: I, pos: TermPos) -> RichTerm
+    where
+        I: Iterator<Item = Self>,
+    {
+        use crate::mk_app;
+
+        contracts.fold(rt, |acc, ctr| {
+            mk_app!(
+                make::op2(BinaryOp::Assume(), ctr.contract, Term::Lbl(ctr.label)).with_pos(pos),
+                acc
+            )
+            .with_pos(pos)
+        })
+    }
+}
+
+impl Traverse<RichTerm> for PendingContract {
+    fn traverse<F, S, E>(self, f: &F, state: &mut S, order: TraverseOrder) -> Result<Self, E>
+    where
+        F: Fn(RichTerm, &mut S) -> Result<RichTerm, E>,
+    {
+        let contract = self.contract.traverse(f, state, order)?;
+        Ok(PendingContract { contract, ..self })
+    }
+}
+
+impl std::convert::TryFrom<LabeledType> for PendingContract {
+    type Error = UnboundTypeVariableError;
+
+    fn try_from(labeled_ty: LabeledType) -> Result<Self, Self::Error> {
+        Ok(PendingContract::new(
+            labeled_ty.types.contract()?,
+            labeled_ty.label,
+        ))
+    }
 }
 
 /// The attributes of a let binding.
@@ -456,6 +504,14 @@ impl TypeAnnotation {
                 .join(",")
         })
     }
+
+    /// Build a list of pending contracts from this type annotation.
+    pub fn as_pending_contracts(&self) -> Result<Vec<PendingContract>, UnboundTypeVariableError> {
+        self.iter()
+            .cloned()
+            .map(PendingContract::try_from)
+            .collect::<Result<Vec<_>, _>>()
+    }
 }
 
 impl From<TypeAnnotation> for LetMetadata {
@@ -1209,11 +1265,16 @@ pub enum BinaryOp {
     /// field with this name to the given record with the expression on top of the stack as
     /// content.
     ///
-    /// The field may have been defined with attached metadata, and may or may not have a defined
-    /// value. We can't store those information as a term argument (metadata aren't first class
-    /// values, at least at the time of writing), so for now we attach it directly to the extend
-    /// primop. This isn't ideal, and in the future we may want to have a more principled primop.
-    DynExtend(FieldMetadata, RecordExtKind),
+    /// The field may have been defined with attached metadata, pending contracts and may or may
+    /// not have a defined value. We can't store those information as a term argument (metadata
+    /// aren't first class values, at least at the time of writing), so for now we attach it
+    /// directly to the extend primop. This isn't ideal, and in the future we may want to have a
+    /// more principled primop.
+    DynExtend {
+        metadata: FieldMetadata,
+        pending_contracts: Vec<PendingContract>,
+        ext_kind: RecordExtKind,
+    },
     /// Remove a field from a record. The field name is given as an arbitrary Nickel expression.
     DynRemove(),
     /// Access the field of record. The field name is given as an arbitrary Nickel expression.
@@ -1250,9 +1311,23 @@ impl BinaryOp {
     pub fn pos(&self) -> OpPos {
         use BinaryOp::*;
         match self {
-            Plus() | Sub() | Mult() | Div() | Modulo() | Pow() | StrConcat() | Eq()
-            | LessThan() | LessOrEq() | GreaterThan() | GreaterOrEq() | DynExtend(..)
-            | DynRemove() | DynAccess() | ArrayConcat() | Merge() => OpPos::Infix,
+            Plus()
+            | Sub()
+            | Mult()
+            | Div()
+            | Modulo()
+            | Pow()
+            | StrConcat()
+            | Eq()
+            | LessThan()
+            | LessOrEq()
+            | GreaterThan()
+            | GreaterOrEq()
+            | DynExtend { .. }
+            | DynRemove()
+            | DynAccess()
+            | ArrayConcat()
+            | Merge() => OpPos::Infix,
             _ => OpPos::Prefix,
         }
     }
diff --git a/src/term/record.rs b/src/term/record.rs
index 93dbf606..0ab9e151 100644
--- a/src/term/record.rs
+++ b/src/term/record.rs
@@ -144,6 +144,9 @@ pub struct Field {
     /// The value is optional because record field may not have a definition (e.g. optional fields).
     pub value: Option<RichTerm>,
     pub metadata: FieldMetadata,
+    /// List of contracts yet to be applied.
+    /// These are only observed when data enter or leave the record.
+    pub pending_contracts: Vec<PendingContract>,
 }
 
 impl From<RichTerm> for Field {
@@ -159,8 +162,8 @@ impl Field {
     /// Map a function over the value of the field, if any.
     pub fn map_value(self, f: impl FnOnce(RichTerm) -> RichTerm) -> Self {
         Field {
-            metadata: self.metadata,
             value: self.value.map(f),
+            ..self
         }
     }
 
@@ -170,8 +173,8 @@ impl Field {
         f: impl FnOnce(RichTerm) -> Result<RichTerm, E>,
     ) -> Result<Self, E> {
         Ok(Field {
-            metadata: self.metadata,
             value: self.value.map(f).transpose()?,
+            ..self
         })
     }
 
@@ -197,17 +200,28 @@ impl Traverse<RichTerm> for Field {
     where
         F: Fn(RichTerm, &mut S) -> Result<RichTerm, E>,
     {
-        let Field { metadata, value } = self;
-
-        let annotation = metadata.annotation.traverse(f, state, order)?;
-        let value = value.map(|v| v.traverse(f, state, order)).transpose()?;
+        let annotation = self.metadata.annotation.traverse(f, state, order)?;
+        let value = self
+            .value
+            .map(|v| v.traverse(f, state, order))
+            .transpose()?;
 
         let metadata = FieldMetadata {
             annotation,
-            ..metadata
+            ..self.metadata
         };
 
-        Ok(Field { metadata, value })
+        let pending_contracts = self
+            .pending_contracts
+            .into_iter()
+            .map(|pending_contract| pending_contract.traverse(f, state, order))
+            .collect::<Result<Vec<_>, _>>()?;
+
+        Ok(Field {
+            metadata,
+            value,
+            pending_contracts,
+        })
     }
 }
 
@@ -299,8 +313,8 @@ impl RecordData {
                 (
                     id,
                     Field {
-                        metadata: field.metadata,
                         value: f(id, field.value),
+                        ..field
                     },
                 )
             })
@@ -318,7 +332,11 @@ impl RecordData {
     }
 
     /// Turn the record into an iterator over the fields' values, ignoring optional fields without
-    /// definition. Fields that aren't optional but yet don't have a definition are mapped to the
+    /// definition.
+    ///
+    /// The returned iterator applies pending contracts to each value.
+    ///
+    /// Fields that aren't optional but yet don't have a definition are mapped to the
     /// error `MissingFieldDefError`.
     pub fn into_iter_without_opts(
         self,
@@ -326,7 +344,13 @@ impl RecordData {
         self.fields
             .into_iter()
             .filter_map(|(id, field)| match field.value {
-                Some(v) => Some(Ok((id, v))),
+                Some(v) => {
+                    let pos = v.pos;
+                    Some(Ok((
+                        id,
+                        PendingContract::apply_all(v, field.pending_contracts.into_iter(), pos),
+                    )))
+                }
                 None if !field.metadata.opt => Some(Err(MissingFieldDefError {
                     id,
                     metadata: field.metadata,
@@ -356,7 +380,12 @@ impl RecordData {
     /// Get the value of a field. Ignore optional fields without value: trying to get their value
     /// returns `None`, as if they weren't present at all. Trying to extract a field without value
     /// which is non optional return an error.
-    pub fn get_value(&self, id: &Ident) -> Result<Option<&RichTerm>, MissingFieldDefError> {
+    ///
+    /// This method automatically applies the potential pending contracts
+    pub fn get_value_with_ctrs(
+        &self,
+        id: &Ident,
+    ) -> Result<Option<RichTerm>, MissingFieldDefError> {
         match self.fields.get(id) {
             Some(Field {
                 value: None,
@@ -366,7 +395,19 @@ impl RecordData {
                 id: *id,
                 metadata: metadata.clone(),
             }),
-            field_opt => Ok(field_opt.and_then(|field| field.value.as_ref())),
+            Some(Field {
+                value: Some(value),
+                pending_contracts,
+                ..
+            }) => {
+                let pos = value.pos;
+                Ok(Some(PendingContract::apply_all(
+                    value.clone(),
+                    pending_contracts.iter().cloned(),
+                    pos,
+                )))
+            }
+            _ => Ok(None),
         }
     }
 }
diff --git a/src/transform/apply_contracts.rs b/src/transform/apply_contracts.rs
deleted file mode 100644
index a520e20f..00000000
--- a/src/transform/apply_contracts.rs
+++ /dev/null
@@ -1,102 +0,0 @@
-//! Generate contract applications from annotations.
-//!
-//! During the evaluation, the following invariant is enforced: any contract (be it the type
-//! annotation or a contract annotation) contained in a `Annotated` or in a field's metadata must
-//! have been applied to the inner value. This invariant is false just after parsing, as there's
-//! merely no direct `Assume` in the output AST. This transformation makes it true after program
-//! transformations by generating corresponding assume.
-//!
-//! It must be run before `share_normal_form` to avoid rechecking contracts each time the inner
-//! value is unwrapped.
-use crate::term::TypeAnnotation;
-use crate::{
-    match_sharedterm, mk_app,
-    position::TermPos,
-    term::{
-        make as mk_term,
-        record::{Field, RecordData},
-        BinaryOp, PendingContract, RichTerm, Term,
-    },
-    types::UnboundTypeVariableError,
-};
-
-/// If the top-level node of the AST is a meta-value, apply the meta-value's contracts to the inner
-/// value.  Otherwise, return the term unchanged.
-/// Fail if an unbound type variable is encountered.
-pub fn transform_one(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
-    fn apply_from_annot(
-        annot: &TypeAnnotation,
-        rt: RichTerm,
-        pos: TermPos,
-    ) -> Result<RichTerm, UnboundTypeVariableError> {
-        let ctrs = annot
-            .iter()
-            .map(|ctr| {
-                Ok(PendingContract::new(
-                    ctr.types.contract()?,
-                    ctr.label.clone(),
-                ))
-            })
-            .collect::<Result<Vec<_>, _>>()?;
-
-        Ok(apply_contracts(rt, ctrs.into_iter(), pos.into_inherited()))
-    }
-
-    fn apply_to_field(field: Field) -> Result<Field, UnboundTypeVariableError> {
-        let Field { metadata, value } = field;
-        let value = value
-            .map(|v| {
-                let pos_v = v.pos;
-                apply_from_annot(&metadata.annotation, v, pos_v)
-            })
-            .transpose()?;
-
-        Ok(Field { value, metadata })
-    }
-
-    let pos = rt.pos;
-    let result = match_sharedterm! {rt.term,
-        with {
-            Term::Annotated(annot, inner) => {
-                let inner_transfd = apply_from_annot(&annot, inner, pos)?;
-                RichTerm::new(Term::Annotated(annot, inner_transfd), pos)
-            },
-            Term::RecRecord(record_data, dyn_fields, deps) => {
-                let RecordData {fields, attrs, sealed_tail} = record_data;
-
-                let fields = fields.into_iter().map(|(id, field)| {
-                    Ok((id, apply_to_field(field)?))
-                }).collect::<Result<_, _>>()?;
-
-                let dyn_fields = dyn_fields.into_iter().map(|(id_term, field)| {
-                    Ok((id_term, apply_to_field(field)?))
-                }).collect::<Result<_, _>>()?;
-
-                RichTerm::new(Term::RecRecord(RecordData {fields, attrs, sealed_tail}, dyn_fields, deps), pos)
-            },
-            Term::Record(record_data) => {
-                let RecordData {fields, attrs, sealed_tail} = record_data;
-
-                let fields = fields.into_iter().map(|(id, field)| {
-                    Ok((id, apply_to_field(field)?))
-                }).collect::<Result<_, _>>()?;
-
-                RichTerm::new(Term::Record(RecordData {fields, attrs, sealed_tail}), pos)
-            }
-        } else rt
-    };
-    Ok(result)
-}
-
-pub fn apply_contracts<I>(rt: RichTerm, contracts: I, pos: TermPos) -> RichTerm
-where
-    I: Iterator<Item = PendingContract>,
-{
-    contracts.fold(rt, |acc, ctr| {
-        mk_app!(
-            mk_term::op2(BinaryOp::Assume(), ctr.contract, Term::Lbl(ctr.label)).with_pos(pos),
-            acc
-        )
-        .with_pos(pos)
-    })
-}
diff --git a/src/transform/gen_pending_contracts.rs b/src/transform/gen_pending_contracts.rs
new file mode 100644
index 00000000..a52efc74
--- /dev/null
+++ b/src/transform/gen_pending_contracts.rs
@@ -0,0 +1,63 @@
+//! Generate contract applications from annotations.
+//!
+//! Since RFC005, contracts aren't "pre-applied" during the apply contract transformation, but lazy
+//! applied during evaluation. This phase still exists, just to generate the pending contracts (the
+//! only ones that the interpreter will care about at runtime) from the static annotations.
+//!
+//! It must be run before `share_normal_form` so that newly generated pending contracts are
+//! transformed as well.
+use crate::{
+    identifier::Ident,
+    match_sharedterm,
+    term::{
+        record::{Field, RecordData},
+        RichTerm, Term,
+    },
+    types::UnboundTypeVariableError,
+};
+
+use std::collections::HashMap;
+
+pub fn transform_one(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
+    fn attach_to_field(field: Field) -> Result<Field, UnboundTypeVariableError> {
+        let pending_contracts = field.metadata.annotation.as_pending_contracts()?;
+
+        Ok(Field {
+            pending_contracts,
+            ..field
+        })
+    }
+
+    fn attach_to_fields(
+        fields: HashMap<Ident, Field>,
+    ) -> Result<HashMap<Ident, Field>, UnboundTypeVariableError> {
+        fields
+            .into_iter()
+            .map(|(id, field)| Ok((id, attach_to_field(field)?)))
+            .collect()
+    }
+
+    let pos = rt.pos;
+    let result = match_sharedterm! {rt.term,
+        with {
+            Term::RecRecord(record_data, dyn_fields, deps) => {
+                let RecordData {fields, attrs, sealed_tail} = record_data;
+
+                let fields = attach_to_fields(fields)?;
+                let dyn_fields = dyn_fields.into_iter().map(|(id_term, field)| {
+                     Ok((id_term, attach_to_field(field)?))
+                }).collect::<Result<_, _>>()?;
+
+                RichTerm::new(Term::RecRecord(RecordData {fields, attrs, sealed_tail}, dyn_fields, deps), pos)
+            },
+            Term::Record(record_data) => {
+                let RecordData {fields, attrs, sealed_tail} = record_data;
+
+                let fields = attach_to_fields(fields)?;
+
+                RichTerm::new(Term::Record(RecordData {fields, attrs, sealed_tail}), pos)
+            }
+        } else rt
+    };
+    Ok(result)
+}
diff --git a/src/transform/mod.rs b/src/transform/mod.rs
index 168772bc..b675b5d1 100644
--- a/src/transform/mod.rs
+++ b/src/transform/mod.rs
@@ -3,17 +3,14 @@ use crate::{
     cache::ImportResolver,
     eval::{cache::Cache, Closure, Environment, IdentKind},
     identifier::Ident,
-    term::{
-        record::{Field, FieldMetadata},
-        BindingType, LabeledType, RichTerm, Term, Traverse, TraverseOrder, TypeAnnotation,
-    },
+    term::{record::Field, BindingType, PendingContract, RichTerm, Term, Traverse, TraverseOrder},
     typecheck::Wildcards,
-    types::{TypeF, Types, UnboundTypeVariableError},
+    types::UnboundTypeVariableError,
 };
 
-pub mod apply_contracts;
 pub mod desugar_destructuring;
 pub mod free_vars;
+pub mod gen_pending_contracts;
 pub mod import_resolution;
 pub mod share_normal_form;
 pub mod substitute_wildcards;
@@ -43,10 +40,9 @@ pub fn transform_no_free_vars(
             if let Some(wildcards) = wildcards {
                 rt = substitute_wildcards::transform_one(rt, wildcards);
             }
-            // before anything, we have to desugar the syntax
+            // We desugar destructuring before other transformations, as this step generates new
+            // record contracts and terms that must be themselves transformed.
             let rt = desugar_destructuring::transform_one(rt);
-            // We need to do contract generation before wrapping stuff in variables
-            let rt = apply_contracts::transform_one(rt)?;
             Ok(rt)
         },
         &mut (),
@@ -55,7 +51,18 @@ pub fn transform_no_free_vars(
 
     Ok(rt
         .traverse(
-            &|rt: RichTerm, _| -> Result<RichTerm, ()> {
+            &|rt: RichTerm, _| -> Result<RichTerm, UnboundTypeVariableError> {
+                // We need to do contract generation before the share normal form transformation,
+                // because `gen_pending_contracts` generates record contracts
+                //
+                // `gen_pending_contracts` is applied bottom-up, because it might generate
+                // additional terms down the AST (pending contracts pushed down the fields of a
+                // record). In a top-down workflow, we would then visit those new duplicated nodes
+                // (already visited as part of transforming the metadata), and do that potentially
+                // again one level down. This results in a potentially non-linear cost in the size
+                // of the AST. This was witnessed on Terraform-Nickel, causing examples using huge
+                // auto-generated contracts (several of MBs) to not terminate in reasonable time.
+                let rt = gen_pending_contracts::transform_one(rt)?;
                 let rt = share_normal_form::transform_one(rt);
                 Ok(rt)
             },
@@ -159,68 +166,27 @@ impl Closurizable for RichTerm {
     }
 }
 
-impl Closurizable for Types {
-    /// Pack the contract of a type together with an environment as a closure.
-    ///
-    /// Extract the underlying contract, closurize it and wrap it back as a flat type (an opaque
-    /// type defined by a custom contract).
-    fn closurize<C: Cache>(
-        self,
-        cache: &mut C,
-        env: &mut Environment,
-        with_env: Environment,
-    ) -> Types {
-        Types(TypeF::Flat(
-            self.contract().unwrap().closurize(cache, env, with_env),
-        ))
-    }
-}
-
-impl Closurizable for LabeledType {
-    fn closurize<C: Cache>(
-        self,
-        cache: &mut C,
-        env: &mut Environment,
-        with_env: Environment,
-    ) -> LabeledType {
-        LabeledType {
-            types: self.types.closurize(cache, env, with_env),
-            label: self.label,
-        }
-    }
-}
-
-impl Closurizable for TypeAnnotation {
+impl Closurizable for PendingContract {
     fn closurize<C: Cache>(
         self,
         cache: &mut C,
         env: &mut Environment,
         with_env: Environment,
-    ) -> TypeAnnotation {
-        let types = self
-            .types
-            .map(|ty| ty.closurize(cache, env, with_env.clone()));
-        let contracts = self
-            .contracts
-            .into_iter()
-            .map(|labeled_ty| labeled_ty.closurize(cache, env, with_env.clone()))
-            .collect();
-
-        TypeAnnotation { types, contracts }
+    ) -> PendingContract {
+        self.map_contract(|ctr| ctr.closurize(cache, env, with_env))
     }
 }
 
-impl Closurizable for FieldMetadata {
+impl Closurizable for Vec<PendingContract> {
     fn closurize<C: Cache>(
         self,
         cache: &mut C,
         env: &mut Environment,
         with_env: Environment,
-    ) -> FieldMetadata {
-        FieldMetadata {
-            annotation: self.annotation.closurize(cache, env, with_env),
-            ..self
-        }
+    ) -> Vec<PendingContract> {
+        self.into_iter()
+            .map(|pending_contract| pending_contract.closurize(cache, env, with_env.clone()))
+            .collect()
     }
 }
 
@@ -231,11 +197,16 @@ impl Closurizable for Field {
         env: &mut Environment,
         with_env: Environment,
     ) -> Field {
-        let metadata = self.metadata.closurize(cache, env, with_env.clone());
         let value = self
             .value
-            .map(|value| value.closurize(cache, env, with_env));
+            .map(|value| value.closurize(cache, env, with_env.clone()));
 
-        Field { metadata, value }
+        let pending_contracts = self.pending_contracts.closurize(cache, env, with_env);
+
+        Field {
+            metadata: self.metadata,
+            value,
+            pending_contracts,
+        }
     }
 }
diff --git a/src/transform/share_normal_form.rs b/src/transform/share_normal_form.rs
index b1b11e1c..d9ea5fea 100644
--- a/src/transform/share_normal_form.rs
+++ b/src/transform/share_normal_form.rs
@@ -32,10 +32,9 @@ use crate::{
     match_sharedterm,
     position::TermPos,
     term::{
-        record::{Field, FieldDeps, FieldMetadata, RecordData},
-        BindingType, LabeledType, LetAttrs, RichTerm, Term, TypeAnnotation,
+        record::{Field, FieldDeps, RecordData},
+        BindingType, LetAttrs, RichTerm, Term,
     },
-    types::{TypeF, Types},
 };
 
 struct Binding {
@@ -56,21 +55,24 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
     let pos = rt.pos;
     match_sharedterm! {rt.term,
         with {
-            Term::Record(record) => {
-                let mut bindings = Vec::with_capacity(record.fields.len());
+            // CAUTION: currently, if the record literals written by a user are always recursive
+            // records, other phases of program transformation (such as desugaring of field paths
+            // like `{foo.bar.baz = val}` or desugaring of destructuring) do introduce non
+            // recursive records.
+            //
+            // I've scratched my head more that once on a transformation seemingly not happening
+            // only for record elaborated by the destructuring desguaring phase, to find that the
+            // `Term::Record` case below has been forgotten, and only the case `Term::RecRecord`
+            // was updated.
+            Term::Record(record_data) => {
+                let mut bindings = Vec::with_capacity(record_data.fields.len());
+                let empty_deps = FieldDeps::empty();
 
-                let record = record.map_defined_values(|id, t| {
-                    if should_share(&t.term) {
-                        let fresh_var = Ident::fresh();
-                        let pos_t = t.pos;
-                        bindings.push(Binding {fresh_var, term: t, binding_type: BindingType::Normal});
-                        RichTerm::new(Term::Var(fresh_var), pos_t)
-                    } else {
-                        t
-                    }
-                });
+                let fields = record_data.fields.into_iter().map(|(id, field)| {
+                    (id, transform_rec_field(field, Some(empty_deps.clone()), &mut bindings))
+                }).collect();
 
-                with_bindings(Term::Record(record), bindings, pos)
+                with_bindings(Term::Record(RecordData { fields, ..record_data }), bindings, pos)
             },
             Term::RecRecord(record_data, dyn_fields, deps) => {
                 let mut bindings = Vec::with_capacity(record_data.fields.len());
@@ -110,9 +112,9 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
 
                 with_bindings(Term::Array(ts, attrs), bindings, pos)
             },
-            Term::Annotated(annot, t) if should_share(&rt.term) => {
+            Term::Annotated(annot, t) if should_share(&t.term) => {
                 let fresh_var = Ident::fresh();
-                let shared = RichTerm::new(Term::Var(fresh_var), rt.pos);
+                let shared = RichTerm::new(Term::Var(fresh_var), t.pos);
                 let inner = RichTerm::new(Term::Annotated(annot, shared), pos);
                 RichTerm::new(Term::Let(fresh_var, t, inner, LetAttrs::default()), pos)
             },
@@ -120,108 +122,56 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
     }
 }
 
-/// Transform a record field. Take care of transforming the contracts contained in the field
-/// metadata as well, as those might be recursively depending on other fields.
+/// Transform the field of a recursive record. Take care of transforming the pending contracts
+/// attached to the field, as those might be recursively depending on other fields.
 ///
-/// When a recursive record is evaluated, all fields need to be turned to closures
-/// anyway (see the corresponding case in `eval::eval()`), which is what the share
-/// normal form transformation does. This is why the test is more lax here than for
-/// other constructors: it is not only about sharing, but also about the future
-/// evaluation of recursive records. Only constants are not required to be
-/// closurized.
+/// When a recursive record is evaluated, all fields need to be turned to closures anyway (see the
+/// corresponding case in `eval::eval()`), which is what the share normal form transformation does.
+/// This is why the test is more lax here than for 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 share normal form transformation ensures 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 [`crate::RichTerm::closurize`] for more details.
+/// 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 share 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 [`crate::RichTerm::closurize`] for more details.
 fn transform_rec_field(
     field: Field,
     field_deps: Option<FieldDeps>,
     bindings: &mut Vec<Binding>,
 ) -> Field {
-    let annotation = field.metadata.annotation;
-
-    let types = annotation.types.map(|labeled_ty| {
-        let as_contract = labeled_ty.types.contract().unwrap();
-
+    let mut share_normal_form = |rt: RichTerm| {
         // CHANGE THIS CONDITION CAREFULLY. Doing so can break the post-condition
-        // explained above.
-        let contract = if !as_contract.as_ref().is_constant() {
+        // explained in this method's documentation above.
+        if !rt.as_ref().is_constant() {
             let fresh_var = Ident::fresh();
-            let pos_contract = as_contract.pos;
+            let pos_contract = rt.pos;
             let binding_type = mk_binding_type(field_deps.clone());
             bindings.push(Binding {
                 fresh_var,
-                term: as_contract,
+                term: rt,
                 binding_type,
             });
             RichTerm::new(Term::Var(fresh_var), pos_contract)
         } else {
-            as_contract
-        };
-
-        LabeledType {
-            types: Types(TypeF::Flat(contract)),
-            ..labeled_ty
+            rt
         }
-    });
+    };
 
-    let contracts = annotation
-        .contracts
+    let pending_contracts = field
+        .pending_contracts
         .into_iter()
-        .map(|labeled_ty| {
-            let as_contract = labeled_ty.types.contract().unwrap();
-
-            // CHANGE THIS CONDITION CAREFULLY. Doing so can break the post-condition
-            // explained above.
-            let contract = if !as_contract.as_ref().is_constant() {
-                let fresh_var = Ident::fresh();
-                let pos_contract = as_contract.pos;
-                let binding_type = mk_binding_type(field_deps.clone());
-                bindings.push(Binding {
-                    fresh_var,
-                    term: as_contract,
-                    binding_type,
-                });
-                RichTerm::new(Term::Var(fresh_var), pos_contract)
-            } else {
-                as_contract
-            };
-
-            LabeledType {
-                types: Types(TypeF::Flat(contract)),
-                ..labeled_ty
-            }
-        })
+        .map(|pending_contract| pending_contract.map_contract(&mut share_normal_form))
         .collect();
 
-    let value = field.value.map(|value| {
-        // CHANGE THIS CONDITION CAREFULLY. Doing so can break the post-condition
-        // explained above.
-        if !value.as_ref().is_constant() {
-            let fresh_var = Ident::fresh();
-            let pos_v = value.pos;
-            let binding_type = mk_binding_type(field_deps);
-            bindings.push(Binding {
-                fresh_var,
-                term: value,
-                binding_type,
-            });
-            RichTerm::new(Term::Var(fresh_var), pos_v)
-        } else {
-            value
-        }
-    });
+    let value = field.value.map(&mut share_normal_form);
 
     Field {
         value,
-        metadata: FieldMetadata {
-            annotation: TypeAnnotation { types, contracts },
-            ..field.metadata
-        },
+        metadata: field.metadata,
+        pending_contracts,
     }
 }
 
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index fda5447f..972db631 100644
--- a/src/typecheck/operation.rs
+++ b/src/typecheck/operation.rs
@@ -287,7 +287,10 @@ pub fn get_bop_type(
             )
         }
         // forall a. Str -> {_ : a} -> a -> {_ : a}
-        BinaryOp::DynExtend(_, RecordExtKind::WithValue) => {
+        BinaryOp::DynExtend {
+            ext_kind: RecordExtKind::WithValue,
+            ..
+        } => {
             let res = UnifType::UnifVar(state.table.fresh_type_var_id());
             (
                 mk_uniftype::str(),
@@ -296,7 +299,10 @@ pub fn get_bop_type(
             )
         }
         // forall a. Str -> {_ : a} -> {_ : a}
-        BinaryOp::DynExtend(_, RecordExtKind::WithoutValue) => {
+        BinaryOp::DynExtend {
+            ext_kind: RecordExtKind::WithoutValue,
+            ..
+        } => {
             let res = UnifType::UnifVar(state.table.fresh_type_var_id());
             (
                 mk_uniftype::str(),


Test patch:
diff --git a/tests/integration/pass/lazy-propagation.ncl b/tests/integration/pass/lazy-propagation.ncl
new file mode 100644
index 00000000..8db45279
--- /dev/null
+++ b/tests/integration/pass/lazy-propagation.ncl
@@ -0,0 +1,46 @@
+let {check, Assert, ..} = import "lib/assert.ncl" in
+
+# tests related to RFC005. Check in particular that the motivating examples of
+# RFC005 are indeed fixed by lazy propagation.
+[
+  # first example from RFC005
+  ({
+    foo | {
+      bar : Num,
+      baz : Str
+    }
+  }
+  & {foo = {}}
+  & {foo.bar = 1}
+  & {foo.baz = "a"})
+  == { foo.bar = 1, foo.baz = "a" },
+
+  # Nixel-inspired example from RFC005
+  let Drv = { out_path | Str, ..} in
+  let Package = { name | Str, drv | Drv, .. } in
+  ({
+    build_inputs | {_: Package} = {
+      foo,
+      bar,
+    },
+    build = m%"
+      %{build_inputs.foo.drv.out_path}/bin/foo $out
+    "%,
+  } & {
+    build_inputs = {
+      foo = { name = "foo", drv.out_path = "/fake/path" },
+      bar = { name = "bar", drv.out_path = "/fake/path" },
+    }
+  })
+  == {
+    build_inputs.foo = { name = "foo", drv.out_path = "/fake/path" },
+    build_inputs.bar = { name = "bar", drv.out_path = "/fake/path" },
+    build = "/fake/path/bin/foo $out",
+  },
+
+  # "Outer-cross application doesn't make sense" example
+  (({foo = 5} | {foo | Num})
+  & {bar = "bar"})
+  == {foo = 5, bar = "bar"},
+]
+|> check
diff --git a/tests/integration/pass/serialize.ncl b/tests/integration/pass/serialize.ncl
index 965f2942..15e9ee1c 100644
--- a/tests/integration/pass/serialize.ncl
+++ b/tests/integration/pass/serialize.ncl
@@ -2,14 +2,14 @@ let {check, ..} = import "lib/assert.ncl" in
 
 let assertSerInv = fun x =>
     let assertAux = fun format x =>
-      %deserialize% format (%serialize% format (%deep_seq% x x)) == x in
+      %deserialize% format (%serialize% format (%force% x)) == x in
     assertAux `Json x &&
     assertAux `Yaml x &&
     assertAux `Toml x in
 
 let assertDeserInv = fun x =>
     let assertAux = fun format x =>
-      let s = %serialize% format (%deep_seq% x x) in
+      let s = %serialize% format (%force% x) in
       %serialize% format (%deserialize% format s) == s in
     assertAux `Json x &&
     assertAux `Yaml x &&