Repository: tweag/nickel
Pull request #509 (2021-12-22 21:09:37)

Fix contract application
Initially, contracts have been simply functions, that we just applied to a label and a value. This is not true anymore, as contracts can now be records. Even for functions, contract application is different from plain function application, as it does additional book-keeping for better error reporting.

The stdlib, and in particular the `contracts` part, keeps considering contract as functions, simply applying them. To cope with that, the `open_contract` transformation wraps every subcontract as a function of the form `fun label value => %assume% contract label value`. This PR inverses the workflow: it makes the functions from the stdlib not assume anymore that what they receive is a readily applicable function, but any contract. Doing so, they can now be used with any contract, and not only the one generated by `open_contract`. `open_contract` is free from wrapping every subcontract it encounters.

To do so, this PRs re-introduces `%assume%` as a first-class operator. It also makes it available in the stdlib to users as the `contracts.apply` function.

The concrete motivations of this change are:

- the initial issue was that the whole contract application phase was losing position information, giving unlocated `missing field definition`. Because `open_contract` was the one introducing the `%assume%`, it would need to be threaded with position information to solve the issue. Here, `open_contract` don't care about `assume` anymore. The contract application transformation is now responsible for this, and can set the positions as needed.
- the contract implementations from the stdlib are more resilient. We dropped the pre-condition that anything passed to them must be of the form `fun label value => %assume% contract label value.` They now accept any kind of contract,and are more in line with what a custom contract should be. This will also help for the implementation of #573.

dpulls[bot]: :tada: All dependencies have been resolved !

