Repository: tweag/nickel
Pull request #1190 (2023-03-19 00:10:35)

flake.lock: Update
Automated changes by the [update-flake-lock](https://github.com/DeterminateSystems/update-flake-lock) GitHub Action.

```
Flake lock file updates:

• Updated input 'flake-utils':
    'github:numtide/flake-utils/3db36a8b464d0c4532ba1c7dda728f4576d6d073' (2023-02-13)
  → 'github:numtide/flake-utils/93a2b84fc4b70d9e089d029deacc3583435c2ed6' (2023-03-15)
• Updated input 'nixpkgs':
    'github:NixOS/nixpkgs/0c4800d579af4ed98ecc47d464a5e7b0870c4b1f' (2023-03-10)
  → 'github:NixOS/nixpkgs/ac718d02867a84b42522a0ece52d841188208f2c' (2023-03-15)
• Updated input 'pre-commit-hooks':
    'github:cachix/pre-commit-hooks.nix/1a20b9708962096ec2481eeb2ddca29ed747770a' (2023-03-09)
  → 'github:cachix/pre-commit-hooks.nix/32b1dbedfd77892a6e375737ef04d8efba634e9e' (2023-03-16)
• Updated input 'pre-commit-hooks/nixpkgs-stable':
    'github:NixOS/nixpkgs/2f9fd351ec37f5d479556cd48be4ca340da59b8f' (2023-01-15)
  → 'github:NixOS/nixpkgs/9b8e5abb18324c7fe9f07cb100c3cd4a29cda8b8' (2023-03-15)
• Updated input 'rust-overlay':
    'github:oxalica/rust-overlay/1c8200cdc4c830d937fbf8b19e1f3e83daf3370a' (2023-03-11)
  → 'github:oxalica/rust-overlay/7313c06ac334d6262ddfe30a38b3abc3da6bd565' (2023-03-18)
```

### Running GitHub Actions on this PR

GitHub Actions will not run workflows on pull requests which are opened by a GitHub Action.

To run GitHub Actions workflows on this PR, run:

```sh
git branch -D update_flake_lock_action
git fetch origin
git checkout update_flake_lock_action
git commit --amend --no-edit
git push origin update_flake_lock_action --force
```


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/flake.lock b/flake.lock
index 650951b0..4d13156d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -72,11 +72,11 @@
     },
     "flake-utils_2": {
       "locked": {
-        "lastModified": 1676283394,
-        "narHash": "sha256-XX2f9c3iySLCw54rJ/CZs+ZK6IQy7GXNY4nSOyu2QG4=",
+        "lastModified": 1678901627,
+        "narHash": "sha256-U02riOqrKKzwjsxc/400XnElV+UtPUQWpANPlyazjH0=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "3db36a8b464d0c4532ba1c7dda728f4576d6d073",
+        "rev": "93a2b84fc4b70d9e089d029deacc3583435c2ed6",
         "type": "github"
       },
       "original": {
@@ -108,11 +108,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1678470307,
-        "narHash": "sha256-OEeMUr3ueLIXyW/OaFUX5jUdimyQwMg/7e+/Q0gC/QE=",
+        "lastModified": 1678898370,
+        "narHash": "sha256-xTICr1j+uat5hk9FyuPOFGxpWHdJRibwZC+ATi0RbtE=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "0c4800d579af4ed98ecc47d464a5e7b0870c4b1f",
+        "rev": "ac718d02867a84b42522a0ece52d841188208f2c",
         "type": "github"
       },
       "original": {
@@ -123,11 +123,11 @@
     },
     "nixpkgs-stable": {
       "locked": {
-        "lastModified": 1673800717,
-        "narHash": "sha256-SFHraUqLSu5cC6IxTprex/nTsI81ZQAtDvlBvGDWfnA=",
+        "lastModified": 1678872516,
+        "narHash": "sha256-/E1YwtMtFAu2KUQKV/1+KFuReYPANM2Rzehk84VxVoc=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "2f9fd351ec37f5d479556cd48be4ca340da59b8f",
+        "rev": "9b8e5abb18324c7fe9f07cb100c3cd4a29cda8b8",
         "type": "github"
       },
       "original": {
@@ -150,11 +150,11 @@
         "nixpkgs-stable": "nixpkgs-stable"
       },
       "locked": {
-        "lastModified": 1678376203,
-        "narHash": "sha256-3tyYGyC8h7fBwncLZy5nCUjTJPrHbmNwp47LlNLOHSM=",
+        "lastModified": 1678976941,
+        "narHash": "sha256-skNr08frCwN9NO+7I77MjOHHAw+L410/37JknNld+W4=",
         "owner": "cachix",
         "repo": "pre-commit-hooks.nix",
-        "rev": "1a20b9708962096ec2481eeb2ddca29ed747770a",
+        "rev": "32b1dbedfd77892a6e375737ef04d8efba634e9e",
         "type": "github"
       },
       "original": {
@@ -207,11 +207,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1678501303,
-        "narHash": "sha256-92s2NOlcvydz0Cxi1OOq/bs7SQc38TaqzuzdHsRANhA=",
+        "lastModified": 1679106165,
+        "narHash": "sha256-03Opt2yu4E/AIFjvlgib0/nhMn6B4B/t/nvwS2bzOGw=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "1c8200cdc4c830d937fbf8b19e1f3e83daf3370a",
+        "rev": "7313c06ac334d6262ddfe30a38b3abc3da6bd565",
         "type": "github"
       },
       "original": {
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..ec4ba7cd 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,
@@ -2305,7 +2305,6 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                 MergeMode::Standard,
                 &mut self.call_stack,
             ),
-
             BinaryOp::Hash() => {
                 let mk_err_fst = |t1| {
                     Err(EvalError::TypeError(
@@ -2798,6 +2797,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 +3193,204 @@ 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(),
+                )))
+            }
+            NAryOp::ArraySlice() => {
+                let mut args = args.into_iter();
+
+                let (
+                    Closure {
+                        body:
+                            RichTerm {
+                                term: t1,
+                                pos: pos1,
+                            },
+                        ..
+                    },
+                    fst_pos,
+                ) = args.next().unwrap();
+
+                let (
+                    Closure {
+                        body:
+                            RichTerm {
+                                term: t2,
+                                pos: pos2,
+                            },
+                        ..
+                    },
+                    snd_pos,
+                ) = args.next().unwrap();
+
+                let (
+                    Closure {
+                        body:
+                            RichTerm {
+                                term: t3,
+                                pos: pos3,
+                            },
+                        env: env3,
+                    },
+                    third_pos,
+                ) = args.next().unwrap();
+                debug_assert!(args.next().is_none());
+
+                let Term::Num(ref start) = &*t1 else {
+                    return Err(EvalError::TypeError(
+                        String::from("Number"),
+                        String::from("%array_slice%, 1st argument"),
+                        fst_pos,
+                        RichTerm {
+                            term: t1,
+                            pos: pos1,
+                        },
+                    ));
+                };
+
+                let Term::Num(ref end) = &*t2 else {
+                    return Err(EvalError::TypeError(
+                        String::from("Number"),
+                        String::from("%array_slice%, 2nd argument"),
+                        snd_pos,
+                        RichTerm {
+                            term: t2,
+                            pos: pos2,
+                        },
+                    ));
+                };
+
+                let t3_owned = t3.into_owned();
+
+                let Term::Array(mut array, attrs) = t3_owned else {
+                    return Err(EvalError::TypeError(
+                        String::from("Array"),
+                        String::from("%array_slice%, 3rd argument"),
+                        third_pos,
+                        RichTerm::new(t3_owned, pos3),
+                    ));
+                };
+
+                let Ok(start_as_usize) = usize::try_from(start) else {
+                    return Err(EvalError::Other(
+                        format!(
+                            "%array_slice%: expected the 1st argument (start) to be a positive integer smaller than {}, got {start}",
+                            usize::MAX
+                        ),
+                        pos_op
+                    ));
+                };
+
+                let Ok(end_as_usize) = usize::try_from(end) else {
+                    return Err(EvalError::Other(
+                        format!(
+                            "%array_slice%: expected the 2nd argument (end) to be a positive integer smaller than {}, got {end}",
+                            usize::MAX
+                        ),
+                        pos_op
+                    ));
+                };
+
+                let result = array.slice(start_as_usize, end_as_usize);
+
+                if let Err(crate::term::array::OutOfBoundError) = result {
+                    return Err(EvalError::Other(
+                        format!(
+                            "%array_slice%: index out of bounds. Expected `start <= end <= {}`, but got `start={start}` and `end={end}`.",
+                            array.len()
+                        ),
+                        pos_op
+                    ));
+                };
+
+                Ok(Closure {
+                    body: RichTerm::new(Term::Array(array, attrs), pos_op_inh),
+                    env: env3,
+                })
+            }
         }
     }
 }
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..1d2588bd 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,10 @@ 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)),
+    "array_slice" <t1: ArgRule> <t2: ArgRule> <t3: ArgRule> =>
+        UniTerm::from(mk_opn!(NAryOp::ArraySlice(), t1, t2, t3)),
 }
 
 TypeBuiltin: Types = {
@@ -1029,6 +1034,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),
@@ -1067,6 +1074,7 @@ extern {
         "label_with_notes" => Token::Normal(NormalToken::LabelWithNotes),
         "label_append_note" => Token::Normal(NormalToken::LabelAppendNote),
         "label_push_diag" => Token::Normal(NormalToken::LabelPushDiag),
+        "array_slice" => Token::Normal(NormalToken::ArraySlice),
 
         "{" => Token::Normal(NormalToken::LBrace),
         "}" => Token::Normal(NormalToken::RBrace),
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 5da96744..19eea13c 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,
@@ -320,6 +324,8 @@ pub enum NormalToken<'input> {
     LabelAppendNote,
     #[token("%label_push_diag%")]
     LabelPushDiag,
+    #[token("%array_slice%")]
+    ArraySlice,
 
     #[token("{")]
     LBrace,
diff --git a/src/stdlib.rs b/src/stdlib.rs
index faf4c426..72881c13 100644
--- a/src/stdlib.rs
+++ b/src/stdlib.rs
@@ -5,7 +5,7 @@ use crate::term::make as mk_term;
 use crate::term::RichTerm;
 
 /// This is an array containing all the Nickel standard library modules.
-pub fn modules() -> [StdlibModule; 8] {
+pub fn modules() -> [StdlibModule; 9] {
     [
         StdlibModule::Builtin,
         StdlibModule::Contract,
@@ -14,6 +14,7 @@ pub fn modules() -> [StdlibModule; 8] {
         StdlibModule::String,
         StdlibModule::Number,
         StdlibModule::Function,
+        StdlibModule::Enum,
         StdlibModule::Internals,
     ]
 }
@@ -28,6 +29,7 @@ pub enum StdlibModule {
     String,
     Number,
     Function,
+    Enum,
     Internals,
 }
 
@@ -41,6 +43,7 @@ impl StdlibModule {
             StdlibModule::String => "<stdlib/string.ncl>",
             StdlibModule::Number => "<stdlib/number.ncl>",
             StdlibModule::Function => "<stdlib/function.ncl>",
+            StdlibModule::Enum => "<stdlib/enum.ncl>",
             StdlibModule::Internals => "<stdlib/internals.ncl>",
         }
     }
@@ -54,6 +57,7 @@ impl StdlibModule {
             StdlibModule::String => include_str!("../stdlib/string.ncl"),
             StdlibModule::Number => include_str!("../stdlib/number.ncl"),
             StdlibModule::Function => include_str!("../stdlib/function.ncl"),
+            StdlibModule::Enum => include_str!("../stdlib/enum.ncl"),
             StdlibModule::Internals => include_str!("../stdlib/internals.ncl"),
         }
     }
@@ -73,6 +77,7 @@ impl TryFrom<Ident> for StdlibModule {
             "string" => StdlibModule::String,
             "number" => StdlibModule::Number,
             "function" => StdlibModule::Function,
+            "enum" => StdlibModule::Enum,
             "internals" => StdlibModule::Internals,
             _ => return Err(UnknownStdlibModule),
         };
@@ -90,6 +95,7 @@ impl From<StdlibModule> for Ident {
             StdlibModule::String => "string",
             StdlibModule::Number => "number",
             StdlibModule::Function => "function",
+            StdlibModule::Enum => "enum",
             StdlibModule::Internals => "internals",
         };
         Ident::from(name)
@@ -119,6 +125,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/array.rs b/src/term/array.rs
index 13f24fb6..d3a318ea 100644
--- a/src/term/array.rs
+++ b/src/term/array.rs
@@ -53,6 +53,10 @@ impl ArrayAttrs {
     }
 }
 
