Repository: tweag/nickel
Pull request #1192 (2023-03-20 17:07:24)

More generic contract generation
This PR introduces a type variable environment into labels and makes the tracking type variable polarities for contract generation dynamic. Additionally, it introduces two new primops to manipulate this environment.

This is preparatory work for #1177.


Patch:
diff --git a/benches/nixpkgs/lists.ncl b/benches/nixpkgs/lists.ncl
index 4b6edb2c..12db775b 100644
--- a/benches/nixpkgs/lists.ncl
+++ b/benches/nixpkgs/lists.ncl
@@ -456,19 +456,29 @@
   = fun before list =>
     let dfsthis = listDfs true before list in
     let toporest = toposort before (dfsthis.visited @ dfsthis.rest) in
+
+    # The repeated `{_ : Array Dyn}` annotations are verbose, and due to
+    # the handling of dictionary types being cumbersome with the current
+    # typechecker.
+    #
+    # RFC004 is supposed to fix those kind of use-cases by introducing a limited
+    # form of subtyping.
     if array.length list < 2
-    then # finish
-      { result| Array Dyn =  list, }
+      then # finish
+        { result| Array Dyn =  list, } : {_ : Array Dyn}
     else if record.has_field "cycle" (dfsthis | {_: Dyn})
-    then # there's a cycle, starting from the current vertex, return it
-      { cycle = reverseList ([ (dfsthis | {cycle: Dyn}).cycle ] @ dfsthis.visited | Array Dyn),
-        loops = (dfsthis | {loops: Array Dyn}).loops, }
+      then # there's a cycle, starting from the current vertex, return it
+        { cycle = reverseList ([ (dfsthis | {cycle: Dyn}).cycle ] @ dfsthis.visited | Array Dyn),
+          loops = (dfsthis | {loops: Array Dyn}).loops, } : {_ : Array Dyn}
     else if record.has_field "cycle" toporest
-    then # there's a cycle somewhere else in the graph, return it
-      toporest
-    # Slow, but short. Can be made a bit faster with an explicit stack.
+      then # there's a cycle somewhere else in the graph, return it
+        toporest
+      # Slow, but short. Can be made a bit faster with an explicit stack.
     else # there are no cycles
-      { result = [ (dfsthis| {minimal:Dyn}).minimal ] @ (toporest | {result: Array Dyn}).result, },
+        {
+          result = [ (dfsthis| {minimal:Dyn}).minimal ]
+                   @ (toporest | {result: Array Dyn}).result
+        } : {_: Array Dyn},
 
   #TODO: can it be statically typed?
   sort | forall a. (a -> a -> Bool) -> Array a -> Array a
@@ -556,7 +566,7 @@
        take 2 [ ]
        >> [ ]
   "%
-  = fun 
+  = fun
     # Number of elements to take
     count => sublist 0 count,
 
diff --git a/lsp/nls/src/requests/completion.rs b/lsp/nls/src/requests/completion.rs
index 843c6be2..647a7a52 100644
--- a/lsp/nls/src/requests/completion.rs
+++ b/lsp/nls/src/requests/completion.rs
@@ -820,7 +820,7 @@ mod tests {
 
     #[test]
     fn test_extract_ident_with_path() {
-        use nickel_lang::{mk_uty_record, mk_uty_row, types::RecordRowsF};
+        use nickel_lang::{mk_uty_record, mk_uty_row};
         use std::convert::TryInto;
 
         // Representing the type: {a: {b : {c1 : Num, c2: Num}}}
diff --git a/src/cache.rs b/src/cache.rs
index db46a9de..de18af31 100644
--- a/src/cache.rs
+++ b/src/cache.rs
@@ -8,8 +8,7 @@ use crate::stdlib::{self as nickel_stdlib, StdlibModule};
 use crate::term::record::{Field, RecordData};
 use crate::term::{RichTerm, SharedTerm, Term};
 use crate::transform::import_resolution;
-use crate::typecheck::type_check;
-use crate::typecheck::{self, Wildcards};
+use crate::typecheck::{self, type_check, Wildcards};
 use crate::types::UnboundTypeVariableError;
 use crate::{eval, parser, transform};
 use codespan::{FileId, Files};
diff --git a/src/eval/operation.rs b/src/eval/operation.rs
index b2128096..ded355cb 100644
--- a/src/eval/operation.rs
+++ b/src/eval/operation.rs
@@ -16,7 +16,7 @@ use super::{
 use crate::{
     error::{EvalError, IllegalPolymorphicTailAction},
     identifier::Ident,
-    label::ty_path,
+    label::{ty_path, Polarity, TypeVarData},
     match_sharedterm, mk_app, mk_fun, mk_opn, mk_record,
     parser::utils::parse_number,
     position::TermPos,
@@ -2798,6 +2798,39 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     pos2.into_inherited(),
                 )))
             }
+            BinaryOp::LookupTypeVar() => {
+                let t1 = t1.into_owned();
+                let t2 = t2.into_owned();
+
+                let Term::SealingKey(key) = t1 else {
+                    return Err(EvalError::TypeError(
+                        String::from("Symbol"),
+                        String::from("lookup_type_variable, 1st argument"),
+                        fst_pos,
+                        RichTerm {
+                            term: t1.into(),
+                            pos: pos1,
+                        }
+                    ));
+                };
+
+                let Term::Lbl(label) = t2 else {
+                    return Err(EvalError::TypeError(
+                        String::from("Label"),
+                        String::from("lookup_type_variable, 2nd argument"),
+                        snd_pos,
+                        RichTerm {
+                            term: t2.into(),
+                            pos: pos2,
+                        }
+                    ));
+                };
+
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    label.type_environment.get(&key).unwrap().into(),
+                    pos_op_inh,
+                )))
+            }
         }
     }
 
@@ -3161,6 +3194,92 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                     )),
                 }
             }
+            NAryOp::InsertTypeVar() => {
+                let mut args = args.into_iter();
+
+                let (
+                    Closure {
+                        body:
+                            RichTerm {
+                                term: key,
+                                pos: key_pos,
+                            },
+                        ..
+                    },
+                    pos1,
+                ) = args.next().unwrap();
+
+                let (
+                    Closure {
+                        body:
+                            RichTerm {
+                                term: polarity,
+                                pos: polarity_pos,
+                            },
+                        ..
+                    },
+                    pos2,
+                ) = args.next().unwrap();
+
+                let (
+                    Closure {
+                        body:
+                            RichTerm {
+                                term: label,
+                                pos: label_pos,
+                            },
+                        ..
+                    },
+                    pos3,
+                ) = args.next().unwrap();
+                debug_assert!(args.next().is_none());
+
+                let Term::SealingKey(key) = *key else {
+                    return Err(EvalError::TypeError(
+                        String::from("Symbol"),
+                        String::from("insert_type_variable, 1st argument"),
+                        key_pos,
+                        RichTerm {
+                            term: key,
+                            pos: pos1,
+                        }
+                    ));
+                };
+
+                let Ok(polarity) = Polarity::try_from(polarity.as_ref()) else {
+                    return Err(EvalError::TypeError(
+                        String::from("Polarity"),
+                        String::from("insert_type_variable, 2nd argument"),
+                        polarity_pos,
+                        RichTerm {
+                            term: polarity,
+                            pos: pos2,
+                        },
+                    ))
+                };
+
+                let Term::Lbl(label) = &*label else {
+                    return Err(EvalError::TypeError(
+                        String::from("Label"),
+                        String::from("insert_type_variable, 3rd argument"),
+                        label_pos,
+                        RichTerm {
+                            term: label,
+                            pos: pos3,
+                        }
+                    ));
+                };
+
+                let mut new_label = label.clone();
+                new_label
+                    .type_environment
+                    .insert(key, TypeVarData { polarity });
+
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Lbl(new_label),
+                    pos2.into_inherited(),
+                )))
+            }
         }
     }
 }
