Repository: tweag/nickel
Pull request #1617 (2023-09-21 09:18:28)

Assume -> ApplyContract
At the very beginning of Nickel, the duality between a type annotation and contract annotation was reflected in their original naming, the assume construct (contract annotation) and the promise construct (a type annotation).

This terminology isn't used anymore, and isn't very telling for new contributors. This PR gets rid of old references to `Assume` and `Promise`, and rename the `Assume` primitive operation to the more boring but more explicit `ApplyContract`.

yannham: No good reason, it's just historical. Let's get rid of them in a follow-up PR.

Patch:
diff --git a/core/src/eval/merge.rs b/core/src/eval/merge.rs
index 3d4b4b44..fdbe960e 100644
--- a/core/src/eval/merge.rs
+++ b/core/src/eval/merge.rs
@@ -207,7 +207,7 @@ pub fn merge<C: Cache>(
             // exactly the same, but can't be shadowed.
             let eq_contract = mk_app!(stdlib::internals::stdlib_contract_equal(), t1);
             let result = mk_app!(
-                mk_term::op2(BinaryOp::Assume(), eq_contract, Term::Lbl(label)),
+                mk_term::op2(BinaryOp::ApplyContract(), eq_contract, Term::Lbl(label)),
                 t2
             )
             .with_pos(pos_op);
diff --git a/core/src/eval/mod.rs b/core/src/eval/mod.rs
index ade3e1c6..62ed6af2 100644
--- a/core/src/eval/mod.rs
+++ b/core/src/eval/mod.rs
@@ -35,11 +35,6 @@
 //!   causes an [`crate::error::EvalError::InternalError`]. A resolved import, identified by a
 //!   `FileId`, is retrieved from the import resolver and evaluation proceeds.
 //!
-//! ## Contracts
-//!
-//! - **`Assume(type, label, term)`** (or `Promise(type, label, term)`): replace the current term
-//! with the contract corresponding to `types`, applied to label and term (`contract label term`).
-//!
 //! ## Operators
 //!
 //! Operators are strict by definition. To evaluate say `exp1 + exp2`, the following steps have to
diff --git a/core/src/eval/operation.rs b/core/src/eval/operation.rs
index 9bd51b85..6903180f 100644
--- a/core/src/eval/operation.rs
+++ b/core/src/eval/operation.rs
@@ -1373,12 +1373,12 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     Err(mk_type_error!("(++)", "String", 1, t1, pos1))
                 }
             }
-            BinaryOp::Assume() => {
+            BinaryOp::ApplyContract() => {
                 if let Term::Lbl(l) = &*t2 {
                     // Track the contract argument for better error reporting, and push back the
                     // label on the stack, so that it becomes the first argument of the contract.
                     let idx = self.stack.track_arg(&mut self.cache).ok_or_else(|| {
-                        EvalError::NotEnoughArgs(3, String::from("assume"), pos_op)
+                        EvalError::NotEnoughArgs(3, String::from("apply_contract"), pos_op)
                     })?;
                     let mut l = l.clone();
                     l.arg_pos = self.cache.get_then(idx.clone(), |c| c.body.pos);
@@ -1425,10 +1425,10 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
 
                             Ok(Closure { body, env: new_env })
                         }
-                        _ => Err(mk_type_error!("assume", "Contract", 1, t1, pos1)),
+                        _ => Err(mk_type_error!("apply_contract", "Contract", 1, t1, pos1)),
                     }
                 } else {
-                    Err(mk_type_error!("assume", "Label", 2, t2, pos2))
+                    Err(mk_type_error!("apply_contract", "Label", 2, t2, pos2))
                 }
             }
             BinaryOp::Unseal() => {
@@ -2063,9 +2063,9 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                 (Term::Str(_), _) => Err(mk_type_error!("str_contains", "String", 2, t2, pos2)),
                 (_, _) => Err(mk_type_error!("str_contains", "String", 1, t1, pos1)),
             },
-            BinaryOp::ArrayLazyAssume() => {
+            BinaryOp::ArrayLazyAppCtr() => {
                 let (ctr, _) = self.stack.pop_arg(&self.cache).ok_or_else(|| {
-                    EvalError::NotEnoughArgs(3, String::from("array_lazy_assume"), pos_op)
+                    EvalError::NotEnoughArgs(3, String::from("array_lazy_app_ctr"), pos_op)
                 })?;
 
                 let Closure {
@@ -2076,7 +2076,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                 // FIXME: use match?
                 let lbl = match_sharedterm! {t1, with {
                         Term::Lbl(lbl) => lbl
-                    } else return Err(mk_type_error!("array_lazy_assume", "Label", 1, t1, pos1))
+                    } else return Err(mk_type_error!("array_lazy_app_ctr", "Label", 1, t1, pos1))
                 };
 
                 match_sharedterm! {t2,
@@ -2098,10 +2098,10 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
 
                             Ok(array_with_ctr)
                         }
-                    } else Err(mk_type_error!("array_lazy_assume", "Array", 2, t2, pos2))
+                    } else Err(mk_type_error!("array_lazy_app_ctr", "Array", 2, t2, pos2))
                 }
             }
-            BinaryOp::RecordLazyAssume() => {
+            BinaryOp::RecordLazyAppCtr() => {
                 // The contract is expected to be of type `String -> Contract`: it takes the name
                 // of the field as a parameter, and returns a contract.
                 let (
@@ -2111,12 +2111,12 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     },
                     _,
                 ) = self.stack.pop_arg(&self.cache).ok_or_else(|| {
-                    EvalError::NotEnoughArgs(3, String::from("record_lazy_assume"), pos_op)
+                    EvalError::NotEnoughArgs(3, String::from("record_lazy_app_ctr"), pos_op)
                 })?;
 
                 let label = match_sharedterm! {t1, with {
                         Term::Lbl(label) => label
-                    } else return Err(mk_type_error!("record_lazy_assume", "Label", 1, t1, pos1))
+                    } else return Err(mk_type_error!("record_lazy_app_ctr", "Label", 1, t1, pos1))
                 };
 
                 match_sharedterm! {t2,
@@ -2164,7 +2164,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                 env,
                             })
                         }
