Repository: tweag/nickel
Pull request #631 (2022-03-02 17:03:44)

Reduce memory leaks by attaching free variables to record fields
# Free vars pass

Partially address #389. Continuation of #543 and #588. The idea is to annotate the fields of recursive records with their free variables (or, more precisely, with the other fields of the record that syntactically appear in their definition, that is the intersection of their free variables and the set of fields of the record) during a transformation pass, and leverage this information when building the fixpoint to avoid undue leaks.

Thanks to this data, we can add to the local environment of each fields only those fields that they use (or, at least, that appear in their definition). Before, every field was added, creating cycles of reference-counted pointers (and thus leaks) in pretty much any record:

```nickel
{
  a = "foo",
  b = a ++ " bar",
  c = b ++ " baz",
}
```

Before this PR, this recursive record would evaluate to an object where each field `a`, `b` and `c` retains a reference (`Rc<RefCell<_>>`) to all other fields, thus creating cycles that wouldn't be reclaimed (`a` -> `a`, `a` -> `b` -> `a`, etc).

After this PR, `a` retains no reference to its siblings, `b` only retains a reference to `a`, and `c` only to `b`. This is a DAG that should be deallocated without problem. Only mutually recursive fields like `{foo = fun a => bar (a +1), bar = fun a => foo (a + 1)}` should leak.

## Content

This PR:

- Augment the `RecRecord` variant to store additional free variables data
- Add a free_vars pass to fill those data during program transformation. In #543 and #588, @Avi-D-coder  tried various approaches to avoid having to do a separate pass or suffer a quadratic complexity for this pass. It turns out it is difficult to both avoid adding a whole new traversal just for free variables and not butcher the current term traversal interface. In the end, I went for a separate traversal. Given the current state, I don't expect it to have bad consequences, and that most of the time is taken by evaluation anyway. This makes the change simpler and a better separation of matters.
- Use the additional data when creating the fixpoint of a recursive records. This requires to persist the free vars data beyond the first evaluation of a recursive records, because since overriding, we produce new recursive records in the middle of evaluation when merging. The free vars are thus directly attached to the revertible thunks introduced by recursive records. This brings a bonus: we can now detect at transformation time expressions that don't actually depend on the other fields of a record recursively, and don't bother introducing a revertible thunk in this case, that would be recomputed at each subsequent merge and consume more memory.
- add unit tests for the computation of free variables.
 


Patch:
diff --git a/Cargo.lock b/Cargo.lock
index d73ac2f2..0b81a994 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1910,6 +1910,7 @@ checksum = "936e4b492acfd135421d8dca4b1aa80a7bfc26e702ef3af710e0752684df5372"
 name = "utilities"
 version = "0.1.0"
 dependencies = [
+ "codespan",
  "criterion",
  "nickel",
 ]
diff --git a/doc/manual/contracts.md b/doc/manual/contracts.md
index 59de1811..eb85ba33 100644
--- a/doc/manual/contracts.md
+++ b/doc/manual/contracts.md
@@ -1,8 +1,4 @@
----
-slug: contracts
----
-
-# Contracts in Nickel
+# Contracts
 
 (For the motivation behind contracts and a high-level overview of contracts and
 types, first read the [correctness](./correctness.md) section.)