diff --git a/src/label.rs b/src/label.rs
index 3eaee485..f1f5957d 100644
--- a/src/label.rs
+++ b/src/label.rs
@@ -2,13 +2,18 @@
 //!
 //! A label is a value holding metadata relative to contract checking. It gives the user useful
 //! information about the context of a contract failure.
-use std::rc::Rc;
+use std::{collections::HashMap, rc::Rc};
 
 use crate::{
     eval::cache::{Cache as EvalCache, CacheIndex},
     identifier::Ident,
+    mk_uty_enum, mk_uty_record,
     position::{RawSpan, TermPos},
-    term::{RichTerm, Term},
+    term::{
+        record::{Field, RecordData},
+        RichTerm, SealingKey, Term,
+    },
+    typecheck::{ReifyAsUnifType, UnifType},
     types::{TypeF, Types},
 };
 
@@ -307,8 +312,42 @@ pub struct Label {
     pub polarity: Polarity,
     /// The path of the type being currently checked in the original type.
     pub path: ty_path::Path,
+    /// An environment mapping type variables to [`TypeVarData`]. Used by
+    /// polymorphic contracts to decide which actions to take when encountering a `forall`.
+    pub type_environment: HashMap<SealingKey, TypeVarData>,
 }
 
+/// Data about type variables that is needed for polymorphic contracts to decide which actions to take.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct TypeVarData {
+    pub polarity: Polarity,
+}
+
+impl From<&TypeVarData> for Term {
+    fn from(value: &TypeVarData) -> Self {
+        Term::Record(RecordData {
+            fields: [(
+                Ident::new("polarity"),
+                Field::from(RichTerm::from(Term::from(value.polarity))),
+            )]
+            .into(),
+            attrs: Default::default(),
+            sealed_tail: None,
+        })
+    }
+}
+
+impl ReifyAsUnifType for TypeVarData {
+    fn unif_type() -> UnifType {
+        mk_uty_record!(("polarity", Polarity::unif_type()))
+    }
+}
+
+impl ReifyAsUnifType for Polarity {
+    fn unif_type() -> UnifType {
+        mk_uty_enum!("Positive", "Negative")
+    }
+}
 /// A polarity. See [`Label`]
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum Polarity {
@@ -334,6 +373,18 @@ impl From<Polarity> for Term {
     }
 }
 
+impl TryFrom<&Term> for Polarity {
+    type Error = ();
+
+    fn try_from(value: &Term) -> Result<Self, Self::Error> {
+        match value {
+            Term::Enum(positive) if positive.label() == "Positive" => Ok(Self::Positive),
+            Term::Enum(negative) if negative.label() == "Negative" => Ok(Self::Negative),
+            _ => Err(()),
+        }
+    }
+}
+
 /// Custom reporting diagnostic that can be set by user-code through the `label` API. Used to
 /// customize contract error messages, and provide more context than "a contract has failed".
 #[derive(Debug, Clone, PartialEq, Default)]
@@ -470,6 +521,7 @@ impl Default for Label {
             arg_idx: Default::default(),
             arg_pos: Default::default(),
             path: Default::default(),
+            type_environment: Default::default(),
         }
     }
 }
