Repository: tweag/nickel
Pull request #834 (2022-09-16 10:11:15)

Unified environment interface for contract equality checking
Preliminary work for the follow-up of #766, which is to fix the contract equality checking during an REPL session. This PR is also required more generally in order to use contract equality checking during evaluation, for example to eliminate redundant contract applications at runtime when merging lazy array contracts.

This PR abstracts over the `TermEnvironment`, that is currently a concrete data structure used by the typechecker, by turning it into a trait. The trait is then implemented by `SimpleTermEnvironment` (formerly `TermEnvironment`) and the eval environment (`eval::Environment`). This change requires to add a bunch of generic parameters, in particular on the contract equality checking functions and for the formerly `TypeWrapper`, but the change are hopefully reasonably localized.

Because the eval environment returns thunks, and not direct references to terms and environments, the interface of `TermEnvironment` has to reverse the control flow and take a continuation instead of returning references, as opposed to e.g. `SimpleTermEnvironment::get`.

yannham: After a remark of @Acaccia, I'll try to simplify this using `impl Deref<_>` as a return type in `TermEnvironment` instead of taking a closure first.
yannham: This would actually require GATs, I think. So keeping things like they are for now :slightly_smiling_face: 

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/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/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..30a369ec 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -355,11 +355,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 +398,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 f1a7a2d3..e6c69ff1 100644
--- a/src/repl/mod.rs
+++ b/src/repl/mod.rs
@@ -217,7 +217,7 @@ impl Repl for ReplImpl {
         typecheck::env_add_term(
             &mut self.env.type_env,
             &term,
-            &typecheck::eq::TermEnvironment::new(),
+            &typecheck::eq::SimpleTermEnvironment::new(),
             &self.cache,
         )
         .unwrap();
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 515e031e..b0cbfcc1 100644
--- a/src/typecheck/eq.rs
+++ b/src/typecheck/eq.rs
@@ -43,24 +43,60 @@
 //! times. For anything more complex, we return false.
 
 use super::*;
-use crate::eval;
-use crate::term::UnaryOp;
+use crate::{eval, term::UnaryOp};
 
 /// The maximal number of variable links we want to unfold before abandoning the check. It should
 /// stay low, but has been fixed arbitrarily: feel fee to increase reasonably if it turns out
 /// legitimate type equalities between simple contracts are unduly rejected in practice.
 pub const MAX_GAS: u8 = 8;
 
+/// Abstract over the term environment, which is represented differently in the typechecker and
+/// during evaluation.
+///
+/// The evaluation environment holds [`crate::eval::lazy::Thunks`], which are `Rc<RefCell<_>>`
+/// under the hood, while the term environment used during typechecking is just maps identifiers to
+/// a pair `(RichTerm, Environment)`. To have an interface that works with both,
+/// `TermEnvironment::get_then` has to take a closure representing the continuation of the task to
+/// do with the result instead of merely returning it.
+pub trait TermEnvironment: Clone {
+    fn get_then<F, T>(&self, id: &Ident, f: F) -> T
+    where
+        F: FnOnce(Option<(&RichTerm, &Self)>) -> T;
+}
+
+/// A simple term environment, as a mapping from identifiers to a tuple of a term and an
+/// environment (i.e. a closure), sufficient for the needs of typechecking.
 #[derive(PartialEq, Clone, Debug)]
-pub struct TermEnvironment(pub GenericEnvironment<Ident, (RichTerm, TermEnvironment)>);
+pub struct SimpleTermEnvironment(pub GenericEnvironment<Ident, (RichTerm, SimpleTermEnvironment)>);
 
-impl TermEnvironment {
+impl SimpleTermEnvironment {
     pub fn new() -> Self {
-        TermEnvironment(GenericEnvironment::new())
+        SimpleTermEnvironment(GenericEnvironment::new())
     }
 }
 
-impl From<eval::Environment> for TermEnvironment {
+impl TermEnvironment for SimpleTermEnvironment {
+    fn get_then<F, T>(&self, id: &Ident, f: F) -> T
+    where
+        F: FnOnce(Option<(&RichTerm, &SimpleTermEnvironment)>) -> T,
+    {
+        f(self.0.get(id).map(|(rt, env)| (rt, env)))
+    }
+}
+
+impl TermEnvironment for eval::Environment {
+    fn get_then<F, T>(&self, id: &Ident, f: F) -> T
+    where
+        F: FnOnce(Option<(&RichTerm, &eval::Environment)>) -> T,
+    {
+        match self.get(id).map(eval::lazy::Thunk::borrow) {
+            Some(closure_ref) => f(Some((&closure_ref.body, &closure_ref.env))),
+            None => f(None),
+        }
+    }
+}
+
+impl From<eval::Environment> for SimpleTermEnvironment {
     fn from(eval_env: eval::Environment) -> Self {
         let generic_env: GenericEnvironment<_, _> = eval_env
             .iter_elems()
@@ -70,12 +106,12 @@ impl From<eval::Environment> for TermEnvironment {
                     id.clone(),
                     (
                         borrowed.body.clone(),
-                        TermEnvironment::from(borrowed.env.clone()),
+                        SimpleTermEnvironment::from(borrowed.env.clone()),
                     ),
                 )
             })
             .collect();
-        TermEnvironment(generic_env)
+        SimpleTermEnvironment(generic_env)
     }
 }
 
@@ -103,10 +139,10 @@ impl State {
     }
 
     /// Create a fresh unique rigid type variable.
-    fn fresh_cst(&mut self) -> TypeWrapper {
+    fn fresh_cst<E: TermEnvironment>(&mut self) -> GenericTypeWrapper<E> {
         let result = self.var_uid;
         self.var_uid += 1;
-        TypeWrapper::Constant(result)
+        GenericTypeWrapper::Constant(result)
     }
 
     /// Try to consume one unit of gas for a variable substitution. Return true in case of success,
@@ -127,24 +163,24 @@ impl State {
 ///
 /// - `env`: an environment mapping variables to their definition (the second placeholder in a
 ///   `let _ = _ in _`)
-pub fn contract_eq(
+pub fn contract_eq<E: TermEnvironment>(
     var_uid: usize,
     t1: &RichTerm,
-    env1: &TermEnvironment,
+    env1: &E,
     t2: &RichTerm,
-    env2: &TermEnvironment,
+    env2: &E,
 ) -> bool {
     contract_eq_bounded(&mut State::new(var_uid), t1, env1, t2, env2)
 }
 
 /// Decide type equality on contracts in their respective environment and given the remaining gas
 /// `gas`.
-fn contract_eq_bounded(
+fn contract_eq_bounded<E: TermEnvironment>(
     state: &mut State,
     t1: &RichTerm,
-    env1: &TermEnvironment,
+    env1: &E,
     t2: &RichTerm,
-    env2: &TermEnvironment,
+    env2: &E,
 ) -> bool {
     use Term::*;
 
@@ -188,34 +224,38 @@ fn contract_eq_bounded(
         // if they have the same identifier: whatever global environment the term will be put in,
         // free variables are not redefined locally and will be bound to the same value in any case.
         (Var(id1), Var(id2)) => {
-            match (env1.0.get(id1), env2.0.get(id2)) {
-                (None, None) => id1 == id2,
-                (Some((t1, env1)), Some((t2, env2))) => {
-                    // We may end up using one more gas unit if gas was exactly 1. That is not very
-                    // important, and it's simpler to just ignore this case. We still return false
-                    // if gas was already at zero.
-                    let had_gas = state.use_gas();
-                    state.use_gas();
-                    had_gas && contract_eq_bounded(state, &t1, &env1, &t2, &env2)
-                }
-                _ => false,
-            }
+            env1.get_then(id1, |binding1| {
+                env2.get_then(id2, |binding2| {
+                    match (binding1, binding2) {
+                        (None, None) => id1 == id2,
+                        (Some((t1, env1)), Some((t2, env2))) => {
+                            // We may end up using one more gas unit if gas was exactly 1. That is not very
+                            // important, and it's simpler to just ignore this case. We still return false
+                            // if gas was already at zero.
+                            let had_gas = state.use_gas();
+                            state.use_gas();
+                            had_gas && contract_eq_bounded(state, t1, env1, t2, env2)
+                        }
+                        _ => false,
+                    }
+                })
+            })
         }
         (Var(id), _) => {
             state.use_gas()
-                && env1
-                    .0
-                    .get(id)
-                    .map(|(t1, env1)| contract_eq_bounded(state, &t1, &env1, t2, env2))
-                    .unwrap_or(false)
+                && env1.get_then(id, |binding| {
+                    binding
+                        .map(|(t1, env1)| contract_eq_bounded(state, t1, env1, t2, env2))
+                        .unwrap_or(false)
+                })
         }
         (_, Var(id)) => {
             state.use_gas()
-                && env2
-                    .0
-                    .get(id)
-                    .map(|(t2, env2)| contract_eq_bounded(state, t1, env1, &t2, &env2))
-                    .unwrap_or(false)
+                && env2.get_then(id, |binding| {
+                    binding
+                        .map(|(t2, env2)| contract_eq_bounded(state, t1, env1, t2, env2))
+                        .unwrap_or(false)
+                })
         }
         (Record(m1, attrs1), Record(m2, attrs2)) => {
             map_eq(contract_eq_bounded, state, m1, env1, m2, env2) && attrs1 == attrs2
@@ -256,9 +296,9 @@ fn contract_eq_bounded(
                 (None, None) => true,
                 (Some(ctr1), Some(ctr2)) => type_eq_bounded(
                     state,
-                    &TypeWrapper::from_type(ctr1.types.clone(), env1), // &TypeWrapper::from(ctr1.types.clone()),
+                    &GenericTypeWrapper::from_type(ctr1.types.clone(), env1), // &TypeWrapper::from(ctr1.types.clone()),
                     env1,
-                    &TypeWrapper::from_type(ctr2.types.clone(), env2), // &TypeWrapper::from(ctr1.types.clone()),
+                    &GenericTypeWrapper::from_type(ctr2.types.clone(), env2), // &TypeWrapper::from(ctr1.types.clone()),
                     env2,
                 ),
                 _ => false,
@@ -275,16 +315,16 @@ fn contract_eq_bounded(
 }
 
 /// Compute the equality between two hashmaps holding either types or terms.
-fn map_eq<V, F>(
+fn map_eq<V, F, E>(
     mut f: F,
     state: &mut State,
     map1: &HashMap<Ident, V>,
-    env1: &TermEnvironment,
+    env1: &E,
     map2: &HashMap<Ident, V>,
-    env2: &TermEnvironment,
+    env2: &E,
 ) -> bool
 where
-    F: FnMut(&mut State, &V, &TermEnvironment, &V, &TermEnvironment) -> bool,
+    F: FnMut(&mut State, &V, &E, &V, &E) -> bool,
 {
     map1.len() == map2.len()
         && map1.iter().all(|(id, v1)| {
@@ -298,7 +338,9 @@ where
 ///
 /// Require the rows to be closed (i.e. the last element must be `RowEmpty`), otherwise `None` is
 /// returned. `None` is returned as well if a type encountered is not row, or if it is a enum row.
-fn rows_as_map(ty: &TypeWrapper) -> Option<HashMap<Ident, &TypeWrapper>> {
+fn rows_as_map<E: TermEnvironment>(
+    ty: &GenericTypeWrapper<E>,
+) -> Option<HashMap<Ident, &GenericTypeWrapper<E>>> {
     let mut map = HashMap::new();
 
     ty.iter_as_rows().try_for_each(|item| match item {
@@ -317,7 +359,7 @@ fn rows_as_map(ty: &TypeWrapper) -> Option<HashMap<Ident, &TypeWrapper>> {
 /// Require the rows to be closed (i.e. the last element must be `RowEmpty`), otherwise `None` is
 /// returned. `None` is returned as well if a type encountered is not row type, or if it is a
 /// record row.
-fn rows_as_set(ty: &TypeWrapper) -> Option<HashSet<Ident>> {
+fn rows_as_set<E: TermEnvironment>(ty: &GenericTypeWrapper<E>) -> Option<HashSet<Ident>> {
     let mut set = HashSet::new();
 
     ty.iter_as_rows().try_for_each(|item| match item {
@@ -341,15 +383,15 @@ fn rows_as_set(ty: &TypeWrapper) -> Option<HashSet<Ident>> {
 /// all the rigid type variables encountered have been introduced by `type_eq_bounded` itself. This
 /// is why we don't need unique identifiers that are distinct from the one used during
 /// typechecking, and we can just start from `0`.
-fn type_eq_bounded(
+fn type_eq_bounded<E: TermEnvironment>(
     state: &mut State,
-    ty1: &TypeWrapper,
-    env1: &TermEnvironment,
-    ty2: &TypeWrapper,
-    env2: &TermEnvironment,
+    ty1: &GenericTypeWrapper<E>,
+    env1: &E,
+    ty2: &GenericTypeWrapper<E>,
+    env2: &E,
 ) -> bool {
     match (ty1, ty2) {
-        (TypeWrapper::Concrete(s1), TypeWrapper::Concrete(s2)) => match (s1, s2) {
+        (GenericTypeWrapper::Concrete(s1), GenericTypeWrapper::Concrete(s2)) => match (s1, s2) {
             (AbsType::Wildcard(id1), AbsType::Wildcard(id2)) => id1 == id2,
             (AbsType::Dyn(), AbsType::Dyn())
             | (AbsType::Num(), AbsType::Num())
@@ -370,12 +412,12 @@ fn type_eq_bounded(
                 rows1.is_some() && rows2.is_some() && rows1 == rows2
             }
             (AbsType::StaticRecord(tyw1), AbsType::StaticRecord(tyw2)) => {
-                fn type_eq_bounded_wrapper(
+                fn type_eq_bounded_wrapper<E: TermEnvironment>(
                     state: &mut State,
-                    tyw1: &&TypeWrapper,
-                    env1: &TermEnvironment,
-                    tyw2: &&TypeWrapper,
-                    env2: &TermEnvironment,
+                    tyw1: &&GenericTypeWrapper<E>,
+                    env1: &E,
+                    tyw2: &&GenericTypeWrapper<E>,
+                    env2: &E,
                 ) -> bool {
                     type_eq_bounded(state, *tyw1, env1, *tyw2, env2)
                 }
@@ -391,7 +433,7 @@ fn type_eq_bounded(
                 contract_eq_bounded(state, t1, env1, t2, env2)
             }
             (AbsType::Forall(i1, tyw1), AbsType::Forall(i2, tyw2)) => {
-                let constant_type: TypeWrapper = state.fresh_cst();
+                let constant_type: GenericTypeWrapper<E> = state.fresh_cst();
 
                 type_eq_bounded(
                     state,
@@ -405,14 +447,14 @@ fn type_eq_bounded(
             // all type variables should have been substituted at this point, so we bail out.
             _ => false,
         },
-        (TypeWrapper::Ptr(p1), TypeWrapper::Ptr(p2)) => {
+        (GenericTypeWrapper::Ptr(p1), GenericTypeWrapper::Ptr(p2)) => {
             debug_assert!(
                 false,
                 "we shouldn't come across unification variables during type equality computation"
             );
             p1 == p2
         }
-        (TypeWrapper::Constant(i1), TypeWrapper::Constant(i2)) => i1 == i2,
+        (GenericTypeWrapper::Constant(i1), GenericTypeWrapper::Constant(i2)) => i1 == i2,
         _ => false,
     }
 }
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index b8b663e4..45d74bf7 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -71,7 +71,7 @@ pub mod reporting;
 pub mod mk_typewrapper;
 pub mod eq;
 
-use eq::TermEnvironment;
+use eq::{SimpleTermEnvironment, TermEnvironment};
 use error::*;
 use operation::{get_bop_type, get_nop_type, get_uop_type};
 
@@ -85,7 +85,7 @@ pub type Wildcards = Vec<Types>;
 #[derive(Debug, PartialEq, Clone)]
 pub struct Context {
     pub type_env: Environment,
-    pub term_env: TermEnvironment,
+    pub term_env: SimpleTermEnvironment,
 }
 
 #[derive(Clone, Debug)]
@@ -102,7 +102,7 @@ pub fn mk_initial_env(initial_env: Vec<RichTerm>) -> Result<Environment, EnvBuil
                 Ok(rec.iter().map(|(id, rt)| {
                     (
                         id.clone(),
-                        infer_record_type(rt.as_ref(), &TermEnvironment::new()),
+                        infer_record_type(rt.as_ref(), &SimpleTermEnvironment::new()),
                     )
                 }))
             } else {
@@ -121,7 +121,7 @@ pub fn mk_initial_env(initial_env: Vec<RichTerm>) -> Result<Environment, EnvBuil
 pub fn env_add_term(
     env: &mut Environment,
     rt: &RichTerm,
-    term_env: &TermEnvironment,
+    term_env: &SimpleTermEnvironment,
     resolver: &dyn ImportResolver,
 ) -> Result<(), EnvBuildError> {
     let RichTerm { term, pos } = rt;
@@ -150,7 +150,7 @@ pub fn env_add(env: &mut Environment, id: Ident, rt: &RichTerm, resolver: &dyn I
         id,
         TypeWrapper::from_apparent_type(
             apparent_type(rt.as_ref(), Some(env), Some(resolver)),
-            &TermEnvironment::new(),
+            &SimpleTermEnvironment::new(),
         ),
     );
 }
@@ -221,7 +221,7 @@ where
             &mut state,
             Context {
                 type_env: initial_env,
-                term_env: TermEnvironment::new(),
+                term_env: SimpleTermEnvironment::new(),
             },
             &mut building,
             linearizer.scope(),
@@ -926,7 +926,7 @@ fn replace_wildcards_with_var(
     table: &mut UnifTable,
     wildcard_vars: &mut Vec<TypeWrapper>,
     ty: Types,
-    env: &TermEnvironment,
+    env: &SimpleTermEnvironment,
 ) -> TypeWrapper {
     match ty.0 {
         AbsType::Wildcard(i) => get_wildcard_var(table, wildcard_vars, i),
@@ -1030,7 +1030,7 @@ pub fn apparent_type(
 
 /// Infer the type of a non annotated record by gathering the apparent type of the fields. It's
 /// currently used essentially to type the stdlib.
-pub fn infer_record_type(t: &Term, term_env: &TermEnvironment) -> TypeWrapper {
+pub fn infer_record_type(t: &Term, term_env: &SimpleTermEnvironment) -> TypeWrapper {
     match t {
         // An explicit annotation must take precedence over this inference, so let's use it.
         t @ Term::MetaValue(MetaValue {
@@ -1056,7 +1056,10 @@ pub fn infer_record_type(t: &Term, term_env: &TermEnvironment) -> TypeWrapper {
             })),
         ))
         .into(),
-        t => TypeWrapper::from_apparent_type(apparent_type(t, None, None), &TermEnvironment::new()),
+        t => TypeWrapper::from_apparent_type(
+            apparent_type(t, None, None),
+            &SimpleTermEnvironment::new(),
+        ),
     }
 }
 
@@ -1080,66 +1083,60 @@ fn has_wildcards(ty: &Types) -> bool {
 
 /// The types on which the unification algorithm operates, which may be either a concrete type, a
 /// type constant or a unification variable.
+///
+/// Contracts store an additional term environment for contract equality checking, which is
+/// represented by `E`. The typechecker always uses the same type for `E`. However, the evaluation
+/// phase may also resort to checking contract equality, using a different environment
+/// representation, hence the parametrization.
 #[derive(Clone, PartialEq, Debug)]
-pub enum TypeWrapper {
+pub enum GenericTypeWrapper<E: TermEnvironment + Clone> {
     /// A concrete type (like `Num` or `Str -> Str`).
-    Concrete(AbsType<Box<TypeWrapper>>),
+    Concrete(AbsType<Box<GenericTypeWrapper<E>>>),
     /// A contract, seen as an opaque type. In order to compute type equality between contracts or
     /// between a contract and a type, we need to carry an additional environment. This is why we
     /// don't reuse the variant from [`crate::types::AbsType`].
-    Contract(RichTerm, TermEnvironment),
+    Contract(RichTerm, E),
     /// A rigid type constant which cannot be unified with anything but itself.
     Constant(usize),
     /// A unification variable.
     Ptr(usize),
 }
 
-impl std::convert::TryInto<Types> for TypeWrapper {
+impl<E: TermEnvironment + Clone> std::convert::TryInto<Types> for GenericTypeWrapper<E> {
     type Error = ();
 
     fn try_into(self) -> Result<Types, ()> {
         match self {
-            TypeWrapper::Concrete(ty) => {
+            GenericTypeWrapper::Concrete(ty) => {
                 let converted: AbsType<Box<Types>> = ty.try_map(|tyw_boxed| {
                     let ty: Types = (*tyw_boxed).try_into()?;
                     Ok(Box::new(ty))
                 })?;
                 Ok(Types(converted))
             }
-            TypeWrapper::Contract(t, _) => Ok(Types(AbsType::Flat(t))),
+            GenericTypeWrapper::Contract(t, _) => Ok(Types(AbsType::Flat(t))),
             _ => Err(()),
         }
     }
 }
 
-impl TypeWrapper {
+impl<E: TermEnvironment + Clone> GenericTypeWrapper<E> {
     /// Create a TypeWrapper from a Types. Contracts are represented as the separate variant
     /// [`TypeWrapper::Contract`] which also stores a term environment, required for checking type
     /// equality involving contracts.
-    pub fn from_type(ty: Types, env: &TermEnvironment) -> Self {
+    pub fn from_type(ty: Types, env: &E) -> Self {
         match ty.0 {
-            AbsType::Flat(t) => TypeWrapper::Contract(t.clone(), env.clone()),
-            ty => TypeWrapper::Concrete(ty.map(|ty_| Box::new(TypeWrapper::from_type(*ty_, env)))),
-        }
-    }
-
-    /// Create a TypeWrapper from an apparent type. As for [`from_type`], this function requires
-    /// the current term environment.
-    pub fn from_apparent_type(at: ApparentType, env: &TermEnvironment) -> Self {
-        match at {
-            ApparentType::Annotated(ty) if has_wildcards(&ty) => {
-                TypeWrapper::Concrete(AbsType::Dyn())
-            }
-            ApparentType::Annotated(ty)
-            | ApparentType::Inferred(ty)
-            | ApparentType::Approximated(ty) => TypeWrapper::from_type(ty, env),
-            ApparentType::FromEnv(tyw) => tyw,
+            AbsType::Flat(t) => GenericTypeWrapper::Contract(t.clone(), env.clone()),
+            ty => GenericTypeWrapper::Concrete(
+                ty.map(|ty_| Box::new(GenericTypeWrapper::from_type(*ty_, env))),
+            ),
         }
     }
 
     /// Substitute all the occurrences of a type variable for a typewrapper.
-    pub fn subst(self, id: Ident, to: TypeWrapper) -> TypeWrapper {
-        use self::TypeWrapper::*;
+    pub fn subst(self, id: Ident, to: GenericTypeWrapper<E>) -> GenericTypeWrapper<E> {
+        use self::GenericTypeWrapper::*;
+
         match self {
             Concrete(AbsType::Var(ref i)) if *i == id => to,
             Concrete(AbsType::Forall(i, t)) => {
@@ -1191,11 +1188,29 @@ impl TypeWrapper {
     /// The iterator continues as long as the next item is of the form `RowExtend(..)`, and
     /// stops once it reaches `RowEmpty` (which ends iteration), or something else which is not a
     /// `RowExtend` (which produces a last item [`typecheck::RowIteratorItem::Tail`]).
-    pub fn iter_as_rows(&self) -> RowIterator<'_, TypeWrapper> {
+    pub fn iter_as_rows(&self) -> RowIterator<'_, GenericTypeWrapper<E>> {
         RowIterator { next: Some(self) }
     }
 }
 
+impl GenericTypeWrapper<SimpleTermEnvironment> {
+    /// Create a TypeWrapper from an apparent type. As for [`from_type`], this function requires
+    /// the current term environment.
+    pub fn from_apparent_type(at: ApparentType, env: &SimpleTermEnvironment) -> Self {
+        match at {
+            ApparentType::Annotated(ty) if has_wildcards(&ty) => {
+                GenericTypeWrapper::Concrete(AbsType::Dyn())
+            }
+            ApparentType::Annotated(ty)
+            | ApparentType::Inferred(ty)
+            | ApparentType::Approximated(ty) => GenericTypeWrapper::from_type(ty, env),
+            ApparentType::FromEnv(tyw) => tyw,
+        }
+    }
+}
+
+pub type TypeWrapper = GenericTypeWrapper<SimpleTermEnvironment>;
+
 // This implementation assumes that `AbsType::Flat` is not possible. If TypeWrappers have been
 // correctly created from a type using `from_type`, this must be the case.
 impl From<AbsType<Box<TypeWrapper>>> for TypeWrapper {
@@ -1205,13 +1220,13 @@ impl From<AbsType<Box<TypeWrapper>>> for TypeWrapper {
     }
 }
 
-impl<'a> Iterator for RowIterator<'a, TypeWrapper> {
-    type Item = RowIteratorItem<'a, TypeWrapper>;
+impl<'a, E: TermEnvironment> Iterator for RowIterator<'a, GenericTypeWrapper<E>> {
+    type Item = RowIteratorItem<'a, GenericTypeWrapper<E>>;
 
     fn next(&mut self) -> Option<Self::Item> {
         self.next.and_then(|next| match next {
-            TypeWrapper::Concrete(AbsType::RowEmpty()) => None,
-            TypeWrapper::Concrete(AbsType::RowExtend(id, ty_row, tail)) => {
+            GenericTypeWrapper::Concrete(AbsType::RowEmpty()) => None,
+            GenericTypeWrapper::Concrete(AbsType::RowExtend(id, ty_row, tail)) => {
                 self.next = Some(tail);
                 Some(RowIteratorItem::Row(id, ty_row.as_ref().map(Box::as_ref)))
             }
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


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!(