Repository: tweag/nickel
Pull request #610 (2022-02-10 16:03:04)

[User manual] Contracts
Add an overarching "correctness" section to introduce both types and contracts system at a high-level, and add a sub-section on contracts.


Patch:
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
new file mode 100644
index 00000000..6cd1da8a
--- /dev/null
+++ b/doc/manual/contracts.md
@@ -0,0 +1,682 @@
+# 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
new file mode 100644
index 00000000..3cb0c449
--- /dev/null
+++ b/doc/manual/correctness.md
@@ -0,0 +1,359 @@
+# 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 651b783b..97eb0df9 100644
--- a/doc/manual/typing.md
+++ b/doc/manual/typing.md
@@ -1,32 +1,7 @@
 # Typing in Nickel
 
-## 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).
+(For the motivations behind typing and a high-level overview of contracts and
+types, first read the [correctness](./correctness.md) section.)
 
 ## Typing modes
 
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/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 329d4459..abc99361 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -1,48 +1,30 @@
-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::UniRecord,
-};
+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,
-};
+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});
-
-AsTypes<Rule>: Types = <ut: WithPos<Rule>> =>?
-    Types::try_from(ut)
-        .map_err(|e| lalrpop_util::ParseError::User{error: e});
+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: Types> <r: @R> => MetaValue {
+    "|" <l: @L> <ty_res: CheckUnbound<Types>> <r: @R> => MetaValue {
         doc: None,
         types: None,
         contracts: vec![Contract {types: ty_res.clone(), label: mk_label(ty_res, src_id, l, r)}],
@@ -63,7 +45,7 @@ AnnotAtom: MetaValue = {
         priority: Default::default(),
         value: None,
     },
-    ":" <l: @L> <ty_res: Types> <r: @R> => MetaValue {
+    ":" <l: @L> <ty_res: CheckUnbound<Types>> <r: @R> => MetaValue {
         doc: None,
         types: Some(Contract {types: ty_res.clone(), label: mk_label(ty_res, src_id, l, r)}),
         contracts: Vec::new(),
@@ -185,33 +167,6 @@ RecordOperationChain: RichTerm = {
         mk_app!(mk_term::op2(BinaryOp::DynExtend(), id, r), t),
 };
 
-RowTail: Types = {
-    <Ident> => Types(AbsType::Var(<>)),
-    "Dyn" => Types(AbsType::Dyn()),
-}
-
-UniRecord: UniRecord = {
-   "{" <fields: (<RecordField> ",")*>
-       <last: RecordLastField?>
-       <l: @L> <tail: (";" RowTail)?> <r: @R>
-   "}" => {
-        let (last_field, attrs) = match last {
-            Some(RecordLastField::Field(f)) => (Some(f), Default::default()),
-            Some(RecordLastField::Ellipsis) =>
-                (None, RecordAttrs { open: true }),
-            None => (None, Default::default())
-        };
-
-        let fields : Vec<_> = fields.into_iter().chain(last_field.into_iter()).collect();
-        UniRecord {
-            fields,
-            tail: tail.map(|t| (t.1, mk_pos(src_id, l, r))),
-            attrs,
-            pos: TermPos::None
-        }
-    },
-};
-
 Atom: RichTerm = {
     "(" <CurriedOp> ")",
     "(" <Term> ")",
@@ -220,9 +175,19 @@ Atom: RichTerm = {
     Bool => RichTerm::from(Term::Bool(<>)),
     StrChunks,
     Ident => RichTerm::from(Term::Var(<>)),
-    AsTerm<UniRecord>,
     "`" <EnumTag> => RichTerm::from(Term::Enum(<>)),
-     "[" <terms: (<Term> ",")*> <last: Term?> "]" => {
+    "{" <fields: (<RecordField> ",")*> <last: RecordLastField?> "}" => {
+        let (last_field, attrs) = match last {
+            Some(RecordLastField::Field(f)) => (Some(f), Default::default()),
+            Some(RecordLastField::Ellipsis) =>
+                (None, RecordAttrs { open: true }),
+            None => (None, Default::default())
+        };
+
+        let fields = fields.into_iter().chain(last_field.into_iter());
+        RichTerm::from(build_record(fields, attrs))
+    },
+    "[" <terms: (<Term> ",")*> <last: Term?> "]" => {
         let terms : Vec<RichTerm> = terms.into_iter()
             .chain(last.into_iter()).collect();
         RichTerm::from(Term::List(terms))
@@ -605,6 +570,11 @@ BaseType: Types = {
     "Str" => Types(AbsType::Str()),
 };
 
+RowTail: Types = {
+    <Ident> => Types(AbsType::Var(<>)),
+    "Dyn" => Types(AbsType::Dyn()),
+}
+
 subType : Types = {
     <BaseType>,
     "List" <ty: subType?> => {
@@ -633,7 +603,25 @@ subType : Types = {
             );
         Types(AbsType::Enum(Box::new(ty)))
     },
-    AsTypes<UniRecord>,
+    "{" <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(<>))),
 };
 
@@ -662,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),
diff --git a/src/label.rs b/src/label.rs
index 2ee0509e..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")),
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 671f8d76..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("$")]
@@ -335,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.
@@ -439,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"),
         }
@@ -459,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"),
@@ -481,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"),
         }
@@ -496,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"),
         }
@@ -507,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),
                 };