Patch:
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 5c52f28b..abc99361 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -524,6 +524,7 @@ InfixExpr: RichTerm = {
 }
 
 BOpPre: BinaryOp = {
+    "assume" => BinaryOp::Assume(),
     "unwrap" => BinaryOp::Unwrap(),
     "go_field" => BinaryOp::GoField(),
     "has_field" => BinaryOp::HasField(),
@@ -699,6 +700,7 @@ extern {
         "is_fun" => Token::Normal(NormalToken::IsFun),
         "is_list" => Token::Normal(NormalToken::IsList),
         "is_record" => Token::Normal(NormalToken::IsRecord),
+        "assume" => Token::Normal(NormalToken::Assume),
         "blame" => Token::Normal(NormalToken::Blame),
         "chng_pol" => Token::Normal(NormalToken::ChangePol),
         "polarity" => Token::Normal(NormalToken::Polarity),
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 16d2989e..322843df 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -162,6 +162,8 @@ pub enum NormalToken<'input> {
     #[token("%is_record%")]
     IsRecord,
 
+    #[token("%assume%")]
+    Assume,
     #[token("%blame%")]
     Blame,
     #[token("%chng_pol%")]
diff --git a/src/transform/apply_contracts.rs b/src/transform/apply_contracts.rs
index a74664d2..ab1f02fd 100644
--- a/src/transform/apply_contracts.rs
+++ b/src/transform/apply_contracts.rs
@@ -8,7 +8,7 @@
 //!
 //! It must be run before `share_normal_form` to avoid rechecking contracts each time the inner
 //! value is unwrapped.
-use crate::term::{RichTerm, Term};
+use crate::term::{make as mk_term, BinaryOp, RichTerm, Term};
 use crate::{match_sharedterm, mk_app};
 
 /// If the top-level node of the AST is a meta-value, apply the meta-value's contracts to the inner
@@ -19,15 +19,20 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
         with {
             Term::MetaValue(meta) if meta.value.is_some() => {
                 let mut meta = meta;
+                let pos_inh = pos.into_inherited();
                 let inner = meta.types.iter().chain(meta.contracts.iter()).fold(
                     meta.value.take().unwrap(),
                     |acc, ctr| {
                         mk_app!(
-                            ctr.types.clone().contract(),
-                            Term::Lbl(ctr.label.clone()),
+                            mk_term::op2(
+                                BinaryOp::Assume(),
+                                ctr.types.contract(),
+                                Term::Lbl(ctr.label.clone())
+                            )
+                            .with_pos(pos_inh),
                             acc
                         )
-                        .with_pos(pos)
+                        .with_pos(pos_inh)
                     },
                 );
 
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index a782905e..607063a7 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -192,11 +192,11 @@ pub fn type_check<LL>(
     mut linearizer: LL,
 ) -> Result<(Types, LL::Completed), TypecheckError>
 where
-    LL: Linearizer<CompletionExtra = (UnifTable, HashMap<usize, Ident>)>,
+    LL: Linearizer<CompletionExtra = (HashMap<usize, Option<TypeWrapper>>, HashMap<usize, Ident>)>,
 {
     let (mut table, mut names) = (UnifTable::new(), HashMap::new());
     let mut building = Linearization::new(LL::Building::default());
-    let ty = table.fresh_unif_var();
+    let ty = TypeWrapper::Ptr(new_var(&mut table));
 
     {
         let mut state: State = State {
@@ -217,10 +217,10 @@ where
         )?;
     }
 
-    let result = to_type(&table, ty);
-    let lin = linearizer.complete(building, (table, names)).into_inner();
-
-    Ok((result, lin))
+    let lin = linearizer
+        .complete(building, (table.clone(), names))
+        .into_inner();
+    Ok((to_type(&table, ty), lin))
 }
 
 /// Typecheck a term using the given global typing environment. Same as
@@ -244,7 +244,7 @@ pub fn type_check_in_env(
         constr: &mut RowConstr::new(),
         names: &mut HashMap::new(),
     };
-    let ty = state.table.fresh_unif_var();
+    let ty = TypeWrapper::Ptr(new_var(state.table));
     type_check_(
         &mut state,
         Envs::from_global(global),
@@ -340,11 +340,11 @@ fn type_check_<L: Linearizer>(
             )
         }
         Term::Fun(x, t) => {
-            let src = state.table.fresh_unif_var();
+            let src = TypeWrapper::Ptr(new_var(state.table));
             // TODO what to do here, this makes more sense to me, but it means let x = foo in bar
             // behaves quite different to (\x.bar) foo, worth considering if it's ok to type these two differently
             // let src = TypeWrapper::The(AbsType::Dyn());
-            let trg = state.table.fresh_unif_var();
+            let trg = TypeWrapper::Ptr(new_var(state.table));
             let arr = mk_tyw_arrow!(src.clone(), trg.clone());
             linearizer.retype_ident(lin, x, src.clone());
 
@@ -354,10 +354,10 @@ fn type_check_<L: Linearizer>(
             type_check_(state, envs, lin, linearizer, strict, t, trg)
         }
         Term::FunPattern(x, pat, t) => {
-            let src = state.table.fresh_unif_var();
+            let src = TypeWrapper::Ptr(new_var(state.table));
             // TODO what to do here, this makes more sense to me, but it means let x = foo in bar
             // behaves quite different to (\x.bar) foo, worth considering if it's ok to type these two differently
-            let trg = state.table.fresh_unif_var();
+            let trg = TypeWrapper::Ptr(new_var(state.table));
             let arr = mk_tyw_arrow!(src.clone(), trg.clone());
             if let Some(x) = x {
                 linearizer.retype_ident(lin, x, src.clone());
@@ -368,7 +368,7 @@ fn type_check_<L: Linearizer>(
             type_check_(state, envs, lin, linearizer, strict, t, trg)
         }
         Term::List(terms) => {
-            let ty_elts = state.table.fresh_unif_var();
+            let ty_elts = TypeWrapper::Ptr(new_var(state.table));
 
             unify(state, strict, ty, mk_typewrapper::list(ty_elts.clone()))
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
@@ -430,7 +430,7 @@ fn type_check_<L: Linearizer>(
             type_check_(state, envs, lin, linearizer, strict, rt, ty)
         }
         Term::App(e, t) => {
-            let src = state.table.fresh_unif_var();
+            let src = TypeWrapper::Ptr(new_var(state.table));
             let arr = mk_tyw_arrow!(src.clone(), ty);
 
             type_check_(
@@ -447,7 +447,7 @@ fn type_check_<L: Linearizer>(
         Term::Switch(exp, cases, default) => {
             // Currently, if it has a default value, we typecheck the whole thing as
             // taking ANY enum, since it's more permissive and there's no loss of information
-            let res = state.table.fresh_unif_var();
+            let res = TypeWrapper::Ptr(new_var(state.table));
 
             for (choice, case) in cases.values().enumerate() {
                 type_check_(
@@ -472,7 +472,7 @@ fn type_check_<L: Linearizer>(
                         t,
                         res.clone(),
                     )?;
-                    state.table.fresh_unif_var()
+                    TypeWrapper::Ptr(new_var(state.table))
                 }
                 None => cases.iter().try_fold(
                     mk_typewrapper::row_empty(),
@@ -495,14 +495,14 @@ fn type_check_<L: Linearizer>(
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Enum(id) => {
-            let row = state.table.fresh_unif_var();
+            let row = TypeWrapper::Ptr(new_var(state.table));
             unify(state, strict, ty, mk_tyw_enum!(id.clone(), row))
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         // If some fields are defined dynamically, the only potential type that works is `{_ : a}`
         // for some `a`
         Term::RecRecord(stat_map, dynamic, _) if !dynamic.is_empty() => {
-            let ty_dyn = state.table.fresh_unif_var();
+            let ty_dyn = TypeWrapper::Ptr(new_var(state.table));
 
             for id in stat_map.keys() {
                 envs.insert(id.clone(), ty_dyn.clone());
@@ -539,7 +539,7 @@ fn type_check_<L: Linearizer>(
             }
 
             let root_ty = if let TypeWrapper::Ptr(p) = ty {
-                state.table.root(p)
+                get_root(state.table, p)
             } else {
                 ty.clone()
             };
@@ -569,7 +569,7 @@ fn type_check_<L: Linearizer>(
                         let ty = if let Term::RecRecord(..) = t.as_ref() {
                             envs.get(id).unwrap()
                         } else {
-                            state.table.fresh_unif_var()
+                            TypeWrapper::Ptr(new_var(state.table))
                         };
 
                         type_check_(
@@ -738,7 +738,7 @@ fn binding_type(
     let ty_apt = apparent_type(t, Some(envs), Some(resolver));
 
     match ty_apt {
-        ApparentType::Approximated(_) if strict => table.fresh_unif_var(),
+        ApparentType::Approximated(_) if strict => TypeWrapper::Ptr(new_var(table)),
         ty_apt => ty_apt.into(),
     }
 }
@@ -973,7 +973,7 @@ fn row_add(
     mut r: TypeWrapper,
 ) -> Result<(Option<Box<TypeWrapper>>, TypeWrapper), RowUnifError> {
     if let TypeWrapper::Ptr(p) = r {
-        r = state.table.root(p);
+        r = get_root(state.table, p);
     }
     match r {
         TypeWrapper::Concrete(AbsType::RowEmpty()) | TypeWrapper::Concrete(AbsType::Dyn()) => {
@@ -996,15 +996,15 @@ fn row_add(
                     return Err(RowUnifError::UnsatConstr(id.clone(), ty.map(|tyw| *tyw)));
                 }
             }
-            let new_row = state.table.fresh_unif_var();
+            let new_row = TypeWrapper::Ptr(new_var(state.table));
             constraint(state, new_row.clone(), id.clone())?;
-            state.table.assign(
+            state.table.insert(
                 root,
-                TypeWrapper::Concrete(AbsType::RowExtend(
+                Some(TypeWrapper::Concrete(AbsType::RowExtend(
                     id.clone(),
                     ty.clone(),
                     Box::new(new_row.clone()),
-                )),
+                ))),
             );
             Ok((ty, new_row))
         }
@@ -1036,10 +1036,10 @@ pub fn unify_(
     mut t2: TypeWrapper,
 ) -> Result<(), UnifError> {
     if let TypeWrapper::Ptr(pt1) = t1 {
-        t1 = state.table.root(pt1);
+        t1 = get_root(state.table, pt1);
     }
     if let TypeWrapper::Ptr(pt2) = t2 {
-        t2 = state.table.root(pt2);
+        t2 = get_root(state.table, pt2);
     }
 
     // t1 and t2 are roots of the type
@@ -1115,7 +1115,7 @@ pub fn unify_(
             (AbsType::DynRecord(t), AbsType::DynRecord(t2)) => unify_(state, *t, *t2),
             (AbsType::Forall(i1, t1t), AbsType::Forall(i2, t2t)) => {
                 // Very stupid (slow) implementation
-                let constant_type = state.table.fresh_const();
+                let constant_type = TypeWrapper::Constant(new_var(state.table));
 
                 unify_(
                     state,
@@ -1138,13 +1138,13 @@ pub fn unify_(
         (TypeWrapper::Ptr(p), tyw) => {
             constr_unify(state.constr, p, &tyw)
                 .map_err(|err| err.into_unif_err(TypeWrapper::Ptr(p), tyw.clone()))?;
-            state.table.assign(p, tyw);
+            state.table.insert(p, Some(tyw));
             Ok(())
         }
         (tyw, TypeWrapper::Ptr(p)) => {
             constr_unify(state.constr, p, &tyw)
                 .map_err(|err| err.into_unif_err(tyw.clone(), TypeWrapper::Ptr(p)))?;
-            state.table.assign(p, tyw);
+            state.table.insert(p, Some(tyw));
             Ok(())
         }
         (TypeWrapper::Constant(i1), TypeWrapper::Constant(i2)) if i1 == i2 => Ok(()),
@@ -1220,7 +1220,7 @@ pub fn unify_rows(
 /// as type constants are replaced with the type `Dyn`.
 fn to_type(table: &UnifTable, ty: TypeWrapper) -> Types {
     match ty {
-        TypeWrapper::Ptr(p) => match table.root(p) {
+        TypeWrapper::Ptr(p) => match get_root(table, p) {
             t @ TypeWrapper::Concrete(_) => to_type(table, t),
             _ => Types(AbsType::Dyn()),
         },
@@ -1257,11 +1257,11 @@ enum ForallInst {
 /// - `inst`: the type of instantiation, either by a type constant or by a unification variable
 fn instantiate_foralls(state: &mut State, mut ty: TypeWrapper, inst: ForallInst) -> TypeWrapper {
     if let TypeWrapper::Ptr(p) = ty {
-        ty = state.table.root(p);
+        ty = get_root(state.table, p);
     }
 
     while let TypeWrapper::Concrete(AbsType::Forall(id, forall_ty)) = ty {
-        let fresh_id = state.table.fresh_var();
+        let fresh_id = new_var(state.table);
         let var = match inst {
             ForallInst::Constant => TypeWrapper::Constant(fresh_id),
             ForallInst::Ptr => TypeWrapper::Ptr(fresh_id),
@@ -1282,58 +1282,7 @@ fn instantiate_foralls(state: &mut State, mut ty: TypeWrapper, inst: ForallInst)
 /// Map each unification variable to either another type variable or a concrete type it has been
 /// unified with. Each binding `(ty, var)` in this map should be thought of an edge in a
 /// unification graph.
-pub struct UnifTable(Vec<Option<TypeWrapper>>);
-
-impl UnifTable {
-    pub fn new() -> Self {
-        UnifTable(Vec::new())
-    }
-
-    /// Assign a type to a unification variable.
-    pub fn assign(&mut self, var: usize, tyw: TypeWrapper) {
-        debug_assert!(self.0[var].is_none());
-        self.0[var] = Some(tyw);
-    }
-
-    /// Retrieve the current assignement of a unification variable.
-    pub fn get(&self, var: usize) -> Option<&TypeWrapper> {
-        self.0[var].as_ref()
-    }
-
-    /// Create a fresh variable identifier and allocate a corresponding slot in the table.
-    fn fresh_var(&mut self) -> usize {
-        let next = self.0.len();
-        self.0.push(None);
-        next
-    }
-
-    /// Create a fresh unification variable and allocate a corresponding slot in the table.
-    pub fn fresh_unif_var(&mut self) -> TypeWrapper {
-        TypeWrapper::Ptr(self.fresh_var())
-    }
-
-    /// Create a fresh type constant.
-    pub fn fresh_const(&mut self) -> TypeWrapper {
-        TypeWrapper::Constant(self.fresh_var())
-    }
-
-    /// Follow the links in the unification table to find the representative of the equivalence class
-    /// of unification variable `x`.
-    ///
-    /// This corresponds to the find in union-find.
-    // TODO This should be a union find like algorithm
-    pub fn root(&self, x: usize) -> TypeWrapper {
-        // All queried variable must have been introduced by `new_var` and thus a corresponding entry
-        // must always exist in `state`. If not, the typechecking algorithm is not correct, and we
-        // panic.
-        match &self.0[x] {
-            None => TypeWrapper::Ptr(x),
-            Some(TypeWrapper::Ptr(y)) => self.root(*y),
-            Some(ty @ TypeWrapper::Concrete(_)) => ty.clone(),
-            Some(k @ TypeWrapper::Constant(_)) => k.clone(),
-        }
-    }
-}
+pub type UnifTable = HashMap<usize, Option<TypeWrapper>>;
 
 /// Row constraints.
 ///
@@ -1343,12 +1292,19 @@ impl UnifTable {
 /// String}`.
 pub type RowConstr = HashMap<usize, HashSet<Ident>>;
 
+/// Create a fresh unification variable.
+fn new_var(table: &mut UnifTable) -> usize {
+    let next = table.len();
+    table.insert(next, None);
+    next
+}
+
 /// Add a row constraint on a type.
 ///
 /// See [`RowConstr`](type.RowConstr.html).
 fn constraint(state: &mut State, x: TypeWrapper, id: Ident) -> Result<(), RowUnifError> {
     match x {
-        TypeWrapper::Ptr(p) => match state.table.root(p) {
+        TypeWrapper::Ptr(p) => match get_root(state.table, p) {
             ty @ TypeWrapper::Concrete(_) => constraint(state, ty, id),
             TypeWrapper::Ptr(root) => {
                 if let Some(v) = state.constr.get_mut(&root) {
@@ -1383,7 +1339,7 @@ fn constraint(state: &mut State, x: TypeWrapper, id: Ident) -> Result<(), RowUni
 ///
 /// Because `constraint_var` should be called on a fresh unification variable `p`, the following is
 /// assumed:
-/// - `state.table.root_of(p) == p`
+/// - `get_root(state.table, p) == p`
 /// - `state.constr.get(&p) == None`
 fn constrain_var(state: &mut State, tyw: &TypeWrapper, p: usize) {
     fn constrain_var_(state: &mut State, mut constr: HashSet<Ident>, tyw: &TypeWrapper, p: usize) {
@@ -1391,7 +1347,7 @@ fn constrain_var(state: &mut State, tyw: &TypeWrapper, p: usize) {
             TypeWrapper::Ptr(u) if p == *u && !constr.is_empty() => {
                 state.constr.insert(p, constr);
             }
-            TypeWrapper::Ptr(u) => match state.table.root(*u) {
+            TypeWrapper::Ptr(u) => match get_root(state.table, *u) {
                 TypeWrapper::Ptr(_) => (),
                 tyw => constrain_var_(state, constr, &tyw, p),
             },
@@ -1478,3 +1434,20 @@ pub fn constr_unify(
         Ok(())
     }
 }
+
+/// Follow the links in the unification table to find the representative of the equivalence class
+/// of unification variable `x`.
+///
+/// This corresponds to the find in union-find.
+// TODO This should be a union find like algorithm
+pub fn get_root(table: &UnifTable, x: usize) -> TypeWrapper {
+    // All queried variable must have been introduced by `new_var` and thus a corresponding entry
+    // must always exist in `state`. If not, the typechecking algorithm is not correct, and we
+    // panic.
+    match table.get(&x).unwrap() {
+        None => TypeWrapper::Ptr(x),
+        Some(TypeWrapper::Ptr(y)) => get_root(table, *y),
+        Some(ty @ TypeWrapper::Concrete(_)) => ty.clone(),
+        Some(k @ TypeWrapper::Constant(_)) => k.clone(),
+    }
+}
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index 8f437093..ac4efd64 100644
--- a/src/typecheck/operation.rs
+++ b/src/typecheck/operation.rs
@@ -15,7 +15,7 @@ pub fn get_uop_type(
     Ok(match op {
         // forall a. bool -> a -> a -> a
         UnaryOp::Ite() => {
-            let branches = TypeWrapper::Ptr(state.table.fresh_var());
+            let branches = TypeWrapper::Ptr(new_var(state.table));
 
             (
                 mk_typewrapper::bool(),
@@ -29,7 +29,7 @@ pub fn get_uop_type(
         | UnaryOp::IsFun()
         | UnaryOp::IsList()
         | UnaryOp::IsRecord() => {
-            let inp = TypeWrapper::Ptr(state.table.fresh_var());
+            let inp = TypeWrapper::Ptr(new_var(state.table));
             (inp, mk_typewrapper::bool())
         }
         // Bool -> Bool -> Bool
@@ -41,7 +41,7 @@ pub fn get_uop_type(
         UnaryOp::BoolNot() => (mk_typewrapper::bool(), mk_typewrapper::bool()),
         // forall a. Dyn -> a
         UnaryOp::Blame() => {
-            let res = TypeWrapper::Ptr(state.table.fresh_var());
+            let res = TypeWrapper::Ptr(new_var(state.table));
 
             (mk_typewrapper::dynamic(), res)
         }
@@ -49,7 +49,7 @@ pub fn get_uop_type(
         UnaryOp::Pol() => (mk_typewrapper::dynamic(), mk_typewrapper::bool()),
         // forall rows. < | rows> -> <id | rows>
         UnaryOp::Embed(id) => {
-            let row = TypeWrapper::Ptr(state.table.fresh_var());
+            let row = TypeWrapper::Ptr(new_var(state.table));
             // Constraining a freshly created variable should never fail.
             constraint(state, row.clone(), id.clone()).unwrap();
             (mk_tyw_enum!(row.clone()), mk_tyw_enum!(id.clone(), row))
@@ -67,15 +67,15 @@ pub fn get_uop_type(
         ),
         // forall rows a. { id: a | rows} -> a
         UnaryOp::StaticAccess(id) => {
-            let row = TypeWrapper::Ptr(state.table.fresh_var());
-            let res = TypeWrapper::Ptr(state.table.fresh_var());
+            let row = TypeWrapper::Ptr(new_var(state.table));
+            let res = TypeWrapper::Ptr(new_var(state.table));
 
             (mk_tyw_record!((id.clone(), res.clone()); row), res)
         }
         // forall a b. List a -> (a -> b) -> List b
         UnaryOp::ListMap() => {
-            let a = TypeWrapper::Ptr(state.table.fresh_var());
-            let b = TypeWrapper::Ptr(state.table.fresh_var());
+            let a = TypeWrapper::Ptr(new_var(state.table));
+            let b = TypeWrapper::Ptr(new_var(state.table));
 
             let f_type = mk_tyw_arrow!(a.clone(), b.clone());
             (
@@ -85,7 +85,7 @@ pub fn get_uop_type(
         }
         // forall a. Num -> (Num -> a) -> List a
         UnaryOp::ListGen() => {
-            let a = TypeWrapper::Ptr(state.table.fresh_var());
+            let a = TypeWrapper::Ptr(new_var(state.table));
 
             let f_type = mk_tyw_arrow!(AbsType::Num(), a.clone());
             (
@@ -98,8 +98,8 @@ pub fn get_uop_type(
             // Assuming f has type Str -> a -> b,
             // this has type DynRecord(a) -> DynRecord(b)
 
-            let a = TypeWrapper::Ptr(state.table.fresh_var());
-            let b = TypeWrapper::Ptr(state.table.fresh_var());
+            let a = TypeWrapper::Ptr(new_var(state.table));
+            let b = TypeWrapper::Ptr(new_var(state.table));
 
             let f_type = mk_tyw_arrow!(AbsType::Str(), a.clone(), b.clone());
             (
@@ -109,19 +109,19 @@ pub fn get_uop_type(
         }
         // forall a b. a -> b -> b
         UnaryOp::Seq() | UnaryOp::DeepSeq() => {
-            let fst = TypeWrapper::Ptr(state.table.fresh_var());
-            let snd = TypeWrapper::Ptr(state.table.fresh_var());
+            let fst = TypeWrapper::Ptr(new_var(state.table));
+            let snd = TypeWrapper::Ptr(new_var(state.table));
 
             (fst, mk_tyw_arrow!(snd.clone(), snd))
         }
         // forall a. List a -> a
         UnaryOp::ListHead() => {
-            let ty_elt = TypeWrapper::Ptr(state.table.fresh_var());
+            let ty_elt = TypeWrapper::Ptr(new_var(state.table));
             (mk_typewrapper::list(ty_elt.clone()), ty_elt)
         }
         // forall a. List a -> List a
         UnaryOp::ListTail() => {
-            let ty_elt = TypeWrapper::Ptr(state.table.fresh_var());
+            let ty_elt = TypeWrapper::Ptr(new_var(state.table));
             (
                 mk_typewrapper::list(ty_elt.clone()),
                 mk_typewrapper::list(ty_elt),
@@ -129,7 +129,7 @@ pub fn get_uop_type(
         }
         // forall a. List a -> Num
         UnaryOp::ListLength() => {
-            let ty_elt = TypeWrapper::Ptr(state.table.fresh_var());
+            let ty_elt = TypeWrapper::Ptr(new_var(state.table));
             (mk_typewrapper::list(ty_elt), mk_typewrapper::num())
         }
         // This should not happen, as ChunksConcat() is only produced during evaluation.
@@ -138,7 +138,7 @@ pub fn get_uop_type(
         // Dyn -> List Str
         UnaryOp::FieldsOf() => (
             mk_typewrapper::dynamic(),
-            //mk_tyw_record!(; TypeWrapper::Ptr(state.table.fresh_var())),
+            //mk_tyw_record!(; TypeWrapper::Ptr(new_var(state.table))),
             mk_typewrapper::list(AbsType::Str()),
         ),
         // Dyn -> List
@@ -197,9 +197,14 @@ pub fn get_bop_type(
             mk_typewrapper::str(),
             mk_typewrapper::str(),
         ),
+        // Ideally: Contract -> Label -> Dyn -> Dyn
+        // Currenty: Dyn -> Dyn -> (Dyn -> Dyn)
+        BinaryOp::Assume() => (
+            mk_typewrapper::dynamic(),
+            mk_typewrapper::dynamic(),
+            mk_tyw_arrow!(mk_typewrapper::dynamic(), mk_typewrapper::dynamic()),
+        ),
         // Sym -> Dyn -> Dyn -> Dyn
-        // This should not happen, as `ApplyContract()` is only produced during evaluation.
-        BinaryOp::Assume() => panic!("cannot typecheck assume"),
         BinaryOp::Unwrap() => (
             mk_typewrapper::sym(),
             mk_typewrapper::dynamic(),
@@ -213,8 +218,8 @@ pub fn get_bop_type(
         ),
         // forall a b. a -> b -> Bool
         BinaryOp::Eq() => (
-            TypeWrapper::Ptr(state.table.fresh_var()),
-            TypeWrapper::Ptr(state.table.fresh_var()),
+            TypeWrapper::Ptr(new_var(state.table)),
+            TypeWrapper::Ptr(new_var(state.table)),
             mk_typewrapper::bool(),
         ),
         // Num -> Num -> Bool
@@ -234,7 +239,7 @@ pub fn get_bop_type(
         ),
         // forall a. Str -> { _ : a} -> a
         BinaryOp::DynAccess() => {
-            let res = TypeWrapper::Ptr(state.table.fresh_var());
+            let res = TypeWrapper::Ptr(new_var(state.table));
 
             (
                 mk_typewrapper::str(),
@@ -244,7 +249,7 @@ pub fn get_bop_type(
         }
         // forall a. Str -> { _ : a } -> a -> { _ : a }
         BinaryOp::DynExtend() => {
-            let res = TypeWrapper::Ptr(state.table.fresh_var());
+            let res = TypeWrapper::Ptr(new_var(state.table));
             (
                 mk_typewrapper::str(),
                 mk_typewrapper::dyn_record(res.clone()),
@@ -253,7 +258,7 @@ pub fn get_bop_type(
         }
         // forall a. Str -> { _ : a } -> { _ : a}
         BinaryOp::DynRemove() => {
-            let res = TypeWrapper::Ptr(state.table.fresh_var());
+            let res = TypeWrapper::Ptr(new_var(state.table));
 
             (
                 mk_typewrapper::str(),
@@ -269,13 +274,13 @@ pub fn get_bop_type(
         ),
         // forall a. List a -> List a -> List a
         BinaryOp::ListConcat() => {
-            let ty_elt = TypeWrapper::Ptr(state.table.fresh_var());
+            let ty_elt = TypeWrapper::Ptr(new_var(state.table));
             let ty_list = mk_typewrapper::list(ty_elt);
             (ty_list.clone(), ty_list.clone(), ty_list)
         }
         // forall a. List a -> Num -> a
         BinaryOp::ListElemAt() => {
-            let ty_elt = TypeWrapper::Ptr(state.table.fresh_var());
+            let ty_elt = TypeWrapper::Ptr(new_var(state.table));
             (
                 mk_typewrapper::list(ty_elt.clone()),
                 mk_typewrapper::num(),
@@ -302,7 +307,7 @@ pub fn get_bop_type(
         ),
         // forall a. <Json, Yaml, Toml> -> a -> Str
         BinaryOp::Serialize() => {
-            let ty_input = TypeWrapper::Ptr(state.table.fresh_var());
+            let ty_input = TypeWrapper::Ptr(new_var(state.table));
             (
                 mk_tyw_enum!("Json", "Yaml", "Toml", mk_typewrapper::row_empty()),
                 ty_input,
diff --git a/src/typecheck/reporting.rs b/src/typecheck/reporting.rs
index c21f850a..2110a521 100644
--- a/src/typecheck/reporting.rs
+++ b/src/typecheck/reporting.rs
@@ -115,7 +115,7 @@ pub fn to_type(
     ty: TypeWrapper,
 ) -> Types {
     match ty {
-        TypeWrapper::Ptr(p) => match table.root(p) {
+        TypeWrapper::Ptr(p) => match get_root(table, p) {
             TypeWrapper::Ptr(p) => var_to_type(reported_names, names, p),
             tyw => to_type(table, reported_names, names, tyw),
         },
diff --git a/src/types.rs b/src/types.rs
index c8d1c67c..b3c0e0ab 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -53,7 +53,7 @@
 //! untyped parts.
 use crate::identifier::Ident;
 use crate::term::make as mk_term;
-use crate::term::{BinaryOp, RichTerm, Term, UnaryOp};
+use crate::term::{RichTerm, Term, UnaryOp};
 use crate::{mk_app, mk_fun};
 use std::collections::HashMap;
 use std::fmt;
@@ -154,15 +154,14 @@ impl<Ty> AbsType<Ty> {
 pub struct Types(pub AbsType<Box<Types>>);
 
 impl Types {
-    /// Return the contract corresponding to a type.
-    ///
-    /// Wrapper for [`contract_open`](fn.contract_open.html).
+    /// 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.
     pub fn contract(&self) -> RichTerm {
         let mut sy = 0;
-        self.contract_open(HashMap::new(), true, &mut sy)
+        self.subcontract(HashMap::new(), true, &mut sy)
     }
 
-    /// Return the contract corresponding to a type.
+    /// Return the contract corresponding to a subtype.
     ///
     /// # Arguments
     ///
@@ -172,28 +171,27 @@ impl Types {
     /// of an arrow type (see [`Label`](../label/struct.label.html)).
     /// - `sy` is a counter used to generate fresh symbols for `forall` contracts (see `Wrapped` in
     /// [terms](../term/enum.Term.html).
-    pub fn contract_open(
+    fn subcontract(
         &self,
         mut h: HashMap<Ident, (RichTerm, RichTerm)>,
         pol: bool,
         sy: &mut i32,
     ) -> RichTerm {
         use crate::stdlib::contracts;
-        use crate::transform::fresh_var;
 
-        let ctr = match self.0 {
+        match self.0 {
             AbsType::Dyn() => contracts::dynamic(),
             AbsType::Num() => contracts::num(),
             AbsType::Bool() => contracts::bool(),
             AbsType::Str() => contracts::string(),
             //TODO: optimization: have a specialized contract for `List Dyn`, to avoid mapping an
             //always successful contract on each element.
-            AbsType::List(ref ty) => mk_app!(contracts::list(), ty.contract_open(h, pol, sy)),
+            AbsType::List(ref ty) => mk_app!(contracts::list(), ty.subcontract(h, pol, sy)),
             AbsType::Sym() => panic!("Are you trying to check a Sym at runtime?"),
             AbsType::Arrow(ref s, ref t) => mk_app!(
                 contracts::func(),
-                s.contract_open(h.clone(), !pol, sy),
-                t.contract_open(h, pol, sy)
+                s.subcontract(h.clone(), !pol, sy),
+                t.subcontract(h, pol, sy)
             ),
             AbsType::Flat(ref t) => t.clone(),
             AbsType::Var(ref i) => {
@@ -209,9 +207,9 @@ impl Types {
 
                 h.insert(i.clone(), (inst_var, inst_tail));
                 *sy += 1;
-                t.contract_open(h, pol, sy)
+                t.subcontract(h, pol, sy)
             }
-            AbsType::RowEmpty() | AbsType::RowExtend(_, _, _) => contracts::fail(),
+            AbsType::RowEmpty() | AbsType::RowExtend(..) => contracts::fail(),
             AbsType::Enum(ref r) => {
                 fn form(ty: Types, h: HashMap<Ident, (RichTerm, RichTerm)>) -> RichTerm {
                     match ty.0 {
@@ -267,7 +265,7 @@ impl Types {
                         }
                         AbsType::RowExtend(id, Some(ty), rest) => {
                             let cont = form(sy, pol, rest.as_ref(), h.clone());
-                            let row_contr = ty.contract_open(h, pol, sy);
+                            let row_contr = ty.subcontract(h, pol, sy);
                             mk_app!(
                                 contracts::record_extend(),
                                 mk_term::string(format!("{}", id)),
@@ -285,26 +283,9 @@ impl Types {
                 mk_app!(contracts::record(), form(sy, pol, ty, h))
             }
             AbsType::DynRecord(ref ty) => {
-                mk_app!(contracts::dyn_record(), ty.contract_open(h, pol, sy))
+                mk_app!(contracts::dyn_record(), ty.subcontract(h, pol, sy))
             }
-        };
-
-        // To track the argument to contracts and support contracts as record, we need to wrap the
-        // function contracts as an `Assume`. Since `Assume` is strict in the label and need to be
-        // fully applied, we need to wrap the whole expression back as a standard function, that is
-        // to form: `fun l val => %assume% ctr l val`
-        let var_l = fresh_var();
-        let var_val = fresh_var();
-        let pos = ctr.pos;
-        mk_fun!(
-            var_l.clone(),
-            var_val.clone(),
-            mk_app!(
-                mk_term::op2(BinaryOp::Assume(), ctr, Term::Var(var_l)),
-                Term::Var(var_val)
-            )
-        )
-        .with_pos(pos.into_inherited())
+        }
     }
 
     /// Find a binding in a record row type. Return `None` if there is no such binding, if the type
diff --git a/stdlib/contracts.ncl b/stdlib/contracts.ncl
index 7a646e83..02be7f1d 100644
--- a/stdlib/contracts.ncl
+++ b/stdlib/contracts.ncl
@@ -7,11 +7,14 @@
 
   string = fun l t => if %is_str% t then t else %blame% l,
 
-  list = fun elt l t => if %is_list% t then %map% t (elt (%go_list% l)) else %blame% l,
+  list = fun elt l t =>
+    if %is_list% t then
+      %map% t (fun value => %assume% elt (%go_list% l) value)
+    else %blame% l,
 
   func = fun s t l e =>
       if %is_fun% e then
-          (fun x => t (%go_codom% l) (e (s (%chng_pol% (%go_dom% l)) x)))
+          (fun x => %assume% t (%go_codom% l) (e (%assume% s (%chng_pol% (%go_dom% l)) x)))
       else
           %blame% l,
 
@@ -28,23 +31,23 @@
       if (case t) then
           t
       else
-          contr (%tag% "NotRowExt" l) t,
+          %assume% contr (%tag% "NotRowExt" l) t,
 
   record = fun cont l t =>
       if %is_record% t then
-          cont {} l t
+          %assume% (cont {}) l t
       else
           %blame% (%tag% "not a record" l),
 
   dyn_record = fun contr l t =>
       if %is_record% t then
-          %record_map% t (fun _field => contr l)
+          %record_map% t (fun _field value => %assume% contr l value)
       else
           %blame% (%tag% "not a record" l),
 
   record_extend = fun field contr cont acc l t =>
       if %has_field% field t then
-          let acc = acc$[field = contr (%go_field% field l) (t."#{field}")] in
+          let acc = acc$[field = %assume% contr (%go_field% field l) (t."#{field}")] in
           let t = t -$ field in
           cont acc l t
       else
@@ -151,5 +154,30 @@
         ```
         "#m
       = fun msg l => %tag% msg l,
+
+    apply
+      | doc m#"
+        Apply a contract to a label and a value.
+
+        Type: `Contract -> Lbl -> Dyn -> Dyn`
+        (for technical reasons, this element isn't actually statically typed)
+
+        Nickel supports user-defined contracts defined as functions, but also as
+        records. Moreover, the interpreter performs additional book-keeping for
+        error reporting when applying a contract in an expression `value |
+        #Contract`. You should not use standard function application to apply a
+        contract, but this function instead. 
+
+        For example:
+        ```
+        let Nullable = fun contract label value =>
+          if value == null then null
+          else contracts.apply contract label value
+        in
+        let Contract = Nullable {foo | Num} in
+        ({foo = 1} | #Contract)
+        ```
+        "#m
+      = fun contract label value => %assume% contract label value,
   },
 }


Test patch:
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
index dd87e8a4..532b819c 100644
--- a/tests/pass/contracts.ncl
+++ b/tests/pass/contracts.ncl
@@ -109,10 +109,27 @@ let Assert = fun l x => x || %blame% l in
 
   // nested_metavalues
   // Regression test for #402
-  let myContract = { x | Str } in
+  let MyContract = { x | Str } in
   {
-    foo | #myContract | default = { x = "From foo" },
+    foo | #MyContract | default = { x = "From foo" },
     bar | #{..} | default = foo
   } == { foo.x = "From foo", bar.x = "From foo"},
+
+  // mixing type and record contracts
+  let f | #{foo | Num} -> #{bar | Num} = fun r =>
+    {bar = r.foo} in
+  (f {foo = 1}).bar == 1,
+  // user-written contract application
+  let Extend = fun base label value =>
+    let derived = if builtins.is_record base then
+      (base & {foo | Num})
+    else
+      base in
+    contracts.apply derived label value in
+  let Contract = Extend {bar | Num, ..} in
+  let Id = Extend (fun label value => value) in
+  ({bar = 1, foo = 1} | #Contract)
+    & ({baz = 1} | #Id)
+  == {foo = 1, bar = 1, baz = 1},
 ]
 |> lists.foldl (fun x y => (x | #Assert) && y) true