Repository: tweag/nickel
Pull request #621 (2022-02-23 14:22:19)

[Language Server] Remove debug info in hover overlays
Suppresses Debug info in hover cards.


Patch:
diff --git a/.github/workflows/deploy-preview.yml b/.github/workflows/deploy-preview.yml
index e1434aed..717bd1ec 100644
--- a/.github/workflows/deploy-preview.yml
+++ b/.github/workflows/deploy-preview.yml
@@ -6,6 +6,8 @@ jobs:
   deploy:
     uses: tweag/nickel-lang.org/.github/workflows/deploy.yml@master
     with:
+      nickel_repository: ${{ github.repository }}
+      nickel_ref: ${{ github.sha }}
       production_deploy: false
     secrets:
       CACHIX_AUTH_TOKEN: ${{ secrets.CACHIX_AUTH_TOKEN }}
diff --git a/.github/workflows/update-flake-lock.yml b/.github/workflows/update-flake-lock.yml
index 7febf69b..0e9eaa2e 100644
--- a/.github/workflows/update-flake-lock.yml
+++ b/.github/workflows/update-flake-lock.yml
@@ -16,4 +16,4 @@ jobs:
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
       - name: Update flake.lock
-        uses: DeterminateSystems/update-flake-lock@v8
+        uses: DeterminateSystems/update-flake-lock@v7
diff --git a/Cargo.lock b/Cargo.lock
index d73ac2f2..b7306dd3 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -128,9 +128,9 @@ dependencies = [
 
 [[package]]
 name = "beef"
-version = "0.5.1"
+version = "0.4.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bed554bd50246729a1ec158d08aa3235d1b69d94ad120ebe187e28894787e736"
+checksum = "474a626a67200bd107d44179bb3d4fc61891172d11696609264589be6a0e6a43"
 
 [[package]]
 name = "bit-set"
@@ -788,18 +788,18 @@ dependencies = [
 
 [[package]]
 name = "logos"
-version = "0.12.0"
+version = "0.11.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "427e2abca5be13136da9afdbf874e6b34ad9001dd70f2b103b083a85daa7b345"
+checksum = "b91c49573597a5d6c094f9031617bb1fed15c0db68c81e6546d313414ce107e4"
 dependencies = [
  "logos-derive",
 ]
 
 [[package]]
 name = "logos-derive"
-version = "0.12.0"
+version = "0.11.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "56a7d287fd2ac3f75b11f19a1c8a874a7d55744bd91f7a1b3e7cf87d4343c36d"
+checksum = "797b1f8a0571b331c1b47e7db245af3dc634838da7a92b3bef4e30376ae1c347"
 dependencies = [
  "beef",
  "fnv",
diff --git a/Cargo.toml b/Cargo.toml
index 973fd10f..8a3dc8b5 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -30,7 +30,7 @@ regex = "0.2.1"
 simple-counter = "0.1.0"
 codespan = "0.11"
 codespan-reporting = "0.11"
-logos = "0.12.0"
+logos = "0.11.4"
 serde = { version = "1.0.117", features = ["derive"] }
 serde_json = "1.0.59"
 serde_yaml = "0.8.15"
diff --git a/benches/lists.rs b/benches/lists.rs
index 9cc88013..c9054e87 100644
--- a/benches/lists.rs
+++ b/benches/lists.rs
@@ -218,21 +218,9 @@ fn pipe_deepseq(c: &mut Criterion) {
     );
 }
 
-fn sort_normal(c: &mut Criterion) {
-    bench(
-        "sort normal",
-        env!("CARGO_MANIFEST_DIR"),
-        "lists/sort",
-        None,
-        20,
-        EvalMode::Normal,
-        c,
-    );
-}
-
 criterion_group! {
     name = benches;
     config = Criterion::default().with_profiler(PProfProfiler::new(100, Output::Flamegraph(None)));
-    targets = fold_strings, fold_strings_deep, fold_nums, fold_nums_deep, fold_lists, fold_lists_deep, foldl_strings, foldl_strings_deep, foldl_nums, foldl_nums_deep, foldl_lists, foldl_lists_deep, generate_normal, generate_deepseq, map_normal, map_deepseq, pipe_normal, pipe_deepseq, sort_normal
+    targets = fold_strings, fold_strings_deep, fold_nums, fold_nums_deep, fold_lists, fold_lists_deep, foldl_strings, foldl_strings_deep, foldl_nums, foldl_nums_deep, foldl_lists, foldl_lists_deep, generate_normal, generate_deepseq, map_normal, map_deepseq, pipe_normal, pipe_deepseq
 }
 criterion_main!(benches);
diff --git a/benches/lists/sort.ncl b/benches/lists/sort.ncl
deleted file mode 100644
index 88f03cc6..00000000
--- a/benches/lists/sort.ncl
+++ /dev/null
@@ -1,5 +0,0 @@
-let nums = [3288, 2438, 1462, 437, 17, 1929, 2595, 2702, 831, 3685, 1906, 420, 2646, 1906, 2539, 184, 299, 3455, 2320, 1471, 1812, 3837, 1000, 2097, 945, 1973, 1090, 2285, 2272, 1045, 848, 3194, 2113, 537, 1953, 561, 2082, 2416, 3182, 3660, 3379, 1458, 39, 2720, 2469, 811, 837, 548, 3021, 2961, 2860, 2092, 942, 2511, 1769, 168, 130, 2755, 2552, 1057, 2619, 1848, 2373, 2012, 2339, 2521, 3593, 2784, 3094, 2260, 1994, 690, 828, 1298, 3434, 2929, 2188, 1285, 3783, 3635, 971, 3334, 87, 1578, 1363, 533, 3634, 1874, 830, 3976, 1140, 789, 1483, 1966, 1626, 3552, 2968, 3301, 749, 2576] in
-let ascending = fun x y => if x < y then `Less else if (x == y) then `Equal else `Greater in
-{
-    run = fun n => lists.sort ascending nums
-}
diff --git a/doc/manual/contracts.md b/doc/manual/contracts.md
deleted file mode 100644
index 6cd1da8a..00000000
--- a/doc/manual/contracts.md
+++ /dev/null
@@ -1,682 +0,0 @@
-# Contracts
-
-(For the motivation behind contracts and a high-level overview of contracts and
-types, first read the [correctness](./correctness.md) section.)
-
-To first approximation, contracts are assertions. They check that a value
-satisfies some property at run-time. If the test passes, the execution can go on
-normally. Otherwise, an error is raised. In Nickel, you can apply a contract
-using the `|` operator:
-
-```nickel
-let x = (1 + 1 | Num) in x
-```
-
-Contract can also be attached to identifiers in a definition:
-
-```nickel
-// let-binding: equivalent to the previous example
-let x | Num = 1 + 1 in x
-
-// on a record field
-{x | Num = 1 + 1}
-```
-
-Here, `x` is bound to a `Num` contract. When evaluating `x`, the following steps
-are performed:
-
-1. Evaluate `1 + 1`.
-2. Check that the result is a number.
-3. If it is, return the expression unchanged. Otherwise, raise an error.
-
-```
-$ nickel repl
-nickel>1 + 1 | Num
-2
-
-nickel>"a" | Num
-error: contract broken by a value.
-[..]
-```
-
-Contracts corresponding to the basic types `Num`, `Str`, `Bool` and `Dyn` are
-available. `Dyn` is a contract that never fails.
-
-## User-defined contracts
-
-### By hand
-
-Where run-time
-mechanisms like contracts really shine is in the ability to check for arbitrary
-properties. Let us see how to define our very own contract. We start the REPL
-(`nickel repl`) and input:
-
-```nickel
-let IsFoo = fun label value =>
-  if builtins.is_str value then
-    if value == "foo" then
-      value
-    else
-      contracts.blame_with "not equal to \"foo\"" label
-  else
-    contracts.blame_with "not a string" label
-```
-
-A custom contract is a function of two arguments:
-
-- A `label`. Provided by the interpreter, the label contains tracking information
-  for error reporting. Its main usage is to be passed to `contracts.blame` or
-  `contracts.blame_with` when the contract isn't satisfied.
-- The value being checked.
-
-Upon success, the contract must return the original value. We will see the reason why
-in the [laziness](#laziness) section. To signal failure, we use
-`contracts.blame` or its variant `contracts.blame_with` that takes an additional
-error message as a parameter. `blame` immediately aborts the execution and
-reports a contract violation error.
-
-In `IsFoo`, we first test if the value is a string, and then if it is equal to
-`"foo"`, in which case the contract succeeds. Otherwise, the contract fails with
-appropriate error messages. Let us try:
-
-```
-nickel>1 | IsFoo
-error: contract broken by a value [not a string].
-[..]
-
-nickel>"a" | IsFoo
-error: contract broken by a value [not equal to "foo"].
-[..]
-
-nickel>"foo" | IsFoo
-"foo"
-```
-
-### With `from_predicate`
-
-Our contract is simple: in the end, it tests the condition `value == "foo"`.
-Unfortunately, it has a few cascading ifs that don't look very nice. This is a
-necessary evil if you want to provide distinct error messages (`not a string`
-and `not a "foo"`). However, one could argue in this case that the information
-of the contract's name (which is automatically printed for contract violiation
-error, as well as various other data) is enough to understand the error. In this
-case, we can write our contract more succinctly as:
-
-```nickel
-let IsFoo = contracts.from_predicate ((==) "foo")
-```
-
-`contracts.from_predicate` takes a predicate (a function of one argument that
-returns a boolean) and converts it to a contract. The syntax `(==)` turns the
-equality operator `==` into a function, and is a shorthand for
-`fun x y => x == y`. The partial application to `(==) "foo"` is then the function
-`fun y => "foo" == y`, which is exactly the condition we want. `from_predicate`
-is useful to quickly define contracts based on a boolean condition, and when
-the contract is simple enough to not require custom error message.
-
-Here is an example of a port number contract:
-
-```nickel
-let Port = contracts.from_predicate (fun value =>
-  builtins.is_num value &&
-  nums.is_int value &&
-  value >= 0 &&
-  value <= 65535)
-```
-
-### Parametrized contracts
-
-Let us consider a contract for bound checking:
-
-```nickel
-let Between5And10 = contracts.from_predicate (fun value =>
-  builtins.is_num value &&
-  value >= 5 &&
-  value <= 10) in
-let MyConfig = {
-  level | Between5And10,
-}
-```
-
-Now, we add a new field to our schema, that must be between `0` and `1`:
-
-```nickel
-let Between5And10 = contracts.from_predicate (fun value =>
-  builtins.is_num value &&
-  value >= 5 &&
-  value <= 10) in
-let Between0And1 = contracts.from_predicate (fun value =>
-  builtins.is_num value &&
-  value >= 0 &&
-  value <= 1) in
-let MyConfig = {
-  level | Between5And10,
-  strength | Between0And1,
-}
-```
-
-`Between5And9` and `Between0And1` are awkwardly similar. Because custom
-contracts are nothing more than functions, we can use function arguments as
-parameters for contracts. Given how partial function application works,
-parameters must appear first, before the `label` and `value` arguments:
-
-```nickel
-let Between = fun min max =>
-  contracts.from_predicate (fun value =>
-    value >= min &&
-    value <= max) in
-// alternative without from_predicate
-let BetweenAlt = fun min max label value =>
-  if builtins.is_num value &&
-     value >= min &&
-     value <= max then
-    value
-  else
-    contracts.blame label in
-let MyConfig = {
-  level | Between 5 10,
-  strength | Between 0 1,
-}
-```
-
-### Contracts parametrized by contracts
-
-Contracts parametrized by other contracts are not really special among
-parametrized contracts, but note that although contracts can be functions, we
-will see soon that they can be different objects as well. Even with functions,
-contract application behaves slightly differently than bare function
-application. Thus, when manually handling a contract `contract`, do not apply it
-as a function `contract label value`, but use `contracts.apply`:
-`contracts.apply contract label value`. One example of such a contract is a
-`Nullable` contract, that accepts a value that is either null or of some other
-given format:
-
-```nickel
-let Nullable = fun contract label value =>
-  if value == null then
-    value 
-  else
-    contracts.apply contract label value in
-// succeeds
-null | Nullable Num
-// succeeds too
-1 | Nullable Num
-```
-
-## Compound contracts
-
-This section describes the different ways of composing existing contracts
-together to create new ones.
-
-### Records
-
-Record contracts are fundamental in a configuration language like Nickel. They
-encode the data schema of a configuration. A record contract is just a record
-literal with contract annotations and whose field definitions are usually
-missing:
-
-```nickel
-let MyConfig = {
-  path | Str,
- 
-  connection | {
-    server_port | Port,
-    host | Str,
-  }
-} in
-
-{
-  path = "/foo/bar",
-  connection = {
-    server_port =
-      if host == "localhost" then
-        8080
-      else
-        80,
-    host = "localhost",
-  }
-} | MyConfig
-```
-
-`MyConfig` is a schema describing a configuration with:
-
-- a field `path` that must be a string
-- a sub-record `connection`, which has a `server_port` and a `host` field that
-  are respectively a port number and a string.
-
-See how we've combined contracts: while defining the `MyConfig` record contract,
-we wrote another inline record contract for the `connection` field, and we
-reused the `Port` contract defined earlier. Composition is this ability of using
-existing contracts seamlessly as building blocks for new contracts.
-
-If we export this example to json, we get:
-
-```
-$ nickel -f config.ncl export
-error: contract broken by a value.
-   ┌─ :1:1
-   │
- 1 │ Port
-   │ ---- expected type
-   │
-   ┌─ .../config.ncl:22:9
-   │
-22 │         "8080"
-   │         ^^^^^^ applied to this expression
-   │
-   ┌─ <unknown> (generated by evaluation):1:1
-   │
- 1 │ "8080"
-   │ ------ evaluated to this value
-
-note:
-   ┌─ .../config.ncl:12:19
-   │
-12 │     server_port | Port,
-   │                   ^^^^ bound here
-```
-
-Indeed, our `server_port` is a string, while a number was expected. If we
-replace `"8080"` by `8080`, we finally obtain:
-
-```json
-{
-  "connection": {
-    "host": "localhost",
-    "server_port": 8080
-  },
-  "path": "/foo/bar"
-}
-```
-
-If for a specific use-case port numbers can actually also be specified as
-strings, you can amend the `Port` contract to be more liberal and accept strings
-representing valid port numbers.
-
-#### Metadata
-
-Additionally to defining the contracts of fields, record contract can also
-attach metadata (see [merging](./merging.md)) to fields, such as a documentation
-or default value:
-
-```
-nickel>let MyConfig = {
-    foo | doc "This documentation will propagate to the final value!"
-        | Str
-        | default = "foo",
-    bar | Num,
-}
-nickel>let config | MyConfig = {bar = 2}
-nickel> builtins.serialize `Json config
-"{
-  "bar": 2,
-  "foo": "foo"
-}"
-nickel>
-nickel>:query config.foo
-* contract: Str
-* default: "foo"
-* documentation: This documentation will propagate to the final value!
-```
-
-#### Open record contracts
-
-By default, record contracts are closed, meaning that additional fields are forbidden:
-
-```
-nickel>let Contract = {foo | Str}
-nickel>{foo = "a", bar = 1} | Contract
-error: contract broken by a value [extra field `bar`].
-[..]
-```
-
-If you want to allow additional fields, append `, ..` after the last field
-definition to define an open contract:
-
-```
-nickel>let Contract = {foo | Str, ..}
-nickel>{foo = "a", bar = 1} | Contract
-{ foo = <contract,value="a">, bar = 1}
-```
-
-#### Giving values for fields
-
-While most record contracts don't have field definitions, they can. In fact,
-records contracts are not special: any record literal can be used both as a
-contract or a normal value. If a field is defined both in the contract and the
-checked value, the two definitions will be merged in the final result. For
-example:
-
-```
-nickel>let Secure = {
-  must_be_very_secure | Bool = true,
-  data | Str,
-}
-nickel>builtins.serialize `Json ({data = ""} | Secure)
-"{
-  "data": "",
-  "must_be_very_secure": true
-}"
-
-nickel>{data = "", must_be_very_secure = false} | Secure
-error: Non mergeable terms
-  ┌─ repl-input-7:1:35
-  │
-1 │ {data = "", must_be_very_secure = false} | Secure
-  │                                   ^^^^^ cannot merge this expression
-  │
-  ┌─ repl-input-4:2:32
-  │
-2 │   must_be_very_secure | Bool = true,
-  │                                ^^^^ with this expression
-```
-
-**Warning: `=` vs `|`**
-
-It may be tempting to use `=` instead of  `|` to attach a record contract to a
-field. That is, writing `Contract = {foo = {bar | Str}}` instead of `Contract =
-{foo | {bar | Str}}`. When applying this contract, the merging operator will
-apply the `Str` contract to the field `foo` of the checked value. At first
-sight, `=` also fits the bill. However, there are a number of subtle but
-potentially surprising differences.
-
-One concerns open contracts. Merging never requires the presence of specific
-fields: thus, the contract `{bar | Str}` attached to `foo` will actually behave
-as an open contract, even if you didn't use `..`. This is usually not what you
-want:
-
-```
-nickel>let ContractPipe = {
-  sub_field | {foo | Str}
-}
-nickel>let ContractEq = {
-  sub_field = {foo | Str}
-}
-nickel>{sub_field.foo = "a", sub_field.bar = "b"} | ContractPipe
-error: contract broken by a value [extra field `bar`].
-[..]
-
-nickel>{sub_field.foo = "a", sub_field.bar = "b"} | ContractEq
-{ sub_field = { foo = <contract,value="a">, bar = "b"}}
-```
-
-There are other discrepancies, e.g. when applying the contract to a record with
-a `default` annotation on `subfield`. Thus, unless you have a specific use-case
-in mind, **you should use `|` instead of `=` when attaching record contracts**.
-
-### Types constructors for contracts
-
-We've already seen that the primitive types `Num`, `Str` and `Bool` can be used
-as contracts. In fact, any type constructor of the
-[static type system](./typing.md) can be used to combine contracts.
-
-#### List
-
-A list contract checks that the value is a list and applies the parameter
-contract to each element:
-
-```
-nickel>let VeryBig = contracts.from_predicate (fun value =>
-  builtins.is_num value
-  && value >= 1000)
-nickel>[1000, 10001, 2] | List VeryBig
-error: contract broken by a value.
-  ┌─ :1:7
-  │
-1 │ List (VeryBig)
-  │       ------- expected list element type
-  │
-  ┌─ repl-input-14:1:15
-  │
-1 │ [1000, 10001, 2] | List VeryBig
-  │               - evaluated to this expression
-[..]
-```
-
-Recall that `List` is an alias for `List Dyn`, thus the `List` contracts only
-checks that the value is a list.
-
-#### Functions
-
-A function contract `In -> Out` returns a wrapped function which, for each call,
-will additionally check the parameter against the `In` contract and the return
-value against the `Out` contract. Put differently, `In` represents
-*pre-conditions* that must hold about the parameter, and `Out` *post-conditions*
-that must hold about the return value of the function.
-
-##### Caller vs callee
-
-Function contracts, as opposed to a contract like `Num`, have the peculiarity of
-involving two parties in the contract checking. For example:
-
-```
-let add_semi | Str -> Str = fun x => x ++ ";" in
-add_semi 1
-
-let wrong | Str -> Str = fun x => 0 in
-wrong "a"
-```
-
-Both of those examples will fail with a contract violation. But they are
-different in nature: in the first one, the function `add_semi` respects its
-contract. Whenever `x` is a string, `add_semi` does return a string. Here, the
-**caller** (the user of the function) is to blame, and not the **callee** (the
-function). This is an important distinction. Say you wrote `add_semi` as a part
-of a library. A wrong call is a random user, somewhere, making a programming
-mistake. This is not your direct responsibility, assuming the contract error
-messages are good enough to let users understand the issue immediately.
-
-The second example is reversed. The caller provides a string, as requested by
-the contract, but the function returns a number. The blame is on the **callee**.
-If you are the library writer who shipped the `wrong` function, this means you
-have a bug that you need to fix.
-
-The interpreter automatically performs book-keeping for functions contracts in
-order to make this caller/callee distinction:
-
-```
-nickel>let add_semi | Str -> Str = fun x => x ++ ";" in
-add_semi 1
-error: contract broken by the caller.
-[..]
-
-nickel>let wrong | Str -> Str = fun x => 0 in
-wrong "a"
-error: contract broken by a function.
-[..]
-```
-
-##### Higher-order functions
-
-The beauty of function contracts is that they gracefully scale to higher-order
-functions as well. Higher-order functions are functions that take other
-functions as parameters. Here is an example:
-
-```
-nickel>let apply_fun | (Num -> Num) -> Num = fun f => f 0 in
-apply_fun (fun x => "a")
-error: contract broken by the caller.
-  ┌─ :1:9
-  │
-1 │ (Num -> Num) -> Num
-  │         --- expected return type of a function provided by the caller
-  │
-  ┌─ repl-input-17:2:21
-  │
-2 │ apply_fun (fun x => "a")
-  │                     --- evaluated to this expression
-[..]
-```
-
-#### Dictionary
-
-The type constructor `{_ : Contract}` represents a record whose field names are not
-constrained but whose field values are checked against `Contract`. In practice, the
-contract `Contract` is mapped onto each field. Such a contract is useful when using
-records as an extensible dictionary, that is a key/value store, where keys are
-strings and values respect `Contract`. Example:
-
-```nickel
-let occurrences | {_: Num} = {a = 2, b = 3, "!" = 5, "^" = 1} in
-occurrences."!"
-```
-
-## Laziness
-
-In the [writing a custom contract by hand](#by-hand) section, we noted the
-strange fact that a custom contract must return a value, instead of just
-returning e.g. a boolean to indicate success or failure. A contract could even
-simply return `null`, as failure is handled separately by aborting. Moreover, the
-contracts we have written so far always returned the original unmodified
-value upon success, which doesn't sound very useful: after all, the caller and
-the interpreter already had access to this value to begin with.
-
-The motivation for this return value relates to laziness. Nickel is designed to
-be *lazy*, meaning that values are evaluated on-demand, only when they are
-needed. For example, record fields are not evaluated until they are accessed,
-printed (in the REPL or as a result of `nickel`), or until the whole record is
-serialized/exported. Thanks to laziness, you can for example query specific
-information on a large configuration without having to actually evaluate
-everything. We will use a dummy failing expression `1 + "a"` to observe where
-evaluation takes place:
-
-```
-nickel>let config = {fail = 1 + "a", data | doc "Some information" = 42}
-nickel>:query config.data
-* value: 42
-* documentation: Some information
-
-nickel>config.fail
-error: type error
-[..]
-```
-
-See how the command `:query config.data` succeeds, although the field `fail`
-causes an error when evaluated.
-
-A large configuration will most probably have a root contract attached,
-corresponding to its schema. If this contract checked everything eagerly,
-forcing the evaluation of the most part of the configuration, we would lose the
-benefits of laziness. Thus, *we want contracts to be lazy as well*. In
-particular, a subcontract attached to a field should only fire when the field is
-requested. This is the case with record contracts, and in general all native
-contracts combinators are lazy too.
-
-### Writing lazy contracts
-
-Imagine we want to write a contract similar to `{_ : Bool}`, that is a
-dictionary of booleans, but we also want keys to be number literals (although
-represented as strings). A valid value could look like `{"1": true, "2": false,
-"10": true}`. If we used boolean predicates as the default for contracts, it
-would be impossible to make it lazy: as soon as your contract is called, you
-would need to produce a `true` or `false` answer, and checking that fields are
-all `Bool` would force their evaluation.
-
-What we can do is to not perform all the checks right away, but **return a new
-value, which is wrapping the original value with delayed checks inside**. This
-is the rationale behind contracts returning a value. Let us see:
-
-```
-let NumBoolDict = fun label value =>
-  if builtins.is_record value then
-    let check_fields = value
-      |> records.fields
-      |> lists.foldl (fun acc field_name =>
-        if strings.is_match "^\\d+$" field_name then
-          acc // unused and always null through iteration
-        else
-          contracts.blame_with "field name `#{field_name}` is not a number" label
-        ) null in
-
-    value
-      |> records.map (fun name value =>
-        let label_with_msg =
-            contracts.tag "field `#{name}` is not a boolean" label in
-        contracts.apply Bool label_with_msg value)
-      |> builtins.seq check_fields
-  else
-    contracts.blame_with "not a record" label
-```
-
-There is a lot to unwrap here. Please refer to the [syntax](./syntax.md) section
-if you have trouble parsing the example. We first check that the value is a
-record on line 2. We then define `check_fields` one line 3, an expression that
-goes over the record field names and check that each one is a sequence of
-digits. We use a left fold with a dummy `null` accumulator as a way to just
-iterate through the list without building up anything interesting.
-
-For laziness, the interesting bit happens here:
-
-```
-value
-  |> records.map (fun _name value =>
-    contracts.apply Bool label value)
-  |> builtins.seq check_fields
-```
-
-This is the final return value of the contract (at least when `value` is a
-record). This code takes the original record, and maps a function which
-substitutes each fields for the same value but wrapped in a `Bool` contract on
-it. Because records are lazy, *this doesn't actually execute the `Bool`
-contracts right away*. They will be run only when the corresponding field will
-be requested.
-
-Finally, we sequence the result with `check_fields`: if we remove this last line
-and return the mapped value directly, because Nickel is lazy and `check_fields`
-is not used elsewhere, the check wouldn't actually trigger. Using `seq` first
-forces the evaluation of `check_fields` unconditionally, ignores the resulting
-value and continues with the second argument (here, our wrapped `value`).
-
-Let us see if we indeed preserved laziness:
-
-```
-nickel>let config | NumBoolDict = {
-    "1" = 1 + "a", // Same as our previous "fail"
-    "0" | doc "Some information" = true,
-}
-nickel>:query config."0"
-* value: true
-* documentation: Some information
-```
-
-Yes! Our contract doesn't unduly cause the evaluation of the field `"1"`. Does
-it check anything, though?
-
-```
-nickel>let config | NumBoolDict = {
-  not_a_number = false,
-  "0" | doc "Some information" = false,
-}
-nickel>:q config."0"
-error: contract broken by a value [field name `not_a_number` is not a number].
-[..]
-
-nickel>let config | NumBoolDict = {
-  "0" | doc "Some information" = "not a boolean",
-}
-nickel>:q config."0"
-error: contract broken by a value [field `0` is not a boolean].
-[..]
-```
-
-It does!
-
-#### Remark: lazy, always?
-
-Note that our check for field names is not lazy in the sense that even when
-requesting another field `"0"`, we've already triggered this check for all field
-names. This is totally fine: early error reporting is a good thing, as long we
-don't force the evaluation of something that wouldn't be evaluated without the
-contract. The field names of a record are readily available and don't incur any
-evaluation, so we can check for them directly. We could also have put this check
-inside each field, along the `Bool` contract application, making it lazy. But we
-prefer to report this error as soon as possible.
-
-#### Conclusion
-
-Our `NumToBool` contract doesn't perform all the checks needed right away.
-Instead, **it returns a new value, which is wrapping the original value with
-delayed checks inside**. Doing so preserves laziness of the language and only
-triggers the checks when the values are used or exported in a configuration.
-This is the reason for contracts to return a value, which must be the original
-value with potential delayed checks inside.
diff --git a/doc/manual/correctness.md b/doc/manual/correctness.md
deleted file mode 100644
index 3cb0c449..00000000
--- a/doc/manual/correctness.md
+++ /dev/null
@@ -1,359 +0,0 @@
-# Correctness
-
-One of the main value proposition of Nickel is to make configurations
-programmable. However, a not less important one is to help you write *correct*
-configurations. Our definition of correctness is not restricted to but includes
-the following properties:
-
-1. The evaluation doesn't end up on non-sensical expressions. For example, when
-   trying to add a number to a string, or to call to a value which is not a
-   function.
-2. The generated configuration is valid. Your program may be correct with
-   respect to the previous point while outputing a field `prto = "80"` instead
-   of `port = 80`. The consumer of the configuration will probably fail.
-   Typically, validity involves respecting a data schema.
-
-Because Nickel an interpreted language, there is no well-defined *ahead-of-time*
-phase that can prevent a class of errors once and for all[^1]. In practice, you
-will often still get an error at the point you are trying to run a program.
-However, what the language can do is to vastly improve the troubleshooting
-experience by providing:
-
-1. An ergonomic way to express properties to check code and data against.
-2. Mechanisms to catch violation as early as possible (e.g. before the code
-   path is triggered).
-3. Informative error messages.
-
-## Solutions
-
-One standard device for correctness is static typing. The static typing
-discipline brings in important benefits for large codebases of common
-applications. But the case of an interpreted configuration language appears less
-clear-cut.
-
-For pure configuration code, which is mostly data, static typing is not as
-useful. First, a configuration is a terminating program run once on fixed
-inputs: here, basic type errors will show up at runtime anyway. Second, for data
-validation, static types are too rigid. Statically checking that an expression
-will always evaluate to a valid port number, for example, requires very advanced
-machinery. On the other hand, checking this property at runtime on the final
-result is trivial.
-
-Nevertheless, if you have ever faced puzzling [dynamic type
-errors](https://www.haskellforall.com/2021/01/dynamic-type-errors-lack-relevance.html),
-you may feel the need for something better. Bare dynamic typing is prone to
-irrelevant error messages, pointing to a location far from the problematic code
-in the source. This is especially true when working with functions, which may be
-called with incorrect values and pass them around until they eventually break
-evaluation in a distant and seemingly unrelated location. For reusable code,
-that is functions, static typing really helps.
-
-## Types and contracts
-
-This apparent dilemma is solved in Nickel by the combination of *gradual typing*
-and *contracts*. Gradual typing is a typing discipline where you can use both
-static typing and dynamic typing, at will. Contracts augment the dynamic typing
-part by providing a principled and ergonomic way to enforce arbitrary assertions
-at run-time.
-
-In essence, the purpose of types and contracts is the same: to ensure that an
-expression verifies some desired properties. And when it doesn't, the
-interpreter must fail with an informative error message. There is a wide range
-of properties that can be checked for, such as:
-
-- To evaluate to a number.
-- To evaluate to the same value as this other field `foo` of the same configuration.
-- To evaluate to a record with at least one field `port` that is a valid port number.
-- To be a function always mapping numbers to numbers.
-- etc.
-
-Both types and contracts are enforced in a similar way, using an annotation:
-
-```
-$ nickel repl
-nickel> 1 + 1.5 : Num
-2.5
-
-nickel> let f : Num -> Num = fun x => x + 1
-nickel> f 0
-1
-
-nickel> let GreaterThan = fun bound =>
-  contracts.from_predicate (fun val => val >= bound) in
--1 | GreaterThan 10
-
-error: contract broken by value
-[..]
-```
-
-`:` introduces a type annotation, while `|` introduces a contract annotation.
-They support the same syntax for properties on the right-hand side.
-
-**The fundamental difference between types and contracts is that type
-annotations are checked statically, before the program even starts, while
-contracts are checked lazily, at run-time**. The characteristics and use-cases of
-types and contracts directly follow from this distinction.
-
-In the next paragraphs, we consider two typical examples to illustrate the
-difference between types and contracts in practice.
-
-### Case 1: a function operating on lists
-
-Say we need a function to convert a list of key-value pairs to a list of keys
-and a list of values. Let's call it `split`:
-
-```
-nickel> split [{key = "foo", value = 1}, {key = "bar", value = 2}]
-{keys = ["foo", "bar"], values = [1, 2]}
-
-nickel> split [
-  {key = "firewall", value = true},
-  {key = "grsec", value = false},
-  {key = "iptables", value = true},
-]
-{ keys: ["firewall", "grsec", "iptables"], values [true, false, true] }
-```
-
-Here is the definition for `split`, but with a twist. We mistakenly forgot to
-wrap `pair.key` as a list before concatenating at line 6:
-
-```nickel
-// lib.ncl
-{
-  split = fun pairs =>
-    lists.fold (fun pair acc =>
-      {
-        // problem: the right expression to use is [pair.key]
-        keys = acc.keys @ pair.key,
-        values = acc.values @ [pair.value],
-      })
-      {keys = [], values = []}
-      pairs
-}
-```
-
-And we call to split from our configuration:
-
-```nickel
-// config.ncl
-let {split} = import "lib.ncl" in
-split [{key = "foo", value = 1}, {key = "bar", value = 2}]
-```
-
-We want to ensure that the callers to `split` pass a list
-verifying:
- - elements are records with a `key` field and a `value` field
- - keys are strings
- - values can be anything, but must all have the same type
-
-We also want to make sure our implementation correctly returns a value which is
-a record with a field `keys` that is a list of strings, and a field `values`
-that is a list of elements of the same type as the input values.
-
-An idiomatic way to express these properties in Nickel is to use the annotation
-
-```nickel
-forall a. List {key: Str, value: a}
-          -> {keys: List Str, values: List a}
-```
-
-The `forall` parts says that the type of values `a` can be anything, but it has
-to be the same `a` in the input and in the output. We'll now see the difference
-between enforcing this specification using a type annotation or a contract
-annotation.
-
-#### Using a contract annotation
-
-A contract performs checks at run-time. At this stage, a function is mostly an
-opaque, inert value, waiting for an argument to hand back a result. In
-consequence, a function contract is doomed to fire only when `split` is applied
-to an argument, in which case the contract checks that:
-
-1. The argument satisfies the `List {key: Str, value: a}` contract.
-2. The return value satisfies the `{keys: List Str, values: List a}` contract.
-
-Those checks produce useful error message when the caller passes arguments of
-the wrong type, or the function returns a value of the wrong type. But the
-function contract for `split` has the following limitations:
-
-- It only checks the values arising in concrete calls. In particular, if `split`
-  is not called by some program yet (e.g. written as part of a library), no check
-  takes place at all. If a particular code path is not triggered, it won't be
-  checked. **Here, evaluating or typechecking `lib.ncl` won't raise any error**.
-- Only the input value and the return value are checked. If `split` mishandles
-  an intermediate internal value not subject to another contract, we're
-  potentially back into unhelpful dynamic type errors. Evaluating `config.ncl`
-  indeed reports the following error:
-
-        error: Type error
-        ┌─ repl-input-12:6:27
-        │
-      6 │         keys = acc.keys @ pair.key,
-        │                           ^^^^^^^^ This expression has type Str, but List was expected
-        │
-        ┌─ repl-input-13:1:45
-        │
-      1 │ lib.split [{key = "foo", value = 1}, {key = "bar", value = 2}]
-        │                                             ----- evaluated to this
-        │
-        = @, 2nd operand
-
-  This error is not very helpful to the caller. It points to inside the
-  implementation of `split`, and to the `key = "bar"` part of the argument,
-  which respects the contract.
-
-#### Using a type annotation
-
-`split` is a generic function operating on builin types. This is a good
-candidate for static typing, which will help:
-
-- Ensure the property holds for all possible values of the parameter.
-- Check all the expressions inside `split` as well.
-- Report errors before execution takes place.
-
-Even if the call site is not statically typed, a type annotation also gives rise
-to a contract (see the [typing section][./typing.md] for more details). Thus,
-any issue with the arguments passed or the return value will be caught and
-correctly reported.
-
-What's more, intermediate values are also typechecked. Evaluating or just
-typechecking `lib.ncl` already reports an error:
-
-```
-error: Incompatible rows declaration
-  ┌─ repl-input-14:9:7
-  │
-9 │       pairs
-  │       ^^^^^ this expression
-[..]
-error: While typing field `key`: Incompatible types
- = The type of the expression was expected to be `List Str`
- = The type of the expression was inferred to be `Str`
- = These types are not compatible
-```
-
-The errors says that the `key` field of the elements of `pairs` is a string, but
-given the call to `fold`, it was expected to be lists of strings.
-
-#### Function contracts
-
-From this example, it seems typing is superior in pretty much every respect for
-functions. Typechecking is indeed more exhaustive, and generally reports errors
-earlier. In return, typechecking is rigid (it can reject valid programs) and
-limited in the properties it can handle. Properties outside the range of being a
-list, a record or a function with other builtin types inside, such as checking
-that a function returning a positive number, are out of the scope of
-typechecking (see case 2 below for another example). In such cases, where
-typechecking is not an option, a function contract can be helpful.
-
-### Case 2: a custom property
-
-The previous example used builtin types: functions, records, lists, and strings.
-To validate a configuration, you may want to check more elaborate properties.
-You can do so by writing your own custom properties, referred to as custom
-contract from now on:
-
-```nickel
-let OptLevel = contracts.from_predicate (fun value =>
-    lists.elem value ["O0", "O1", "O2", "O3"]) in
-{
-  opt_level = "O2",
-}
-```
-
-`OptLevel` checks that its argument is a valid optimization level, that is
-either `"O0"`, `"O1"`, `"O2"` or `"O3"`. You can ignore the details of the
-implementation of `OptLevel` for now. Writing custom contracts is more
-extensively covered in the [contracts section](./contracts.md). As for the
-previous example, let's see the difference between using a type annotation and a
-contract annotation.
-
-#### Using a type annotation
-
-If we write:
-
-```nickel
-let level = 1 in
-{
-  opt_level : OptLevel = "0" ++ srings.from_num level,
-}
-```
-
-We get:
-
-```
-error: incompatible types
-  ┌─ repl-input-3:3:27
-  │
-3 │   opt_level : OptLevel = "0" ++ (if level == 1 then "1" else "2"),
-  │                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ this expression
-  │
-  = The type of the expression was expected to be `OptLevel`
-  = The type of the expression was inferred to be `Str`
-  = These types are not compatible
-```
-
-Because `OptLevel` is a custom predicate, the typechecker can't prove that `"0"`
-concatenated with `strings.from_num 1"` is a valid optimization level. For that
-matter, even `"01" : OptLevel` doesn't typecheck. It's possible to build values
-that are accepted to be of type `OptLevel`, but it's very restricted and they
-can't really be used in a meaningful way inside typed code, beside being passed
-around.
-
-#### Using a contract annotation
-
-For such custom properties, a contract is the way to go:
-
-```nickel
-let level = 4 in
-{
-  opt_level | #OptLevel = "0" ++ strings.from_num level,
-}
-```
-
-This correctly reports an error, and even gives the computed offending value:
-
-```
-error: contract broken by a value.
-  ┌─ :1:1
-  │
-1 │ OptLevel
-  │ -------- expected type
-  │
-  ┌─ repl-input-4:3:27
-  │
-3 │   opt_level | OptLevel = "0" ++ strings.from_num level,
-  │                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ applied to this expression
-  │
-  ┌─ <unknown> (generated by evaluation):1:1
-  │
-1 │ "04"
-  │ ---- evaluated to this value
-```
-
-### Summary
-
-Types and contracts are the two mechanisms to enforce correctness of Nickel
-programs. Typechecking is a static and ahead-of-time mechanism, which is
-exhaustive and reports errors early, but is rigid and limited in the properties
-that can be checked. Contract checking is a run-time mechanism, making contracts
-more flexible and able to enforce arbitrary user-defined properties, but may
-reports less errors than typechecking, and report them later.
-
-As a rule of thumb, you should usually use types for functions operating on
-fairly generic data. Contracts are most adapted for data (records and lists),
-especially data that ends up in the final configuration. To enforce custom
-properties that are out of the scope of builtin types, you should use contracts,
-either for functions or data.
-
-You'll find a in-depth description of the type system and how to use it in the
-[typing section](./typing.md). For contracts, refer to the
-[contract section](./contracts.md). Finally, if you are looking for a quick
-cheat-sheet about when to use static typing or contracts, go to
-[Type versus contracts: when to?](./types-vs-contracts.md).
-
-[^1]: This statement is to be nuanced. Using the Nickel LSP server in your
-  editor, for example, does perform checks ahead of time, while you are typing
-  program. You can also perform typechecking separately before distributing a
-  configuration using `nickel typecheck`. However, a source program is not
-  guaranteed to have been checked in any way before execution.
diff --git a/doc/manual/syntax.md b/doc/manual/syntax.md
deleted file mode 100644
index 54d4a5c0..00000000
--- a/doc/manual/syntax.md
+++ /dev/null
@@ -1,446 +0,0 @@
-# Nickel Syntax
-
-## Simple values
-
-There are three basic kind of values in Nickel : 
- 1. numeric values, 
- 2. boolean values,
- 3. strings.
- 
-### Numeric values
-
-Nickel has a support for numbers, positive and negative, with or without decimals.
-Internally, those numbers are stored as 64-bits floating point numbers, following the IEEE 754 standard.
-
-Examples:
-
-```
-1
-0.543
-42
--1000000
--6.8
-```
-
-There are a some predefined operators for working with numbers :
-| Operator | Description                                          | Example       |
-|:--------:|:----------------------------------------------------:|:-------------:|
-| +        | The addition operator                                | `1 + 2 = 3`   |
-| \-       | The subtraction operator                             | `1 - 2 = -1`  |
-| *        | The multiplication operator                          | `1 * 2 = 2`   |
-| /        | The division operator                                | `1 / 2 = 0.5` |
-| %        | The modulo operator (returns the *signed* remainder) | `5 % 3 = 2`   |
-
-> **Remark about the `-` operator:**  
-> Since `-` can be used inside an identifier, the subtraction operators **needs** to be surrounded by spaces:
-> write `1 - 1`, not `1-1`.
-
-Numbers can be compared using the following operators :
-| Operator | Description      | Example   |
-|:--------:|:----------------:|:---------:|
-| ==       | Equal            | `5 == 5`  |
-| !=       | Not Equal        | `5 != 4`  |
-| <        | Smaller than     | `2 < 3`   |
-| >        | Greater than     | `1 > -5`  |
-| >=       | Greater or Equal | `1 >= 1`  |
-| <=       | Smaller or Equal | `-1 <= 6` |
-
-In the table below, you will find the operators sorted from highest to lowest precedence:
-|       Operators      | Associativity | Remark                                        |
-|:--------------------:|:-------------:|-----------------------------------------------|
-|       `( ... )`      |               | parentheses always have the highest precedence |
-|          `-`         |               | unary negation (as in `-1`)                   |
-|     `*`, `/`, `%`    | left-to-right |                                               |
-|       `+`, `-`       | left-to-right | binary addition and subtraction               |
-| `<`, `>`, `=<`, `>=` | left-to-right |                                               |
-|      `==`, `!=`      | left-to-right |                                               |
-
-### Boolean values
-
-The boolean values in Nickel are denoted `true` and `false`.
-
-Nickel features the classical boolean operators *AND* (&&), *OR* (||) and *NOT* (!).
-The _AND_ and _OR_ operators are lazy in the evaluation of the second argument: for example, in `exp1 && exp2`, `exp2` is only evaluated if `exp1` evaluates to `false`.
-
-Examples:
-```
-> true && false
-false
-
-> false || true
-true
-
-> ! true
-false
-```
-
-### Strings
-
-Nickel can work with sequences of characters, or strings. 
-Strings are enclosed by `" ... "` for a single line string or by `m#" ... "#m` for a multiline string.
-They can be concatenated with the operator `++`.
-Strings must be UTF-8 valid.
-
-The string interpolation syntax is `"#{ < expression that evaluates to a string > }"`.
-
-Examples:
-```
-> "Hello, World!"
-"Hello, World!"
-
-> m#"Well, if this isn't a multiline string?
-Yes it is, indeed it is"#m
-"Well, if this isn't a string?
-Yes it is, indeed it is"
-
-> "Hello" ++ "World"
-"HelloWorld"
-
-> let h = "Hello" in "#{h} World"
-"Hello World"
-
-> let n = 5 in "The number #{n}."
-error: Type error
-
-> let n = 5 in "The number #{strings.from_num n}."
-"The number 5."
-```
-
-Multiline strings are useful to write indented lines. The indentation is stripped from the beginning of the first line, and first and last lines are ignored if they are empty or contain only spaces.
-
-Example:
-```
-> m#"
-This line has no identation.
-  This line is indented.
-    This line is even more indented.
-This line has no more identation.
-"#m
-"This line has no indentation.
-  This line is indented.
-    This line is even more indented.
-This line has no more indentation." 
-```
-
-The only special sequence in a multiline string is the string interpolation.
-
-Examples:
-```
-> m#"Multiline\nString?"#m
-"Multiline\nString?"
-
-> m#"Multiline#{"\n"}String"#m
-"Multiline
-String"
-```
-
-A multiline string can be introduced and closed by multiple `#` signs, as long as this amount is equal. If you want to use string interpolation, you must use the same amount of `#` as in the delimiters.
-
-Examples:
-```
-> m##"Hello World"##m
-"Hello World"
-
-> m#####"Hello World"#####m
-"Hello World"
-
-> let w = "World" in m##"Hello #{w}"##m
-"Hello #{w}"
-
-> let w = "World" in m##"Hello ##{w}"##m
-"Hello World"
-```
-
-Multiline strings are "indentation-aware". This means that one could use an indented string interpolation and the indentation would behave as expected:
-```
-> let log = m#"
-if log:
-  print("log:", s)
-"#m in m#"
-def concat(str_list, log=false):
-  res = []
-  for s in str_list:
-    #{log}
-    res.append(s)
-  return res
-"#m
-"def concat(str_list, log=false):
-  res = []
-  for s in str_list:
-    if log:
-      print("log:", s)
-    res.append(s)
-  return res"
-```
-
-## Equality
-
-Operators `==` and `!=` are used to compare values. Two values of different types are never equal: that is, `==` doesn't perform implicit conversions.
-
-Examples:
-```
-> 1 == 1
-true
-
-> 5 == 5.0
-true
-
-> "Hello" == "Hello"
-true
-
-> "Hello" != "World"
-true
-
-> 5 == "Hello"
-false
-
-> true == "true"
-false
-```
-
-
-## Composite values
-
-### List
-A list is a sequence of values. They are delimited by `[` and `]`, and elements are separated with `,`.
-
-Examples:
-```
-[1, 2, 3]
-["Hello", "World"]
-[1, true, "true"]
-[]
-```
-
-Lists can be concatenated with the operator `@`:
-```
-> [1] @ [2, 3]
-[ 1, 2, 3 ]
-```
-
-### Record
-Records are key-value storage, or in Nickel terms, field-value storage. They are delimited by `{` and `}`, and elements are separated with `,`.
-Field-value elements are noted as `field = value`.
-The fields are strings, but can be written without quotes `"` if they respect identifiers syntax. Values can be of any type.
-Elements inside a record are unordered.
-Two records can be _merged_ together using the operator `&`. The reader can find more information about merging in the relevant documentation.
-
-Examples:
-```
-{}
-{a = 3}
-{my_id_n5 = "my id number 5", "my id n4" = "my id number 4" }
-{"5" = 5, six = 6}
-```
-
-Accessing a record field can be done using the `.` operator :
-```
-> { a = 1, b = 5 }.a
-1
-
-> { a = 1 }.b
-error: Missing field
-
-> { "1" = "one" }."1"
-"one"
-```
-
-It is possible to write records of records via the *piecewise syntax*, where we separate fields by dots:
-```
-> { a = { b = 1 } }
-{ a = { b = 1 } }
- 
-> { a.b = 1 }
-{ a = { b = 1 } }
-
-> { a.b = 1, a.c = 2, b = 3}
-{ a = { b = 1, c = 2 }, b = 3 }
-```
-
-When fields are enclosed with double quotes (`"`), you can use string interpolation to create or access fields:
-```
-> let k = "a" in { "#{k}" = 1 }
-{ a = 1 }
-
-> let k = "a" in { a = 1 }."#{k}"
-1
-```
-
-## Constructs
-
-### If-Then-Else
-This construct allows conditional branching in your code. You can use it as `if <bool expr> then <expr> else <expr>`.
-
-Examples:
-```
-> if true then "TRUE :)" else "false :("
-"TRUE :)"
-
-> if false then "Not this one" else "This one"
-"This one"
-
-> if "forty-two" == 42 then "equal?" else "unequal"
-"unequal"
-
-> ["1"] @ (if 42 == "42" then ["3"] else ["2"]) @ ["3"]
-["1", "2", "3"]
-```
-
-### Let-In
-Let-in allows the binding of an expression. It is used as `let <ident> = <expr> in <expr>`.
-
-Examples:
-```
-> let r = { a = "a", b = "b" } in r.a
-"a"
-
-> let inner = { inside = true } in let outer = { outside = inner.inside } in outer.outside
-true
-
-> let a = 1 in let b = 2 in a + b
-3
-```
-
-## Functions
-A function is declared using the `fun` keyword, then arguments separated with spaces, and finally an arrow `=>` to add the body of the function.
-To call a function, just add the arguments after it separated with spaces.
-Functions in Nickel are curried, meaning that a function taking multiple arguments is actually a function that takes a single argument and returns a function taking the rest of the arguments, until it is applied.
-
-Examples:
-```
-> (fun a b => a + b) 1 2
-3
-
-let add = fun a b => a + b in add 1 2
-3
-
-> let add = fun a b => a + b in
-    let add1 = add 1 in
-        add1 2
-3
-```
-
-All existing infix operators in Nickel can be turned into functions by putting them inside parentheses.
-
-Examples:
-```
-> 1 + 2
-3
-
-> (+) 1 2
-3
-
-> let increment = fun n => (+) 1 n in
-    increment 41
-42
-
-> let increment = (+) 1 in
-    increment 41
-42
-
-> let flatten = lists.fold (@) [] in flatten [[1, 2], [3], [4, 5]]
-[ 1, 2, 3, 4, 5 ]
-```
-
-Functions might be composed using the *pipe operator*. The pipe operator allows for a function application `f x` to be written as `x |> f`.
-This operator is left-associative, so `x |> f |> g` will be interpreted as `g (f x)`.
-
-Examples:
-```
-> "Hello World" |> strings.split " "
-["Hello", "World"]
-
-> "Hello World"
-  |> strings.split " "
-  |> lists.head
-"Hello"
-
-> "Hello World"
-  |> strings.split " "
-  |> lists.head
-  |> strings.uppercase
-"HELLO"
-```
-
-## Typing
-To give a type to a value, we write it with `< value > : < type >`.
-More information on typing in the relevant document.
-
-Examples:
-```
-5 : Num
-"Hello" : Str
-
-(fun a b => a + b) : Num -> Num -> Num
-let add : Num -> Num -> Num = fun a b => a + b
-
-{a: Num = 1, b: Bool = true, c : List Num = [ 1 ]}
-let r : {a : Num, b : Bool, c : List Num} = { a = 1, b = true, c = [ 1 ] }
-
-{ a = 1, b = 2 } : { _ : Num }
-let r : { _ : Num } = { a = 1, b = 2 }
-```
-
-## Metadata
-Metadata are used to attach contracts (more information in relevant documentation), documentation or priority to values.
-A metadata is introduced with the syntax `<value> | <metadata>`. Multiple metadata can be chained.
-
-
-Examples:
-```
-> 5 | Num
-5
-
-> 5 | Bool
-error: Blame error: contract broken by a value.
-
-> let SmallNum = contracts.from_predicate (fun x => x < 5) in
-1 | #SmallNum
-1
-
-> let SmallNum = contracts.from_predicate (fun x => x < 5) in
-10 | #SmallNum
-error: Blame error: contract broken by a value.
-
-> let SmallNum = contracts.from_predicate (fun x => x < 5) in
-  let NotTooSmallNum = contracts.from_predicate (fun x => x >= 2) in
-  3 | Num
-    | #SmallNum
-    | #NotTooSmallNum
-3
-```
-
-Adding documentation can be done with `| doc < string >`.  
-Examples:
-```
-> 5 | doc "The number five"
-5
-
-> true | Bool | doc m#"
-    If something is true,
-    it is based on facts rather than being invented or imagined,
-    and is accurate and reliable.
-    (Collins dictionary)
-    "#m
-true
-```
-
-Record contracts can set default values using the `default` metadata:
-It is noted as `| default = < default value >`.
-This is especially useful when merging records (more about this in the dedicated document about merge).  
-Examples:
-```
-> let Ais2ByDefault = { a | default = 2 } in
-  {} | #Ais2ByDefault
-{ a = 2 }
-
-> let Ais2ByDefault = { a | default = 2 } in
-  { a = 1 } | #Ais2ByDefault
-{ a = 1 }
-
-> { foo | default = 1, bar = foo + 1 }
-{ foo = 1, bar = 2 }
-
-> {foo | default = 1, bar = foo + 1} & {foo = 2}
-{ foo = 2, bar = 3 }
-```
diff --git a/doc/manual/typing.md b/doc/manual/typing.md
index 97eb0df9..651b783b 100644
--- a/doc/manual/typing.md
+++ b/doc/manual/typing.md
@@ -1,7 +1,32 @@
 # Typing in Nickel
 
-(For the motivations behind typing and a high-level overview of contracts and
-types, first read the [correctness](./correctness.md) section.)
+## Introduction
+
+Usually, static typing brings in important benefits for large codebases of
+general-purpose programming languages, but the case of an interpreted
+configuration language appears less clear-cut.
+
+For pure configuration code, which is mostly data, static typing is not as
+useful. First, a configuration is a terminating program run once on fixed
+inputs: here, basic type errors will show up at runtime anyway. Second, Nickel
+has a powerful validation system, contracts, that can do the same job as types
+and more.
+
+Nevertheless, if you have ever faced puzzling [dynamic type
+errors](https://www.haskellforall.com/2021/01/dynamic-type-errors-lack-relevance.html),
+you may have felt the need for something better. Classic dynamic typing is prone
+to error messages being unrelated to the actual issue and pointing to a location
+far from the offending code. This is especially salient when working with
+functions, which tend to delay type errors by passing around ill-formed values
+until they eventually break evaluation somewhere else. For reusable code, i.e.
+functions, static typing really helps.
+
+This apparent dilemma is solved in Nickel by supporting *gradual typing*.
+Gradual typing enables to mix both static typing and dynamic typing.
+
+The following is a detailed exposition of this gradual type system. If you are
+rather looking for a cheat-sheet about when to use static typing or contracts,
+please visit [Type versus contracts: when to?](./types-vs-contracts.md).
 
 ## Typing modes
 
diff --git a/examples/config-gcc/config-gcc.ncl b/examples/config-gcc/config-gcc.ncl
index ee01c987..a944eba9 100644
--- a/examples/config-gcc/config-gcc.ncl
+++ b/examples/config-gcc/config-gcc.ncl
@@ -52,15 +52,15 @@ let OptLevel = fun label value =>
 
 let Contract = {
   path_libc | doc "Path to libc."
-            | Path
-            | SharedObjectFile
-            | default = "/lib/x86_64-linux-gnu/libc.so",
+           | #Path
+           | #SharedObjectFile
+           | default = "/lib/x86_64-linux-gnu/libc.so",
 
   flags | doc "
             Additional flags to pass to GCC. Either provide a string without the
             leading `-`, or a structured value `{flag : Str, arg: Str}`.
           "
-        | List GccFlag
+        | List #GccFlag
         | default = [],
 
   optimization_level | doc "
@@ -70,11 +70,11 @@ let Contract = {
                         - *1*: normal
                         - *2*: use optimizations
                       "
-                     | OptLevel
-                     | default = 1,
+                    | #OptLevel
+                    | default = 1,
 } in
 
 {
   flags = ["Wextra", {flag = "o", arg = "stuff.o"}],
   optimization_level = 2,
-} | Contract
+} | #Contract
diff --git a/examples/record-contract/record-contract.ncl b/examples/record-contract/record-contract.ncl
index 232abe2d..90b98e7a 100644
--- a/examples/record-contract/record-contract.ncl
+++ b/examples/record-contract/record-contract.ncl
@@ -12,17 +12,17 @@ let PortElt
   | doc "A contract for a port element of a Kubernetes configuration"
   = {
     name | Str,
-    containerPort | Port,
+    containerPort | #Port,
   } in
 
 let Container = {
   name | Str,
   image | Str,
-  ports | List PortElt,
+  ports | List #PortElt,
 } in
 
 let KubernetesConfig = {
-  kind | [| ReplicationController, ReplicaSet, Pod |]
+  kind | <ReplicationController, ReplicaSet, Pod>
        | doc "The kind of the element being configured."
        | default = `Pod,
 
@@ -34,7 +34,7 @@ let KubernetesConfig = {
   },
 
   spec = {
-    replicas | nums.PosNat
+    replicas | #nums.PosNat
              | doc "The number of replicas"
              | default = 1,
 
@@ -42,7 +42,7 @@ let KubernetesConfig = {
 
     template = {
       metadata.labels.app | Str,
-      spec.containers | List Container,
+      spec.containers | List #Container,
     },
   },
 } in
@@ -81,4 +81,4 @@ let metadata_ = {
         }
     }
   }
-} | KubernetesConfig
+} | #KubernetesConfig
diff --git a/examples/simple-contracts/simple-contract-bool.ncl b/examples/simple-contracts/simple-contract-bool.ncl
index 411daa4f..f636bd69 100644
--- a/examples/simple-contracts/simple-contract-bool.ncl
+++ b/examples/simple-contracts/simple-contract-bool.ncl
@@ -14,5 +14,5 @@ let AlwaysFalse = EqualsTo false in
 // promise that the return value is false.
 // Try passing `false` to `not`, or to use the identity function (replacing `!x`
 // by `x`) to see contract errors appear.
-let not | AlwaysTrue -> AlwaysFalse = fun x => !x in
+let not | #AlwaysTrue -> #AlwaysFalse = fun x => !x in
 not true
diff --git a/examples/simple-contracts/simple-contract-div.ncl b/examples/simple-contracts/simple-contract-div.ncl
index 8e33eef5..90655cce 100644
--- a/examples/simple-contracts/simple-contract-div.ncl
+++ b/examples/simple-contracts/simple-contract-div.ncl
@@ -12,5 +12,5 @@ let DivBy3 = fun label value =>
   else
     contracts.blame label in
 // Will cause an error! 4 is no divided by 3.
-(4 | Even
-   | DivBy3)
+(4 | #Even
+   | #DivBy3)
diff --git a/flake.lock b/flake.lock
index af4da6bf..7f438591 100644
--- a/flake.lock
+++ b/flake.lock
@@ -2,11 +2,11 @@
   "nodes": {
     "flake-utils": {
       "locked": {
-        "lastModified": 1644229661,
-        "narHash": "sha256-1YdnJAsNy69bpcjuoKdOYQX0YxZBiCYZo4Twxerqv7k=",
+        "lastModified": 1642700792,
+        "narHash": "sha256-XqHrk7hFb+zBvRg6Ghl+AZDq03ov6OshJLiSWOoX5es=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "3cecb5b042f7f209c56ffd8371b2711a290ec797",
+        "rev": "846b2ae0fc4cc943637d3d1def4454213e203cba",
         "type": "github"
       },
       "original": {
@@ -32,11 +32,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1644525281,
-        "narHash": "sha256-D3VuWLdnLmAXIkooWAtbTGSQI9Fc1lkvAr94wTxhnTU=",
+        "lastModified": 1643805626,
+        "narHash": "sha256-AXLDVMG+UaAGsGSpOtQHPIKB+IZ0KSd9WS77aanGzgc=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "48d63e924a2666baf37f4f14a18f19347fbd54a2",
+        "rev": "554d2d8aa25b6e583575459c297ec23750adb6cb",
         "type": "github"
       },
       "original": {
@@ -87,11 +87,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1644633594,
-        "narHash": "sha256-Te6mBYYirUwsoqENvVx1K1EEoRq2CKrTnNkWF42jNgE=",
+        "lastModified": 1643941258,
+        "narHash": "sha256-uHyEuICSu8qQp6adPTqV33ajiwoF0sCh+Iazaz5r7fo=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "14c48021a9a5fe6ea8ae6b21c15caa106afa9d19",
+        "rev": "674156c4c2f46dd6a6846466cb8f9fee84c211ca",
         "type": "github"
       },
       "original": {
diff --git a/lsp/nls/src/requests/hover.rs b/lsp/nls/src/requests/hover.rs
index d862725b..06e417e0 100644
--- a/lsp/nls/src/requests/hover.rs
+++ b/lsp/nls/src/requests/hover.rs
@@ -72,10 +72,6 @@ pub fn handle(
                     language: "plain".into(),
                     value: meta.join("\n"),
                 }),
-                MarkedString::LanguageString(LanguageString {
-                    language: "plain".into(),
-                    value: format!("{:?} @ {:?}", item, range,),
-                }),
             ]),
 
             range: Some(range),
diff --git a/src/cache.rs b/src/cache.rs
index b6cd2ba7..d7145ebf 100644
--- a/src/cache.rs
+++ b/src/cache.rs
@@ -8,7 +8,6 @@ use crate::term::{RichTerm, SharedTerm, Term};
 use crate::transform::import_resolution;
 use crate::typecheck;
 use crate::typecheck::{linearization::StubHost, type_check};
-use crate::types::UnboundTypeVariableError;
 use crate::{eval, parser, transform};
 use codespan::{FileId, Files};
 use io::Read;
@@ -444,10 +443,7 @@ impl Cache {
     /// or do nothing if the entry has already been transformed. Require that the corresponding
     /// source has been parsed.
     /// If the source contains imports, recursively perform transformations on the imports too.
-    pub fn transform(
-        &mut self,
-        file_id: FileId,
-    ) -> Result<CacheOp<()>, CacheError<UnboundTypeVariableError>> {
+    pub fn transform(&mut self, file_id: FileId) -> Result<CacheOp<()>, CacheError<()>> {
         match self.entry_state(file_id) {
             Some(state) if state >= EntryState::Transformed => Ok(CacheOp::Cached(())),
             Some(state) if state >= EntryState::Parsed => {
@@ -455,7 +451,7 @@ impl Cache {
                     let CachedTerm {
                         term, parse_errs, ..
                     } = self.terms.remove(&file_id).unwrap();
-                    let term = transform::transform(term)?;
+                    let term = transform::transform(term);
                     self.terms.insert(
                         file_id,
                         CachedTerm {
@@ -508,38 +504,29 @@ impl Cache {
                 } = self.terms.remove(&file_id).unwrap();
 
                 if state < EntryState::Transforming {
-                    let pos = term.pos;
-
                     match SharedTerm::make_mut(&mut term.term) {
                         Term::Record(ref mut map, _) => {
-                            let map_res: Result<_, UnboundTypeVariableError> = std::mem::take(map)
+                            let map_res = std::mem::take(map)
                                 .into_iter()
-                                .map(|(id, t)| Ok((id, transform::transform(t)?)))
+                                .map(|(id, t)| (id, transform::transform(t)))
                                 .collect();
-                            *map = map_res.map_err(|err| {
-                                CacheError::Error(ImportError::ParseErrors(err.into(), pos))
-                            })?;
+                            *map = map_res;
                         }
                         Term::RecRecord(ref mut map, ref mut dyn_fields, _) => {
-                            let map_res: Result<_, UnboundTypeVariableError> = std::mem::take(map)
+                            let map_res = std::mem::take(map)
+                                .into_iter()
+                                .map(|(id, t)| (id, transform::transform(t)))
+                                .collect();
+
+                            let dyn_fields_res = std::mem::take(dyn_fields)
                                 .into_iter()
-                                .map(|(id, t)| Ok((id, transform::transform(t)?)))
+                                .map(|(id_t, t)| {
+                                    (transform::transform(id_t), transform::transform(t))
+                                })
                                 .collect();
 
-                            let dyn_fields_res: Result<_, UnboundTypeVariableError> =
-                                std::mem::take(dyn_fields)
-                                    .into_iter()
-                                    .map(|(id_t, t)| {
-                                        Ok((transform::transform(id_t)?, transform::transform(t)?))
-                                    })
-                                    .collect();
-
-                            *map = map_res.map_err(|err| {
-                                CacheError::Error(ImportError::ParseErrors(err.into(), pos))
-                            })?;
-                            *dyn_fields = dyn_fields_res.map_err(|err| {
-                                CacheError::Error(ImportError::ParseErrors(err.into(), pos))
-                            })?;
+                            *map = map_res;
+                            *dyn_fields = dyn_fields_res;
                         }
                         _ => panic!("cache::transform_inner(): not a record"),
                     }
@@ -645,15 +632,9 @@ impl Cache {
             result = CacheOp::Done(());
         };
 
-        let transform_res = self.transform(file_id).map_err(|cache_err| {
-            Error::ParseErrors(
-                cache_err
-                    .unwrap_error(
-                        "cache::prepare(): expected source to be parsed before transformations",
-                    )
-                    .into(),
-            )
-        })?;
+        let transform_res = self.transform(file_id).unwrap_or_else(|_| {
+            panic!("cache::prepare(): expected source to be parsed before transformations",)
+        });
 
         if transform_res == CacheOp::Done(()) {
             result = CacheOp::Done(());
@@ -679,7 +660,7 @@ impl Cache {
         }
         let (term, pending) = import_resolution::resolve_imports(term, self)?;
         type_check(&term, global_env, self, StubHost::<(), (), _>::new())?;
-        let term = transform::transform(term).map_err(|err| Error::ParseErrors(err.into()))?;
+        let term = transform::transform(term);
         Ok((term, pending))
     }
 
diff --git a/src/destruct.rs b/src/destruct.rs
index e3f070aa..e076f96f 100644
--- a/src/destruct.rs
+++ b/src/destruct.rs
@@ -3,7 +3,6 @@
 
 use crate::identifier::Ident;
 use crate::label::Label;
-use crate::position::RawSpan;
 use crate::term::{Contract, MetaValue, RecordAttrs, RichTerm, Term};
 use crate::types::{AbsType, Types};
 
@@ -34,15 +33,10 @@ pub enum LastMatch {
 /// A destructuring pattern without the `x @` part.
 #[derive(Debug, PartialEq, Clone)]
 pub enum Destruct {
-    /// A record pattern, the only one implemented for now.
-    Record {
-        matches: Vec<Match>,
-        open: bool,
-        rest: Option<Ident>,
-        span: RawSpan,
-    },
+    /// A record pattern, the onlyone implemented for now.
+    Record(Vec<Match>, bool, Option<Ident>),
     /// A list destructuring. Not implemented.
-    List { matches: Vec<Match>, span: RawSpan },
+    List(Vec<Match>),
     /// An empty destructuring. In this case, the pattern is a clasical `let var = something in
     /// body` form.
     Empty,
@@ -51,11 +45,6 @@ pub enum Destruct {
 impl Destruct {
     /// generate the metavalue containing the contract representing this pattern.
     pub fn as_contract(self) -> MetaValue {
-        let label = self.label();
-        self.as_contract_with_lbl(label)
-    }
-
-    fn as_contract_with_lbl(self, label: Label) -> MetaValue {
         let open = self.is_open();
         MetaValue {
             contracts: vec![Contract {
@@ -69,7 +58,7 @@ impl Destruct {
                     )
                     .into(),
                 )),
-                label,
+                label: Label::dummy(),
             }],
             ..Default::default()
         }
@@ -78,25 +67,17 @@ impl Destruct {
     /// Get the inner vector of `Matches` of the pattern. If `Empty` return a empty vector.
     pub fn inner(self) -> Vec<Match> {
         match self {
-            Destruct::Record { matches, .. } | Destruct::List { matches, .. } => matches,
+            Destruct::Record(i, _, _) | Destruct::List(i) => i,
             Destruct::Empty => vec![],
         }
     }
 
-    // Generate a label for this `Destruct`. if `Empty`, return default label.
-    fn label(&self) -> Label {
-        match *self {
-            Destruct::Record { span, .. } | Destruct::List { span, .. } => Label {
-                span,
-                ..Default::default()
-            },
-            Destruct::Empty => Label::default(),
-        }
-    }
-
     /// Is this pattern open? Does it finish with `, ..}` form?
     pub fn is_open(&self) -> bool {
-        matches!(self, Destruct::Record { open: true, .. })
+        match self {
+            Destruct::Record(_, o, _) => *o,
+            _ => false,
+        }
     }
 
     /// check if the pattern is empty.
@@ -113,22 +94,11 @@ impl Match {
             Match::Assign(id, m, (_, Destruct::Empty)) | Match::Simple(id, m) => {
                 (id, Term::MetaValue(m).into())
             }
-
-            // In this case we fuse spans of the `Ident` (LHS) with the destruct (RHS)
-            // because we can have two cases:
-            //
-            // - extra field on the destructuring `d`
-            // - missing field on the `id`
-            Match::Assign(id, m, (_, d @ Destruct::Record { .. })) => {
-                let label @ Label { span, .. } = d.label();
-                let span = RawSpan::fuse(id.pos.unwrap(), span).unwrap();
-                let label = Label { span, ..label };
-                (
-                    id,
-                    Term::MetaValue(MetaValue::flatten(m, d.as_contract_with_lbl(label))).into(),
-                )
-            }
-            Match::Assign(_id, _m, (_, _d @ Destruct::List { .. })) => unimplemented!(),
+            Match::Assign(id, m, (_, d @ Destruct::Record(..))) => (
+                id,
+                Term::MetaValue(MetaValue::flatten(m, d.as_contract())).into(),
+            ),
+            Match::Assign(_id, _m, (_, _d @ Destruct::List(..))) => unimplemented!(),
         }
     }
 }
diff --git a/src/error.rs b/src/error.rs
index 415c30c4..374e6fb8 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -291,21 +291,6 @@ pub enum ParseError {
     ),
     /// Unbound type variable
     UnboundTypeVariables(Vec<Ident>, RawSpan),
-    /// Illegal record literal in the uniterm syntax. In practice, this is a record with a
-    /// polymorphic tail that contains a construct that wasn't permitted inside a record type in
-    /// the original syntax. Typically, a field assignment:
-    ///
-    /// ```nickel
-    /// forall a. {foo : Num; a} // allowed
-    /// forall a. {foo : Num = 1; a} // InvalidUniRecord error: giving a value to foo is forbidden
-    /// ```
-    ///
-    /// See [RFC002](../../rfcs/002-merge-types-terms-syntax.md) for more details.
-    InvalidUniRecord(
-        RawSpan, /* illegal (in conjunction with a tail) construct position */
-        RawSpan, /* tail position */
-        RawSpan, /* whole record position */
-    ),
 }
 
 /// An error occurring during the resolution of an import.
@@ -459,9 +444,6 @@ impl ParseError {
                 InternalParseError::UnboundTypeVariables(idents, span) => {
                     ParseError::UnboundTypeVariables(idents, span)
                 }
-                InternalParseError::InvalidUniRecord(illegal_pos, tail_pos, pos) => {
-                    ParseError::InvalidUniRecord(illegal_pos, tail_pos, pos)
-                }
             },
         }
     }