+/// A Nickel array, represented as a view (slice) into a shared backing array. The view is
+/// delimited by `start` (included) and `end` (excluded). This allows to take the tail of an array,
+/// or an arbitrary slice, in constant time, providing actual linear time iteration when
+/// imlementing recursive functions, such as folds, for example.
 #[derive(Debug, Clone, PartialEq)]
 pub struct Array {
     inner: Rc<[RichTerm]>,
@@ -60,6 +64,8 @@ pub struct Array {
     end: usize,
 }
 
+pub struct OutOfBoundError;
+
 impl Array {
     /// Creates a Nickel array from reference-counted slice.
     pub fn new(inner: Rc<[RichTerm]>) -> Self {
@@ -69,6 +75,23 @@ impl Array {
         Self { inner, start, end }
     }
 
+    /// Resize the view to be a a sub-view of the current one, by considering a slice `start`
+    /// (included) to `end` (excluded).
+    ///
+    /// The parameters must satisfy `0 <= start <= end <= self.end - self.start`. Otherwise,
+    /// `Err(..)` is returned.
+    pub fn slice(&mut self, start: usize, end: usize) -> Result<(), OutOfBoundError> {
+        if start > end || end > self.len() {
+            return Err(OutOfBoundError);
+        }
+
+        let prev_start = self.start;
+        self.start = prev_start + start;
+        self.end = prev_start + end;
+
+        Ok(())
+    }
+
     /// Returns the effective length of the array.
     pub fn len(&self) -> usize {
         self.end - self.start
diff --git a/src/term/mod.rs b/src/term/mod.rs
index 0b4a660d..ad0435e0 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,18 @@ 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(),
+    /// Return a sub-array corresponding to a range. Given that Nickel uses array slices under the
+    /// hood, as long as the array isn't modified later, this operation is constant in time and
+    /// memory.
+    ArraySlice(),
 }
 
 impl NAryOp {
@@ -1372,7 +1388,9 @@ impl NAryOp {
             | NAryOp::StrReplaceRegex()
             | NAryOp::StrSubstr()
             | NAryOp::MergeContract()
-            | NAryOp::RecordUnsealTail() => 3,
+            | NAryOp::RecordUnsealTail()
+            | NAryOp::InsertTypeVar()
+            | NAryOp::ArraySlice() => 3,
             NAryOp::RecordSealTail() => 4,
         }
     }
@@ -1381,12 +1399,14 @@ impl NAryOp {
 impl fmt::Display for NAryOp {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match self {
-            NAryOp::StrReplace() => write!(f, "strReplace"),
-            NAryOp::StrReplaceRegex() => write!(f, "strReplaceRegex"),
+            NAryOp::StrReplace() => write!(f, "str_replace"),
+            NAryOp::StrReplaceRegex() => write!(f, "str_replace_regex"),
             NAryOp::StrSubstr() => write!(f, "substring"),
-            NAryOp::MergeContract() => write!(f, "mergeContract"),
-            NAryOp::RecordSealTail() => write!(f, "%record_seal_tail%"),
-            NAryOp::RecordUnsealTail() => write!(f, "%record_unseal_tail%"),
+            NAryOp::MergeContract() => write!(f, "merge_contract"),
+            NAryOp::RecordSealTail() => write!(f, "record_seal_tail"),
+            NAryOp::RecordUnsealTail() => write!(f, "record_unseal_tail"),
+            NAryOp::InsertTypeVar() => write!(f, "insert_type_variable"),
+            NAryOp::ArraySlice() => write!(f, "array_slice"),
         }
     }
 }
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..b0fccbcf 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,11 +426,18 @@ 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(),
+        ),
     })
 }
 
 pub fn get_nop_type(
-    _state: &mut State,
+    state: &mut State,
     op: &NAryOp,
 ) -> Result<(Vec<UnifType>, UnifType), TypecheckError> {
     Ok(match op {
@@ -462,7 +470,30 @@ pub fn get_nop_type(
             ],
             mk_uniftype::dynamic(),
         ),
+        // Num -> Num -> Array a -> Array a
+        NAryOp::ArraySlice() => {
+            let element_type = state.table.fresh_type_uvar();
+
+            (
+                vec![
+                    mk_uniftype::num(),
+                    mk_uniftype::num(),
+                    mk_uniftype::array(element_type.clone()),
+                ],
+                mk_uniftype::array(element_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/array.ncl b/stdlib/array.ncl
index f3c4f097..c23bcbda 100644
--- a/stdlib/array.ncl
+++ b/stdlib/array.ncl
@@ -47,7 +47,7 @@
             [ 2, 3 ]
         ```
         "%
-      = fun l => %tail% l,
+      = fun array => %array_slice% 1 (%length% array) array,
 
     drop_last : forall a. Array a -> Array a
       | doc m%"
@@ -59,11 +59,7 @@
             [ 1, 2 ]
         ```
         "%
-      # TODO: we need a slice primop
-      = fun l => l
-        |> reverse
-        |> drop_first
-        |> reverse,
+      = fun array => %array_slice% 0 (%length% array - 1) array,
 
     length : forall a. Array a -> Number
       | doc m%"
@@ -116,12 +112,62 @@
 
     fold_left : forall a b. (a -> b -> a) -> a -> Array b -> a
       | doc m%"
-        Fold a function over an array.
+        Fold a function over an array. Folds serve a similar purpose to loops or
+        iterators in a functional language like Nickel. `fold_left` iterates over
+        an array, by repeatedly applying a function over each element, threading
+        an additional arbitrary state (the accumulator, of type `a` in the
+        signature).
+
         `fold_left f init [x1, x2, ..., xn]` results in `f (... (f (f init x1) x2) ...) xn`.
 
         This function is strict in the intermediate accumulator.
 
-        For example:
+        # Left vs right
+
+        Folds come in two variants, left and right. How to decide which one to
+        use?
+
+        - If the folded function isn't associative (such as subtraction), then
+          each variant will give a different result. The choice is dictacted by
+          which one you need. For example:
+
+          ```nickel
+          array.fold_right (-) 0 [1, 2, 3, 4]
+           => -2
+          array.fold_left (-) 0 [1, 2, 3, 4]
+           => -10
+          ```
+        - If the folded function is associative, both `fold_right` and
+          `fold_left` return the same result. In that case, **`fold_left` is
+          generally preferred**, because it forces the evaluation of the
+          intermediate results resulting in less memory consumption and overall
+          better performance (outside of pathological cases).
+          `fold_left` also iterates from the start of the array, which
+          correponds to the usual behavior of loops and iterators in most
+          programming languages. There is one case where `fold_right` might be
+          preferred, see the next point.
+        - If the folded function is associative but _(left) short-circuiting_,
+          meaning that it can sometimes determine the result without using the
+          right argument, then `fold_right` provides early return. An example is
+          the boolean AND operator `&&`: when evaluating `left && right`, if
+          `left` is `false`, the whole expression will evaluate to `false`
+          without even evaluating `right`. Consider the following expression:
+
+          ```nickel
+          array.replicate 1000 true
+          # gives [false, .. true 1000 times]
+          |> array.prepend false
+          |> array.fold_right (&&) [false]
+          ```
+
+          Here, `fold_right` will stop at the first element, and the operation
+          runs in constant time, given the definition of `fold_right` and the
+          lazy evaluation of Nickel. If we had used `fold_left` instead, which
+          is closer to a standard iterator, we would have iterated over all of
+          the 1000 elements of the array.
+
+        # Examples
+
         ```nickel
           fold_left (fun acc e => acc + e) 0 [ 1, 2, 3 ] =>
             (((0 + 1) + 2) 3) =>
@@ -142,10 +188,21 @@
 
     fold_right : forall a b. (a -> b -> b) -> b -> Array a -> b
       | doc m%"
-        Fold a function over a array.
+        Fold a function over an array. Folds serve a similar purpose to loops or
+        iterators in a functional language like Nickel. `fold_right` iterates
+        over an array, by repeatedly applying a function to each element and
+        threading an additional arbitrary state (the accumulator of type `a` in
+        the signature).
+
         `fold_right f init [x1, x2, ..., xn]` results in `f x1 (f x2 (... (f xn init) ...))`.
 
-        For example:
+        # Left vs right
+
+        Folds come in two variants, left and right. How to decide which one to
+        use? Please refer to the documentation of `fold_left`.
+
+        # Examples
+
         ```nickel
           fold_right (fun e acc => acc @ [e]) [] [ 1, 2, 3 ] =>
             ((([] @ [3]) @ [2]) @ [1]) =>
@@ -346,5 +403,193 @@
         if %length% arr <= 1
         then arr
         else [ %head% arr ] @ (%tail% arr |> flat_map (fun a => [v, a])),
+
+    slice
+      : forall a. Number -> Number -> Array a -> Array a
+      | doc m%"
+          `slice start end array` returns the slice of `array` between `start` (included) and
+          `end` (excluded).
+
+          # Preconditions
+
+          In `slice start end value`, `start` and `end` must be positive
+          integers such that `0 <= start <= end <= array.length value`.
+
+          # Examples
+
+          ```nickel
+          slice 1 3 [ 0, 1, 2, 3, 4, 5]
+            => [ 1, 2 ]
+          slice 0 3 [ "Hello", "world", "!" ]
+            => [ "Hello", "world", "!" ]
+          slice 2 3 [ "Hello", "world", "!" ]
+            => [ "!" ]
+           ```
+        "%
+      = fun start end value => %array_slice% start end value,
+
+    split_at
+      : forall a. Number -> Array a -> {left: Array a, right: Array a}
+      | doc m%"
+          Splits an array in two at a given index, and puts all the elements
+          to the left of the element at the given index (excluded) in the
+          `left` field, and the rest of the array in the `right` field.
+
+          # Preconditions
+
+          In `split_at inded value`, `index` must be a positive integer such
+          that `0 <= index <= array.length value`.
+
+          # Examples
+
+          ```nickel
+          split_at 2 [ 0, 1, 2, 3, 4, 5]
+            => { left = [ 2, 3, 4, 5 ], right = [ 0, 1 ] }
+          split_at 0 [ "Hello", "world", "!" ]
+            => { left = [  ], right = [ "Hello", "world", "!" ] }
+          split_at 3 [ "Hello", "world", "!" ]
+            => { left = [ "Hello", "world", "!" ], right = [  ] }
+          ```
+        "%
+      = fun index value => {
+        left = %array_slice% 0 index value,
+        right = %array_slice% index (%length% value) value
+      },
+
+    replicate
+      : forall a. Number -> a -> Array a
+      | doc m%"
+          `replicate n x` creates an array containing `x` exactly `n` times.
+
+          # Preconditions
+
+          `n` must be an integer greater or equal to `0`.
+
+          # Examples
+
+          ```nickel
+          replicate 0 false
+            => [ ]
+          replicate 5 "x"
+            => [ "x", "x", "x", "x", "x" ]
+          ```
+        "%
+      = fun n x => %generate% n (fun _i => x),
+
+    range_step
+      : Number -> Number -> Number -> Array Number
+      | doc m%"
+          `range_step start end step` generates the array of numbers
+          `[start, start + step, start + 2*step, ..]` up to the first element
+          (excluded) larger than or equal to `end`
+
+          # Preconditions
+
+          In `range_step start end step`, `start` and `end` must satisfy `start
+          <= end`. `step` must be strictly greater than `0`.
+
+          # Examples
+
+          ```nickel
+          range_step (-1.5) 2 0.5
+           => [ -1.5, -1, -0.5, 0, 0.5, 1, 1.5 ]
+          ```
+        "%
+      = fun start end step => %generate%
+          ((end - start) / step |> number.floor)
+          (fun i => start + i*step),
+
+    range
+      : Number -> Number -> Array Number
+      | doc m%"
+          `range start end` generates the array of numbers
+          `[start, start + 1, start + 2, ..]` up to the first element
+          (excluded) larger than or equal to `end`.
+
+          `range start end` is equivalent to `range_step start end 1`.
+
+          # Preconditions
+
+          In `range_step start end`, `start` and `end` must satisfy
+          `start <= end`.
+
+          # Examples
+
+          ```nickel
+          range 0 5
+           => [ 0, 1, 2, 3, 4 ]
+          ```
+        "%
+      = fun start end => range_step start end 1,
+
+    reduce_left
+      : forall a. (a -> a -> a) -> Array a -> a
+      | doc m%"
+        Reduces the elements to a single one, by repeatedly applying a reducing
+        operation. If the array is empty, returns an empty array.
+
+        `reduce_left` associates to the left, that is
+        `reduce_left op [x1, x2, ..., xn]` results in `op (... (op (op x1 x2) x3) ...) xn`.
+
+        `reduce_left` is the same as `fold_left`, but uses the first element as
+        the initial accumulator.
+
+        # Left vs right
+
+        The rationale to decide between `fold_left` and `fold_right` applies to
+        `reduce_left` and `reduce_right` as well. See the documentation of
+        `fold_left`.
+
+        # Examples
+
+        ```nickel
+          reduce_left (@) [ [1, 2], [3], [4,5] ]
+            => (([1, 2] @ [3]) @ [4,5])
+            => [ 1, 2, 4, 5 ]
+          reduce_left (-) [ 1, 2, 3, 4]
+            => ((1 - 2) - 3) - 4
+            => -8
+        ```
+        "%
+      = fun f array =>
+        let first = %elem_at% array 0 in
+        let rest = %array_slice% 1 (%length% array) array in
+        fold_left f first rest,
+
+    reduce_right
+      : forall a. (a -> a -> a) -> Array a -> a
+      | doc m%"
+        Reduces the elements to a single one, by repeatedly applying a reducing
+        operation. If the array is empty, returns an empty array.
+
+        `reduce_right` associates to the right, that is
+        `reduce_right op [x1, x2, ..., xn]` results in
+        `op x1 (op x2 (... (op xn-1 xn) ...))`.
+
+        `reduce_right` is the same as `fold_right`, but uses the last element as
+        the initial element.
+
+        # Left vs right
+
+        The rationale to decide between `fold_left` and `fold_right` applies to
+        `reduce_left` and `reduce_right` as well. See the documentation of
+        `fold_left`.
+
+        # Examples
+
+        ```nickel
+          reduce_right (@) [ [1, 2], [3], [4,5] ]
+            => [1, 2] @ ([3] @ [4,5])
+            => [ 1, 2, 4, 5 ]
+          reduce_right (-) [ 1, 2, 3, 4]
+            => 1 - (2 - (3 - 4))
+            => -2
+        ```
+        "%
+      = fun f array =>
+         let last_index = %length% array - 1 in
+         let last =  %elem_at% array last_index in
+         let rest = %array_slice% 0 last_index array in
+         fold_right f last rest,
   }
 }
diff --git a/stdlib/enum.ncl b/stdlib/enum.ncl
new file mode 100644
index 00000000..e4b04482
--- /dev/null
+++ b/stdlib/enum.ncl
@@ -0,0 +1,62 @@
+{
+    enum = {
+      Tag
+        | doc m%"
+          Contract to enforce the value is an enum tag.
+
+          # Examples
+
+          ```nickel
+            (`foo | Tag) =>
+              `foo
+            (`FooBar | Tag) =>
+              `FooBar
+            ("tag" | Tag) =>
+              error
+          ```
+          "%
+        = contract.from_predicate builtin.is_enum,
+
+      TagOrString
+        | doc m%%"
+            Accepts both enum tags and strings. Strings are automatically
+            converted to an enum tag.
+
+            `TagOrString` is typically used in conjunction with an enum type, to
+            accept tags represented as strings (e.g. coming from a JSON
+            serialization) as well.
+
+            # Examples
+
+            ``` nickel
+            let Schema = {
+              protocol
+                | enum.TagOrString
+                | [| `http, `ftp |],
+              port
+                | Number,
+              method
+                | enum.TagOrString
+                | [| `GET, `POST |]
+            } in
+            let serialized =
+              m%"
+                {"protocol": "http", "port": 80, "method": "GET"}
+              "%
+              |> builtin.deserialize `Json
+            in
+
+            serialized | Schema
+            ```
+          "%%
+        = fun label value =>
+          %typeof% value
+          |> match {
+            `String => %enum_from_str% value,
+            `Enum => value,
+             _ => contract.blame_with_message
+               "expected either a string or an enum tag"
+               label,
+            },
+    }
+}
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
diff --git a/stdlib/record.ncl b/stdlib/record.ncl
index a2425b10..f698ca85 100644
--- a/stdlib/record.ncl
+++ b/stdlib/record.ncl
@@ -107,7 +107,7 @@
         else
           r in
         %record_insert% field r content,
-    
+
     map_values : forall a b. (a -> b) -> {_: a} -> {_: b}
     | doc m%"
       Maps a function over every field value of a record.
@@ -159,7 +159,7 @@
     is_empty : forall a. {_: a} -> Bool
     | doc m%"
       Check whether a record is empty.
-      
+
       ```nickel
       is_empty {} => true
       is_empty { foo = 1 } => false
diff --git a/stdlib/string.ncl b/stdlib/string.ncl
index 1e673fca..268ee877 100644
--- a/stdlib/string.ncl
+++ b/stdlib/string.ncl
@@ -76,22 +76,6 @@
       else
         %blame% (%label_with_message% "not a string" l),
 
-    EnumTag
-    | doc m%"
-      Contract to enforce the value is an enum tag.
-
-      For example:
-      ```nickel
-        (`foo | EnumTag) =>
-          `foo
-        (`FooBar | EnumTag) =>
-          `FooBar
-        ("tag" | EnumTag) =>
-          error
-      ```
-      "%
-    = contract.from_predicate builtin.is_enum,
-
     Stringable
     | doc m%"
       Contract to enforce the value is convertible to a string via
@@ -434,7 +418,7 @@
     = from,
 
     # from_enum | < | Dyn> -> String = fun tag => %to_str% tag,
-    from_enum | EnumTag -> String
+    from_enum | enum.Tag -> String
     | doc m%"
       Converts an enum variant to its string representation.
 
@@ -487,7 +471,7 @@
     = fun s => s == "true",
 
     # to_enum | String -> < | Dyn> = fun s => %enum_from_str% s,
-    to_enum | String -> EnumTag
+    to_enum | String -> enum.Tag
     | doc m%"
       Converts any string that represents an enum variant to that enum variant.
 


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/integration/pass/stdlib_string.ncl b/tests/integration/pass/stdlib_string.ncl
index d7b7cb52..c994178c 100644
--- a/tests/integration/pass/stdlib_string.ncl
+++ b/tests/integration/pass/stdlib_string.ncl
@@ -13,8 +13,8 @@ let {check, ..} = import "lib/assert.ncl" in
   ("9001" | string.NumLiteral) == "9001",
   # string.CharLiteral
   ("e" | string.Character) == "e",
-  # string.EnumTag
-  (`Foo | string.EnumTag) == `Foo,
+  # enum.Tag
+  (`Foo | enum.Tag) == `Foo,
   # string.Stringable
   (`Foo | string.Stringable) == `Foo,
   (true | string.Stringable) == true,
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