Repository: tweag/nickel
Pull request #839 (2022-09-19 17:21:21)

Maintain a term environment during an REPL session
Follow up of #766 and #834. Correctly check for contract equality during an REPL session, by providing an initial context (typing environment + term environment), instead of just a typing environment, to various typechecking.

Sadly, we don't really use the machinery introduced in #834, because that would require to use `GenericTypeWrapper<E>` instead of `TypeWrapper` in a lot of places inside the `typecheck` module, which is a verbose and heavy change. Thus we somehow maintain two environments which contain the same information but in slightly different form (`eval_env` and `term_env`), but the overhead is expected to be insignificant and it lets the meat of the `typecheck` module untouched.

Depends on #834


Patch:
diff --git a/benches/arrays.rs b/benches/arrays.rs
index 896d90f5..f4d14a9e 100644
--- a/benches/arrays.rs
+++ b/benches/arrays.rs
@@ -1,7 +1,5 @@
-use std::rc::Rc;
-
 use criterion::{criterion_main, Criterion};
-use nickel_lang::term::{array::Array, ArrayAttrs, RichTerm, Term};
+use nickel_lang::term::{ArrayAttrs, RichTerm, Term};
 use nickel_lang_utilities::{ncl_bench_group, EvalMode};
 use pprof::criterion::{Output, PProfProfiler};
 use pretty::{BoxAllocator, DocBuilder, Pretty};
@@ -20,10 +18,7 @@ fn ncl_random_array(len: usize) -> String {
         numbers.push(RichTerm::from(Term::Num(acc as f64)));
     }
 
-    let xs = RichTerm::from(Term::Array(
-        Array::new(Rc::from(numbers)),
-        ArrayAttrs::default(),
-    ));
+    let xs = RichTerm::from(Term::Array(numbers, ArrayAttrs::default()));
     let doc: DocBuilder<_, ()> = xs.pretty(&BoxAllocator);
     let mut out = Vec::new();
     doc.render(80, &mut out).unwrap();
diff --git a/benches/nixpkgs/lists.ncl b/benches/nixpkgs/lists.ncl
index 30b57e12..987b1d7c 100644
--- a/benches/nixpkgs/lists.ncl
+++ b/benches/nixpkgs/lists.ncl
@@ -233,16 +233,16 @@
     # Predicate
     pred => foldl_ (fun c x => if pred x then c + 1 else c) 0,
 
-  optional': forall a. Bool -> a -> Array a
+  optional: forall a. Bool -> a -> Array a
   | doc m%"
       Return a singleton list or an empty list, depending on a boolean
      value.  Useful when building lists with optional elements