-                    } else Err(mk_type_error!("record_lazy_assume", "Record", 2, t2, pos2))
+                    } else Err(mk_type_error!("record_lazy_app_ctr", "Record", 2, t2, pos2))
                 }
             }
             BinaryOp::LabelWithMessage() => {
diff --git a/core/src/label.rs b/core/src/label.rs
index 8cf8f5a4..f4ee61f6 100644
--- a/core/src/label.rs
+++ b/core/src/label.rs
@@ -25,13 +25,12 @@ pub mod ty_path {
     //! Checking higher-order contracts can involve a good share of intermediate contract checking.
     //! Take the following example:
     //! ```text
-    //! Assume(
-    //!     (Number -> Number) -> Number) -> Number -> Number,
-    //!     fun ev => fun cst => ev (fun x => cst)
-    //! )
+    //! (fun ev => fun cst => ev (fun x => cst))
+    //!   | ((Number -> Number) -> Number) -> Number -> Number,
     //! ```
     //! Once called, various checks will be performed on the arguments of functions and their return
     //! values:
+    //!
     //! 1. Check that `ev` provides a `Number` to `(fun x => cst)`
     //! 2. Check that `(fun x => cst)` returns a `Number`
     //! 3. Check that `ev (fun x => cst)` return a `Number`
@@ -39,8 +38,8 @@ pub mod ty_path {
     //!
     //! Each check can be linked to a base type occurrence (here, a `Number`) in the original type:
     //! ```text
-    //! (Number -> Number) -> Number) -> Number -> Number
-    //!  ^^^^^1    ^^^^^^2    ^^^^^^3    etc.
+    //! ((Number -> Number) -> Number) -> Number -> Number
+    //!   ^^^^^1    ^^^^^^2    ^^^^^^3    etc.
     //! ```
     //!
     //! This is the information encoded by a type path: what part of the original type is currently
diff --git a/core/src/parser/grammar.lalrpop b/core/src/parser/grammar.lalrpop
index ce6b21a1..cd0e3806 100644
--- a/core/src/parser/grammar.lalrpop
+++ b/core/src/parser/grammar.lalrpop
@@ -836,9 +836,9 @@ InfixExpr: UniTerm = {
 }
 
 BOpPre: BinaryOp = {
-    "assume" => BinaryOp::Assume(),
-    "array_lazy_assume" => BinaryOp::ArrayLazyAssume(),
-    "record_lazy_assume" => BinaryOp::RecordLazyAssume(),
+    "apply_contract" => BinaryOp::ApplyContract(),
+    "array_lazy_app_ctr" => BinaryOp::ArrayLazyAppCtr(),
+    "record_lazy_app_ctr" => BinaryOp::RecordLazyAppCtr(),
     "unseal" => BinaryOp::Unseal(),
     "seal" => BinaryOp::Seal(),
     "go_field" => BinaryOp::GoField(),
@@ -1019,9 +1019,9 @@ extern {
         "Array" => Token::Normal(NormalToken::Array),
 
         "typeof" => Token::Normal(NormalToken::Typeof),
-        "assume" => Token::Normal(NormalToken::Assume),
-        "array_lazy_assume" => Token::Normal(NormalToken::ArrayLazyAssume),
-        "record_lazy_assume" => Token::Normal(NormalToken::RecordLazyAssume),
+        "apply_contract" => Token::Normal(NormalToken::ApplyContract),
+        "array_lazy_app_ctr" => Token::Normal(NormalToken::ArrayLazyAppCtr),
+        "record_lazy_app_ctr" => Token::Normal(NormalToken::RecordLazyAppCtr),
         "op force" => Token::Normal(NormalToken::OpForce),
         "blame" => Token::Normal(NormalToken::Blame),
         "chng_pol" => Token::Normal(NormalToken::ChangePol),
diff --git a/core/src/parser/lexer.rs b/core/src/parser/lexer.rs
index a377138c..2dbd2b06 100644
--- a/core/src/parser/lexer.rs
+++ b/core/src/parser/lexer.rs
@@ -184,12 +184,12 @@ pub enum NormalToken<'input> {
     #[token("%typeof%")]
     Typeof,
 
-    #[token("%assume%")]
-    Assume,
-    #[token("%array_lazy_assume%")]
-    ArrayLazyAssume,
-    #[token("%record_lazy_assume%")]
-    RecordLazyAssume,
+    #[token("%apply_contract%")]
+    ApplyContract,
+    #[token("%array_lazy_app_ctr%")]
+    ArrayLazyAppCtr,
+    #[token("%record_lazy_app_ctr%")]
+    RecordLazyAppCtr,
     #[token("%blame%")]
     Blame,
     #[token("%chng_pol%")]
diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs
index 2e07da3a..15cd8559 100644
--- a/core/src/term/mod.rs
+++ b/core/src/term/mod.rs
@@ -168,11 +168,12 @@ pub enum Term {
     /// Sealed terms are introduced by contracts on polymorphic types. Take the following example:
     ///
     /// ```text
-    /// let f = Assume(forall a. forall b. a -> b -> a, fun x y => y) in
+    /// let f | forall a b. a -> b -> a = fun x y => y in
     /// f true "a"
     /// ```
     ///
     /// This function is ill-typed. To check that, a polymorphic contract will:
+    ///
     /// - Assign a unique identifier to each type variable: say `a => 1`, `b => 2`
     /// - For each cast on a negative occurrence of a type variable `a` or `b` (corresponding to an
     /// argument position), tag the argument with the associated identifier. In our example, `f
@@ -268,8 +269,8 @@ pub enum BindingType {
     Revertible(FieldDeps),
 }
 
-/// A runtime representation of a contract, as a term ready to be applied via `Assume()` together
-/// with its label.
+/// A runtime representation of a contract, as a term ready to be applied via `AppContract`
+/// together with its label.
 #[derive(Debug, PartialEq, Clone)]
 pub struct RuntimeContract {
     /// The pending contract, can be a function or a record.
@@ -300,7 +301,12 @@ impl RuntimeContract {
         use crate::mk_app;
 
         mk_app!(
-            make::op2(BinaryOp::Assume(), self.contract, Term::Lbl(self.label)).with_pos(pos),
+            make::op2(
+                BinaryOp::ApplyContract(),
+                self.contract,
+                Term::Lbl(self.label)
+            )
+            .with_pos(pos),
             rt
         )
         .with_pos(pos)
@@ -324,8 +330,12 @@ impl Traverse<RichTerm> for RuntimeContract {
         Ok(RuntimeContract { contract, ..self })
     }
 
-    fn traverse_ref<U>(&self, f: &mut dyn FnMut(&RichTerm) -> TraverseControl<U>) -> Option<U> {
-        self.contract.traverse_ref(f)
+    fn traverse_ref<S, U>(
+        &self,
+        f: &mut dyn FnMut(&RichTerm, &S) -> TraverseControl<S, U>,
+        state: &S,
+    ) -> Option<U> {
+        self.contract.traverse_ref(f, state)
     }
 }
 
@@ -478,8 +488,12 @@ impl Traverse<RichTerm> for LabeledType {
         typ.traverse(f, order).map(|typ| LabeledType { typ, label })
     }
 
-    fn traverse_ref<U>(&self, f: &mut dyn FnMut(&RichTerm) -> TraverseControl<U>) -> Option<U> {
-        self.typ.traverse_ref(f)
+    fn traverse_ref<S, U>(
+        &self,
+        f: &mut dyn FnMut(&RichTerm, &S) -> TraverseControl<S, U>,
+        state: &S,
+    ) -> Option<U> {
+        self.typ.traverse_ref(f, state)
     }
 }
 
@@ -592,11 +606,15 @@ impl Traverse<RichTerm> for TypeAnnotation {
         Ok(TypeAnnotation { typ, contracts })
     }
 
-    fn traverse_ref<U>(&self, f: &mut dyn FnMut(&RichTerm) -> TraverseControl<U>) -> Option<U> {
+    fn traverse_ref<S, U>(
+        &self,
+        f: &mut dyn FnMut(&RichTerm, &S) -> TraverseControl<S, U>,
+        state: &S,
+    ) -> Option<U> {
         self.contracts
             .iter()
-            .find_map(|c| c.traverse_ref(f))
-            .or_else(|| self.typ.as_ref().and_then(|t| t.traverse_ref(f)))
+            .find_map(|c| c.traverse_ref(f, state))
+            .or_else(|| self.typ.as_ref().and_then(|t| t.traverse_ref(f, state)))
     }
 }
 
@@ -1074,7 +1092,7 @@ pub enum UnaryOp {
 
     /// Force full evaluation of a term and return it.
     ///
-    /// This was added in the context of [`BinaryOp::ArrayLazyAssume`], in particular to make
+    /// This was added in the context of [`BinaryOp::ArrayLazyAppCtr`], in particular to make
     /// serialization work with lazy array contracts.
     ///
     /// # `Force` vs. `DeepSeq`
@@ -1308,14 +1326,12 @@ pub enum BinaryOp {
     /// Greater than or equal comparison operator.
     GreaterOrEq(),
 
-    /// An assume.
-    ///
     /// Apply a contract to a label and a value. The value is is stored on the stack unevaluated,
-    /// while the contract and the label are the strict arguments to this operator. Assume also
-    /// accepts contracts as records, that are translates to a function that performs a merge
-    /// operation with its argument. Finally, this operator marks the location of the contract
-    /// argument for better error reporting.
-    Assume(),
+    /// while the contract and the label are the strict arguments to this operator. `ApplyContract`
+    /// also accepts contracts as records, which are translated to a function that merge said
+    /// contract with its argument. Finally, this operator marks the location of the contract
+    /// argument on the stack for better error reporting.
+    ApplyContract(),
 
     /// Unseal a sealed term.
     ///
@@ -1385,11 +1401,11 @@ pub enum BinaryOp {
 
     /// Lazily apply a contract to an Array.
     /// This simply inserts a contract into the array attributes.
-    ArrayLazyAssume(),
+    ArrayLazyAppCtr(),
 
     /// Lazily map contracts over a record. The arguments are a label and a function which takes
     /// the name of the field as a parameter and returns the corresponding contract.
-    RecordLazyAssume(),
+    RecordLazyAppCtr(),
 
     /// Set the message of the current diagnostic of a label.
     LabelWithMessage(),
@@ -1432,7 +1448,7 @@ impl fmt::Display for BinaryOp {
             LessOrEq() => write!(f, "less_or_eq"),
             GreaterThan() => write!(f, "greater_than"),
             GreaterOrEq() => write!(f, "greater_or_eq"),
-            Assume() => write!(f, "assume"),
+            ApplyContract() => write!(f, "apply_contract"),
             Unseal() => write!(f, "unseal"),
             GoField() => write!(f, "go_field"),
             DynExtend { .. } => write!(f, "record_insert"),
@@ -1448,8 +1464,8 @@ impl fmt::Display for BinaryOp {
             StrSplit() => write!(f, "str_split"),
             StrContains() => write!(f, "str_contains"),
             Seal() => write!(f, "seal"),
-            ArrayLazyAssume() => write!(f, "array_lazy_assume"),
-            RecordLazyAssume() => write!(f, "record_lazy_assume"),
+            ArrayLazyAppCtr() => write!(f, "array_lazy_app_ctr"),
+            RecordLazyAppCtr() => write!(f, "record_lazy_app_ctr"),
             LabelWithMessage() => write!(f, "label_with_message"),
             LabelWithNotes() => write!(f, "label_with_notes"),
             LabelAppendNote() => write!(f, "label_append_note"),
@@ -1625,8 +1641,14 @@ impl RichTerm {
 }
 
 /// Flow control for tree traverals.
-pub enum TraverseControl<U> {
+pub enum TraverseControl<S, U> {
     /// Normal control flow: continue recursing into the children.
+    ///
+    /// Pass the state &S to all children.
+    ContinueWithScope(S),
+    /// Normal control flow: continue recursing into the children.
+    ///
+    /// The state that was passed to the parent will be re-used for the children.
     Continue,
 
     /// Skip this branch of the tree.
@@ -1636,7 +1658,7 @@ pub enum TraverseControl<U> {
     Return(U),
 }
 
-impl<U> From<Option<U>> for TraverseControl<U> {
+impl<S, U> From<Option<U>> for TraverseControl<S, U> {
     fn from(value: Option<U>) -> Self {
         match value {
             Some(u) => TraverseControl::Return(u),
@@ -1659,7 +1681,19 @@ pub trait Traverse<T>: Sized {
     ///
     /// Through its return value, `f` can short-circuit one branch of the traversal or
     /// the entire traversal.
-    fn traverse_ref<U>(&self, f: &mut dyn FnMut(&T) -> TraverseControl<U>) -> Option<U>;
+    ///
+    /// This traversal can make use of "scoped" state. The `scope` argument is passed to
+    /// each callback, and the callback can optionally override that scope just for its
+    /// own subtree in the traversal. For example, when traversing a tree of terms you can
+    /// maintain an environment. Most of the time the environment should get passed around
+    /// unchanged, but a `Term::Let` should override the environment of its subtree. It
+    /// does this by returning a `TraverseControl::ContinueWithScope` that contains the
+    /// new environment.
+    fn traverse_ref<S, U>(
+        &self,
+        f: &mut dyn FnMut(&T, &S) -> TraverseControl<S, U>,
+        scope: &S,
+    ) -> Option<U>;
 }
 
 impl Traverse<RichTerm> for RichTerm {
@@ -1857,9 +1891,14 @@ impl Traverse<RichTerm> for RichTerm {
         }
     }
 
-    fn traverse_ref<U>(&self, f: &mut dyn FnMut(&RichTerm) -> TraverseControl<U>) -> Option<U> {
-        match f(self) {
-            TraverseControl::Continue => {}
+    fn traverse_ref<S, U>(
+        &self,
+        f: &mut dyn FnMut(&RichTerm, &S) -> TraverseControl<S, U>,
+        state: &S,
+    ) -> Option<U> {
+        let child_state = match f(self, state) {
+            TraverseControl::Continue => None,
+            TraverseControl::ContinueWithScope(s) => Some(s),
             TraverseControl::SkipBranch => {
                 return None;
             }
@@ -1867,6 +1906,7 @@ impl Traverse<RichTerm> for RichTerm {
                 return Some(ret);
             }
         };
+        let state = child_state.as_ref().unwrap_or(state);
 
         match &*self.term {
             Term::Null
@@ -1883,7 +1923,7 @@ impl Traverse<RichTerm> for RichTerm {
             | Term::RuntimeError(_) => None,
             Term::StrChunks(chunks) => chunks.iter().find_map(|ch| {
                 if let StrChunk::Expr(term, _) = ch {
-                    term.traverse_ref(f)
+                    term.traverse_ref(f, state)
                 } else {
                     None
                 }
@@ -1891,29 +1931,37 @@ impl Traverse<RichTerm> for RichTerm {
             Term::Fun(_, t)
             | Term::FunPattern(_, _, t)
             | Term::Op1(_, t)
-            | Term::Sealed(_, t, _) => t.traverse_ref(f),
+            | Term::Sealed(_, t, _) => t.traverse_ref(f, state),
             Term::Let(_, t1, t2, _)
             | Term::LetPattern(_, _, t1, t2)
             | Term::App(t1, t2)
-            | Term::Op2(_, t1, t2) => t1.traverse_ref(f).or_else(|| t2.traverse_ref(f)),
-            Term::Record(data) => data.fields.values().find_map(|field| field.traverse_ref(f)),
+            | Term::Op2(_, t1, t2) => t1
+                .traverse_ref(f, state)
+                .or_else(|| t2.traverse_ref(f, state)),
+            Term::Record(data) => data
+                .fields
+                .values()
+                .find_map(|field| field.traverse_ref(f, state)),
             Term::RecRecord(data, dyn_data, _) => data
                 .fields
                 .values()
-                .find_map(|field| field.traverse_ref(f))
+                .find_map(|field| field.traverse_ref(f, state))
                 .or_else(|| {
                     dyn_data.iter().find_map(|(id, field)| {
-                        id.traverse_ref(f).or_else(|| field.traverse_ref(f))
+                        id.traverse_ref(f, state)
+                            .or_else(|| field.traverse_ref(f, state))
                     })
                 }),
             Term::Match { cases, default } => cases
                 .iter()
-                .find_map(|(_id, t)| t.traverse_ref(f))
-                .or_else(|| default.as_ref().and_then(|t| t.traverse_ref(f))),
-            Term::Array(ts, _) => ts.iter().find_map(|t| t.traverse_ref(f)),
-            Term::OpN(_, ts) => ts.iter().find_map(|t| t.traverse_ref(f)),
-            Term::Annotated(annot, t) => t.traverse_ref(f).or_else(|| annot.traverse_ref(f)),
-            Term::Type(ty) => ty.traverse_ref(f),
+                .find_map(|(_id, t)| t.traverse_ref(f, state))
+                .or_else(|| default.as_ref().and_then(|t| t.traverse_ref(f, state))),
+            Term::Array(ts, _) => ts.iter().find_map(|t| t.traverse_ref(f, state)),
+            Term::OpN(_, ts) => ts.iter().find_map(|t| t.traverse_ref(f, state)),
+            Term::Annotated(annot, t) => t
+                .traverse_ref(f, state)
+                .or_else(|| annot.traverse_ref(f, state)),
+            Term::Type(ty) => ty.traverse_ref(f, state),
         }
     }
 }
@@ -1934,11 +1982,18 @@ impl Traverse<Type> for RichTerm {
         )
     }
 
-    fn traverse_ref<U>(&self, f: &mut dyn FnMut(&Type) -> TraverseControl<U>) -> Option<U> {
-        self.traverse_ref(&mut |rt: &RichTerm| match &*rt.term {
-            Term::Type(ty) => ty.traverse_ref(f).into(),
-            _ => TraverseControl::Continue,
-        })
+    fn traverse_ref<S, U>(
+        &self,
+        f: &mut dyn FnMut(&Type, &S) -> TraverseControl<S, U>,
+        state: &S,
+    ) -> Option<U> {
+        self.traverse_ref(
+            &mut |rt: &RichTerm, state: &S| match &*rt.term {
+                Term::Type(ty) => ty.traverse_ref(f, state).into(),
+                _ => TraverseControl::Continue,
+            },
+            state,
+        )
     }
 }
 
@@ -2230,12 +2285,16 @@ pub mod make {
         Term::OpN(op, args.into_iter().map(T::into).collect()).into()
     }
 
-    pub fn assume<T>(typ: Type, l: Label, t: T) -> Result<RichTerm, UnboundTypeVariableError>
+    pub fn apply_contract<T>(
+        typ: Type,
+        l: Label,
+        t: T,
+    ) -> Result<RichTerm, UnboundTypeVariableError>
     where
         T: Into<RichTerm>,
     {
         Ok(mk_app!(
-            op2(BinaryOp::Assume(), typ.contract()?, Term::Lbl(l)),
+            op2(BinaryOp::ApplyContract(), typ.contract()?, Term::Lbl(l)),
             t.into()
         ))
     }
diff --git a/core/src/term/record.rs b/core/src/term/record.rs
index 85ad780c..0d363cf5 100644
--- a/core/src/term/record.rs
+++ b/core/src/term/record.rs
@@ -191,15 +191,19 @@ impl Traverse<RichTerm> for Field {
         })
     }
 
-    fn traverse_ref<U>(&self, f: &mut dyn FnMut(&RichTerm) -> TraverseControl<U>) -> Option<U> {
+    fn traverse_ref<S, U>(
+        &self,
+        f: &mut dyn FnMut(&RichTerm, &S) -> TraverseControl<S, U>,
+        state: &S,
+    ) -> Option<U> {
         self.metadata
             .annotation
-            .traverse_ref(f)
-            .or_else(|| self.value.as_ref().and_then(|v| v.traverse_ref(f)))
+            .traverse_ref(f, state)
+            .or_else(|| self.value.as_ref().and_then(|v| v.traverse_ref(f, state)))
             .or_else(|| {
                 self.pending_contracts
                     .iter()
-                    .find_map(|c| c.traverse_ref(f))
+                    .find_map(|c| c.traverse_ref(f, state))
             })
     }
 }
diff --git a/core/src/typ.rs b/core/src/typ.rs
index e37da908..50741cf1 100644
--- a/core/src/typ.rs
+++ b/core/src/typ.rs
@@ -624,11 +624,16 @@ impl Traverse<Type> for RecordRows {
         Ok(RecordRows(rows))
     }
 
-    fn traverse_ref<U>(&self, f: &mut dyn FnMut(&Type) -> TraverseControl<U>) -> Option<U> {
+    fn traverse_ref<S, U>(
+        &self,
+        f: &mut dyn FnMut(&Type, &S) -> TraverseControl<S, U>,
+        state: &S,
+    ) -> Option<U> {
         match &self.0 {
-            RecordRowsF::Extend { row, tail } => {
-                row.typ.traverse_ref(f).or_else(|| tail.traverse_ref(f))
-            }
+            RecordRowsF::Extend { row, tail } => row
+                .typ
+                .traverse_ref(f, state)
+                .or_else(|| tail.traverse_ref(f, state)),
             _ => None,
         }
     }
@@ -923,7 +928,7 @@ impl Type {
     }
 
     /// Return the contract corresponding to a type, either as a function or a record. Said
-    /// contract must then be applied using the `Assume` primitive operation.
+    /// contract must then be applied using the `ApplyContract` primitive operation.
     pub fn contract(&self) -> Result<RichTerm, UnboundTypeVariableError> {
         let mut sy = 0;
         self.subcontract(HashMap::new(), Polarity::Positive, &mut sy)
@@ -1054,10 +1059,13 @@ impl Type {
 
     /// Searches for a `TypeF::Flat`. If one is found, returns the term it contains.
     pub fn find_flat(&self) -> Option<RichTerm> {
-        self.traverse_ref(&mut |ty: &Type| match &ty.typ {
-            TypeF::Flat(f) => TraverseControl::Return(f.clone()),
-            _ => TraverseControl::Continue,
-        })
+        self.traverse_ref(
+            &mut |ty: &Type, _: &()| match &ty.typ {
+                TypeF::Flat(f) => TraverseControl::Return(f.clone()),
+                _ => TraverseControl::Continue,
+            },
+            &(),
+        )
     }
 }
 
@@ -1089,12 +1097,22 @@ impl Traverse<Type> for Type {
         }
     }
 
-    fn traverse_ref<U>(&self, f: &mut dyn FnMut(&Type) -> TraverseControl<U>) -> Option<U> {
-        match f(self) {
-            TraverseControl::Continue => (),
-            TraverseControl::SkipBranch => return None,
-            TraverseControl::Return(ret) => return Some(ret),
+    fn traverse_ref<S, U>(
+        &self,
+        f: &mut dyn FnMut(&Type, &S) -> TraverseControl<S, U>,
+        state: &S,
+    ) -> Option<U> {
+        let child_state = match f(self, state) {
+            TraverseControl::Continue => None,
+            TraverseControl::ContinueWithScope(s) => Some(s),
+            TraverseControl::SkipBranch => {
+                return None;
+            }
+            TraverseControl::Return(ret) => {
+                return Some(ret);
+            }
         };
+        let state = child_state.as_ref().unwrap_or(state);
 
         match &self.typ {
             TypeF::Dyn
@@ -1105,12 +1123,14 @@ impl Traverse<Type> for Type {
             | TypeF::Var(_)
             | TypeF::Enum(_)
             | TypeF::Wildcard(_) => None,
-            TypeF::Flat(rt) => rt.traverse_ref(f),
-            TypeF::Arrow(t1, t2) => t1.traverse_ref(f).or_else(|| t2.traverse_ref(f)),
+            TypeF::Flat(rt) => rt.traverse_ref(f, state),
+            TypeF::Arrow(t1, t2) => t1
+                .traverse_ref(f, state)
+                .or_else(|| t2.traverse_ref(f, state)),
             TypeF::Forall { body: t, .. }
             | TypeF::Dict { type_fields: t, .. }
-            | TypeF::Array(t) => t.traverse_ref(f),
-            TypeF::Record(rrows) => rrows.traverse_ref(f),
+            | TypeF::Array(t) => t.traverse_ref(f, state),
+            TypeF::Record(rrows) => rrows.traverse_ref(f, state),
         }
     }
 }
@@ -1131,17 +1151,24 @@ impl Traverse<RichTerm> for Type {
         )
     }
 
-    fn traverse_ref<U>(&self, f: &mut dyn FnMut(&RichTerm) -> TraverseControl<U>) -> Option<U> {
-        self.traverse_ref(&mut |ty: &Type| match &ty.typ {
-            TypeF::Flat(t) => {
-                if let Some(ret) = t.traverse_ref(f) {
-                    TraverseControl::Return(ret)
-                } else {
-                    TraverseControl::SkipBranch
+    fn traverse_ref<S, U>(
+        &self,
+        f: &mut dyn FnMut(&RichTerm, &S) -> TraverseControl<S, U>,
+        state: &S,
+    ) -> Option<U> {
+        self.traverse_ref(
+            &mut |ty: &Type, s: &S| match &ty.typ {
+                TypeF::Flat(t) => {
+                    if let Some(ret) = t.traverse_ref(f, s) {
+                        TraverseControl::Return(ret)
+                    } else {
+                        TraverseControl::SkipBranch
+                    }
                 }
-            }
-            _ => TraverseControl::Continue,
-        })
+                _ => TraverseControl::Continue,
+            },
+            state,
+        )
     }
 }
 
diff --git a/core/src/typecheck/mod.rs b/core/src/typecheck/mod.rs
index a87bf00c..1e43aa55 100644
--- a/core/src/typecheck/mod.rs
+++ b/core/src/typecheck/mod.rs
@@ -2514,7 +2514,7 @@ fn field_apparent_type(
 ///
 /// When a let-binding `let x = bound_exp in body` is processed, the type of `bound_exp` must be
 /// determined in order to be bound to the variable `x` in the typing environment.
-/// Then, future occurrences of `x` can be given this type when used in a `Promise` block.
+/// Then, future occurrences of `x` can be given this type when used in a statically typed block.
 ///
 /// The role of `apparent_type` is precisely to determine the type of `bound_exp`:
 /// - if `bound_exp` is annotated by a type or contract annotation, return the user-provided type,
diff --git a/core/src/typecheck/operation.rs b/core/src/typecheck/operation.rs
index ad9dc1cc..736016cd 100644
--- a/core/src/typecheck/operation.rs
+++ b/core/src/typecheck/operation.rs
@@ -236,7 +236,7 @@ pub fn get_bop_type(
         BinaryOp::StrConcat() => (mk_uniftype::str(), mk_uniftype::str(), mk_uniftype::str()),
         // Ideally: Contract -> Label -> Dyn -> Dyn
         // Currently: Dyn -> Dyn -> (Dyn -> Dyn)
-        BinaryOp::Assume() => (
+        BinaryOp::ApplyContract() => (
             mk_uniftype::dynamic(),
             mk_uniftype::dynamic(),
             mk_uty_arrow!(mk_uniftype::dynamic(), mk_uniftype::dynamic()),
@@ -366,7 +366,7 @@ pub fn get_bop_type(
         ),
         // The first argument is a contract, the second is a label.
         // forall a. Dyn -> Dyn -> Array a -> Array a
-        BinaryOp::ArrayLazyAssume() => {
+        BinaryOp::ArrayLazyAppCtr() => {
             let ty_elt = state.table.fresh_type_uvar(var_level);
             let ty_array = mk_uniftype::array(ty_elt);
             (
@@ -377,7 +377,7 @@ pub fn get_bop_type(
         }
         // The first argument is a label, the third is a contract.
         // forall a. Dyn -> {_: a} -> Dyn -> {_: a}
-        BinaryOp::RecordLazyAssume() => {
+        BinaryOp::RecordLazyAppCtr() => {
             let ty_field = state.table.fresh_type_uvar(var_level);
             let ty_dict = mk_uniftype::dict(ty_field);
             (
diff --git a/core/stdlib/internals.ncl b/core/stdlib/internals.ncl
index 01b9ca28..9c5a8efc 100644
--- a/core/stdlib/internals.ncl
+++ b/core/stdlib/internals.ncl
@@ -15,13 +15,13 @@
 
   "$array" = fun element_contract label value =>
     if %typeof% value == 'Array then
-      %array_lazy_assume% (%go_array% label) value element_contract
+      %array_lazy_app_ctr% (%go_array% label) value element_contract
     else
       %blame% label,
 
   "$func" = fun domain codomain label value =>
     if %typeof% value == 'Function then
-      (fun x => %assume% codomain (%go_codom% label) (value (%assume% domain (%chng_pol% (%go_dom% label)) x)))
+      (fun x => %apply_contract% codomain (%go_codom% label) (value (%apply_contract% domain (%chng_pol% (%go_dom% label)) x)))
     else
       %blame% label,
 
@@ -49,7 +49,7 @@
 
   "$enums" = fun case label value =>
     if %typeof% value == 'Enum then
-      %assume% case label value
+      %apply_contract% case label value
     else
       %blame% (%label_with_message% "not an enum tag" label),
 
@@ -85,7 +85,7 @@
                   let contract = field_contracts."%{field}" in
                   let label = %go_field% field label in
                   let val = value."%{field}" in
-                  %record_insert% field acc (%assume% contract label val)
+                  %record_insert% field acc (%apply_contract% contract label val)
                 else
                   acc
             )
@@ -107,7 +107,7 @@
   # Lazy dictionary contract for `{_ | T}`
   "$dict_contract" = fun contract label value =>
     if %typeof% value == 'Record then
-      %record_lazy_assume% (%go_dict% label) value (fun _field => contract)
+      %record_lazy_app_ctr% (%go_dict% label) value (fun _field => contract)
     else
       %blame% (%label_with_message% "not a record" label),
 
@@ -118,7 +118,7 @@
         value
         (
           fun _field field_value =>
-            %assume% contract (%go_dict% label) field_value
+            %apply_contract% contract (%go_dict% label) field_value
         )
     else
       %blame% (%label_with_message% "not a record" label),
diff --git a/core/stdlib/std.ncl b/core/stdlib/std.ncl
index 6f348a14..e5973373 100644
--- a/core/stdlib/std.ncl
+++ b/core/stdlib/std.ncl
@@ -836,7 +836,7 @@
                 else if %length% diff.missing != 0 then
                   blame_fields_differ "missing" diff.missing ctr_label
                 else
-                  %record_lazy_assume%
+                  %record_lazy_app_ctr%
                     ctr_label
                     value
                     (
@@ -1168,7 +1168,7 @@
           using the parent contract message and note.
         "%
       = fun contract label value =>
-        %assume% contract (%label_push_diag% label) value,
+        %apply_contract% contract (%label_push_diag% label) value,
 
     unstable
       | doc m%"
diff --git a/lsp/nls/Cargo.toml b/lsp/nls/Cargo.toml
index b8b95cd9..fa86c214 100644
--- a/lsp/nls/Cargo.toml
+++ b/lsp/nls/Cargo.toml
@@ -15,7 +15,7 @@ name = "nls"
 path = "src/main.rs"
 
 [features]
-default = ["format", "old-completer"]
+default = ["format"]
 format = ["nickel-lang-core/format"]
 old-completer = []
 
diff --git a/lsp/nls/src/field_walker.rs b/lsp/nls/src/field_walker.rs
index 2f484a38..9aabe758 100644
--- a/lsp/nls/src/field_walker.rs
+++ b/lsp/nls/src/field_walker.rs
@@ -131,6 +131,18 @@ pub struct DefWithPath {
     pub metadata: Option<FieldMetadata>,
 }
 
+impl DefWithPath {
+    pub fn completion_item(&self) -> CompletionItem {
+        CompletionItem {
+            label: ident_quoted(&self.ident.into()),
+            detail: self.metadata.as_ref().and_then(metadata_detail),
+            kind: Some(CompletionItemKind::Property),
+            documentation: self.metadata.as_ref().and_then(metadata_doc),
+            ..Default::default()
+        }
+    }
+}
+
 #[cfg(test)]
 impl DefWithPath {
     pub fn path(&self) -> &[Ident] {
@@ -242,6 +254,7 @@ impl<'a> FieldResolver<'a> {
                 let defs = self.resolve_annot(annot);
                 defs.chain(self.resolve_term(term)).collect()
             }
+            Term::Type(typ) => self.resolve_type(typ),
             _ => Default::default(),
         };
 
diff --git a/lsp/nls/src/files.rs b/lsp/nls/src/files.rs
index ee629a2e..e8373022 100644
--- a/lsp/nls/src/files.rs
+++ b/lsp/nls/src/files.rs
@@ -82,6 +82,10 @@ pub fn handle_save(server: &mut Server, params: DidChangeTextDocumentParams) ->
     let invalid = server.cache.get_rev_imports_transitive(file_id);
     for f in &invalid {
         server.lin_registry.map.remove(f);
+        server.lin_registry.position_lookups.remove(f);
+        server.lin_registry.usage_lookups.remove(f);
+        server.lin_registry.parent_lookups.remove(f);
+        server.lin_registry.type_lookups.remove(f);
     }
 
     // TODO: make this part more abstracted
diff --git a/lsp/nls/src/incomplete.rs b/lsp/nls/src/incomplete.rs
index 828811ac..dd4947ef 100644
--- a/lsp/nls/src/incomplete.rs
+++ b/lsp/nls/src/incomplete.rs
@@ -11,7 +11,7 @@ use nickel_lang_core::{
     cache::SourcePath,
     parser::lexer::{self, NormalToken, SpannedToken, Token},
     position::RawSpan,
-    term::RichTerm,
+    term::{RichTerm, Term},
     transform::import_resolution,
 };
 
@@ -160,13 +160,13 @@ pub fn parse_path_from_incomplete_input(
         .replace_string(SourcePath::Snippet(path), to_parse);
 
     match server.cache.parse_nocache(file_id) {
-        Ok((rt, _errors)) => {
+        Ok((rt, _errors)) if !matches!(rt.as_ref(), Term::ParseError(_)) => {
             server
                 .lin_registry
                 .usage_lookups
                 .insert(file_id, UsageLookup::new_with_env(&rt, env));
             Some(resolve_imports(rt, server))
         }
-        Err(_) => None,
+        _ => None,
     }
 }
diff --git a/lsp/nls/src/linearization/completed.rs b/lsp/nls/src/linearization/completed.rs
index 21f1b989..b9cc9ea8 100644
--- a/lsp/nls/src/linearization/completed.rs
+++ b/lsp/nls/src/linearization/completed.rs
@@ -51,6 +51,7 @@ impl Completed {
     /// Returns the closest item to the left (if any) and to the right (if any) of
     /// a specified item. The "closeness" metric in this context is just the source
     /// position.
+    #[cfg(feature = "old-completer")]
     pub fn get_items_adjacent(
         &self,
         id: ItemId,
@@ -141,6 +142,7 @@ impl Completed {
     }
 
     /// Return all the items in the scope of the given linearization item.
+    #[cfg(feature = "old-completer")]
     pub fn get_in_scope<'a>(
         &'a self,
         LinearizationItem { env, .. }: &'a LinearizationItem<Resolved>,
diff --git a/lsp/nls/src/linearization/mod.rs b/lsp/nls/src/linearization/mod.rs
index 3d104831..6160e7a0 100644
--- a/lsp/nls/src/linearization/mod.rs
+++ b/lsp/nls/src/linearization/mod.rs
@@ -7,7 +7,7 @@ use nickel_lang_core::{
     position::TermPos,
     term::{
         record::{Field, FieldMetadata},
-        RichTerm, Term, UnaryOp,
+        RichTerm, Term, Traverse, TraverseControl, UnaryOp,
     },
     typ::TypeF,
     typecheck::{linearization::Linearizer, reporting::NameReg, UnifType},
@@ -30,6 +30,57 @@ pub mod interface;
 
 pub type Environment = nickel_lang_core::environment::Environment<Ident, ItemId>;
 
+#[derive(Clone, Debug)]
+pub struct ParentLookup {
+    table: HashMap<RichTermPtr, RichTerm>,
+}
+
+impl ParentLookup {
+    pub fn new(rt: &RichTerm) -> Self {
+        let mut table = HashMap::new();
+        let mut traverse_merge =
+            |rt: &RichTerm, parent: &Option<RichTerm>| -> TraverseControl<Option<RichTerm>, ()> {
+                if let Some(parent) = parent {
+                    table.insert(RichTermPtr(rt.clone()), parent.clone());
+                }
+                TraverseControl::ContinueWithScope(Some(rt.clone()))
+            };
+
+        rt.traverse_ref(&mut traverse_merge, &None);
+
+        ParentLookup { table }
+    }
+
+    pub fn parent(&self, rt: &RichTerm) -> Option<&RichTerm> {
+        self.table.get(&RichTermPtr(rt.clone()))
+    }
+
+    pub fn parent_chain<'a>(&'a self, rt: &'a RichTerm) -> ParentChainIter<'_> {
+        ParentChainIter {
+            table: self,
+            next: Some(rt),
+        }
+    }
+}
+
+pub struct ParentChainIter<'a> {
+    table: &'a ParentLookup,
+    next: Option<&'a RichTerm>,
+}
+
+impl<'a> Iterator for ParentChainIter<'a> {
+    type Item = &'a RichTerm;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        if let Some(next) = self.next {
+            self.next = self.table.parent(next);
+            Some(next)
+        } else {
+            None
+        }
+    }
+}
+
 /// A registry mapping file ids to their corresponding linearization. The registry stores the
 /// linearization of every file that has been imported and analyzed, including the main open
 /// document.
@@ -40,11 +91,17 @@ pub type Environment = nickel_lang_core::environment::Environment<Ident, ItemId>
 pub struct LinRegistry {
     pub map: HashMap<FileId, Completed>,
     // TODO: these are supposed to eventually *replace* part of the linearization, at
-    // which point we'll rename `LinRegistry` (and probably just have one HashMap<FileId,
-    // everything>)
+    // which point we'll rename `LinRegistry` (and probably just have one
+    // HashMap<FileId, everything>)
+    //
+    // Most of these tables do one more lookup than necessary: they look up a
+    // file id and then they look up a term in an inner table. This is a little
+    // inefficient for lookups, but it makes it easy to invalidate a whole file
+    // in one go.
     pub position_lookups: HashMap<FileId, PositionLookup>,
     pub usage_lookups: HashMap<FileId, UsageLookup>,
-    pub type_lookups: HashMap<RichTermPtr, Type>,
+    pub parent_lookups: HashMap<FileId, ParentLookup>,
+    pub type_lookups: HashMap<FileId, HashMap<RichTermPtr, Type>>,
 }
 
 impl LinRegistry {
@@ -63,8 +120,8 @@ impl LinRegistry {
         self.position_lookups
             .insert(file_id, PositionLookup::new(term));
         self.usage_lookups.insert(file_id, UsageLookup::new(term));
-
-        self.type_lookups.extend(type_lookups);
+        self.parent_lookups.insert(file_id, ParentLookup::new(term));
+        self.type_lookups.insert(file_id, type_lookups);
     }
 
     /// Look for the linearization corresponding to an item's id, and return the corresponding item
@@ -96,7 +153,13 @@ impl LinRegistry {
     }
 
     pub fn get_type(&self, rt: &RichTerm) -> Option<&Type> {
-        self.type_lookups.get(&RichTermPtr(rt.clone()))
+        let file = rt.pos.as_opt_ref()?.src_id;
+        self.type_lookups.get(&file)?.get(&RichTermPtr(rt.clone()))
+    }
+
+    pub fn get_parent_chain<'a>(&'a self, rt: &'a RichTerm) -> Option<ParentChainIter<'a>> {
+        let file = rt.pos.as_opt_ref()?.src_id;
+        Some(self.parent_lookups.get(&file)?.parent_chain(rt))
     }
 }
 
diff --git a/lsp/nls/src/position.rs b/lsp/nls/src/position.rs
index f45bc9ed..e3d6b25e 100644
--- a/lsp/nls/src/position.rs
+++ b/lsp/nls/src/position.rs
@@ -111,7 +111,7 @@ impl PositionLookup {
     pub fn new(rt: &RichTerm) -> Self {
         let mut all_term_ranges = Vec::new();
         let mut idents = Vec::new();
-        let mut fun = |term: &RichTerm| {
+        let mut fun = |term: &RichTerm, _state: &()| {
             if let TermPos::Original(pos) = &term.pos {
                 all_term_ranges.push((
                     Range {
@@ -139,10 +139,10 @@ impl PositionLookup {
                 Term::Match { cases, .. } => idents.extend(cases.keys().cloned()),
                 _ => {}
             }
-            TraverseControl::<()>::Continue
+            TraverseControl::<(), ()>::Continue
         };
 
-        rt.traverse_ref(&mut fun);
+        rt.traverse_ref(&mut fun, &());
 
         let mut ident_ranges: Vec<_> = idents
             .into_iter()
diff --git a/lsp/nls/src/requests/completion.rs b/lsp/nls/src/requests/completion.rs
index 335c154d..78cb783a 100644
--- a/lsp/nls/src/requests/completion.rs
+++ b/lsp/nls/src/requests/completion.rs
@@ -1,3 +1,5 @@
+#![allow(unused_imports)]
+
 use crate::{
     cache::CacheExt,
     field_walker::{FieldHaver, FieldResolver},
@@ -17,7 +19,6 @@ use lsp_server::{RequestId, Response, ResponseError};
 use lsp_types::{
     CompletionItem, CompletionItemKind, CompletionParams, Documentation, MarkupContent, MarkupKind,
 };
-use nickel_lang_core::cache::InputFormat;
 use nickel_lang_core::{
     cache,
     identifier::{Ident, LocIdent},
@@ -28,6 +29,7 @@ use nickel_lang_core::{
     },
     typ::{RecordRows, RecordRowsIteratorItem, Type, TypeF},
 };
+use nickel_lang_core::{cache::InputFormat, term::BinaryOp};
 use regex::Regex;
 use std::collections::HashSet;
 use std::ffi::OsString;
@@ -43,6 +45,7 @@ use std::path::PathBuf;
 // We follow the path by traversing a term, type or contract which represents a record
 // and stop when there is nothing else on the path
 
+#[cfg(feature = "old-completer")]
 #[derive(Debug)]
 struct IdentWithType {
     ident: Ident,
@@ -50,6 +53,7 @@ struct IdentWithType {
     meta: Option<FieldMetadata>,
 }
 
+#[cfg(feature = "old-completer")]
 impl From<Ident> for IdentWithType {
     fn from(ident: Ident) -> Self {
         IdentWithType {
@@ -60,6 +64,7 @@ impl From<Ident> for IdentWithType {
     }
 }
 
+#[cfg(feature = "old-completer")]
 impl From<&str> for IdentWithType {
     fn from(ident: &str) -> Self {
         IdentWithType {
@@ -70,6 +75,7 @@ impl From<&str> for IdentWithType {
     }
 }
 
+#[cfg(feature = "old-completer")]
 impl IdentWithType {
     fn detail(&self) -> String {
         self.meta
@@ -119,6 +125,7 @@ impl IdentWithType {
     }
 }
 
+#[cfg(feature = "old-completer")]
 /// Completion context: general data structures required by most completion functions.
 #[derive(Clone, Copy)]
 pub struct ComplCtx<'a> {
@@ -126,6 +133,7 @@ pub struct ComplCtx<'a> {
     lin_registry: &'a LinRegistry,
 }
 
+#[cfg(feature = "old-completer")]
 /// Find the record field associated with a particular ID in the linearization
 /// using lexical scoping rules.
 fn find_fields_from_term_kind(
@@ -201,6 +209,7 @@ fn find_fields_from_term_kind(
     result.into_iter().chain(contract_result).collect()
 }
 
+#[cfg(feature = "old-completer")]
 /// Find the record fields associated with an ID in the linearization using
 /// its contract information.
 fn find_fields_from_contract(
@@ -233,6 +242,7 @@ fn find_fields_from_contract(
     }
 }
 
+#[cfg(feature = "old-completer")]
 /// Find record field associated with a field's metadata. This can be gotten from the type or the
 /// contracts.
 fn find_fields_from_contracts(
@@ -249,6 +259,7 @@ fn find_fields_from_contracts(
         .collect()
 }
 
+#[cfg(feature = "old-completer")]
 /// Find the fields that can be found from a type.
 fn find_fields_from_type(
     ty: &Type,
@@ -266,6 +277,7 @@ fn find_fields_from_type(
     }
 }
 
+#[cfg(feature = "old-completer")]
 /// Extract the fields from a given record type.
 fn find_fields_from_rrows(
     rrows: &RecordRows,
@@ -305,6 +317,7 @@ fn find_fields_from_rrows(
     }
 }
 
+#[cfg(feature = "old-completer")]
 fn find_fields_from_field(
     field: &Field,
     path: &mut Vec<LocIdent>,
@@ -313,6 +326,7 @@ fn find_fields_from_field(
     find_fields_from_term_with_annot(&field.metadata.annotation, field.value.as_ref(), path, info)
 }
 
+#[cfg(feature = "old-completer")]
 // TODO: impl a trait FindField to avoid having long names
 fn find_fields_from_term_with_annot(
     annot: &TypeAnnotation,
@@ -329,6 +343,7 @@ fn find_fields_from_term_with_annot(
     info_from_metadata
 }
 
+#[cfg(feature = "old-completer")]
 /// Extract record fields from a record term.
 fn find_fields_from_term(
     term: &RichTerm,
@@ -371,6 +386,7 @@ fn find_fields_from_term(
     }
 }
 
+#[cfg(feature = "old-completer")]
 lazy_static! {
     // Unwraps are safe here because we know these are correct regexes. This regexp must be the same
     // as the regex for identifiers in the lexer (nickel_lang_core::parser::lexer)
@@ -378,6 +394,7 @@ lazy_static! {
     static ref RE_SPACE: Regex = Regex::new(r"\s+").unwrap();
 }
 
+#[cfg(feature = "old-completer")]
 /// Get the string chunks that make up an identifier path.
 fn get_identifier_path(text: &str) -> Option<Vec<String>> {
     /// Remove quotes from a record fields name (if any) and return a tuple
@@ -420,6 +437,7 @@ fn get_identifier_path(text: &str) -> Option<Vec<String>> {
     Some(path)
 }
 
+#[cfg(feature = "old-completer")]
 /// Get the identifiers before `.<text>` for record completion.
 fn get_identifiers_before_field(text: &str) -> Option<Vec<String>> {
     // Skip `<text>`
@@ -445,6 +463,7 @@ fn remove_duplicates(items: &Vec<CompletionItem>) -> Vec<CompletionItem> {
     seen
 }
 
+#[cfg(feature = "old-completer")]
 /// Search the linearization to find the record information associated with a
 /// partiular ID, and in the scope of a given linearization item.
 fn collect_record_info(
@@ -507,6 +526,7 @@ fn collect_record_info(
         .unwrap_or_default()
 }
 
+#[cfg(feature = "old-completer")]
 /// As we traverse a nested record all the way to the topmost record,
 /// accumulate all the record metadata and corresponding path.
 fn accumulate_record_meta_data<'a>(
@@ -546,6 +566,7 @@ fn accumulate_record_meta_data<'a>(
     }
 }
 
+#[cfg(feature = "old-completer")]
 /// Generate possible completion identifiers given a source text, its linearization
 /// and the current item the cursor points at.
 fn get_completion_identifiers(
@@ -682,7 +703,8 @@ fn extract_static_path(mut rt: RichTerm) -> (RichTerm, Vec<Ident>) {
     }
 }
 
-fn sanitize_term_for_completion(
+// Try to interpret `term` as a record path to offer completions for.
+fn sanitize_record_path_for_completion(
     term: &RichTerm,
     cursor: RawPos,
     server: &mut Server,
@@ -709,16 +731,68 @@ fn sanitize_term_for_completion(
     }
 }
 
-fn term_based_completion(
-    term: RichTerm,
-    server: &Server,
-) -> Result<Vec<CompletionItem>, ResponseError> {
+fn record_path_completion(term: RichTerm, server: &Server) -> Vec<CompletionItem> {
     log::info!("term based completion path: {term:?}");
 
     let (start_term, path) = extract_static_path(term);
 
     let defs = FieldResolver::new(server).resolve_term_path(&start_term, &path);
-    Ok(defs.iter().flat_map(FieldHaver::completion_items).collect())
+    defs.iter().flat_map(FieldHaver::completion_items).collect()
+}
+
+fn env_completion(rt: &RichTerm, server: &Server) -> Vec<CompletionItem> {
+    let env = server.lin_registry.get_env(rt).cloned().unwrap_or_default();
+    let resolver = FieldResolver::new(server);
+    let mut items: Vec<_> = env
+        .iter_elems()
+        .map(|(_, def_with_path)| def_with_path.completion_item())
+        .collect();
+
+    // If the current term is a record, add its fields. (They won't be in the environment,
+    // because that's the environment *of* the current term. And we don't want to treat
+    // all possible FieldHavers here, because for example if the current term is a Term::Var
+    // that references a record, we don't want it.)
+    if matches!(rt.as_ref(), Term::RecRecord(..)) {
+        items.extend(
+            resolver
+                .resolve_term(rt)
+                .iter()
+                .flat_map(FieldHaver::completion_items),
+        );
+    }
+
+    // Iterate through all ancestors of our term, looking for identifiers that are "in scope"
+    // because they're in an uncle/aunt/cousin that gets merged into our direct ancestors.
+    if let Some(parents) = server.lin_registry.get_parent_chain(rt) {
+        // We're only interested in adding identifiers from terms that are records or
+        // merges/annotations of records. But actually we can skip the records, because any
+        // records that are our direct ancestor have already contributed to `env`.
+        let env_term = |rt: &RichTerm| {
+            matches!(
+                rt.as_ref(),
+                Term::Op2(BinaryOp::Merge(_), _, _) | Term::Annotated(_, _)
+            )
+        };
+
+        let mut parents = parents.peekable();
+        while let Some(rt) = parents.next() {
+            // If a parent and a grandparent were both merges, we can skip the parent
+            // because the grandparent will have a superset of its fields. This prevents
+            // quadratic behavior on long chains of merges.
+            if let Some(gp) = parents.peek() {
+                if env_term(gp) {
+                    continue;
+                }
+            }
+
+            if env_term(rt) {
+                let records = resolver.resolve_term(rt);
+                items.extend(records.iter().flat_map(FieldHaver::completion_items));
+            }
+        }
+    }
+
+    items
 }
 
 pub fn handle_completion(
@@ -758,11 +832,13 @@ pub fn handle_completion(
 
     let sanitized_term = term
         .as_ref()
-        .and_then(|rt| sanitize_term_for_completion(rt, cursor, server));
+        .and_then(|rt| sanitize_record_path_for_completion(rt, cursor, server));
 
-    let mut completions = match sanitized_term {
-        Some(sanitized) => term_based_completion(sanitized, server)?,
-        None => Vec::new(),
+    #[allow(unused_mut)] // needs to be mut with feature = old-completer
+    let mut completions = match (sanitized_term, term) {
+        (Some(sanitized), _) => record_path_completion(sanitized, server),
+        (_, Some(term)) => env_completion(&term, server),
+        (None, None) => Vec::new(),
     };
 
     log::info!("term-based completion provided {completions:?}");
@@ -866,6 +942,7 @@ fn handle_import_completion(
     Ok(completions)
 }
 
+#[cfg(feature = "old-completer")]
 #[cfg(test)]
 mod tests {
     use super::*;
diff --git a/lsp/nls/src/term.rs b/lsp/nls/src/term.rs
index e7ba5637..a12ce81f 100644
--- a/lsp/nls/src/term.rs
+++ b/lsp/nls/src/term.rs
@@ -6,19 +6,19 @@ use nickel_lang_core::{
     term::{RichTerm, SharedTerm, Term},
 };
 
-// A term that uses source position and a pointer to Term to implement Eq and Hash.
+// A term that uses a pointer to Term to implement Eq and Hash.
 #[derive(Clone, Debug)]
 pub struct RichTermPtr(pub RichTerm);
 
 impl PartialEq for RichTermPtr {
     fn eq(&self, other: &Self) -> bool {
-        self.0.pos == other.0.pos && SharedTerm::ptr_eq(&self.0.term, &other.0.term)
+        SharedTerm::ptr_eq(&self.0.term, &other.0.term)
     }
 }
 
 impl Hash for RichTermPtr {
     fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
-        (self.0.pos, self.0.term.as_ref() as *const Term).hash(state)
+        (self.0.term.as_ref() as *const Term).hash(state)
     }
 }
 
diff --git a/lsp/nls/src/usage.rs b/lsp/nls/src/usage.rs
index 2b9628ee..8819a289 100644
--- a/lsp/nls/src/usage.rs
+++ b/lsp/nls/src/usage.rs
@@ -126,84 +126,81 @@ impl UsageLookup {
     }
 
     fn fill(&mut self, rt: &RichTerm, env: &Environment) {
-        rt.traverse_ref(&mut |term: &RichTerm| {
-            if let Some(span) = term.pos.as_opt_ref() {
-                self.def_table.insert(*span, env.clone());
-            }
-
-            match term.term.as_ref() {
-                Term::Fun(id, body) => {
-                    let mut new_env = env.clone();
-                    new_env.def_noval(*id, None);
-                    self.fill(body, &new_env);
-                    TraverseControl::SkipBranch
+        rt.traverse_ref(
+            &mut |term: &RichTerm, env: &Environment| {
+                if let Some(span) = term.pos.as_opt_ref() {
+                    self.def_table.insert(*span, env.clone());
                 }
-                Term::FunPattern(maybe_id, pat, body) => {
-                    let mut new_env = env.clone();
-                    if let Some(id) = maybe_id {
+
+                match term.term.as_ref() {
+                    Term::Fun(id, _body) => {
+                        let mut new_env = env.clone();
                         new_env.def_noval(*id, None);
+                        TraverseControl::ContinueWithScope(new_env)
                     }
+                    Term::FunPattern(maybe_id, pat, _body) => {
+                        let mut new_env = env.clone();
+                        if let Some(id) = maybe_id {
+                            new_env.def_noval(*id, None);
+                        }
 
-                    for m in &pat.matches {
-                        for (_path, id, field) in m.to_flattened_bindings() {
-                            new_env.def_noval(id, Some(field.metadata));
+                        for m in &pat.matches {
+                            for (_path, id, field) in m.to_flattened_bindings() {
+                                new_env.def_noval(id, Some(field.metadata));
+                            }
                         }
+                        TraverseControl::ContinueWithScope(new_env)
                     }
-                    self.fill(body, &new_env);
-                    TraverseControl::SkipBranch
-                }
-                Term::Let(id, val, body, attrs) => {
-                    let mut new_env = env.clone();
-                    new_env.def(*id, Some(val.clone()), None);
+                    Term::Let(id, val, body, attrs) => {
+                        let mut new_env = env.clone();
+                        new_env.def(*id, Some(val.clone()), None);
 
-                    self.fill(val, if attrs.rec { &new_env } else { env });
-                    self.fill(body, &new_env);
+                        self.fill(val, if attrs.rec { &new_env } else { env });
+                        self.fill(body, &new_env);
 
-                    TraverseControl::SkipBranch
-                }
-                Term::LetPattern(maybe_id, pat, val, body) => {
-                    let mut new_env = env.clone();
-                    if let Some(id) = maybe_id {
-                        new_env.def(*id, Some(val.clone()), None);
+                        TraverseControl::SkipBranch
                     }
+                    Term::LetPattern(maybe_id, pat, val, _body) => {
+                        let mut new_env = env.clone();
+                        if let Some(id) = maybe_id {
+                            new_env.def(*id, Some(val.clone()), None);
+                        }
 
-                    for m in &pat.matches {
-                        for (path, id, field) in m.to_flattened_bindings() {
-                            let path = path.iter().map(|i| i.ident()).rev().collect();
-                            let term = TermAtPath {
-                                term: val.clone(),
-                                path,
-                            };
-                            new_env.def(id, Some(term), Some(field.metadata));
+                        for m in &pat.matches {
+                            for (path, id, field) in m.to_flattened_bindings() {
+                                let path = path.iter().map(|i| i.ident()).rev().collect();
+                                let term = TermAtPath {
+                                    term: val.clone(),
+                                    path,
+                                };
+                                new_env.def(id, Some(term), Some(field.metadata));
+                            }
                         }
+                        TraverseControl::ContinueWithScope(new_env)
                     }
-                    self.fill(body, &new_env);
-                    TraverseControl::SkipBranch
-                }
-                Term::RecRecord(data, _interp_fields, _deps) => {
-                    let mut new_env = env.clone();
+                    Term::RecRecord(data, _interp_fields, _deps) => {
+                        let mut new_env = env.clone();
 
-                    // Records are recursive and the order of fields is unimportant, so define
-                    // all the fields in the environment and then recurse into their values.
-                    for (id, field) in &data.fields {
-                        new_env.def(*id, field.value.clone(), Some(field.metadata.clone()));
-                    }
+                        // Records are recursive and the order of fields is unimportant, so define
+                        // all the fields in the environment and then recurse into their values.
+                        for (id, field) in &data.fields {
+                            new_env.def(*id, field.value.clone(), Some(field.metadata.clone()));
+                        }
 
-                    for val in data.fields.values().filter_map(|fld| fld.value.as_ref()) {
-                        self.fill(val, &new_env);
+                        TraverseControl::ContinueWithScope(new_env)
                     }
-                    TraverseControl::SkipBranch
-                }
-                Term::Var(id) => {
-                    let id = LocIdent::from(*id);
-                    if let Some(def) = env.get(&id.ident) {
-                        self.usage_table.entry(def.ident).or_default().push(id);
+                    Term::Var(id) => {
+                        let id = LocIdent::from(*id);
+                        if let Some(def) = env.get(&id.ident) {
+                            self.usage_table.entry(def.ident).or_default().push(id);
+                        }
+                        TraverseControl::Continue
                     }
-                    TraverseControl::Continue
+                    _ => TraverseControl::<_, ()>::Continue,
                 }
-                _ => TraverseControl::<()>::Continue,
-            }
-        });
+            },
+            env,
+        );
     }
 }
 
diff --git a/notes/fixing-sealing-and-recursive-records.md b/notes/fixing-sealing-and-recursive-records.md
index 8a4a1f69..24d2046c 100644
--- a/notes/fixing-sealing-and-recursive-records.md
+++ b/notes/fixing-sealing-and-recursive-records.md
@@ -125,9 +125,9 @@ Op1(record_map, record); {stack..}
 record ~ RecRecord {..}
 
 RECORD{ foo |pending Num = %1, bar |pending [PosNat,Even] = %2}
-%2 := (%assume% Num label %1) + 1
+%2 := (%apply_contract% Num label %1) + 1
 
-RECORD{ foo = f (%assume% Num %1), bar = f (%assume% PosNat,Even %2) }
+RECORD{ foo = f (%apply_contract% Num %1), bar = f (%apply_contract% PosNat,Even %2) }
 
 # With a call to pending_contract.dualize()
 


Test patch:
diff --git a/lsp/nls/tests/inputs/completion-patterns.ncl b/lsp/nls/tests/inputs/completion-patterns.ncl
index d1278288..2f042ef3 100644
--- a/lsp/nls/tests/inputs/completion-patterns.ncl
+++ b/lsp/nls/tests/inputs/completion-patterns.ncl
@@ -23,23 +23,45 @@ in
 ### type = "Completion"
 ### textDocument.uri = "file:///input.ncl"
 ### position = { line = 13, character = 18 }
+###
 ### [[request]]
 ### type = "Completion"
 ### textDocument.uri = "file:///input.ncl"
 ### position = { line = 14, character = 22 }
+###
 ### [[request]]
 ### type = "Completion"
 ### textDocument.uri = "file:///input.ncl"
 ### position = { line = 15, character = 26 }
+###
 ### [[request]]
 ### type = "Completion"
 ### textDocument.uri = "file:///input.ncl"
 ### position = { line = 16, character = 18 }
+###
 ### [[request]]
 ### type = "Completion"
 ### textDocument.uri = "file:///input.ncl"
 ### position = { line = 17, character = 22 }
+###
 ### [[request]]
 ### type = "Completion"
 ### textDocument.uri = "file:///input.ncl"
 ### position = { line = 18, character = 22 }
+###
+### # Env completions
+###
+### [[request]]
+### type = "Completion"
+### textDocument.uri = "file:///input.ncl"
+### position = { line = 1, character = 3 }
+###
+### [[request]]
+### type = "Completion"
+### textDocument.uri = "file:///input.ncl"
+### position = { line = 3, character = 5 }
+###
+### [[request]]
+### type = "Completion"
+### textDocument.uri = "file:///input.ncl"
+### position = { line = 5, character = 6 }
diff --git a/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__completion-basic.ncl.snap b/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__completion-basic.ncl.snap
index bf38fc79..eeb232e0 100644
--- a/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__completion-basic.ncl.snap
+++ b/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__completion-basic.ncl.snap
@@ -11,10 +11,10 @@ expression: output
 [foo, really, verified, version]
 ["has a space", lalala]
 [falala]
-[config, field]
 [field]
-[config, subfield]
-[config, f, foo]
-[config, field]
-[config, field]
+[field]
+[subfield]
+[foo]
+[field]
+[field]
 
diff --git a/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__completion-patterns.ncl.snap b/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__completion-patterns.ncl.snap
index f19fb1c0..77274bd3 100644
--- a/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__completion-patterns.ncl.snap
+++ b/lsp/nls/tests/snapshots/main__lsp__nls__tests__inputs__completion-patterns.ncl.snap
@@ -2,10 +2,13 @@
 source: lsp/nls/tests/main.rs
 expression: output
 ---
+[extra, foo]
+[bar, more]
+[baz, most]
+[bar, more]
+[baz, most]
+[baz, most]
 [extra, foo, inner, innermost, outer]
-[bar, inner, innermost, more, outer]
-[baz, inner, innermost, most, outer]
-[bar, inner, innermost, more, outer]
-[baz, inner, innermost, most, outer]
-[baz, inner, innermost, most, outer]
+[bar, extra, foo, inner, innermost, more, outer]
+[bar, baz, extra, foo, inner, innermost, more, most, outer]