@@ -198,7 +194,7 @@ given format:
 ```nickel
 let Nullable = fun contract label value =>
   if value == null then
-    value
+    value 
   else
     contract.apply contract label value in
 // succeeds
@@ -222,7 +218,7 @@ missing:
 ```nickel
 let MyConfig = {
   path | Str,
-
+ 
   connection | {
     server_port | Port,
     host | Str,
@@ -414,7 +410,7 @@ We've already seen that the primitive types `Num`, `Str` and `Bool` can be used
 as contracts. In fact, any type constructor of the
 [static type system](./typing.md) can be used to combine contracts.
 
-#### Array
+#### Array 
 
 An array contract checks that the value is an array and applies the parameter
 contract to each element:
@@ -437,6 +433,9 @@ error: contract broken by a value.
 [..]
 ```
 
+Recall that `Array` is an alias for `Array Dyn`, thus the `Array` contracts only
+checks that the value is an array.
+
 #### Functions
 
 A function contract `In -> Out` returns a wrapped function which, for each call,
diff --git a/doc/manual/cookbook.md b/doc/manual/cookbook.md
index 02bca2bb..a4eb2088 100644
--- a/doc/manual/cookbook.md
+++ b/doc/manual/cookbook.md
@@ -1,7 +1,3 @@
----
-slug: cookbook
----
-
 # Cookbook
 
 For now, this is an unorganized, temporary document not to forget some pieces of
diff --git a/doc/manual/correctness.md b/doc/manual/correctness.md
index 95ae5125..018a6c0e 100644
--- a/doc/manual/correctness.md
+++ b/doc/manual/correctness.md
@@ -1,8 +1,4 @@
----
-slug: correctness
----
-
-# Correctness in Nickel
+# Correctness
 
 One of the main value proposition of Nickel is to make configurations
 programmable. However, a not less important one is to help you write *correct*
@@ -101,7 +97,7 @@ types and contracts directly follow from this distinction.
 In the next paragraphs, we consider two typical examples to illustrate the
 difference between types and contracts in practice.
 
-### Case 1: a function operating on arrays
+### Case 1: a function operating on arrays 
 
 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`:
diff --git a/doc/manual/merging.md b/doc/manual/merging.md
deleted file mode 100644
index 5fffd4fe..00000000
--- a/doc/manual/merging.md
+++ /dev/null
@@ -1,526 +0,0 @@
----
-slug: merging
----
-
-# Merging records
-
-In Nickel, the basic building blocks for data are records (objects in JSON or
-attribute sets in Nix). Merging is a fundamental built-in operation whose role
-is to combine records togethers. Fields common to several records will be
-themselves recursively merged if possible, following the semantics described in
-this document.
-
-Merging is useful to compose small and logical blocks into a potentially complex
-final configuration, making it more manageable. A merge is performed by the `&`
-operator.
-
-Merge is a **symmetric** operation (or, pedantically, commutative). In practice,
-this means that order doesn't matter, and `left & right` is the same thing as
-`right & left`. When the operands need to be distinguished, as we will see for
-default values for example, the idea is to use metadata to do so (annotations),
-rather than relying on the left or right position.
-
-**Warning**: At the time of writing, Nickel's version is 0.1. Important
-additions to merging are planned for coming versions, including priorities and
-custom merge functions. They are not detailed here yet. For more details, see
-the associated technical document [RFC001][rfc001].
-
-The section describes the behavior and use-cases of merge, by considering the
-following situations:
-
-- [Merging two records without common fields](#simple-merge-(no-common-fields))
-- [Merging records with common fields](#recursive-merge-(with-common-fields))
-- [Merging records with metadata](#merging-record-with-metadata)
-  * [Default values](#default-values)
-  * [Contracts](#contracts)
-  * [Documentation](#documentation)
-- [Recursive overriding](#recursive-overriding)
-
-## Simple merge (no common fields)
-
-Merging two records with no common fields results in a record with the fields
-from both operands. That is, `{foo = 1, bar = "bar"} & {baz =false}` evaluates
-to `{foo = 1, bar = "bar", baz = false}`.
-
-### Specification
-
-Technically, if we write the left operand as:
-
-```
-left = {
-  field_left_1 = value_left_1,
-  ..,
-  field_left_n = value_left_n,
-}
-```
-
-And the right operand as:
-
-```
-right {
-  field_right_1 = value_right_1,
-  ..,
-  field_right_k = value_right_k
-}
-```
-
-Then the merge `left & right` evaluates to the record:
-
-```
-{
-  field_left_1 = value_left_1,
-  ..,
-  field_left_n = value_left_n,
-  field_right_1 = value_right_1,
-  ..,
-  field_right_k = value_right_k
-}
-```
-
-In other terms, `left & right` is the union of `left` and `right`.
-
-### Examples
-
-#### Split
-
-You can split a configuration into subdomains:
-
-```nickel
-// file: server.ncl
-{
-    host_name = "example",
-    host = "example.org",
-    ip_addr = "0.0.0.0",
-}
-
-// file: firewall.ncl
-{
-    enable_firewall = true,
-    open_ports = [23, 80, 443],
-}
-
-// file: network.ncl
-let server = import "server.ncl" in
-let firewall = import "firewall.ncl" in
-server & firewall
-```
-
-This gives:
-
-```nickel
-{
-    host_name = "example",
-    host = "example.org",
-    ip_addr = "0.0.0.0",
-    enable_firewall = true,
-    open_ports = [23, 80, 443],
-}
-```
-
-#### Extension
-
-Given a configuration, you can use merge to add new fields:
-
-```nickel
-// file: safe-network.ncl
-let base = import "network.ncl" in
-base & {use_iptables = true}
-```
-
-## Recursive merge (with common fields)
-
-When the two operands have fields in common, those fields are recursively
-merged. For example:
-
-```nickel
-{
-  top_left = 1,
-  common = {left = "left"}}
-& {
-  top_right = 2,
-  common = {right = "right"}
-}
-```
-
-Evaluates to the record:
-
-```nickel
-{
-  top_left = 1,
-  top_right = 2,
-  common = {left = "left", right = "right"}
-}
-```
-
-When one or both of the common fields are not records, the merge will fail
-unless one of the following condition hold:
-
-- They are both of a primitive data type `Num`, `Bool`, `Enum`, `String` and
-  they are equal
-- They are both null
-
-### Specification
-
-```
-left = {
-  field_left_1 = value_left_1,
-  ..,
-  field_left_n = value_left_n,
-  common_1 = common_vleft_1,
-  ..,
-  common_m = common_vleft_m,
-}
-```
-
-And the right operand as:
-
-```
-right {
-  field_right_1 = value_right_1,
-  ..,
-  field_right_k = value_right_k
-  common_1 = common_vright_1,
-  ..,
-  common_m = common_vright_m,
-}
-```
-
-Where the `field_left_i` and `field_right_j` are distinct for all `i` and `j`.
-Then the merge `left & right` evaluates to the record:
-
-```
-{
-  field_left_1 = value_left_1,
-  ..,
-  field_left_n = value_left_n,
-  field_right_1 = value_right_1,
-  ..,
-  field_right_k = value_right_k
-  common_1 = common_vleft_1 & common_vright_1,
-  ..,
-  common_m = common_vleft_m & common_vright_m,
-}
-```
-
-For two values `v1` and `v2`, if at least one value is not a record, then
-
-```
-v1 & v2 = v1    if (type_of(v1) is Num, Bool, Str, Enum or v1 == null)
-                   AND v1 == v2
-          _|_   otherwise (indicates failure)
-```
-
-### Example
-
-```nickel
-// file: udp.ncl
-{
-    // same as firewall = {open_ports = {udp = [...]}},
-    firewall.open_ports.udp = [12345,12346],
-}
-
-// file: tcp.ncl
-{
-    // same as firewall = {open_ports = {tcp = [...]}},
-    firewall.open_ports.tcp = [23, 80, 443],
-}
-
-// firewall.ncl
-let udp = import "udp.ncl" in
-let tcp = import "tcp.ncl" in
-udp & tcp
-```
-
-In the above example, we merge two records, both with a field `firewall`. On
-both sides, the value is a record, which is therefore merged. The same process
-happens one layer below, on the common field `open_ports`, to result in the
-final record:
-
-```nickel
-{
-    firewall = {
-      open_ports = {
-        udp = [12345, 12346],
-        tcp = [23, 80, 443],
-      }
-    }
-}
-```
-
-## Merging record with metadata
-
-Metadata can be attached to values thanks to the `|` operator. Metadata
-currently includes contract annotations, default value, and documentation. We
-describe in this section how metadata interacts with merging.
-
-### 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}`. 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
-
-We can consider the merging system to feature priorities. To each field
-definition `foo = val` is associated a priority `p(val)`. When merging two
-common fields `value_left` and `value_right`, then the results is either the one
-with the highest priority (that overrides the other), or the two are tentatively
-recursively merged, if the priorities are the same. Without loss of generality,
-we consider the simple case of two records with only one field, which is the
-same on both side:
-
-```
-{common = left} & {common = right}
-= {
-  common = left          if p(left) > p(right)
-           right         if p(left) < p(right)
-           left & right  if p(left) = p(right)
-}
-```
-
-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
-restrictive configuration by default, which can still be overridden if needed.
-
-Let us first try without default values:
-
-```nickel
-let base = {
-  firewall.enabled = true,
-  firewall.type = "iptables",
-  firewall.open_ports = [21, 80, 443],
-} in
-let patch = {
-  firewall.enabled = false,
-  server.host.options = "TLS",
-} in
-base & patch
-```
-
-Because merging is meant to be symmetric, Nickel is unable to know which value
-to pick between `enabled = true` and `enabled = false` for the firewall, and
-thus fail:
-
-```
-error: non mergeable terms
-  ┌─ repl-input-0:2:22
-  │
-2 │   firewall.enabled = true,
-  │                      ^^^^ cannot merge this expression
-  ·
-7 │   firewall.enabled = false,
-  │                      ^^^^^ with this expression
-
-```
-
-We can use default values to give the priority to the right side:
-
-```nickel
-let base = {
-  firewall.enabled | default = true,
-  firewall.type | default = "iptables",
-  firewall.open_ports | default = [21, 80, 443],
-} in
-let patch = {
-  firewall.enabled = false,
-  server.host.options = "TLS",
-} in
-base & patch
-```
-
-This evaluates to:
-
-```
-{
-  firewall = {
-    enabled = false,
-    open_ports = [21, 80, 443],
-    type = "iptables",
-  },
-  server = {
-    host = {
-      "options": "TLS"
-    }
-  }
-}
-```
-
-### Contracts
-
-*Note*: see the [correctness section](./correctness.md) and the
-[contracts section](./contracts.md) for a thorough introduction to contracts in
-Nickel.
-
-Fields may have contracts attached, either directly, as in `{foo | Num = 1}`, or
-propagated from an annotation higher up, as in `{foo = 1} | {foo | Num}`. In
-both cases, `foo` must satisfy the contract `Num`. What happens if the value of
-`foo` is altered in a subsequent merge? For example:
-
-- Should `{foo | default | Num = 1} & {foo = "bar"}` succeed, although `foo`
-  would be a string in the final result?
-- Should `{foo.subfield | Str = "a"} & {foo.other_subfield = 1}`
-  succeed, although a closed contract `{subfield | Str}` is attached to `foo`,
-  and the final result would have an additional field `other_subfield` ?
-
-Nickel chooses to answer **no** to both. In general, when a contract is attached
-to a field `foo`, merging ensures that whatever is this field merged with,
-including being dropped in favor of another value, the final value for `foo` has
-to respect the contract as well or the evaluation will fail accordingly.
-
-#### Specification
-
-For two operands with one field each, which is the same on both side, with respective
-contracts `Left1, .., Leftn` and `Right1, .., Rightk` attached:
-
-```nickel
-left = {
-  common | Left1
-         | ..
-         | Leftn
-}
-```
-
-And
-
-```nickel
-right = {
-  common | Right1
-         | ..
-         | Rightk
-}
-```
-
-Then the `common` field of `left & right` will be checked against `Left1, ..,
-Leftn, Right1, .., Rightk`. Here, we ignore the case of type annotations such as
-`common: LeftType` that can just be considered as an additional contract
-`Left0`.
-
-#### Example
-
-```nickel
-let Port
-  | doc "A valid port number"
-  = contract.from_predicate (fun value =>
-    builtin.is_num value &&
-    value % 1 == 0 &&
-    value >= 0 &&
-    value <= 65535) in
-let GreaterThan
-  | doc "A number greater than the paramater"
-  = fun x => contract.from_predicate (fun value => value > x) in
-
-{
-    port | GreaterThan 1024
-         | default = 8080,
-} & {
-    port | Port = 80,
-}
-```
-
-This fails at evaluation:
-
-```
-error: contract broken by a value.
-[..]
-   ┌─ repl-input-1:16:19
-   │
-16 │     port | Port = 80,
-   │                   ^^ applied to this expression
-
-note:
-   ┌─ repl-input-1:13:12
-   │
-13 │     port | GreaterThan 1024
-   │            ^^^^^^^^^^^^^^^^ bound here
-```
-
-
-### Documentation
-
-Documentation is attached via the `doc` keyword. Documentation is propagated
-during merging. For example, querying `foo` by using the command `nickel -f
-config.ncl query foo` on:
-
-```nickel
-// config.ncl
-{
-  foo | doc "Some documentation"
-      | = {}
-} & {
-  foo.field = null,
-}
-```
-
-Will print `"Some documentation"` as expected. If both sides have documentation, the behavior
-is unspecified, as merging two distinct blobs of text doesn't make sense
-in general. Currently, Nickel will randomly keeps one of the two in practice.
-
-## Recursive overriding
-
-We've seen in the section on default values that they are useful to override
-(update) a single field with a different value. The combo of merging and default
-values can do more. In Nickel, records are recursive by default, in order to
-express easily dependencies between the different fields of the configuration.
-Concretely, you can refer to other fields of a record from within this record:
-
-```nickel
-let base_config = {
-  version | default = "20.09",
-  input.url | default = "nixpkgs/nixos-%{version}",
-} in
-base_config
-```
-
-Here, we referred to `version` from the `input` field transparently. This
-configuration evaluates to:
-
-```nickel
-{
-  version = "20.09",
-  input = {url = "nixpkgs/nixos-20.09"},
-}
-```
-
-Merging handles overriding on recursive record too. More precisely, when we
-override the default value of `version`, *the fields that depend on `version` --
-here, `input` -- will also be updated automatically*. For example, `base_config
-& {version = "unstable"}` will evaluate to:
-
-```nickel
-{
-  version = "unstable",
-  input = {url = "nixpkgs/nixos-unstable"},
-}
-```
-
-Currently, one can only override a field that has been marked as default beforehand. A
-more ergonomic way of overriding is planned, and described in [RFC001][rfc001].
-
-### Example
-
-Here is another variation of recursive overriding on our `firewall` example:
-
-```nickel
-let security = {
-    firewall.open_proto.http | default = true,
-    firewall.open_proto.https | default = true,
-    firewall.open_proto.ftp | default = true,
-    firewall.open_ports = []
-        @ (if firewall.open_proto.ftp then [21] else [])
-        @ (if firewall.open_proto.http then [80] else [])
-        @ (if firewall.open_proto.https then [443] else []),
-} in // => security.firewall.open_ports = [21, 80, 443]
-security & {firewall.open_proto.ftp = false} // => firewall.open_ports = [80, 443]
-```
-
-Here, `security.firewall.open_ports` is `[21, 80, 443]`. But in the returned
-configuration (let's call it `result`), `result.firewall.open_ports = [80, 443]`.
-
-[rfc001]: https://github.com/tweag/nickel/blob/c21cf280dc610821fceed4c2caafedb60ce7177c/rfcs/001-overriding.md
diff --git a/doc/manual/syntax.md b/doc/manual/syntax.md
index cb4ff395..a6df77a0 100644
--- a/doc/manual/syntax.md
+++ b/doc/manual/syntax.md
@@ -1,16 +1,12 @@
----
-slug: syntax
----
-
 # Nickel Syntax
 
 ## Simple values
 
-There are three basic kind of values in Nickel :
- 1. numeric values,
+There are three basic kind of values in Nickel : 
+ 1. numeric values, 
  2. boolean values,
  3. strings.
-
+ 
 ### Numeric values
 
 Nickel has a support for numbers, positive and negative, with or without decimals.
@@ -35,7 +31,7 @@ There are a some predefined operators for working with numbers :
 | /        | The division operator                                | `1 / 2 = 0.5` |
 | %        | The modulo operator (returns the *signed* remainder) | `5 % 3 = 2`   |
 
-> **Remark about the `-` operator:**
+> **Remark about the `-` operator:**  
 > Since `-` can be used inside an identifier, the subtraction operators **needs** to be surrounded by spaces:
 > write `1 - 1`, not `1-1`.
 
@@ -123,7 +119,7 @@ This line has no more identation.
 "This line has no indentation.
   This line is indented.
     This line is even more indented.
-This line has no more indentation."
+This line has no more indentation." 
 ```
 
 The only special sequence in a multiline string is the string interpolation.
@@ -206,7 +202,7 @@ false
 
 ## Composite values
 
-### Array
+### Array 
 An array is a sequence of values. They are delimited by `[` and `]`, and elements are separated with `,`.
 
 Examples:
@@ -254,7 +250,7 @@ It is possible to write records of records via the *piecewise syntax*, where we
 ```
 > { a = { b = 1 } }
 { a = { b = 1 } }
-
+ 
 > { a.b = 1 }
 { a = { b = 1 } }
 
@@ -415,7 +411,7 @@ error: Blame error: contract broken by a value.
 3
 ```
 
-Adding documentation can be done with `| doc < string >`.
+Adding documentation can be done with `| doc < string >`.  
 Examples:
 ```
 > 5 | doc "The number five"
@@ -432,7 +428,7 @@ true
 
 Record contracts can set default values using the `default` metadata:
 It is noted as `| default = < default value >`.
-This is especially useful when merging records (more about this in the dedicated document about merge).
+This is especially useful when merging records (more about this in the dedicated document about merge).  
 Examples:
 ```
 > let Ais2ByDefault = { a | default = 2 } in
diff --git a/doc/manual/types-vs-contracts.md b/doc/manual/types-vs-contracts.md
index 68cd211e..4574cba2 100644
--- a/doc/manual/types-vs-contracts.md
+++ b/doc/manual/types-vs-contracts.md
@@ -1,8 +1,4 @@
----
-slug: type-vs-contract
----
-
-# Type vs contract: when to?
+# Type vs contracts: when to?
 
 You are writing Nickel code and wonder how it should be annotated. Leave it
 alone? Add type annotations? Use contracts? Here is a quick guide when you don't
diff --git a/doc/manual/typing.md b/doc/manual/typing.md
index d47be7b2..52e301d2 100644
--- a/doc/manual/typing.md
+++ b/doc/manual/typing.md
@@ -1,7 +1,3 @@
----
-slug: typing
----
-
 # Typing in Nickel
 
 (For the motivations behind typing and a high-level overview of contracts and
@@ -167,7 +163,8 @@ Let us now have a quick tour of the type system. The basic types are:
 
 The following type constructors are available:
 
-- **Array**: `Array T`. An array of elements of type `T`.
+- **Array**: `Array T`. An array of elements of type `T`. When no `T` is specified, `Array`
+  alone is an alias for `Array Dyn`.
 
   Example:
   ```nickel
diff --git a/lsp/nls/src/linearization/mod.rs b/lsp/nls/src/linearization/mod.rs
index a108face..812123f2 100644
--- a/lsp/nls/src/linearization/mod.rs
+++ b/lsp/nls/src/linearization/mod.rs
@@ -290,7 +290,7 @@ impl Linearizer for AnalysisHost {
                     }
                 }
             }
-            Term::Record(fields, _) | Term::RecRecord(fields, _, _) => {
+            Term::Record(fields, _) | Term::RecRecord(fields, ..) => {
                 lin.push(LinearizationItem {
                     id,
                     pos: pos.unwrap(),
@@ -340,7 +340,7 @@ impl Linearizer for AnalysisHost {
                             walk_terms(lin, host.scope(), rt1);
                             walk_terms(lin, host.scope(), rt2);
                         }
-                        Term::Record(rts, _) | Term::RecRecord(rts, _, _) => rts
+                        Term::Record(rts, _) | Term::RecRecord(rts, ..) => rts
                             .values()
                             .for_each(|rt| walk_terms(lin, host.scope(), rt)),
                         _ => {}
diff --git a/src/cache.rs b/src/cache.rs
index b6cd2ba7..2235228b 100644
--- a/src/cache.rs
+++ b/src/cache.rs
@@ -520,7 +520,7 @@ impl Cache {
                                 CacheError::Error(ImportError::ParseErrors(err.into(), pos))
                             })?;
                         }
-                        Term::RecRecord(ref mut map, ref mut dyn_fields, _) => {
+                        Term::RecRecord(ref mut map, ref mut dyn_fields, ..) => {
                             let map_res: Result<_, UnboundTypeVariableError> = std::mem::take(map)
                                 .into_iter()
                                 .map(|(id, t)| Ok((id, transform::transform(t)?)))
diff --git a/src/eval/fixpoint.rs b/src/eval/fixpoint.rs
index 6231bd97..9cfb0ab2 100644
--- a/src/eval/fixpoint.rs
+++ b/src/eval/fixpoint.rs
@@ -33,6 +33,11 @@ pub fn rec_env<'a, I: Iterator<Item = (&'a Ident, &'a RichTerm)>>(
 
 /// Update the environment of the content of a recursive record field by extending it with a
 /// recursive environment.
+///
+/// For each field, retrieve the set set of dependencies from the corresponding thunk in the
+/// environment, and only add those dependencies to the environment. This avoid retaining
+/// reference-counted pointers to unused data. If no dependencies are available, conservatively add
+/// all the recursive environment. See [`transform::free_var`].
 pub fn patch_field(
     rt: &RichTerm,
     rec_env: &Vec<(Ident, Thunk)>,
@@ -42,8 +47,19 @@ pub fn patch_field(
         let mut thunk = env
             .get(var_id)
             .ok_or_else(|| EvalError::UnboundIdentifier(var_id.clone(), rt.pos))?;
-        thunk.borrow_mut().env.extend(rec_env.iter().cloned());
+
+        let deps = thunk.deps();
+
+        match deps {
+            ThunkDeps::Known(deps) => thunk
+                .borrow_mut()
+                .env
+                .extend(rec_env.iter().filter(|(id, _)| deps.contains(id)).cloned()),
+            ThunkDeps::Unknown => thunk.borrow_mut().env.extend(rec_env.clone()),
+            ThunkDeps::Empty => (),
+        };
     }
+
     // Thanks to the share normal form transformation, the content is either a constant or a
     // variable. In the constant case, the environment is irrelevant and we don't have to do
     // anything in the `else` case.
diff --git a/src/eval/lazy.rs b/src/eval/lazy.rs
index df094d4e..e4ef43f4 100644
--- a/src/eval/lazy.rs
+++ b/src/eval/lazy.rs
@@ -1,6 +1,8 @@
 //! Thunks and associated devices used to implement lazy evaluation.
 use super::{Closure, IdentKind};
+use crate::{identifier::Ident, term::FieldDeps};
 use std::cell::{Ref, RefCell, RefMut};
+use std::collections::HashSet;
 use std::rc::{Rc, Weak};
 
 /// The state of a thunk.
@@ -29,14 +31,17 @@ pub struct ThunkData {
 /// The part of [ThunkData] responsible for storing the closure itself. It can either be:
 /// - A standard thunk, that is destructively updated once and for all
 /// - A revertible thunk, that can be restored to its original expression. Used to implement
-/// recursive merging of records and overriding (see the [RFC
-/// overriding](https://github.com/tweag/nickel/pull/330))
+///   recursive merging of records and overriding (see the
+///   [RFC overriding](https://github.com/tweag/nickel/pull/330)). A revertible thunks optionally
+///   stores the set of recusive fields it depends on. See the [`transform::free_vars`] for more
+///   details.
 #[derive(Clone, Debug, PartialEq)]
 pub enum InnerThunkData {
     Standard(Closure),
     Revertible {
         orig: Rc<Closure>,
         cached: Rc<Closure>,
+        deps: FieldDeps,
     },
 }
 
@@ -50,13 +55,14 @@ impl ThunkData {
     }
 
     /// Create new revertible thunk data.
-    pub fn new_rev(orig: Closure) -> Self {
+    pub fn new_rev(orig: Closure, deps: FieldDeps) -> Self {
         let rc = Rc::new(orig);
 
         ThunkData {
             inner: InnerThunkData::Revertible {
                 orig: rc.clone(),
                 cached: rc,
+                deps,
             },
             state: ThunkState::Suspended,
         }
@@ -82,7 +88,7 @@ impl ThunkData {
     pub fn into_closure(self) -> Closure {
         match self.inner {
             InnerThunkData::Standard(closure) => closure,
-            InnerThunkData::Revertible { orig, cached } => {
+            InnerThunkData::Revertible { orig, cached, .. } => {
                 std::mem::drop(orig);
                 Rc::try_unwrap(cached).unwrap_or_else(|rc| (*rc).clone())
             }
@@ -105,15 +111,29 @@ impl ThunkData {
     pub fn revert(&self) -> Self {
         match self.inner {
             InnerThunkData::Standard(_) => self.clone(),
-            InnerThunkData::Revertible { ref orig, .. } => ThunkData {
+            InnerThunkData::Revertible {
+                ref orig, ref deps, ..
+            } => ThunkData {
                 inner: InnerThunkData::Revertible {
                     orig: Rc::clone(orig),
                     cached: Rc::clone(orig),
+                    deps: deps.clone(),
                 },
                 state: ThunkState::Suspended,
             },
         }
     }
+
+    /// Return the potential field dependencies stored in a revertible thunk. See [`transform::free_vars`]
+    pub fn deps(&self) -> ThunkDeps {
+        match self.inner {
+            InnerThunkData::Standard(_) => ThunkDeps::Empty,
+            InnerThunkData::Revertible { ref deps, .. } => deps
+                .as_ref()
+                .map(|deps| ThunkDeps::Known(Rc::clone(deps)))
+                .unwrap_or(ThunkDeps::Unknown),
+        }
+    }
 }
 
 /// A thunk.
@@ -147,9 +167,9 @@ impl Thunk {
     }
 
     /// Create a new revertible thunk.
-    pub fn new_rev(closure: Closure, ident_kind: IdentKind) -> Self {
+    pub fn new_rev(closure: Closure, ident_kind: IdentKind, deps: FieldDeps) -> Self {
         Thunk {
-            data: Rc::new(RefCell::new(ThunkData::new_rev(closure))),
+            data: Rc::new(RefCell::new(ThunkData::new_rev(closure, deps))),
             ident_kind,
         }
     }
@@ -224,6 +244,27 @@ impl Thunk {
         let term = &self.borrow().body.term;
         !term.is_whnf() && !term.is_metavalue()
     }
+
+    /// Return a clone of the potential field dependencies stored in a revertible thunk. See
+    /// [`transform::free_vars`].
+    pub fn deps(&self) -> ThunkDeps {
+        self.data.borrow().deps().clone()
+    }
+}
+
+/// Possible alternatives for the field dependencies of a thunk.
+#[derive(Clone, Debug)]
+pub enum ThunkDeps {
+    /// The thunk is revertible, containing potential recursive references to other fields, and the
+    /// set of dependencies has been computed
+    Known(Rc<HashSet<Ident>>),
+    /// The thunk is revertible, but the set of dependencies hasn't been computed. In that case,
+    /// the interpreter should be conservative and assume that any recursive references can appear
+    /// in the content of the corresponding thunk.
+    Unknown,
+    /// The thunk is not revertible and can't contain recursive references. The interpreter can
+    /// safely eschews the environment patching process entirely.
+    Empty,
 }
 
 /// A thunk update frame.
diff --git a/src/eval/mod.rs b/src/eval/mod.rs
index 092b2a52..662497c7 100644
--- a/src/eval/mod.rs
+++ b/src/eval/mod.rs
@@ -366,7 +366,9 @@ where
 
                 let thunk = match btype {
                     BindingType::Normal => Thunk::new(closure, IdentKind::Let),
-                    BindingType::Revertible => Thunk::new_rev(closure, IdentKind::Let),
+                    BindingType::Revertible(deps) => {
+                        Thunk::new_rev(closure, IdentKind::Let, deps.clone())
+                    }
                 };
 
                 env.insert(x.clone(), thunk);
@@ -498,7 +500,7 @@ where
                     }
                 }
             }
-            Term::RecRecord(ts, dyn_fields, attrs) => {
+            Term::RecRecord(ts, dyn_fields, attrs, _) => {
                 let rec_env = fixpoint::rec_env(ts.iter(), &env)?;
 
                 ts.iter()
@@ -750,7 +752,7 @@ pub fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichT
 
                 RichTerm::new(Term::Record(map, attrs), pos)
             }
-            Term::RecRecord(map, dyn_fields, attrs) => {
+            Term::RecRecord(map, dyn_fields, attrs, deps) => {
                 let map = map
                     .into_iter()
                     .map(|(id, t)| {
@@ -771,7 +773,7 @@ pub fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichT
                     })
                     .collect();
 
-                RichTerm::new(Term::RecRecord(map, dyn_fields, attrs), pos)
+                RichTerm::new(Term::RecRecord(map, dyn_fields, attrs, deps), pos)
             }
             Term::Array(ts) => {
                 let ts = ts
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 5f14aba2..7e0274a2 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -241,7 +241,6 @@ Forall: Types =
 // also includes previous levels).
 Applicative: UniTerm = {
     "import" <s: StaticString> => UniTerm::from(Term::Import(OsString::from(s))),
-    AsUniTerm<TypeArray>,
     <t1: AsTerm<Applicative>> <t2: AsTerm<RecordOperand>> =>
         UniTerm::from(mk_app!(t1, t2)),
     <op: UOp> <t: AsTerm<RecordOperand>> => UniTerm::from(mk_term::op1(op, t)),
@@ -251,9 +250,25 @@ Applicative: UniTerm = {
     RecordOperand,
 };
 
-// The parametrized array type.
-TypeArray: Types = "Array" <AsType<Atom>> =>
-    Types(AbsType::Array(Box::new(<>)));
+// The array type, potentially with an argument. Take precedence over
+// application: `Array Foo` is always interpreted as the type `Array` parametrized
+// by `Foo`, rather than the dynamic array type `Array Dyn` aliased to `Array` and
+// seen as a contract applied to term `Foo`.
+TypeArray: Types =
+    "Array" <TypeArrayParam?> => {
+        let ty = Box::new(<>.unwrap_or(Types(AbsType::Dyn())));
+        Types(AbsType::Array(ty))
+    };
+
+// Possible parameter for the array type. It's `TypeAtom` augmented with an
+// argument-less `Array`, which allows to parse `Array Array`. We can't add
+// argument-less `Array` to type atoms directly, as it would make `Array Foo`
+// ambiguous: could be parsed both as `Array` as a term applied to `Array` as a
+// term, or as the parametrized type `Array Array`).
+TypeArrayParam: Types = {
+    "Array" => Types(AbsType::Array(Box::new(Types(AbsType::Dyn())))),
+    AsType<Atom>,
+};
 
 RecordOperand: UniTerm = {
     Atom,
@@ -665,6 +680,7 @@ InfixLazyBOpApp<UOp, LExpr, RExpr>: UniTerm =
 InfixExpr: UniTerm = {
     #[precedence(level="0")]
     Applicative,
+    AsUniTerm<TypeArray>,
 
     #[precedence(level="1")]
     "-" <AsTerm<InfixExpr>> =>
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index b8d1b885..aa7c28ff 100644
--- a/src/parser/utils.rs
+++ b/src/parser/utils.rs
@@ -250,7 +250,7 @@ where
         }
     });
 
-    Term::RecRecord(static_map, dynamic_fields, attrs)
+    Term::RecRecord(static_map, dynamic_fields, attrs, None)
 }
 
 /// Merge two fields by performing the merge of both their value and MetaValue if any.
diff --git a/src/repl/query_print.rs b/src/repl/query_print.rs
index eae28abb..3d0c777d 100644
--- a/src/repl/query_print.rs
+++ b/src/repl/query_print.rs
@@ -191,7 +191,7 @@ fn write_query_result_<R: QueryPrinter>(
                 fields.sort();
                 renderer.write_fields(out, fields.into_iter())
             }
-            Term::RecRecord(map, dyn_fields, _) if !map.is_empty() => {
+            Term::RecRecord(map, dyn_fields, ..) if !map.is_empty() => {
                 let mut fields: Vec<_> = map.keys().collect();
                 fields.sort();
                 let dynamic = Ident::from("<dynamic>");
diff --git a/src/repl/rustyline_frontend.rs b/src/repl/rustyline_frontend.rs
index aca23a6f..3901657f 100644
--- a/src/repl/rustyline_frontend.rs
+++ b/src/repl/rustyline_frontend.rs
@@ -56,7 +56,7 @@ pub fn repl(histfile: PathBuf) -> Result<(), InitError> {
                         Term::Record(map, _) => {
                              println!("Loaded {} symbol(s) in the environment.", map.len())
                         }
-                        Term::RecRecord(map, dyn_fields, _) => {
+                        Term::RecRecord(map, dyn_fields, ..) => {
                             if !dyn_fields.is_empty() {
                                 println!("Warning: loading dynamic fields is currently not supported. {} symbols ignored", dyn_fields.len());
                             }
diff --git a/src/term.rs b/src/term.rs
index 5fb9e589..14b3887d 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -24,7 +24,7 @@ use crate::position::TermPos;
 use crate::types::{AbsType, Types, UnboundTypeVariableError};
 use codespan::FileId;
 use serde::{Deserialize, Serialize};
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 use std::ffi::OsString;
 use std::fmt;
 use std::ops::Deref;
@@ -93,6 +93,7 @@ pub enum Term {
         HashMap<Ident, RichTerm>,
         Vec<(RichTerm, RichTerm)>, /* field whose name is defined by interpolation */
         RecordAttrs,
+        Option<RecordDeps>, /* dependency tracking between fields. None before the free var pass */
     ),
     /// A switch construct. The evaluation is done by the corresponding unary operator, but we
     /// still need this one for typechecking.
@@ -165,10 +166,12 @@ impl From<MetaValue> for Term {
 /// Type of let-binding. This only affects run-time behavior. Revertible bindings introduce
 /// revertible thunks at evaluation, which are devices used for the implementation of recursive
 /// records merging. See the [`merge`] and [`eval`] modules for more details.
-#[derive(Debug, Eq, PartialEq, Copy, Clone)]
+#[derive(Debug, Eq, PartialEq, Clone)]
 pub enum BindingType {
     Normal,
-    Revertible,
+    /// In the revertible case, we also store an optional set of dependencies. See
+    /// [`transform::free_vars`] for more details.
+    Revertible(FieldDeps),
 }
 
 impl Default for BindingType {
@@ -190,6 +193,19 @@ impl RecordAttrs {
     }
 }
 
+/// Store field interdependencies in a recursive record. Map each static and dynamic field to the
+/// set of recursive fields that syntactically appears in their definition as free variables.
+#[derive(Debug, Default, Eq, PartialEq, Clone)]
+pub struct RecordDeps {
+    /// Must have exactly the same keys as the static fields map of the recursive record.
+    pub stat_fields: HashMap<Ident, HashSet<Ident>>,
+    /// Must have exactly the same length as the dynamic fields list of the recursive record.
+    pub dyn_fields: Vec<HashSet<Ident>>,
+}
+
+/// Potential dependencies of a single field over the sibling fields in a recursive record.
+pub type FieldDeps = Option<Rc<HashSet<Ident>>>;
+
 #[derive(Debug, Eq, PartialEq, Ord, PartialOrd, Copy, Clone)]
 pub enum MergePriority {
     Default,
@@ -336,7 +352,7 @@ impl Term {
             Record(ref mut static_map, _) => {
                 static_map.iter_mut().for_each(|(_, t)| func(t));
             }
-            RecRecord(ref mut static_map, ref mut dyn_fields, _) => {
+            RecRecord(ref mut static_map, ref mut dyn_fields, ..) => {
                 static_map.iter_mut().for_each(|(_, t)| func(t));
                 dyn_fields.iter_mut().for_each(|(t1, t2)| {
                     func(t1);
@@ -488,14 +504,14 @@ impl Term {
     /// Return a deep string representation of a term, used for printing in the REPL
     pub fn deep_repr(&self) -> String {
         match self {
-            Term::Record(fields, _) | Term::RecRecord(fields, _, _) => {
+            Term::Record(fields, _) | Term::RecRecord(fields, ..) => {
                 let fields_str: Vec<String> = fields
                     .iter()
                     .map(|(ident, term)| format!("{} = {}", ident, term.as_ref().deep_repr()))
                     .collect();
 
                 let suffix = match self {
-                    Term::RecRecord(_, dyn_fields, _) if !dyn_fields.is_empty() => ", ..",
+                    Term::RecRecord(_, dyn_fields, ..) if !dyn_fields.is_empty() => ", ..",
                     _ => "",
                 };
 
@@ -1071,7 +1087,7 @@ impl RichTerm {
                     pos,
                 )
             },
-            Term::RecRecord(map, dyn_fields, attrs) => {
+            Term::RecRecord(map, dyn_fields, attrs, deps) => {
                 // The annotation on `map_res` uses Result's corresponding trait to convert from
                 // Iterator<Result> to a Result<Iterator>
                 let map_res: Result<HashMap<Ident, RichTerm>, E> = map
@@ -1089,7 +1105,7 @@ impl RichTerm {
                     })
                     .collect();
                 RichTerm::new(
-                    Term::RecRecord(map_res?, dyn_fields_res?, attrs),
+                    Term::RecRecord(map_res?, dyn_fields_res?, attrs, deps),
                     pos,
                 )
             },
diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs
new file mode 100644
index 00000000..afc5972d
--- /dev/null
+++ b/src/transform/free_vars.rs
@@ -0,0 +1,231 @@
+//! Annotate recursive record fields with the intersection of the set of their free variables and
+//! the fields of the record. This way, we can track dependencies between recursive fields, which
+//! make it possible in particular to avoid potential memory leaks by providing only references to
+//! the recursive fields that actually appear in the definition of each field when computing the
+//! fixpoint.
+use crate::{
+    destruct::{Destruct, Match},
+    identifier::Ident,
+    term::{RecordDeps, RichTerm, SharedTerm, StrChunk, Term},
+    types::{AbsType, Types},
+};
+
+use std::collections::{HashMap, HashSet};
+
+/// Apply the full free var transformation on a term.
+pub fn transform(rt: &mut RichTerm) {
+    collect_free_vars(rt, &mut HashSet::new())
+}
+
+/// Collect the free variables of a term inside the provided hashset. Doing so, fill the recursive
+/// record dependencies data accordingly.
+fn collect_free_vars(rt: &mut RichTerm, free_vars: &mut HashSet<Ident>) {
+    match SharedTerm::make_mut(&mut rt.term) {
+        Term::Var(id) => {
+            free_vars.insert(id.clone());
+        }
+        Term::ParseError
+        | Term::Null
+        | Term::Bool(_)
+        | Term::Num(_)
+        | Term::Str(_)
+        | Term::Lbl(_)
+        | Term::Sym(_)
+        | Term::Enum(_)
+        | Term::Import(_)
+        | Term::ResolvedImport(_) => (),
+        Term::Fun(id, t) => {
+            let mut fresh = HashSet::new();
+
+            collect_free_vars(t, &mut fresh);
+            fresh.remove(id);
+
+            free_vars.extend(fresh);
+        }
+        Term::FunPattern(id, dest_pat, body) => {
+            let mut fresh = HashSet::new();
+
+            collect_free_vars(body, &mut fresh);
+            bind_pattern(dest_pat, &mut fresh);
+            if let Some(id) = id {
+                fresh.remove(id);
+            }
+
+            free_vars.extend(fresh);
+        }
+        Term::Let(id, t1, t2, _) => {
+            let mut fresh = HashSet::new();
+
+            collect_free_vars(t1, free_vars);
+            collect_free_vars(t2, &mut fresh);
+            fresh.remove(id);
+
+            free_vars.extend(fresh);
+        }
+        Term::LetPattern(id, dest_pat, t1, t2) => {
+            let mut fresh = HashSet::new();
+
+            collect_free_vars(t1, free_vars);
+            collect_free_vars(t2, &mut fresh);
+            bind_pattern(dest_pat, &mut fresh);
+            if let Some(id) = id {
+                fresh.remove(id);
+            }
+
+            free_vars.extend(fresh);
+        }
+        Term::App(t1, t2) => {
+            collect_free_vars(t1, free_vars);
+            collect_free_vars(t2, free_vars);
+        }
+        Term::Switch(t, cases, default) => {
+            collect_free_vars(t, free_vars);
+            for t in cases.values_mut().chain(default.iter_mut()) {
+                collect_free_vars(t, free_vars);
+            }
+        }
+        Term::Op1(_, t) => collect_free_vars(t, free_vars),
+        Term::Op2(_, t1, t2) => {
+            collect_free_vars(t1, free_vars);
+            collect_free_vars(t2, free_vars);
+        }
+        Term::OpN(_, ts) => {
+            for t in ts {
+                collect_free_vars(t, free_vars);
+            }
+        }
+        Term::Wrapped(_, t) => collect_free_vars(t, free_vars),
+        Term::Record(map, _) => {
+            for t in map.values_mut() {
+                collect_free_vars(t, free_vars);
+            }
+        }
+        Term::RecRecord(map, dyn_fields, _, deps) => {
+            let rec_fields: HashSet<Ident> = map.keys().cloned().collect();
+            let mut fresh = HashSet::new();
+            let mut new_deps = RecordDeps {
+                stat_fields: HashMap::with_capacity(map.len()),
+                dyn_fields: Vec::with_capacity(dyn_fields.len()),
+            };
+
+            for (id, t) in map.iter_mut() {
+                fresh.clear();
+
+                collect_free_vars(t, &mut fresh);
+                new_deps
+                    .stat_fields
+                    .insert(id.clone(), &fresh & &rec_fields);
+
+                free_vars.extend(&fresh - &rec_fields);
+            }
+            for (t1, t2) in dyn_fields.iter_mut() {
+                fresh.clear();
+
+                // Currently, the identifier part of a dynamic definition is not recursive, i.e.
+                // one can't write `{foo = "hey", "%{foo}" = 5}`. Hence, we add their free
+                // variables directly in the final set without taking them into account for
+                // recursive dependencies.
+                collect_free_vars(t1, free_vars);
+                collect_free_vars(t2, &mut fresh);
+                new_deps.dyn_fields.push(&fresh & &rec_fields);
+
+                free_vars.extend(&fresh - &rec_fields);
+            }
+
+            // Even if deps were previously filled (it shouldn't), we had to recompute the free
+            // variables anyway for the nodes higher up, because deps alone is not sufficient to
+            // reconstruct the full set of free variables. At this point, we override it in any
+            // case.
+            *deps = Some(new_deps);
+        }
+        Term::Array(ts) => {
+            for t in ts {
+                collect_free_vars(t, free_vars);
+            }
+        }
+        Term::StrChunks(chunks) => {
+            for chunk in chunks {
+                match chunk {
+                    StrChunk::Expr(t, _) => collect_free_vars(t, free_vars),
+                    _ => (),
+                }
+            }
+        }
+        Term::MetaValue(meta) => {
+            for ctr in meta.contracts.iter_mut().chain(meta.types.iter_mut()) {
+                collect_type_free_vars(&mut ctr.types, free_vars)
+            }
+
+            if let Some(ref mut t) = meta.value {
+                collect_free_vars(t, free_vars);
+            }
+        }
+    }
+}
+
+/// Collect the free variables of the potential terms inside a type (custom contracts) and insert
+/// them the provided hashset. Doing so, fill the recursive records dependencies data accordingly.
+fn collect_type_free_vars(ty: &mut Types, set: &mut HashSet<Ident>) {
+    match &mut ty.0 {
+        AbsType::Dyn()
+        | AbsType::Num()
+        | AbsType::Bool()
+        | AbsType::Str()
+        | AbsType::Sym()
+        | AbsType::Var(_)
+        | AbsType::RowEmpty() => (),
+        AbsType::Forall(_, ty)
+        | AbsType::Enum(ty)
+        | AbsType::StaticRecord(ty)
+        | AbsType::DynRecord(ty)
+        | AbsType::Array(ty) => collect_type_free_vars(ty.as_mut(), set),
+        AbsType::Arrow(ty1, ty2) => {
+            collect_type_free_vars(ty1.as_mut(), set);
+            collect_type_free_vars(ty2.as_mut(), set);
+        }
+        AbsType::RowExtend(_, ty_opt, tail) => {
+            if let Some(ref mut ty) = ty_opt {
+                collect_type_free_vars(ty, set);
+            }
+            collect_type_free_vars(tail.as_mut(), set);
+        }
+        AbsType::Flat(ref mut rt) => collect_free_vars(rt, set),
+    }
+}
+
+/// Remove the variables bound by a destructuring pattern from a set of free variables.
+fn bind_pattern(dest_pat: &Destruct, free_vars: &mut HashSet<Ident>) {
+    match dest_pat {
+        Destruct::Record { matches, rest, .. } => {
+            for m in matches {
+                bind_match(m, free_vars);
+            }
+
+            if let Some(rest) = rest {
+                free_vars.remove(rest);
+            }
+        }
+        Destruct::Array { matches, .. } => {
+            for m in matches {
+                bind_match(m, free_vars);
+            }
+        }
+        Destruct::Empty => {}
+    }
+}
+
+/// Remove the variables bound by a match expression (constituents of a destructuring pattern) from
+/// a set of free variables.
+fn bind_match(m: &Match, free_vars: &mut HashSet<Ident>) {
+    match m {
+        Match::Assign(_, _, (id, sub_pat)) => {
+            if let Some(id) = id {
+                free_vars.remove(id);
+            }
+            bind_pattern(sub_pat, free_vars);
+        }
+        Match::Simple(id, _) => {
+            free_vars.remove(id);
+        }
+    }
+}
diff --git a/src/transform/mod.rs b/src/transform/mod.rs
index 3c918888..acbf2895 100644
--- a/src/transform/mod.rs
+++ b/src/transform/mod.rs
@@ -13,6 +13,7 @@ generate_counter!(FreshVarCounter, usize);
 
 pub mod apply_contracts;
 pub mod desugar_destructuring;
+pub mod free_vars;
 pub mod import_resolution;
 pub mod share_normal_form;
 
@@ -22,7 +23,13 @@ pub mod share_normal_form;
 /// Do not perform transformations on the imported files. If needed, either do it yourself using
 /// pending imports returned by [`resolve_imports`](../fn.resolve_imports.html) or use the
 /// [`Cache`](../../cache/struct.Cache.html)
-pub fn transform(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
+pub fn transform(mut rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
+    free_vars::transform(&mut rt);
+    transform_no_free_vars(rt)
+}
+
+/// Same as [`transform`], but doesn't apply the free vars transformation.
+pub fn transform_no_free_vars(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
     let rt = rt.traverse(
         &mut |rt: RichTerm, _| -> Result<RichTerm, UnboundTypeVariableError> {
             // before anything, we have to desugar the syntax
diff --git a/src/transform/share_normal_form.rs b/src/transform/share_normal_form.rs
index d9abc2b1..61bf8784 100644
--- a/src/transform/share_normal_form.rs
+++ b/src/transform/share_normal_form.rs
@@ -28,10 +28,14 @@
 //! Newly introduced variables begin with a special character to avoid clashing with user-defined
 //! variables.
 use super::fresh_var;
-use crate::identifier::Ident;
-use crate::match_sharedterm;
-use crate::position::TermPos;
-use crate::term::{BindingType, RichTerm, Term};
+use crate::{
+    identifier::Ident,
+    match_sharedterm,
+    position::TermPos,
+    term::{BindingType, RichTerm, Term},
+};
+
+use std::{collections::HashSet, rc::Rc};
 
 /// Transform the top-level term of an AST to a share normal form, if it can.
 ///
@@ -54,7 +58,7 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
                         if should_share(&t.term) {
                             let fresh_var = fresh_var();
                             let pos_t = t.pos;
-                            bindings.push((fresh_var.clone(), t));
+                            bindings.push((fresh_var.clone(), t, BindingType::Normal));
                             (id, RichTerm::new(Term::Var(fresh_var), pos_t))
                         } else {
                             (id, t)
@@ -62,9 +66,9 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
                     })
                     .collect();
 
-                with_bindings(Term::Record(map, attrs), bindings, pos, BindingType::Normal)
+                with_bindings(Term::Record(map, attrs), bindings, pos)
             },
-            Term::RecRecord(map, dyn_fields, attrs) => {
+            Term::RecRecord(map, dyn_fields, attrs, deps) => {
                 // When a recursive record is evaluated, all fields need to be turned to closures
                 // anyway (see the corresponding case in `eval::eval()`), which is what the share
                 // normal form transformation does. This is why the test is more lax here than for
@@ -81,6 +85,21 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
                 // marker). See comments inside [`RichTerm::closurize`] for more details.
                 let mut bindings = Vec::with_capacity(map.len());
 
+                fn mk_binding_type(field_deps: Option<HashSet<Ident>>) -> BindingType {
+                    // If the fields has an empty set of dependencies, we can eschew the
+                    // useless introduction of a revertible thunk. Note that if
+                    // `field_deps` being `None` doesn't mean "empty dependencies" but
+                    // rather that the dependencies haven't been computed. In the latter
+                    // case, we must be conservative and assume the field is potentially
+                    // recursive.
+                    let is_non_rec = (&field_deps).as_ref().map(|deps| deps.is_empty()).unwrap_or(false);
+                    if is_non_rec {
+                        BindingType::Normal
+                    } else {
+                        BindingType::Revertible(field_deps.map(Rc::new))
+                    }
+                }
+
                 let map = map
                     .into_iter()
                     .map(|(id, t)| {
@@ -89,7 +108,11 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
                         if !t.as_ref().is_constant() {
                             let fresh_var = fresh_var();
                             let pos_t = t.pos;
-                            bindings.push((fresh_var.clone(), t));
+                            let field_deps = deps.as_ref().and_then(|deps| deps.stat_fields.get(&id)).cloned();
+                            let is_non_rec = (&field_deps).as_ref().map(|deps| deps.is_empty()).unwrap_or(false);
+                            let btype = mk_binding_type(field_deps);
+                            bindings.push((fresh_var.clone(), t, btype));
+
                             (id, RichTerm::new(Term::Var(fresh_var), pos_t))
                         } else {
                             (id, t)
@@ -99,11 +122,14 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
 
                 let dyn_fields = dyn_fields
                     .into_iter()
-                    .map(|(id_t, t)| {
+                    .enumerate()
+                    .map(|(index, (id_t, t))| {
                         if !t.as_ref().is_constant() {
                             let fresh_var = fresh_var();
                             let pos_t = t.pos;
-                            bindings.push((fresh_var.clone(), t));
+                            let field_deps = deps.as_ref().and_then(|deps| deps.dyn_fields.get(index)).cloned();
+                            let btype = mk_binding_type(field_deps);
+                            bindings.push((fresh_var.clone(), t, btype));
                             (id_t, RichTerm::new(Term::Var(fresh_var), pos_t))
                         } else {
                             (id_t, t)
@@ -111,7 +137,7 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
                     })
                     .collect();
 
-                with_bindings(Term::RecRecord(map, dyn_fields, attrs), bindings, pos, BindingType::Revertible)
+                with_bindings(Term::RecRecord(map, dyn_fields, attrs, deps), bindings, pos)
             },
             Term::Array(ts) => {
                 let mut bindings = Vec::with_capacity(ts.len());
@@ -122,7 +148,7 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
                         if should_share(&t.term) {
                             let fresh_var = fresh_var();
                             let pos_t = t.pos;
-                            bindings.push((fresh_var.clone(), t));
+                            bindings.push((fresh_var.clone(), t, BindingType::Normal));
                             RichTerm::new(Term::Var(fresh_var), pos_t)
                         } else {
                             t
@@ -130,7 +156,7 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
                     })
                     .collect();
 
-                with_bindings(Term::Array(ts), bindings, pos, BindingType::Normal)
+                with_bindings(Term::Array(ts), bindings, pos)
             },
             Term::MetaValue(meta) if meta.value.as_ref().map(|t| should_share(&t.term)).unwrap_or(false) => {
                     let mut meta = meta;
@@ -165,20 +191,18 @@ fn should_share(t: &Term) -> bool {
     }
 }
 
-/// Bind a list of pairs `(identifier, term)` in a term.
+/// Bind a list of pairs `(identifier, term, binding_type)` in a term.
 ///
 /// Given the term `body` and bindings of identifiers to terms represented as a list of pairs
 /// `(id_1, term_1), .., (id_n, term_n)`, return the new term `let id_n = term_n in ... let
 /// id_1 = term_1 in body`.
 fn with_bindings(
     body: Term,
-    bindings: Vec<(Ident, RichTerm)>,
+    bindings: Vec<(Ident, RichTerm, BindingType)>,
     pos: TermPos,
-    btype: BindingType,
 ) -> RichTerm {
-    bindings
-        .into_iter()
-        .fold(RichTerm::new(body, pos.into_inherited()), |acc, (id, t)| {
-            RichTerm::new(Term::Let(id, t, acc, btype), pos)
-        })
+    bindings.into_iter().fold(
+        RichTerm::new(body, pos.into_inherited()),
+        |acc, (id, t, btype)| RichTerm::new(Term::Let(id, t, acc, btype), pos),
+    )
 }
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index 1c4fb7c1..fb8ac776 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -492,7 +492,7 @@ fn type_check_<L: Linearizer>(
         }
         // If some fields are defined dynamically, the only potential type that works is `{_ : a}`
         // for some `a`
-        Term::RecRecord(stat_map, dynamic, _) if !dynamic.is_empty() => {
+        Term::RecRecord(stat_map, dynamic, ..) if !dynamic.is_empty() => {
             let ty_dyn = state.table.fresh_unif_var();
 
             for id in stat_map.keys() {
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index 01cef877..127d71be 100644
--- a/src/typecheck/operation.rs
+++ b/src/typecheck/operation.rs
@@ -141,7 +141,7 @@ pub fn get_uop_type(
             //mk_tyw_record!(; TypeWrapper::Ptr(state.table.fresh_var())),
             mk_typewrapper::array(AbsType::Str()),
         ),
-        // Dyn -> Array Dyn
+        // Dyn -> Array
         UnaryOp::ValuesOf() => (
             mk_typewrapper::dynamic(),
             mk_typewrapper::array(AbsType::Dyn()),
diff --git a/src/types.rs b/src/types.rs
index 4bfe1dc0..e20af57f 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -365,7 +365,7 @@ impl Types {
 
         match &self.0 {
             Dyn() | Num() | Bool() | Str() | Var(_) => true,
-            Flat(rt) if matches!(*rt.term, Term::Var(_)) => true,
+            Array(ty) if ty.0 == AbsType::Dyn() => true,
             _ => false,
         }
     }
@@ -378,6 +378,7 @@ impl fmt::Display for Types {
             AbsType::Num() => write!(f, "Num"),
             AbsType::Bool() => write!(f, "Bool"),
             AbsType::Str() => write!(f, "Str"),
+            AbsType::Array(ty) if ty.0 == AbsType::Dyn() => write!(f, "Array"),
             AbsType::Array(ty) => {
                 write!(f, "Array ")?;
 
@@ -482,10 +483,11 @@ mod test {
         assert_format_eq("[|a, b, c, d|]");
         assert_format_eq("forall r. [|tag1, tag2, tag3 ; r|]");
 
+        assert_format_eq("Array");
         assert_format_eq("Array Num");
         assert_format_eq("Array (Array Num)");
         assert_format_eq("Num -> Array (Array Str) -> Num");
         assert_format_eq("Array (Num -> Num)");
-        assert_format_eq("Array (Array (Array Dyn) -> Num)");
+        assert_format_eq("Array (Array Array -> Num)");
     }
 }
diff --git a/stdlib/array.ncl b/stdlib/array.ncl
index 7bb1f8c2..773c16e3 100644
--- a/stdlib/array.ncl
+++ b/stdlib/array.ncl
@@ -209,7 +209,7 @@
         "%m
       = fun pred l => fold (fun x acc => if pred x then true else acc) false l,
 
-    elem : Dyn -> Array Dyn -> Bool
+    elem : Dyn -> Array -> Bool
       | doc m%"
         Results in true if the given element is a member of the array, false otherwise.
 
diff --git a/stdlib/record.ncl b/stdlib/record.ncl
index 1adf436d..64ced7fe 100644
--- a/stdlib/record.ncl
+++ b/stdlib/record.ncl
@@ -26,7 +26,7 @@
       "%m
     = fun r => %fields% r,
 
-    values | { ; Dyn} -> Array Dyn
+    values | { ; Dyn} -> Array
     | doc m%"
       Given a record, results in a array containing all the values in that record.
 
diff --git a/utilities/Cargo.toml b/utilities/Cargo.toml
index da4285db..8fa9dd1f 100644
--- a/utilities/Cargo.toml
+++ b/utilities/Cargo.toml
@@ -11,3 +11,4 @@ bench = false
 [dependencies]
 nickel = {path = "../"}
 criterion = "0.3"
+codespan = "0.11"
diff --git a/utilities/src/lib.rs b/utilities/src/lib.rs
index 492e365d..e4a60952 100644
--- a/utilities/src/lib.rs
+++ b/utilities/src/lib.rs
@@ -1,10 +1,14 @@
 //! Helpers for tests and benches.
+use codespan::Files;
 use criterion::Criterion;
-use nickel::error::Error;
-use nickel::program::Program;
-use nickel::term::Term;
-use std::io::Cursor;
-use std::path::PathBuf;
+use nickel::{
+    error::{Error, ParseError},
+    parser::{grammar, lexer},
+    program::Program,
+    term::{RichTerm, Term},
+};
+
+use std::{io::Cursor, path::PathBuf};
 
 pub fn eval(s: impl std::string::ToString) -> Result<Term, Error> {
     let mut p = Program::new_from_source(Cursor::new(s.to_string()), "test").unwrap();
@@ -18,6 +22,14 @@ pub fn eval_file(f: &str) -> Result<Term, Error> {
     p.eval().map(Term::from)
 }
 
+pub fn parse(s: &str) -> Result<RichTerm, ParseError> {
+    let id = Files::new().add("<test>", String::from(s));
+
+    grammar::TermParser::new()
+        .parse_term(id, lexer::Lexer::new(&s))
+        .map_err(|errs| errs.errors.first().unwrap().clone())
+}
+
 #[derive(Clone, Copy, Eq, PartialEq, Debug)]
 pub enum EvalMode {
     Normal,


Test patch:
diff --git a/src/parser/tests.rs b/src/parser/tests.rs
index bff0f86d..bee46003 100644
--- a/src/parser/tests.rs
+++ b/src/parser/tests.rs
@@ -179,7 +179,8 @@ fn record_terms() {
             .into_iter()
             .collect(),
             Vec::new(),
-            Default::default()
+            Default::default(),
+            None,
         )
         .into()
     );
@@ -198,6 +199,7 @@ fn record_terms() {
                 mk_app!(mk_term::op1(UnaryOp::Ite(), Num(4.)), Num(5.), Num(6.))
             )],
             Default::default(),
+            None,
         )
         .into()
     );
@@ -213,6 +215,7 @@ fn record_terms() {
             .collect(),
             Vec::new(),
             Default::default(),
+            None,
         )
         .into()
     );
diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs
index 82d6e32c..3e89390c 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -138,11 +138,11 @@ fn lists_contracts() {
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
     assert_matches!(
-        eval("1 | Array Dyn"),
+        eval("1 | Array"),
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
     assert_matches!(
-        eval("(fun x => x) | Array Dyn"),
+        eval("(fun x => x) | Array"),
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
 
diff --git a/tests/free_vars.rs b/tests/free_vars.rs
new file mode 100644
index 00000000..6597d428
--- /dev/null
+++ b/tests/free_vars.rs
@@ -0,0 +1,165 @@
+use nickel::{identifier::Ident, term::Term, transform::free_vars};
+
+use std::collections::{HashMap, HashSet};
+use std::iter::IntoIterator;
+
+use utilities::parse;
+
+// fn is_subset_of<'a>(free_vars: impl IntoIterator<Item = &'a Ident>, rec_fields: &Vec<&Ident>) -> bool {
+//    free_vars.into_iter().all(|id| rec_fields.contains(&id))
+// }
+
+fn free_vars_eq(free_vars: &HashSet<Ident>, expected: Vec<&str>) -> bool {
+    let expected_set: HashSet<Ident> = expected.into_iter().map(|s| Ident::from(s)).collect();
+    *free_vars == expected_set
+}
+
+fn stat_free_vars_incl(
+    stat_fields: &HashMap<Ident, HashSet<Ident>>,
+    mut expected: HashMap<&str, Vec<&str>>,
+) -> bool {
+    stat_fields
+        .iter()
+        .all(|(id, set)| free_vars_eq(set, expected.remove(id.as_ref()).unwrap()))
+}
+
+fn dyn_free_vars_incl(dyn_fields: &Vec<HashSet<Ident>>, mut expected: Vec<Vec<&str>>) -> bool {
+    dyn_fields
+        .iter()
+        .enumerate()
+        .all(|(i, set)| free_vars_eq(set, std::mem::take(&mut expected[i])))
+}
+
+fn check_dyn_vars(expr: &str, expected: Vec<Vec<&str>>) -> bool {
+    let mut rt = parse(expr).unwrap();
+    free_vars::transform(&mut rt);
+
+    match rt.term.into_owned() {
+        Term::RecRecord(_, dyns, _, deps) => {
+            let deps = deps.unwrap();
+            dyns.len() == deps.dyn_fields.len() && dyn_free_vars_incl(&deps.dyn_fields, expected)
+        }
+        _ => panic!("{} hasn't been parsed as a record", expr),
+    }
+}
+
+fn check_stat_vars(expr: &str, expected: HashMap<&str, Vec<&str>>) -> bool {
+    let mut rt = parse(expr).unwrap();
+    free_vars::transform(&mut rt);
+
+    match rt.term.into_owned() {
+        Term::RecRecord(map, _, _, deps) => {
+            let deps = deps.unwrap();
+            println!(
+                "-- comparing {:#?} **AND* {:#?}",
+                deps.stat_fields, expected
+            );
+            map.len() == deps.stat_fields.len() && stat_free_vars_incl(&deps.stat_fields, expected)
+        }
+        _ => panic!("{} hasn't been parsed as a record", expr),
+    }
+}
+
+#[test]
+fn static_record() {
+    assert!(check_stat_vars(
+        "{
+          a = b + 1 + h,
+          b = f (a + 1) z,
+          c = if a.r then [b] else {foo = c}
+        }",
+        HashMap::from([
+            ("a", vec!["b"]),
+            ("b", vec!["a"]),
+            ("c", vec!["a", "b", "c"])
+        ])
+    ));
+}
+
+#[test]
+fn dynamic_record() {
+    assert!(check_dyn_vars(
+        "{
+          a = null,
+          b = null,
+          \"%{\"a_dyn\"}\" = b + 1 + h,
+          \"%{\"b_dyn\"}\" = f (a + 1) z,
+          \"%{\"c\"}\" = if a.r then [b] else {foo = c, bar.booz = a_dyn}
+        }",
+        vec![vec!["b"], vec!["a"], vec!["a", "b"]]
+    ));
+}
+
+#[test]
+fn simple_let() {
+    assert!(check_stat_vars(
+        "{
+          a = let b = 0 in b + a + h,
+          b = let a = c in f (a + 1) z,
+          c = let foo = null in let bar = null in if a.r then [b] else {foo = c}
+        }",
+        HashMap::from([
+            ("a", vec!["a"]),
+            ("b", vec!["c"]),
+            ("c", vec!["a", "b", "c"])
+        ])
+    ));
+}
+
+#[test]
+fn destruct_let() {
+    assert!(check_stat_vars(
+        "{
+          a = let {b={foo, bar}} = null in b + a + h,
+          b = let {a, b={c=e@{d}}} = null in f (a + 1 - c) z,
+          c = null
+        }",
+        HashMap::from([("a", vec!["a", "b"]), ("b", vec!["c"]), ("c", vec![]),])
+    ));
+}
+
+#[test]
+fn simple_fun() {
+    assert!(check_stat_vars(
+        "{
+          a = let f = fun a b => a + b + c in f null,
+          b = (fun a => a + (fun b => b + (fun z => c))) a,
+          c = [],
+        }",
+        HashMap::from([("a", vec!["c"]), ("b", vec!["a", "c"]), ("c", vec![]),])
+    ));
+}
+
+#[test]
+fn destruct_fun() {
+    assert!(check_stat_vars(
+        "{
+          a = let f = fun {a=foo} {b=b@{}} => a + b + c in f null,
+          b = (fun {a={b={a}}} => a + (fun {foo={bar=b@{b=e}}} => b + (fun z => b))) c,
+          c = [],
+        }",
+        HashMap::from([("a", vec!["a", "c"]), ("b", vec!["c"]), ("c", vec![]),])
+    ));
+}
+
+#[test]
+fn nested_records() {
+    assert!(check_stat_vars(
+        "{
+          a = {
+            foo = {bar = a},
+            a = 2 + c,
+          },
+          b = {
+            bar = a,
+            baz = {b = b},
+            baz.e = c,
+          },
+          c = {
+            baz.b = b,
+            baz.e = b,
+          },
+        }",
+        HashMap::from([("a", vec!["c"]), ("b", vec!["a", "c"]), ("c", vec!["b"]),])
+    ));
+}
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
index 6c408904..8fcedbe9 100644
--- a/tests/pass/contracts.ncl
+++ b/tests/pass/contracts.ncl
@@ -98,7 +98,7 @@ let Assert = fun l x => x || %blame% l in
   ({a = 0, b = 0, c = 0} | Contract) == {a = 0, b = 0, c = 0},
 
   // arrays 
-  ([1, "2", false] | Array Dyn) == [1, "2", false],
+  ([1, "2", false] | Array) == [1, "2", false],
   ([1, 2, 3] | Array Num) == [1, 2, 3],
   (["1", "2", "false"] | Array Str) == ["1", "2", "false"],
 
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index e339b523..19c9fb88 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -102,7 +102,7 @@ let typecheck = [
   // arrays_simple
   [1, "2", false],
   //TODO: the type system may accept the following test at some point.
-  //([1, "2", false] : Array Dyn),
+  //([1, "2", false] : Array),
   ["a", "b", "c"] : Array Str,
   [1, 2, 3] : Array Num,
   (fun x => [x]) : forall a. a -> Array a,
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index ba076801..99f3b1fc 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -29,7 +29,6 @@ macro_rules! assert_typecheck_fails {
 
 #[test]
 fn unbound_variable_always_throws() {
-    type_check_expr("x").map_err(|err| println!("{:#?}", err));
     assert_matches!(
         type_check_expr("x"),
         Err(TypecheckError::UnboundIdentifier(..))
@@ -136,7 +135,7 @@ fn dynamic_record_simple() {
 #[test]
 fn simple_array() {
     assert_typecheck_fails!("[1, 2, false] : Array Num");
-    assert_typecheck_fails!("[(1 : Str), true, \"b\"] : Array Dyn");
+    assert_typecheck_fails!("[(1 : Str), true, \"b\"] : Array");
     assert_typecheck_fails!("[1, 2, \"3\"] : Array Str");
 }
 
@@ -144,7 +143,7 @@ fn simple_array() {
 fn arrays_operations() {
     assert_typecheck_fails!("(fun l => %head% l) : forall a b. (Array a -> b)");
     assert_typecheck_fails!(
-        "(fun f l => %elem_at% (%map% l f) 0) : forall a. (forall b. (a -> b) -> Array Dyn -> b)"
+        "(fun f l => %elem_at% (%map% l f) 0) : forall a. (forall b. (a -> b) -> Array -> b)"
     );
 }