diff --git a/src/parser/grammar.lalrpop b/src/parser/grammar.lalrpop
index b3ef0bf4..6c9af2cb 100644
--- a/src/parser/grammar.lalrpop
+++ b/src/parser/grammar.lalrpop
@@ -864,6 +864,7 @@ BOpPre: BinaryOp = {
     "label_with_message" => BinaryOp::LabelWithMessage(),
     "label_with_notes" => BinaryOp::LabelWithNotes(),
     "label_append_note" => BinaryOp::LabelAppendNote(),
+    "lookup_type_variable" => BinaryOp::LookupTypeVar(),
 }
 
 NOpPre<ArgRule>: UniTerm = {
@@ -877,6 +878,8 @@ NOpPre<ArgRule>: UniTerm = {
         UniTerm::from(mk_opn!(NAryOp::RecordSealTail(), t1, t2, t3, t4)),
     "record_unseal_tail" <t1: ArgRule> <t2: ArgRule> <t3: ArgRule> =>
         UniTerm::from(mk_opn!(NAryOp::RecordUnsealTail(), t1, t2, t3)),
+    "insert_type_variable" <key: ArgRule> <pol: ArgRule> <label: ArgRule> =>
+        UniTerm::from(mk_opn!(NAryOp::InsertTypeVar(), key, pol, label)),
 }
 
 TypeBuiltin: Types = {
@@ -1029,6 +1032,8 @@ extern {
         "rec_force_op" => Token::Normal(NormalToken::RecForceOp),
         "rec_default_op" => Token::Normal(NormalToken::RecDefaultOp),
         "trace" => Token::Normal(NormalToken::Trace),
+        "insert_type_variable" => Token::Normal(NormalToken::InsertTypeVar),
+        "lookup_type_variable" => Token::Normal(NormalToken::LookupTypeVar),
 
         "has_field" => Token::Normal(NormalToken::HasField),
         "map" => Token::Normal(NormalToken::Map),
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 5da96744..2324c084 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -204,6 +204,10 @@ pub enum NormalToken<'input> {
     GoArray,
     #[token("%go_dict%")]
     GoDict,
+    #[token("%insert_type_variable%")]
+    InsertTypeVar,
+    #[token("%lookup_type_variable%")]
+    LookupTypeVar,
 
     #[token("%seal%")]
     Seal,
diff --git a/src/stdlib.rs b/src/stdlib.rs
index faf4c426..da43042f 100644
--- a/src/stdlib.rs
+++ b/src/stdlib.rs
@@ -119,6 +119,7 @@ pub mod contract {
     generate_accessor!(array);
     generate_accessor!(func);
     generate_accessor!(forall_var);
+    generate_accessor!(forall);
     generate_accessor!(fail);
     generate_accessor!(enums);
     generate_accessor!(enum_fail);
diff --git a/src/term/mod.rs b/src/term/mod.rs
index 0b4a660d..9f50d399 100644
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@@ -1305,6 +1305,10 @@ pub enum BinaryOp {
     LabelWithNotes(),
     /// Append a note to the current diagnostic of a label.
     LabelAppendNote(),
+
+    /// Look up the [`TypeVarData`] associated with a [`SealingKey`] in the
+    /// type environment of a [label](Term::Lbl)
+    LookupTypeVar(),
 }
 
 impl BinaryOp {
@@ -1363,6 +1367,14 @@ pub enum NAryOp {
     ///     something goes wrong while unsealing,
     ///   - the [record](Term::Record) whose tail we wish to unseal.
     RecordUnsealTail(),
+    /// Insert type variable data into the [`type_environment`] of a [`Label`]
+    ///
+    /// Takes four arguments:
+    ///   - the [sealing key](Term::SealingKey) assigned to the type variable
+    ///   - the [introduction polarity](label::Polarity) of the type variable
+    ///   - the [kind](types::VarKind) of the type variable
+    ///   - a [label](Term::Label) on which to operate
+    InsertTypeVar(),
 }
 
 impl NAryOp {
@@ -1372,7 +1384,8 @@ impl NAryOp {
             | NAryOp::StrReplaceRegex()
             | NAryOp::StrSubstr()
             | NAryOp::MergeContract()
-            | NAryOp::RecordUnsealTail() => 3,
+            | NAryOp::RecordUnsealTail()
+            | NAryOp::InsertTypeVar() => 3,
             NAryOp::RecordSealTail() => 4,
         }
     }
@@ -1387,6 +1400,7 @@ impl fmt::Display for NAryOp {
             NAryOp::MergeContract() => write!(f, "mergeContract"),
             NAryOp::RecordSealTail() => write!(f, "%record_seal_tail%"),
             NAryOp::RecordUnsealTail() => write!(f, "%record_unseal_tail%"),
+            NAryOp::InsertTypeVar() => write!(f, "%insert_type_variable%"),
         }
     }
 }
diff --git a/src/typecheck/mk_uniftype.rs b/src/typecheck/mk_uniftype.rs
index 357e9c85..e57d16f3 100644
--- a/src/typecheck/mk_uniftype.rs
+++ b/src/typecheck/mk_uniftype.rs
@@ -13,7 +13,7 @@ macro_rules! mk_uty_arrow {
         )
     };
     ( $fst:expr, $snd:expr , $( $types:expr ),+ ) => {
-        mk_uty_arrow!($fst, mk_uty_arrow!($snd, $( $types ),+))
+        $crate::mk_uty_arrow!($fst, $crate::mk_uty_arrow!($snd, $( $types ),+))
     };
 }
 
@@ -22,7 +22,7 @@ macro_rules! mk_uty_arrow {
 #[macro_export]
 macro_rules! mk_uty_enum_row {
     () => {
-        $crate::typecheck::UnifEnumRows::Concrete(EnumRowsF::Empty)
+        $crate::typecheck::UnifEnumRows::Concrete($crate::types::EnumRowsF::Empty)
     };
     (; $tail:expr) => {
         $crate::typecheck::UnifEnumRows::from($tail)
@@ -31,7 +31,7 @@ macro_rules! mk_uty_enum_row {
         $crate::typecheck::UnifEnumRows::Concrete(
             $crate::types::EnumRowsF::Extend {
                 row: Ident::from($id),
-                tail: Box::new(mk_uty_enum_row!($( $ids ),* $(; $tail)?))
+                tail: Box::new($crate::mk_uty_enum_row!($( $ids ),* $(; $tail)?))
             }
         )
     };
@@ -43,7 +43,7 @@ macro_rules! mk_uty_enum_row {
 #[macro_export]
 macro_rules! mk_uty_row {
     () => {
-        $crate::typecheck::UnifRecordRows::Concrete(RecordRowsF::Empty)
+        $crate::typecheck::UnifRecordRows::Concrete($crate::types::RecordRowsF::Empty)
     };
     (; $tail:expr) => {
         $crate::typecheck::UnifRecordRows::from($tail)
@@ -55,7 +55,7 @@ macro_rules! mk_uty_row {
                     id: Ident::from($id),
                     types: Box::new($ty.into()),
                 },
-                tail: Box::new(mk_uty_row!($(($ids, $tys)),* $(; $tail)?)),
+                tail: Box::new($crate::mk_uty_row!($(($ids, $tys)),* $(; $tail)?)),
             }
         )
     };
@@ -67,7 +67,7 @@ macro_rules! mk_uty_enum {
     ($( $ids:expr ),* $(; $tail:expr)?) => {
         $crate::typecheck::UnifType::Concrete(
             $crate::types::TypeF::Enum(
-                mk_uty_enum_row!($( $ids ),* $(; $tail)?)
+                $crate::mk_uty_enum_row!($( $ids ),* $(; $tail)?)
             )
         )
     };
@@ -79,7 +79,7 @@ macro_rules! mk_uty_record {
     ($(($ids:expr, $tys:expr)),* $(; $tail:expr)?) => {
         $crate::typecheck::UnifType::Concrete(
             $crate::types::TypeF::Record(
-                mk_uty_row!($(($ids, $tys)),* $(; $tail)?)
+                $crate::mk_uty_row!($(($ids, $tys)),* $(; $tail)?)
             )
         )
     };
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index f04118d1..0b979098 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -1,38 +1,46 @@
-//! Implementation of the typechecker.
+//! Typechecking and type inference.
 //!
-//! # Mode
+//! Nickel uses a mix of a bidirectional typechecking algorithm, together with standard
+//! unification-based type inference. Nickel is gradually typed, and dynamic typing is the default.
+//! Static typechecking is triggered by a type annotation.
 //!
-//! Typechecking can be made in to different modes:
-//! - **Strict**: correspond to traditional typechecking in statically typed languages. This
-//!   happens inside a statically typed block. Statically typed blocks are introduced by the type
-//!   ascription operator `:`, as in `1 + 1 : Num` or `let f : Num -> Num = fun x => x + 1 in ..`. This is
-//!   implemented by [`type_check_`] and variants.
-//! - **Non strict**: do not enforce any typing but continue to traverse the AST looking for other
-//!   typed blocks to typecheck and store the annotations of let bindings in the environment. This is
-//!   implemented by the [`walk`] function.
+//! # Modes
 //!
-//! The algorithm starts in non strict mode. It is switched to strict mode when entering a
-//! statically typed block (an expression annotated with a type), and is switched back to
-//! non-strict mode when entering an expression annotated with a contract. Type and contract
-//! annotations thus serve both another purpose beside enforcing a type or a contract, which is to
-//! switch the typechecking mode.
+//! The typechecking algorithm runs in two separate modes, corresponding to static and dynamic
+//! typing:
+//!
+//! - **enforce** corresponds to traditional typechecking in a statically typed language. This
+//!   happens inside a statically typed block. Such blocks are introduced by the type ascription
+//!   operator `:`, as in `1 + 1 : Number` or `let f : Number -> Number = fun x => x + 1 in ..`. Enforce
+//!   mode is implemented by [`type_check`] and variants.
+//! - **walk** doesn't enforce any typing but traverses the AST looking for typed blocks to
+//!   typecheck. Walk mode also stores the annotations of bound identifiers in the environment. This
+//!   is implemented by the [`walk`] function.
+//!
+//! The algorithm starts in walk mode. A typed block (an expression annotated with a type) switches
+//! to enforce mode, and is switched back to walk mode when entering an expression annotated with a
+//! contract. Type and contract annotations thus serve as a switch for the typechecking mode.
+//!
+//! Note that the static typing part is based on the bidirectional typing framework, which defines
+//! two different modes. Thus, the enforce mode is itself divided again into **checking** mode and
+//! **inference** mode.
 //!
 //! # Type inference
 //!
 //! Type inference is done via a form of bidirectional typechecking coupled with unification, in
-//! the same spirit as GHC (Haskell), albeit the type system of Nickel is much simpler. The type of
+//! the same spirit as GHC (Haskell), although the type system of Nickel is simpler. The type of
 //! un-annotated let-bound expressions (the type of `bound_exp` in `let x = bound_exp in body`) is
-//! inferred in strict mode, but it is never implicitly generalized. For example, the following
+//! inferred in enforce mode, but it is never implicitly generalized. For example, the following
 //! program is rejected:
 //!
 //! ```nickel
 //! # Rejected
-//! let id = fun x => x in seq (id "a") (id 5) : Num
+//! let id = fun x => x in seq (id "a") (id 5) : Number
 //! ```
 //!
 //! Indeed, `id` is given the type `_a -> _a`, where `_a` is a unification variable, but is not
-//! generalized to `forall a. a -> a`. At the first call site, `_a` is unified with `Str`, and at the second
-//! call site the typechecker complains that `5` is not of type `Str`.
+//! generalized to `forall a. a -> a`. At the first call site, `_a` is unified with `String`, and at the second
+//! call site the typechecker complains that `5` is not of type `String`.
 //!
 //! This restriction is on purpose, as generalization is not trivial to implement efficiently and
 //! more importantly can interact with other components of the type system and type inference. If
@@ -43,7 +51,7 @@
 //! let id : forall a. a -> a = fun x => x in seq (id "a") (id 5) : Num
 //! ```
 //!
-//! In non-strict mode, the type of let-bound expressions is inferred in a shallow way (see
+//! In walk mode, the type of let-bound expressions is inferred in a shallow way (see
 //! [`apparent_type`]).
 use crate::{
     cache::ImportResolver,
@@ -576,6 +584,10 @@ impl<'a> Iterator for EnumRowsIterator<'a, UnifEnumRows> {
     }
 }
 
+pub trait ReifyAsUnifType {
+    fn unif_type() -> UnifType;
+}
+
 /// The typing context is a structure holding the scoped, environment-like data structures required
 /// to perform typechecking.
 ///
@@ -1044,7 +1056,7 @@ fn walk_annotated<L: Linearizer>(
 }
 
 /// Walk an annotated term, either via [crate::term::record::FieldMetadata], or via a standalone
-/// type or contract annotation. A type annotation switches the typechecking mode to _checking_.
+/// type or contract annotation. A type annotation switches the typechecking mode to _enforce_.
 fn walk_with_annot<L: Linearizer>(
     state: &mut State,
     ctxt: Context,
@@ -1067,7 +1079,7 @@ fn walk_with_annot<L: Linearizer>(
         ) => {
             let uty2 = UnifType::from_type(ty2.clone(), &ctxt.term_env);
             let instantiated = instantiate_foralls(state, uty2, ForallInst::Constant);
-            type_check_(state, ctxt, lin, linearizer.scope(), value, instantiated)
+            check(state, ctxt, lin, linearizer.scope(), value, instantiated)
         }
         (_, Some(value)) => walk(state, ctxt, lin, linearizer.scope(), value),
         // TODO: we might have something to do with the linearizer to clear the current
@@ -1077,9 +1089,41 @@ fn walk_with_annot<L: Linearizer>(
     }
 }
 
-/// Typecheck a term against a specific type.
+/// Check a term against a given type. Although this method mostly corresponds to checking mode in
+/// the classical bidirectional framework, it combines both checking and inference modes in
+/// practice, to avoid duplicating rules (that is, code) as detailed below.
+///
+/// # Literals
+///
+/// Checking a literal (a number, a string, a boolean, etc.) unifies the checked type with the
+/// corresponding primitive type (`Number`, `String`, `Bool`, etc.). If the checked type is a
+/// unification variable, `check` acts as an inference rule. If the type is concrete, unification
+/// enforces equality, and `check` acts as a checking rule.
+///
+/// # Introduction rules
+///
+/// Following Pfenning's recipe (see [Bidirectional Typing][bidirectional-typing]),
+/// introduction rules (e.g. typechecking a record) are checking. `check` follows the same logic
+/// here: it uses unification to "match" on the expected type (in the case of record, a record type
+/// or a dictionary type) and pushes typechecking down the record fields.
+///
+/// # Elimination rules
+///
+/// Elimination rules (such as function application or primitive operator application) only exist in
+/// inference mode (still following Pfenning's recipe). `check` follows the inference mode here
+/// (typically on function application, where we first call to `infer` on the function part, and
+/// then check the argument).
+///
+/// Still, `check` is supposed to be implementing checking mode from the outside. We thus also
+/// apply the typing rule which switches from inference to checking mode. Currently, subtyping
+/// isn't supported yet in Nickel but is planned as part of RFC004. When subtyping lands, as the
+/// name suggests, [`subsumption`] will be the place where we apply subsumption, as customary in
+/// bidirectional type systems with subtyping.
 ///
-/// # Arguments
+/// To sum up, elimination rules inside `check` correspond to an inference rule composed with the
+/// switching/subsumption rule, resulting in a composite checking rule.
+///
+/// # Parameters
 ///
 /// - `state`: the unification state (see [`State`]).
 /// - `env`: the typing environment, mapping free variable to types.
@@ -1088,9 +1132,13 @@ fn walk_with_annot<L: Linearizer>(
 /// - `t`: the term to check.
 /// - `ty`: the type to check the term against.
 ///
-/// Registers every term with the `linearizer` and makes sure to scope the
-/// liearizer accordingly
-fn type_check_<L: Linearizer>(
+/// # Linearization (LSP)
+///
+/// `check` is in charge of registering every term with the `linearizer` and makes sure to scope
+/// the linearizer accordingly
+///
+/// [bidirectional-typing]: (https://arxiv.org/abs/1908.05839)
+fn check<L: Linearizer>(
     state: &mut State,
     mut ctxt: Context,
     lin: &mut Linearization<L::Building>,
@@ -1122,7 +1170,7 @@ fn type_check_<L: Linearizer>(
                 .try_for_each(|chunk| -> Result<(), TypecheckError> {
                     match chunk {
                         StrChunk::Literal(_) => Ok(()),
-                        StrChunk::Expr(t, _) => type_check_(
+                        StrChunk::Expr(t, _) => check(
                             state,
                             ctxt.clone(),
                             lin,
@@ -1133,27 +1181,27 @@ fn type_check_<L: Linearizer>(
                     }
                 })
         }
+        // Fun is an introduction rule for the arrow type. The target type is thus expected to be
+        // `T -> U`, which is enforced by unification, and we then check the body of the function
+        // against `U`, after adding `x : T` in the environment.
         Term::Fun(x, t) => {
             let src = state.table.fresh_type_uvar();
-            // 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_type_uvar();
             let arr = mk_uty_arrow!(src.clone(), trg.clone());
+
             linearizer.retype_ident(lin, x, src.clone());
 
             unify(state, &ctxt, ty, arr).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
 
             ctxt.type_env.insert(*x, src);
-            type_check_(state, ctxt, lin, linearizer, t, trg)
+            check(state, ctxt, lin, linearizer, t, trg)
         }
         Term::FunPattern(x, pat, t) => {
             let src_rows_ty = destructuring::build_pattern_type_check_mode(state, &ctxt, pat)?;
             let src = UnifType::Concrete(TypeF::Record(src_rows_ty.clone()));
-
-            // 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_type_uvar();
             let arr = mk_uty_arrow!(src.clone(), trg.clone());
+
             if let Some(x) = x {
                 linearizer.retype_ident(lin, x, src.clone());
                 ctxt.type_env.insert(*x, src);
@@ -1161,7 +1209,7 @@ fn type_check_<L: Linearizer>(
 
             destructuring::inject_pattern_variables(state, &mut ctxt.type_env, pat, src_rows_ty);
             unify(state, &ctxt, ty, arr).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
-            type_check_(state, ctxt, lin, linearizer, t, trg)
+            check(state, ctxt, lin, linearizer, t, trg)
         }
         Term::Array(terms, _) => {
             let ty_elts = state.table.fresh_type_uvar();
@@ -1172,7 +1220,7 @@ fn type_check_<L: Linearizer>(
             terms
                 .iter()
                 .try_for_each(|t| -> Result<(), TypecheckError> {
-                    type_check_(
+                    check(
                         state,
                         ctxt.clone(),
                         lin,
@@ -1201,7 +1249,7 @@ fn type_check_<L: Linearizer>(
             }
 
             linearizer.retype_ident(lin, x, ty_let.clone());
-            type_check_(
+            check(
                 state,
                 ctxt.clone(),
                 lin,
@@ -1213,7 +1261,7 @@ fn type_check_<L: Linearizer>(
             if !attrs.rec {
                 ctxt.type_env.insert(*x, ty_let);
             }
-            type_check_(state, ctxt, lin, linearizer, rt, ty)
+            check(state, ctxt, lin, linearizer, rt, ty)
         }
         Term::LetPattern(x, pat, re, rt) => {
             // The inferred type of the pattern w/ unification vars
@@ -1226,7 +1274,7 @@ fn type_check_<L: Linearizer>(
             unify(state, &ctxt, ty_let.clone(), pattern_type)
                 .map_err(|e| e.into_typecheck_err(state, re.pos))?;
 
-            type_check_(
+            check(
                 state,
                 ctxt.clone(),
                 lin,
@@ -1247,14 +1295,22 @@ fn type_check_<L: Linearizer>(
                 pattern_rows_type,
             );
 
-            type_check_(state, ctxt, lin, linearizer, rt, ty)
+            check(state, ctxt, lin, linearizer, rt, ty)
         }
         Term::App(e, t) => {
+            // This part corresponds to the infer rule for application.
+            let function_type = infer(state, ctxt.clone(), lin, linearizer.scope(), e)?;
+
             let src = state.table.fresh_type_uvar();
-            let arr = mk_uty_arrow!(src.clone(), ty);
+            let tgt = state.table.fresh_type_uvar();
+            let arr = mk_uty_arrow!(src.clone(), tgt.clone());
+
+            unify(state, &ctxt, arr, function_type)
+                .map_err(|err| err.into_typecheck_err(state, e.pos))?;
 
-            type_check_(state, ctxt.clone(), lin, linearizer.scope(), e, arr)?;
-            type_check_(state, ctxt, lin, linearizer, t, src)
+            check(state, ctxt.clone(), lin, linearizer, t, src)?;
+
+            subsumption(state, &ctxt, tgt, ty).map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Match { cases, default } => {
             // Currently, if it has a default value, we typecheck the whole thing as
@@ -1263,10 +1319,20 @@ fn type_check_<L: Linearizer>(
             // A match expression is a special kind of function. Thus it's typed as `a -> b`, where
             // `a` is a enum type determined by the matched tags and `b` is the type of each match
             // arm.
+            let arg_type = state.table.fresh_type_uvar();
             let return_type = state.table.fresh_type_uvar();
 
+            // We unify the expected type of the match expression with `arg_type -> return_type`
+            unify(
+                state,
+                &ctxt,
+                ty,
+                mk_uty_arrow!(arg_type.clone(), return_type.clone()),
+            )
+            .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
+
             for case in cases.values() {
-                type_check_(
+                check(
                     state,
                     ctxt.clone(),
                     lin,
@@ -1278,14 +1344,7 @@ fn type_check_<L: Linearizer>(
 
             let erows = match default {
                 Some(t) => {
-                    type_check_(
-                        state,
-                        ctxt.clone(),
-                        lin,
-                        linearizer.scope(),
-                        t,
-                        return_type.clone(),
-                    )?;
+                    check(state, ctxt.clone(), lin, linearizer.scope(), t, return_type)?;
                     state.table.fresh_erows_uvar()
                 }
                 None => cases.iter().try_fold(
@@ -1296,12 +1355,7 @@ fn type_check_<L: Linearizer>(
                 )?,
             };
 
-            // `arg_type` represents the type of arguments that the match expression can be applied
-            // to.
-            let arg_type = mk_uty_enum!(; erows);
-
-            // we unify the expected type of the match expression with `arg_type -> return_type`
-            unify(state, &ctxt, ty, mk_uty_arrow!(arg_type, return_type))
+            unify(state, &ctxt, arg_type, mk_uty_enum!(; erows))
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Var(x) => {
@@ -1321,22 +1375,27 @@ fn type_check_<L: Linearizer>(
                 .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`
+        // for some `a`. In other words, the checking rule is not the same depending on the target
+        // type: if the target type is a dictionary type, we simply check each field against the
+        // element type.
         Term::RecRecord(record, dynamic, ..) if !dynamic.is_empty() => {
             let ty_dict = state.table.fresh_type_uvar();
+            unify(state, &ctxt, ty, mk_uniftype::dyn_record(ty_dict.clone()))
+                .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
 
+            //TODO: should we insert in the environment the checked type, or the actual type?
             for id in record.fields.keys() {
                 ctxt.type_env.insert(*id, ty_dict.clone());
                 linearizer.retype_ident(lin, id, ty_dict.clone())
             }
 
-            // We don't bind the fields in the term environment used to check for contract. See
-            // `Let` case in `walk`.
+            // We don't bind recursive fields in the term environment used to check for contract.
+            // See the recursive let case in `walk`.
             record
                 .fields
                 .iter()
                 .try_for_each(|(id, field)| -> Result<(), TypecheckError> {
-                    type_check_field(
+                    check_field(
                         state,
                         ctxt.clone(),
                         lin,
@@ -1345,15 +1404,14 @@ fn type_check_<L: Linearizer>(
                         field,
                         ty_dict.clone(),
                     )
-                })?;
-
-            unify(state, &ctxt, ty, mk_uniftype::dyn_record(ty_dict))
-                .map_err(|err| err.into_typecheck_err(state, rt.pos))
+                })
         }
         Term::Record(record) | Term::RecRecord(record, ..) => {
             // For recursive records, we look at the apparent type of each field and bind it in
             // ctxt before actually typechecking the content of fields.
-            // Fields defined by interpolation are ignored.
+            //
+            // Fields defined by interpolation are ignored, because they can't be referred to
+            // recursively.
             if let Term::RecRecord(..) = t.as_ref() {
                 for (id, field) in &record.fields {
                     let uty = field_type(state, field, &ctxt, true);
@@ -1370,7 +1428,7 @@ fn type_check_<L: Linearizer>(
                     .fields
                     .iter()
                     .try_for_each(|(id, field)| -> Result<(), TypecheckError> {
-                        type_check_field(
+                        check_field(
                             state,
                             ctxt.clone(),
                             lin,
@@ -1381,51 +1439,85 @@ fn type_check_<L: Linearizer>(
                         )
                     })
             } else {
-                let rows = record.fields.iter().try_fold(
+                // Building the type {id1 : ?a1, id2: ?a2, .., idn: ?an}
+                let mut field_types: HashMap<Ident, UnifType> = record
+                    .fields
+                    .keys()
+                    .map(|id| (*id, state.table.fresh_type_uvar()))
+                    .collect();
+
+                let rows = field_types.iter().fold(
                     mk_uty_row!(),
-                    |acc, (id, field)| -> Result<UnifRecordRows, TypecheckError> {
-                        // In the case of a recursive record, new types (either type variables or
-                        // annotations) have already be determined and put in the typing context,
-                        // and we need to use the same.
-                        let ty = if let Term::RecRecord(..) = t.as_ref() {
-                            ctxt.type_env.get(id).cloned().unwrap()
-                        } else {
-                            state.table.fresh_type_uvar()
-                        };
-
-                        type_check_field(
+                    |acc, (id, row_ty)| mk_uty_row!((*id, row_ty.clone()); acc),
+                );
+
+                unify(state, &ctxt, ty, mk_uty_record!(; rows))
+                    .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
+
+                for (id, field) in record.fields.iter() {
+                    if let Term::RecRecord(..) = t.as_ref() {
+                        let affected_type = ctxt.type_env.get(id).cloned().unwrap();
+                        unify(
                             state,
-                            ctxt.clone(),
-                            lin,
-                            linearizer.scope(),
-                            *id,
-                            field,
-                            ty.clone(),
-                        )?;
+                            &ctxt,
+                            field_types.get(id).cloned().unwrap(),
+                            affected_type,
+                        )
+                        .map_err(|err| {
+                            err.into_typecheck_err(
+                                state,
+                                field.value.as_ref().map(|v| v.pos).unwrap_or_default(),
+                            )
+                        })?;
+                    }
 
-                        Ok(mk_uty_row!((*id, ty); acc))
-                    },
-                )?;
+                    check_field(
+                        state,
+                        ctxt.clone(),
+                        lin,
+                        linearizer.scope(),
+                        *id,
+                        field,
+                        // expect(): we've built `rows` in this very function from
+                        // record.fields.keys(), so it must contain `id`
+                        field_types
+                            .remove(id)
+                            .expect("inserted `id` inside the `field_types` hashmap previously; expected it to be there"),
+                    )?;
+                }
 
-                unify(state, &ctxt, ty, mk_uty_record!(; rows))
-                    .map_err(|err| err.into_typecheck_err(state, rt.pos))
+                Ok(())
             }
         }
+        // Primitive operator application follows the inference discipline, like function
+        // application, because it's an elimination rule (as far as typechecking is concerned,
+        // primitive operator application is strictly the same as normal function application).
+        //
+        // Note that the order of checking an argument against an inferred type or unifying the
+        // target type with an expected value doesn't matter (those operation commutes). We usually
+        // `unify` first, because it doesn't consume the context, while `check` needs an owned
+        // value.
         Term::Op1(op, t) => {
             let (ty_arg, ty_res) = get_uop_type(state, op)?;
 
-            type_check_(state, ctxt.clone(), lin, linearizer.scope(), t, ty_arg)?;
+            //TODO: this should go after the call to `subsumption`, to avoid context cloning, once
+            //we get rid of the special casing of type instantation below. For the time being, the
+            //instantiation is depending on this check having happened before, so we have to leave
+            //it as it is.
+            check(state, ctxt.clone(), lin, linearizer.scope(), t, ty_arg)?;
 
             let instantiated = instantiate_foralls(state, ty_res, ForallInst::Ptr);
-            unify(state, &ctxt, ty, instantiated)
+            subsumption(state, &ctxt, instantiated, ty)
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Op2(op, t1, t2) => {
             let (ty_arg1, ty_arg2, ty_res) = get_bop_type(state, op)?;
 
-            unify(state, &ctxt, ty, ty_res).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
-            type_check_(state, ctxt.clone(), lin, linearizer.scope(), t1, ty_arg1)?;
-            type_check_(state, ctxt, lin, linearizer, t2, ty_arg2)
+            subsumption(state, &ctxt, ty_res, ty)
+                .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
+
+            check(state, ctxt.clone(), lin, linearizer.scope(), t1, ty_arg1)?;
+            check(state, ctxt, lin, linearizer, t2, ty_arg2)
         }
         Term::OpN(op, args) => {
             let (tys_op, ty_ret) = get_nop_type(state, op)?;
@@ -1434,19 +1526,17 @@ fn type_check_<L: Linearizer>(
 
             tys_op.into_iter().zip(args.iter()).try_for_each(
                 |(ty_t, t)| -> Result<_, TypecheckError> {
-                    type_check_(state, ctxt.clone(), lin, linearizer.scope(), t, ty_t)?;
+                    check(state, ctxt.clone(), lin, linearizer.scope(), t, ty_t)?;
                     Ok(())
                 },
             )?;
 
             Ok(())
         }
-        Term::Annotated(annot, rt) => {
-            type_check_annotated(state, ctxt, lin, linearizer, annot, rt, ty)
-        }
+        Term::Annotated(annot, rt) => check_annotated(state, ctxt, lin, linearizer, annot, rt, ty),
         Term::SealingKey(_) => unify(state, &ctxt, ty, mk_uniftype::sym())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
-        Term::Sealed(_, t, _) => type_check_(state, ctxt, lin, linearizer, t, ty),
+        Term::Sealed(_, t, _) => check(state, ctxt, lin, linearizer, t, ty),
         Term::Import(_) => unify(state, &ctxt, ty, mk_uniftype::dynamic())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
         // We use the apparent type of the import for checking. This function doesn't recursively
@@ -1465,7 +1555,21 @@ fn type_check_<L: Linearizer>(
     }
 }
 
-fn type_check_field<L: Linearizer>(
+/// Change from inference mode to checking mode, and apply a potential subsumption rule.
+///
+/// Currently, there is no subtyping (until RFC004 is implemented), hence this function simply
+/// performs unification (put differently, the subtyping relation is the equality relation). In the
+/// future, this function might implement a non-trivial subsumption rule.
+pub fn subsumption(
+    state: &mut State,
+    ctxt: &Context,
+    inferred: UnifType,
+    checked: UnifType,
+) -> Result<(), UnifError> {
+    unify(state, ctxt, checked, inferred)
+}
+
+fn check_field<L: Linearizer>(
     state: &mut State,
     ctxt: Context,
     lin: &mut Linearization<L::Building>,
@@ -1476,7 +1580,7 @@ fn type_check_field<L: Linearizer>(
 ) -> Result<(), TypecheckError> {
     linearizer.add_field_metadata(lin, field);
 
-    type_check_with_annot(
+    check_with_annot(
         state,
         ctxt,
         lin,
@@ -1488,7 +1592,7 @@ fn type_check_field<L: Linearizer>(
     )
 }
 
-fn type_check_annotated<L: Linearizer>(
+fn check_annotated<L: Linearizer>(
     state: &mut State,
     ctxt: Context,
     lin: &mut Linearization<L::Building>,
@@ -1497,16 +1601,16 @@ fn type_check_annotated<L: Linearizer>(
     rt: &RichTerm,
     ty: UnifType,
 ) -> Result<(), TypecheckError> {
-    type_check_with_annot(state, ctxt, lin, linearizer, annot, Some(rt), ty, rt.pos)
+    check_with_annot(state, ctxt, lin, linearizer, annot, Some(rt), ty, rt.pos)
 }
 
-/// Subfunction handling the common part of typechecking term with type or contract annotation, with
+/// Function handling the common part of typechecking terms with type or contract annotation, with
 /// or without definitions. This encompasses both standalone type annotation (where `value` is
 /// always `Some(_)`) as well as field definiitions (where `value` may or may not be defined).
 ///
 /// The last argument is a position to use for error reporting when `value` is `None`.
 #[allow(clippy::too_many_arguments)] // TODO: Is it worth doing something about it?
-fn type_check_with_annot<L: Linearizer>(
+fn check_with_annot<L: Linearizer>(
     state: &mut State,
     ctxt: Context,
     lin: &mut Linearization<L::Building>,
@@ -1532,7 +1636,7 @@ fn type_check_with_annot<L: Linearizer>(
             let instantiated = instantiate_foralls(state, uty2.clone(), ForallInst::Constant);
 
             unify(state, &ctxt, uty2, ty).map_err(|err| err.into_typecheck_err(state, pos))?;
-            type_check_(state, ctxt, lin, linearizer, value, instantiated)
+            check(state, ctxt, lin, linearizer, value, instantiated)
         }
         // A annotation without a type but with a contract switches the typechecker back to walk
         // mode. If there are several contracts, we arbitrarily chose the first one as the apparent
@@ -1569,7 +1673,7 @@ fn type_check_with_annot<L: Linearizer>(
         }
         // A non-empty value without a type or a contract annotation is typechecked in the same way
         // as its inner value
-        (_, Some(value)) => type_check_(state, ctxt, lin, linearizer, value, ty),
+        (_, Some(value)) => check(state, ctxt, lin, linearizer, value, ty),
         // A empty value is a record field without definition. We don't check anything, and infer
         // its type to be either the first annotation defined if any, or `Dyn` otherwise.
         //
@@ -1586,6 +1690,28 @@ fn type_check_with_annot<L: Linearizer>(
     }
 }
 
+/// Infer a type for an expression.
+///
+/// `infer` corresponds to the inference mode of bidirectional typechecking. Nickel uses a mix of
+/// bidirectional typechecking together with traditional ML-like unification. In practice, to avoid
+/// duplicating a lot of rules for both checking mode and inference mode, the current [`check`]
+/// function mixes both and inference simply corresponds to checking against a free unification
+/// variable.
+///
+/// Still, using this dedicated method - although it is a thin wrapper - helps making clear when
+/// inference mode is used and when checking mode is used in the typechecking algorithm.
+fn infer<L: Linearizer>(
+    state: &mut State,
+    ctxt: Context,
+    lin: &mut Linearization<L::Building>,
+    linearizer: L,
+    rt: &RichTerm,
+) -> Result<UnifType, TypecheckError> {
+    let inferred = state.table.fresh_type_uvar();
+    check(state, ctxt, lin, linearizer, rt, inferred.clone())?;
+    Ok(inferred.into_root(state.table))
+}
+
 /// Determine the type of a let-bound expression.
 ///
 /// Call [`apparent_type`] to see if the binding is annotated. If it is, return this type as a
@@ -1602,7 +1728,7 @@ fn type_check_with_annot<L: Linearizer>(
 ///     * in strict mode, the wildcard is typechecked, and we return the unification variable
 ///       corresponding to it.
 fn binding_type(state: &mut State, t: &Term, ctxt: &Context, strict: bool) -> UnifType {
-    apparent_or_uvar(
+    apparent_or_infer(
         state,
         apparent_type(t, Some(&ctxt.type_env), Some(state.resolver)),
         ctxt,
@@ -1612,7 +1738,7 @@ fn binding_type(state: &mut State, t: &Term, ctxt: &Context, strict: bool) -> Un
 
 /// Same as `binding_type` but for record field definition.
 fn field_type(state: &mut State, field: &Field, ctxt: &Context, strict: bool) -> UnifType {
-    apparent_or_uvar(
+    apparent_or_infer(
         state,
         field_apparent_type(field, Some(&ctxt.type_env), Some(state.resolver)),
         ctxt,
@@ -1620,7 +1746,11 @@ fn field_type(state: &mut State, field: &Field, ctxt: &Context, strict: bool) ->
     )
 }
 
-fn apparent_or_uvar(
+/// Either returns the exact type annotation extracted as an apparent type, or return a fresh
+/// unification variable, for the type to be inferred by the typechecker, in enforce mode.
+///
+/// In walk mode, returns the type as approximated by [`apparent_type`].
+fn apparent_or_infer(
     state: &mut State,
     aty: ApparentType,
     ctxt: &Context,
@@ -1676,11 +1806,10 @@ fn replace_wildcards_with_var(
 
 /// Different kinds of apparent types (see [`apparent_type`]).
 ///
-/// Indicate the nature of an apparent type. In particular, when in strict mode, the typechecker
-/// throws away approximations as it can do better and infer the actual type of an expression by
-/// generating a fresh unification variable.  In non-strict mode, however, the approximation is the
-/// best we can do. This type allows the caller of `apparent_type` to determine which situation it
-/// is.
+/// Indicate the nature of an apparent type. In particular, when in enforce mode, the typechecker
+/// throws away approximations as it can do better and infer the actual type of an expression.  In
+/// walk mode, however, the approximation is the best we can do. This type allows the caller of
+/// `apparent_type` to determine which situation it is.
 #[derive(Debug)]
 pub enum ApparentType {
     /// The apparent type is given by a user-provided annotation.
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index 776e3bcf..cd5f44c8 100644
--- a/src/typecheck/operation.rs
+++ b/src/typecheck/operation.rs
@@ -2,10 +2,11 @@
 use super::*;
 use crate::{
     error::TypecheckError,
+    label::{Polarity, TypeVarData},
     term::{BinaryOp, NAryOp, RecordExtKind, UnaryOp},
     types::TypeF,
 };
-use crate::{mk_uty_arrow, mk_uty_enum, mk_uty_enum_row, mk_uty_record, mk_uty_row};
+use crate::{mk_uty_arrow, mk_uty_enum, mk_uty_record};
 
 /// Type of unary operations.
 pub fn get_uop_type(
@@ -425,6 +426,13 @@ pub fn get_bop_type(
             mk_uniftype::dynamic(),
             mk_uniftype::dynamic(),
         ),
+        // Morally: Sym -> Lbl -> TypeVarData
+        // Actual: Sym -> Dyn -> TypeVarData
+        BinaryOp::LookupTypeVar() => (
+            mk_uniftype::sym(),
+            mk_uniftype::dynamic(),
+            TypeVarData::unif_type(),
+        ),
     })
 }
 
@@ -464,5 +472,15 @@ pub fn get_nop_type(
         ),
         // This should not happen, as MergeContract() is only produced during evaluation.
         NAryOp::MergeContract() => panic!("cannot typecheck MergeContract()"),
+        // Morally: Sym -> Polarity -> Lbl -> Lbl
+        // Actual: Sym -> Polarity -> Dyn -> Dyn
+        NAryOp::InsertTypeVar() => (
+            vec![
+                mk_uniftype::sym(),
+                Polarity::unif_type(),
+                mk_uniftype::dynamic(),
+            ],
+            mk_uniftype::dynamic(),
+        ),
     })
 }
diff --git a/src/types.rs b/src/types.rs
index b3d74186..e52aa0c2 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -137,6 +137,29 @@ pub enum VarKind {
     RecordRows,
 }
 
+impl From<VarKind> for Term {
+    fn from(value: VarKind) -> Self {
+        match value {
+            VarKind::Type => Term::Enum(Ident::new("Type")),
+            VarKind::EnumRows => Term::Enum(Ident::new("EnumRows")),
+            VarKind::RecordRows => Term::Enum(Ident::new("RecordRows")),
+        }
+    }
+}
+
+impl TryFrom<&Term> for VarKind {
+    type Error = ();
+
+    fn try_from(value: &Term) -> Result<Self, Self::Error> {
+        match value {
+            Term::Enum(type_) if type_.label() == "Type" => Ok(Self::Type),
+            Term::Enum(enum_rows) if enum_rows.label() == "EnumRows" => Ok(Self::EnumRows),
+            Term::Enum(record_rows) if record_rows.label() == "RecordRows" => Ok(Self::RecordRows),
+            _ => Err(()),
+        }
+    }
+}
+
 /// A Nickel type.
 ///
 /// # Generic representation (functor)
@@ -904,22 +927,21 @@ impl Types {
                 var_kind,
             } => {
                 use VarKind::*;
+
+                let sealing_key = Term::SealingKey(*sy);
                 let contract = match var_kind {
-                    Type => mk_app!(
-                        contract::forall_var(),
-                        Term::SealingKey(*sy),
-                        Term::from(pol)
-                    ),
-                    EnumRows | RecordRows => mk_app!(
-                        contract::forall_tail(),
-                        Term::SealingKey(*sy),
-                        Term::from(pol)
-                    ),
+                    Type => mk_app!(contract::forall_var(), sealing_key.clone()),
+                    EnumRows | RecordRows => mk_app!(contract::forall_tail(), sealing_key.clone()),
                 };
-
                 vars.insert(*var, contract);
+
                 *sy += 1;
-                body.subcontract(vars, pol, sy)?
+                mk_app!(
+                    contract::forall(),
+                    sealing_key,
+                    Term::from(pol),
+                    body.subcontract(vars, pol, sy)?
+                )
             }
             TypeF::Enum(ref erows) => erows.subcontract()?,
             TypeF::Record(ref rrows) => rrows.subcontract(vars, pol, sy)?,
diff --git a/stdlib/internals.ncl b/stdlib/internals.ncl
index 1123ef8b..0eaf05a4 100644
--- a/stdlib/internals.ncl
+++ b/stdlib/internals.ncl
@@ -25,9 +25,10 @@
       else
           %blame% label,
 
-  "$forall_var" = fun sealing_key polarity label value =>
-      let current-polarity = %polarity% label in
-      if polarity == current-polarity then
+  "$forall_var" = fun sealing_key label value =>
+      let current_polarity = %polarity% label in
+      let polarity = (%lookup_type_variable% sealing_key label).polarity in
+      if polarity == current_polarity then
           %unseal% sealing_key value (%blame% label)
       else
           # Here, we know that this term should be sealed, but to give the right
@@ -36,6 +37,9 @@
           # blaming polymorphic contracts.
           %seal% sealing_key (%chng_pol% label) value,
 
+  "$forall" = fun sealing_key polarity contract label value =>
+    contract (%insert_type_variable% sealing_key polarity label) value,
+
   "$enums" = fun case label value =>
       if %typeof% value == `Enum then
           %assume% case label value
@@ -89,8 +93,10 @@
       else
           %blame% (%label_with_message% "not a record" label),
 
-  "$forall_tail" = fun sealing_key polarity acc label value =>
-      if polarity == (%polarity% label) then
+  "$forall_tail" = fun sealing_key acc label value =>
+      let current_polarity = %polarity% label in
+      let polarity = (%lookup_type_variable% sealing_key label).polarity in
+      if polarity == current_polarity then
           if value == {} then
             let tagged_label = %label_with_message% "polymorphic tail mismatch" label in
             let tail = %record_unseal_tail% sealing_key tagged_label value in


Test patch:
diff --git a/tests/integration/destructuring.rs b/tests/integration/destructuring.rs
index 3e07e497..7369a808 100644
--- a/tests/integration/destructuring.rs
+++ b/tests/integration/destructuring.rs
@@ -60,7 +60,7 @@ fn typecontract_fail() {
 fn type_mismatch_fail() {
     assert_matches!(
         eval_file("destructuring/type_mismatch_fail.ncl"),
-        Err(Error::TypecheckError(TypecheckError::RowMismatch(..)))
+        Err(Error::TypecheckError(TypecheckError::TypeMismatch(..)))
     )
 }
 
@@ -68,7 +68,7 @@ fn type_mismatch_fail() {
 fn type_mismatch_field_pattern_fail() {
     assert_matches!(
         eval_file("destructuring/type_mismatch_field_pattern_fail.ncl"),
-        Err(Error::TypecheckError(TypecheckError::RowMismatch(..)))
+        Err(Error::TypecheckError(TypecheckError::TypeMismatch(..)))
     )
 }
 
@@ -76,7 +76,7 @@ fn type_mismatch_field_pattern_fail() {
 fn type_mismatch_nested_destructuring_fail() {
     assert_matches!(
         eval_file("destructuring/type_mismatch_nested_destructuring_fail.ncl"),
-        Err(Error::TypecheckError(TypecheckError::RowMismatch(..)))
+        Err(Error::TypecheckError(TypecheckError::TypeMismatch(..)))
     )
 }
 
diff --git a/tests/snapshot/snapshots/snapshot__error_annotated_record_pattern_typecheck_fail.ncl.snap b/tests/snapshot/snapshots/snapshot__error_annotated_record_pattern_typecheck_fail.ncl.snap
index a2ec6b2f..a4812cff 100644
--- a/tests/snapshot/snapshots/snapshot__error_annotated_record_pattern_typecheck_fail.ncl.snap
+++ b/tests/snapshot/snapshots/snapshot__error_annotated_record_pattern_typecheck_fail.ncl.snap
@@ -2,19 +2,14 @@
 source: tests/snapshot/main.rs
 expression: snapshot
 ---
-error: incompatible rows declaration
-  ┌─ [INPUTS_PATH]/errors/annotated_record_pattern_typecheck_fail.ncl:2:22
+error: incompatible types
+  ┌─ [INPUTS_PATH]/errors/annotated_record_pattern_typecheck_fail.ncl:2:28
   │
 2 │   let { x : Bool } = { x = 5 } in
-  │                      ^^^^^^^^^ this expression
+  │                            ^ this expression
   │
-  = The type of the expression was expected to have the row `x: Bool`
-  = The type of the expression was inferred to have the row `x: Number`
-  = Could not match the two declaration of `x`
-
-error: While typing field `x`: incompatible types
- = The type of the expression was expected to be `Bool`
- = The type of the expression was inferred to be `Number`
- = These types are not compatible
+  = The type of the expression was expected to be `Bool`
+  = The type of the expression was inferred to be `Number`
+  = These types are not compatible
 
 
diff --git a/tests/snapshot/snapshots/snapshot__error_nested_annotated_record_pattern_typecheck_fail.ncl.snap b/tests/snapshot/snapshots/snapshot__error_nested_annotated_record_pattern_typecheck_fail.ncl.snap
index ee6484de..decf953a 100644
--- a/tests/snapshot/snapshots/snapshot__error_nested_annotated_record_pattern_typecheck_fail.ncl.snap
+++ b/tests/snapshot/snapshots/snapshot__error_nested_annotated_record_pattern_typecheck_fail.ncl.snap
@@ -2,19 +2,14 @@
 source: tests/snapshot/main.rs
 expression: snapshot
 ---
-error: incompatible rows declaration
-  ┌─ [INPUTS_PATH]/errors/nested_annotated_record_pattern_typecheck_fail.ncl:2:31
+error: incompatible types
+  ┌─ [INPUTS_PATH]/errors/nested_annotated_record_pattern_typecheck_fail.ncl:2:43
   │
 2 │   let { x = { a : Number }} = { x = { a = "" }} in
-  │                               ^^^^^^^^^^^^^^^^^ this expression
+  │                                           ^^ this expression
   │
-  = The type of the expression was expected to have the row `x.a: Number`
-  = The type of the expression was inferred to have the row `x.a: String`
-  = Could not match the two declaration of `x.a`
-
-error: While typing field `x.a`: incompatible types
- = The type of the expression was expected to be `Number`
- = The type of the expression was inferred to be `String`
- = These types are not compatible
+  = The type of the expression was expected to be `Number`
+  = The type of the expression was inferred to be `String`
+  = These types are not compatible