@@ -1213,17 +1195,6 @@ impl ToDiagnostic<FileId> for ParseError {
                         .join(",")
                 ))
                 .with_labels(vec![primary(span)]),
-            ParseError::InvalidUniRecord(illegal_span, tail_span, span) => Diagnostic::error()
-                .with_message(format!("invalid record literal"))
-                .with_labels(vec![
-                    primary(span),
-                    secondary(illegal_span).with_message("can't use this record construct"),
-                    secondary(tail_span).with_message("in presence of a tail"),
-                ])
-                .with_notes(vec![
-                    String::from("Using a polymorphic tail in a record `{ ..; a}` requires the rest of the record to be only composed of type annotations, of the form `<field>: <type>`."),
-                    String::from("Value assignements, such as `<field> = <expr>`, metadata, etc. are forbidden."),
-                ]),
         };
 
         vec![diagnostic]
diff --git a/src/eval/merge.rs b/src/eval/merge.rs
index a578881a..f5b55d94 100644
--- a/src/eval/merge.rs
+++ b/src/eval/merge.rs
@@ -258,7 +258,7 @@ pub fn merge(
                         &env1,
                         types2.iter().chain(contracts2.iter()),
                         &env2,
-                    )?;
+                    );
                     (Some(v), e)
                 }
                 v1 => (v1, env1.clone()),