@@ -568,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
@@ -647,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 4a70384c..00000000
--- a/src/parser/uniterm.rs
+++ /dev/null
@@ -1,143 +0,0 @@
-//! Additional AST nodes for the common UniTerm syntax (see RFC002 for more details).
-use super::*;
-use crate::types::UnboundTypeVariableError;
-use error::ParseError;
-use utils::{build_record, FieldPathElem};
-
-use crate::{
-    position::{RawSpan, TermPos},
-    term::{MergePriority, MetaValue, RecordAttrs, RichTerm, Term},
-    types::{AbsType, Types},
-};
-
-use std::convert::TryFrom;
-
-/// A record in the UniTerm syntax.
-#[derive(Clone)]
-pub struct UniRecord {
-    pub fields: Vec<(FieldPathElem, RichTerm)>,
-    pub tail: Option<(Types, TermPos)>,
-    pub attrs: RecordAttrs,
-    pub pos: TermPos,
-}
-
-/// Error indicating that a construct is not allowed when trying to interpret an `UniRecord` as a
-/// record type in a strict way. See [`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 if 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> {
-        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, (path_elem, rt)| {
-                    match path_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.
-    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(|ty| {
-                    ty.contract().map_err(|UnboundTypeVariableError(id)| {
-                        ParseError::UnboundTypeVariables(vec![id], pos.unwrap())
-                    })
-                })
-        } else {
-            Ok(RichTerm::from(build_record(
-                ur.fields.into_iter(),
-                ur.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 as
-    /// a flat type.
-    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))))
-        }
-    }
-}
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index e890ca5f..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
@@ -302,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,
@@ -534,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 5a634b8e..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 {
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 5c3bf65e..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),
         }
     }
 }
@@ -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/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/mod.rs b/src/typecheck/mod.rs
index bcf09f67..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;
@@ -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(())
         }
diff --git a/src/types.rs b/src/types.rs
index c058cb06..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
@@ -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/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.
 


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/contracts_fail.rs b/tests/contracts_fail.rs
index 5ae5316c..473c5876 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -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,8 +172,8 @@ 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!("{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)");
 }
 
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
index 60d6833a..532b819c 100644
--- a/tests/pass/contracts.ncl
+++ b/tests/pass/contracts.ncl
@@ -61,10 +61,10 @@ 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) &&
@@ -75,7 +75,7 @@ let Assert = fun l x => x || %blame% l in
     (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 =
+    (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"
@@ -83,10 +83,10 @@ let Assert = fun l x => x || %blame% l in
   ),
 
   // 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},
diff --git a/tests/pass/strings.ncl b/tests/pass/strings.ncl
index 6ed8c7b9..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
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index 8d476f8b..85a47dd0 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -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/typecheck_fail.rs b/tests/typecheck_fail.rs
index 2e82d86d..0468c9e8 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -114,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)"
     );
@@ -185,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);
@@ -201,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 ffb871b0..00000000
--- a/tests/unbound_type_variables.rs
+++ /dev/null
@@ -1,35 +0,0 @@
-use assert_matches::assert_matches;
-use nickel::{
-    error::{Error, ParseError, ParseErrors},
-    identifier::Ident,
-};
-
-use utilities::eval;
-
-macro_rules! assert_unbound {
-    ( $term:expr, $var:expr ) => {
-        let res = eval($term);
-        assert_matches!(res, Err(Error::ParseErrors(_)));
-
-        match res {
-            Err(Error::ParseErrors(ParseErrors {errors})) => {
-                assert_matches!(errors.as_slice(), [ParseError::UnboundTypeVariables(vars, _)] if vars.contains(&Ident::from($var)) && vars.len() == 1)
-            }
-            _ => unreachable!(),
-        };
-    }
-}
-
-#[test]
-fn unbound_type_variables() {
-    assert_unbound!("1 | a", "a");
-    assert_unbound!(
-        "null | forall a b c. a -> (b -> List c) -> {foo : List {_ : d}, bar: b; Dyn}",
-        "d"
-    );
-    assert_unbound!(
-        "null | forall a b c. a -> (b -> List c) -> {foo : List {_ : a}, bar: b; e}",
-        "e"
-    );
-    assert_unbound!("null | a -> (forall a. a -> a)", "a");
-}