-     (e.g. `++ optional' (system == "i686-linux") firefox').
+     (e.g. `++ optional (system == "i686-linux") firefox').
 
      Example:
-       optional' true "foo"
+       optional true "foo"
        >> [ "foo" ]
-       optional' false "foo"
+       optional false "foo"
        >> [ ]
   "%m
   = fun cond elem => if cond then [elem] else [],
diff --git a/benches/stdlib.rs b/benches/stdlib.rs
index 62f0739a..a4757b47 100644
--- a/benches/stdlib.rs
+++ b/benches/stdlib.rs
@@ -6,7 +6,7 @@ use nickel_lang::cache::{Cache, ErrorTolerance};
 pub fn typecheck_stdlib(c: &mut Criterion) {
     let mut cache = Cache::new(ErrorTolerance::Strict);
     cache.load_stdlib().unwrap();
-    let type_env = cache.mk_type_env().unwrap();
+    let type_env = cache.mk_type_ctxt().unwrap();
     c.bench_function("typecheck stdlib", |b| {
         b.iter_batched(
             || cache.clone(),
diff --git a/doc/manual/correctness.md b/doc/manual/correctness.md
index 619cab4c..595ad347 100644
--- a/doc/manual/correctness.md
+++ b/doc/manual/correctness.md
@@ -4,83 +4,77 @@ slug: correctness
 
 # Correctness in Nickel
 
-One of the main value propositions of Nickel is to make configurations
-programmable. However, an equally important aim is to help developers write
-*correct* configurations. Our definition of correctness includes, but is not
-restricted to, the following properties:
-
-1. Evaluation of nonsensical expressions is not permitted. For example, trying
-   to add a number to a string, or calling a value which is not a function.
-2. Generated configurations are valid. For example, a program may be correct
-   with respect to the previous point while mistakenly outputting a field
-   `prto = "80"` instead of `port = 80`. This means consumers of this
-   configuration are likely to fail. Typically, validity involves respecting
-   some data schema.
-
-Because Nickel is an interpreted language, there is no well-defined
-*ahead-of-time* phase during which errors can be detected once and for all[^1].
-In practice, errors will still be raised when trying to run the program.
-However, what Nickel *can* do is vastly improve the troubleshooting experience
-by providing:
-
-1. an ergonomic way to express properties of code and data which should be
-   checked,
-2. mechanisms to catch violations as early as possible (i.e., before a code path
-   is triggered),
-3. informative error messages.
+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 outputting 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, which can have obvious
-benefits for many kinds of application. However, the case of an interpreted
-configuration language is somewhat less clear-cut.
-
-For pure configuration code, consisting predominantly of data, static typing is
-perhaps less useful than in other kinds of application. Firstly, a configuration
-is a terminating program run once on fixed inputs, so basic type errors will
-show up at runtime. Secondly, for data validation, static types are too rigid.
-For example, statically checking that an expression will always evaluate to a
-valid port number requires very advanced machinery. On the other hand, checking
-this property at runtime is trivial.
-
-Nevertheless, those who have faced puzzling [dynamic type errors], may desire
-something better. Bare dynamic typing is prone to irrelevant error messages,
-pointing to locations far from the problematic code. This is especially true
-when working with functions, which may be called with incorrect values which
-eventually break evaluation in a distant and seemingly unrelated place. In these
-cases, static typing can provide huge benefits.
-
-[dynamic type errors]: https://haskellforall.com/2021/01/dynamic-type-errors-lack-relevance.html
+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 through a combination of *gradual
-typing* and *contracts*. Gradual typing is a typing discipline where both static
-and dynamic typing may be used at will. Contracts augment dynamic typing by
-giving developers a principled and ergonomic way to enforce arbitrary assertions
-at runtime.
+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 does not, to fail with
-an informative error message.
-
-A wide range of properties can be checked for, such as:
-
-- that an expression evaluates to a number,
-- that some field `foo` evaluates to the same value as some other field `bar` of
-  the same configuration,
-- that an expression evaluates to a record with at least one field, `port`,
-  whose value is a valid port number,
-- that a given expression is a function mapping numbers to numbers
+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.
 
-Types and contracts are enforced in a similar way, via annotations.
-
-Type annotations are introduced with `:`. For example:
+Both types and contracts are enforced in a similar way, using an annotation:
 
 ```text
 $ nickel repl
-
 nickel> 1 + 1.5 : Num
 2.5
 
@@ -88,16 +82,6 @@ nickel> let f : Num -> Num = fun x => x + 1
 nickel> f 0
 1
 
-nickel> "not a Num" : Num
-error: incompatible types
-[..]
-```
-
-Contract annotations are introduced with `|`. For example:
-
-```text
-$ nickel repl
-
 nickel> let GreaterThan = fun bound =>
   contract.from_predicate (fun val => val >= bound) in
 -1 | GreaterThan 10
@@ -106,21 +90,21 @@ error: contract broken by value
 [..]
 ```
 
-Both type and contract annotations support the same syntax for properties on
-their right-hand side.
+`:` 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, whereas
-contract annotations are checked lazily, at run-time**. The characteristics and
-use-cases of types and contracts directly follow from this distinction.
+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 following sections, we consider two typical examples to illustrate the
-practical differences between types and contracts.
+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 arrays
 
-Suppose we need a function to convert an array of key-value pairs into an array
-of keys and an array of values. Let's call it `split`:
+Say we need a function to convert an array of key-value pairs to an array of keys
+and an array of values. Let's call it `split`:
 
 ```text
 nickel> split [{key = "foo", value = 1}, {key = "bar", value = 2}]
@@ -134,9 +118,8 @@ nickel> split [
 { keys: ["firewall", "grsec", "iptables"], values [true, false, true] }
 ```
 
-Here is the definition for `split`, but with a twist. On line 6 we accidentally
-try to pass the string `pair.key` to the concatenation operation `@`, without
-first wrapping it in an array:
+Here is the definition for `split`, but with a twist. We mistakenly forgot to
+wrap `pair.key` as an array before concatenating at line 6:
 
 ```nickel
 # lib.ncl
@@ -153,7 +136,7 @@ first wrapping it in an array:
 }
 ```
 
-We call `split` from our configuration file:
+And we call to split from our configuration:
 
 ```nickel
 # config.ncl
@@ -161,171 +144,145 @@ let {split} = import "lib.ncl" in
 split [{key = "foo", value = 1}, {key = "bar", value = 2}]
 ```
 
-We wish to ensure that the callers to `split` pass an array with the following
-properties:
+We want to ensure that the callers to `split` pass an array
+verifying:
 
-- elements are records with `key` and `value` fields,
-- `key`s are strings,
-- `value`s can be anything, but all must have the same type.
+- 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 returns a record with fields `keys`
-and `values`, where `keys` is an array of strings, and `values` is an array of
-elements of the same type as the input `value`s.
+We also want to make sure our implementation correctly returns a value which is
+a record with a field `keys` that is an array of strings, and a field `values`
+that is an array of elements of the same type as the input values.
 
-An idiomatic way to express these properties in Nickel is to use the following
-annotation:
+An idiomatic way to express these properties in Nickel is to use the annotation
 
 ```nickel
 forall a. Array {key: Str, value: a}
           -> {keys: Array Str, values: Array a}
 ```
 
-Where `forall a.` means that `a` can be any type, but that the `a` in the input
-type must match the `a` in the output type.
-
-We'll now consider the differences that arise when enforcing this specification
-using contract and type annotations.
+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
 
-`split` can be given a contract annotation as follows:
-
-```nickel
-split | forall a. Array {key: Str, value: a} -> {keys: Array Str, values: Array a} = # etc.
-```
-
-Contract annotations are checked at runtime. At this point functions are
-essentially opaque values which must be passed an argument in order to evaluate
-further. As a result, `split`'s contract will only be checked when the function
-is actually applied to an argument. When this happens, the contract checks that:
+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 provided argument satisfies the `Array {key: Str, value: a}` contract,
-2. the return value satisfies the `{keys: Array Str, values: Array a}` contract.
+1. The argument satisfies the `Array {key: Str, value: a}` contract.
+2. The return value satisfies the `{keys: Array Str, values: Array a}` contract.
 
 Those checks produce useful error message when the caller passes arguments of
-the wrong type, or if function were to return a value of the wrong type. But the
+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 values arising from concrete calls. In particular, if `split`
-  is not called - e.g. when part of a library - no checks take place. This can
-  be tested by evaluating or typechecking `lib.ncl` and observing that no errors
-  are raised.
-- Only the input value and the return value are checked against the contract. If
-  `split` mishandles an intermediate value - as indeed it currently does - then
-  the caller is left with only unhelpful dyamic type errors. For example,
-  evaluating `config.ncl` reports the following error:
-
-  ```text
-  error: type error
-    ┌─ /path/to/lib.ncl:6:27
-    │
-  6 │         keys = acc.keys @ pair.key,
-    │                           ^^^^^^^^ this expression has type Str, but Array was expected
-    │
-    ┌─ /path/to/config.ncl:2:41
-    │
-  2 │ split [{key = "foo", value = 1}, {key = "bar", value = 2}]
-    │                                         ----- evaluated to this
-    │
-    = @, 2nd operand
-
-  ```
-
-  From the caller's perspective, this is not a particularly helpful error. For
-  one thing, it points inside the body of `split`, which the caller may not
-  easily be able to change. At the same time, it points to the `key = "bar"`
-  part of the argument, which is not problematic and indeed respects the
-  contract.
+- 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:
+
+     ```text
+     error: Type error
+       ┌─ repl-input-12:6:27
+       │
+     6 │         keys = acc.keys @ pair.key,
+       │                           ^^^^^^^^ This expression has type Str, but Array 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 builtin types, which makes it a good
-candidate for static typing. The presence of static types here will help ensure
-that:
+`split` is a generic function operating on builtin types. This is a good
+candidate for static typing, which will help:
 
-1. the property expressed in the annotation above holds for all possible values
-   of the type parameter `a`,
-2. all expressions in the body of `split` also typecheck,
-3. errors are reported before any code is executed.
+- 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.
 
-`split` can be given a type annotation as follows:
+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.
 
-```nickel
-split : forall a. Array {key: Str, value: a} -> {keys: Array Str, values: Array a} = # etc.
-```
-
-Type annotations also give rise to contracts, which means that even if `split`'s
-callsite is not statically typed, problems with arguments or the return value
-will still be caught and reported correctly. (See the [documentation on static
-typing](./typing.md) for more details).
-
-Intermediate values are also typechecked. Evaluating or typechecking `lib.ncl`
-now reports an error:
+What's more, intermediate values are also typechecked. Evaluating or just
+typechecking `lib.ncl` already reports an error:
 
 ```text
-error: incompatible rows declaration
-   ┌─ /path/to/lib.ncl:10:7
-   │
-10 │       pairs
-   │       ^^^^^ this expression
-   │
+error: Incompatible rows declaration
+  ┌─ repl-input-14:9:7
+  │
+9 │       pairs
+  │       ^^^^^ this expression
 [..]
-error: While typing field `key`: incompatible types
+error: While typing field `key`: Incompatible types
  = The type of the expression was expected to be `Array Str`
  = The type of the expression was inferred to be `Str`
  = These types are not compatible
-
 ```
 
-The error says that the `key` field of the elements of `pairs` is a string, but
-because of the call to `fold`, it was expected to be lists of strings.
+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 the example above, it may seem that when it comes to functions,
-typechecking is superior to contract validation in every respect. Typechecking
-is more exhaustive and errors are reported earlier. In return, however,
-typechecking can cause valid programs to be rejected, and the properties which
-can be checked are limited. For example, checking that a function always returns
-a positive number is outside the scope of typechecking.
-
-In such cases, function contracts can help fill the gap.
-
-### Case 2: checking a custom property
+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.
 
-The previous example used only builtin types: functions, records, lists, and
-strings. It is likely that in the course of validating a configuration, you
-may wish to check more elaborate properties. This can be done by writing a
-custom contract.
+### Case 2: a custom property
 
-For example, `OptLevel` is a contract which checks that a provided optimization
-level is valid:
+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
-# lib.ncl
+let OptLevel = contract.from_predicate (fun value =>
+    array.elem value ["O0", "O1", "O2", "O3"]) in
 {
-  OptLevel = contract.from_predicate (fun value =>
-    array.elem value ["O0", "O1", "O2", "O3"])
+  opt_level = "O2",
 }
 ```
 
-The details of the implementation can be ignored for now. It is enough to know
-that a value passes the check if it is one of `"O0"`, `"O1"`, `"O2"` or `"O3"`.
-Writing custom contracts is covered in more detail in [the relevant documentation](./contracts.md).
-
-As in the previous example, we will consider the differences arising when using
-`OptLevel` as a type and contract annotation.
+`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
-# config.ncl
-let {OptLevel} = import "lib.ncl" in
 let level = 1 in
 {
-  opt_level : OptLevel = "A" ++ string.from_num level,
+  opt_level : OptLevel = "0" ++ string.from_num level,
 }
 ```
 
@@ -333,9 +290,9 @@ We get:
 
 ```text
 error: incompatible types
-  ┌─ /path/to/config.ncl:4:26
+  ┌─ repl-input-0:3:26
   │
-4 │   opt_level : OptLevel = "A" ++ string.from_num level,
+3 │   opt_level : OptLevel = "0" ++ string.from_num level,
   │                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ this expression
   │
   = The type of the expression was expected to be `OptLevel`
@@ -343,28 +300,21 @@ error: incompatible types
   = These types are not compatible
 ```
 
-Because `OptLevel` is a custom predicate, the typechecker is unable to check
-whether `"A"` concatenated with `string.from_num 1"` is a valid value. For that
-matter, even `"O1" : OptLevel` doesn't typecheck.
-
-It *is* possible to build values which the typechecker will accept as valid
-`OptLevel`s, but doing so creates restrictions on how the value can be used
-in typed code, so it's not what we want here. For more information see [the
-relevant section in the typing documentation].
-
-[the relevant section in the typing documentation]: ./typing.md#using-contracts-as-types
+Because `OptLevel` is a custom predicate, the typechecker can't prove that `"0"`
+concatenated with `string.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 validating custom properties such as `OptLevel`, a contract is the way to
-go:
+For such custom properties, a contract is the way to go:
 
 ```nickel
-# config.ncl
-let {OptLevel} = import "lib.ncl" in
 let level = 4 in
 {
-  opt_level | OptLevel = "A" ++ string.from_num level,
+  opt_level | OptLevel = "0" ++ string.from_num level,
 }
 ```
 
@@ -377,42 +327,36 @@ error: contract broken by a value.
 1 │ OptLevel
   │ -------- expected type
   │
-  ┌─ /path/to/config.ncl:4:26
+  ┌─ repl-input-4:3:27
   │
-3 │   opt_level | OptLevel = "A" ++ string.from_num level,
+3 │   opt_level | OptLevel = "0" ++ string.from_num level,
   │                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^ applied to this expression
   │
   ┌─ <unknown> (generated by evaluation):1:1
   │
-1 │ "A4"
+1 │ "04"
   │ ---- evaluated to this value
 ```
 
 ### Summary
 
-Types and contracts are the two mechanisms to ensure the correctness of Nickel
-programs.
-
-Typechecking is a static, ahead-of-time mechanism, which is exhaustive
-and reports errors early, but is rigid and limited in the properties which can
-be checked.
-
-Contract checking is a runtime mechanism, meaning contracts are more flexible
-and able to enforce arbitrary user-defined properties. However, contract
-checking alone may report fewer errors than typechecking, and report them later.
-
-As a rule of thumb, types should usually be used for functions operating on
-fairly generic data. Contracts work best on data, and are especially useful
-for data that will end up in a final configuration. When enforcing custom
-properties which are outside the scope of builtin types, contracts work best
-for both functions and data.
-
-An in-depth explanation of the type system and how to use it can be found in the
-[typing section](./typing.md). For contracts, refer to the [contracts section](./contracts.md).
-
-[^1]: The use of "well-defined" here is somewhat nuanced. Using the Nickel LSP
-      server in an editor, for example, does perform checks ahead of time, while
-      the program is being written. It is also possible to perform typechecking
-      separately before distributing a configuration using `nickel typecheck`.
-      However, a raw source program is not guaranteed to have been checked in
-      any way prior to execution.
+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/merging.md b/doc/manual/merging.md
index a5f4ac1b..63975c2a 100644
--- a/doc/manual/merging.md
+++ b/doc/manual/merging.md
@@ -254,64 +254,16 @@ final record:
 ## Merging record with metadata
 
 Metadata can be attached to values thanks to the `|` operator. Metadata
-currently includes contract annotations, default value, merge priority, and
-documentation. We describe in this section how metadata interacts with merging.
+currently includes contract annotations, default value, and documentation. We
+describe in this section how metadata interacts with merging.
 
-### Merge priorities
-
-Priorities are specified using the `priority` annotation, followed by a number
-literal. There are also two other special priorities, the bottom priority, specified
-using the `default` annotation, and the top priority, specified using the
-`force` annotation.
-
-Priorities dictate which values take precedence over other values. By default,
-values are given the priority `0`. Values with the same priority are recursively
-merged as specified in this document, which can mean failure if the values can't
-be meaningfully merged:
-
-```text
-nickel> {foo = 1} & {foo = 2}
-error: non mergeable terms
-  ┌─ repl-input-1:1:8
-  │
-1 │ {foo = 1} & {foo = 2}
-  │        ^           ^ with this expression
-  │        │
-  │        cannot merge this expression
-  │
-  = Both values have the same merge priority but they can't be combined
-```
-
-On the other hand, if the priorities differ, the value with highest priority
-simply erases the other in the final result:
-
-```text
-nickel> {foo | priority 1 = 1} & {foo = 2}
-{ foo = 1 }
-
-nickel> {foo | priority -1 = 1} & {foo = 2}
-{ foo = 2 }
-```
-
-The priorities are ordered in the following way:
-
-- bottom is the lowest priority
-- numeral priorities are ordered as usual numbers (priorities can be any valid Nickel
-  number, including fractions and negative values)
-- top is the highest priority
-
-#### Default values
+### Default values
 
 A `default` annotation can be used to provide a base value, but let it be
 overridable through merging. For example, `{foo | default = 1} & {foo = 2}`
-evaluates to `{foo = 2}`. A default value is just a special case of a priority,
-being the lowest possible one.
-
-#### Forcing values
-
-Dually, values with the `force` annotation are given the highest priority. Such
-a value can never be overriden, and will either take precedence over another
-value or be tentatively merged if the other value is forcing as well.
+evaluates to `{foo = 2}`. Without the default value, this merge would have
+failed with a `non mergeable fields` error, because merging being symmetric, it
+doesn't know how to combine `1` and `2` in a generic and meaningful way.
 
 #### Specification
 
@@ -332,6 +284,10 @@ same on both side:
 }
 ```
 
+Currently, there are only two priorities, `normal` (by default, when nothing is
+specified) and the `default` one, with `default < normal`. We plan to add more
+in the future (see [RFC001](https://github.com/tweag/nickel/blob/c21cf280dc610821fceed4c2caafedb60ce7177c/rfcs/001-overriding.md#priorities)).
+
 #### Example
 
 Let us stick to our firewall example. Thanks to default values, we set the most
diff --git a/doc/manual/syntax.md b/doc/manual/syntax.md
index f4b1b023..d9ab9181 100644
--- a/doc/manual/syntax.md
+++ b/doc/manual/syntax.md
@@ -12,7 +12,7 @@ alphanumeric characters, `_` (underscores) or `'` (single quotes). For example,
 
 ## Simple values
 
-There are four basic kinds of values in Nickel :
+There are four basic kind of values in Nickel :
 
 1. numeric values
 2. boolean values
@@ -532,14 +532,9 @@ Adding documentation can be done with `| doc < string >`. Examples:
 true
 ```
 
-Metadata can also set merge priorities using the following annotations:
-
-- `default` gives the lowest priority (default values)
-- `priority NN`, where `NN` is a number literal, gives a numeral priority
-- `force` gives the highest priority
-
-If there is no priority specified, `priority 0` is given by default. See more
-about this in the dedicated section on merging.
+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:
 
@@ -557,13 +552,4 @@ Examples:
 
 > {foo | default = 1, bar = foo + 1} & {foo = 2}
 { foo = 2, bar = 3 }
-
-> {foo | force = 1, bar = foo + 1} & {foo = 2}
-{ bar = 2, foo = 1 }
-
-> {foo | priority 10 = 1} & {foo | priority 8 = 2} & {foo = 3}
-{ foo = 1 }
-
-> {foo | priority -1 = 1} & {foo = 2}
-{ foo = 2 }
 ```
diff --git a/examples/merge-priorities/README.md b/examples/merge-priorities/README.md
deleted file mode 100644
index 3951f2f1..00000000
--- a/examples/merge-priorities/README.md
+++ /dev/null
@@ -1,12 +0,0 @@
-# Merge priorities
-
-This example is a variant of the merge example that makes use of merge
-priorities. The code to run lies in `main.ncl`. The default value
-`firewall.enabled` defined in `security.ncl` is overwritten in the final
-configuration.
-
-## Run
-
-```console
-nickel -f main.ncl export
-```
diff --git a/examples/merge-priorities/main.ncl b/examples/merge-priorities/main.ncl
deleted file mode 100644
index ac87ec9c..00000000
--- a/examples/merge-priorities/main.ncl
+++ /dev/null
@@ -1,20 +0,0 @@
-# Merge several blocks into one final configuration. In a real world case, one
-# would also want contracts to validate the shape of the data.
-let server = import "server.ncl" in
-let security = import "security.ncl" in
-# Disabling firewall in the final result
-server & security & {
-  # As opposed to the simple merge example, this would now fail
-  # firewall.enabled = false
-
-  firewall.open_ports | priority 10 = [80],
-  firewall.type = "superiptables",
-  server.host.ip = "89.22.11.01",
-
-  # this will only be selected if no values with higher priority (or no priority
-  # annotation, which is the same as priority 0) is ever defined
-  # because there's a definite value below, this won't be selected.
-  server.host.name | priority -1 = "hello-world.backup.com",
-} & {
-  server.host.name = "hello-world.main.com",
-}
diff --git a/examples/merge-priorities/security.ncl b/examples/merge-priorities/security.ncl
deleted file mode 100644
index ffcc5ad0..00000000
--- a/examples/merge-priorities/security.ncl
+++ /dev/null
@@ -1,8 +0,0 @@
-{
-  server.host.options | priority 10 = "TLS",
-
-  # force make it impossible to override this value with false
-  firewall.enabled | force = true,
-  firewall.type | default = "iptables",
-  firewall.open_ports | priority 5 = [21, 80, 443],
-}
diff --git a/examples/merge-priorities/server.ncl b/examples/merge-priorities/server.ncl
deleted file mode 100644
index 9474686a..00000000
--- a/examples/merge-priorities/server.ncl
+++ /dev/null
@@ -1,5 +0,0 @@
-{
-  server.host.ip | default = "182.168.1.1",
-  server.host.port | default = 80,
-  server.host.name | default = "hello-world.net",
-}
diff --git a/lsp/nls/src/cache.rs b/lsp/nls/src/cache.rs
index 5a174674..ae60d0cb 100644
--- a/lsp/nls/src/cache.rs
+++ b/lsp/nls/src/cache.rs
@@ -14,7 +14,7 @@ pub trait CacheExt {
     fn typecheck_with_analysis(
         &mut self,
         file_id: FileId,
-        initial_env: &typecheck::Environment,
+        initial_ctxt: &typecheck::Context,
         lin_cache: &mut HashMap<FileId, Completed>,
     ) -> Result<CacheOp<()>, CacheError<TypecheckError>>;
 }
@@ -35,7 +35,7 @@ impl CacheExt for Cache {
     fn typecheck_with_analysis<'a>(
         &mut self,
         file_id: FileId,
-        initial_env: &typecheck::Environment,
+        initial_ctxt: &typecheck::Context,
         lin_cache: &mut HashMap<FileId, Completed>,
     ) -> Result<CacheOp<()>, CacheError<TypecheckError>> {
         if !self.terms_mut().contains_key(&file_id) {
@@ -50,7 +50,7 @@ impl CacheExt for Cache {
         } else if *state >= EntryState::Parsed {
             let host = AnalysisHost::new();
             let (_, linearized) =
-                typecheck::type_check_linearize(term, initial_env.clone(), self, host)?;
+                typecheck::type_check_linearize(term, initial_ctxt.clone(), self, host)?;
             self.update_state(file_id, EntryState::Typechecked);
             lin_cache.insert(file_id, linearized);
             Ok(CacheOp::Done(()))
diff --git a/lsp/nls/src/files.rs b/lsp/nls/src/files.rs
index ce692bc7..b53d9902 100644
--- a/lsp/nls/src/files.rs
+++ b/lsp/nls/src/files.rs
@@ -72,7 +72,7 @@ pub fn handle_save(server: &mut Server, params: DidChangeTextDocumentParams) ->
 fn typecheck(server: &mut Server, file_id: FileId) -> Result<CacheOp<()>, Vec<Diagnostic<FileId>>> {
     server
         .cache
-        .typecheck_with_analysis(file_id, &server.initial_env, &mut server.lin_cache)
+        .typecheck_with_analysis(file_id, &server.initial_ctxt, &mut server.lin_cache)
         .map_err(|error| match error {
             CacheError::Error(tc_error) => tc_error.to_diagnostic(server.cache.files_mut(), None),
             CacheError::NotParsed => unreachable!(),
diff --git a/lsp/nls/src/server.rs b/lsp/nls/src/server.rs
index 358e91ec..41733d3c 100644
--- a/lsp/nls/src/server.rs
+++ b/lsp/nls/src/server.rs
@@ -17,7 +17,7 @@ use lsp_types::{
 };
 
 use nickel_lang::cache::{Cache, ErrorTolerance};
-use nickel_lang::typecheck::Environment;
+use nickel_lang::typecheck::Context;
 
 use crate::{
     linearization::completed::Completed,
@@ -29,7 +29,7 @@ pub struct Server {
     pub connection: Connection,
     pub cache: Cache,
     pub lin_cache: HashMap<FileId, Completed>,
-    pub initial_env: Environment,
+    pub initial_ctxt: Context,
 }
 
 impl Server {
@@ -61,13 +61,13 @@ impl Server {
     pub fn new(connection: Connection) -> Server {
         let mut cache = Cache::new(ErrorTolerance::Tolerant);
         cache.load_stdlib().unwrap();
-        let initial_env = cache.mk_type_env().unwrap();
+        let initial_ctxt = cache.mk_type_ctxt().unwrap();
         let lin_cache = HashMap::new();
         Server {
             connection,
             cache,
             lin_cache,
-            initial_env,
+            initial_ctxt,
         }
     }
 
diff --git a/src/cache.rs b/src/cache.rs
index 4dc9e0ae..d77b7f8d 100644
--- a/src/cache.rs
+++ b/src/cache.rs
@@ -86,22 +86,20 @@ pub enum ErrorTolerance {
     Strict,
 }
 
-/// wrapping eval environment with typing environment
+/// The different environments maintained during the REPL session for evaluation and typechecking.
 #[derive(Debug, Clone)]
 pub struct Envs {
     /// The eval environment.
     pub eval_env: eval::Environment,
-    /// The typing environment, counterpart of the eval environment for typechecking. Entries are
-    /// [`crate::typecheck::TypeWrapper`] for the ease of interacting with the typechecker, but
-    /// there are not any unification variable in it.
-    pub type_env: typecheck::Environment,
+    /// The typing context.
+    pub type_ctxt: typecheck::Context,
 }
 
 impl Envs {
     pub fn new() -> Self {
         Envs {
             eval_env: eval::Environment::new(),
-            type_env: typecheck::Environment::new(),
+            type_ctxt: typecheck::Context::new(),
         }
     }
 }
@@ -471,7 +469,7 @@ impl Cache {
     pub fn typecheck(
         &mut self,
         file_id: FileId,
-        initial_env: &typecheck::Environment,
+        initial_ctxt: &typecheck::Context,
     ) -> Result<CacheOp<()>, CacheError<TypecheckError>> {
         match self.terms.get(&file_id) {
             Some(CachedTerm { state, .. }) if *state >= EntryState::Typechecked => {
@@ -479,14 +477,14 @@ impl Cache {
             }
             Some(CachedTerm { term, state, .. }) if *state >= EntryState::Parsed => {
                 if *state < EntryState::Typechecking {
-                    let wildcards = type_check(term, initial_env.clone(), self)?;
+                    let wildcards = type_check(term, initial_ctxt.clone(), self)?;
                     self.update_state(file_id, EntryState::Typechecking);
                     self.wildcards.insert(file_id, wildcards);
                 }
 
                 if let Some(imports) = self.imports.get(&file_id).cloned() {
                     for f in imports.into_iter() {
-                        self.typecheck(f, initial_env)?;
+                        self.typecheck(f, initial_ctxt)?;
                     }
                 }
 
@@ -677,7 +675,7 @@ impl Cache {
     pub fn prepare(
         &mut self,
         file_id: FileId,
-        initial_env: &typecheck::Environment,
+        initial_ctxt: &typecheck::Context,
     ) -> Result<CacheOp<()>, Error> {
         let mut result = CacheOp::Cached(());
 
@@ -694,7 +692,7 @@ impl Cache {
             result = CacheOp::Done(());
         };
 
-        let typecheck_res = self.typecheck(file_id, initial_env).map_err(|cache_err| {
+        let typecheck_res = self.typecheck(file_id, initial_ctxt).map_err(|cache_err| {
             cache_err
                 .unwrap_error("cache::prepare(): expected source to be parsed before typechecking")
         })?;
@@ -729,14 +727,14 @@ impl Cache {
     pub fn prepare_nocache(
         &mut self,
         file_id: FileId,
-        initial_env: &typecheck::Environment,
+        initial_ctxt: &typecheck::Context,
     ) -> Result<(RichTerm, Vec<FileId>), Error> {
         let (term, errs) = self.parse_nocache(file_id)?;
         if errs.no_errors() {
             return Err(Error::ParseErrors(errs));
         }
         let (term, pending) = import_resolution::resolve_imports(term, self)?;
-        let wildcards = type_check(&term, initial_env.clone(), self)?;
+        let wildcards = type_check(&term, initial_ctxt.clone(), self)?;
         let term = transform::transform(term, Some(&wildcards))
             .map_err(|err| Error::ParseErrors(err.into()))?;
         Ok((term, pending))
@@ -858,7 +856,7 @@ impl Cache {
         // 1. The stdlib is meant to stay relatively light.
         // 2. Typechecking the standard library ought to occur only during development. Once the
         //    stdlib is stable, we won't have typecheck it at every execution.
-        let initial_env = self.mk_type_env().map_err(|err| match err {
+        let initial_env = self.mk_type_ctxt().map_err(|err| match err {
             CacheError::NotParsed => CacheError::NotParsed,
             CacheError::Error(_) => unreachable!(),
         })?;
@@ -869,12 +867,12 @@ impl Cache {
     /// it's used in benches. It probably does not have to be used for something else.
     pub fn typecheck_stdlib_(
         &mut self,
-        initial_env: &typecheck::Environment,
+        initial_ctxt: &typecheck::Context,
     ) -> Result<CacheOp<()>, CacheError<TypecheckError>> {
         if let Some(ids) = self.stdlib_ids.as_ref().cloned() {
             ids.iter()
                 .try_fold(CacheOp::Cached(()), |cache_op, file_id| {
-                    match self.typecheck(*file_id, initial_env)? {
+                    match self.typecheck(*file_id, initial_ctxt)? {
                         done @ CacheOp::Done(()) => Ok(done),
                         _ => Ok(cache_op),
                     }
@@ -894,7 +892,7 @@ impl Cache {
             return Ok(Envs::new());
         }
         self.load_stdlib()?;
-        let type_env = self.mk_type_env().unwrap();
+        let type_ctxt = self.mk_type_ctxt().unwrap();
 
         self.stdlib_ids
             .as_ref()
@@ -907,12 +905,15 @@ impl Cache {
                     .unwrap_error("cache::prepare_stdlib(): expected standard library to be parsed")
             })?;
         let eval_env = self.mk_eval_env().unwrap();
-        Ok(Envs { eval_env, type_env })
+        Ok(Envs {
+            eval_env,
+            type_ctxt,
+        })
     }
 
-    /// Generate the initial typing environment from the list of `file_ids` corresponding to the
+    /// Generate the initial typing context from the list of `file_ids` corresponding to the
     /// standard library parts.
-    pub fn mk_type_env(&self) -> Result<typecheck::Environment, CacheError<Void>> {
+    pub fn mk_type_ctxt(&self) -> Result<typecheck::Context, CacheError<Void>> {
         let stdlib_terms_vec =
             self.stdlib_ids
                 .as_ref()
@@ -926,7 +927,7 @@ impl Cache {
                         })
                         .collect())
                 })?;
-        Ok(typecheck::mk_initial_env(stdlib_terms_vec).unwrap())
+        Ok(typecheck::mk_initial_ctxt(&stdlib_terms_vec).unwrap())
     }
 
     /// Generate the initial evaluation environment from the list of `file_ids` corresponding to the standard
diff --git a/src/deserialize.rs b/src/deserialize.rs
index e7ea0ab4..591b743b 100644
--- a/src/deserialize.rs
+++ b/src/deserialize.rs
@@ -1,7 +1,6 @@
 //! Deserialization of an evaluated program to plain Rust types.
 
 use std::collections::HashMap;
-use std::iter::ExactSizeIterator;
 
 use serde::de::{
     Deserialize, DeserializeSeed, EnumAccess, IntoDeserializer, MapAccess, SeqAccess,
@@ -9,7 +8,6 @@ use serde::de::{
 };
 
 use crate::identifier::Ident;
-use crate::term::array::{self, Array};
 use crate::term::{MetaValue, RichTerm, Term};
 
 macro_rules! deserialize_number {
@@ -342,13 +340,13 @@ impl<'de> serde::Deserializer<'de> for RichTerm {
 }
 
 struct ArrayDeserializer {
-    iter: array::IntoIter,
+    iter: std::vec::IntoIter<RichTerm>,
 }
 
 impl ArrayDeserializer {
-    fn new(array: Array) -> Self {
+    fn new(vec: Vec<RichTerm>) -> Self {
         ArrayDeserializer {
-            iter: array.into_iter(),
+            iter: vec.into_iter(),
         }
     }
 }
@@ -389,7 +387,10 @@ fn unwrap_term(mut rich_term: RichTerm) -> Result<Term, RustDeserializationError
     }
 }
 
-fn visit_array<'de, V>(array: Array, visitor: V) -> Result<V::Value, RustDeserializationError>
+fn visit_array<'de, V>(
+    array: Vec<RichTerm>,
+    visitor: V,
+) -> Result<V::Value, RustDeserializationError>
 where
     V: Visitor<'de>,
 {
diff --git a/src/error.rs b/src/error.rs
index 3ac62f61..24afc4a3 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -1116,10 +1116,7 @@ impl ToDiagnostic<FileId> for EvalError {
 
                 vec![Diagnostic::error()
                     .with_message("non mergeable terms")
-                    .with_labels(labels)
-                    .with_notes(vec![String::from(
-                        "Both values have the same merge priority but they can't be combined",
-                    )])]
+                    .with_labels(labels)]
             }
             EvalError::UnboundIdentifier(ident, span_opt) => vec![Diagnostic::error()
                 .with_message("unbound identifier")
diff --git a/src/eval/mod.rs b/src/eval/mod.rs
index 282166dc..5ee3ef76 100644
--- a/src/eval/mod.rs
+++ b/src/eval/mod.rs
@@ -642,11 +642,9 @@ where
             // See the comment on the `BinaryOp::ArrayConcat` match arm.
             Term::Array(terms, attrs) if !attrs.closurized => {
                 let mut local_env = Environment::new();
-
                 let closurized_array = terms
-                    .clone()
-                    .into_iter()
-                    .map(|t| t.closurize(&mut local_env, env.clone()))
+                    .iter()
+                    .map(|t| t.clone().closurize(&mut local_env, env.clone()))
                     .collect();
 
                 let closurized_ctrs = attrs
diff --git a/src/eval/operation.rs b/src/eval/operation.rs
index 22dbcb41..7747d415 100644
--- a/src/eval/operation.rs
+++ b/src/eval/operation.rs
@@ -21,14 +21,14 @@ use crate::{
     position::TermPos,
     serialize,
     serialize::ExportFormat,
-    term::{array::Array, make as mk_term, PendingContract},
+    term::{make as mk_term, PendingContract},
     term::{ArrayAttrs, BinaryOp, NAryOp, RichTerm, StrChunk, Term, UnaryOp},
     transform::{apply_contracts::apply_contracts, fresh_var, Closurizable},
 };
 use md5::digest::Digest;
 use simple_counter::*;
+use std::collections::HashMap;
 use std::iter::Extend;
-use std::{collections::HashMap, rc::Rc};
 
 generate_counter!(FreshVariableCounter, usize);
 
@@ -472,7 +472,6 @@ fn process_unary_operation(
                         .collect();
                     fields.sort();
                     let terms = fields.into_iter().map(mk_term::string).collect();
-
                     Ok(Closure::atomic_closure(RichTerm::new(
                         Term::Array(terms, ArrayAttrs::new().closurized()),
                         pos_op_inh,
@@ -504,7 +503,7 @@ fn process_unary_operation(
                     Ok(Closure {
                         // TODO: once sure that the Record is properly closurized, we can
                         // safely assume that the extracted array here is, in turn, also closuried.
-                        body: RichTerm::new(Term::Array(terms, ArrayAttrs::default()), pos_op_inh),
+                        body: RichTerm::new(Term::Array(terms, Default::default()), pos_op_inh),
                         env,
                     })
                 }
@@ -731,7 +730,7 @@ fn process_unary_operation(
         }
         UnaryOp::ArrayHead() => {
             if let Term::Array(ts, attrs) = &*t {
-                if let Some(head) = ts.get(0) {
+                if let Some(head) = ts.first() {
                     let head_with_ctr = apply_contracts(
                         head.clone(),
                         attrs.pending_contracts.iter().cloned(),
@@ -756,9 +755,10 @@ fn process_unary_operation(
         }
         UnaryOp::ArrayTail() => match_sharedterm! {t, with {
                     Term::Array(ts, attrs) => {
-                        if !ts.is_empty() {
+                        let mut ts_it = ts.into_iter();
+                        if ts_it.next().is_some() {
                             Ok(Closure {
-                                body: RichTerm::new(Term::Array(ts.advance_by(1), attrs), pos_op_inh),
+                                body: RichTerm::new(Term::Array(ts_it.collect(), attrs), pos_op_inh),
                                 env,
                             })
                         } else {
@@ -858,7 +858,6 @@ fn process_unary_operation(
                     .chars()
                     .map(|c| RichTerm::from(Term::Str(c.to_string())))
                     .collect();
-
                 Ok(Closure::atomic_closure(RichTerm::new(
                     Term::Array(ts, ArrayAttrs::new().closurized()),
                     pos_op_inh,
@@ -1091,7 +1090,7 @@ fn process_unary_operation(
                 let capt = regex.captures(s);
                 let result = if let Some(capt) = capt {
                     let first_match = capt.get(0).unwrap();
-                    let groups = capt
+                    let groups: Vec<RichTerm> = capt
                         .iter()
                         .skip(1)
                         .filter_map(|s_opt| {
@@ -1112,10 +1111,7 @@ fn process_unary_operation(
                     mk_record!(
                         ("match", Term::Str(String::new())),
                         ("index", Term::Num(-1.)),
-                        (
-                            "groups",
-                            Term::Array(Array::default(), ArrayAttrs::default())
-                        )
+                        ("groups", Term::Array(Vec::new(), Default::default()))
                     )
                 };
 
@@ -1194,7 +1190,7 @@ fn process_unary_operation(
                             // It's important to collect here, otherwise the two usages below
                             // will each do their own .closurize(...) calls and end up with
                             // different variables, which means that `cont` won't be properly updated.
-                            .collect::<Array>();
+                            .collect::<Vec<_>>();
 
                         let terms = ts.clone().into_iter();
                         let cont = RichTerm::new(Term::Array(ts, attrs), pos.into_inherited());
@@ -2007,13 +2003,6 @@ fn process_binary_operation(
                             debug_assert!(attrs1.closurized, "the left-hand side of ArrayConcat (@) is not closurized.");
                             debug_assert!(attrs2.closurized, "the right-hand side of ArrayConcat (@) is not closurized.");
 
-                            // NOTE: To avoid the extra Vec allocation, we could use Rc<[T]>::new_uninit_slice()
-                            // and fill up the slice manually, but that's a nightly-only experimental API.
-                            // Note that collecting into an Rc<[T]> will also allocate a intermediate vector,
-                            // unless the input iterator implements the nightly-only API TrustedLen, and Array's iterator currently doesn't.
-                            // Even if we could implement TrustedLen we would have to contend with the fact that .chain(..) tends to be slow.
-                            // - Rc<[T]>::from_iter docs: https://doc.rust-lang.org/std/rc/struct.Rc.html#impl-FromIterator%3CT%3E
-                            // - chain issue: https://github.com/rust-lang/rust/issues/63340
                             let mut ts: Vec<RichTerm> = Vec::with_capacity(ts1.len() + ts2.len());
 
                             let mut env = env1.clone();
@@ -2054,7 +2043,7 @@ fn process_binary_operation(
                             };
 
                             Ok(Closure {
-                                body: RichTerm::new(Term::Array(Array::new(Rc::from(ts)), attrs), pos_op_inh),
+                                body: RichTerm::new(Term::Array(ts, attrs), pos_op_inh),
                                 env,
                             })
                         }
@@ -2092,7 +2081,7 @@ fn process_binary_operation(
                     Err(EvalError::Other(format!("elemAt: index out of bounds. Expected a value between 0 and {}, got {}", ts.len(), n), pos_op))
                 } else {
                     let elem_with_ctr = apply_contracts(
-                        ts.get(n_int).unwrap().clone(),
+                        ts[n_int].clone(),
                         attrs.pending_contracts.iter().cloned(),
                         pos1.into_inherited(),
                     );
@@ -2294,11 +2283,10 @@ fn process_binary_operation(
         }
         BinaryOp::StrSplit() => match (&*t1, &*t2) {
             (Term::Str(s1), Term::Str(s2)) => {
-                let array = s1
+                let array: Vec<RichTerm> = s1
                     .split(s2)
                     .map(|s| Term::Str(String::from(s)).into())
                     .collect();
-
                 Ok(Closure::atomic_closure(RichTerm::new(
                     Term::Array(array, ArrayAttrs::new().closurized()),
                     pos_op_inh,
diff --git a/src/parser/grammar.lalrpop b/src/parser/grammar.lalrpop
index 287dbd28..8decf3f6 100644
--- a/src/parser/grammar.lalrpop
+++ b/src/parser/grammar.lalrpop
@@ -60,8 +60,7 @@ use crate::{
     term::{
         BinaryOp, RichTerm, Term, UnaryOp, StrChunk, MetaValue,
         MergePriority, Contract, NAryOp, RecordAttrs, SharedTerm,
-        NumeralPriority, array::Array, make as mk_term,
-    },
+        make as mk_term},
     types::{Types, AbsType},
     position::TermPos,
     label::Label,
@@ -102,16 +101,7 @@ AnnotAtom<TypeRule>: MetaValue = {
         ..Default::default()
     },
     "|" "default" => MetaValue {
-        priority: MergePriority::Bottom,
-        ..Default::default()
-    },
-    "|" "force" => MetaValue {
-        priority: MergePriority::Top,
-        ..Default::default()
-    },
-    "|" "priority" <SignedNumLiteral> => MetaValue {
-        // unwrap(): a literal can't be NaN
-        priority: MergePriority::Numeral(NumeralPriority::try_from(<>).unwrap()),
+        priority: MergePriority::Default,
         ..Default::default()
     },
     "|" "doc" <s: StaticString> => MetaValue {
@@ -322,10 +312,8 @@ Atom: UniTerm = {
     UniRecord => UniTerm::from(UniTermNode::Record(<>)),
     <EnumTag> => UniTerm::from(Term::Enum(<>)),
     "[" <terms: (<Term> ",")*> <last: Term?> "]" => {
-        let terms = terms
-            .into_iter()
-            .chain(last.into_iter())
-            .collect();
+        let terms : Vec<RichTerm> = terms.into_iter()
+            .chain(last.into_iter()).collect();
 
         UniTerm::from(Term::Array(terms, Default::default()))
     },
@@ -439,7 +427,7 @@ Match: Match = {
 
 // A default annotation in a pattern.
 DefaultAnnot: MetaValue = "?" <t: Term> => MetaValue {
-    priority: MergePriority::Bottom,
+    priority: MergePriority::Default,
     value: Some(t),
     ..Default::default()
 };
@@ -544,7 +532,7 @@ UOp: UnaryOp = {
     "record_map" => UnaryOp::RecordMap(),
     "seq" => UnaryOp::Seq(),
     "deep_seq" => UnaryOp::DeepSeq(None),
-    "op force" => UnaryOp::Force(None),
+    "force" => UnaryOp::Force(None),
     "head" => UnaryOp::ArrayHead(),
     "tail" => UnaryOp::ArrayTail(),
     "length" => UnaryOp::ArrayLength(),
@@ -790,14 +778,6 @@ TypeAtom: Types = {
     },
 }
 
-SignedNumLiteral: f64 = <sign: "-"?> <value: "num literal"> => {
-    if sign.is_some() {
-        -value
-    } else {
-        value
-    }
-};
-
 extern {
     type Location = usize;
     type Error = ParseError;
@@ -869,7 +849,7 @@ extern {
         "typeof" => Token::Normal(NormalToken::Typeof),
         "assume" => Token::Normal(NormalToken::Assume),
         "array_lazy_assume" => Token::Normal(NormalToken::ArrayLazyAssume),
-        "op force" => Token::Normal(NormalToken::OpForce),
+        "force" => Token::Normal(NormalToken::Force),
         "blame" => Token::Normal(NormalToken::Blame),
         "chng_pol" => Token::Normal(NormalToken::ChangePol),
         "polarity" => Token::Normal(NormalToken::Polarity),
@@ -898,10 +878,8 @@ extern {
         "elem_at" => Token::Normal(NormalToken::ElemAt),
         "merge" => Token::Normal(NormalToken::Merge),
         "default" => Token::Normal(NormalToken::Default),
-        "force" => Token::Normal(NormalToken::Force),
         "doc" => Token::Normal(NormalToken::Doc),
         "optional" => Token::Normal(NormalToken::Optional),
-        "priority" => Token::Normal(NormalToken::Priority),
 
         "hash" => Token::Normal(NormalToken::OpHash),
         "serialize" => Token::Normal(NormalToken::Serialize),
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 543c0850..9dc25a83 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -186,7 +186,7 @@ pub enum NormalToken<'input> {
     #[token("%deep_seq%")]
     DeepSeq,
     #[token("%force%")]
-    OpForce,
+    Force,
     #[token("%head%")]
     Head,
     #[token("%tail%")]
@@ -216,10 +216,6 @@ pub enum NormalToken<'input> {
     Doc,
     #[token("optional")]
     Optional,
-    #[token("priority")]
-    Priority,
-    #[token("force")]
-    Force,
 
     #[token("%hash%")]
     OpHash,
diff --git a/src/parser/uniterm.rs b/src/parser/uniterm.rs
index 35c90ad7..b7ac1872 100644
--- a/src/parser/uniterm.rs
+++ b/src/parser/uniterm.rs
@@ -211,7 +211,7 @@ impl UniRecord {
                                         types: Some(ctrt),
                                         contracts,
                                         opt: false,
-                                        priority: MergePriority::Neutral,
+                                        priority: MergePriority::Normal,
                                         value: None,
                                     }) if contracts.is_empty() => Ok(Types(AbsType::RowExtend(
                                         id,
diff --git a/src/pretty.rs b/src/pretty.rs
index 27b22a71..4528d684 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -99,7 +99,7 @@ where
             }),
             self.line().clone(),
         ))
-        .append(if mv.priority == crate::term::MergePriority::Bottom {
+        .append(if mv.priority == crate::term::MergePriority::Default {
             self.line().append(self.text("| default"))
         } else {
             self.nil()
@@ -207,7 +207,7 @@ where
                                 MetaValue {
                                     types,
                                     contracts,
-                                    priority: crate::term::MergePriority::Bottom,
+                                    priority: crate::term::MergePriority::Default,
                                     value: Some(value),
                                     ..
                                 } => allocator
diff --git a/src/program.rs b/src/program.rs
index 35bafd65..92a14bd0 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -71,8 +71,11 @@ impl Program {
     /// Retrieve the parsed term and typecheck it, and generate a fresh initial environment. Return
     /// both.
     fn prepare_eval(&mut self) -> Result<(RichTerm, eval::Environment), Error> {
-        let Envs { eval_env, type_env } = self.cache.prepare_stdlib()?;
-        self.cache.prepare(self.main_id, &type_env)?;
+        let Envs {
+            eval_env,
+            type_ctxt,
+        } = self.cache.prepare_stdlib()?;
+        self.cache.prepare(self.main_id, &type_ctxt)?;
         Ok((self.cache.get(self.main_id).unwrap(), eval_env))
     }
 
@@ -104,7 +107,7 @@ impl Program {
     pub fn typecheck(&mut self) -> Result<(), Error> {
         self.cache.parse(self.main_id)?;
         self.cache.load_stdlib()?;
-        let initial_env = self.cache.mk_type_env().expect("program::typecheck(): stdlib has been loaded but was not found in cache on mk_types_env()");
+        let initial_env = self.cache.mk_type_ctxt().expect("program::typecheck(): stdlib has been loaded but was not found in cache on mk_types_env()");
         self.cache
             .resolve_imports(self.main_id)
             .map_err(|cache_err| {
@@ -181,7 +184,7 @@ pub fn query(
     initial_env: &Envs,
     path: Option<String>,
 ) -> Result<Term, Error> {
-    cache.prepare(file_id, &initial_env.type_env)?;
+    cache.prepare(file_id, &initial_env.type_ctxt)?;
 
     let t = if let Some(p) = path {
         // Parsing `y.path`. We `seq` it to force the evaluation of the underlying value,
@@ -355,11 +358,23 @@ mod doc {
 mod tests {
     use super::*;
     use crate::error::EvalError;
+    use crate::parser::{grammar, lexer};
     use crate::position::TermPos;
-    use crate::term::ArrayAttrs;
+    use crate::term::SharedTerm;
     use assert_matches::assert_matches;
+    use codespan::Files;
     use std::io::Cursor;
 
+    fn parse(s: &str) -> Option<RichTerm> {
+        let id = Files::new().add("<test>", String::from(s));
+
+        grammar::TermParser::new()
+            .parse_term(id, lexer::Lexer::new(&s))
+            .map(RichTerm::without_pos)
+            .map_err(|err| println!("{:?}", err))
+            .ok()
+    }
+
     fn eval_full(s: &str) -> Result<RichTerm, Error> {
         let src = Cursor::new(s);
 
@@ -386,21 +401,30 @@ mod tests {
 
     #[test]
     fn evaluation_full() {
-        use crate::{mk_array, mk_record};
+        use crate::mk_record;
+        use crate::term::make as mk_term;
 
         let t = eval_full("[(1 + 1), (\"a\" ++ \"b\"), ([ 1, [1 + 2] ])]").unwrap();
-
-        // [2, "ab", [1, [3]]]
-        let expd = mk_array!(
-            Term::Num(2_f64),
-            Term::Str(String::from("ab")),
-            mk_array!(
-                Term::Num(1_f64),
-                mk_array!(Term::Num(3_f64); ArrayAttrs::new().closurized());
-                ArrayAttrs::new().closurized()
-            );
-            ArrayAttrs::new().closurized()
-        );
+        let mut expd = parse("[2, \"ab\", [1, [3]]]").unwrap();
+
+        // Strings are parsed as StrChunks, but evaluated to Str, so we need to hack the array a bit
+        // The evaluator will change the attributes so we neeed to anticipate that too.
+        if let Term::Array(ref mut data, ref mut attrs) = SharedTerm::make_mut(&mut expd.term) {
+            *data.get_mut(1).unwrap() = mk_term::string("ab");
+            attrs.closurized = true;
+            if let Term::Array(data, attrs) =
+                SharedTerm::make_mut(&mut data.get_mut(2).unwrap().term)
+            {
+                attrs.closurized = true;
+                if let Term::Array(_, attrs) =
+                    SharedTerm::make_mut(&mut data.get_mut(1).unwrap().term)
+                {
+                    attrs.closurized = true;
+                }
+            }
+        } else {
+            panic!();
+        }
 
         assert_eq!(t.without_pos(), expd.without_pos());
 
diff --git a/src/repl/mod.rs b/src/repl/mod.rs
index e6c69ff1..63a13293 100644
--- a/src/repl/mod.rs
+++ b/src/repl/mod.rs
@@ -74,9 +74,9 @@ pub struct ReplImpl {
     /// The current environment (for evaluation and typing). Contain the initial environment with
     /// the stdlib, plus toplevel declarations and loadings made inside the REPL.
     env: Envs,
-    /// The initial type environment, without the toplevel declarations made inside the REPL. Used
-    /// to typecheck imports in a fresh environment.
-    initial_type_env: typecheck::Environment,
+    /// The initial typing context, without the toplevel declarations made inside the REPL. Used to
+    /// typecheck imports in a fresh environment.
+    initial_type_ctxt: typecheck::Context,
 }
 
 impl ReplImpl {
@@ -86,7 +86,7 @@ impl ReplImpl {
             cache: Cache::new(ErrorTolerance::Strict),
             parser: grammar::ExtendedTermParser::new(),
             env: Envs::new(),
-            initial_type_env: typecheck::Environment::new(),
+            initial_type_ctxt: typecheck::Context::new(),
         }
     }
 
@@ -94,7 +94,7 @@ impl ReplImpl {
     /// typing environment.
     pub fn load_stdlib(&mut self) -> Result<(), Error> {
         self.env = self.cache.prepare_stdlib()?;
-        self.initial_type_env = self.env.type_env.clone();
+        self.initial_type_ctxt = self.env.type_ctxt.clone();
         Ok(())
     }
 
@@ -135,16 +135,28 @@ impl ReplImpl {
             }
 
             let wildcards =
-                typecheck::type_check(&t, repl_impl.env.type_env.clone(), &repl_impl.cache)?;
+                typecheck::type_check(&t, repl_impl.env.type_ctxt.clone(), &repl_impl.cache)?;
 
             if let Some(id) = id {
-                typecheck::env_add(&mut repl_impl.env.type_env, id, &t, &repl_impl.cache);
+                typecheck::env_add(
+                    &mut repl_impl.env.type_ctxt.type_env,
+                    id.clone(),
+                    &t,
+                    &repl_impl.env.type_ctxt.term_env,
+                    &repl_impl.cache,
+                );
+                repl_impl
+                    .env
+                    .type_ctxt
+                    .term_env
+                    .0
+                    .insert(id, (t.clone(), repl_impl.env.type_ctxt.term_env.clone()));
             }
 
             for id in &pending {
                 repl_impl
                     .cache
-                    .typecheck(*id, &repl_impl.initial_type_env)
+                    .typecheck(*id, &repl_impl.initial_type_ctxt)
                     .map_err(|cache_err| {
                         cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
                     })?;
@@ -213,11 +225,10 @@ impl Repl for ReplImpl {
         for id in &pending {
             self.cache.resolve_imports(*id).unwrap();
         }
-        //FIXME: use a non-empty term environment
         typecheck::env_add_term(
-            &mut self.env.type_env,
+            &mut self.env.type_ctxt.type_env,
             &term,
-            &typecheck::eq::SimpleTermEnvironment::new(),
+            &self.env.type_ctxt.term_env,
             &self.cache,
         )
         .unwrap();
@@ -234,7 +245,7 @@ impl Repl for ReplImpl {
         for id in &pending {
             self.cache.resolve_imports(*id).unwrap();
         }
-        let wildcards = typecheck::type_check(&term, self.env.type_env.clone(), &self.cache)?;
+        let wildcards = typecheck::type_check(&term, self.env.type_ctxt.clone(), &self.cache)?;
         // Substitute the wildcard types for their inferred types
         // We need to `traverse` the term, in case the type depends on inner terms that also contain wildcards
         let term = term
@@ -249,10 +260,12 @@ impl Repl for ReplImpl {
             )
             .unwrap();
 
-        Ok(
-            typecheck::apparent_type(term.as_ref(), Some(&self.env.type_env), Some(&self.cache))
-                .into(),
+        Ok(typecheck::apparent_type(
+            term.as_ref(),
+            Some(&self.env.type_ctxt.type_env),
+            Some(&self.cache),
         )
+        .into())
     }
 
     fn query(&mut self, exp: &str) -> Result<Term, Error> {
diff --git a/src/repl/query_print.rs b/src/repl/query_print.rs
index 990ad2b3..5fe43348 100644
--- a/src/repl/query_print.rs
+++ b/src/repl/query_print.rs
@@ -235,7 +235,7 @@ fn write_query_result_<R: QueryPrinter>(
 
             match &meta {
                 MetaValue {
-                    priority: MergePriority::Bottom,
+                    priority: MergePriority::Default,
                     value: Some(t),
                     ..
                 } if selected_attrs.default => {
@@ -243,11 +243,10 @@ fn write_query_result_<R: QueryPrinter>(
                     found = true;
                 }
                 MetaValue {
-                    priority: MergePriority::Numeral(n),
+                    priority: MergePriority::Normal,
                     value: Some(t),
                     ..
                 } if selected_attrs.value => {
-                    renderer.write_metadata(out, "priority", &format!("{}", n))?;
                     renderer.write_metadata(out, "value", &t.as_ref().shallow_repr())?;
                     found = true;
                 }
diff --git a/src/serialize.rs b/src/serialize.rs
index c601dedd..cc1e48e2 100644
--- a/src/serialize.rs
+++ b/src/serialize.rs
@@ -3,7 +3,7 @@ use crate::{
     error::SerializationError,
     eval::{self, is_empty_optional},
     identifier::Ident,
-    term::{array::Array, ArrayAttrs, MetaValue, RecordAttrs, RichTerm, Term},
+    term::{ArrayAttrs, MetaValue, RecordAttrs, RichTerm, Term},
 };
 
 use serde::{
@@ -11,7 +11,7 @@ use serde::{
     ser::{Error, Serialize, SerializeMap, SerializeSeq, Serializer},
 };
 
-use std::{collections::HashMap, fmt, io, rc::Rc, str::FromStr};
+use std::{collections::HashMap, fmt, io, str::FromStr};
 
 /// Available export formats.
 // If you add or remove variants, remember to update the CLI docs in `src/bin/nickel.rs'
@@ -134,7 +134,7 @@ where
 
 /// Serialize for an Array. Required to hide the internal attributes.
 pub fn serialize_array<S>(
-    terms: &Array,
+    terms: &Vec<RichTerm>,
     _attrs: &ArrayAttrs,
     serializer: S,
 ) -> Result<S::Ok, S::Error>
@@ -150,11 +150,11 @@ where
 }
 
 /// Deserialize for an Array. Required to set the default attributes.
-pub fn deserialize_array<'de, D>(deserializer: D) -> Result<(Array, ArrayAttrs), D::Error>
+pub fn deserialize_array<'de, D>(deserializer: D) -> Result<(Vec<RichTerm>, ArrayAttrs), D::Error>
 where
     D: Deserializer<'de>,
 {
-    let terms = Array::new(Rc::from(Vec::deserialize(deserializer)?));
+    let terms: Vec<RichTerm> = Vec::deserialize(deserializer)?;
     Ok((terms, Default::default()))
 }
 
@@ -200,8 +200,8 @@ pub fn validate(format: ExportFormat, t: &RichTerm) -> Result<(), SerializationE
                 map.iter().try_for_each(|(_, t)| validate(format, t))?;
                 Ok(())
             }
-            Array(array, _) => {
-                array.iter().try_for_each(|t| validate(format, t))?;
+            Array(vec, _) => {
+                vec.iter().try_for_each(|t| validate(format, t))?;
                 Ok(())
             }
             //TODO: have a specific error for such missing value.
diff --git a/src/term.rs b/src/term.rs
index 880434ff..5f98a5bc 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -16,30 +16,20 @@
 //! contracts, default values, documentation, etc. They bring such usually external object down to
 //! the term level, and together with [crate::eval::merge], they allow for flexible and modular
 //! definitions of contracts, record and metadata all together.
-use array::Array;
-
-use crate::{
-    destruct::Destruct,
-    error::ParseError,
-    identifier::Ident,
-    label::Label,
-    match_sharedterm,
-    position::TermPos,
-    types::{AbsType, Types, UnboundTypeVariableError},
-};
-
+use crate::destruct::Destruct;
+use crate::error::ParseError;
+use crate::identifier::Ident;
+use crate::label::Label;
+use crate::match_sharedterm;
+use crate::position::TermPos;
+use crate::types::{AbsType, Types, UnboundTypeVariableError};
 use codespan::FileId;
-
 use serde::{Deserialize, Serialize};
-
-use std::{
-    cmp::{Ordering, PartialOrd},
-    collections::{HashMap, HashSet},
-    ffi::OsString,
-    fmt,
-    ops::Deref,
-    rc::Rc,
-};
+use std::collections::{HashMap, HashSet};
+use std::ffi::OsString;
+use std::fmt;
+use std::ops::Deref;
+use std::rc::Rc;
 
 /// The AST of a Nickel expression.
 ///
@@ -118,7 +108,7 @@ pub enum Term {
     /// An array.
     #[serde(serialize_with = "crate::serialize::serialize_array")]
     #[serde(deserialize_with = "crate::serialize::deserialize_array")]
-    Array(Array, ArrayAttrs),
+    Array(Vec<RichTerm>, ArrayAttrs),
 
     /// A primitive unary operator.
     #[serde(skip)]
@@ -211,161 +201,7 @@ impl PendingContract {
     }
 }
 
-pub mod array {
-    use std::mem::transmute;
-    use std::mem::ManuallyDrop;
-
-    use super::*;
-
-    #[derive(Debug, Clone, PartialEq)]
-    pub struct Array {
-        inner: Rc<[RichTerm]>,
-        start: usize,
-        end: usize,
-    }
-
-    impl Array {
-        /// Creates a Nickel array from reference-counted slice.
-        pub fn new(inner: Rc<[RichTerm]>) -> Self {
-            let start = 0;
-            let end = inner.len();
-
-            Self { inner, start, end }
-        }
-
-        /// Returns the effective length of the array.
-        pub fn len(&self) -> usize {
-            self.end - self.start
-        }
-
-        /// Returns `true` if the array is empty.
-        pub fn is_empty(&self) -> bool {
-            self.end == self.start
-        }
-
-        /// Returns a reference to the term at the given index.
-        pub fn get(&self, idx: usize) -> Option<&RichTerm> {
-            self.inner.get(self.start + idx)
-        }
-
-        /// Discards the first `diff` terms of the array.
-        pub fn advance_by(mut self, diff: usize) -> Self {
-            self.start += usize::min(diff, self.len());
-            self
-        }
-
-        /// Makes a mutable slice into the given `Array`.
-        pub fn make_mut(&mut self) -> &mut [RichTerm] {
-            // NOTE: trying to use `Rc::make_mut` will result in the following compiler error:
-            // > the trait `Clone` is not implemented for `[term::RichTerm]`
-            // This seems to be an edge-case in the standard library.
-            // As a workaround, if `get_mut` fails we recollect the array into a new `Rc` by cloning all terms.
-            // Thus we make sure that the second call to `get_mut` won't fail.
-
-            // This condition is the same as `!Rc::is_unique(&mut self.inner)`, but that function
-            // is not public.
-            if Rc::strong_count(&mut self.inner) != 1 || Rc::weak_count(&mut self.inner) != 0 {
-                self.inner = self.iter().cloned().collect::<Rc<[_]>>();
-            }
-
-            Rc::get_mut(&mut self.inner).expect("non-unique Rc after deep-cloning Array")
-        }
-
-        /// Returns an iterator of references over the array.
-        pub fn iter(&self) -> std::slice::Iter<'_, RichTerm> {
-            self.as_ref().iter()
-        }
-    }
-
-    impl Default for Array {
-        fn default() -> Self {
-            Self::new(Rc::new([]))
-        }
-    }
-
-    impl FromIterator<RichTerm> for Array {
-        fn from_iter<T: IntoIterator<Item = RichTerm>>(iter: T) -> Self {
-            let inner = iter.into_iter().collect::<Rc<[_]>>();
-            let start = 0;
-            let end = inner.len();
-
-            Self { inner, start, end }
-        }
-    }
-
-    impl AsRef<[RichTerm]> for Array {
-        fn as_ref(&self) -> &[RichTerm] {
-            &self.inner[self.start..self.end]
-        }
-    }
-
-    impl IntoIterator for Array {
-        type Item = RichTerm;
-
-        type IntoIter = IntoIter;
-
-        fn into_iter(self) -> Self::IntoIter {
-            // SAFETY: If there are no other strong or weak references
-            // to the inner slice, then we can:
-            // - Drop the elements outside our inner view,
-            // - Move out the elements inside out inner view.
-            // Otherwise, we clone everything.
-
-            unsafe {
-                let mut inner: Rc<[ManuallyDrop<RichTerm>]> = transmute(self.inner);
-                let idx = self.start;
-                let end = self.end;
-
-                if let Some(slice) = Rc::get_mut(&mut inner) {
-                    for term in &mut slice[..idx] {
-                        ManuallyDrop::drop(term)
-                    }
-                    for term in &mut slice[end..] {
-                        ManuallyDrop::drop(term)
-                    }
-                }
-
-                IntoIter { inner, idx, end }
-            }
-        }
-    }
-
-    pub struct IntoIter {
-        inner: Rc<[ManuallyDrop<RichTerm>]>,
-        idx: usize,
-        end: usize,
-    }
-
-    impl Iterator for IntoIter {
-        type Item = RichTerm;
-
-        fn next(&mut self) -> Option<Self::Item> {
-            if self.idx == self.end {
-                None
-            } else {
-                let term = match Rc::get_mut(&mut self.inner) {
-                    None => self.inner[..self.end]
-                        .get(self.idx)
-                        .cloned()
-                        .map(ManuallyDrop::into_inner),
-                    Some(slice) => slice[..self.end]
-                        .get_mut(self.idx)
-                        .map(|t| unsafe { ManuallyDrop::take(t) }),
-                };
-
-                self.idx += 1;
-                term
-            }
-        }
-    }
-
-    impl ExactSizeIterator for IntoIter {
-        fn len(&self) -> usize {
-            self.end - self.idx
-        }
-    }
-}
-
+/// The attributes of an Array.
 #[derive(Debug, Default, PartialEq, Clone)]
 pub struct ArrayAttrs {
     /// A `closurized` array verifies the following conditions:
@@ -451,130 +287,15 @@ pub struct RecordDeps {
 /// Potential dependencies of a single field over the sibling fields in a recursive record.
 pub type FieldDeps = Option<Rc<HashSet<Ident>>>;
 
-/// A wrapper around f64 which makes `NaN` not representable. As opposed to floats, it is `Eq` and
-/// `Ord`.
-#[derive(Debug, Copy, Clone, PartialEq, PartialOrd)]
-pub struct NumeralPriority(f64);
-
-/// Error raised when trying to convert a float with `NaN` value to a `NumeralPriority`.
-#[derive(Debug, Copy, Clone)]
-pub struct PriorityIsNaN;
-
-// The following impl are ok because `NumeralPriority(NaN)` can't be constructed.
-impl Eq for NumeralPriority {}
-impl Ord for NumeralPriority {
-    fn cmp(&self, other: &Self) -> Ordering {
-        // Ok: NaN is forbidden
-        self.partial_cmp(other).unwrap()
-    }
-}
-
-impl NumeralPriority {
-    pub fn zero() -> Self {
-        NumeralPriority(0.0)
-    }
-}
-
-impl TryFrom<f64> for NumeralPriority {
-    type Error = PriorityIsNaN;
-
-    fn try_from(f: f64) -> Result<Self, Self::Error> {
-        if f.is_nan() {
-            Err(PriorityIsNaN)
-        } else {
-            Ok(NumeralPriority(f))
-        }
-    }
-}
-
-impl From<NumeralPriority> for f64 {
-    fn from(n: NumeralPriority) -> Self {
-        n.0
-    }
-}
-
-impl fmt::Display for NumeralPriority {
-    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        self.0.fmt(f)
-    }
-}
-
-#[derive(Debug, Copy, Clone)]
+#[derive(Debug, Eq, PartialEq, Ord, PartialOrd, Copy, Clone)]
 pub enum MergePriority {
-    /// The priority of default values that are overridden by everything else.
-    Bottom,
-    /// The priority by default, when no priority annotation (`default`, `force`, `priority`) is
-    /// provided.
-    ///
-    /// Act as the value `MergePriority::Numeral(0.0)` with respect to ordering and equality
-    /// testing. The only way to discriminate this variant is to pattern match on it.
-    Neutral,
-    /// A numeral priority.
-    Numeral(NumeralPriority),
-    /// The priority of values that override everything else and can't be overridden.
-    Top,
-}
-
-impl PartialOrd for MergePriority {
-    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
-        Some(self.cmp(other))
-    }
-}
-
-impl PartialEq for MergePriority {
-    fn eq(&self, other: &Self) -> bool {
-        match (self, other) {
-            (MergePriority::Bottom, MergePriority::Bottom)
-            | (MergePriority::Neutral, MergePriority::Neutral)
-            | (MergePriority::Top, MergePriority::Top) => true,
-            (MergePriority::Numeral(p1), MergePriority::Numeral(p2)) => p1 == p2,
-            (MergePriority::Neutral, MergePriority::Numeral(p))
-            | (MergePriority::Numeral(p), MergePriority::Neutral)
-                if p == &NumeralPriority::zero() =>
-            {
-                true
-            }
-            _ => false,
-        }
-    }
-}
-
-impl Eq for MergePriority {}
-
-impl Ord for MergePriority {
-    fn cmp(&self, other: &Self) -> Ordering {
-        match (self, other) {
-            // Equalities
-            (MergePriority::Bottom, MergePriority::Bottom)
-            | (MergePriority::Top, MergePriority::Top)
-            | (MergePriority::Neutral, MergePriority::Neutral) => Ordering::Equal,
-            (MergePriority::Numeral(p1), MergePriority::Numeral(p2)) => p1.cmp(p2),
-
-            // Top and bottom.
-            (MergePriority::Bottom, _) | (_, MergePriority::Top) => Ordering::Less,
-            (MergePriority::Top, _) | (_, MergePriority::Bottom) => Ordering::Greater,
-
-            // Neutral and numeral.
-            (MergePriority::Neutral, MergePriority::Numeral(n)) => NumeralPriority::zero().cmp(n),
-            (MergePriority::Numeral(n), MergePriority::Neutral) => n.cmp(&NumeralPriority::zero()),
-        }
-    }
+    Default,
+    Normal,
 }
 
 impl Default for MergePriority {
     fn default() -> Self {
-        Self::Neutral
-    }
-}
-
-impl fmt::Display for MergePriority {
-    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        match self {
-            MergePriority::Bottom => write!(f, "default"),
-            MergePriority::Neutral => write!(f, "{}", NumeralPriority::zero()),
-            MergePriority::Numeral(p) => write!(f, "{}", p),
-            MergePriority::Top => write!(f, "force"),
-        }
+        Self::Normal
     }
 }
 
@@ -614,7 +335,7 @@ impl MetaValue {
     }
 
     /// Flatten two nested metavalues into one, combining their metadata. If data that can't be
-    /// combined (typically, the documentation, the type annotation or the priority) are set by both metavalues,
+    /// combined (typically, the documentation or the type annotation) are set by both metavalues,
     /// outer's one are kept.
     ///
     /// Note that no environment management such as closurization takes place, because this
@@ -624,7 +345,7 @@ impl MetaValue {
     /// #Preconditions
     ///
     /// - `outer.value` is assumed to be `inner`. While `flatten` may still work fine if this
-    ///   condition is not fulfilled, the value of the final metavalue is set to be `inner`'s one,
+    ///   condition is not fullfilled, the value of the final metavalue is set to be `inner`'s one,
     ///   and `outer`'s one is dropped.
     pub fn flatten(mut outer: MetaValue, mut inner: MetaValue) -> MetaValue {
         // Keep the outermost value for non-mergeable information, such as documentation, type annotation,
@@ -643,21 +364,12 @@ impl MetaValue {
 
         outer.contracts.extend(inner.contracts.into_iter());
 
-        let priority = match (outer.priority, inner.priority) {
-            // Neutral corresponds to the case where no priority was specified. In that case, the
-            // other priority takes precedence.
-            (MergePriority::Neutral, p) | (p, MergePriority::Neutral) => p,
-            // Otherwise, we keep the maximum of both priorities, as we would do when merging
-            // values.
-            (p1, p2) => std::cmp::max(p1, p2),
-        };
-
         MetaValue {
             doc: outer.doc.or(inner.doc),
             types: outer.types.or(inner.types),
             contracts: outer.contracts,
             opt: outer.opt || inner.opt,
-            priority,
+            priority: std::cmp::min(outer.priority, inner.priority),
             value: inner.value,
         }
     }
@@ -738,10 +450,9 @@ impl Term {
                 func(t1);
                 func(t2);
             }
-            OpN(_, ref mut terms) => terms.iter_mut().for_each(|t| {
+            OpN(_, ref mut terms) | Array(ref mut terms, _) => terms.iter_mut().for_each(|t| {
                 func(t);
             }),
-            Array(ref mut terms, _) => terms.make_mut().iter_mut().for_each(|t| func(t)),
             StrChunks(chunks) => chunks.iter_mut().for_each(|chunk| match chunk {
                 StrChunk::Literal(_) => (),
                 StrChunk::Expr(e, _) => func(e),
@@ -830,7 +541,7 @@ impl Term {
                     content.push_str("contract,");
                 }
 
-                let value_label = if meta.priority == MergePriority::Bottom {
+                let value_label = if meta.priority == MergePriority::Default {
                     "default"
                 } else {
                     "value"
@@ -1574,13 +1285,13 @@ impl RichTerm {
                 )
             },
             Term::Array(ts, attrs) => {
-                let ts_res = Array::new(ts
+                let ts_res: Result<Vec<RichTerm>, E> = ts
                     .into_iter()
                     .map(|t| t.traverse(f, state, order))
-                    .collect::<Result<Rc<[_]>, _>>()?);
+                    .collect();
 
                 RichTerm::new(
-                    Term::Array(ts_res, attrs),
+                    Term::Array(ts_res?, attrs),
                     pos,
                 )
             },
@@ -1789,7 +1500,7 @@ pub mod make {
     #[macro_export]
     macro_rules! mk_fun {
         ( $id:expr, $body:expr ) => {
-            $crate::term::RichTerm::from($crate::term::Term::Fun($crate::identifier::Ident::from($id), $crate::term::RichTerm::from($body)))
+            $crate::term::RichTerm::from($crate::term::Term::Fun($crate::identifier::Ident::from($id), $crate::term::RichTerm::from($body).into()))
         };
         ( $id1:expr, $id2:expr , $( $rest:expr ),+ ) => {
             mk_fun!($crate::identifier::Ident::from($id1), mk_fun!($id2, $( $rest ),+))
@@ -1837,25 +1548,6 @@ pub mod make {
         };
     }
 
-    /// Array for types implementing `Into<RichTerm>` (for elements).
-    /// The array's attributes are a trailing (optional) `ArrayAttrs`, separated by a `;`.
-    /// `mk_array!(Term::Num(42)) corresponds to `[42]`. Here the attributes are `ArrayAttrs::default()`, though the evaluated array may have different attributes.
-    #[macro_export]
-    macro_rules! mk_array {
-        ( $( $terms:expr ),* ; $attrs:expr ) => {
-            {
-                let ts = $crate::term::array::Array::new(std::rc::Rc::new([$( crate::term::RichTerm::from($terms) ),*]));
-                $crate::term::RichTerm::from(Term::Array(ts, $attrs))
-            }
-        };
-        ( $( $terms:expr ),* ) => {
-            {
-                let ts = $crate::term::array::Array::new(std::rc::Rc::new([$( crate::term::RichTerm::from($terms) ),*]));
-                $crate::term::RichTerm::from(Term::Array(ts, ArrayAttrs::default()))
-            }
-        };
-    }
-
     pub fn var<I>(v: I) -> RichTerm
     where
         I: Into<Ident>,
diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs
index fd100cd9..2867c21c 100644
--- a/src/transform/free_vars.rs
+++ b/src/transform/free_vars.rs
@@ -144,7 +144,7 @@ fn collect_free_vars(rt: &mut RichTerm, free_vars: &mut HashSet<Ident>) {
             *deps = Some(new_deps);
         }
         Term::Array(ts, _) => {
-            for t in ts.make_mut().iter_mut() {
+            for t in ts {
                 collect_free_vars(t, free_vars);
             }
         }
diff --git a/src/typecheck/eq.rs b/src/typecheck/eq.rs
index b0cbfcc1..5c40e10d 100644
--- a/src/typecheck/eq.rs
+++ b/src/typecheck/eq.rs
@@ -84,6 +84,17 @@ impl TermEnvironment for SimpleTermEnvironment {
     }
 }
 
+impl std::iter::FromIterator<(Ident, (RichTerm, SimpleTermEnvironment))> for SimpleTermEnvironment {
+    fn from_iter<T>(iter: T) -> Self
+    where
+        T: IntoIterator<Item = (Ident, (RichTerm, SimpleTermEnvironment))>,
+    {
+        SimpleTermEnvironment(
+            GenericEnvironment::<Ident, (RichTerm, SimpleTermEnvironment)>::from_iter(iter),
+        )
+    }
+}
+
 impl TermEnvironment for eval::Environment {
     fn get_then<F, T>(&self, id: &Ident, f: F) -> T
     where
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index 45d74bf7..e7fefaa8 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -81,38 +81,57 @@ pub type Environment = GenericEnvironment<Ident, TypeWrapper>;
 /// Mapping from wildcard ID to inferred type
 pub type Wildcards = Vec<Types>;
 
-/// A structure holding the typing context, that is, scoped, environment-like data.
+/// The typing context is a structure holding the scoped, environment-like data structures required
+/// to perform typechecking.
+///
+/// The typing context currently includes the typing environment, counterpart of the eval
+/// environment for typechecking, and the term environment.
 #[derive(Debug, PartialEq, Clone)]
 pub struct Context {
     pub type_env: Environment,
     pub term_env: SimpleTermEnvironment,
 }
 
+impl Context {
+    pub fn new() -> Self {
+        Context {
+            type_env: Environment::new(),
+            term_env: SimpleTermEnvironment::new(),
+        }
+    }
+}
+
 #[derive(Clone, Debug)]
 pub enum EnvBuildError {
     NotARecord(RichTerm),
 }
 
 /// Populate the initial typing environment from a `Vec` of parsed files.
-pub fn mk_initial_env(initial_env: Vec<RichTerm>) -> Result<Environment, EnvBuildError> {
-    Ok(initial_env
+pub fn mk_initial_ctxt(initial_env: &Vec<RichTerm>) -> Result<Context, EnvBuildError> {
+    // Collect the bindings for each module, clone them and flatten the result to a single list.
+    let bindings = initial_env
         .iter()
         .map(|rt| {
             if let Term::RecRecord(rec, ..) = rt.as_ref() {
-                Ok(rec.iter().map(|(id, rt)| {
-                    (
-                        id.clone(),
-                        infer_record_type(rt.as_ref(), &SimpleTermEnvironment::new()),
-                    )
-                }))
+                Ok(rec.iter().map(|(id, rt)| (id.clone(), rt.clone())))
             } else {
                 Err(EnvBuildError::NotARecord(rt.clone()))
             }
         })
         .collect::<Result<Vec<_>, EnvBuildError>>()?
         .into_iter()
-        .flatten()
-        .collect())
+        .flatten();
+
+    let term_env = bindings
+        .clone()
+        .map(|(id, rt)| (id, (rt, SimpleTermEnvironment::new())))
+        .collect();
+
+    let type_env = bindings
+        .map(|(id, rt)| (id.clone(), infer_record_type(rt.as_ref(), &term_env)))
+        .collect();
+
+    Ok(Context { type_env, term_env })
 }
 
 /// Add the bindings of a record to a typing environment. Ignore fields whose name are defined
@@ -143,14 +162,18 @@ pub fn env_add_term(
 }
 
 /// Bind one term in a typing environment.
-pub fn env_add(env: &mut Environment, id: Ident, rt: &RichTerm, resolver: &dyn ImportResolver) {
-    // FIXME: we probably need to build an initial term environment first, instead of
-    // using an empty one.
+pub fn env_add(
+    env: &mut Environment,
+    id: Ident,
+    rt: &RichTerm,
+    term_env: &SimpleTermEnvironment,
+    resolver: &dyn ImportResolver,
+) {
     env.insert(
         id,
         TypeWrapper::from_apparent_type(
             apparent_type(rt.as_ref(), Some(env), Some(resolver)),
-            &SimpleTermEnvironment::new(),
+            term_env,
         ),
     );
 }
@@ -183,10 +206,10 @@ pub struct State<'a> {
 /// Return the type inferred for type wildcards.
 pub fn type_check(
     t: &RichTerm,
-    initial_env: Environment,
+    initial_ctxt: Context,
     resolver: &impl ImportResolver,
 ) -> Result<Wildcards, TypecheckError> {
-    type_check_linearize(t, initial_env, resolver, StubHost::<(), (), _>::new())
+    type_check_linearize(t, initial_ctxt, resolver, StubHost::<(), (), _>::new())
         .map(|(wildcards, _)| wildcards)
 }
 
@@ -197,7 +220,7 @@ pub fn type_check(
 /// Linearization is solely used by the LSP server.
 pub fn type_check_linearize<LL>(
     t: &RichTerm,
-    initial_env: Environment,
+    initial_ctxt: Context,
     resolver: &impl ImportResolver,
     mut linearizer: LL,
 ) -> Result<(Wildcards, LL::Completed), TypecheckError>
@@ -219,10 +242,7 @@ where
 
         walk(
             &mut state,
-            Context {
-                type_env: initial_env,
-                term_env: SimpleTermEnvironment::new(),
-            },
+            initial_ctxt,
             &mut building,
             linearizer.scope(),
             t,
diff --git a/stdlib/contract.ncl b/stdlib/contract.ncl
index 713274d9..dc31920c 100644
--- a/stdlib/contract.ncl
+++ b/stdlib/contract.ncl
@@ -26,11 +26,7 @@
       if pol == lPol then
           %unseal% sy t (%blame% l)
       else
-          # Here, we know that this term should be sealed, but to give the right 
-          # blame for the contract, we have to change the polarity to match the 
-          # polarity of the `Forall`, because this is what's important for 
-          # blaming polymorphic contracts.
-          %seal% sy (%chng_pol% l) t,
+          %seal% sy l t,
 
   "$enums" = fun case l t =>
       if %typeof% t == `Enum then
diff --git a/utilities/src/lib.rs b/utilities/src/lib.rs
index 0ba539a0..e92d0f3d 100644
--- a/utilities/src/lib.rs
+++ b/utilities/src/lib.rs
@@ -118,7 +118,10 @@ impl<'b> Bench<'b> {
 
 pub fn bench_terms<'r>(rts: Vec<Bench<'r>>) -> Box<dyn Fn(&mut Criterion) + 'r> {
     let mut cache = Cache::new(ErrorTolerance::Strict);
-    let Envs { eval_env, type_env } = cache.prepare_stdlib().unwrap();
+    let Envs {
+        eval_env,
+        type_ctxt,
+    } = cache.prepare_stdlib().unwrap();
     Box::new(move |c: &mut Criterion| {
         rts.iter().for_each(|bench| {
             let t = bench.term();
@@ -133,9 +136,9 @@ pub fn bench_terms<'r>(rts: Vec<Bench<'r>>) -> Box<dyn Fn(&mut Criterion) + 'r>
                     },
                     |(mut c_local, id, t)| {
                         if bench.eval_mode == EvalMode::TypeCheck {
-                            c_local.typecheck(id, &type_env).unwrap();
+                            c_local.typecheck(id, &type_ctxt).unwrap();
                         } else {
-                            c_local.prepare(id, &type_env).unwrap();
+                            c_local.prepare(id, &type_ctxt).unwrap();
                             eval::eval(t, &eval_env, &mut c_local).unwrap();
                         }
                     },
@@ -186,7 +189,7 @@ macro_rules! ncl_bench_group {
             let mut c: criterion::Criterion<_> = $config
                 .configure_from_args();
             let mut cache = Cache::new(ErrorTolerance::Strict);
-            let Envs {eval_env, type_env} = cache.prepare_stdlib().unwrap();
+            let Envs {eval_env, type_ctxt} = cache.prepare_stdlib().unwrap();
             $(
                 let bench = $crate::ncl_bench!$b;
                 let t = bench.term();
@@ -205,9 +208,9 @@ macro_rules! ncl_bench_group {
                         },
                         |(mut c_local, id, t)| {
                             if bench.eval_mode == $crate::EvalMode::TypeCheck {
-                                c_local.typecheck(id, &type_env).unwrap();
+                                c_local.typecheck(id, &type_ctxt).unwrap();
                             } else {
-                                c_local.prepare(id, &type_env).unwrap();
+                                c_local.prepare(id, &type_ctxt).unwrap();
                                 eval(t, &eval_env, &mut c_local).unwrap();
                             }
                         },


Test patch:
diff --git a/src/eval/tests.rs b/src/eval/tests.rs
index 7c725e85..b6554864 100644
--- a/src/eval/tests.rs
+++ b/src/eval/tests.rs
@@ -102,7 +102,7 @@ fn mk_default(t: RichTerm) -> Term {
     use crate::term::MergePriority;
 
     let mut meta = MetaValue::from(t);
-    meta.priority = MergePriority::Bottom;
+    meta.priority = MergePriority::Default;
     Term::MetaValue(meta)
 }
 
diff --git a/tests/pass.rs b/tests/pass.rs
index 498db4c1..4d0cfb66 100644
--- a/tests/pass.rs
+++ b/tests/pass.rs
@@ -127,8 +127,3 @@ fn recursive_let() {
 fn quote_in_indentifier() {
     check_file("quote_in_identifier.ncl")
 }
-
-#[test]
-fn priorities() {
-    check_file("priorities.ncl")
-}
diff --git a/tests/pass/priorities.ncl b/tests/pass/priorities.ncl
deleted file mode 100644
index 81c70849..00000000
--- a/tests/pass/priorities.ncl
+++ /dev/null
@@ -1,41 +0,0 @@
-let {Assert, ..} =  import "testlib.ncl" in
-
-let block1 = {
-  foo | default = 1,
-  bar = 1,
-  baz | force = 1,
-  x | priority 10 = 1,
-  y | priority -5 = 1,
-  z | priority 0 = 1,
-  d | default = 1,
-} in
-
-let block2 = {
-  foo | priority -10 = 2,
-  bar | priority 10 = 2,
-  baz = 2,
-  x | priority 11 = 2,
-  y  = 2,
-  z | priority 10 = 2,
-
-} in 
-
-let block3 = {
-  foo | priority -10.1 = 3,
-  bar | default = 3,
-  baz | priority 1000 = 3,
-  x | priority 12 = 3,
-  y | priority -1 = 3,
-  z | priority 50 = 3,
-} in
-
-block1 & block2 & block3
-== {
-  foo = 2,
-  bar = 2,
-  baz = 1,
-  x = 3,
-  y = 2,
-  z = 3,
-  d = 1,
-} | Assert
diff --git a/tests/records_fail.rs b/tests/records_fail.rs
index 147da5cd..81b17cbb 100644
--- a/tests/records_fail.rs
+++ b/tests/records_fail.rs
@@ -42,22 +42,6 @@ fn non_mergeable_piecewise() {
     );
 }
 
-#[test]
-fn non_mergeable_prio() {
-    assert_matches!(
-        eval("({a.b | priority 0 = 1, a = {b = 2}}).a.b"),
-        Err(Error::EvalError(EvalError::MergeIncompatibleArgs(..)))
-    );
-    assert_matches!(
-        eval("({a | force = false} & {a | force = true}).a"),
-        Err(Error::EvalError(EvalError::MergeIncompatibleArgs(..)))
-    );
-    assert_matches!(
-        eval("({foo.bar | priority -10 = false, foo.bar | priority -10 = true}).foo.bar"),
-        Err(Error::EvalError(EvalError::MergeIncompatibleArgs(..)))
-    );
-}
-
 #[test]
 fn dynamic_not_recursive() {
     assert_matches!(
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index 671aa01c..bfc5d6f0 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -5,10 +5,10 @@ use nickel_lang::error::TypecheckError;
 use nickel_lang::parser::{grammar, lexer};
 use nickel_lang::term::RichTerm;
 use nickel_lang::types::{AbsType, Types};
-use nickel_lang::{typecheck, typecheck::Environment};
+use nickel_lang::{typecheck, typecheck::Context};
 
 fn type_check(rt: &RichTerm) -> Result<(), TypecheckError> {
-    typecheck::type_check(rt, Environment::new(), &mut DummyResolver {}).map(|_| ())
+    typecheck::type_check(rt, Context::new(), &mut DummyResolver {}).map(|_| ())
 }
 
 fn type_check_expr(s: impl std::string::ToString) -> Result<(), TypecheckError> {