@@ -275,7 +275,7 @@ pub fn merge(
                         &env2,
                         types1.iter().chain(contracts1.iter()),
                         &env1,
-                    )?;
+                    );
                     (Some(v), e)
                 }
                 v2 => (v2, env2.clone()),
@@ -433,26 +433,21 @@ pub fn merge(
 fn cross_apply_contracts<'a>(
     t1: RichTerm,
     env1: &Environment,
-    mut it2: impl Iterator<Item = &'a Contract>,
+    it2: impl Iterator<Item = &'a Contract>,
     env2: &Environment,
-) -> Result<(RichTerm, Environment), EvalError> {
+) -> (RichTerm, Environment) {
     let mut env = Environment::new();
     let mut env1_local = env1.clone();
 
     let pos = t1.pos.into_inherited();
     let result = it2
-        .try_fold(t1, |acc, ctr| {
+        .fold(t1, |acc, ctr| {
             let ty_closure = ctr.types.clone().closurize(&mut env1_local, env2.clone());
-            mk_term::assume(ty_closure, ctr.label.clone(), acc)
-                .map_err(|crate::types::UnboundTypeVariableError(id)| {
-                    let pos = id.pos;
-                    EvalError::UnboundIdentifier(id, pos)
-                })
-                .map(|rt| rt.with_pos(pos))
-        })?
+            mk_term::assume(ty_closure, ctr.label.clone(), acc).with_pos(pos)
+        })
         .closurize(&mut env, env1_local);
 
-    Ok((result, env))
+    (result, env)
 }
 
 /// Merge the two optional documentations of a metavalue.
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index e597e4b3..abc99361 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -1,101 +1,33 @@
-//! The Nickel grammar.
-//!
-//! # Uniterm
-//!
-//! Nickel uses the uniterm grammar since
-//! [RFC002](../rfcs/002-merge-types-terms-syntax.md). Uniterm is a common
-//! grammar for both term and types. However, it is only a front-end: the rest of
-//! the interpreter pipeline needs terms and types to be separate objects.
-//!
-//! Most of the time, grammar constructs determine unambiguously if an expression
-//! should be considered as a type or a term. Typically, `e1 -> e2` will always
-//! be a type, and `e1 + e2` a term. This doesn't contradict the fact that `e1 ->
-//! e2` can be used as a term: the point is, even in the latter case, we still
-//! parse `e1 -> e2` as a type first, and then derive a term from it wherever it
-//! is used in a context expecting a term.
-//!
-//! This is not the case of all rules. Record literals and variables can both be
-//! interpreted in a different way, depending on how their usage. In
-//! `x : {foo : Num}`, `{foo : Num}` is interpreted as a record type. In `{foo :
-//! Num}.foo`, it is a record literal with a missing definition for `foo`. The
-//! first interpretation is **not** equivalent to first interpreting it as a
-//! term, and then as a type.
-//!
-//! For those reasons, the `uniterm` module introduces a new AST definition, that
-//! just wraps `RichTerm` and `Types`, together with dedicated variants for the
-//! common constructs that are variables and records. As long as a common
-//! construct is not used in a term or a type context, it can be still
-//! interpreted as both. Once the usage determines the nature of a record or a
-//! variable, it is converted to either a `RichTerm` or a `Types` (although still
-//! possibly wrapped as a `UniTerm`).
-//!
-//! In consequence, this grammar uses three main types `RichTerm`, `Types` and
-//! `UniTerm`, as well as conversion macros `AsTerm`, `AsType` and `AsUniTerm`.
-//! Some rules that are known to only produce `RichTerm` or `Types` may have the
-//! corresponding more precise return type. Other rules that produce or just
-//! propagate general uniterms have to return a `UniTerm`.
-use std::{
-    collections::HashMap,
-    ffi::OsString,
-    convert::TryFrom,
-};
+use std::collections::HashMap;
+use std::ffi::OsString;
 
 use codespan::FileId;
+
 use lalrpop_util::ErrorRecovery;
 
-use super::{
-    ExtendedTerm,
-    utils::*,
-    lexer::{Token, NormalToken, StringToken, MultiStringToken},
-    error::ParseError,
-    uniterm::*,
-};
+use super::ExtendedTerm;
+use super::utils::*;
+use super::lexer::{Token, NormalToken, StringToken, MultiStringToken};
 
-use crate::{
-    mk_app,
-    mk_opn,
-    mk_fun,
-    identifier::Ident,
-    destruct::{Match, LastMatch, Destruct},
-    term::{
-        BinaryOp, RichTerm, Term, UnaryOp, StrChunk, MetaValue,
-        MergePriority, Contract, NAryOp, RecordAttrs, SharedTerm,
-        make as mk_term},
-    types::{Types, AbsType},
-    position::TermPos,
-    label::Label,
-};
+use crate::{mk_app, mk_opn, mk_fun};
+use crate::identifier::Ident;
+use crate::destruct::{Match, LastMatch, Destruct};
+use crate::parser::error::ParseError;
+use crate::term::{BinaryOp, RichTerm, Term, UnaryOp, StrChunk, MetaValue,
+    MergePriority, Contract, NAryOp, RecordAttrs, SharedTerm};
+use crate::term::make as mk_term;
+use crate::types::{Types, AbsType};
 
 grammar<'input, 'err>(src_id: FileId, errors: &'err mut Vec<ErrorRecovery<usize, Token<'input>, ParseError>>);
 
-WithPos<Rule>: Rule = <l: @L> <t: Rule> <r: @R> => t.with_pos(mk_pos(src_id, l, r));
-
-AsTerm<Rule>: RichTerm = <ut: WithPos<Rule>> =>?
-    RichTerm::try_from(ut)
-        .map_err(|e| lalrpop_util::ParseError::User{error: e});
-
-AsType<Rule>: Types = <ut: WithPos<Rule>> =>?
-    Types::try_from(ut)
-        .map_err(|e| lalrpop_util::ParseError::User{error: e});
-
-AsUniTerm<Rule>: UniTerm = <l: @L> <ut: Rule> <r: @R> =>
-    UniTerm::from(ut).with_pos(mk_pos(src_id, l, r));
-
-// A single type or meta-data annotation. The `Types` rule forbids the use of
-// constructs that can themselves have annotation on the right, such as a `let`.
-// Otherwise, `foo | let x = 1 in x : Num` is ambiguous (the annotation could be
-// either `foo | (let x = 1 in (x : Num))` or `(foo | let x = 1 in x) : Num`).
-//
-// The rule to use for type annotations is given as a parameter. We always use a
-// rule that is syntactically equivalent to the `Types` rule. The parameter is
-// here to control if the type should have its variables fixed now (`FixedType`)
-// or later (bare `Types`). Almost all rules are of the former kind, and use
-// `FixedType` (see `FixedType` and `parser::utils::fix_type_vars`).
-AnnotAtom<TypeRule>: MetaValue = {
-    "|" <l: @L> <ty: TypeRule> <r: @R> => MetaValue {
+WithPos<Rule>: RichTerm = <l: @L> <t: Rule> <r: @R> => t.with_pos(mk_pos(src_id, l, r));
+CheckUnbound<Rule>: Types = <l: @L> <t: Rule> <r: @R> =>? check_unbound(&t, mk_span(src_id, l, r)).map_err(|e| lalrpop_util::ParseError::User{error: e}).and(Ok(t));
+
+AnnotAtom: MetaValue = {
+    "|" <l: @L> <ty_res: CheckUnbound<Types>> <r: @R> => MetaValue {
         doc: None,
         types: None,
-        contracts: vec![Contract {types: ty.clone(), label: mk_label(ty, src_id, l, r)}],
+        contracts: vec![Contract {types: ty_res.clone(), label: mk_label(ty_res, src_id, l, r)}],
         priority: Default::default(),
         value: None,
     },
@@ -113,40 +45,27 @@ AnnotAtom<TypeRule>: MetaValue = {
         priority: Default::default(),
         value: None,
     },
-    ":" <l: @L> <ty: TypeRule> <r: @R> => MetaValue {
+    ":" <l: @L> <ty_res: CheckUnbound<Types>> <r: @R> => MetaValue {
         doc: None,
-        types: Some(Contract {types: ty.clone(), label: mk_label(ty, src_id, l, r)}),
+        types: Some(Contract {types: ty_res.clone(), label: mk_label(ty_res, src_id, l, r)}),
         contracts: Vec::new(),
         priority: Default::default(),
         value: None,
     },
 };
 
-// An annotation, with possibly many metadata annotations chained.
-Annot<TypeRule>: MetaValue = <anns: AnnotAtom<TypeRule>+> => anns.into_iter().fold(MetaValue::new(), MetaValue::flatten);
-
-// A general term. Wrap the root of the grammar as a `RichTerm`.
-pub Term: RichTerm = AsTerm<UniTerm>;
-
-// A general type. Chosen such that it can't have top-level annotations.
-// (see `AnnotAtom`)
-Types: Types = {
-    AsType<InfixExpr>,
-    Forall,
+DefaultAnnot: MetaValue = "?" <t: Term> => MetaValue {
+    priority: MergePriority::Default,
+    value: Some(t),
+    ..Default::default()
 };
 
-// A type with type variables fixed. See `parser::utils::fix_type_vars`.
-FixedType: Types = {
-    <mut ty: Types> => {
-        fix_type_vars(&mut ty);
-        ty
-    }
-};
+Annot: MetaValue = <anns: AnnotAtom+> => anns.into_iter().fold(MetaValue::new(), MetaValue::flatten);
+
+pub Term: RichTerm = WithPos<RootTerm>;
 
-// Either a term or a top-level let-binding (a let-binding without an `in`).
-// Used exclusively for the REPL.
 pub ExtendedTerm: ExtendedTerm = {
-    "let" <id: Ident> <meta: Annot<FixedType>?> "=" <t: Term> => {
+    "let" <id: Ident> <meta: Annot?> "=" <t: Term> => {
         let t = if let Some(mut meta) = meta {
             let pos = t.pos;
             meta.value = Some(t);
@@ -155,20 +74,14 @@ pub ExtendedTerm: ExtendedTerm = {
         else {
             t
         };
-
         ExtendedTerm::ToplevelLet(id, t)
     },
     Term => ExtendedTerm::RichTerm(<>),
-};
+}
 
-// A general uniterm. The root of the grammar.
-UniTerm: UniTerm = {
-    InfixExpr,
-    AnnotatedInfixExpr,
-    AsUniTerm<Forall>,
-    "let" <pat:Pattern> <meta: Annot<FixedType>?>
-        "=" <t1: Term>
-        "in" <t2: Term> => {
+RootTerm: RichTerm = {
+    "let" <pat:Pattern> <meta: Annot?> "=" <t1: Term> "in"
+        <t2: Term> => {
         let t1 = if let Some(mut meta) = meta {
             let pos = t1.pos;
             meta.value = Some(t1);
@@ -178,18 +91,16 @@ UniTerm: UniTerm = {
             t1
         };
 
-        UniTerm::from(mk_term::let_pat(pat.0, pat.1, t1, t2))
+        mk_term::let_pat(pat.0, pat.1, t1, t2)
     },
     <l: @L> "fun" <pats: Pattern+> "=>" <t: Term> <r: @R> => {
         let pos = mk_pos(src_id, l, r);
-        let rt = pats.into_iter().rev().fold(t, |t, (id, destruct)| RichTerm {
+        pats.into_iter().rev().fold(t, |t, (id, destruct)| RichTerm {
             term: SharedTerm::new(Term::FunPattern(id, destruct, t)),
             pos,
-        });
-
-        UniTerm::from(rt)
+        })
     },
-    "switch" "{" <cases: (SwitchCase ",")*> <last: SwitchCase?> "}"
+    "switch" "{" <cases: (switch_case ",")*> <last: switch_case?> "}"
         <exp: Term> => {
         let mut acc = HashMap::with_capacity(cases.len());
         let mut default = None;
@@ -203,7 +114,7 @@ UniTerm: UniTerm = {
             };
         }
 
-        UniTerm::from(
+        RichTerm::from(
             Term::Switch(
                 exp,
                 acc,
@@ -212,90 +123,60 @@ UniTerm: UniTerm = {
         )
     },
     "if" <cond: Term> "then" <t1: Term> "else" <t2: Term> =>
-        UniTerm::from(mk_app!(Term::Op1(UnaryOp::Ite(), cond), t1, t2)),
-    <l: @L> <t: !> <r: @R> => {
-        let pos = mk_pos(src_id, l, r);
-        errors.push(t);
-
-        UniTerm::from(RichTerm::new(Term::ParseError, pos))
-    },
+        mk_app!(Term::Op1(UnaryOp::Ite(), cond), t1, t2),
+    AnnotatedTerm,
+    <l: @L> <t: !> <r: @R> => { errors.push(t); RichTerm { term: SharedTerm::new(Term::ParseError), pos: mk_pos(src_id, l, r)} },
 };
 
-AnnotatedInfixExpr: UniTerm = {
-    <t: AsTerm<InfixExpr>> <mut meta: Annot<FixedType>> => {
-        let pos = t.pos;
-        meta.value = Some(t);
-        UniTerm::from(RichTerm::new(Term::MetaValue(meta), pos))
+AnnotatedTerm: RichTerm = {
+    <t: WithPos<Infix>> <meta: Annot?> => {
+        if let Some(mut meta) = meta {
+            let pos = t.pos;
+            meta.value = Some(t);
+            RichTerm::new(Term::MetaValue(meta), pos)
+        }
+        else {
+            t
+        }
     },
 };
 
-Forall: Types =
-    "forall" <ids: Ident+> "." <ty: Types> => {
-        ids.into_iter().rev().fold(
-            ty,
-            |acc, id| Types(AbsType::Forall(id, Box::new(acc)))
-        )
-    };
-
-// A n-ary application-like expression (n may be 0, in the sense that this rule
-// also includes previous levels).
-Applicative: UniTerm = {
-    "import" <s: StaticString> => UniTerm::from(Term::Import(OsString::from(s))),
-    <t1: AsTerm<Applicative>> <t2: AsTerm<RecordOperand>> =>
-        UniTerm::from(mk_app!(t1, t2)),
-    <op: UOp> <t: AsTerm<RecordOperand>> => UniTerm::from(mk_term::op1(op, t)),
-    <op: BOpPre> <t1: AsTerm<RecordOperand>> <t2: AsTerm<Atom>>
-        => UniTerm::from(mk_term::op2(op, t1, t2)),
-    NOpPre<AsTerm<RecordOperand>>,
-    RecordOperand,
+Infix: RichTerm = {
+    InfixExpr,
 };
 
-// The list type, potentially with an argument. Take precedence over
-// application: `List Foo` is always interpreted as the type `List` parametrized
-// by `Foo`, rather than the dynamic list type `List Dyn` aliased to `List` and
-// seen as a contract applied to term `Foo`.
-TypeList: Types =
-    "List" <TypeListParam?> => {
-        let ty = Box::new(<>.unwrap_or(Types(AbsType::Dyn())));
-        Types(AbsType::List(ty))
-    };
-
-// Possible parameter for the list type. It's `TypeAtom` augmented with an
-// argument-less `List`, which allows to parse `List List`. We can't add
-// argument-less `List` to type atoms directly, as it would make `List Foo`
-// ambiguous: could be parsed both as `List` as a term applied to `List` as a
-// term, or as the parametrized type `List List`).
-TypeListParam: Types = {
-    "List" => Types(AbsType::List(Box::new(Types(AbsType::Dyn())))),
-    AsType<Atom>,
+Applicative: RichTerm = {
+    "import" <s: StaticString> => RichTerm::from(Term::Import(OsString::from(s))),
+    <t1:WithPos<Applicative>> <t2: WithPos<RecordOperand>> => mk_app!(t1, t2),
+    <op: UOp> <t: WithPos<RecordOperand>> => mk_term::op1(op, t),
+    <op: BOpPre> <t1: WithPos<RecordOperand>> <t2: WithPos<Atom>> => mk_term::op2(op, t1, t2),
+    NOpPre<WithPos<RecordOperand>>,
+    RecordOperand,
 };
 
-RecordOperand: UniTerm = {
+RecordOperand: RichTerm = {
     Atom,
-    AsUniTerm<RecordOperationChain>,
-};
+    RecordOperationChain,
+}
 
-// A record operation chain, such as `{foo = data}.bar.baz`.
 RecordOperationChain: RichTerm = {
-    <t: AsTerm<RecordOperand>> "." <id: Ident> => mk_term::op1(UnaryOp::StaticAccess(id), t),
-    <t: AsTerm<RecordOperand>> "." <t_id: WithPos<StrChunks>> => mk_access(t_id, t),
-    <t: AsTerm<RecordOperand>> "-$" <t_id: AsTerm<Atom>> => mk_term::op2(BinaryOp::DynRemove(), t_id, t),
-    <r: AsTerm<RecordOperand>> "$[" <id: Term> "=" <t: Term> "]" =>
+    <t: WithPos<RecordOperand>> "." <id: Ident> => mk_term::op1(UnaryOp::StaticAccess(id), t),
+    <t: WithPos<RecordOperand>> "." <t_id: WithPos<StrChunks>> => mk_access(t_id, t),
+    <t: WithPos<RecordOperand>> "-$" <t_id: WithPos<Atom>> => mk_term::op2(BinaryOp::DynRemove(), t_id, t),
+    <r: WithPos<RecordOperand>> "$[" <id: Term> "=" <t: Term> "]" =>
         mk_app!(mk_term::op2(BinaryOp::DynExtend(), id, r), t),
 };
 
-RowTail: Types = {
-    <Ident> => Types(AbsType::Var(<>)),
-    "Dyn" => Types(AbsType::Dyn()),
-};
-
-// A record, that can be later interpreted either as a record literal or as a
-// record type.
-UniRecord: UniRecord = {
-   "{" <fields: (<RecordField> ",")*>
-       <last_l: @L> <last: RecordLastField?> <last_r: @R>
-       <tail_l: @L> <tail: (";" RowTail)?> <tail_r: @R>
-   "}" => {
+Atom: RichTerm = {
+    "(" <CurriedOp> ")",
+    "(" <Term> ")",
+    "num literal" => RichTerm::from(Term::Num(<>)),
+    "null" => RichTerm::from(Term::Null),
+    Bool => RichTerm::from(Term::Bool(<>)),
+    StrChunks,
+    Ident => RichTerm::from(Term::Var(<>)),
+    "`" <EnumTag> => RichTerm::from(Term::Enum(<>)),
+    "{" <fields: (<RecordField> ",")*> <last: RecordLastField?> "}" => {
         let (last_field, attrs) = match last {
             Some(RecordLastField::Field(f)) => (Some(f), Default::default()),
             Some(RecordLastField::Ellipsis) =>
@@ -303,48 +184,18 @@ UniRecord: UniRecord = {
             None => (None, Default::default())
         };
 
-        let pos_ellipsis = if attrs.open {
-                mk_pos(src_id, last_l, last_r)
-            }
-            else {
-                TermPos::None
-            };
-
-        let fields : Vec<_> = fields.into_iter().chain(last_field.into_iter()).collect();
-        UniRecord {
-            fields,
-            tail: tail.map(|t| (t.1, mk_pos(src_id, tail_l, tail_r))),
-            attrs,
-            pos: TermPos::None,
-            pos_ellipsis,
-        }
+        let fields = fields.into_iter().chain(last_field.into_iter());
+        RichTerm::from(build_record(fields, attrs))
     },
-};
-
-Atom: UniTerm = {
-    "(" <AsUniTerm<CurriedOp>> ")",
-    "(" <UniTerm> ")",
-    "num literal" => UniTerm::from(Term::Num(<>)),
-    "null" => UniTerm::from(Term::Null),
-    Bool => UniTerm::from(Term::Bool(<>)),
-    AsUniTerm<StrChunks>,
-    Ident => UniTerm::from(UniTermNode::Var(<>)),
-    UniRecord => UniTerm::from(UniTermNode::Record(<>)),
-    "`" <EnumTag> => UniTerm::from(Term::Enum(<>)),
     "[" <terms: (<Term> ",")*> <last: Term?> "]" => {
         let terms : Vec<RichTerm> = terms.into_iter()
             .chain(last.into_iter()).collect();
-
-        UniTerm::from(Term::List(terms))
-    },
-    AsUniTerm<TypeAtom>,
+        RichTerm::from(Term::List(terms))
+    }
 };
 
-// A record field definition. The is the only place where we don't fix the type
-// variables inside the annotation right away (note the `Annot<Types>` instead
-// of `Annot<Fixed>`).
-RecordField: (FieldPath, RichTerm) = {
-    <l: @L> <path: FieldPath> <ann: Annot<Types>?> <r: @R> <t: ("=" <Term>)?> => {
+RecordField: (FieldPathElem, RichTerm) = {
+    <l: @L> <path: FieldPath> <ann: Annot?> <r: @R> <t: ("=" <Term>)?> => {
         let pos = t.as_ref()
             .map(|t| t.pos.clone())
             .unwrap_or(mk_pos(src_id, l, r));
@@ -358,19 +209,18 @@ RecordField: (FieldPath, RichTerm) = {
                 RichTerm::new(Term::Null, pos)
             }
         };
-
-        (path, term)
+        elaborate_field_path(path, term)
     }
-};
+}
 
 RecordLastField: RecordLastField = {
     <RecordField> => RecordLastField::Field(<>),
     ".." => RecordLastField::Ellipsis,
-};
+}
 
-// A field path syntax in a field definition, as in `{foo."bar bar".baz = "value"}`.
 FieldPath: Vec<FieldPathElem> = {
-    <mut elems: (<FieldPathElem> ".")*> <last: FieldPathElem> => {
+    <elems: (<FieldPathElem> ".")*> <last: FieldPathElem> => {
+        let mut elems = elems;
         elems.push(last);
         elems
     }
@@ -381,84 +231,59 @@ FieldPathElem: FieldPathElem = {
     <WithPos<StrChunks>> => FieldPathElem::Expr(<>),
 };
 
-// Last field of a pattern
-LastMatch: LastMatch = {
-    Match => LastMatch::Match(<>),
-    ".." <Ident?> => LastMatch::Ellipsis(<>),
-};
-
-// The right hand side of an `=` inside a destructuring pattern.
 #[inline]
 Pattern: (Option<Ident>,Destruct) = {
     <id:(<Ident> "@")?> <pat:Destruct> => (id,pat),
     Ident => (Some(<>),Destruct::Empty),
 };
 
-// A full pattern at the left-hand side of a destructuring let.
 Destruct: Destruct = {
-    <start: @L> "{" <mut matches: (<Match> ",")*> <last:LastMatch?> "}" <end: @R> => {
-        let (open, rest) = match last {
+    "{" <mut matches: (<Match> ",")*> <last:LastMatch?> "}" => {
+        let (open, rst) = match last {
 	    Some(LastMatch::Match(m)) => {
 	        matches.push(m);
 	        (false,None)
 	    },
-	    Some(LastMatch::Ellipsis(rest)) => (true, rest),
+	    Some(LastMatch::Ellipsis(rst)) => (true, rst),
 	    _ => (false, None),
 	};
-	let span = mk_span(src_id, start, end);
-	Destruct::Record{matches, open, rest, span}
+	Destruct::Record(matches, open, rst)
     },
 };
 
-// A binding `ident = <pattern>` inside a destructuring pattern.
 Match: Match = {
-    <left:Ident> <anns: Annot<FixedType>?> <default: DefaultAnnot?> "=" <right: Pattern> => {
+    <left:Ident> <anns: Annot?> <default: DefaultAnnot?> "=" <right: Pattern> => {
 	let meta = match (default, anns) {
 	    (Some(d), Some(m)) => MetaValue::flatten(d,m),
 	    (Some(m),_) | (_,Some(m)) => m,
-  	    _ => MetaValue {
-	            contracts: vec![Contract{
-	                types: Types(AbsType::Dyn().into()),
-		        label: Label{span: left.pos.unwrap(), ..Default::default()},
-		    }],
-		    ..Default::default()
-	    },
+  	    _ => MetaValue::new(),
 	};
 	Match::Assign(left, meta, right)
     },
-    <id:Ident> <anns: Annot<FixedType>?> <default: DefaultAnnot?> => {
+    <id:Ident> <anns: Annot?> <default: DefaultAnnot?> => {
 	let meta = match (default, anns) {
 	    (Some(d), Some(m)) => MetaValue::flatten(d,m),
 	    (Some(m),_) | (_,Some(m)) => m,
-  	    _ => MetaValue {
-	            contracts: vec![Contract{
-	                types: Types(AbsType::Dyn().into()),
-		        label: Label{span: id.pos.unwrap(), ..Default::default()},
-		    }],
-		    ..Default::default()
-	    },
+  	    _ => MetaValue::new(),
 	};
 	Match::Simple(id, meta)
     },
 };
 
-// A default annotation in a pattern.
-DefaultAnnot: MetaValue = "?" <t: Term> => MetaValue {
-    priority: MergePriority::Default,
-    value: Some(t),
-    ..Default::default()
+LastMatch: LastMatch = {
+    Match => LastMatch::Match(<>),
+    ".."<Ident?> => LastMatch::Ellipsis(<>),
 };
 
-Ident: Ident = <l:@L> <i: "identifier"> <r:@R> =>
-    Ident { label: i.to_string(), pos: mk_pos(src_id, l, r) };
+Ident: Ident = <l:@L> <i: "identifier"> <r:@R>
+    => Ident { label: i.to_string(), pos: mk_pos(src_id, l, r) };
 
 Bool: bool = {
     "true" => true,
     "false" => false,
 };
 
-// Strings that support interpolation.
-StrChunks: RichTerm = {
+StrChunks : RichTerm = {
   <start: StringStart> <fst: ChunkLiteral?> <chunks: (ChunkExpr+ChunkLiteral)*> <lasts:ChunkExpr*> <end: StringEnd> => {
         debug_assert_eq!(start, end);
 
@@ -518,11 +343,12 @@ EnumTag: Ident = {
     <StaticString> => <>.into(),
 }
 
+
 ChunkLiteralPart: ChunkLiteralPart<'input> = {
     "str literal" => ChunkLiteralPart::Str(<>),
     "multstr literal" => ChunkLiteralPart::Str(<>),
     "str esc char" => ChunkLiteralPart::Char(<>),
-};
+    };
 
 UOp: UnaryOp = {
     "is_num" => UnaryOp::IsNum(),
@@ -561,14 +387,11 @@ UOp: UnaryOp = {
     "enum_from" => UnaryOp::EnumFromStr(),
 };
 
-SwitchCase: SwitchCase = {
+switch_case: SwitchCase = {
     "`" <id: EnumTag> "=>" <t: Term> => SwitchCase::Normal(id, t),
     "_" "=>" <t: Term> => SwitchCase::Default(<>),
 }
 
-// Infix operators by precedence levels. Lowest levels take precedence over
-// highest ones.
-
 InfixBOp2: BinaryOp = {
     "++" => BinaryOp::StrConcat(),
     "@" => BinaryOp::ListConcat(),
@@ -633,8 +456,7 @@ InfixOp: InfixOp = {
 }
 
 CurriedOp: RichTerm = {
-    <l: @L> <op: InfixOp> <r: @R> =>
-        op.eta_expand(mk_pos(src_id, l, r)),
+    <l: @L> <op: InfixOp> <r: @R> => op.eta_expand(mk_pos(src_id, l, r)),
     <l: @L> "|>" <r: @R> =>
         mk_fun!("x1", "x2",
             mk_app!(mk_term::var("x2"), mk_term::var("x1"))
@@ -651,40 +473,24 @@ CurriedOp: RichTerm = {
             )
             .with_pos(mk_pos(src_id, l, r))
         ),
-    //<l: @L> "->" <r: @R> =>?
-    //    UniTerm::from(
-    //        mk_fun!("x1", "x2",
-    //            mk_term::op1(
-    //                UnaryOp::BoolNot(),
-    //                Term::Op2(BinaryOp::Eq(),
-    //                    mk_term::var("x2"),
-    //                    mk_term::var("x1")
-    //                )
-    //            )
-    //            .with_pos(mk_pos(src_id, l, r))
-    //        )
-    //    ),
 }
 
-InfixUOpApp<UOp, Expr>: UniTerm =
-  <op: UOp> <t: AsTerm<Expr>> => UniTerm::from(mk_term::op1(op, t));
+InfixUOpApp<UOp, Expr>: RichTerm =
+  <op: UOp> <t: WithPos<Expr>> => mk_term::op1(op, t);
 
-InfixBOpApp<BOp, LExpr, RExpr>: UniTerm =
-  <t1: AsTerm<LExpr>> <op: BOp> <t2: AsTerm<RExpr>> =>
-      UniTerm::from(mk_term::op2(op, t1, t2));
+InfixBOpApp<BOp, LExpr, RExpr>: RichTerm =
+  <t1: WithPos<LExpr>> <op: BOp> <t2: WithPos<RExpr>> => mk_term::op2(op, t1, t2);
 
-InfixLazyBOpApp<UOp, LExpr, RExpr>: UniTerm =
-  <t1: AsTerm<LExpr>> <op: UOp> <t2: AsTerm<RExpr>> =>
-    UniTerm::from(mk_app!(mk_term::op1(op, t1), t2));
+InfixLazyBOpApp<UOp, LExpr, RExpr>: RichTerm =
+  <t1: WithPos<LExpr>> <op: UOp> <t2: WithPos<RExpr>> =>
+    mk_app!(mk_term::op1(op, t1), t2);
 
-InfixExpr: UniTerm = {
+InfixExpr: RichTerm = {
     #[precedence(level="0")]
     Applicative,
-    AsUniTerm<TypeList>,
 
     #[precedence(level="1")]
-    "-" <AsTerm<InfixExpr>> =>
-        UniTerm::from(mk_term::op2(BinaryOp::Sub(), Term::Num(0.0), <>)),
+    "-" <WithPos<InfixExpr>> => mk_term::op2(BinaryOp::Sub(), Term::Num(0.0), <>),
 
     #[precedence(level="2")] #[assoc(side="left")]
     InfixBOpApp<InfixBOp2, InfixExpr, InfixExpr>,
@@ -700,28 +506,21 @@ InfixExpr: UniTerm = {
 
     #[precedence(level="6")] #[assoc(side="left")]
     InfixBOpApp<InfixBOp6, InfixExpr, InfixExpr>,
-    <t1: AsTerm<InfixExpr>> "|>" <t2: AsTerm<InfixExpr>> =>
-        UniTerm::from(mk_app!(t2, t1)),
+    <t1: WithPos<InfixExpr>> "|>" <t2: WithPos<InfixExpr>> => mk_app!(t2, t1),
 
     #[precedence(level="7")] #[assoc(side="left")]
     InfixBOpApp<InfixBOp7, InfixExpr, InfixExpr>,
 
     #[precedence(level="8")] #[assoc(side="left")]
     InfixBOpApp<InfixBOp8, InfixExpr, InfixExpr>,
-    <t1: AsTerm<InfixExpr>> "!=" <t2: AsTerm<InfixExpr>> =>
-        UniTerm::from(
-            mk_term::op1(UnaryOp::BoolNot(), Term::Op2(BinaryOp::Eq(), t1, t2))
-        ),
+    <t1: WithPos<InfixExpr>> "!=" <t2: WithPos<InfixExpr>> =>
+        mk_term::op1(UnaryOp::BoolNot(), Term::Op2(BinaryOp::Eq(), t1, t2)),
 
     #[precedence(level="9")] #[assoc(side="left")]
     InfixLazyBOpApp<InfixLazyBOp9, InfixExpr, InfixExpr>,
 
     #[precedence(level="10")] #[assoc(side="left")]
     InfixLazyBOpApp<InfixLazyBOp10, InfixExpr, InfixExpr>,
-
-    #[precedence(level="11")] #[assoc(side="right")]
-    <s: AsType<InfixExpr>> "->" <t: AsType<InfixExpr>> =>
-        UniTerm::from(Types(AbsType::Arrow(Box::new(s), Box::new(t)))),
 }
 
 BOpPre: BinaryOp = {
@@ -741,25 +540,51 @@ BOpPre: BinaryOp = {
     "str_is_match" => BinaryOp::StrIsMatch(),
 }
 
-NOpPre<ArgRule>: UniTerm = {
+NOpPre<ArgRule>: RichTerm = {
     "str_replace" <t1: ArgRule> <t2: ArgRule> <t3: ArgRule> =>
-        UniTerm::from(mk_opn!(NAryOp::StrReplace(), t1, t2, t3)),
+        mk_opn!(NAryOp::StrReplace(), t1, t2, t3),
     "str_replace_regex" <t1: ArgRule> <t2: ArgRule> <t3: ArgRule> =>
-        UniTerm::from(mk_opn!(NAryOp::StrReplaceRegex(), t1, t2, t3)),
+        mk_opn!(NAryOp::StrReplaceRegex(), t1, t2, t3),
     "str_substr" <t1: ArgRule> <t2: ArgRule> <t3: ArgRule> =>
-        UniTerm::from(mk_opn!(NAryOp::StrSubstr(), t1, t2, t3)),
+        mk_opn!(NAryOp::StrSubstr(), t1, t2, t3),
 }
 
-TypeBuiltin: Types = {
+Types: Types = {
+    "forall" <ids: Ident+> "." <ty: Arrows> =>
+        ids.into_iter().rev().fold(
+            ty,
+            |acc, id| Types(AbsType::Forall(id, Box::new(acc)))
+        ),
+    <Arrows>
+}
+
+Arrows: Types = {
+    <s: subType> "->" <t:Arrows> => Types(AbsType::Arrow(Box::new(s), Box::new(t))),
+    <subType>,
+};
+
+BaseType: Types = {
     "Dyn" => Types(AbsType::Dyn()),
     "Num" => Types(AbsType::Num()),
     "Bool" => Types(AbsType::Bool()),
     "Str" => Types(AbsType::Str()),
+};
+
+RowTail: Types = {
+    <Ident> => Types(AbsType::Var(<>)),
+    "Dyn" => Types(AbsType::Dyn()),
 }
 
-TypeAtom: Types = {
-    <TypeBuiltin>,
-    "[|" <rows:(<EnumTag> ",")*> <last: (<EnumTag>)?> <tail: (";" <EnumTag>)?> "|]" => {
+subType : Types = {
+    <BaseType>,
+    "List" <ty: subType?> => {
+        let ty = Box::new(ty.unwrap_or(Types(AbsType::Dyn())));
+        Types(AbsType::List(ty))
+    },
+    <Ident> => Types(AbsType::Var(<>)),
+    "#" <WithPos<RecordOperand>> => Types(AbsType::Flat(<>)),
+    "(" <Types> ")",
+    "<" <rows:(<EnumTag> ",")*> <last: (<EnumTag>)?> <tail: ("|" <EnumTag>)?> ">" => {
         let ty = rows.into_iter()
             .chain(last.into_iter())
             // As we build row types as a linked list via a fold on the original
@@ -778,8 +603,27 @@ TypeAtom: Types = {
             );
         Types(AbsType::Enum(Box::new(ty)))
     },
+    "{" <rows:(<Ident> ":" <Types> ",")*>
+        <last:(<Ident> ":" <Types>)?>
+        <tail: ("|" <RowTail>)?> "}" => {
+        let ty = rows.into_iter()
+            .chain(last.into_iter())
+            // As we build row types as a linked list via a fold on the original
+            // iterator, the order of identifiers is reversed. This not a big deal
+            // but it's less confusing to the user to print them in the original
+            // order for error reporting.
+            .rev()
+            .fold(
+                tail.unwrap_or(Types(AbsType::RowEmpty())),
+                |t, i_ty| {
+                    let (i, ty) = i_ty;
+                    Types(AbsType::RowExtend(i, Some(Box::new(ty)), Box::new(t)))
+                }
+            );
+        Types(AbsType::StaticRecord(Box::new(ty)))
+    },
     "{" "_" ":" <Types> "}" => Types(AbsType::DynRecord(Box::new(<>))),
-}
+};
 
 extern {
     type Location = usize;
@@ -806,7 +650,6 @@ extern {
 
         "?" => Token::Normal(NormalToken::QuestionMark),
         "," => Token::Normal(NormalToken::Comma),
-        ";" => Token::Normal(NormalToken::Semicolon),
         ":" => Token::Normal(NormalToken::Colon),
         "$" => Token::Normal(NormalToken::Dollar),
         "=" => Token::Normal(NormalToken::Equals),
@@ -917,7 +760,5 @@ extern {
         "<=" => Token::Normal(NormalToken::LessOrEq),
         ">" => Token::Normal(NormalToken::RAngleBracket),
         ">=" => Token::Normal(NormalToken::GreaterOrEq),
-        "[|" => Token::Normal(NormalToken::EnumOpen),
-        "|]" => Token::Normal(NormalToken::EnumClose),
     }
 }
diff --git a/src/identifier.rs b/src/identifier.rs
index b096827c..570aab72 100644
--- a/src/identifier.rs
+++ b/src/identifier.rs
@@ -4,7 +4,7 @@ use std::{fmt, hash::Hash};
 
 use crate::position::TermPos;
 
-#[derive(Debug, Clone, Default, Deserialize, Serialize)]
+#[derive(Debug, Clone, Deserialize, Serialize)]
 #[serde(into = "String", from = "String")]
 pub struct Ident {
     pub label: String,
diff --git a/src/label.rs b/src/label.rs
index 129ab27e..700c0742 100644
--- a/src/label.rs
+++ b/src/label.rs
@@ -2,8 +2,6 @@
 //!
 //! 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 crate::eval::lazy::Thunk;
 use crate::position::{RawSpan, TermPos};
 use crate::types::{AbsType, Types};
@@ -234,7 +232,7 @@ pub mod ty_path {
 #[derive(Debug, Clone, PartialEq)]
 pub struct Label {
     /// The type checked by the original contract.
-    pub types: Rc<Types>,
+    pub types: Types,
     /// A string tag to be printed together with the error message.
     pub tag: String,
     /// The position of the original contract.
@@ -254,7 +252,7 @@ impl Label {
     /// Generate a dummy label for testing purpose.
     pub fn dummy() -> Label {
         Label {
-            types: Rc::new(Types(AbsType::Num())),
+            types: Types(AbsType::Num()),
             tag: "testing".to_string(),
             span: RawSpan {
                 src_id: Files::new().add("<test>", String::from("empty")),
@@ -268,21 +266,3 @@ impl Label {
         }
     }
 }
-
-impl Default for Label {
-    fn default() -> Label {
-        Label {
-            types: Rc::new(Types(AbsType::Dyn())),
-            tag: "".to_string(),
-            span: RawSpan {
-                src_id: Files::new().add("<null>", String::from("")),
-                start: 0.into(),
-                end: 1.into(),
-            },
-            arg_thunk: None,
-            arg_pos: TermPos::None,
-            polarity: true,
-            path: Vec::new(),
-        }
-    }
-}
diff --git a/src/parser/error.rs b/src/parser/error.rs
index 18e310d5..6d71bdf5 100644
--- a/src/parser/error.rs
+++ b/src/parser/error.rs
@@ -1,4 +1,5 @@
-use crate::{identifier::Ident, position::RawSpan};
+use crate::identifier::Ident;
+use crate::position::RawSpan;
 
 #[derive(Clone, PartialEq, Debug)]
 pub enum LexicalError {
@@ -18,19 +19,4 @@ pub enum ParseError {
     Lexical(LexicalError),
     /// Unbound type variable(s)
     UnboundTypeVariables(Vec<Ident>, RawSpan),
-    /// Illegal record literal in the uniterm syntax. In practice, this is a record with a
-    /// polymorphic tail that contains a construct that wasn't permitted inside a record type in
-    /// the original syntax. Typically, a field assignment:
-    ///
-    /// ```nickel
-    /// forall a. {foo : Num; a} // allowed
-    /// forall a. {foo : Num = 1; a} // InvalidUniRecord error: giving a value to foo is forbidden
-    /// ```
-    ///
-    /// See [RFC002](../../rfcs/002-merge-types-terms-syntax.md) for more details.
-    InvalidUniRecord(
-        RawSpan, /* illegal (in conjunction with a tail) construct position */
-        RawSpan, /* tail position */
-        RawSpan, /* whole record position */
-    ),
 }
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index ac237c61..322843df 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -82,8 +82,6 @@ pub enum NormalToken<'input> {
     QuestionMark,
     #[token(",")]
     Comma,
-    #[token(";")]
-    Semicolon,
     #[token(":")]
     Colon,
     #[token("$")]
@@ -282,10 +280,6 @@ pub enum NormalToken<'input> {
     RAngleBracket,
     #[token(">=")]
     GreaterOrEq,
-    #[token("[|")]
-    EnumOpen,
-    #[token("|]")]
-    EnumClose,
     #[regex("//[^\n]*")]
     LineComment,
 }
@@ -339,7 +333,7 @@ pub enum MultiStringToken<'input> {
     /// The other rules should be sufficient to match this as a double quote followed by a
     /// `CandidateInterpolation`, but if we omit this token, the lexer can fail unexpectedly on
     /// valid inputs because of #200.
-    #[regex("\"#+\\{")]
+    #[token("\"#+\\{")]
     QuotesCandidateInterpolation(&'input str),
     /// Token emitted by the modal lexer for the parser once it has decided that a `CandidateEnd` is
     /// an actual end token.
@@ -443,7 +437,7 @@ impl<'input> Lexer<'input> {
             //  `Normal`
             Some(ModalLexer::Normal(lexer)) => {
                 self.stack.push(ModeElt::Normal(self.count));
-                self.lexer = Some(morph(lexer));
+                self.lexer.replace(morph(lexer));
             }
             _ => panic!("lexer::enter_strlike"),
         }
@@ -463,11 +457,11 @@ impl<'input> Lexer<'input> {
         match self.lexer.take() {
             //count must be zero, and we do not push it on the stack
             Some(ModalLexer::Str(lexer)) => {
-                self.lexer = Some(ModalLexer::Normal(lexer.morph()));
+                self.lexer.replace(ModalLexer::Normal(lexer.morph()));
                 self.stack.push(ModeElt::Str);
             }
             Some(ModalLexer::MultiStr(lexer)) => {
-                self.lexer = Some(ModalLexer::Normal(lexer.morph()));
+                self.lexer.replace(ModalLexer::Normal(lexer.morph()));
                 self.stack.push(ModeElt::MultiStr(self.count));
             }
             _ => panic!("lexer::enter_normal"),
@@ -485,7 +479,7 @@ impl<'input> Lexer<'input> {
                     mode => panic!("lexer::leave_str (popped mode {:?})", mode),
                 };
 
-                self.lexer = Some(ModalLexer::Normal(lexer.morph()));
+                self.lexer.replace(ModalLexer::Normal(lexer.morph()));
             }
             _ => panic!("lexer::leave_str"),
         }
@@ -500,7 +494,7 @@ impl<'input> Lexer<'input> {
                     mode => panic!("lexer::leave_str (popped mode {:?})", mode),
                 };
 
-                self.lexer = Some(ModalLexer::Normal(lexer.morph()));
+                self.lexer.replace(ModalLexer::Normal(lexer.morph()));
             }
             _ => panic!("lexer::leave_str"),
         }
@@ -511,10 +505,10 @@ impl<'input> Lexer<'input> {
             Some(ModalLexer::Normal(lexer)) => {
                 // count must be 0
                 match self.stack.pop() {
-                    Some(ModeElt::Str) => self.lexer = Some(ModalLexer::Str(lexer.morph())),
+                    Some(ModeElt::Str) => self.lexer.replace(ModalLexer::Str(lexer.morph())),
                     Some(ModeElt::MultiStr(count)) => {
                         self.count = count;
-                        self.lexer = Some(ModalLexer::MultiStr(lexer.morph()))
+                        self.lexer.replace(ModalLexer::MultiStr(lexer.morph()))
                     }
                     mode => panic!("lexer::leave_normal (popped mode {:?})", mode),
                 };
@@ -572,36 +566,28 @@ impl<'input> Iterator for Lexer<'input> {
                 token = Some(MultiStr(MultiStringToken::Interpolation));
                 self.enter_normal();
             }
-            // We never lex something as a `MultiStringToken::Interpolation` directly, but rather
-            // generate it in this very function from other tokens. However, such a token could
-            // have still been buffered in the previous iteration, and can thus be matched here,
-            // which is why we need the case below.
-            Some(MultiStr(MultiStringToken::Interpolation)) => self.enter_normal(),
             // If we encouter a `QuotesCandidateInterpolation` token with the right number of
             // characters, we need to split it into two tokens:
-            // - a literal starting by a `"` followed by between 0 and k hashes `#`
-            // - an interpolation token
+            // - a simple `"` literal
+            // - a interpolation token
             // The interpolation token is put in the buffer such that it will be returned next
             // time.
-            //
-            // For example, in `m##""###{exp}"##m`, the `"###{` is a `QuotesCandidateInterpolation`
-            // which is split as a `"#` literal followed by an interpolation token.
             Some(MultiStr(MultiStringToken::QuotesCandidateInterpolation(s)))
-                if s.len() >= self.count =>
+                if s.len() == self.count =>
             {
-                let split_at = s.len() - self.count + 1;
                 let next_token = MultiStr(MultiStringToken::Interpolation);
                 let next_span = Range {
-                    start: span.start + split_at,
+                    start: span.start + 1,
                     end: span.end,
                 };
-                self.buffer = Some((next_token, next_span));
+                self.buffer.replace((next_token, next_span));
 
-                token = Some(MultiStr(MultiStringToken::Literal(&s[0..split_at])));
+                token = Some(MultiStr(MultiStringToken::Literal(&s[0..1])));
                 span = Range {
                     start: span.start,
-                    end: span.start + split_at,
+                    end: span.start + 1,
                 };
+                self.enter_normal();
             }
             // Otherwise, it is just part of the string, so we transform the token into a
             // `FalseInterpolation` one
@@ -651,7 +637,7 @@ impl<'input> Iterator for Lexer<'input> {
             // Ignore comment
             Some(Normal(NormalToken::LineComment)) => return self.next(),
             _ => (),
-        };
+        }
 
         token.map(|t| Ok((span.start, t, span.end)))
     }
diff --git a/src/parser/mod.rs b/src/parser/mod.rs
index d01afdf0..7ffbf90f 100644
--- a/src/parser/mod.rs
+++ b/src/parser/mod.rs
@@ -11,11 +11,9 @@ lalrpop_mod!(
 
 pub mod error;
 pub mod lexer;
-pub mod uniterm;
-pub mod utils;
-
 #[cfg(test)]
 mod tests;
+pub mod utils;
 
 /// Either a term or a toplevel let declaration.
 pub enum ExtendedTerm {
diff --git a/src/parser/uniterm.rs b/src/parser/uniterm.rs
deleted file mode 100644
index cf09bb1b..00000000
--- a/src/parser/uniterm.rs
+++ /dev/null
@@ -1,411 +0,0 @@
-//! Additional AST nodes for the common UniTerm syntax (see RFC002 for more details).
-use super::*;
-use error::ParseError;
-use utils::{build_record, elaborate_field_path, FieldPath, FieldPathElem};
-
-use crate::{
-    position::{RawSpan, TermPos},
-    term::{Contract, MergePriority, MetaValue, RecordAttrs, RichTerm, SharedTerm, Term},
-    types::{AbsType, Types, UnboundTypeVariableError},
-};
-
-use std::{borrow::Cow, collections::HashSet, convert::TryFrom};
-
-/// A node of the uniterm AST. We only define new variants for those constructs that are common to
-/// types and terms. Otherwise, we piggyback on the existing ASTs to avoid duplicating methods and
-/// type definitions.
-///
-/// During parsing, some constructs are common to both terms and types, such as variables or record
-/// literals ([`UniRecord`]s). They may be the source of ambiguities in the grammar, if we add two
-/// different derivation for them. This happens inside rules that accepts both a term and and a
-/// type, say the operands of an arrow `lhs -> rhs`. Take for example `lhs` to be a variable `a`.
-/// It's hard not to end up having two possible derivation for `a`, one going first through term
-/// rules and then types rules (a custom contract `#a` in the old syntax), and vice-versa (a type
-/// variable `a` in the old syntax).
-///
-/// To avoid the issue, we parse the source as a `UniTermNode`s, and give only one possible
-/// derivation - we will continue with the variable example in the following - through the parsing
-/// rules. As long as we can't decide yet how to see this variable, we keep it as a
-/// `UniTermNode::Var`.
-///
-/// As soon as this variable is used in a compound expression, the top-level rule tells us how to
-/// translate it. For example, if we see an arrow `a -> Num`, then we will convert it to a type
-/// variable, and return `UniTermNode::Types(AbsType::Arrow(..))` (there is actually a subtelty:
-/// see [`fix_type_vars`], but let's ignore it here). If, on the other hand, we enter the rule for
-/// an infix operator as in `a + 1`, `a` will be converted to a `Term::Var` and the resulting
-/// uniterm will be `UniTermNode::Term(Term::Op2(..))`.
-pub enum UniTermNode {
-    /// A variable. Can refer both to a term variable or a type variable.
-    Var(Ident),
-    /// A record. Can refer both to a record literal or a record type.
-    Record(UniRecord),
-    /// A uniterm that has been determined to be a term.
-    Term(RichTerm),
-    /// A uniterm that has been determined to be a type.
-    Types(Types),
-}
-
-/// A uniterm with positional information.
-pub struct UniTerm {
-    node: UniTermNode,
-    pos: TermPos,
-}
-
-impl From<UniTermNode> for UniTerm {
-    fn from(node: UniTermNode) -> Self {
-        UniTerm {
-            node,
-            pos: TermPos::None,
-        }
-    }
-}
-
-impl UniTerm {
-    pub fn with_pos(mut self, pos: TermPos) -> Self {
-        self.pos = pos;
-        self
-    }
-}
-
-impl TryFrom<UniTerm> for Types {
-    type Error = ParseError;
-
-    fn try_from(ut: UniTerm) -> Result<Self, ParseError> {
-        match ut.node {
-            UniTermNode::Var(id) => Ok(Types(AbsType::Var(id))),
-            UniTermNode::Record(r) => Types::try_from(r),
-            UniTermNode::Types(ty) => Ok(ty),
-            UniTermNode::Term(rt) => Ok(Types(AbsType::Flat(rt))),
-        }
-    }
-}
-
-impl TryFrom<UniTerm> for RichTerm {
-    type Error = ParseError;
-
-    fn try_from(ut: UniTerm) -> Result<Self, ParseError> {
-        let UniTerm { node, pos } = ut;
-        let rt = match node {
-            UniTermNode::Var(id) => RichTerm::new(Term::Var(id), pos),
-            UniTermNode::Record(r) => RichTerm::try_from(r)?,
-            UniTermNode::Types(ty) => {
-                ty.contract().map_err(|UnboundTypeVariableError(id)| {
-                    // We unwrap the position of the identifier, which must be set at this stage of parsing
-                    let pos = id.pos;
-                    ParseError::UnboundTypeVariables(vec![id], pos.unwrap())
-                })?
-            }
-            UniTermNode::Term(rt) => rt,
-        };
-
-        Ok(rt.with_pos(pos))
-    }
-}
-
-impl From<RichTerm> for UniTerm {
-    fn from(rt: RichTerm) -> Self {
-        let pos = rt.pos;
-
-        UniTerm {
-            node: UniTermNode::Term(rt),
-            pos,
-        }
-    }
-}
-
-impl From<Term> for UniTerm {
-    fn from(t: Term) -> Self {
-        Self::from(RichTerm::from(t))
-    }
-}
-
-impl From<Types> for UniTerm {
-    fn from(ty: Types) -> Self {
-        UniTerm {
-            node: UniTermNode::Types(ty),
-            pos: TermPos::None,
-        }
-    }
-}
-
-impl From<UniRecord> for UniTerm {
-    fn from(ur: UniRecord) -> Self {
-        let pos = ur.pos;
-
-        UniTerm {
-            node: UniTermNode::Record(ur),
-            pos,
-        }
-    }
-}
-
-/// A record in the `UniTerm` syntax.
-#[derive(Clone)]
-pub struct UniRecord {
-    pub fields: Vec<(FieldPath, RichTerm)>,
-    pub tail: Option<(Types, TermPos)>,
-    pub attrs: RecordAttrs,
-    pub pos: TermPos,
-    /// The position of the final ellipsis `..`, if any. Used for error reporting. `pos_ellipsis`
-    /// must be different from `TermPos::None` if and only if `attrs.open` is `true`.
-    pub pos_ellipsis: TermPos,
-}
-
-/// Error indicating that a construct is not allowed when trying to interpret an `UniRecord` as a
-/// record type in a strict way. See [`UniRecord::into_type_strict`]. Hold the position of the
-/// illegal construct.
-pub struct InvalidRecordTypeError(pub TermPos);
-
-impl UniRecord {
-    /// Try to convert a `UniRecord` to a type. The strict part means that the `UniRecord` must be
-    /// a plain record type, uniquely containing fields of the form `fields: Type`. Currently, it
-    /// doesn't support the field path syntax: `{foo.bar.baz : Type}.into_type_strict()` returns an
-    /// `Err`.
-    pub fn into_type_strict(self) -> Result<Types, InvalidRecordTypeError> {
-        // An open record (with an ellipsis `..` at the end) can't be translated to a record type.
-        // `pos_ellipsis` should be set iff `attrs.open` is true.
-        debug_assert!((self.pos_ellipsis == TermPos::None) == !self.attrs.open);
-
-        if let Some(raw_span) = self.pos_ellipsis.into_opt() {
-            return Err(InvalidRecordTypeError(TermPos::Original(raw_span)));
-        }
-
-        let ty = self
-            .fields
-            .into_iter()
-            // Because we build row types as a linked list by folding on the original iterator, the
-            // order of identifiers is reversed. This not a big deal but it's less confusing to the
-            // user to print them in the original order for error reporting.
-            .rev()
-            .try_fold(
-                self.tail
-                    .map(|(tail, _)| tail)
-                    .unwrap_or(Types(AbsType::RowEmpty())),
-                |acc, (mut path, rt)| {
-                    // We don't support compound paths for types, yet.
-                    if path.len() > 1 {
-                        let span = path
-                            .into_iter()
-                            .map(|path_elem| match path_elem {
-                                FieldPathElem::Ident(id) => id.pos.into_opt(),
-                                FieldPathElem::Expr(rt) => rt.pos.into_opt(),
-                            })
-                            .reduce(|acc, pos| {
-                                acc.zip(pos)
-                                    .and_then(|(acc, span)| RawSpan::fuse(acc, span))
-                            })
-                            .flatten();
-
-                        Err(InvalidRecordTypeError(
-                            span.map_or(TermPos::None, TermPos::Original),
-                        ))
-                    } else {
-                        let elem = path.pop().unwrap();
-                        match elem {
-                            FieldPathElem::Ident(id) => {
-                                // At parsing stage, all `Rc`s must be 1-counted. We can thus call
-                                // `into_owned()` without risking to actually clone anything.
-                                match rt.term.into_owned() {
-                                    Term::MetaValue(MetaValue {
-                                        doc: None,
-                                        types: Some(ctrt),
-                                        contracts,
-                                        priority: MergePriority::Normal,
-                                        value: None,
-                                    }) if contracts.is_empty() => Ok(Types(AbsType::RowExtend(
-                                        id,
-                                        Some(Box::new(ctrt.types)),
-                                        Box::new(acc),
-                                    ))),
-                                    _ => {
-                                        // Position of identifiers must always be set at this stage
-                                        // (parsing)
-                                        let span_id = id.pos.unwrap();
-                                        let term_pos = rt.pos.into_opt().unwrap_or(span_id);
-                                        Err(InvalidRecordTypeError(TermPos::Original(
-                                            RawSpan::fuse(span_id, term_pos).unwrap(),
-                                        )))
-                                    }
-                                }
-                            }
-                            FieldPathElem::Expr(rt) => Err(InvalidRecordTypeError(rt.pos)),
-                        }
-                    }
-                },
-            )?;
-        Ok(Types(AbsType::StaticRecord(Box::new(ty))))
-    }
-
-    pub fn with_pos(mut self, pos: TermPos) -> Self {
-        self.pos = pos;
-        self
-    }
-}
-
-impl TryFrom<UniRecord> for RichTerm {
-    type Error = ParseError;
-
-    /// Convert a `UniRecord` to a term. If the `UniRecord` has a tail, it is first interpreted as
-    /// a type and then converted to a contract. Otherwise it is interpreted as a record directly.
-    /// Fail if the `UniRecord` has a tail but isn't syntactically a record type either. Elaborate
-    /// field paths `foo.bar = value` to the expanded form `{foo = {bar = value}}`.
-    ///
-    /// We also fix the type variables of the type appearing inside annotations (see
-    /// [`fix_type_vars`]).
-    fn try_from(ur: UniRecord) -> Result<Self, ParseError> {
-        let pos = ur.pos;
-
-        let result = if let Some((_, tail_pos)) = ur.tail {
-            ur.into_type_strict()
-                // We unwrap all positions: at this stage of the parsing, they must all be set
-                .map_err(|InvalidRecordTypeError(pos)| {
-                    ParseError::InvalidUniRecord(pos.unwrap(), tail_pos.unwrap(), pos.unwrap())
-                })
-                .and_then(|mut ty| {
-                    fix_type_vars(&mut ty);
-                    ty.contract().map_err(|UnboundTypeVariableError(id)| {
-                        ParseError::UnboundTypeVariables(vec![id], pos.unwrap())
-                    })
-                })
-        } else {
-            let UniRecord { fields, attrs, .. } = ur;
-            let elaborated = fields.into_iter().map(|(path, mut rt)| {
-                fix_field_types(&mut rt);
-                elaborate_field_path(path, rt)
-            });
-
-            Ok(RichTerm::from(build_record(elaborated, attrs)))
-        };
-
-        result.map(|rt| rt.with_pos(pos))
-    }
-}
-
-impl TryFrom<UniRecord> for Types {
-    type Error = ParseError;
-
-    /// Convert a `UniRecord` to a type. If the `UniRecord` has a tail, it is interpreted strictly
-    /// as a type and fail if it isn't a plain record type. Otherwise, we first try to interpret it
-    /// as a plain record type, and if that doesn't work, we interpret it as a term and wrap it
-    /// back as a user-defined contract.
-    fn try_from(ur: UniRecord) -> Result<Self, ParseError> {
-        let pos = ur.pos;
-
-        if let Some((_, tail_pos)) = ur.tail {
-            ur.into_type_strict()
-                .map_err(|InvalidRecordTypeError(illegal_pos)| {
-                    ParseError::InvalidUniRecord(
-                        illegal_pos.unwrap(),
-                        tail_pos.unwrap(),
-                        pos.unwrap(),
-                    )
-                })
-        } else {
-            ur.clone()
-                .into_type_strict()
-                .or_else(|_| RichTerm::try_from(ur).map(|rt| Types(AbsType::Flat(rt))))
-        }
-    }
-}
-
-/// Post-process a type at the right hand side of an annotation by replacing each unbound type
-/// variable by a term variable with the same identifier seen as a custom contract
-/// (`AbsType::Var(id)` to `AbsType::Flat(Term::Var(id))`).
-///
-/// Since parsing is done bottom-up, and given the specification of the uniterm syntax for
-/// variables occurring in types, we often can't know right away if a such a variable occurrence
-/// will eventually be a type variable or a term variable seen as a custom contract.
-///
-/// Take for example `a -> b`. At this stage, `a` and `b` could be both variables referring to a
-/// contract (e.g. in `x | a -> b`) or a type variable (e.g. in `x | forall a b. a -> b`),
-/// depending on enclosing `forall`s. To handle both cases, we initially parse all variables inside
-/// types as type variables. When reaching the right-hand side of an annotation, because `forall`s
-/// can only bind locally in a type, we can then decide the actual nature of each occurrence. We
-/// thus recurse into the newly constructed type to change those type variables that are not
-/// actually bound by a `forall` to be term variables. This is the role of `fix_type_vars()`.
-///
-/// Once again because `forall`s only bind variables locally, and don't bind inside contracts, we
-/// don't have to recurse into contracts and this pass will only visit each node of the AST at most
-/// once in total.
-///
-/// There is one subtlety with unirecords, though. A unirecord can still be in interpreted as a
-/// record type later. Take the following example:
-///
-/// ```nickel
-/// let mk_pair : forall a b. a -> b -> {fst: a, snd: b} = <exp>
-/// ```
-///
-/// Since this unirecord will eventually be interpreted as a record type, we can't know yet when
-/// parsing `fst: a` if `a` will be a type variable or a term variable (while, for all other
-/// constructs, an annotation is a boundary that `forall` binders can't cross). In this example,
-/// there is indeed an enclosing forall binding `a`. With unirecords, before fixing type variables,
-/// we have to wait until we eventually convert the unirecord to a term (in which case we fix all the
-/// top-level annotations) or a type (in which case we do nothing: the enclosing type will trigger
-/// the fix once it's fully constructed). Fixing a unirecord prior to a conversion to a term is
-/// done by [`fix_fields_types`].
-pub fn fix_type_vars(ty: &mut Types) {
-    fn fix_type_vars_aux(ty: &mut Types, mut bound_vars: Cow<HashSet<Ident>>) {
-        match ty.0 {
-            AbsType::Dyn()
-            | AbsType::Num()
-            | AbsType::Bool()
-            | AbsType::Str()
-            | AbsType::Sym()
-            | AbsType::Flat(_)
-            | AbsType::RowEmpty() => (),
-            AbsType::Arrow(ref mut s, ref mut t) => {
-                fix_type_vars_aux(s.as_mut(), Cow::Borrowed(bound_vars.as_ref()));
-                fix_type_vars_aux(t.as_mut(), bound_vars);
-            }
-            AbsType::Var(ref mut id) => {
-                if !bound_vars.contains(id) {
-                    let id = std::mem::take(id);
-                    let pos = id.pos;
-                    ty.0 = AbsType::Flat(RichTerm::new(Term::Var(id), pos));
-                }
-            }
-            AbsType::Forall(ref id, ref mut ty) => {
-                bound_vars.to_mut().insert(id.clone());
-                fix_type_vars_aux(&mut *ty, bound_vars);
-            }
-            AbsType::RowExtend(_, ref mut ty_opt, ref mut tail) => {
-                if let Some(ref mut ty) = *ty_opt {
-                    fix_type_vars_aux(ty.as_mut(), Cow::Borrowed(bound_vars.as_ref()));
-                }
-
-                // We don't touch a row tail that is a type variable, because the typechecker
-                // relies on row types being well-formed, which the parser must ensure.
-                // Well-formedness requires that only type variables and `Dyn` may appear in a row
-                // tail position, so we don't turn such variables into term variables (having a
-                // contract in tail position doesn't make sense, in the current model at least,
-                // both for typechecking and at evaluation).
-                if !matches!((**tail).0, AbsType::Var(_)) {
-                    fix_type_vars_aux(tail.as_mut(), bound_vars);
-                }
-            }
-            AbsType::DynRecord(ref mut ty)
-            | AbsType::List(ref mut ty)
-            | AbsType::Enum(ref mut ty)
-            | AbsType::StaticRecord(ref mut ty) => fix_type_vars_aux(ty.as_mut(), bound_vars),
-        }
-    }
-
-    fix_type_vars_aux(ty, Cow::Owned(HashSet::new()))
-}
-
-/// Fix the type variables of types appearing as annotations of record fields. See
-/// [`fix_type_vars`].
-pub fn fix_field_types(rt: &mut RichTerm) {
-    match SharedTerm::make_mut(&mut rt.term) {
-        Term::MetaValue(ref mut m) => {
-            if let Some(Contract { ref mut types, .. }) = m.types {
-                fix_type_vars(types);
-            }
-
-            for ctr in m.contracts.iter_mut() {
-                fix_type_vars(&mut ctr.types);
-            }
-        }
-        _ => (),
-    }
-}
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index 196c39ac..73471720 100644
--- a/src/parser/utils.rs
+++ b/src/parser/utils.rs
@@ -1,9 +1,8 @@
 //! Various helpers and companion code for the parser are put here to keep the grammar definition
 //! uncluttered.
 use std::collections::hash_map::Entry;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 use std::fmt::Debug;
-use std::rc::Rc;
 
 use codespan::FileId;
 
@@ -11,9 +10,10 @@ use crate::{
     identifier::Ident,
     label::Label,
     mk_app, mk_fun,
+    parser::error::ParseError,
     position::{RawSpan, TermPos},
     term::{make as mk_term, BinaryOp, MetaValue, RecordAttrs, RichTerm, StrChunk, Term, UnaryOp},
-    types::Types,
+    types::{AbsType, Types},
 };
 
 /// Distinguish between the standard string separators `"`/`"` and the multi-line string separators
@@ -43,8 +43,6 @@ pub enum FieldPathElem {
     Expr(RichTerm),
 }
 
-pub type FieldPath = Vec<FieldPathElem>;
-
 /// A string chunk literal atom, being either a string or a single char.
 ///
 /// Because of the way the lexer handles escaping and interpolation, a contiguous static string
@@ -58,7 +56,7 @@ pub enum ChunkLiteralPart<'input> {
 /// The last field of a record, that can either be a normal field declaration or an ellipsis.
 #[derive(Clone, Debug)]
 pub enum RecordLastField {
-    Field((FieldPath, RichTerm)),
+    Field((FieldPathElem, RichTerm)),
     Ellipsis,
 }
 
@@ -304,7 +302,7 @@ pub fn mk_pos(src_id: FileId, l: usize, r: usize) -> TermPos {
 /// Same as `mk_span`, but for labels.
 pub fn mk_label(types: Types, src_id: FileId, l: usize, r: usize) -> Label {
     Label {
-        types: Rc::new(types),
+        types,
         tag: String::new(),
         span: mk_span(src_id, l, r),
         arg_thunk: None,
@@ -536,3 +534,64 @@ pub fn strip_indent_doc(doc: String) -> String {
         .next()
         .expect("expected non-empty chunks after indentation of documentation")
 }
+
+/// Recursively checks for unbound type variables in a type
+pub fn check_unbound(types: &Types, span: RawSpan) -> Result<(), ParseError> {
+    // heavy lifting function, recurses into a type expression and returns a set of unbound vars
+    fn find_unbound_vars(types: &Types, unbound_set: &mut HashSet<Ident>) {
+        match &types.0 {
+            AbsType::Var(ident) => {
+                unbound_set.insert(ident.clone());
+            }
+            AbsType::Forall(ident, ty) => {
+                // forall needs a "scoped" set for the variables in its nodes
+                let mut forall_unbound_vars = HashSet::new();
+                find_unbound_vars(ty, &mut forall_unbound_vars);
+
+                forall_unbound_vars.remove(ident);
+
+                // once the forall vars are recursed into and analyzed, the parent set and
+                // the forall set are merged
+                unbound_set.extend(forall_unbound_vars);
+            }
+            AbsType::Arrow(s, t) => {
+                find_unbound_vars(s, unbound_set);
+                find_unbound_vars(t, unbound_set);
+            }
+            AbsType::DynRecord(ty)
+            | AbsType::StaticRecord(ty)
+            | AbsType::List(ty)
+            | AbsType::Enum(ty) => {
+                find_unbound_vars(ty, unbound_set);
+            }
+            AbsType::RowExtend(_, opt_ty, ty) => {
+                if let Some(ty) = opt_ty {
+                    find_unbound_vars(ty, unbound_set);
+                }
+
+                find_unbound_vars(ty, unbound_set);
+            }
+            AbsType::Dyn()
+            | AbsType::Bool()
+            | AbsType::Num()
+            | AbsType::Str()
+            | AbsType::Sym()
+            | AbsType::Flat(_)
+            | AbsType::RowEmpty() => {}
+        }
+    }
+
+    let mut unbound_set: HashSet<Ident> = HashSet::new();
+
+    // recurse into type and find unbound type vars
+    find_unbound_vars(types, &mut unbound_set);
+
+    if !unbound_set.is_empty() {
+        return Err(ParseError::UnboundTypeVariables(
+            unbound_set.into_iter().collect(),
+            span,
+        ));
+    }
+
+    Ok(())
+}
diff --git a/src/position.rs b/src/position.rs
index 5cc3107d..9f5fb0d1 100644
--- a/src/position.rs
+++ b/src/position.rs
@@ -4,7 +4,7 @@
 //! raw byte indices.  They are prefixed with Raw to differentiate them from codespan's types and
 //! indicate that they do not store human friendly data like lines and columns.
 use codespan::{ByteIndex, FileId};
-use std::cmp::{max, min, Ordering};
+use std::cmp::Ordering;
 
 /// A position identified by a byte offset in a file.
 #[derive(Debug, Clone, Copy, Eq, PartialEq)]
@@ -23,22 +23,6 @@ pub struct RawSpan {
     pub end: ByteIndex,
 }
 
-impl RawSpan {
-    /// Fuse two spans if they are from the same source file. The resulting span is the smallest
-    /// span that contain both `span1` and `span2`.
-    pub fn fuse(span1: RawSpan, span2: RawSpan) -> Option<RawSpan> {
-        if span1.src_id == span2.src_id {
-            Some(RawSpan {
-                src_id: span1.src_id,
-                start: min(span1.start, span2.start),
-                end: max(span1.end, span2.end),
-            })
-        } else {
-            None
-        }
-    }
-}
-
 /// The position span of a term.
 #[derive(Debug, Clone, Copy, Eq, PartialEq, Hash)]
 pub enum TermPos {
@@ -52,12 +36,6 @@ pub enum TermPos {
     None,
 }
 
-impl Default for TermPos {
-    fn default() -> Self {
-        TermPos::None
-    }
-}
-
 impl TermPos {
     /// Apply a transformation to the inner position, if any.
     pub fn map<F: FnOnce(RawSpan) -> RawSpan>(self, f: F) -> Self {
diff --git a/src/repl/mod.rs b/src/repl/mod.rs
index 210ca64c..08c76699 100644
--- a/src/repl/mod.rs
+++ b/src/repl/mod.rs
@@ -118,60 +118,56 @@ impl ReplImpl {
             return Err(parse_errs.into());
         }
 
-        // Because we don't use the cache for input, we have to perform recursive import
-        // resolution/typechecking/transformation by ourselves.
-        //
-        // `id` must be set to `None` for normal lets and to `Some(id_)` for top-level lets. In the
-        // latter case, we need to update the current type environment before doing program
-        // transformations in the case of a top-level let.
-        fn prepare(
-            repl_impl: &mut ReplImpl,
-            id: Option<Ident>,
-            t: RichTerm,
-        ) -> Result<RichTerm, Error> {
-            let (t, pending) = import_resolution::resolve_imports(t, &mut repl_impl.cache)?;
-            for id in &pending {
-                repl_impl.cache.resolve_imports(*id).unwrap();
-            }
-
-            typecheck::type_check_in_env(&t, &repl_impl.env.type_env, &repl_impl.cache)?;
-
-            if let Some(id) = id {
-                typecheck::Envs::env_add(
-                    &mut repl_impl.env.type_env,
-                    id.clone(),
-                    &t,
-                    &repl_impl.cache,
-                );
-            }
-
-            for id in &pending {
-                repl_impl
-                    .cache
-                    .typecheck(*id, &repl_impl.init_type_env)
-                    .map_err(|cache_err| {
-                        cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
-                    })?;
-            }
-
-            let t = transform::transform(t).map_err(|err| Error::ParseErrors(err.into()))?;
-            for id in &pending {
-                repl_impl
-                    .cache
-                    .transform(*id)
-                    .unwrap_or_else(|_| panic!("repl::eval_(): expected imports to be parsed"));
-            }
-
-            Ok(t)
-        }
-
         match term {
+            // Because we don't use the cache for input, we have to perform recursive import
+            // resolution/typechecking/transformation by oursleves.
             ExtendedTerm::RichTerm(t) => {
-                let t = prepare(self, None, t)?;
+                let (t, pending) = import_resolution::resolve_imports(t, &mut self.cache)?;
+                for id in &pending {
+                    self.cache.resolve_imports(*id).unwrap();
+                }
+
+                typecheck::type_check_in_env(&t, &self.env.type_env, &self.cache)?;
+                for id in &pending {
+                    self.cache
+                        .typecheck(*id, &self.init_type_env)
+                        .map_err(|cache_err| {
+                            cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
+                        })?;
+                }
+
+                let t = transform::transform(t);
+                for id in &pending {
+                    self.cache
+                        .transform(*id)
+                        .unwrap_or_else(|_| panic!("repl::eval_(): expected imports to be parsed"));
+                }
+
                 Ok(eval_function(t, &self.env.eval_env, &mut self.cache)?.into())
             }
             ExtendedTerm::ToplevelLet(id, t) => {
-                let t = prepare(self, Some(id.clone()), t)?;
+                let (t, pending) = import_resolution::resolve_imports(t, &mut self.cache)?;
+                for id in &pending {
+                    self.cache.resolve_imports(*id).unwrap();
+                }
+
+                typecheck::type_check_in_env(&t, &self.env.type_env, &self.cache)?;
+                typecheck::Envs::env_add(&mut self.env.type_env, id.clone(), &t, &self.cache);
+                for id in &pending {
+                    self.cache
+                        .typecheck(*id, &self.init_type_env)
+                        .map_err(|cache_err| {
+                            cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
+                        })?;
+                }
+
+                let t = transform::transform(t);
+                for id in &pending {
+                    self.cache
+                        .transform(*id)
+                        .unwrap_or_else(|_| panic!("repl::eval_(): expected imports to be parsed"));
+                }
+
                 let local_env = self.env.eval_env.clone();
                 eval::env_add(&mut self.env.eval_env, id.clone(), t, local_env);
                 Ok(EvalResult::Bound(id))
diff --git a/src/term.rs b/src/term.rs
index 1d66e0fc..03a8c340 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -21,7 +21,7 @@ use crate::identifier::Ident;
 use crate::label::Label;
 use crate::match_sharedterm;
 use crate::position::TermPos;
-use crate::types::{AbsType, Types, UnboundTypeVariableError};
+use crate::types::{AbsType, Types};
 use codespan::FileId;
 use serde::{Deserialize, Serialize};
 use std::collections::HashMap;
@@ -910,7 +910,7 @@ impl fmt::Display for NAryOp {
 }
 
 #[derive(Copy, Clone)]
-pub enum TraverseOrder {
+pub enum TraverseMethod {
     TopDown,
     BottomUp,
 }
@@ -952,21 +952,21 @@ impl RichTerm {
         self
     }
 
-    /// Apply a transformation on a whole term by mapping a faillible function `f` on each node in
-    /// manner as prescribed by the order.
+    /// Apply a transformation on a whole term by mapping a function `f` on each node in
+    /// manner defined by the method.
     /// `f` may return a generic error `E` and use the state `S` which is passed around.
     pub fn traverse<F, S, E>(
         self,
         f: &mut F,
         state: &mut S,
-        method: TraverseOrder,
+        method: TraverseMethod,
     ) -> Result<RichTerm, E>
     where
         F: FnMut(RichTerm, &mut S) -> Result<RichTerm, E>,
     {
         let rt = match method {
-            TraverseOrder::TopDown => f(self, state)?,
-            TraverseOrder::BottomUp => self,
+            TraverseMethod::TopDown => f(self, state)?,
+            TraverseMethod::BottomUp => self,
         };
         let pos = rt.pos;
 
@@ -1168,8 +1168,8 @@ impl RichTerm {
         };
 
         match method {
-            TraverseOrder::TopDown => Ok(result),
-            TraverseOrder::BottomUp => f(result, state),
+            TraverseMethod::TopDown => Ok(result),
+            TraverseMethod::BottomUp => f(result, state),
         }
     }
 }
@@ -1349,7 +1349,7 @@ pub mod make {
         I: Into<Ident>,
     {
         match pat.into() {
-            d @ (Destruct::Record { .. } | Destruct::List { .. }) => {
+            d @ (Destruct::Record(..) | Destruct::List(_)) => {
                 Term::LetPattern(id.map(|i| i.into()), d, t1.into(), t2.into()).into()
             }
             Destruct::Empty => {
@@ -1394,14 +1394,14 @@ pub mod make {
         Term::OpN(op, args.into_iter().map(T::into).collect()).into()
     }
 
-    pub fn assume<T>(types: Types, l: Label, t: T) -> Result<RichTerm, UnboundTypeVariableError>
+    pub fn assume<T>(types: Types, l: Label, t: T) -> RichTerm
     where
         T: Into<RichTerm>,
     {
-        Ok(mk_app!(
-            op2(BinaryOp::Assume(), types.contract()?, Term::Lbl(l)),
+        mk_app!(
+            op2(BinaryOp::Assume(), types.contract(), Term::Lbl(l)),
             t.into()
-        ))
+        )
     }
 
     pub fn string<S>(s: S) -> RichTerm
diff --git a/src/transform/apply_contracts.rs b/src/transform/apply_contracts.rs
index b4162d36..ab1f02fd 100644
--- a/src/transform/apply_contracts.rs
+++ b/src/transform/apply_contracts.rs
@@ -8,42 +8,37 @@
 //!
 //! It must be run before `share_normal_form` to avoid rechecking contracts each time the inner
 //! value is unwrapped.
-use crate::{
-    match_sharedterm, mk_app,
-    term::{make as mk_term, BinaryOp, RichTerm, Term},
-    types::UnboundTypeVariableError,
-};
+use crate::term::{make as mk_term, BinaryOp, RichTerm, Term};
+use crate::{match_sharedterm, mk_app};
 
 /// If the top-level node of the AST is a meta-value, apply the meta-value's contracts to the inner
 /// value.  Otherwise, return the term unchanged.
-/// Fail if an unbound type variable is encountered.
-pub fn transform_one(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
+pub fn transform_one(rt: RichTerm) -> RichTerm {
     let pos = rt.pos;
-    let result = match_sharedterm! {rt.term,
+    match_sharedterm! {rt.term,
         with {
             Term::MetaValue(meta) if meta.value.is_some() => {
                 let mut meta = meta;
                 let pos_inh = pos.into_inherited();
-                let inner = meta.types.iter().chain(meta.contracts.iter()).try_fold(
+                let inner = meta.types.iter().chain(meta.contracts.iter()).fold(
                     meta.value.take().unwrap(),
                     |acc, ctr| {
-                        Ok(mk_app!(
+                        mk_app!(
                             mk_term::op2(
                                 BinaryOp::Assume(),
-                                ctr.types.contract()?,
+                                ctr.types.contract(),
                                 Term::Lbl(ctr.label.clone())
                             )
                             .with_pos(pos_inh),
                             acc
                         )
-                        .with_pos(pos_inh))
+                        .with_pos(pos_inh)
                     },
-                )?;
+                );
 
                 meta.value.replace(inner);
                 RichTerm::new(Term::MetaValue(meta), pos)
             }
         } else rt
-    };
-    Ok(result)
+    }
 }
diff --git a/src/transform/desugar_destructuring.rs b/src/transform/desugar_destructuring.rs
index 5dc99200..8b3d3858 100644
--- a/src/transform/desugar_destructuring.rs
+++ b/src/transform/desugar_destructuring.rs
@@ -133,24 +133,9 @@ pub fn desugar(rt: RichTerm) -> RichTerm {
 /// generate a fresh variable.
 fn bind_open_field(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
     let (matches, var) = match pat {
-        Destruct::Record {
-            matches,
-            open: true,
-            rest: Some(x),
-            ..
-        } => (matches, x.clone()),
-        Destruct::Record {
-            matches,
-            open: true,
-            rest: None,
-            ..
-        } => (matches, super::fresh_var()),
-        Destruct::Record {
-            open: false,
-            rest: None,
-            ..
-        }
-        | Destruct::Empty => return body,
+        Destruct::Record(matches, true, Some(x)) => (matches, x.clone()),
+        Destruct::Record(matches, true, None) => (matches, super::fresh_var()),
+        Destruct::Record(_, false, None) | Destruct::Empty => return body,
         _ => panic!("A closed pattern can not have a rest binding"),
     };
     Term::Let(
@@ -171,7 +156,7 @@ fn bind_open_field(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
 fn destruct_term(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
     let pos = body.pos;
     match pat {
-        Destruct::Record { matches, .. } => matches.iter().fold(body, move |t, m| match m {
+        Destruct::Record(matches, ..) => matches.iter().fold(body, move |t, m| match m {
             Match::Simple(id, _) => RichTerm::new(
                 Term::Let(
                     id.clone(),
diff --git a/src/transform/import_resolution.rs b/src/transform/import_resolution.rs
index f79a8505..8b013f41 100644
--- a/src/transform/import_resolution.rs
+++ b/src/transform/import_resolution.rs
@@ -3,7 +3,7 @@
 //! identifier directly.
 use super::ImportResolver;
 use crate::error::ImportError;
-use crate::term::{RichTerm, Term, TraverseOrder};
+use crate::term::{RichTerm, Term, TraverseMethod};
 use codespan::FileId;
 use std::path::PathBuf;
 
@@ -55,7 +55,7 @@ where
             Ok(rt)
         },
         &mut state,
-        TraverseOrder::BottomUp,
+        TraverseMethod::BottomUp,
     )?;
 
     Ok((transformed, stack))
diff --git a/src/transform/mod.rs b/src/transform/mod.rs
index 3c918888..c27467b2 100644
--- a/src/transform/mod.rs
+++ b/src/transform/mod.rs
@@ -1,12 +1,9 @@
 //! Various post transformations of nickel code.
-use crate::{
-    cache::ImportResolver,
-    eval::{lazy::Thunk, Closure, Environment, IdentKind},
-    identifier::Ident,
-    term::{Contract, RichTerm, Term, TraverseOrder},
-    types::{AbsType, Types, UnboundTypeVariableError},
-};
-
+use crate::cache::ImportResolver;
+use crate::eval::{lazy::Thunk, Closure, Environment, IdentKind};
+use crate::identifier::Ident;
+use crate::term::{Contract, RichTerm, Term, TraverseMethod};
+use crate::types::{AbsType, Types};
 use simple_counter::*;
 
 generate_counter!(FreshVarCounter, usize);
@@ -22,29 +19,30 @@ pub mod share_normal_form;
 /// Do not perform transformations on the imported files. If needed, either do it yourself using
 /// pending imports returned by [`resolve_imports`](../fn.resolve_imports.html) or use the
 /// [`Cache`](../../cache/struct.Cache.html)
-pub fn transform(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
-    let rt = rt.traverse(
-        &mut |rt: RichTerm, _| -> Result<RichTerm, UnboundTypeVariableError> {
-            // before anything, we have to desugar the syntax
-            let rt = desugar_destructuring::transform_one(rt);
-            // We need to do contract generation before wrapping stuff in variables
-            let rt = apply_contracts::transform_one(rt)?;
-            Ok(rt)
-        },
-        &mut (),
-        TraverseOrder::TopDown,
-    )?;
-
-    Ok(rt
+pub fn transform(rt: RichTerm) -> RichTerm {
+    let rt = rt
         .traverse(
             &mut |rt: RichTerm, _| -> Result<RichTerm, ()> {
-                let rt = share_normal_form::transform_one(rt);
+                // before anything, we have to desugar the syntax
+                let rt = desugar_destructuring::transform_one(rt);
+                // We need to do contract generation before wrapping stuff in variables
+                let rt = apply_contracts::transform_one(rt);
                 Ok(rt)
             },
             &mut (),
-            TraverseOrder::BottomUp,
+            TraverseMethod::TopDown,
         )
-        .unwrap())
+        .unwrap();
+
+    rt.traverse(
+        &mut |rt: RichTerm, _| -> Result<RichTerm, ()> {
+            let rt = share_normal_form::transform_one(rt);
+            Ok(rt)
+        },
+        &mut (),
+        TraverseMethod::BottomUp,
+    )
+    .unwrap()
 }
 
 /// Generate a new fresh variable which do not clash with user-defined variables.
@@ -107,7 +105,7 @@ impl Closurizable for RichTerm {
         //
         //
         // We currently only do this optimization for generated variables (introduced by the share
-        // normal form). We could do it for non-generated identifiers as well, but we would be
+        // normal form). We could do it for non-generated identifiers as well, but be we would be
         // renaming user-supplied variables by gibberish generated names. It may hamper error
         // reporting, so for the time being, we restrict ourselves to generated identifiers. Note
         // that performing or not performing this optimization for user-supplied variables doesn't
@@ -142,9 +140,7 @@ impl Closurizable for Types {
     /// Extract the underlying contract, closurize it and wrap it back as a flat type (an opaque
     /// type defined by a custom contract).
     fn closurize(self, env: &mut Environment, with_env: Environment) -> Types {
-        Types(AbsType::Flat(
-            self.contract().unwrap().closurize(env, with_env),
-        ))
+        Types(AbsType::Flat(self.contract().closurize(env, with_env)))
     }
 }
 
diff --git a/src/typecheck/error.rs b/src/typecheck/error.rs
index 05136420..aa3a5502 100644
--- a/src/typecheck/error.rs
+++ b/src/typecheck/error.rs
@@ -36,8 +36,6 @@ pub enum RowUnifError {
     WithConst(usize, TypeWrapper),
     /// Tried to unify two distinct type constants.
     ConstMismatch(usize, usize),
-    /// An unbound type variable was referenced.
-    UnboundTypeVariable(Ident),
 }
 
 impl RowUnifError {
@@ -64,7 +62,6 @@ impl RowUnifError {
             RowUnifError::UnsatConstr(id, tyw) => UnifError::RowConflict(id, tyw, left, right),
             RowUnifError::WithConst(c, tyw) => UnifError::WithConst(c, tyw),
             RowUnifError::ConstMismatch(c1, c2) => UnifError::ConstMismatch(c1, c2),
-            RowUnifError::UnboundTypeVariable(id) => UnifError::UnboundTypeVariable(id),
         }
     }
 }
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index f223b71b..657f27af 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -50,7 +50,7 @@ use crate::{mk_tyw_arrow, mk_tyw_enum, mk_tyw_enum_row, mk_tyw_record, mk_tyw_ro
 use std::collections::{HashMap, HashSet};
 use std::convert::TryInto;
 
-use self::linearization::{Linearization, Linearizer, StubHost};
+use self::linearization::{Linearization, Linearizer, ScopeId, StubHost};
 
 pub mod error;
 pub mod linearization;
@@ -285,8 +285,8 @@ fn type_check_<L: Linearizer>(
     // TODO: The insertion of values in the type environment is done but everything is
     // typed as `Dyn`.
     fn inject_pat_vars(pat: &Destruct, envs: &mut Envs) {
-        if let Destruct::Record { matches, rest, .. } = pat {
-            if let Some(id) = rest {
+        if let Destruct::Record(matches, _, rst) = pat {
+            if let Some(id) = rst {
                 envs.insert(id.clone(), TypeWrapper::Concrete(AbsType::Dyn()));
             }
             matches.iter().for_each(|m| match m {
@@ -620,8 +620,10 @@ fn type_check_<L: Linearizer>(
             unify(state, strict, ty, ty_ret)
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
 
-            tys_op.into_iter().zip(args.iter()).try_for_each(
-                |(ty_t, t)| -> Result<_, TypecheckError> {
+            tys_op
+                .into_iter()
+                .zip(args.iter())
+                .try_for_each(|(ty_t, t)| {
                     type_check_(
                         state,
                         envs.clone(),
@@ -632,8 +634,7 @@ fn type_check_<L: Linearizer>(
                         ty_t,
                     )?;
                     Ok(())
-                },
-            )?;
+                })?;
 
             Ok(())
         }
@@ -1095,13 +1096,10 @@ pub fn unify_(
                         err.into_unif_err(mk_tyw_record!(; r1), mk_tyw_record!(; r2))
                     })
                 }
-                (TypeWrapper::Concrete(AbsType::Var(id)), _)
-                | (_, TypeWrapper::Concrete(AbsType::Var(id))) => {
-                    Err(UnifError::UnboundTypeVariable(id))
+                (TypeWrapper::Concrete(r), _) if !r.is_row_type() => {
+                    Err(UnifError::IllformedType(mk_tyw_record!(; r)))
                 }
-                (TypeWrapper::Concrete(r), _) | (_, TypeWrapper::Concrete(r))
-                    if !r.is_row_type() =>
-                {
+                (_, TypeWrapper::Concrete(r)) if !r.is_row_type() => {
                     Err(UnifError::IllformedType(mk_tyw_record!(; r)))
                 }
                 (tyw1, tyw2) => unify_(state, tyw1, tyw2),
@@ -1159,7 +1157,6 @@ pub fn unify_rows(
     t2: AbsType<Box<TypeWrapper>>,
 ) -> Result<(), RowUnifError> {
     match (t1, t2) {
-        (AbsType::Var(id), _) | (_, AbsType::Var(id)) => Err(RowUnifError::UnboundTypeVariable(id)),
         (AbsType::RowEmpty(), AbsType::RowEmpty()) | (AbsType::Dyn(), AbsType::Dyn()) => Ok(()),
         (AbsType::RowEmpty(), AbsType::Dyn()) => Err(RowUnifError::ExtraDynTail()),
         (AbsType::Dyn(), AbsType::RowEmpty()) => Err(RowUnifError::MissingDynTail()),
diff --git a/src/types.rs b/src/types.rs
index 99014929..b3c0e0ab 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -51,7 +51,6 @@
 //! otherwise.  Contract checks are introduced by `Promise` and `Assume` blocks or alternatively by
 //! enriched values `Contract` or `ContractDefault`. They ensure sane interaction between typed and
 //! untyped parts.
-use crate::error::{ParseError, ParseErrors, TypecheckError};
 use crate::identifier::Ident;
 use crate::term::make as mk_term;
 use crate::term::{RichTerm, Term, UnaryOp};
@@ -150,29 +149,6 @@ impl<Ty> AbsType<Ty> {
     }
 }
 
-#[derive(Clone, Debug)]
-pub struct UnboundTypeVariableError(pub Ident);
-
-impl From<UnboundTypeVariableError> for TypecheckError {
-    fn from(err: UnboundTypeVariableError) -> Self {
-        let pos = err.0.pos;
-        TypecheckError::UnboundTypeVariable(err.0, pos)
-    }
-}
-
-impl From<UnboundTypeVariableError> for ParseError {
-    fn from(err: UnboundTypeVariableError) -> Self {
-        let pos = err.0.pos;
-        ParseError::UnboundTypeVariables(vec![err.0], pos.unwrap())
-    }
-}
-
-impl From<UnboundTypeVariableError> for ParseErrors {
-    fn from(err: UnboundTypeVariableError) -> Self {
-        ParseErrors::from(ParseError::from(err))
-    }
-}
-
 /// Concrete, recursive type for a Nickel type.
 #[derive(Clone, PartialEq, Debug)]
 pub struct Types(pub AbsType<Box<Types>>);
@@ -180,7 +156,7 @@ pub struct Types(pub AbsType<Box<Types>>);
 impl Types {
     /// Return the contract corresponding to a type, either as a function or a record. Said
     /// contract must then be applied using the `Assume` primitive operation.
-    pub fn contract(&self) -> Result<RichTerm, UnboundTypeVariableError> {
+    pub fn contract(&self) -> RichTerm {
         let mut sy = 0;
         self.subcontract(HashMap::new(), true, &mut sy)
     }
@@ -200,40 +176,30 @@ impl Types {
         mut h: HashMap<Ident, (RichTerm, RichTerm)>,
         pol: bool,
         sy: &mut i32,
-    ) -> Result<RichTerm, UnboundTypeVariableError> {
+    ) -> RichTerm {
         use crate::stdlib::contracts;
 
-        fn get_var(
-            vars: &HashMap<Ident, (RichTerm, RichTerm)>,
-            id: &Ident,
-            pol: bool,
-        ) -> Result<RichTerm, UnboundTypeVariableError> {
-            let (pos, neg) = vars
-                .get(id)
-                .ok_or_else(|| UnboundTypeVariableError(id.clone()))?;
-            if pol {
-                Ok(pos.clone())
-            } else {
-                Ok(neg.clone())
-            }
-        }
-
-        let ctr = match self.0 {
+        match self.0 {
             AbsType::Dyn() => contracts::dynamic(),
             AbsType::Num() => contracts::num(),
             AbsType::Bool() => contracts::bool(),
             AbsType::Str() => contracts::string(),
             //TODO: optimization: have a specialized contract for `List Dyn`, to avoid mapping an
             //always successful contract on each element.
-            AbsType::List(ref ty) => mk_app!(contracts::list(), ty.subcontract(h, pol, sy)?),
+            AbsType::List(ref ty) => mk_app!(contracts::list(), ty.subcontract(h, pol, sy)),
             AbsType::Sym() => panic!("Are you trying to check a Sym at runtime?"),
             AbsType::Arrow(ref s, ref t) => mk_app!(
                 contracts::func(),
-                s.subcontract(h.clone(), !pol, sy)?,
-                t.subcontract(h, pol, sy)?
+                s.subcontract(h.clone(), !pol, sy),
+                t.subcontract(h, pol, sy)
             ),
             AbsType::Flat(ref t) => t.clone(),
-            AbsType::Var(ref id) => get_var(&h, id, true)?,
+            AbsType::Var(ref i) => {
+                let (rt, _) = h
+                    .get(i)
+                    .unwrap_or_else(|| panic!("Unbound type variable {:?}", i));
+                rt.clone()
+            }
             AbsType::Forall(ref i, ref t) => {
                 let inst_var = mk_app!(contracts::forall_var(), Term::Sym(*sy), Term::Bool(pol));
 
@@ -241,21 +207,18 @@ impl Types {
 
                 h.insert(i.clone(), (inst_var, inst_tail));
                 *sy += 1;
-                t.subcontract(h, pol, sy)?
+                t.subcontract(h, pol, sy)
             }
             AbsType::RowEmpty() | AbsType::RowExtend(..) => contracts::fail(),
             AbsType::Enum(ref r) => {
-                fn form(
-                    ty: Types,
-                    h: HashMap<Ident, (RichTerm, RichTerm)>,
-                ) -> Result<RichTerm, UnboundTypeVariableError> {
-                    let ctr = match ty.0 {
+                fn form(ty: Types, h: HashMap<Ident, (RichTerm, RichTerm)>) -> RichTerm {
+                    match ty.0 {
                         AbsType::RowEmpty() => contracts::fail(),
                         AbsType::RowExtend(_, Some(_), _) => {
                             panic!("It should be a row without type")
                         }
                         AbsType::RowExtend(id, None, rest) => {
-                            let rest_contract = form(*rest, h)?;
+                            let rest_contract = form(*rest, h);
                             let mut map = HashMap::new();
                             map.insert(id, Term::Bool(true).into());
 
@@ -272,14 +235,17 @@ impl Types {
                                 )
                             )
                         }
-                        AbsType::Var(ref id) => get_var(&h, id, true)?,
+                        AbsType::Var(ref i) => {
+                            let (rt, _) = h
+                                .get(i)
+                                .unwrap_or_else(|| panic!("Unbound type variable {:?}", i));
+                            rt.clone()
+                        }
                         not_row => panic!("It should be a row!! {:?}", not_row),
-                    };
-
-                    Ok(ctr)
+                    }
                 }
 
-                form(*r.clone(), h)?
+                form(*r.clone(), h)
             }
             AbsType::StaticRecord(ref ty) => {
                 fn form(
@@ -287,14 +253,19 @@ impl Types {
                     pol: bool,
                     ty: &Types,
                     h: HashMap<Ident, (RichTerm, RichTerm)>,
-                ) -> Result<RichTerm, UnboundTypeVariableError> {
-                    let ctr = match &ty.0 {
+                ) -> RichTerm {
+                    match &ty.0 {
                         AbsType::RowEmpty() => contracts::empty_tail(),
                         AbsType::Dyn() => contracts::dyn_tail(),
-                        AbsType::Var(id) => get_var(&h, id, false)?,
+                        AbsType::Var(id) => {
+                            let (_, rt) = h
+                                .get(id)
+                                .unwrap_or_else(|| panic!("Unbound type variable {:?}", id));
+                            rt.clone()
+                        }
                         AbsType::RowExtend(id, Some(ty), rest) => {
-                            let cont = form(sy, pol, rest.as_ref(), h.clone())?;
-                            let row_contr = ty.subcontract(h, pol, sy)?;
+                            let cont = form(sy, pol, rest.as_ref(), h.clone());
+                            let row_contr = ty.subcontract(h, pol, sy);
                             mk_app!(
                                 contracts::record_extend(),
                                 mk_term::string(format!("{}", id)),
@@ -306,19 +277,15 @@ impl Types {
                             "types::contract_open(): invalid row type {}",
                             Types(ty.clone())
                         ),
-                    };
-
-                    Ok(ctr)
+                    }
                 }
 
-                mk_app!(contracts::record(), form(sy, pol, ty, h)?)
+                mk_app!(contracts::record(), form(sy, pol, ty, h))
             }
             AbsType::DynRecord(ref ty) => {
-                mk_app!(contracts::dyn_record(), ty.subcontract(h, pol, sy)?)
+                mk_app!(contracts::dyn_record(), ty.subcontract(h, pol, sy))
             }
-        };
-
-        Ok(ctr)
+        }
     }
 
     /// Find a binding in a record row type. Return `None` if there is no such binding, if the type
@@ -389,7 +356,7 @@ impl fmt::Display for Types {
                 }
             }
             AbsType::Sym() => write!(f, "Sym"),
-            AbsType::Flat(ref t) => write!(f, "{}", t.as_ref().shallow_repr()),
+            AbsType::Flat(ref t) => write!(f, "#{}", t.as_ref().shallow_repr()),
             AbsType::Var(var) => write!(f, "{}", var),
             AbsType::Forall(i, ref ty) => {
                 let mut curr: &Types = ty.as_ref();
@@ -400,7 +367,7 @@ impl fmt::Display for Types {
                 }
                 write!(f, ". {}", curr)
             }
-            AbsType::Enum(row) => write!(f, "[|{}|]", row),
+            AbsType::Enum(row) => write!(f, "<{}>", row),
             AbsType::StaticRecord(row) => write!(f, "{{{}}}", row),
             AbsType::DynRecord(ty) => write!(f, "{{_: {}}}", ty),
             AbsType::RowEmpty() => Ok(()),
@@ -413,8 +380,8 @@ impl fmt::Display for Types {
 
                 match tail.0 {
                     AbsType::RowEmpty() => write!(f, "{}", tail),
-                    AbsType::Var(_) => write!(f, " ; {}", tail),
-                    AbsType::Dyn() => write!(f, " ; Dyn"),
+                    AbsType::Var(_) => write!(f, " | {}", tail),
+                    AbsType::Dyn() => write!(f, " | Dyn"),
                     _ => write!(f, ", {}", tail),
                 }
             }
@@ -477,11 +444,11 @@ mod test {
         assert_format_eq("{_: (Str -> Str) -> Str}");
 
         assert_format_eq("{x: (Bool -> Bool) -> Bool, y: Bool}");
-        assert_format_eq("forall r. {x: Bool, y: Bool, z: Bool ; r}");
+        assert_format_eq("forall r. {x: Bool, y: Bool, z: Bool | r}");
         assert_format_eq("{x: Bool, y: Bool, z: Bool}");
 
-        assert_format_eq("[|a, b, c, d|]");
-        assert_format_eq("forall r. [|tag1, tag2, tag3 ; r|]");
+        assert_format_eq("<a, b, c, d>");
+        assert_format_eq("forall r. <tag1, tag2, tag3 | r>");
 
         assert_format_eq("List");
         assert_format_eq("List Num");
diff --git a/stdlib/builtins.ncl b/stdlib/builtins.ncl
index 115cdb8a..b0d609b3 100644
--- a/stdlib/builtins.ncl
+++ b/stdlib/builtins.ncl
@@ -84,14 +84,14 @@
       "#m
     = fun x => %is_record% x,
 
-    typeof : Dyn -> [|
+    typeof : Dyn -> <
       TypeNum,
       TypeBool,
       TypeStr,
       TypeFun,
       TypeList,
       TypeRecord,
-      Other |]
+      Other>
     | doc m#"
       Results in a value representing the type of the typed value.
 
@@ -144,7 +144,7 @@
       "#m
     = fun x y => %deep_seq% x y,
 
-    hash : [| Md5, Sha1, Sha256, Sha512 |] -> Str -> Str
+    hash : <Md5, Sha1, Sha256, Sha512> -> Str -> Str
     | doc m#"
       Hashes the given string provided the desired hash algorithm.
 
@@ -156,7 +156,7 @@
       "#m
     = fun type s => %hash% type s,
 
-    serialize : [| Json, Toml, Yaml |] -> Dyn -> Str
+    serialize : <Json, Toml, Yaml> -> Dyn -> Str
     | doc m#"
       Serializes the given value to the desired representation.
 
@@ -171,7 +171,7 @@
       "#m
     = fun format x => %serialize% format (%deep_seq% x x),
 
-    deserialize : [| Json, Toml, Yaml |] -> Str -> Dyn
+    deserialize : <Json, Toml, Yaml> -> Str -> Dyn
     | doc m#"
       Deserializes the given string to a nickel value given the encoding of the string.
 
diff --git a/stdlib/lists.ncl b/stdlib/lists.ncl
index 4ccacead..6507f820 100644
--- a/stdlib/lists.ncl
+++ b/stdlib/lists.ncl
@@ -254,7 +254,7 @@
         "#m
       = fun f n => %generate% n f,
 
-    sort : forall a. (a -> a -> [| Less, Equal, Greater |]) -> List a -> List a
+    sort : forall a. (a -> a -> <Less, Equal, Greater>) -> List a -> List a
       | doc m#"
         Sorts the given lists based on the provided comparison operator.
 
diff --git a/stdlib/records.ncl b/stdlib/records.ncl
index dac0ad86..309790b8 100644
--- a/stdlib/records.ncl
+++ b/stdlib/records.ncl
@@ -15,7 +15,7 @@
       "#m
     = fun f r => %record_map% r f,
 
-    fields | { ; Dyn} -> List Str
+    fields | { | Dyn} -> List Str
     | doc m#"
       Given a record, results in a list of the string representation of all fields in the record.
 
@@ -26,7 +26,7 @@
       "#m
     = fun r => %fields% r,
 
-    values | { ; Dyn} -> List
+    values | { | Dyn} -> List
     | doc m#"
       Given a record, results in a list containing all the values in that record.
 
diff --git a/stdlib/strings.ncl b/stdlib/strings.ncl
index 1ec5f687..7a92b38a 100644
--- a/stdlib/strings.ncl
+++ b/stdlib/strings.ncl
@@ -177,7 +177,7 @@
       "#m
     = fun s => %str_chars% s,
 
-    code | CharLiteral -> Num
+    code | #CharLiteral -> Num
     | doc m#"
       Results in the ascii code of the given character.
 
@@ -193,7 +193,7 @@
       "#m
     = fun s => %char_code% s,
 
-    from_code | Num -> CharLiteral
+    from_code | Num -> #CharLiteral
     | doc m#"
       Results in the character for a given ascii code. Any number outside the ascii range results in an error.
 
@@ -382,7 +382,7 @@
       "#m
     = fun b => %to_str% b,
 
-    to_num | NumLiteral -> Num
+    to_num | #NumLiteral -> Num
     | doc m#"
       Converts a string that represents an integer to that integer.
 
@@ -394,7 +394,7 @@
       "#m
     = fun s => %num_from_str% s,
 
-    to_bool | BoolLiteral -> Bool
+    to_bool | #BoolLiteral -> Bool
     | doc m#"
       Converts a string that represents a boolean to that boolean.
 
@@ -410,7 +410,7 @@
     = fun s => s == "true",
 
     // to_enum | #Ident -> < | Dyn> = fun s => %enum_from_str% s,
-    to_enum | Ident -> Dyn
+    to_enum | #Ident -> Dyn
     | doc m#"
       Converts any string that represents an enum variant to that enum variant.
 


Test patch:
diff --git a/src/parser/tests.rs b/src/parser/tests.rs
index 84795587..792d979c 100644
--- a/src/parser/tests.rs
+++ b/src/parser/tests.rs
@@ -279,7 +279,8 @@ fn string_lexing() {
         lex_without_pos(r##"m#""#"#m"##),
         Ok(vec![
             Token::Normal(NormalToken::MultiStringStart(3)),
-            Token::MultiStr(MultiStringToken::Literal("\"#")),
+            Token::MultiStr(MultiStringToken::Literal("\"")),
+            Token::MultiStr(MultiStringToken::Literal("#")),
             Token::MultiStr(MultiStringToken::End),
         ])
     );
@@ -373,3 +374,30 @@ fn line_comments() {
         parse_without_pos("{field = foo}")
     );
 }
+
+#[test]
+fn unbound_type_variables() {
+    // should fail, "a" is unbound
+    assert_matches!(
+        parse("1 | a"),
+        Err(ParseError::UnboundTypeVariables(unbound_vars, _)) if (unbound_vars.contains(&Ident::from("a")) && unbound_vars.len() == 1)
+    );
+
+    // should fail, "d" is unbound
+    assert_matches!(
+        parse("null: forall a b c. a -> (b -> List c) -> {foo : List {_ : d}, bar: b | Dyn}"),
+        Err(ParseError::UnboundTypeVariables(unbound_vars, _)) if (unbound_vars.contains(&Ident::from("d")) && unbound_vars.len() == 1)
+    );
+
+    // should fail, "e" is unbound
+    assert_matches!(
+        parse("null: forall a b c. a -> (b -> List c) -> {foo : List {_ : a}, bar: b | e}"),
+        Err(ParseError::UnboundTypeVariables(unbound_vars, _)) if (unbound_vars.contains(&Ident::from("e")) && unbound_vars.len() == 1)
+    );
+
+    // should fail, "a" is unbound
+    assert_matches!(
+        parse("null: a -> (forall a. a -> a)"),
+        Err(ParseError::UnboundTypeVariables(unbound_vars, _)) if (unbound_vars.contains(&Ident::from("a")) && unbound_vars.len() == 1)
+    );
+}
diff --git a/tests/basics_fail.rs b/tests/basics_fail.rs
index cfc12e50..07cae89e 100644
--- a/tests/basics_fail.rs
+++ b/tests/basics_fail.rs
@@ -42,7 +42,7 @@ fn comparisons() {
 #[test]
 fn boolean_ops() {
     assert_matches!(
-        eval("let throw | fail = null in false || true && throw"),
+        eval("let throw | #fail = null in false || true && throw"),
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
     assert_matches!(
diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs
index 48defd0d..473c5876 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -16,9 +16,9 @@ macro_rules! assert_raise_blame {
 #[test]
 fn flat_contract_fail() {
     assert_raise_blame!(
-        "let AlwaysTrue = fun l t => let boolT | Bool = t in
+        "let alwaysTrue = fun l t => let boolT | Bool = t in
         if boolT then boolT else %blame% l in
-        (false | AlwaysTrue)"
+        (false | #alwaysTrue)"
     );
 }
 
@@ -32,9 +32,9 @@ fn id_fail() {
 
 #[test]
 fn enum_simple() {
-    assert_raise_blame!("`far | [|foo, bar|]");
-    assert_raise_blame!("123 | [|foo, bar|]");
-    assert_raise_blame!("`foo | [| |]");
+    assert_raise_blame!("`far | <foo, bar>");
+    assert_raise_blame!("123 | <foo, bar>");
+    assert_raise_blame!("`foo | < >");
 }
 
 #[test]
@@ -58,7 +58,7 @@ fn merge_compose_contract() {
         format!(
             "let Even = fun l x => if x % 2 == 0 then x else %blame% l in
         let DivBy3 = fun l x => if x % 3 ==  0 then x else %blame% l in
-        let composed = {{a | Even}} & {{a | DivBy3}} in
+        let composed = {{a | #Even}} & {{a | #DivBy3}} in
         (({{a = {},}}) & composed).a",
             arg
         )
@@ -98,13 +98,13 @@ fn records_contracts_poly() {
     // but this is not yet the case.
     // eval_string(&format!("{} {{foo = 2}}", extd)).unwrap_err();
 
-    let remv = "let f | forall a. {foo: Num ; a} -> { ; a} = fun x => x -$ \"foo\" in f";
+    let remv = "let f | forall a. {foo: Num | a} -> { | a} = fun x => x -$ \"foo\" in f";
     assert_raise_blame!(&format!("{} {{}}", remv));
 
-    let bad_cst = "let f | forall a. { ; a} -> { ; a} = fun x => {a=1} in f";
-    let bad_acc = "let f | forall a. { ; a} -> { ; a} = fun x => %seq% x.a x in f";
-    let bad_extd = "let f | forall a. { ; a} -> {foo: Num ; a} = fun x => x -$ \"foo\" in f";
-    let bad_rmv = "let f | forall a. {foo: Num ; a} -> { ; a} = fun x => x$[\"foo\"=1] in f";
+    let bad_cst = "let f | forall a. { | a} -> { | a} = fun x => {a=1} in f";
+    let bad_acc = "let f | forall a. { | a} -> { | a} = fun x => %seq% x.a x in f";
+    let bad_extd = "let f | forall a. { | a} -> {foo: Num | a} = fun x => x -$ \"foo\" in f";
+    let bad_rmv = "let f | forall a. {foo: Num | a} -> { | a} = fun x => x$[\"foo\"=1] in f";
 
     assert_raise_blame!(&format!("{} {{}}", bad_cst));
     // The polymorphic parts is protected by hiding it. Thus, trying to access the protected field
@@ -121,9 +121,9 @@ fn records_contracts_poly() {
     assert_raise_blame!(
         "let f |
             forall a.
-                (forall b. {a: Num, b: Num ; b} -> { a: Num ; b})
-                -> {a: Num ; a}
-                -> { ; a}
+                (forall b. {a: Num, b: Num | b} -> { a: Num | b})
+                -> {a: Num | a}
+                -> { | a}
             = fun f rec => (f rec) -$ \"a\" -$ \"b\" in
         f (fun x => x) {a = 1, b = true, c = 3}"
     );
@@ -172,9 +172,9 @@ fn lists_contracts() {
 
 #[test]
 fn records_contracts_closed() {
-    assert_raise_blame!("{a=1} | {}");
-    assert_raise_blame!("{a=1, b=2} | {a | Num}");
-    assert_raise_blame!("let Contract = {a | Num} & {b | Num} in ({a=1, b=2, c=3} | Contract)");
+    assert_raise_blame!("{a=1} | #{}");
+    assert_raise_blame!("{a=1, b=2} | #{a | Num}");
+    assert_raise_blame!("let Contract = {a | Num} & {b | Num} in ({a=1, b=2, c=3} | #Contract)");
 }
 
 // #[test]
diff --git a/tests/pass/annotations.ncl b/tests/pass/annotations.ncl
index 81a6aa2e..f00e6c3d 100644
--- a/tests/pass/annotations.ncl
+++ b/tests/pass/annotations.ncl
@@ -4,24 +4,24 @@ let Assert = fun l x => x || %blame% l in
   // left_annot_precedence
   (let dummy = null in
     let LocalAssert = Assert in
-    true | LocalAssert),
+    true | #LocalAssert),
 
   (if false then
       null
     else
       let dummy = null in
       let LocalAssert = Assert in
-      true | LocalAssert),
+      true | #LocalAssert),
 
   (let f = fun x =>
       let dummy = null in
       let LocalAssert = Assert in
-      x | LocalAssert in
+      x | #LocalAssert in
     f true),
 
   // others_precedence
-  ((fun x => x | Assert) true),
+  ((fun x => x | #Assert) true),
   (let AssertOk = fun l t => if t == `Ok then t else %blame% l in
-    switch {`Ok => true, `Err => false} `Ok | AssertOk),
+    switch {`Ok => true, `Err => false} `Ok | #AssertOk),
 ]
 |> lists.foldl (fun x y => x && y) true
diff --git a/tests/pass/basics.ncl b/tests/pass/basics.ncl
index 593590c3..a876f9b3 100644
--- a/tests/pass/basics.ncl
+++ b/tests/pass/basics.ncl
@@ -34,4 +34,4 @@ let Assert = fun l x => x || %blame% l in
   // This test checks that the terms of a switch are closured
   let x = 3 in (switch { `foo => 1, _ => x} (3 + 2)) == 3,
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/builtins.ncl b/tests/pass/builtins.ncl
index c005ea70..5ba3dcf8 100644
--- a/tests/pass/builtins.ncl
+++ b/tests/pass/builtins.ncl
@@ -27,4 +27,4 @@ let Assert = fun l x => x || %blame% l in
    |> builtins.deserialize `Json
    == [3,4],
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/complete.ncl b/tests/pass/complete.ncl
index be0c3958..0ab8bc49 100644
--- a/tests/pass/complete.ncl
+++ b/tests/pass/complete.ncl
@@ -7,4 +7,4 @@ let fibo : Num -> Num = Y (fun fibo =>
   (fun x => if or (x == 0) (dec x == 0) then 1 else (fibo (dec x)) + (fibo (dec (dec x))))) in
 let val : Num = 4 in
 
-(fibo val | AssertEq 5)
+(fibo val | #(AssertEq 5))
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
index 1006a487..532b819c 100644
--- a/tests/pass/contracts.ncl
+++ b/tests/pass/contracts.ncl
@@ -7,7 +7,7 @@ let Assert = fun l x => x || %blame% l in
   let AlwaysFalse = fun l t =>
     let boolT | Bool = t in
     if boolT then %blame% l else boolT
-  in let not | AlwaysTrue -> AlwaysFalse = fun b => if b then false else true in
+  in let not | #AlwaysTrue -> #AlwaysFalse = fun b => if b then false else true in
   not true == false,
 
   // id_polymorphic_contract
@@ -28,27 +28,27 @@ let Assert = fun l x => x || %blame% l in
   ("hello" ++ " world" | Str) == "hello world",
 
   // enums_simple
-  (`foo | [| foo, bar |]) == `foo,
-  (`bar | forall r. [| foo, bar ; r|]) == `bar,
+  (`foo | <foo, bar>) == `foo,
+  (`bar | forall r. <foo, bar | r>) == `bar,
 
   // enums_escaped
-  (`"foo:baz" | [| "foo:baz", "bar:baz" |]) == `"foo:baz",
-  (`"bar:baz" | forall r. [| "foo:baz", "bar:baz" ; r |]) == `"bar:baz",
+  (`"foo:baz" | <"foo:baz", "bar:baz">) == `"foo:baz",
+  (`"bar:baz" | forall r. <"foo:baz", "bar:baz" | r>) == `"bar:baz",
 
   // enums_complex
-  let f : forall r. [| foo, bar ; r |] -> Num =
+  let f : forall r. <foo, bar | r> -> Num =
     fun x => switch { `foo => 1, `bar => 2, _ => 3, } x in
   f `bar == 2,
 
-  let f : forall r. [| foo, bar ; r |] -> Num =
+  let f : forall r. <foo, bar | r> -> Num =
     fun x => switch { `foo => 1, `bar => 2, _ => 3, } x in
   f `boo == 3,
 
-  let f : forall r. [| foo, "bar:baz" ; r |] -> Num =
+  let f : forall r. <foo, "bar:baz" | r> -> Num =
     fun x => switch { `foo => 1, `"bar:baz" => 2, _ => 3, } x in
   f `"bar:baz" == 2,
 
-  let f : forall r. [| foo, "bar:baz" ; r |] -> Num =
+  let f : forall r. <foo, "bar:baz" | r> -> Num =
     fun x => switch { `foo => 1, `"bar:baz" => 2, _ => 3, } x in
   f `"boo,grr" == 3,
 
@@ -61,41 +61,41 @@ let Assert = fun l x => x || %blame% l in
     %deep_seq% x x == {a = 1, s = { foo = true}},
 
   // polymorphism
-  (let id | forall a. { ; a} -> { ; a} = fun x => x in
-    let extend | forall a. { ; a} -> {foo: Num ; a} = fun x =>
+  (let id | forall a. { | a} -> { | a} = fun x => x in
+    let extend | forall a. { | a} -> {foo: Num | a} = fun x =>
       x & {foo = 1} in
-    let remove | forall a. {foo: Num ; a} -> { ; a} = fun x =>
+    let remove | forall a. {foo: Num | a} -> { | a} = fun x =>
       x -$ "foo" in
 
-    (id {} == {} | Assert) &&
-    (id {a = 1, b = false} == {a = 1, b = false} | Assert) &&
-    (extend {} == {foo = 1} | Assert) &&
-    (extend {bar = false} == {foo = 1, bar = false} | Assert) &&
-    (remove {foo = 1} == {} | Assert) &&
-    (remove {foo = 1, bar = 1} == {bar = 1} | Assert) &&
-    (remove (extend {}) == {} | Assert) &&
-    (extend (remove {foo = 2}) == {foo =1} | Assert) &&
-    (let f | forall a b. {f: a -> a, arg: a ; b} -> a =
+    (id {} == {} | #Assert) &&
+    (id {a = 1, b = false} == {a = 1, b = false} | #Assert) &&
+    (extend {} == {foo = 1} | #Assert) &&
+    (extend {bar = false} == {foo = 1, bar = false} | #Assert) &&
+    (remove {foo = 1} == {} | #Assert) &&
+    (remove {foo = 1, bar = 1} == {bar = 1} | #Assert) &&
+    (remove (extend {}) == {} | #Assert) &&
+    (extend (remove {foo = 2}) == {foo =1} | #Assert) &&
+    (let f | forall a b. {f: a -> a, arg: a | b} -> a =
         fun rec => rec.f (rec.arg) in
       f { f = fun x => x ++ " suffix", arg = "foo" }
       == "foo suffix"
-      | Assert)
+      | #Assert)
   ),
 
   // records_dynamic_tail
-  ({a = 1, b = "b"} | {a: Num, b: Str ; Dyn}) == {a = 1, b = "b"},
-  ({a = 1, b = "b", c = false} | {a: Num, b: Str ; Dyn})
+  ({a = 1, b = "b"} | {a: Num, b: Str | Dyn}) == {a = 1, b = "b"},
+  ({a = 1, b = "b", c = false} | {a: Num, b: Str | Dyn})
   == {a = 1, b = "b", c = false},
-  ((fun r => r.b) | {a: Num ; Dyn} -> Dyn) {a = 1, b = 2} == 2,
+  ((fun r => r.b) | {a: Num | Dyn} -> Dyn) {a = 1, b = 2} == 2,
 
   // records_open_contracts
-  ({a = 0, b = 0} | {a | Num, ..}) == {a = 0, b = 0},
+  ({a = 0, b = 0} | #{a | Num, ..}) == {a = 0, b = 0},
   let Contract = {a | Num} & {..} in
-  ({a = 0, b = 0} | Contract) == {a = 0, b = 0},
+  ({a = 0, b = 0} | #Contract) == {a = 0, b = 0},
   let Contract = {..} & {b | Num} in
-  ({a = 0, b = 0} | Contract) == {a = 0, b = 0},
+  ({a = 0, b = 0} | #Contract) == {a = 0, b = 0},
   let Contract = {a | Num, ..} & {b | Num, ..} in
-  ({a = 0, b = 0, c = 0} | Contract) == {a = 0, b = 0, c = 0},
+  ({a = 0, b = 0, c = 0} | #Contract) == {a = 0, b = 0, c = 0},
 
   // lists
   ([1, "2", false] | List) == [1, "2", false],
@@ -111,12 +111,12 @@ let Assert = fun l x => x || %blame% l in
   // Regression test for #402
   let MyContract = { x | Str } in
   {
-    foo | MyContract | default = { x = "From foo" },
-    bar | {..} | default = foo
+    foo | #MyContract | default = { x = "From foo" },
+    bar | #{..} | default = foo
   } == { foo.x = "From foo", bar.x = "From foo"},
 
   // mixing type and record contracts
-  let f | {foo | Num} -> {bar | Num} = fun r =>
+  let f | #{foo | Num} -> #{bar | Num} = fun r =>
     {bar = r.foo} in
   (f {foo = 1}).bar == 1,
   // user-written contract application
@@ -128,8 +128,8 @@ let Assert = fun l x => x || %blame% l in
     contracts.apply derived label value in
   let Contract = Extend {bar | Num, ..} in
   let Id = Extend (fun label value => value) in
-  ({bar = 1, foo = 1} | Contract)
-    & ({baz = 1} | Id)
-   == {foo = 1, bar = 1, baz = 1},
+  ({bar = 1, foo = 1} | #Contract)
+    & ({baz = 1} | #Id)
+  == {foo = 1, bar = 1, baz = 1},
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/eq.ncl b/tests/pass/eq.ncl
index 2ad1dcd3..7fcf18af 100644
--- a/tests/pass/eq.ncl
+++ b/tests/pass/eq.ncl
@@ -75,4 +75,4 @@ let Assert = fun l x => x || %blame% l in
       == false
   ),
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/functions.ncl b/tests/pass/functions.ncl
index 30f67b40..6afbaebb 100644
--- a/tests/pass/functions.ncl
+++ b/tests/pass/functions.ncl
@@ -15,4 +15,4 @@ let Assert = fun l x => x || %blame% l in
     g true
     == 4,
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/import.ncl b/tests/pass/import.ncl
index 0850f46e..f6ae0ee0 100644
--- a/tests/pass/import.ncl
+++ b/tests/pass/import.ncl
@@ -1,3 +1,3 @@
 let Assert = fun l x => x || %blame% l in
 
-(import "imported.ncl" 3 == 3 | Assert)
+(import "imported.ncl" 3 == 3 | #Assert)
diff --git a/tests/pass/imported.ncl b/tests/pass/imported.ncl
index 0d72daea..54d96487 100644
--- a/tests/pass/imported.ncl
+++ b/tests/pass/imported.ncl
@@ -1,2 +1,3 @@
 // This isn’t really a test, mostly an auxiliary file used by `import.ncl`
+
 fun x => x
diff --git a/tests/pass/lists.ncl b/tests/pass/lists.ncl
index cfb3efdf..5576e6f1 100644
--- a/tests/pass/lists.ncl
+++ b/tests/pass/lists.ncl
@@ -33,4 +33,4 @@ let Assert = fun l x => x || %blame% l in
     let isZ = fun x => x == 0 in
     all isZ [0, 0, 0, 1] == false,
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/metavalues.ncl b/tests/pass/metavalues.ncl
index e4e5706c..c000e388 100644
--- a/tests/pass/metavalues.ncl
+++ b/tests/pass/metavalues.ncl
@@ -28,29 +28,29 @@ let Assert = fun l x => x || %blame% l in
   // composed
   let Even = fun l x => if x % 2 == 0 then x else %blame% l in
     let DivBy3 = fun l x => if x % 3 ==  0 then x else %blame% l in
-    let composed = {a | Even} & {a | DivBy3} in
-    (composed & {a = 6} == {a = 6} | Assert) &&
-    (composed & {a = 12} == {a = 12} | Assert),
+    let composed = {a | #Even} & {a | #DivBy3} in
+    (composed & {a = 6} == {a = 6} | #Assert) &&
+    (composed & {a = 12} == {a = 12} | #Assert),
 
 
   // Check that the environments of contracts are correctly saved and restored when merging. See
   // issue [#117](https://github.com/tweag/nickel/issues/117)
-  (let ctr_num = let x = num in {a | x} in
-    let ctr_id = let x = fun l x => x in {a | x} in
+  (let ctr_num = let x = num in {a | #x} in
+    let ctr_id = let x = fun l x => x in {a | #x} in
     let val = let x = 1 in {a = x} in
     let def = let x = 2 in {a | default = x} in
     let def2 = let x = (1 + 1) in {a | default = x} in
   // contract/contract -> contract/value -> value/default
-  ((ctr_num & ctr_id & val & def).a == 1 | Assert) &&
+  ((ctr_num & ctr_id & val & def).a == 1 | #Assert) &&
   // default/value <- value/contract
-  ((def & (val & ctr_num)).a == 1 | Assert) &&
+  ((def & (val & ctr_num)).a == 1 | #Assert) &&
   // default/contract-> contract-default/contract-default <- contract/default
-  (((def & ctr_num) & (ctr_id & def2)).a == 2 | Assert) &&
+  (((def & ctr_num) & (ctr_id & def2)).a == 2 | #Assert) &&
   // default/contract -> contract-default/contract -> contract-default/value
-  ((def & ctr_num & ctr_id & val).a == 1 | Assert) &&
+  ((def & ctr_num & ctr_id & val).a == 1 | #Assert) &&
   // default/contract -> contract-default/default
-  ((def & ctr_num & def2).a == 2 | Assert) &&
+  ((def & ctr_num & def2).a == 2 | #Assert) &&
   // value/contract-default <- contract/contract-default
-  ((val & (ctr_num & def)).a == 1 | Assert)),
+  ((val & (ctr_num & def)).a == 1 | #Assert)),
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/overriding.ncl b/tests/pass/overriding.ncl
index c0515472..f05240ff 100644
--- a/tests/pass/overriding.ncl
+++ b/tests/pass/overriding.ncl
@@ -71,4 +71,4 @@ let Assert = contracts.from_predicate functions.id in
   ({foo | default = 1, bar = foo} & {foo = 2}).bar == 2,
   ({foo | default = 1, bar = foo, baz = bar} & {foo = 2}).baz == 2,
 ]
-|> lists.foldl (fun next acc => (next | Assert) && acc) true
+|> lists.foldl (fun next acc => (next | #Assert) && acc) true
diff --git a/tests/pass/record-defs.ncl b/tests/pass/record-defs.ncl
index 443a6e89..bb6e1eeb 100644
--- a/tests/pass/record-defs.ncl
+++ b/tests/pass/record-defs.ncl
@@ -40,4 +40,4 @@ let Assert = fun l x => x || %blame% l in
   let x = "foo" in {"#{x}" = bar, bar = 1} == {foo = 1, bar = 1},
   ({"#foo"."#bar".baz = other + 1, other = 0}."#foo"."#bar".baz == 1),
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/records.ncl b/tests/pass/records.ncl
index 837670d6..7ed6ff00 100644
--- a/tests/pass/records.ncl
+++ b/tests/pass/records.ncl
@@ -104,12 +104,12 @@ let Assert = fun l x => x || %blame% l in
   let Name = fun b label name => if b then "hijack" else contracts.blame label in
   let Config = {
       b | Bool,
-      name | Name b,
+      name | #(Name b),
   } in
-  let data | Config = {
+  let data | #Config = {
       b = true,
       name = "name",
   } in
   data.name == "hijack",
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/serialize-package.ncl b/tests/pass/serialize-package.ncl
index 1f59153c..1c5b2e7d 100644
--- a/tests/pass/serialize-package.ncl
+++ b/tests/pass/serialize-package.ncl
@@ -9,7 +9,7 @@ let ctr = {
     buildInputs | doc "
                   The list of inputs for this package, specified as a
                   `NixPackage`."
-                | List NixPackage,
+                | List #NixPackage,
     // Many more missing
   },
 
@@ -25,7 +25,7 @@ let ctr = {
                ```
                myPkg = {
                  name  = \"myPkg\",
-                 buildInputs | List NixPackage = [{package = \"hello\"}]\",
+                 buildInputs | List #NixPackage = [{package = \"hello\"}]\",
                }
                ```
                This will give the following attribute sets once imported in Nix:
@@ -57,7 +57,7 @@ builtins.serialize `Json (
   {
     name = "nickel",
     buildInputs = [{package = "hello"}],
-  } | ctr.Shell
+  } | #ctr.Shell
 ) == builtins.serialize `Json {
   name = "nickel",
   buildInputs = [{input = "nixpkgs", package = "hello", "_type" = "package"}],
diff --git a/tests/pass/serialize.ncl b/tests/pass/serialize.ncl
index 1c8340d5..ff3ff8c2 100644
--- a/tests/pass/serialize.ncl
+++ b/tests/pass/serialize.ncl
@@ -29,4 +29,4 @@ let assertDeserInv = fun x =>
       baz = {subfoo = true, subbar = 0}
     },
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/strings.ncl b/tests/pass/strings.ncl
index 52db2961..9648f296 100644
--- a/tests/pass/strings.ncl
+++ b/tests/pass/strings.ncl
@@ -15,10 +15,5 @@ let Assert = fun l x => x || %blame% l in
   m#""#{"foo"}""#m == "\"foo\"",
   m#"""#m == "\"",
   m#""#"#"#"#m == "\"#\"#\"#",
-
-  // regression test for issue #596 (https://github.com/tweag/nickel/issues/596)
-  let s = "Hello" in m##""##{s}" World"##m == "\"Hello\" World",
-  let s = "Hello" in m##""###{s}" World"##m == "\"#Hello\" World",
-  m##""##s"##m == "\"##s",
 ]
-|> lists.foldl (fun x y => (x | Assert) && y) true
+|> lists.foldl (fun x y => (x | #Assert) && y) true
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index 8ae8353f..85a47dd0 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -19,7 +19,7 @@ let typecheck = [
   (fun id => (id 4) + (id true: Bool)) (fun x => x),
   // contracts are opaque types
   (let AlwaysTrue = fun l t => if t then t else %blame% l in
-  ((fun x => x) : AlwaysTrue -> AlwaysTrue)),
+  ((fun x => x) : #alwaysTrue -> #alwaysTrue)),
 
   // simple_polymorphism
   let f : forall a. a -> a = fun x => x in
@@ -49,28 +49,28 @@ let typecheck = [
     ((if (f true) then (f 2) else 3) : Num),
 
   // enums_simple
-  (`bla : [|bla |]),
-  (`blo : [|bla, blo |]),
-  (`bla : forall r. [|bla ; r |]),
-  (`bla : forall r. [|bla, blo ; r |]),
+  (`bla : <bla>),
+  (`blo : <bla, blo>),
+  (`bla : forall r. <bla | r>),
+  (`bla : forall r. <bla, blo | r>),
   ((switch {`bla => 3} `bla) : Num),
   ((switch {`bla => 3, _ => 2} `blo) : Num),
 
   // enums_complex
-  ((fun x => switch {`bla => 1, `ble => 2} x) : [|bla, ble |] -> Num),
+  ((fun x => switch {`bla => 1, `ble => 2} x) : <bla, ble> -> Num),
   ((fun x => switch {`bla => 1, `ble => 2, `bli => 4} (%embed% bli x))
-    : [|bla, ble |] -> Num),
+    : <bla, ble> -> Num),
   ((fun x =>
       (switch {`bla => 3, `bli => 2} x)
       + (switch {`bli => 6, `bla => 20} x))
     `bla
     : Num),
 
-  let f : forall r. [|blo, ble ; r |] -> Num = fun x =>
+  let f : forall r. <blo, ble | r> -> Num = fun x =>
     switch {`blo => 1, `ble => 2, _ => 3} x in
             (f `bli : Num),
 
-  let f : forall r. (forall p. [|blo, ble ; r |] -> [|bla, bli ; p |]) =
+  let f : forall r. (forall p. <blo, ble | r> -> <bla, bli | p>) =
     fun x => switch {`blo => `bla, `ble => `bli, _ => `bla} x in
     f `bli,
 
@@ -82,7 +82,7 @@ let typecheck = [
   let r : {bla : Bool, blo : Num} = {blo = 1, bla = true} in
     ((if r.bla then r.blo else 2) : Num),
 
-  let f : forall a r. {bla : Bool, blo : a, ble : a ; r} -> a =
+  let f : forall a r. {bla : Bool, blo : a, ble : a | r} -> a =
       fun r => if r.bla then r.blo else r.ble in
     (if (f {bla = true, blo = false, ble = true, blip = 1, }) then
       (f {bla = true, blo = 1, ble = 2, blip = `blip, })
@@ -130,12 +130,12 @@ let typecheck = [
     : {f : Num -> Num},
 
   // polymorphic_row_constraints
-  let extend | forall c. { ; c} -> {a: Str ; c} = 0 in
-    let remove | forall c. {a: Str ; c} -> { ; c} = 0 in
+  let extend | forall c. { | c} -> {a: Str | c} = 0 in
+    let remove | forall c. {a: Str | c} -> { | c} = 0 in
     (let good = remove (extend {}) in 0) : Num,
 
-  let r | {a: Num ; Dyn} = {a = 1, b = 2} in (r.a : Num),
-  ({a = 1, b = 2} | {a: Num ; Dyn}) : {a: Num ; Dyn},
+  let r | {a: Num | Dyn} = {a = 1, b = 2} in (r.a : Num),
+  ({a = 1, b = 2} | {a: Num | Dyn}) : {a: Num | Dyn},
 
   //Regression test following [#270](https://github.com/tweag/nickel/issues/270). Check that
   //unifying a variable with itself doesn't introduce a loop. The failure of this test results
diff --git a/tests/pass/types.ncl b/tests/pass/types.ncl
index ac3e0bd1..1cea0bd7 100644
--- a/tests/pass/types.ncl
+++ b/tests/pass/types.ncl
@@ -1,4 +1,4 @@
 let Assert = fun l x => x || %blame% l in
 
 (let plus : Num -> Num -> Num = fun x => fun y => x + y in
- plus (54 : Num) (6 : Num) == 60 | Assert)
+ plus (54 : Num) (6 : Num) == 60 | #Assert)
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index 2334c563..0468c9e8 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -29,7 +29,6 @@ macro_rules! assert_typecheck_fails {
 
 #[test]
 fn unbound_variable_always_throws() {
-    type_check_expr("x").map_err(|err| println!("{:#?}", err));
     assert_matches!(
         type_check_expr("x"),
         Err(TypecheckError::UnboundIdentifier(..))
@@ -53,7 +52,7 @@ fn promise_complicated() {
     // no implicit polymorphism
     assert_typecheck_fails!("(fun id => (id 4 : Num) + (id true : Bool)) (fun x => x)");
     // contract equality (to be fair, the current implementation is full of issues: to be reworked)
-    assert_typecheck_fails!("(fun x => x) : (fun l t => t) -> (fun l t => t)");
+    assert_typecheck_fails!("(fun x => x) : #(fun l t => t) -> #(fun l t => t)");
 }
 
 #[test]
@@ -78,7 +77,7 @@ fn simple_forall() {
 
 #[test]
 fn enum_simple() {
-    assert_typecheck_fails!("`foo : [| bar |]");
+    assert_typecheck_fails!("`foo : <bar>");
     assert_typecheck_fails!("switch { `foo => 3} `bar : Num");
     assert_typecheck_fails!("switch { `foo => 3, `bar => true} `bar : Num");
 }
@@ -86,7 +85,7 @@ fn enum_simple() {
 #[test]
 fn enum_complex() {
     assert_typecheck_fails!(
-        "(fun x => switch {`bla => 1, `ble => 2, `bli => 4} x) : [| bla, ble |] -> Num"
+        "(fun x => switch {`bla => 1, `ble => 2, `bli => 4} x) : <bla, ble> -> Num"
     );
     // TODO typecheck this, I'm not sure how to do it with row variables
     // LATER NOTE: this requires row subtyping, not easy
@@ -96,12 +95,12 @@ fn enum_complex() {
             (switch {`bla => 6, `blo => 20} x)) `bla : Num"
     );
     assert_typecheck_fails!(
-        "let f : forall r. [| blo, ble ; r |] -> Num =
+        "let f : forall r. <blo, ble | r> -> Num =
             fun x => (switch {`blo => 1, `ble => 2, `bli => 3} x) in
         f"
     );
     assert_typecheck_fails!(
-        "let f : forall r. (forall p. [| blo, ble ; r |] -> [| bla, bli ; p |]) =
+        "let f : forall r. (forall p. <blo, ble | r> -> <bla, bli | p>) =
             fun x => (switch {`blo => `bla, `ble => `bli, _ => `blo} x) in
         f `bli"
     );
@@ -115,12 +114,12 @@ fn static_record_simple() {
     assert_typecheck_fails!("{blo = 1}.blo : Bool");
 
     assert_typecheck_fails!(
-        "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a ; r} -> a) =
+        "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
             fun r => if r.bla then r.blo else r.ble in
          (f {bla = true, blo = 1, ble = true, blip = `blip} : Num)"
     );
     assert_typecheck_fails!(
-        "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a ; r} -> a) =
+        "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
             fun r => if r.bla then (r.blo + 1) else r.ble in
          (f {bla = true, blo = 1, ble = 2, blip = `blip} : Num)"
     );
@@ -186,13 +185,13 @@ fn polymorphic_row_constraints() {
     }
 
     let mut res = type_check_expr(
-        "let extend | forall c. { ; c} -> {a: Str ; c} = null in
+        "let extend | forall c. { | c} -> {a: Str | c} = null in
            (let bad = extend {a = 1} in 0) : Num",
     );
     assert_row_conflict(res);
 
     res = type_check_expr(
-        "let remove | forall c. {a: Str ; c} -> { ; c} = nul in
+        "let remove | forall c. {a: Str | c} -> { | c} = nul in
            (let bad = remove (remove {a = \"a\"}) in 0) : Num",
     );
     assert_row_conflict(res);
@@ -202,10 +201,10 @@ fn polymorphic_row_constraints() {
 fn dynamic_row_tail() {
     // Currently, typechecking is conservative wrt the dynamic row type, meaning it can't
     // convert to a less precise type with a dynamic tail.
-    assert_typecheck_fails!("{a = 1, b = 2} : {a: Num ; Dyn}");
-    assert_typecheck_fails!("{a = 1} : {a: Num ; Dyn}");
-    assert_typecheck_fails!("({a = 1} | {a: Num ; Dyn}) : {a: Num}");
-    assert_typecheck_fails!("{a = 1} : {a: Num ; Dyn}");
+    assert_typecheck_fails!("{a = 1, b = 2} : {a: Num | Dyn}");
+    assert_typecheck_fails!("{a = 1} : {a: Num | Dyn}");
+    assert_typecheck_fails!("({a = 1} | {a: Num | Dyn}) : {a: Num}");
+    assert_typecheck_fails!("{a = 1} : {a: Num | Dyn}");
 }
 
 #[test]
diff --git a/tests/unbound_type_variables.rs b/tests/unbound_type_variables.rs
deleted file mode 100644
index 13d8ee78..00000000
--- a/tests/unbound_type_variables.rs
+++ /dev/null
@@ -1,60 +0,0 @@
-// Since [RFC002](../rfcs/002-merge-types-terms-syntax.md), the following tests don't raise an
-// unbound type variable error anymore. Instead, the variable is interpreted as a term variable:
-// the tests should still fail, but they can now fail with a standard unbound identifier error.
-use assert_matches::assert_matches;
-use nickel::{
-    error::{Error, EvalError, ParseError, ParseErrors, TypecheckError},
-    identifier::Ident,
-};
-
-use utilities::eval;
-
-macro_rules! assert_unbound {
-    ( $term:expr, $var:expr ) => {
-        let res = eval($term);
-        // Because expressions inside user-defined contracts are not currently typechecked, the
-        // error should be an `EvalError::UnboundIdentifier` at the time of writing this comment.
-        // Since it may not be the case forever, we accept alternative errors that make sense.
-        assert_matches!(res, Err(Error::ParseErrors(_)) | Err(Error::TypecheckError(_)) | Err(Error::EvalError(_)));
-
-        match res {
-            Err(Error::ParseErrors(ParseErrors {errors})) =>
-                assert_matches!(errors.as_slice(),
-                    [ParseError::UnboundTypeVariables(vars, _)]
-                    if vars.contains(&Ident::from($var)) && vars.len() == 1),
-            Err(Error::TypecheckError(err)) =>
-                assert_matches!(err,
-                    TypecheckError::UnboundIdentifier(id, ..)
-                    | TypecheckError::UnboundTypeVariable(id, ..)
-                    if id.label.as_str() == $var),
-            Err(Error::EvalError(err)) =>
-                assert_matches!(err,
-                    EvalError::UnboundIdentifier(id, ..)
-                    if id.label.as_str() == $var),
-            _ => unreachable!(),
-        };
-    }
-}
-
-#[test]
-fn unbound_type_variables() {
-    assert_unbound!("1 | a", "a");
-    assert_unbound!(
-        "let f | forall a b c. a -> (b -> List c) -> {foo : List {_ : d}, bar: a; Dyn}
-           = fun bar_ _g => {foo = [{field = 1}], bar = bar_} in
-         (f 1 (fun _x => [])).foo == [{field = 1}]",
-        "d"
-    );
-    assert_unbound!(
-        "let f : forall a b c. a -> (b -> List c) -> {foo : List {field : a}, bar: a; e}
-           = fun bar_ _g => {foo = [{field = bar_}], bar = bar_} in
-         null",
-        "e"
-    );
-    assert_unbound!(
-        "let f | a -> (forall a. a -> a)
-                       = fun x => builtins.seq x null in
-                       f null",
-        "a"
-    );
-}