Repository: tweag/nickel
Pull request #1092 (2023-02-01 17:04:20)

Rename stdlib functions


Patch:
diff --git a/benches/arrays/fold.ncl b/benches/arrays/fold.ncl
index ddc13b03..2c75ae8d 100644
--- a/benches/arrays/fold.ncl
+++ b/benches/arrays/fold.ncl
@@ -6,29 +6,29 @@ let letter | Num -> string.CharLiteral = fun n =>
   right = {
     strings = {
       run = fun n =>
-        array.fold (fun x acc => acc ++ x) "" (array.generate (fun n => letter n) n)
+        array.fold_right (fun x acc => acc ++ x) "" (array.generate (fun n => letter n) n)
     },
     nums = {
       run = fun n =>
-        array.fold (fun x acc => x*acc + (x - acc)) 0 (array.generate (fun n => n/2) n)
+        array.fold_right (fun x acc => x*acc + (x - acc)) 0 (array.generate (fun n => n/2) n)
     },
     arrays = {
       run = fun n =>
-        array.fold (fun x acc => acc @ [x]) [] (array.generate (fun n => [n]) n)
+        array.fold_right (fun x acc => acc @ [x]) [] (array.generate (fun n => [n]) n)
     },
   },
   left = {
     strings = {
       run = fun n =>
-        array.foldl (fun acc x => acc ++ x) "" (array.generate (fun n => letter n) n)
+        array.fold_left (fun acc x => acc ++ x) "" (array.generate (fun n => letter n) n)
     },
     nums = {
       run = fun n =>
-        array.foldl (fun acc x => x*acc + (x - acc)) 0 (array.generate (fun n => n/2) n)
+        array.fold_left (fun acc x => x*acc + (x - acc)) 0 (array.generate (fun n => n/2) n)
     },
     arrays = {
       run = fun n =>
-        array.foldl (fun acc x => acc @ [x]) [] (array.generate (fun n => [n]) n)
+        array.fold_left (fun acc x => acc @ [x]) [] (array.generate (fun n => [n]) n)
     },
   }
 }
diff --git a/benches/arrays/sum.ncl b/benches/arrays/sum.ncl
index 55b2397b..018fb0b3 100644
--- a/benches/arrays/sum.ncl
+++ b/benches/arrays/sum.ncl
@@ -2,7 +2,7 @@ let rec sum
   | Array Num -> Num 
   = fun xs =>
     if array.length xs == 0 then 0
-    else array.head xs + sum (array.tail xs)
+    else array.first xs + sum (array.drop_first xs)
 in {
   run = fun n => array.generate (fun x => x + 1) n |> sum
 }
diff --git a/benches/functions/church.ncl b/benches/functions/church.ncl
index c3a986d6..c1615654 100644
--- a/benches/functions/church.ncl
+++ b/benches/functions/church.ncl
@@ -21,12 +21,12 @@
       |> array.map encode
       |> array.map (fun nChurch =>
         add (mult (encode 3) nChurch) (encode 5))
-      |> array.fold add (encode 0) in
+      |> array.fold_right add (encode 0) in
 
     let decoded =
       base
       |> array.map (fun n => 3*n + 5)
-      |> array.foldl (fun acc n => acc + n) 0 in
+      |> array.fold_left (fun acc n => acc + n) 0 in
 
     decode encoded == decoded,
 }
diff --git a/benches/mantis/lib.ncl b/benches/mantis/lib.ncl
index 8fb7e516..165fbba9 100644
--- a/benches/mantis/lib.ncl
+++ b/benches/mantis/lib.ncl
@@ -1,6 +1,6 @@
 {
   contracts = {
-    AllOf = fun contracts label value => array.fold (fun c acc => c label
+    AllOf = fun contracts label value => array.fold_right (fun c acc => c label
       acc) contracts value,
     Dummy = fun label value => value,
     OneOf = fun values => contract.from_predicate (fun value => array.elem value
@@ -22,7 +22,7 @@
           contract.blame_with "no match" label
       else contract.blame_with "not a string" label,
     PseudoOr = fun alts label value =>
-      array.fold (fun ctr rest =>
+      array.fold_right (fun ctr rest =>
         if ctr.pred value then
           ctr.contract value
         else
diff --git a/benches/nixpkgs/lists.ncl b/benches/nixpkgs/lists.ncl
index 96a0a13d..176eb0f2 100644
--- a/benches/nixpkgs/lists.ncl
+++ b/benches/nixpkgs/lists.ncl
@@ -46,7 +46,7 @@
     let rec fold_ = fun n =>
         if n == len
         then nul
-        else op (array.elem_at n list) (fold_ (n + 1))
+        else op (array.at n list) (fold_ (n + 1))
     in fold_ 0,
 
   fold: forall a b. (a -> b -> b) -> b -> (Array a) -> b
@@ -74,7 +74,7 @@
     let rec foldl_ = fun n =>
         if n == -1
         then nul
-        else op (foldl_ (n - 1)) (array.elem_at n list)
+        else op (foldl_ (n - 1)) (array.at n list)
     in foldl_ (array.length list - 1),
 
   foldl_: forall a b. (b -> a -> b) -> b -> (Array a) -> b
@@ -85,7 +85,7 @@
      with small whole results (in contrast with lazily-generated list or large
      lists where only a part is consumed.)
   "%
-  = fun op nul list => array.foldl op nul list,
+  = fun op nul list => array.fold_left op nul list,
 
   imap0: forall a b. (Num -> a -> b) -> (Array a) -> (Array b)
   | doc m%%"
@@ -95,7 +95,7 @@
        imap0 (fun i v => "%{v}-%{%to_string% i}") ["a", "b"]
        >> [ "a-0", "b-1" ]
   "%%
-  = fun f list => array.generate (fun n => f n (array.elem_at n list)) (array.length list),
+  = fun f list => array.generate (fun n => f n (array.at n list)) (array.length list),
 
   imap1: forall a b. (Num -> a -> b) -> (Array a) -> (Array b)
   | doc m%%"
@@ -105,7 +105,7 @@
        imap1 (fun i v => "%{v}-%{toString i}") ["a", "b"]
        >> [ "a-1", "b-2" ]
   "%%
-  = fun f list => array.generate (fun n => f (n + 1) (array.elem_at n list)) (array.length list),
+  = fun f list => array.generate (fun n => f (n + 1) (array.at n list)) (array.length list),
 
   concatMap: forall a b. (a -> (Array b)) -> (Array a) -> (Array b)
   | doc m%"
@@ -171,7 +171,7 @@
        let len = array.length found in
        if len == 0 then def
        else if len != 1 then multiple
-       else array.head found,
+       else array.first found,
 
   findFirst: forall a. (a -> Bool) -> a -> Array a -> a
   | doc m%"
@@ -192,7 +192,7 @@
     # Input list
     list
     => let found = array.filter pred list in
-       if found == [] then def else array.head found,
+       if found == [] then def else array.first found,
 
   any: forall a. (a -> Bool) -> Array a -> Bool
   | doc m%"
@@ -367,7 +367,7 @@
     fst
     # Second list
     snd
-    => array.generate (fun n => f (array.elem_at n fst) (array.elem_at n snd)) (num.min (array.length fst) (array.length snd)),
+    => array.generate (fun n => f (array.at n fst) (array.at n snd)) (num.min (array.length fst) (array.length snd)),
 
   zipLists: forall a b. Array a -> Array b -> Array { fst: a, snd: b}
   | doc m%"
@@ -390,7 +390,7 @@
   "%
   = fun xs =>
     let l = array.length xs in
-    array.generate (fun n => array.elem_at (l - n - 1) xs) l,
+    array.generate (fun n => array.at (l - n - 1) xs) l,
 
   #TODO: is there a way to type statically?
   listDfs |  forall a. Bool -> (a -> a -> Bool) -> Array a -> {visited: Array a, rest: Array a ; Dyn}
@@ -424,11 +424,11 @@
         then # nothing is before us
           { minimal = us, visited = visited_, rest = rest_ }
         else # grab the first one before us and continue
-          (dfs_ (array.head b.right)
+          (dfs_ (array.first b.right)
                 ([ us ] @ visited_)
-                (array.tail b.right @ b.wrong)
+                (array.drop_first b.right @ b.wrong)
     ) in
-    dfs_ (array.head list) [] (array.tail list),
+    dfs_ (array.first list) [] (array.drop_first list),
 
   toposort: forall a. (a -> a -> Bool) -> Array a -> {_: Array Dyn}
   | doc m%"
@@ -484,9 +484,9 @@
   "%
   = fun strictLess list =>
     let len = array.length list in
-    let first = array.head list in
+    let first = array.first list in
     let rec pivot_ = (fun n acc@{ left=left_, right=right_ } =>
-      let el = array.elem_at n list in
+      let el = array.at n list in
       let next = pivot_ (n + 1) in
       if n == len
       then acc
@@ -519,9 +519,9 @@
          else -1
     else if b == []
          then 1
-         else let rel = cmp (array.head a) (array.head b) in
+         else let rel = cmp (array.first a) (array.first b) in
               if rel == 0
-              then compareLists cmp (array.tail a) (array.tail b)
+              then compareLists cmp (array.drop_first a) (array.drop_first b)
               else rel,
 
 # naturalSort: Array Str -> Array Str
@@ -539,11 +539,11 @@
 # "%
 # # TODO: broken. how to implement it in nickel?
 # = fun lst =>
-#   let vectorise = fun s => array.map (fun x => if builtin.is_array x then (array.head x) | Num else x | Num) (string.split "(0|[1-9][0-9]*)" s) | Array Dyn
+#   let vectorise = fun s => array.map (fun x => if builtin.is_array x then (array.first x) | Num else x | Num) (string.split "(0|[1-9][0-9]*)" s) | Array Dyn
 #   in
 #     let prepared = array.map (fun x => [ (vectorise x), x ]) lst in # remember vectorised version for O(n) regex splits
-#     let less = fun a b => (compareLists compare (array.head a) (array.head b)) < 0 in
-#     array.map (fun x => array.elem_at 1 x) (sort less prepared),
+#     let less = fun a b => (compareLists compare (array.first a) (array.first b)) < 0 in
+#     array.map (fun x => array.at 1 x) (sort less prepared),
 
   take: forall a. Num -> Array a -> Array a
   | doc m%"
@@ -598,7 +598,7 @@
     lst =>
     let len = array.length lst in
     array.generate
-      (fun n => array.elem_at (n + start) lst)
+      (fun n => array.at (n + start) lst)
       (if start >= len then 0
        else if start + count > len then len - start
        else count),
@@ -616,7 +616,7 @@
   "%
   = fun lst =>
     #assert lib.assertMsg (lst != []) "lists.last: list must not be empty!",
-    array.elem_at (array.length lst - 1) lst,
+    array.at (array.length lst - 1) lst,
 
   init: forall a. Array a -> Array a
   | doc m%"
diff --git a/benches/numeric/reduce.ncl b/benches/numeric/reduce.ncl
index 082b05a4..9e60ae7f 100644
--- a/benches/numeric/reduce.ncl
+++ b/benches/numeric/reduce.ncl
@@ -2,12 +2,12 @@
   sum = {
     run = fun n =>
       let numbers = array.generate function.id n in
-      array.foldl (fun acc x => acc + x) 0 numbers
+      array.fold_left (fun acc x => acc + x) 0 numbers
   },
 
   product = {
     run = fun n =>
       let numbers = array.generate function.id n in
-      array.foldl (fun acc x => acc * x) 1 numbers
+      array.fold_left (fun acc x => acc * x) 1 numbers
   },
 }
diff --git a/benches/numeric/scalar.ncl b/benches/numeric/scalar.ncl
index 9cf27bb2..76ed0bca 100644
--- a/benches/numeric/scalar.ncl
+++ b/benches/numeric/scalar.ncl
@@ -3,12 +3,12 @@
     if l1 == [] || l2 == [] then
       []
     else
-      [f (array.head l1) (array.head l2)]
-      @ map2 f (array.tail l1) (array.tail l2),
+      [f (array.first l1) (array.first l2)]
+      @ map2 f (array.drop_first l1) (array.drop_first l2),
 
   run = fun n =>
     let left = array.generate function.id n in
     let right = array.generate (fun n => n*n/2) n in
     let prod = map2 (fun x y => x * y) left right in
-    array.foldl (fun x y => x + y) 0 prod
+    array.fold_left (fun x y => x + y) 0 prod
 }
diff --git a/benches/records/countLetters.ncl b/benches/records/countLetters.ncl
index 86833106..4b4eb020 100644
--- a/benches/records/countLetters.ncl
+++ b/benches/records/countLetters.ncl
@@ -5,5 +5,5 @@
         record.update char (dict."%{char}" + 1) dict
       else
         record.insert "%{char}" 1 dict in
-    array.foldl update_dict {} (string.chars s)
+    array.fold_left update_dict {} (string.chars s)
 }
diff --git a/benches/records/merge.ncl b/benches/records/merge.ncl
index c77f61c3..0714b360 100644
--- a/benches/records/merge.ncl
+++ b/benches/records/merge.ncl
@@ -2,7 +2,7 @@
   run = fun n m =>
     let prefix = fun n =>
       array.generate (fun _n => "a") n
-      |> array.foldl (fun x y => x ++ y) "" in
+      |> array.fold_left (fun x y => x ++ y) "" in
     let make_rec_step = fun state k =>
       let name = state.prev_name ++ (string.from_num k) in
       {
@@ -12,8 +12,8 @@
     let top_array = array.generate function.id m in
     let make_rec = fun m =>
       let l = array.generate function.id n in
-      let result = array.foldl make_rec_step {value = {}, prev_name = prefix m} l in
+      let result = array.fold_left make_rec_step {value = {}, prev_name = prefix m} l in
       result.value in
     array.map make_rec top_array
-    |> array.foldl (fun r1 r2 => r1 & r2) {}
+    |> array.fold_left (fun r1 r2 => r1 & r2) {}
 }
diff --git a/doc/manual/contracts.md b/doc/manual/contracts.md
index 162e72ff..a710293d 100644
--- a/doc/manual/contracts.md
+++ b/doc/manual/contracts.md
@@ -582,7 +582,7 @@ let NumBoolDict = fun label value =>
   if builtin.is_record value then
     let check_fields = value
       |> record.fields
-      |> array.foldl (fun acc field_name =>
+      |> array.fold_left (fun acc field_name =>
         if string.is_match "^\\d+$" field_name then
           acc # unused and always null through iteration
         else
diff --git a/doc/manual/correctness.md b/doc/manual/correctness.md
index 619cab4c..e2e3c10d 100644
--- a/doc/manual/correctness.md
+++ b/doc/manual/correctness.md
@@ -142,7 +142,7 @@ first wrapping it in an array:
 # lib.ncl
 {
   split = fun pairs =>
-    array.fold (fun pair acc =>
+    array.fold_right (fun pair acc =>
       {
         # problem: the right expression to use is [pair.key]
         keys = acc.keys @ pair.key,
diff --git a/doc/manual/syntax.md b/doc/manual/syntax.md
index 59afc56c..4994e78b 100644
--- a/doc/manual/syntax.md
+++ b/doc/manual/syntax.md
@@ -439,7 +439,7 @@ Examples:
     increment 41
 42
 
-> let flatten = array.fold (@) [] in flatten [[1, 2], [3], [4, 5]]
+> let flatten = array.fold_right (@) [] in flatten [[1, 2], [3], [4, 5]]
 [ 1, 2, 3, 4, 5 ]
 ```
 
@@ -455,12 +455,12 @@ Examples:
 
 > "Hello World"
   |> string.split " "
-  |> array.head
+  |> array.first
 "Hello"
 
 > "Hello World"
   |> string.split " "
-  |> array.head
+  |> array.first
   |> string.uppercase
 "HELLO"
 ```
diff --git a/doc/manual/typing.md b/doc/manual/typing.md
index 0b080d35..ad472a03 100644
--- a/doc/manual/typing.md
+++ b/doc/manual/typing.md
@@ -63,7 +63,7 @@ are using functions. Say we want to filter over an array of elements:
 
 ```nickel
 let filter = fun pred l =>
-  array.foldl (fun acc x => if pred x then acc @ [x] else acc) [] l in
+  array.fold_left (fun acc x => if pred x then acc @ [x] else acc) [] l in
 filter (fun x => if x % 2 == 0 then x else null) [1,2,3,4,5,6]
 ```
 
@@ -73,7 +73,7 @@ Result:
 error: Type error
   ┌─ repl-input-11:2:32
   │
-2 │   array.foldl (fun acc x => if pred x then acc @ [x] else acc) [] l in
+2 │   array.fold_left (fun acc x => if pred x then acc @ [x] else acc) [] l in
   │                                ^^^^^^ This expression has type Num, but Bool was expected
 3 │ filter (fun x => if x % 2 == 0 then x else null) [1,2,3,4,5,6]
   │                                                             - evaluated to this
@@ -123,7 +123,7 @@ a type annotation at the top-level:
 
 ```nickel
 (let filter = fun pred l =>
-     array.foldl (fun acc x => if pred x then acc @ [x] else acc) [] l in
+     array.fold_left (fun acc x => if pred x then acc @ [x] else acc) [] l in
 filter (fun x => if x % 2 == 0 then x else null) [1,2,3,4,5,6]) : Array Num
 ```
 
diff --git a/examples/arrays/README.md b/examples/arrays/README.md
index 66f66b6d..bd52611e 100644
--- a/examples/arrays/README.md
+++ b/examples/arrays/README.md
@@ -2,7 +2,7 @@
 
 This example shows how to write generic, statically typed functions in Nickel.
 The code is illustrative: in practice, you should use the array stdlib functions
-`array.map` and `array.fold` instead of redefining your own.
+`array.map` and `array.fold_right` instead of redefining your own.
 
 ## Run
 
diff --git a/examples/arrays/arrays.ncl b/examples/arrays/arrays.ncl
index 3fd5d5c0..3ee919f3 100644
--- a/examples/arrays/arrays.ncl
+++ b/examples/arrays/arrays.ncl
@@ -1,14 +1,14 @@
 # test: pass
 
 # Example array functions. This code is illustrative: prefer using the array 
-# stdlib functions `array.map` and `array.fold` instead.
+# stdlib functions `array.map` and `array.fold_right` instead.
 let my_array_lib = {
   map : forall a b. (a -> b) -> Array a -> Array b = fun f arr =>
     if arr == [] then
       []
     else
-      let head = array.head arr in
-      let tail = array.tail arr in
+      let head = array.first arr in
+      let tail = array.drop_first arr in
       [f head] @ map f tail,
 
   fold : forall a b. (a -> b -> b) -> Array a -> b -> b =
@@ -16,8 +16,8 @@ let my_array_lib = {
         if arr == [] then
           first
         else
-          let head = array.head arr in
-          let tail = array.tail arr in
+          let head = array.first arr in
+          let tail = array.drop_first arr in
           f head (fold f tail first),
 } in
 # Compute `7!`
diff --git a/flake.lock b/flake.lock
index 38d1eacb..d9b5e444 100644
--- a/flake.lock
+++ b/flake.lock
@@ -10,11 +10,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1677370089,
-        "narHash": "sha256-sdZ3ull2bldQYXK7tsX097C8JEuhBGIFPSfmA5nVoXE=",
+        "lastModified": 1677892403,
+        "narHash": "sha256-/Wi0L1spSWLFj+UQxN3j0mPYMoc7ZoAujpUF/juFVII=",
         "owner": "ipetkov",
         "repo": "crane",
-        "rev": "685e7494b02c6ac505482b1a471de4c285e87543",
+        "rev": "105e27adb70a9890986b6d543a67761cbc1964a2",
         "type": "github"
       },
       "original": {
@@ -108,11 +108,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1677342105,
-        "narHash": "sha256-kv1fpkfCJGb0M+LZaCHFUuIS9kRIwyVgupHu86Y28nc=",
+        "lastModified": 1677932085,
+        "narHash": "sha256-+AB4dYllWig8iO6vAiGGYl0NEgmMgGHpy9gzWJ3322g=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "b1f87ca164a9684404c8829b851c3586c4d9f089",
+        "rev": "3c5319ad3aa51551182ac82ea17ab1c6b0f0df89",
         "type": "github"
       },
       "original": {
@@ -150,11 +150,11 @@
         "nixpkgs-stable": "nixpkgs-stable"
       },
       "locked": {
-        "lastModified": 1677160285,
-        "narHash": "sha256-tBzpCjMP+P3Y3nKLYvdBkXBg3KvTMo3gvi8tLQaqXVY=",
+        "lastModified": 1677832802,
+        "narHash": "sha256-XQf+k6mBYTiQUjWRf/0fozy5InAs03O1b30adCpWeXs=",
         "owner": "cachix",
         "repo": "pre-commit-hooks.nix",
-        "rev": "2bd861ab81469428d9c823ef72c4bb08372dd2c4",
+        "rev": "382bee738397ca005206eefa36922cc10df8a21c",
         "type": "github"
       },
       "original": {
@@ -184,11 +184,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1676437770,
-        "narHash": "sha256-mhJye91Bn0jJIE7NnEywGty/U5qdELfsT8S+FBjTdG4=",
+        "lastModified": 1677812689,
+        "narHash": "sha256-EakqhgRnjVeYJv5+BJx/NZ7/eFTMBxc4AhICUNquhUg=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "a619538647bd03e3ee1d7b947f7c11ff289b376e",
+        "rev": "e53e8853aa7b0688bc270e9e6a681d22e01cf299",
         "type": "github"
       },
       "original": {
@@ -207,11 +207,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1677292251,
-        "narHash": "sha256-D+6q5Z2MQn3UFJtqsM5/AvVHi3NXKZTIMZt1JGq/spA=",
+        "lastModified": 1677896940,
+        "narHash": "sha256-F4YW6/+35dwctY4Ogb/vvMfvA6O0UwhDbXE7urDhk4A=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "34cdbf6ad480ce13a6a526f57d8b9e609f3d65dc",
+        "rev": "c25d3e1951863ac0061d47a3fabf9aa7c91db5e5",
         "type": "github"
       },
       "original": {
diff --git a/lsp/nls/src/linearization/completed.rs b/lsp/nls/src/linearization/completed.rs
index 3ec039bb..e61b28d3 100644
--- a/lsp/nls/src/linearization/completed.rs
+++ b/lsp/nls/src/linearization/completed.rs
@@ -168,9 +168,7 @@ impl Completed {
             if let Some(doc) = doc {
                 extra.push(doc.to_owned());
             }
-            if let Some(types) = &annotation.types {
-                extra.push(types.label.tag.to_string());
-            }
+
             if let Some(contracts) = annotation.contracts_to_string() {
                 extra.push(contracts);
             }
diff --git a/lsp/nls/src/linearization/mod.rs b/lsp/nls/src/linearization/mod.rs
index 7330c106..4a921eed 100644
--- a/lsp/nls/src/linearization/mod.rs
+++ b/lsp/nls/src/linearization/mod.rs
@@ -562,9 +562,9 @@ impl<'a> Linearizer for AnalysisHost<'a> {
                 id_mapping.insert(*id, index);
             });
 
-        fn transform_wildcard(wildcars: &[Types], t: Types) -> Types {
-            match t {
-                Types(TypeF::Wildcard(i)) => wildcars.get(i).unwrap_or(&t).clone(),
+        fn transform_wildcard(wildcards: &[Types], t: Types) -> Types {
+            match t.types {
+                TypeF::Wildcard(i) => wildcards.get(i).unwrap_or(&t).clone(),
                 _ => t,
             }
         }
diff --git a/lsp/nls/src/requests/completion.rs b/lsp/nls/src/requests/completion.rs
index 4aab7d6d..bcbe5e33 100644
--- a/lsp/nls/src/requests/completion.rs
+++ b/lsp/nls/src/requests/completion.rs
@@ -47,7 +47,7 @@ impl From<Ident> for IdentWithType {
     fn from(ident: Ident) -> Self {
         IdentWithType {
             ident,
-            ty: Types(TypeF::Dyn),
+            ty: Types::from(TypeF::Dyn),
             meta: None,
         }
     }
@@ -57,7 +57,7 @@ impl From<&str> for IdentWithType {
     fn from(ident: &str) -> Self {
         IdentWithType {
             ident: Ident::from(ident),
-            ty: Types(TypeF::Dyn),
+            ty: Types::from(TypeF::Dyn),
             meta: None,
         }
     }
@@ -246,13 +246,13 @@ fn find_fields_from_type(
     path: &mut Vec<Ident>,
     info @ ComplCtx { .. }: &'_ ComplCtx<'_>,
 ) -> Vec<IdentWithType> {
-    match ty {
-        Types(TypeF::Record(row)) => find_fields_from_rrows(row, path, info),
-        Types(TypeF::Dict(ty)) => match path.pop() {
+    match &ty.types {
+        TypeF::Record(row) => find_fields_from_rrows(row, path, info),
+        TypeF::Dict(ty) => match path.pop() {
             Some(..) => find_fields_from_type(ty, path, info),
             _ => Vec::new(),
         },
-        Types(TypeF::Flat(term)) => find_fields_from_term(term, path, info),
+        TypeF::Flat(term) => find_fields_from_term(term, path, info),
         _ => Vec::new(),
     }
 }
@@ -270,10 +270,14 @@ fn find_fields_from_rrows(
         });
 
         match type_of_current {
-            Some(Types(TypeF::Record(rrows_current))) => {
-                find_fields_from_rrows(&rrows_current, path, info)
-            }
-            Some(Types(TypeF::Flat(term))) => find_fields_from_term(&term, path, info),
+            Some(Types {
+                types: TypeF::Record(rrows_current),
+                ..
+            }) => find_fields_from_rrows(&rrows_current, path, info),
+            Some(Types {
+                types: TypeF::Flat(term),
+                ..
+            }) => find_fields_from_term(&term, path, info),
             _ => Vec::new(),
         }
     } else {
@@ -331,7 +335,7 @@ fn find_fields_from_term(
                     ident: *ident,
                     // This Dyn type is only displayed if the metadata's
                     // contract or type annotation is not present.
-                    ty: Types(TypeF::Dyn),
+                    ty: Types::from(TypeF::Dyn),
                     meta: Some(field.metadata.clone()),
                 })
                 .collect(),
@@ -449,9 +453,9 @@ fn collect_record_info(
         .get_item(id, lin_cache)
         .map(|item| {
             let (ty, _) = linearization.resolve_item_type_meta(item, lin_cache);
-            match (&item.kind, ty) {
+            match (&item.kind, &ty.types) {
                 // Get record fields from static type info
-                (_, Types(TypeF::Record(rrows))) => find_fields_from_rrows(&rrows, path, &info),
+                (_, TypeF::Record(rrows)) => find_fields_from_rrows(rrows, path, &info),
                 (
                     TermKind::Declaration {
                         value: ValueState::Known(body_id),
@@ -726,7 +730,7 @@ mod tests {
             env: Environment::new(),
             id,
             pos: TermPos::None,
-            ty: Types(TypeF::Dyn),
+            ty: Types::from(TypeF::Dyn),
             kind,
             metadata,
         }
diff --git a/src/destructuring.rs b/src/destructuring.rs
index b5dc8735..a5cf280a 100644
--- a/src/destructuring.rs
+++ b/src/destructuring.rs
@@ -4,7 +4,7 @@
 use crate::{
     identifier::Ident,
     label::Label,
-    position::RawSpan,
+    position::{RawSpan, TermPos},
     term::{
         record::{Field, RecordAttrs, RecordData},
         LabeledType, Term,
@@ -66,16 +66,19 @@ impl RecordPattern {
 
     fn into_contract_with_lbl(self, label: Label) -> LabeledType {
         let is_open = self.is_open();
-
+        let pos = TermPos::Original(self.span);
         LabeledType {
-            types: Types(TypeF::Flat(
-                Term::Record(RecordData::new(
-                    self.inner().into_iter().map(Match::as_binding).collect(),
-                    RecordAttrs { open: is_open },
-                    None,
-                ))
-                .into(),
-            )),
+            types: Types {
+                types: TypeF::Flat(
+                    Term::Record(RecordData::new(
+                        self.inner().into_iter().map(Match::as_binding).collect(),
+                        RecordAttrs { open: is_open },
+                        None,
+                    ))
+                    .into(),
+                ),
+                pos,
+            },
             label,
         }
     }
diff --git a/src/error.rs b/src/error.rs
index f6dc9b93..3dc4b8f1 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -2,8 +2,6 @@
 //!
 //! Define error types for different phases of the execution, together with functions to generate a
 //! [codespan](https://crates.io/crates/codespan-reporting) diagnostic from them.
-use std::fmt::Write;
-
 use codespan::{FileId, Files};
 use codespan_reporting::diagnostic::{Diagnostic, Label, LabelStyle};
 use lalrpop_util::ErrorRecovery;
@@ -28,8 +26,6 @@ use crate::{
     types::{TypeF, Types},
 };
 
-use self::blame_error::ExtendWithCallStack;
-
 /// A general error occurring during either parsing or evaluation.
 #[derive(Debug, Clone, PartialEq)]
 pub enum Error {
@@ -306,11 +302,11 @@ impl IntoDiagnostics<FileId> for ParseErrors {
     fn into_diagnostics(
         self,
         files: &mut Files<String>,
-        contract_id: Option<FileId>,
+        stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Diagnostic<FileId>> {
         self.errors
             .into_iter()
-            .flat_map(|e| e.into_diagnostics(files, contract_id))
+            .flat_map(|e| e.into_diagnostics(files, stdlib_ids))
             .collect()
     }
 }
@@ -612,7 +608,7 @@ pub trait IntoDiagnostics<FileId> {
     ///
     /// - `files`: to know why it takes a mutable reference to `Files<String>`, see
     ///   `label_alt`.
-    /// - `contract_id` is required to format the callstack when reporting blame errors. For some
+    /// - `stdlib_ids` is required to format the callstack when reporting blame errors. For some
     ///   errors (such as [`ParseError`])), contracts may not have been loaded yet, hence the
     ///   optional. See also [`crate::eval::callstack::CallStack::group_by_calls`].
     ///
@@ -625,7 +621,7 @@ pub trait IntoDiagnostics<FileId> {
     fn into_diagnostics(
         self,
         files: &mut Files<String>,
-        contract_id: Option<FileId>,
+        stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Diagnostic<FileId>>;
 }
 
@@ -749,20 +745,20 @@ impl IntoDiagnostics<FileId> for Error {
     fn into_diagnostics(
         self,
         files: &mut Files<String>,
-        contract_id: Option<FileId>,
+        stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Diagnostic<FileId>> {
         match self {
             Error::ParseErrors(errs) => errs
                 .errors
                 .into_iter()
-                .flat_map(|e| e.into_diagnostics(files, contract_id))
+                .flat_map(|e| e.into_diagnostics(files, stdlib_ids))
                 .collect(),
-            Error::TypecheckError(err) => err.into_diagnostics(files, contract_id),
-            Error::EvalError(err) => err.into_diagnostics(files, contract_id),
-            Error::ImportError(err) => err.into_diagnostics(files, contract_id),
-            Error::SerializationError(err) => err.into_diagnostics(files, contract_id),
-            Error::IOError(err) => err.into_diagnostics(files, contract_id),
-            Error::ReplError(err) => err.into_diagnostics(files, contract_id),
+            Error::TypecheckError(err) => err.into_diagnostics(files, stdlib_ids),
+            Error::EvalError(err) => err.into_diagnostics(files, stdlib_ids),
+            Error::ImportError(err) => err.into_diagnostics(files, stdlib_ids),
+            Error::SerializationError(err) => err.into_diagnostics(files, stdlib_ids),
+            Error::IOError(err) => err.into_diagnostics(files, stdlib_ids),
+            Error::ReplError(err) => err.into_diagnostics(files, stdlib_ids),
         }
     }
 }
@@ -771,46 +767,21 @@ impl IntoDiagnostics<FileId> for EvalError {
     fn into_diagnostics(
         self,
         files: &mut Files<String>,
-        contract_id: Option<FileId>,
+        stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Diagnostic<FileId>> {
         match self {
             EvalError::BlameError {
                 evaluated_arg,
                 label,
                 call_stack,
-            } => {
-                let mut msg = String::new();
-
-                write!(&mut msg, "{}", blame_error::title(&label))
-                    .expect("writing formatted data into a string should not raise an error");
-
-                if !label.tag.is_empty() {
-                    write!(&mut msg, ": {}", &escape(&label.tag)).unwrap();
-                }
-
-                let (path_label, notes) = blame_error::report_ty_path(&label, files);
-                let labels = blame_error::build_diagnostic_labels(
-                    evaluated_arg,
-                    &label,
-                    path_label,
-                    files,
-                    contract_id,
-                );
-
-                let mut diagnostics = vec![Diagnostic::error()
-                    .with_message(msg)
-                    .with_labels(labels)
-                    .with_notes(notes)];
-
-                diagnostics.push(blame_error::note(&label));
-
-                if ty_path::has_no_dom(&label.path) {
-                } else if let Some(id) = contract_id {
-                    diagnostics.extend_with_call_stack(id, &call_stack);
-                }
-
-                diagnostics
-            }
+            } => blame_error::blame_diagnostics(
+                files,
+                stdlib_ids,
+                label,
+                evaluated_arg,
+                &call_stack,
+                "",
+            ),
             EvalError::MissingFieldDef {
                 id,
                 metadata,
@@ -844,7 +815,7 @@ impl IntoDiagnostics<FileId> for EvalError {
                     .first()
                     .map(|labeled_ty| labeled_ty.label.clone())
                 {
-                    diags.push(blame_error::note(&label));
+                    diags.push(blame_error::contract_bind_loc(&label));
                 }
 
                 diags
@@ -873,7 +844,7 @@ impl IntoDiagnostics<FileId> for EvalError {
                     .with_labels(labels)
                     .with_notes(vec![msg])]
             }
-            EvalError::ParseError(parse_error) => parse_error.into_diagnostics(files, contract_id),
+            EvalError::ParseError(parse_error) => parse_error.into_diagnostics(files, stdlib_ids),
             EvalError::NotAFunc(t, arg, pos_opt) => vec![Diagnostic::error()
                 .with_message("not a function")
                 .with_labels(vec![
@@ -987,7 +958,7 @@ impl IntoDiagnostics<FileId> for EvalError {
                     .with_labels(labels)
                     .with_notes(vec![String::from(INTERNAL_ERROR_MSG)])]
             }
-            EvalError::SerializationError(err) => err.into_diagnostics(files, contract_id),
+            EvalError::SerializationError(err) => err.into_diagnostics(files, stdlib_ids),
             EvalError::DeserializationError(format, msg, span_opt) => {
                 let labels = span_opt
                     .as_opt_ref()
@@ -1024,41 +995,17 @@ impl IntoDiagnostics<FileId> for EvalError {
             }
             EvalError::IllegalPolymorphicTailAccess {
                 action,
-                label: l,
+                label: contract_label,
                 evaluated_arg,
                 call_stack,
-            } => {
-                let mut msg = String::new();
-
-                write!(&mut msg, "{}", blame_error::title(&l)).unwrap();
-                write!(&mut msg, " - {}", action.message()).unwrap();
-                if !l.tag.is_empty() {
-                    write!(&mut msg, ": {}", &escape(&l.tag)).unwrap();
-                }
-
-                let (path_label, notes) = blame_error::report_ty_path(&l, files);
-                let labels = blame_error::build_diagnostic_labels(
-                    evaluated_arg,
-                    &l,
-                    path_label,
-                    files,
-                    contract_id,
-                );
-
-                let mut diagnostics = vec![Diagnostic::error()
-                    .with_message(msg)
-                    .with_labels(labels)
-                    .with_notes(notes)];
-
-                diagnostics.push(blame_error::note(&l));
-
-                if ty_path::has_no_dom(&l.path) {
-                } else if let Some(id) = contract_id {
-                    diagnostics.extend_with_call_stack(id, &call_stack);
-                }
-
-                diagnostics
-            }
+            } => blame_error::blame_diagnostics(
+                files,
+                stdlib_ids,
+                contract_label,
+                evaluated_arg,
+                &call_stack,
+                &format!("- {}", &action.message()),
+            ),
         }
     }
 }
@@ -1101,7 +1048,7 @@ mod blame_error {
         blame_label: &label::Label,
         path_label: Label<FileId>,
         files: &mut Files<String>,
-        contract_id: Option<FileId>,
+        stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Label<FileId>> {
         let mut labels = vec![path_label];
 
@@ -1111,8 +1058,9 @@ mod blame_error {
             // point to the builtin implementation contract like `func` or `record`, so
             // there's no good reason to show it. Note than even in that case, the
             // information contained at the argument index can still be useful.
-            if contract_id
-                .map(|ctrs_id| arg_pos.src_id != ctrs_id)
+            if stdlib_ids
+                .as_ref()
+                .map(|ctrs_id| !ctrs_id.contains(&arg_pos.src_id))
                 .unwrap_or(true)
             {
                 labels.push(primary(arg_pos).with_message("applied to this expression"));
@@ -1126,11 +1074,11 @@ mod blame_error {
             match (
                 evaluated_arg.pos,
                 blame_label.arg_pos.as_opt_ref(),
-                contract_id,
+                stdlib_ids,
             ) {
                 // Avoid showing a position inside builtin contracts, it's rarely
                 // informative.
-                (TermPos::Original(val_pos), _, Some(c_id)) if val_pos.src_id == c_id => {
+                (TermPos::Original(val_pos), _, Some(c_id)) if c_id.contains(&val_pos.src_id) => {
                     evaluated_arg.pos = TermPos::None;
                     labels.push(
                         secondary_term(&evaluated_arg, files)
@@ -1155,8 +1103,16 @@ mod blame_error {
                 }
                 // Finally, if the parameter reduced to a value which originates from a
                 // different expression, show both the expression and the value.
-                (TermPos::Inherited(ref val_pos), ..) => {
-                    labels.push(secondary(val_pos).with_message("evaluated to this expression"));
+                (TermPos::Inherited(ref val_pos), _, ids) => {
+                    if ids
+                        .as_ref()
+                        .map(|cids| !cids.contains(&val_pos.src_id))
+                        .unwrap_or(true)
+                    {
+                        labels
+                            .push(secondary(val_pos).with_message("evaluated to this expression"));
+                    }
+
                     evaluated_arg.pos = TermPos::None;
                     labels.push(
                         secondary_term(&evaluated_arg, files)
@@ -1173,12 +1129,12 @@ mod blame_error {
     }
 
     pub trait ExtendWithCallStack {
-        fn extend_with_call_stack(&mut self, contract_id: FileId, call_stack: &CallStack);
+        fn extend_with_call_stack(&mut self, stdlib_ids: &[FileId], call_stack: &CallStack);
     }
 
     impl ExtendWithCallStack for Vec<Diagnostic<FileId>> {
-        fn extend_with_call_stack(&mut self, contract_id: FileId, call_stack: &CallStack) {
-            let (calls, curr_call) = call_stack.group_by_calls(contract_id);
+        fn extend_with_call_stack(&mut self, stdlib_ids: &[FileId], call_stack: &CallStack) {
+            let (calls, curr_call) = call_stack.group_by_calls(stdlib_ids);
             let diag_curr_call = curr_call.map(|cdescr| {
                 let name = cdescr
                     .head
@@ -1328,20 +1284,119 @@ is None but last_arrow_elem is Some"),
     }
 
     /// Return a note diagnostic showing where a contract was bound.
-    pub fn note(l: &label::Label) -> Diagnostic<FileId> {
+    pub fn contract_bind_loc(l: &label::Label) -> Diagnostic<FileId> {
         Diagnostic::note().with_labels(vec![Label::primary(
             l.span.src_id,
             l.span.start.to_usize()..l.span.end.to_usize(),
         )
         .with_message("bound here")])
     }
+
+    /// Generate codespan diagnostics from blame data. Mostly used by `into_diagnostics`
+    /// implementations.
+    ///
+    /// # Parameters
+    ///
+    /// The `msg_addendum` is used to customize the main error message. It's inserted between the
+    /// leading "contract broken by .." and the custom contract diagnostic message in tail
+    /// position.
+    pub fn blame_diagnostics(
+        files: &mut Files<String>,
+        stdlib_ids: Option<&Vec<FileId>>,
+        mut label: label::Label,
+        evaluated_arg: Option<RichTerm>,
+        call_stack: &CallStack,
+        msg_addendum: &str,
+    ) -> Vec<Diagnostic<FileId>> {
+        use std::fmt::Write;
+
+        let mut diagnostics = Vec::new();
+
+        // Contract diagnostics are stacked up in order, which means the last one is
+        // usually the latest/most precise/most relevant. We ignore empty diagnostics and
+        // iterate in reverse order, to show the most relevant diagnostics first.
+        let mut contract_diagnostics = std::mem::take(&mut label.diagnostics)
+            .into_iter()
+            .rev()
+            .filter(|diag| !label::ContractDiagnostic::is_empty(diag));
+        let head_contract_diagnostic = contract_diagnostics.next();
+
+        let mut msg = format!("{}{msg_addendum}", title(&label));
+
+        if let Some(contract_msg) = head_contract_diagnostic
+            .as_ref()
+            .and_then(|diag| diag.message.as_ref())
+        {
+            write!(&mut msg, ": {}", &super::escape(contract_msg)).unwrap();
+        }
+
+        let contract_notes = head_contract_diagnostic
+            .map(|diag| diag.notes)
+            .unwrap_or_default();
+        let (path_label, notes_higher_order) = report_ty_path(&label, files);
+
+        let labels = build_diagnostic_labels(evaluated_arg, &label, path_label, files, stdlib_ids);
+
+        // If there are notes in the head contract diagnostic, we build the first
+        // diagnostic using them and will put potential generated notes on higher-order
+        // contracts in a following diagnostic.
+        if !contract_notes.is_empty() {
+            diagnostics.push(
+                Diagnostic::error()
+                    .with_message(msg)
+                    .with_labels(labels)
+                    .with_notes(contract_notes),
+            );
+
+            if !notes_higher_order.is_empty() {
+                diagnostics.push(
+                    Diagnostic::note()
+                        .with_message("due to a function contract violation")
+                        .with_notes(notes_higher_order),
+                );
+            }
+        } else {
+            diagnostics.push(
+                Diagnostic::error()
+                    .with_message(msg)
+                    .with_labels(labels)
+                    .with_notes(notes_higher_order),
+            );
+        }
+
+        diagnostics.push(contract_bind_loc(&label));
+
+        for ctr_diag in contract_diagnostics {
+            let mut msg = String::from("from a parent contract violation");
+
+            if let Some(msg_contract) = ctr_diag.message {
+                msg.push_str(": ");
+                msg.push_str(&super::escape(&msg_contract));
+            }
+
+            diagnostics.push(
+                Diagnostic::note()
+                    .with_message(msg)
+                    .with_notes(ctr_diag.notes),
+            );
+        }
+
+        match stdlib_ids {
+            Some(id) if !ty_path::has_no_dom(&label.path) => {
+                diagnostics.extend_with_call_stack(id, call_stack)
+            }
+            _ => (),
+        };
+
+        diagnostics
+    }
 }
 
 impl IntoDiagnostics<FileId> for ParseError {
     fn into_diagnostics(
         self,
         files: &mut Files<String>,
-        _contract_id: Option<FileId>,
+        _stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Diagnostic<FileId>> {
         let diagnostic = match self {
             ParseError::UnexpectedEOF(file_id, _expected) => {
@@ -1431,7 +1486,7 @@ impl IntoDiagnostics<FileId> for TypecheckError {
     fn into_diagnostics(
         self,
         files: &mut Files<String>,
-        contract_id: Option<FileId>,
+        stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Diagnostic<FileId>> {
         fn mk_expr_label(span_opt: &TermPos) -> Vec<Label<FileId>> {
             span_opt
@@ -1445,7 +1500,7 @@ impl IntoDiagnostics<FileId> for TypecheckError {
             // Use the same diagnostic as `EvalError::UnboundIdentifier` for consistency.
                 {
                     EvalError::UnboundIdentifier(ident, pos_opt)
-                        .into_diagnostics(files, contract_id)
+                        .into_diagnostics(files, stdlib_ids)
                 }
             TypecheckError::MissingRow(ident, expd, actual, span_opt) =>
                 vec![Diagnostic::error()
@@ -1495,13 +1550,13 @@ impl IntoDiagnostics<FileId> for TypecheckError {
             ,
             TypecheckError::TypeMismatch(expd, actual, span_opt) => {
                 fn addendum(ty: &Types) -> &str {
-                    if ty.0.is_flat() {
+                    if ty.types.is_flat() {
                         " (a contract)"
                     } else {
                         ""
                     }
                 }
-                let last_note = if expd.0.is_flat() ^ actual.0.is_flat() {
+                let last_note = if expd.types.is_flat() ^ actual.types.is_flat() {
                     "Static types and contracts are not compatible"
                 } else {
                     "These types are not compatible"
@@ -1554,7 +1609,7 @@ impl IntoDiagnostics<FileId> for TypecheckError {
                 let row_msg = |word, field, ty| format!("The type of the expression was {word} to have the row `{field}: {ty}`");
                 let default_msg = |word, ty| format!("The type of the expression was {word} to be `{ty}`");
 
-                let note1 = if let TypeF::Record(rrows) = &expd.0 {
+                let note1 = if let TypeF::Record(rrows) = &expd.types {
                     match rrows.row_find_path(path.as_slice()) {
                         Some(ty) => row_msg("expected", &field, ty),
                         None => default_msg("expected", &expd),
@@ -1563,7 +1618,7 @@ impl IntoDiagnostics<FileId> for TypecheckError {
                     default_msg("expected", &expd)
                 };
 
-                let note2 = if let TypeF::Record(rrows) = &actual.0 {
+                let note2 = if let TypeF::Record(rrows) = &actual.types {
                     match rrows.row_find_path(path.as_slice()) {
                         Some(ty) => row_msg("inferred", &field, ty),
                         None => default_msg("inferred", &expd),
@@ -1585,7 +1640,7 @@ impl IntoDiagnostics<FileId> for TypecheckError {
                 // We generate a diagnostic for the underlying error, but append a prefix to the
                 // error message to make it clear that this is not a separated error but a more
                 // precise description of why the unification of a row failed.
-                diags.extend((*err).into_diagnostics(files, contract_id).into_iter()
+                diags.extend((*err).into_diagnostics(files, stdlib_ids).into_iter()
                     .map(|mut diag| {
                         diag.message = format!("While typing field `{}`: {}", field, diag.message);
                         diag
@@ -1639,7 +1694,7 @@ impl IntoDiagnostics<FileId> for TypecheckError {
                     // information, so we just ignore it.
                     TypecheckError::TypeMismatch(_, _, _) => (),
                     err => {
-                        diags.extend(err.into_diagnostics(files, contract_id).into_iter()
+                        diags.extend(err.into_diagnostics(files, stdlib_ids).into_iter()
                             .map(|mut diag| {
                                 diag.message = format!("While matching function types: {}", diag.message);
                                 diag
@@ -1674,7 +1729,7 @@ impl IntoDiagnostics<FileId> for ImportError {
     fn into_diagnostics(
         self,
         files: &mut Files<String>,
-        contract_id: Option<FileId>,
+        stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Diagnostic<FileId>> {
         match self {
             ImportError::IOError(path, error, span_opt) => {
@@ -1691,7 +1746,7 @@ impl IntoDiagnostics<FileId> for ImportError {
                 let mut diagnostic: Vec<Diagnostic<FileId>> = error
                     .errors
                     .into_iter()
-                    .flat_map(|e| e.into_diagnostics(files, contract_id))
+                    .flat_map(|e| e.into_diagnostics(files, stdlib_ids))
                     .collect();
 
                 if let Some(span) = span_opt.as_opt_ref() {
@@ -1710,7 +1765,7 @@ impl IntoDiagnostics<FileId> for SerializationError {
     fn into_diagnostics(
         self,
         files: &mut Files<String>,
-        _contract_id: Option<FileId>,
+        _stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Diagnostic<FileId>> {
         match self {
             SerializationError::NotAString(rt) => vec![Diagnostic::error()
@@ -1738,7 +1793,7 @@ impl IntoDiagnostics<FileId> for IOError {
     fn into_diagnostics(
         self,
         _files: &mut Files<String>,
-        _contract_id: Option<FileId>,
+        _stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Diagnostic<FileId>> {
         match self {
             IOError(msg) => vec![Diagnostic::error().with_message(msg)],
@@ -1750,7 +1805,7 @@ impl IntoDiagnostics<FileId> for ReplError {
     fn into_diagnostics(
         self,
         files: &mut Files<String>,
-        contract_id: Option<FileId>,
+        stdlib_ids: Option<&Vec<FileId>>,
     ) -> Vec<Diagnostic<FileId>> {
         match self {
             ReplError::UnknownCommand(s) => vec![Diagnostic::error()
@@ -1758,7 +1813,7 @@ impl IntoDiagnostics<FileId> for ReplError {
                 .with_notes(vec![String::from(
                     "type `:?` or `:help` for a list of available commands.",
                 )])],
-            ReplError::InvalidQueryPath(err) => err.into_diagnostics(files, contract_id),
+            ReplError::InvalidQueryPath(err) => err.into_diagnostics(files, stdlib_ids),
             ReplError::MissingArg { cmd, msg_opt } => {
                 let mut notes = msg_opt
                     .as_ref()
diff --git a/src/eval/callstack.rs b/src/eval/callstack.rs
index ed98561a..1327e15d 100644
--- a/src/eval/callstack.rs
+++ b/src/eval/callstack.rs
@@ -130,11 +130,11 @@ impl CallStack {
     ///
     /// # Arguments
     ///
-    /// - `contract_id`: the `FileId` of the source containing standard contracts, to filter their
+    /// - `stdlib_ids`: the `FileId`s of the sources containing standard contracts, to filter their
     ///   calls out.
     pub fn group_by_calls(
         self: &CallStack,
-        contract_id: FileId,
+        stdlib_ids: &[FileId],
     ) -> (Vec<CallDescr>, Option<CallDescr>) {
         // We filter out calls and accesses made from within the builtin contracts, as well as
         // generated variables introduced by program transformations.
@@ -149,7 +149,7 @@ impl CallStack {
             // We avoid applications (Fun/App) with inherited positions. Such calls include
             // contracts applications which add confusing call items whose positions don't point to
             // an actual call in the source.
-                if *src_id != contract_id =>
+                if !stdlib_ids.contains(src_id) =>
             {
                 true
             }
diff --git a/src/eval/merge.rs b/src/eval/merge.rs
index e6b8d3c2..3a60680b 100644
--- a/src/eval/merge.rs
+++ b/src/eval/merge.rs
@@ -246,7 +246,15 @@ pub fn merge<C: Cache>(
                     let fields: Vec<String> =
                         left.keys().map(|field| format!("`{field}`")).collect();
                     let plural = if fields.len() == 1 { "" } else { "s" };
-                    lbl.tag = format!("extra field{} {}", plural, fields.join(","));
+                    let fields_list = fields.join(",");
+
+                    lbl.set_diagnostic_message(format!("extra field{plural} {fields_list}"));
+                    lbl.set_diagnostic_notes(vec![
+                        format!("Have you misspelled a field?"),
+                        String::from("The record contract might also be too strict. By default, record contracts exclude any field which is not listed.
+Append `, ..` at the end of the record contract, as in `{some_field | SomeContract, ..}`, to make it accept extra fields."),
+                    ]);
+
                     return Err(EvalError::BlameError {
                         evaluated_arg: lbl.get_evaluated_arg(cache),
                         label: lbl,
diff --git a/src/eval/operation.rs b/src/eval/operation.rs
index 2d5ec0ba..1752c5c9 100644
--- a/src/eval/operation.rs
+++ b/src/eval/operation.rs
@@ -1692,11 +1692,12 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
             }
             BinaryOp::Tag() => match_sharedterm! {t1, with {
                     Term::Str(s) => match_sharedterm!{t2, with {
-                                Term::Lbl(l) => {
-                                    let mut l = l;
-                                    l.tag = s;
+                                Term::Lbl(label) => {
+                                    let mut label = label;
+                                    label.set_diagnostic_message(s);
+
                                     Ok(Closure::atomic_closure(RichTerm::new(
-                                        Term::Lbl(l),
+                                        Term::Lbl(label),
                                         pos_op_inh,
                                     )))
                                 }
diff --git a/src/label.rs b/src/label.rs
index 3a19795e..5c1d501e 100644
--- a/src/label.rs
+++ b/src/label.rs
@@ -138,7 +138,7 @@ pub mod ty_path {
         // peek() returns a reference, and hence keeps a mutable borrow of `path_it` which forbids
         // to call to next() in the same region. This is why we need to split the match in two
         // different blocks.
-        let forall_offset = match (&ty.0, path_it.peek()) {
+        let forall_offset = match (&ty.types, path_it.peek()) {
             (_, None) => {
                 let repr = format!("{ty}");
                 return PathSpan {
@@ -151,7 +151,7 @@ pub mod ty_path {
             (TypeF::Forall { .. }, Some(_)) => {
                 // The length of "forall" plus the final separating dot and whitespace ". "
                 let mut result = 8;
-                while let TypeF::Forall { var, body, .. } = &ty.0 {
+                while let TypeF::Forall { var, body, .. } = &ty.types {
                     // The length of the identifier plus the preceding whitespace
                     result += var.to_string().len() + 1;
                     ty = body.as_ref();
@@ -162,7 +162,7 @@ pub mod ty_path {
             _ => 0,
         };
 
-        match (&ty.0, path_it.next()) {
+        match (&ty.types, path_it.next()) {
             (TypeF::Arrow(dom, codom), Some(next)) => {
                 // The potential shift of the start position of the domain introduced by the couple
                 // of parentheses around the domain. Parentheses are added when printing a function
@@ -170,7 +170,7 @@ pub mod ty_path {
                 // For example, `Arrow(Arrow(Num, Num), Num)` is rendered as "(Num -> Num) -> Num".
                 // In this case, the position of the sub-type "Num -> Num" starts at 1 instead of
                 // 0.
-                let paren_offset = match dom.0 {
+                let paren_offset = match dom.types {
                     TypeF::Arrow(_, _) => 1,
                     _ => 0,
                 };
@@ -248,10 +248,10 @@ pub mod ty_path {
                     "span: current type path element indicates to go to field `{}`,\
 but this field doesn't exist in {}",
                     ident,
-                    Types(TypeF::Record(rows.clone()))
+                    Types::from(TypeF::Record(rows.clone())),
                 )
             }
-            (TypeF::Array(ty), Some(Elem::Array)) if *ty.as_ref() == Types(TypeF::Dyn) =>
+            (TypeF::Array(ty), Some(Elem::Array)) if ty.as_ref().types == TypeF::Dyn =>
             // Dyn shouldn't be the target of any blame
             {
                 panic!("span(): unexpected blame of a dyn contract inside an array")
@@ -318,7 +318,7 @@ but this field doesn't exist in {}",
 /// are types with arrows in it. Consider the simplest example:
 ///
 /// ```text
-/// Assume(Num -> Num, f)
+/// f | Num -> Num
 /// ```
 ///
 /// This does not entail that `f` returns a `Num` in *every* situation. The identity function `id
@@ -329,9 +329,9 @@ but this field doesn't exist in {}",
 /// checked, which is not the responsibility of `f`, but the caller's (or context)
 /// one.
 ///
-/// `Assume(Num -> Num, f)` should thus be evaluated as `Assume(Num, fun arg
-/// => f (Assume(Num, arg)))`, but we want to report the failures of the two introduced
-/// subcontracts in a different way:
+/// `f | Num -> Num` should thus be evaluated as `fun arg => ((f (arg | Num)) | Num)`, but we want
+/// to report the failures of the two introduced subcontracts in a different way:
+///
 ///  - The inner one (on the argument) says that `f` has been misused: it has been applied to
 ///  something that is not a `Num`.
 ///  - The outer one says that `f` failed to satisfy its contract, as it has been provided with a
@@ -347,8 +347,12 @@ but this field doesn't exist in {}",
 pub struct Label {
     /// The type checked by the original contract.
     pub types: Rc<Types>,
-    /// A string tag to be printed together with the error message.
-    pub tag: String,
+    /// Custom diagnostics set by user code. There might be several diagnostics stacked up, as some
+    /// contracts might in turn apply other subcontracts.
+    ///
+    /// The last diagnostic of the stack is usually the current working diagnostic (the one mutated
+    /// by corresponding primops), and the latest/most precise when a blame error is raised.
+    pub diagnostics: Vec<ContractDiagnostic>,
     /// The position of the original contract.
     pub span: RawSpan,
     /// The index corresponding to the value being checked. Set at run-time by the interpreter.
@@ -362,43 +366,127 @@ pub struct Label {
     pub path: ty_path::Path,
 }
 
+/// Custom reporting diagnostic that can be set by user-code through the `label` API. Used to
+/// customize contract error messages, and provide more context than "a contract has failed".
+#[derive(Debug, Clone, PartialEq, Default)]
+pub struct ContractDiagnostic {
+    /// The main error message tag to be printed together with the error message.
+    pub message: Option<String>,
+    /// Additional notes printed at the end of the message.
+    pub notes: Vec<String>,
+}
+
+impl ContractDiagnostic {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    /// Attach a message to this diagnostic, and return the updated value. Erase potential previous
+    /// message.
+    pub fn with_message(mut self, message: impl Into<String>) -> Self {
+        self.message = Some(message.into());
+        self
+    }
+
+    /// Attach notes to this diagnostic, and return the updated value. Erase potential previous
+    /// notes.
+    pub fn with_notes(mut self, notes: Vec<String>) -> Self {
+        self.notes = notes;
+        self
+    }
+
+    /// Append a note to this diagnostic.
+    pub fn append_note(&mut self, note: impl Into<String>) {
+        self.notes.push(note.into());
+    }
+
+    /// Return `true` if this diagnostic is empty, that is if `message` is either not set (`None`)
+    /// or is set but empty, AND notes are empty.
+    pub fn is_empty(&self) -> bool {
+        self.message.as_ref().map(String::is_empty).unwrap_or(true) && self.notes.is_empty()
+    }
+}
+
 impl Label {
     /// Generate a dummy label for testing purpose.
     pub fn dummy() -> Label {
         Label {
-            types: Rc::new(Types(TypeF::Num)),
-            tag: "testing".to_string(),
+            types: Rc::new(Types::from(TypeF::Num)),
+            diagnostics: vec![ContractDiagnostic::new().with_message(String::from("testing"))],
             span: RawSpan {
                 src_id: Files::new().add("<test>", String::from("empty")),
                 start: 0.into(),
                 end: 1.into(),
             },
-            arg_idx: None,
-            arg_pos: TermPos::None,
             polarity: true,
-            path: Vec::new(),
+            ..Default::default()
         }
     }
 
     pub fn get_evaluated_arg<EC: EvalCache>(&self, cache: &EC) -> Option<RichTerm> {
         self.arg_idx.clone().map(|idx| cache.get(idx).body)
     }
+
+    /// Set the message of the current diagnostic (the last diagnostic of the stack). Potentially
+    /// erase the previous value.
+    ///
+    /// If the diagnostic stack is empty, this methods pushes a new diagnostic with the given notes.
+    pub fn set_diagnostic_message(&mut self, message: impl Into<String>) {
+        if let Some(current) = self.diagnostics.last_mut() {
+            current.message = Some(message.into());
+        } else {
+            self.diagnostics
+                .push(ContractDiagnostic::new().with_message(message));
+        }
+    }
+
+    /// Set the notes of the current diagnostic (the last diagnostic of the stack). Potentially
+    /// erase the previous value.
+    ///
+    /// If the diagnostic stack is empty, this methods pushes a new diagnostic with the given notes.
+    pub fn set_diagnostic_notes(&mut self, notes: Vec<String>) {
+        if let Some(current) = self.diagnostics.last_mut() {
+            current.notes = notes;
+        } else {
+            self.diagnostics
+                .push(ContractDiagnostic::new().with_notes(notes));
+        }
+    }
+
+    /// Append a note to the current diagnostic (the last diagnostic of the stack). Potentially
+    /// erase the previous value.
+    ///
+    /// If the diagnostic stack is empty, this methods pushes a new diagnostic with the given note.
+    pub fn append_diagnostic_note(&mut self, note: impl Into<String>) {
+        if let Some(current) = self.diagnostics.last_mut() {
+            current.append_note(note);
+        } else {
+            self.diagnostics
+                .push(ContractDiagnostic::new().with_notes(vec![note.into()]));
+        }
+    }
+
+    /// Return a reference to the current contract diagnostic, that is the last one of the stack,
+    /// if any.
+    pub fn current_diagnostic(&self) -> Option<&ContractDiagnostic> {
+        self.diagnostics.last()
+    }
 }
 
 impl Default for Label {
     fn default() -> Label {
         Label {
-            types: Rc::new(Types(TypeF::Dyn)),
-            tag: "".to_string(),
+            types: Rc::new(Types::from(TypeF::Dyn)),
             span: RawSpan {
                 src_id: Files::new().add("<null>", String::from("")),
                 start: 0.into(),
                 end: 1.into(),
             },
-            arg_idx: None,
-            arg_pos: TermPos::None,
             polarity: true,
-            path: Vec::new(),
+            diagnostics: Default::default(),
+            arg_idx: Default::default(),
+            arg_pos: Default::default(),
+            path: Default::default(),
         }
     }
 }
diff --git a/src/parser/grammar.lalrpop b/src/parser/grammar.lalrpop
index 87c9d207..6f1dbed0 100644
--- a/src/parser/grammar.lalrpop
+++ b/src/parser/grammar.lalrpop
@@ -259,7 +259,7 @@ Forall: Types =
             // The variable kind will be determined during the `fix_type_vars`
             // phase. For now, we put a random one (which is also the default
             // one, for unused type variables)
-            |acc, var| Types(TypeF::Forall { var, var_kind: VarKind::Type, body: Box::new(acc) })
+            |acc, var| Types::from(TypeF::Forall { var, var_kind: VarKind::Type, body: Box::new(acc) })
         )
     };
 
@@ -298,8 +298,11 @@ Applicative: UniTerm = {
 };
 
 // The parametrized array type.
-TypeArray: Types = "Array" <AsType<RecordOperand>> =>
-    Types(TypeF::Array(Box::new(<>)));
+TypeArray: Types = "Array" <t: AsType<RecordOperand>> =>
+    // For some reason, we have to bind the type into a `t`
+    // rather than using the usual `<>` placeholder, otherwise,
+    // it doens't compile.
+    Types::from(TypeF::Array(Box::new(t)));
 
 RecordOperand: UniTerm = {
     Atom,
@@ -367,7 +370,7 @@ Atom: UniTerm = {
 
         UniTerm::from(Term::Array(terms, Default::default()))
     },
-    AsUniTerm<TypeAtom>,
+    AsUniTerm<WithPos<TypeAtom>>,
 };
 
 // A record field definition. The is the only place where we don't fix the type
@@ -822,7 +825,7 @@ InfixExpr: UniTerm = {
 
     #[precedence(level="11")] #[assoc(side="right")]
     <s: AsType<InfixExpr>> "->" <t: AsType<InfixExpr>> =>
-        UniTerm::from(Types(TypeF::Arrow(Box::new(s), Box::new(t)))),
+        UniTerm::from(Types::from(TypeF::Arrow(Box::new(s), Box::new(t)))),
 }
 
 BOpPre: BinaryOp = {
@@ -863,10 +866,10 @@ NOpPre<ArgRule>: UniTerm = {
 }
 
 TypeBuiltin: Types = {
-    "Dyn" => Types(TypeF::Dyn),
-    "Num" => Types(TypeF::Num),
-    "Bool" => Types(TypeF::Bool),
-    "Str" => Types(TypeF::Str),
+     "Dyn" => Types::from(TypeF::Dyn),
+     "Num" => Types::from(TypeF::Num),
+     "Bool" => Types::from(TypeF::Bool),
+     "Str" => Types::from(TypeF::Str),
 }
 
 TypeAtom: Types = {
@@ -888,13 +891,15 @@ TypeAtom: Types = {
                 ),
                 |erows, row| EnumRows(EnumRowsF::Extend { row, tail: Box::new(erows) })
             );
-        Types(TypeF::Enum(ty))
+ 	    Types::from(TypeF::Enum(ty))
+    },
+    "{" "_" ":" <t: WithPos<Types>> "}" => {
+        Types::from(TypeF::Dict(Box::new(t)))
     },
-    "{" "_" ":" <Types> "}" => Types(TypeF::Dict(Box::new(<>))),
     "_" => {
         let id = *next_wildcard_id;
-        *next_wildcard_id += 1;
-        Types(TypeF::Wildcard(id))
+        *next_wildcard_id += 1;        
+        Types::from(TypeF::Wildcard(id))
     },
 }
 
diff --git a/src/parser/uniterm.rs b/src/parser/uniterm.rs
index 1ced757c..1a4f0739 100644
--- a/src/parser/uniterm.rs
+++ b/src/parser/uniterm.rs
@@ -79,10 +79,16 @@ impl TryFrom<UniTerm> for Types {
 
     fn try_from(ut: UniTerm) -> Result<Self, ParseError> {
         match ut.node {
-            UniTermNode::Var(id) => Ok(Types(TypeF::Var(id))),
+            UniTermNode::Var(id) => Ok(Types {
+                types: TypeF::Var(id),
+                pos: ut.pos,
+            }),
             UniTermNode::Record(r) => Types::try_from(r),
             UniTermNode::Types(ty) => Ok(ty),
-            UniTermNode::Term(rt) => Ok(Types(TypeF::Flat(rt))),
+            UniTermNode::Term(rt) => Ok(Types {
+                types: TypeF::Flat(rt),
+                pos: ut.pos,
+            }),
         }
     }
 }
@@ -129,9 +135,10 @@ impl From<Term> for UniTerm {
 
 impl From<Types> for UniTerm {
     fn from(ty: Types) -> Self {
+        let pos = ty.pos;
         UniTerm {
             node: UniTermNode::Types(ty),
-            pos: TermPos::None,
+            pos,
         }
     }
 }
@@ -267,7 +274,10 @@ impl UniRecord {
                     }
                 },
             )?;
-        Ok(Types(TypeF::Record(rrows)))
+        Ok(Types {
+            types: TypeF::Record(rrows),
+            pos: self.pos,
+        })
     }
 
     pub fn with_pos(mut self, pos: TermPos) -> Self {
@@ -338,9 +348,13 @@ impl TryFrom<UniRecord> for Types {
                     )
                 })
         } else {
-            ur.clone()
-                .into_type_strict()
-                .or_else(|_| RichTerm::try_from(ur).map(|rt| Types(TypeF::Flat(rt))))
+            let pos = ur.pos;
+            ur.clone().into_type_strict().or_else(|_| {
+                RichTerm::try_from(ur).map(|rt| Types {
+                    types: TypeF::Flat(rt),
+                    pos,
+                })
+            })
         }
     }
 }
@@ -499,7 +513,7 @@ impl FixTypeVars for Types {
         mut bound_vars: BoundVarEnv,
         span: RawSpan,
     ) -> Result<(), ParseError> {
-        match self.0 {
+        match self.types {
             TypeF::Dyn
             | TypeF::Num
             | TypeF::Bool
@@ -519,7 +533,7 @@ impl FixTypeVars for Types {
                 } else {
                     let id = *id;
                     let pos = id.pos;
-                    self.0 = TypeF::Flat(RichTerm::new(Term::Var(id), pos));
+                    self.types = TypeF::Flat(RichTerm::new(Term::Var(id), pos));
                 }
                 Ok(())
             }
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index 62c87293..ccaaa2e5 100644
--- a/src/parser/utils.rs
+++ b/src/parser/utils.rs
@@ -316,7 +316,10 @@ pub fn combine_match_annots(
         (None, None) => {
             let dummy_annot = TypeAnnotation {
                 contracts: vec![LabeledType {
-                    types: Types(TypeF::Dyn),
+                    types: Types {
+                        types: TypeF::Dyn,
+                        pos: TermPos::Original(span),
+                    },
                     label: Label {
                         span,
                         ..Default::default()
@@ -549,12 +552,8 @@ pub fn mk_pos(src_id: FileId, l: usize, r: usize) -> TermPos {
 pub fn mk_label(types: Types, src_id: FileId, l: usize, r: usize) -> Label {
     Label {
         types: Rc::new(types),
-        tag: String::new(),
         span: mk_span(src_id, l, r),
-        arg_idx: None,
-        arg_pos: TermPos::None,
-        polarity: true,
-        path: Vec::new(),
+        ..Default::default()
     }
 }
 
diff --git a/src/pretty.rs b/src/pretty.rs
index 81b9f80f..9955f4b7 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -796,7 +796,7 @@ where
 {
     fn pretty(self, allocator: &'a D) -> DocBuilder<'a, D, A> {
         use TypeF::*;
-        match self.0 {
+        match self.types {
             Dyn => allocator.text("Dyn"),
             Num => allocator.text("Num"),
             Bool => allocator.text("Bool"),
@@ -816,7 +816,11 @@ where
             Forall { var, ref body, .. } => {
                 let mut curr = body.as_ref();
                 let mut foralls = vec![&var];
-                while let Types(Forall { var, ref body, .. }) = curr {
+                while let Types {
+                    types: Forall { var, ref body, .. },
+                    ..
+                } = curr
+                {
                     foralls.push(var);
                     curr = body;
                 }
@@ -843,7 +847,7 @@ where
                 .append(ty.pretty(allocator))
                 .append(allocator.line())
                 .braces(),
-            Arrow(dom, codom) => match dom.0 {
+            Arrow(dom, codom) => match dom.types {
                 Arrow(..) | Forall { .. } => dom
                     .pretty(allocator)
                     .parens()
diff --git a/src/program.rs b/src/program.rs
index b05c95a6..9cdb82f8 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -288,8 +288,8 @@ impl<EC: EvalCache> Program<EC> {
         E: IntoDiagnostics<FileId>,
     {
         let cache = self.vm.import_resolver_mut();
-        let contracts_id = cache.id_of("<stdlib/contract.ncl>");
-        let diagnostics = error.into_diagnostics(cache.files_mut(), contracts_id);
+        let stdlib_ids = cache.get_all_stdlib_modules_file_id();
+        let diagnostics = error.into_diagnostics(cache.files_mut(), stdlib_ids.as_ref());
         let mut buffer = Ansi::new(Cursor::new(Vec::new()));
         let config = codespan_reporting::term::Config::default();
         // write to `buffer`
@@ -379,8 +379,8 @@ where
 {
     let writer = StandardStream::stderr(color_opt.into());
     let config = codespan_reporting::term::Config::default();
-    let contracts_id = cache.id_of("<stdlib/contract.ncl>");
-    let diagnostics = error.into_diagnostics(cache.files_mut(), contracts_id);
+    let stdlib_ids = cache.get_all_stdlib_modules_file_id();
+    let diagnostics = error.into_diagnostics(cache.files_mut(), stdlib_ids.as_ref());
 
     let result = diagnostics.iter().try_for_each(|d| {
         codespan_reporting::term::emit(&mut writer.lock(), &config, cache.files_mut(), d)
diff --git a/src/repl/simple_frontend.rs b/src/repl/simple_frontend.rs
index b260abea..0185ad7a 100644
--- a/src/repl/simple_frontend.rs
+++ b/src/repl/simple_frontend.rs
@@ -47,7 +47,7 @@ pub fn input<R: Repl>(repl: &mut R, line: &str) -> Result<InputResult, InputErro
             ))),
             Ok(Command::Typecheck(exp)) => repl
                 .typecheck(&exp)
-                .map(|types| InputResult::Success(format!("Ok: {}", types)))
+                .map(|types| InputResult::Success(format!("Ok: {types}")))
                 .map_err(InputError::from),
             Ok(Command::Query { target, path }) => repl
                 .query(target, path)
diff --git a/src/repl/wasm_frontend.rs b/src/repl/wasm_frontend.rs
index 1fd04a47..565b1e93 100644
--- a/src/repl/wasm_frontend.rs
+++ b/src/repl/wasm_frontend.rs
@@ -194,8 +194,8 @@ impl WasmInputResult {
     fn error(cache: &mut Cache, error: InputError) -> Self {
         let (msg, errors) = match error {
             InputError::NickelError(err) => {
-                let contracts_id = cache.id_of("<stdlib/contract.ncl>");
-                let diagnostics = err.into_diagnostics(cache.files_mut(), contracts_id);
+                let stdlib_ids = cache.get_all_stdlib_modules_file_id();
+                let diagnostics = err.into_diagnostics(cache.files_mut(), stdlib_ids.as_ref());
 
                 let msg = diags_to_string(cache, &diagnostics);
                 let errors: Vec<WasmErrorDiagnostic> = diagnostics
@@ -290,8 +290,8 @@ pub fn diags_to_string(cache: &mut Cache, diags: &[Diagnostic<FileId>]) -> Strin
 pub fn err_to_string(cache: &mut Cache, error: InputError) -> String {
     match error {
         InputError::NickelError(nickel_err) => {
-            let contracts_id = cache.id_of("<stdlib/contract.ncl>");
-            let diags = nickel_err.into_diagnostics(cache.files_mut(), contracts_id);
+            let stdlib_ids = cache.get_all_stdlib_modules_file_id();
+            let diags = nickel_err.into_diagnostics(cache.files_mut(), stdlib_ids.as_ref());
             diags_to_string(cache, &diags)
         }
         InputError::Other(msg) => msg,
diff --git a/src/serialize.rs b/src/serialize.rs
index 927d95d7..542233da 100644
--- a/src/serialize.rs
+++ b/src/serialize.rs
@@ -385,7 +385,7 @@ mod tests {
             json!(["a", "bc", "def", "g"])
         );
         assert_json_eq!(
-            r#"array.fold (fun elt acc => [[elt]] @ acc) [] [1, 2, 3, 4]"#,
+            r#"array.fold_right (fun elt acc => [[elt]] @ acc) [] [1, 2, 3, 4]"#,
             json!([[1], [2], [3], [4]])
         );
         assert_json_eq!("[\"a\", 1, false, `foo]", json!(["a", 1, false, "foo"]));
diff --git a/src/term/mod.rs b/src/term/mod.rs
index b349883f..b804bd84 100644
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@@ -615,7 +615,7 @@ impl Term {
             }
             Annotated(ref mut annot, ref mut t) => {
                 annot.iter_mut().for_each(|LabeledType { types, .. }| {
-                    if let TypeF::Flat(ref mut rt) = types.0 {
+                    if let TypeF::Flat(ref mut rt) = types.types {
                         func(rt)
                     }
                 });
@@ -1960,7 +1960,7 @@ mod tests {
 
         let inner = TypeAnnotation {
             types: Some(LabeledType {
-                types: Types(TypeF::Num),
+                types: Types::from(TypeF::Num),
                 label: Label::dummy(),
             }),
             ..Default::default()
diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs
index 0d866d4d..5e1868d6 100644
--- a/src/transform/free_vars.rs
+++ b/src/transform/free_vars.rs
@@ -178,7 +178,7 @@ impl CollectFreeVars for RichTerm {
 
 impl CollectFreeVars for Types {
     fn collect_free_vars(&mut self, set: &mut HashSet<Ident>) {
-        match &mut self.0 {
+        match &mut self.types {
             TypeF::Dyn
             | TypeF::Num
             | TypeF::Bool
diff --git a/src/transform/substitute_wildcards.rs b/src/transform/substitute_wildcards.rs
index 39387fff..da2c827c 100644
--- a/src/transform/substitute_wildcards.rs
+++ b/src/transform/substitute_wildcards.rs
@@ -53,7 +53,10 @@ pub fn transform_one(rt: RichTerm, wildcards: &Wildcards) -> RichTerm {
 
 /// Get the inferred type for a wildcard, or `Dyn` if no type was inferred.
 fn get_wildcard_type(wildcards: &Wildcards, id: usize) -> Types {
-    wildcards.get(id).cloned().unwrap_or(Types(TypeF::Dyn))
+    wildcards
+        .get(id)
+        .cloned()
+        .unwrap_or(Types::from(TypeF::Dyn))
 }
 
 trait SubstWildcard {
@@ -64,8 +67,8 @@ trait SubstWildcard {
 impl SubstWildcard for Types {
     fn subst_wildcards(self, wildcards: &Wildcards) -> Types {
         self.traverse::<_, _, Infallible>(
-            &|ty, _| {
-                if let Types(TypeF::Wildcard(id)) = ty {
+            &|ty: Types, _| {
+                if let TypeF::Wildcard(id) = ty.types {
                     Ok(get_wildcard_type(wildcards, id))
                 } else {
                     Ok(ty)
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index 4adcbb8a..69629fba 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -184,9 +184,15 @@ impl<E: TermEnvironment + Clone> std::convert::TryInto<Types> for GenericUnifTyp
                     GenericUnifRecordRows::try_into,
                     UnifEnumRows::try_into,
                 )?;
-                Ok(Types(converted))
+                Ok(Types::from(converted))
+            }
+            GenericUnifType::Contract(t, _) => {
+                let pos = t.pos;
+                Ok(Types {
+                    types: TypeF::Flat(t),
+                    pos,
+                })
             }
-            GenericUnifType::Contract(t, _) => Ok(Types(TypeF::Flat(t))),
             _ => Err(()),
         }
     }
@@ -340,7 +346,7 @@ impl<E: TermEnvironment + Clone> GenericUnifType<E> {
     /// [`GenericUnifType::Contract`] which also stores a term environment, required for checking type
     /// equality involving contracts.
     pub fn from_type(ty: Types, env: &E) -> Self {
-        match ty.0 {
+        match ty.types {
             TypeF::Flat(t) => GenericUnifType::Contract(t, env.clone()),
             ty => GenericUnifType::Concrete(ty.map(
                 |ty_| Box::new(GenericUnifType::from_type(*ty_, env)),
@@ -433,18 +439,18 @@ impl UnifType {
         match self {
             UnifType::UnifVar(p) => match table.root_type(p) {
                 t @ UnifType::Concrete(_) => t.into_type(table),
-                _ => Types(TypeF::Dyn),
+                _ => Types::from(TypeF::Dyn),
             },
-            UnifType::Constant(_) => Types(TypeF::Dyn),
+            UnifType::Constant(_) => Types::from(TypeF::Dyn),
             UnifType::Concrete(t) => {
                 let mapped = t.map(
                     |btyp| Box::new(btyp.into_type(table)),
                     |urrows| urrows.into_rrows(table),
                     |uerows| uerows.into_erows(table),
                 );
-                Types(mapped)
+                Types::from(mapped)
             }
-            UnifType::Contract(t, _) => Types(TypeF::Flat(t)),
+            UnifType::Contract(t, _) => Types::from(TypeF::Flat(t)),
         }
     }
 
@@ -962,7 +968,7 @@ fn walk_type<L: Linearizer>(
     mut linearizer: L,
     ty: &Types,
 ) -> Result<(), TypecheckError> {
-    match &ty.0 {
+    match &ty.types {
        TypeF::Dyn
        | TypeF::Num
        | TypeF::Bool
@@ -1652,10 +1658,10 @@ fn replace_wildcards_with_var(
         ))
     }
 
-    match ty.0 {
+    match ty.types {
         TypeF::Wildcard(i) => get_wildcard_var(table, wildcard_vars, i),
         TypeF::Flat(t) => UnifType::Contract(t, env.clone()),
-        _ => UnifType::Concrete(ty.0.map_state(
+        _ => UnifType::Concrete(ty.types.map_state(
             |ty, (table, wildcard_vars)| {
                 Box::new(replace_wildcards_with_var(table, wildcard_vars, *ty, env))
             },
@@ -1690,11 +1696,11 @@ pub enum ApparentType {
 impl From<ApparentType> for Types {
     fn from(at: ApparentType) -> Self {
         match at {
-            ApparentType::Annotated(ty) if has_wildcards(&ty) => Types(TypeF::Dyn),
+            ApparentType::Annotated(ty) if has_wildcards(&ty) => Types::from(TypeF::Dyn),
             ApparentType::Annotated(ty)
             | ApparentType::Inferred(ty)
             | ApparentType::Approximated(ty) => ty,
-            ApparentType::FromEnv(uty) => uty.try_into().ok().unwrap_or(Types(TypeF::Dyn)),
+            ApparentType::FromEnv(uty) => uty.try_into().ok().unwrap_or(Types::from(TypeF::Dyn)),
         }
     }
 }
@@ -1719,7 +1725,7 @@ fn field_apparent_type(
                 .as_ref()
                 .map(|v| apparent_type(v.as_ref(), env, resolver))
         })
-        .unwrap_or(ApparentType::Approximated(Types(TypeF::Dyn)))
+        .unwrap_or(ApparentType::Approximated(Types::from(TypeF::Dyn)))
 }
 
 /// Determine the apparent type of a let-bound expression.
@@ -1767,17 +1773,17 @@ pub fn apparent_type(
                 .first()
                 .map(|labeled_ty| ApparentType::Annotated(labeled_ty.types.clone()))
                 .unwrap_or_else(|| apparent_type(value.as_ref(), env, resolver)),
-            Term::Num(_) => ApparentType::Inferred(Types(TypeF::Num)),
-            Term::Bool(_) => ApparentType::Inferred(Types(TypeF::Bool)),
-            Term::SealingKey(_) => ApparentType::Inferred(Types(TypeF::Sym)),
-            Term::Str(_) | Term::StrChunks(_) => ApparentType::Inferred(Types(TypeF::Str)),
-            Term::Array(..) => {
-                ApparentType::Approximated(Types(TypeF::Array(Box::new(Types(TypeF::Dyn)))))
-            }
+            Term::Num(_) => ApparentType::Inferred(Types::from(TypeF::Num)),
+            Term::Bool(_) => ApparentType::Inferred(Types::from(TypeF::Bool)),
+            Term::SealingKey(_) => ApparentType::Inferred(Types::from(TypeF::Sym)),
+            Term::Str(_) | Term::StrChunks(_) => ApparentType::Inferred(Types::from(TypeF::Str)),
+            Term::Array(..) => ApparentType::Approximated(Types::from(TypeF::Array(Box::new(
+                Types::from(TypeF::Dyn),
+            )))),
             Term::Var(id) => env
                 .and_then(|envs| envs.get(id).cloned())
                 .map(ApparentType::FromEnv)
-                .unwrap_or(ApparentType::Approximated(Types(TypeF::Dyn))),
+                .unwrap_or(ApparentType::Approximated(Types::from(TypeF::Dyn))),
             Term::ResolvedImport(file_id) => match resolver {
                 Some(r) if !imports_seen.contains(file_id) => {
                     imports_seen.insert(*file_id);
@@ -1787,9 +1793,9 @@ pub fn apparent_type(
                         .expect("Internal error: resolved import not found during typechecking.");
                     apparent_type_check_cycle(&t.term, env, Some(r), imports_seen)
                 }
-                _ => ApparentType::Approximated(Types(TypeF::Dyn)),
+                _ => ApparentType::Approximated(Types::from(TypeF::Dyn)),
             },
-            _ => ApparentType::Approximated(Types(TypeF::Dyn)),
+            _ => ApparentType::Approximated(Types::from(TypeF::Dyn)),
         }
     }
 
@@ -1831,7 +1837,7 @@ fn has_wildcards(ty: &Types) -> bool {
     ty.clone()
         .traverse::<_, _, std::convert::Infallible>(
             &|ty: Types, has_wildcard| {
-                if ty.0.is_wildcard() {
+                if ty.types.is_wildcard() {
                     *has_wildcard = true;
                 }
                 Ok(ty)
diff --git a/src/typecheck/reporting.rs b/src/typecheck/reporting.rs
index 079d5a2a..169f73db 100644
--- a/src/typecheck/reporting.rs
+++ b/src/typecheck/reporting.rs
@@ -163,8 +163,8 @@ pub fn to_type(
     let ty = ty.into_root(table);
 
     match ty {
-        UnifType::UnifVar(p) => Types(TypeF::Var(var_name(reported_names, names, p))),
-        UnifType::Constant(c) => Types(TypeF::Var(cst_name(reported_names, names, c))),
+        UnifType::UnifVar(p) => Types::from(TypeF::Var(var_name(reported_names, names, p))),
+        UnifType::Constant(c) => Types::from(TypeF::Var(cst_name(reported_names, names, c))),
         UnifType::Concrete(t) => {
             let mapped = t.map_state(
                 |btyp, names| Box::new(to_type(table, reported_names, names, *btyp)),
@@ -172,8 +172,8 @@ pub fn to_type(
                 |erows, names| erows_to_type(table, reported_names, names, erows),
                 names,
             );
-            Types(mapped)
+            Types::from(mapped)
         }
-        UnifType::Contract(t, _) => Types(TypeF::Flat(t)),
+        UnifType::Contract(t, _) => Types::from(TypeF::Flat(t)),
     }
 }
diff --git a/src/types.rs b/src/types.rs
index 7ce4e503..47ba4c0c 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -53,6 +53,7 @@ use crate::{
     error::{EvalError, ParseError, ParseErrors, TypecheckError},
     identifier::Ident,
     mk_app, mk_fun,
+    position::TermPos,
     term::make as mk_term,
     term::{record::RecordData, RichTerm, Term, Traverse, TraverseOrder},
 };
@@ -262,9 +263,13 @@ pub type RecordRow = RecordRowF<Box<Types>>;
 #[derive(Clone, PartialEq, Debug)]
 /// Concrete, recursive definition for record rows.
 pub struct RecordRows(pub RecordRowsF<Box<Types>, Box<RecordRows>>);
+
 /// Concrete, recursive type for a Nickel type.
 #[derive(Clone, PartialEq, Debug)]
-pub struct Types(pub TypeF<Box<Types>, RecordRows, EnumRows>);
+pub struct Types {
+    pub types: TypeF<Box<Types>, RecordRows, EnumRows>,
+    pub pos: TermPos,
+}
 
 impl<Ty, RRows> RecordRowsF<Ty, RRows> {
     /// Map functions over the children nodes of record rows, when seen as a tree. The mutable
@@ -805,7 +810,7 @@ impl RecordRows {
         if path.len() == 1 {
             next
         } else {
-            match next.map(|ty| ty.0) {
+            match next.map(|ty| ty.types) {
                 Some(TypeF::Record(rrows)) => rrows.row_find_path(&path[1..]),
                 _ => None,
             }
@@ -820,7 +825,21 @@ impl RecordRows {
     }
 }
 
+impl From<TypeF<Box<Types>, RecordRows, EnumRows>> for Types {
+    fn from(types: TypeF<Box<Types>, RecordRows, EnumRows>) -> Self {
+        Types {
+            types,
+            pos: TermPos::None,
+        }
+    }
+}
+
 impl Types {
+    /// Creates a `Type` with the specified position
+    pub fn with_pos(self, pos: TermPos) -> Types {
+        Types { pos, ..self }
+    }
+
     /// Return the contract corresponding to a type, either as a function or a record. Said
     /// contract must then be applied using the `Assume` primitive operation.
     pub fn contract(&self) -> Result<RichTerm, UnboundTypeVariableError> {
@@ -830,10 +849,10 @@ impl Types {
 
     /// Returns true if this type is a function type, false otherwise.
     pub fn is_function_type(&self) -> bool {
-        match self {
-            Types(TypeF::Forall { body, .. }) => body.is_function_type(),
-            Types(TypeF::Arrow(..)) => true,
-            Types(_) => false,
+        match &self.types {
+            TypeF::Forall { body, .. } => body.is_function_type(),
+            TypeF::Arrow(..) => true,
+            _ => false,
         }
     }
 
@@ -854,7 +873,7 @@ impl Types {
     ) -> Result<RichTerm, UnboundTypeVariableError> {
         use crate::stdlib::contract;
 
-        let ctr = match self.0 {
+        let ctr = match self.types {
             TypeF::Dyn => contract::dynamic(),
             TypeF::Num => contract::num(),
             TypeF::Bool => contract::bool(),
@@ -906,7 +925,7 @@ impl Types {
     pub fn fmt_is_atom(&self) -> bool {
         use TypeF::*;
 
-        match &self.0 {
+        match &self.types {
             Dyn | Num | Bool | Str | Var(_) | Record(_) | Enum(_) => true,
             Flat(rt) if matches!(*rt.term, Term::Var(_)) => true,
             _ => false,
@@ -921,24 +940,24 @@ impl Traverse<Types> for Types {
     {
         match order {
             TraverseOrder::TopDown => {
-                let inner = f(self, state)?.0.try_map_state(
+                let inner = f(self, state)?.types.try_map_state(
                     |ty, state| Ok(Box::new(ty.traverse(f, state, order)?)),
                     |rrows, state| rrows.traverse(f, state, order),
                     |erows, _| Ok(erows),
                     state,
                 )?;
 
-                Ok(Types(inner))
+                Ok(Types::from(inner))
             }
             TraverseOrder::BottomUp => {
-                let traversed_depth_first = self.0.try_map_state(
+                let traversed_depth_first = self.types.try_map_state(
                     |ty, state| Ok(Box::new(ty.traverse(f, state, order)?)),
                     |rrows, state| rrows.traverse(f, state, order),
                     |erows, _| Ok(erows),
                     state,
                 )?;
 
-                f(Types(traversed_depth_first), state)
+                f(Types::from(traversed_depth_first), state)
             }
         }
     }
@@ -949,8 +968,8 @@ impl Traverse<RichTerm> for Types {
     where
         F: Fn(RichTerm, &mut S) -> Result<RichTerm, E>,
     {
-        let f_on_type = |ty: Types, s: &mut S| match ty.0 {
-            TypeF::Flat(t) => t.traverse(f, s, order).map(|t| Types(TypeF::Flat(t))),
+        let f_on_type = |ty: Types, s: &mut S| match ty.types {
+            TypeF::Flat(t) => t.traverse(f, s, order).map(|t| Types::from(TypeF::Flat(t))),
             _ => Ok(ty),
         };
 
@@ -995,7 +1014,7 @@ impl Display for EnumRows {
 
 impl Display for Types {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        match &self.0 {
+        match &self.types {
             TypeF::Dyn => write!(f, "Dyn"),
             TypeF::Num => write!(f, "Num"),
             TypeF::Bool => write!(f, "Bool"),
@@ -1015,7 +1034,11 @@ impl Display for Types {
             TypeF::Forall { var, ref body, .. } => {
                 let mut curr: &Types = body.as_ref();
                 write!(f, "forall {var}")?;
-                while let Types(TypeF::Forall { var, ref body, .. }) = curr {
+                while let Types {
+                    types: TypeF::Forall { var, ref body, .. },
+                    ..
+                } = curr
+                {
                     write!(f, " {var}")?;
                     curr = body;
                 }
@@ -1024,7 +1047,7 @@ impl Display for Types {
             TypeF::Enum(row) => write!(f, "[|{row}|]"),
             TypeF::Record(row) => write!(f, "{{{row}}}"),
             TypeF::Dict(ty) => write!(f, "{{_: {ty}}}"),
-            TypeF::Arrow(dom, codom) => match dom.0 {
+            TypeF::Arrow(dom, codom) => match dom.types {
                 TypeF::Arrow(_, _) | TypeF::Forall { .. } => write!(f, "({dom}) -> {codom}"),
                 _ => write!(f, "{dom} -> {codom}"),
             },
diff --git a/stdlib/array.ncl b/stdlib/array.ncl
index 30652e4e..36a24a48 100644
--- a/stdlib/array.ncl
+++ b/stdlib/array.ncl
@@ -21,30 +21,50 @@
        else
          %blame% (%tag% "not a array" label),
 
-    head : forall a. Array a -> a
+    first : forall a. Array a -> a
       | doc m%"
-        Results in the head (first element) of the given array.
+        Results in the first element of the given array.
 
         For example:
         ```nickel
-          head [ "this is the head", "this is not" ] =>
+          first [ "this is the head", "this is not" ] =>
             "this is the head"
         ```
         "%
       = fun l => %head% l,
 
-    tail : forall a. Array a -> Array a
+    last : forall a. Array a -> a
+      | doc "TODO"
+      = fun l => %elem_at% l (%length% l - 1),
+
+    drop_first : forall a. Array a -> Array a
       | doc m%"
-        Results in the tail (everything but the first element) of the given array.
+        Results in the given array without the first element.
 
         For example:
         ```nickel
-          tail [ 1, 2, 3 ] =>
+          drop_first [ 1, 2, 3 ] =>
             [ 2, 3 ]
         ```
         "%
       = fun l => %tail% l,
 
+    drop_last : forall a. Array a -> Array a
+      | doc m%"
+        Results in the given array without the last element.
+
+        For example:
+        ```nickel
+          drop_last [ 1, 2, 3 ] =>
+            [ 1, 2 ]
+        ```
+        "%
+      # TODO: we need a slice primop
+      = fun l => l
+        |> reverse
+        |> drop_first
+        |> reverse,
+
     length : forall a. Array a -> Num
       | doc m%"
         Results in a number representing the length of the given array.
@@ -70,13 +90,13 @@
         "%
       = fun f l => %map% l f,
 
-    elem_at : forall a. Num -> Array a -> a
+    at : forall a. Num -> Array a -> a
       | doc m%"
         Retrieves the n'th element from a array (0-indexed).
 
         For example:
         ```nickel
-          elem_at 3 [ "zero" "one" "two" "three" "four" ] =>
+          at 3 [ "zero" "one" "two" "three" "four" ] =>
             "three"
         ```
         "%
@@ -94,16 +114,16 @@
         "%
       = fun l1 l2 => l1 @ l2,
 
-    foldl : forall a b. (a -> b -> a) -> a -> Array b -> a
+    fold_left : forall a b. (a -> b -> a) -> a -> Array b -> a
       | doc m%"
-        Fold a function over a array.
-        `foldl f init [x1, x2, ..., xn]` results in `f (... (f (f init x1) x2) ...) xn`.
+        Fold a function over an array.
+        `fold_left f init [x1, x2, ..., xn]` results in `f (... (f (f init x1) x2) ...) xn`.
 
         This function is strict in the intermediate accumulator.
 
         For example:
         ```nickel
-          foldl (fun acc e => acc + e) 0 [ 1, 2, 3 ] =>
+          fold_left (fun acc e => acc + e) 0 [ 1, 2, 3 ] =>
             (((0 + 1) + 2) 3) =>
             6
         ```
@@ -120,14 +140,14 @@
           in
           go acc 0,
 
-    fold : forall a b. (a -> b -> b) -> b -> Array a -> b
+    fold_right : forall a b. (a -> b -> b) -> b -> Array a -> b
       | doc m%"
         Fold a function over a array.
-        `fold f init [x1, x2, ..., xn]` results in `f x1 (f x2 (... (f xn init) ...))`.
+        `fold_right f init [x1, x2, ..., xn]` results in `f x1 (f x2 (... (f xn init) ...))`.
 
         For example:
         ```nickel
-          fold (fun e acc => acc @ [e]) [] [ 1, 2, 3 ] =>
+          fold_right (fun e acc => acc @ [e]) [] [ 1, 2, 3 ] =>
             ((([] @ [3]) @ [2]) @ [1]) =>
             [ 3, 2, 1 ]
         ```
@@ -142,18 +162,31 @@
             |> f (%elem_at% l n)
         in go 0,
 
-    cons : forall a. a -> Array a -> Array a
+    prepend : forall a. a -> Array a -> Array a
       | doc m%"
-        Construct a array given the head and tail of the array.
+        Construct an array given the first element and the rest of the array.
 
         For example:
         ```nickel
-          cons 1 [ 2, 3 ] =>
+          prepend 1 [ 2, 3 ] =>
             [ 1, 2, 3 ]
         ```
         "%
       = fun x l => [x] @ l,
 
+    append : forall a. a -> Array a -> Array a
+      | doc m%"
+        Construct an array given the last element and the rest of the array.
+
+        For example:
+        ```nickel
+          append 3 [ 1, 2 ] =>
+            [ 1, 2, 3 ]
+        ```
+        "%
+      = fun x l => l @ [x],
+
+
     reverse : forall a. Array a -> Array a
       | doc m%"
         Reverses the order of a array.
@@ -164,7 +197,7 @@
             [ 3, 2, 1 ]
         ```
         "%
-      = fun l => foldl (fun acc e => [e] @ acc) [] l,
+      = fun l => fold_left (fun acc e => [e] @ acc) [] l,
 
     filter : forall a. (a -> Bool) -> Array a -> Array a
       | doc m%"
@@ -176,7 +209,7 @@
             [ 3, 2, 1 ]
         ```
         "%
-      = fun pred l => foldl (fun acc x => if pred x then acc @ [x] else acc) [] l,
+      = fun pred l => fold_left (fun acc x => if pred x then acc @ [x] else acc) [] l,
 
     flatten : forall a. Array (Array a) -> Array a
       | doc m%"
@@ -188,7 +221,7 @@
             [1, 2, 3, 4]
         ```
         "%
-      = fun l => fold (fun l acc => l @ acc) [] l,
+      = fun l => fold_right (fun l acc => l @ acc) [] l,
 
     all : forall a. (a -> Bool) -> Array a -> Bool
       | doc m%"
@@ -202,7 +235,7 @@
             false
         ```
         "%
-      = fun pred l => fold (fun x acc => if pred x then acc else false) true l,
+      = fun pred l => fold_right (fun x acc => if pred x then acc else false) true l,
 
     any : forall a. (a -> Bool) -> Array a -> Bool
       | doc m%"
@@ -216,9 +249,9 @@
             false
         ```
         "%
-      = fun pred l => fold (fun x acc => if pred x then true else acc) false l,
+      = fun pred l => fold_right (fun x acc => if pred x then true else acc) false l,
 
-    elem : Dyn -> Array Dyn -> Bool
+    elem : forall a. a -> Array a -> Bool
       | doc m%"
         Results in true if the given element is a member of the array, false otherwise.
 
@@ -248,7 +281,7 @@
           else
             {right = acc.right, wrong = acc.wrong @ [x]}
         in
-        foldl aux {right = [], wrong = []} l,
+        fold_left aux {right = [], wrong = []} l,
 
     generate : forall a. (Num -> a) -> Num -> Array a
       | doc m%"
@@ -273,6 +306,7 @@
             [ 1, 2, 4, 5 ]
         ```
         "%
+      #TODO: maybe inline partition to avoid contract checks?
       = fun cmp l =>
         let first = %head% l in
         let parts = partition (fun x => (cmp x first == `Lesser)) (%tail% l) in
@@ -309,8 +343,8 @@
         ```
       "%
       = fun v arr =>
-        if length arr <= 1
+        if %length% arr <= 1
         then arr
-        else [ head arr ] @ (tail arr |> flat_map (fun a => [v, a])),
+        else [ %head% arr ] @ (%tail% arr |> flat_map (fun a => [v, a])),
   }
 }
diff --git a/stdlib/builtin.ncl b/stdlib/builtin.ncl
index 9be3764e..1f23d90d 100644
--- a/stdlib/builtin.ncl
+++ b/stdlib/builtin.ncl
@@ -57,15 +57,15 @@
 
     = fun x => %typeof% x == `Enum,
 
-    is_fun : Dyn -> Bool
+    is_function : Dyn -> Bool
     | doc m%"
       Checks if the given value is a function.
 
       For example
       ```nickel
-        is_fun (fun x => x) =>
+        is_function (fun x => x) =>
           true
-        is_fun 42 =>
+        is_function 42 =>
           false
       ```
       "%
diff --git a/stdlib/function.ncl b/stdlib/function.ncl
index e332bff7..3cdd6038 100644
--- a/stdlib/function.ncl
+++ b/stdlib/function.ncl
@@ -40,20 +40,20 @@
     "%%
     = fun f x y => f y x,
 
-    fst : forall a b. a -> b -> a
+    first : forall a b. a -> b -> a
     | doc m%"
     Always returns the first argument:
     ```nickel
-    fst 5 7 => 5
+    first 5 7 => 5
     ```
     "%
     = const,
 
-    snd : forall a b. a -> b -> b
+    second : forall a b. a -> b -> b
     | doc m%"
     Always returns the second argument:
     ```nickel
-    snd 5 7 => 7
+    second 5 7 => 7
     ```
     "%
     = flip const,
@@ -70,6 +70,6 @@
         => "Hello, World!"
       ```
     "%%
-    = fun x fs => array.foldl (|>) x fs,
+    = fun x fs => array.fold_left (|>) x fs,
   }
 }
diff --git a/stdlib/internals.ncl b/stdlib/internals.ncl
index 3e4f293c..90e32c74 100644
--- a/stdlib/internals.ncl
+++ b/stdlib/internals.ncl
@@ -50,7 +50,7 @@
       # Returns the sub-record of `l` containing only those fields which are not
       # present in `r`. If `l` has a sealed polymorphic tail then it will be
       # preserved.
-      let field_diff = fun l r => array.foldl
+      let field_diff = fun l r => array.fold_left
         (fun acc f =>
           if %has_field% f r then
             acc
@@ -65,7 +65,7 @@
 
       if %length% missing_fields == 0 then
         let tail_fields = field_diff t field_contracts in
-        let fields_with_contracts = array.foldl
+        let fields_with_contracts = array.fold_left
           (fun acc f =>
             if %has_field% f field_contracts then
               let contract = field_contracts."%{f}" in
diff --git a/stdlib/num.ncl b/stdlib/num.ncl
index 667b554f..f47ea6af 100644
--- a/stdlib/num.ncl
+++ b/stdlib/num.ncl
@@ -1,14 +1,14 @@
 {
   num = {
-    Int
+    Integer
     | doc m%"
       Contract to enforce a number is an integer.
 
       For example:
       ```nickel
-        (1.5 | Int) =>
+        (1.5 | Integer) =>
           error
-        (42 | Int) =>
+        (42 | Integer) =>
           42
       ```
       "%
@@ -88,7 +88,7 @@
       else
         %blame% (%tag% "not a number" label),
 
-    is_int : Num -> Bool
+    is_integer : Num -> Bool
     | doc m%"
       Checks if the given number is an integer.
 
@@ -169,15 +169,15 @@
       "%
     = fun x => x % 1,
 
-    trunc : Num -> Num
+    truncate : Num -> Num
     | doc m%"
       Truncates the given number.
 
       For example:
       ```nickel
-        trunc (-13.37) =>
+        truncate (-13.37) =>
           -13
-        trunc 42.5 =>
+        truncate 42.5 =>
           42
       ```
       "%
diff --git a/stdlib/record.ncl b/stdlib/record.ncl
index 4e682f59..d862412a 100644
--- a/stdlib/record.ncl
+++ b/stdlib/record.ncl
@@ -79,7 +79,7 @@
       "%
       = fun field r => %record_remove% field r,
 
-    update | forall a. Str -> a -> {_: a} -> {_: a}
+    update : forall a. Str -> a -> {_: a} -> {_: a}
       | doc m%"
         Update a field of a record with a new value. `update` doesn't mutate the
         original record but returns a new one instead. If the field to update is absent
@@ -177,7 +177,7 @@
         => { foo = 1, bar = 2 }
       ```
     "%
-    = array.foldl (&) {},
+    = array.fold_left (&) {},
 
     filter : forall a. (Str -> a -> Bool) -> {_: a} -> {_: a}
     | doc m%"
diff --git a/stdlib/string.ncl b/stdlib/string.ncl
index 92617673..c83cb7b7 100644
--- a/stdlib/string.ncl
+++ b/stdlib/string.ncl
@@ -51,19 +51,19 @@
         else
           %blame% (%tag% "not a string" l),
 
-    CharLiteral
+    Character
     | doc m%"
-      Contract to enforce the value is a character literal (i.e. a string of length 1).
+      Contract to enforce the value is a character (i.e. a string of length 1).
 
       For example:
       ```nickel
-        ("e" | CharLiteral) =>
+        ("e" | Character) =>
           "e"
-        ("#" | CharLiteral) =>
+        ("#" | Character) =>
           "#"
-        ("" | CharLiteral) =>
+        ("" | Character) =>
           error
-        (1 | CharLiteral) =>
+        (1 | Character) =>
           error
       ```
       "%
@@ -160,7 +160,7 @@
       if %length% l == 0 then
         ""
       else
-        %head% l ++ array.foldl (fun acc s => acc ++ sep ++ s) "" (%tail% l),
+        %head% l ++ array.fold_left (fun acc s => acc ++ sep ++ s) "" (%tail% l),
 
     split : Str -> Str -> Array Str
     | doc m%"
@@ -190,7 +190,7 @@
       "%
     = fun s => %str_trim% s,
 
-    chars : Str -> Array Str
+    characters : Str -> Array Str
     | doc m%"
       Separates a string into its individual characters.
 
@@ -202,9 +202,9 @@
       "%
     = fun s => %str_chars% s,
 
-    code | CharLiteral -> Num
+    codepoint | Character -> Num
     | doc m%%"
-      Results in the ascii code of the given character.
+      Results in the unicode codepoint of the given character if it fits into a single codepoint.
 
       For example:
       ```nickel
@@ -218,9 +218,9 @@
       "%%
     = fun s => %char_code% s,
 
-    from_code | Num -> CharLiteral
+    from_codepoint | Num -> Character
     | doc m%%"
-      Results in the character for a given ascii code. Any number outside the ascii range results in an error.
+      Results in the character for a given unicode codepoint.
 
       For example:
       ```nickel


Test patch:
diff --git a/tests/integration/pass/arrays.ncl b/tests/integration/pass/arrays.ncl
index 244ac7a5..737f2b0a 100644
--- a/tests/integration/pass/arrays.ncl
+++ b/tests/integration/pass/arrays.ncl
@@ -2,8 +2,8 @@ let {check, ..} = import "lib/assert.ncl" in
 
 [
   # accesses
-  array.elem_at 1 [1,2,3] == 2,
-  array.elem_at 1 (array.map (fun x => x + 1) [1,2,3]) == 3,
+  array.at 1 [1,2,3] == 2,
+  array.at 1 (array.map (fun x => x + 1) [1,2,3]) == 3,
 
   # length
   array.length [] == 0,
diff --git a/tests/integration/pass/lib/assert.ncl b/tests/integration/pass/lib/assert.ncl
index 8fd84aad..db4f3d63 100644
--- a/tests/integration/pass/lib/assert.ncl
+++ b/tests/integration/pass/lib/assert.ncl
@@ -26,5 +26,5 @@
 
     But will give more precise error reporting when one test fails.
     "%
-    = array.foldl (fun acc test => (test | Assert) && acc) true,
+    = array.fold_left (fun acc test => (test | Assert) && acc) true,
 }
diff --git a/tests/integration/pass/stdlib_string.ncl b/tests/integration/pass/stdlib_string.ncl
index afbc13bd..9b3487f1 100644
--- a/tests/integration/pass/stdlib_string.ncl
+++ b/tests/integration/pass/stdlib_string.ncl
@@ -12,7 +12,7 @@ let {check, ..} = import "lib/assert.ncl" in
   ("-1.2" | string.NumLiteral) == "-1.2",
   ("9001" | string.NumLiteral) == "9001",
   # string.CharLiteral
-  ("e" | string.CharLiteral) == "e",
+  ("e" | string.Character) == "e",
   # string.EnumTag
   (`Foo | string.EnumTag) == `Foo,
   # string.Stringable
@@ -37,19 +37,19 @@ let {check, ..} = import "lib/assert.ncl" in
   string.trim "​ ​ ​ a ​ ​ ​" == "​ ​ ​ a ​ ​ ​", # zero width spaces aren't whitespace
   string.trim "   \n   new\nline\n" == "new\nline",
   string.trim "　   	  " == "",
-  # string.chars
-  string.chars "漢字" == ["漢", "字"],
-  string.chars "👨‍❤️‍💋‍👨" == ["👨", "‍", "❤", "️", "‍", "💋", "‍", "👨"], # arguably wrong, splits the ZWJ combined emoji
-  string.chars "ab_cd" == ["a", "b", "_", "c", "d"],
-  string.chars "" == [],
+  # string.characters
+  string.characters "漢字" == ["漢", "字"],
+  string.characters "👨‍❤️‍💋‍👨" == ["👨", "‍", "❤", "️", "‍", "💋", "‍", "👨"], # arguably wrong, splits the ZWJ combined emoji
+  string.characters "ab_cd" == ["a", "b", "_", "c", "d"],
+  string.characters "" == [],
   # string.code
-  string.code "A" == 65,
-  string.code "%" == 37,
+  string.codepoint "A" == 65,
+  string.codepoint "%" == 37,
   # string.from_code
-  string.from_code 65 == "A",
-  string.from_code 37 == "%",
+  string.from_codepoint 65 == "A",
+  string.from_codepoint 37 == "%",
   # code/from_code round trip
-  (array.all (fun code => (string.code (string.from_code code)) == code) (array.generate function.id 127)),
+  (array.all (fun code => (string.codepoint (string.from_codepoint code)) == code) (array.generate function.id 127)),
   # string.uppercase
   string.uppercase "abcd" == "ABCD",
   string.uppercase "子供" == "子供",
diff --git a/tests/integration/stdlib_arrays_fail.rs b/tests/integration/stdlib_arrays_fail.rs
index 089c2ce3..4ce1d3d1 100644
--- a/tests/integration/stdlib_arrays_fail.rs
+++ b/tests/integration/stdlib_arrays_fail.rs
@@ -27,11 +27,11 @@ fn elem_at() {
     );
 
     assert_matches!(
-        eval("array.elem_at 0 {} 0"),
+        eval("array.at 0 {} 0"),
         Err(Error::EvalError(EvalError::BlameError { .. }))
     );
     assert_matches!(
-        eval("array.elem_at \"a\" []"),
+        eval("array.at \"a\" []"),
         Err(Error::EvalError(EvalError::BlameError { .. }))
     );
 }
@@ -55,9 +55,9 @@ fn head_tail() {
         Err(Error::EvalError(EvalError::TypeError(..)))
     );
 
-    // TODO: add non-empty contract to the input of array.head and array.tail
+    // TODO: add non-empty contract to the input of array.first and array.tail
     // assert_matches!(
-    //     eval("array.head []"),
+    //     eval("array.first []"),
     //     Err(Error::EvalError(EvalError::BlameError {..}))
     // );
     // assert_matches!(
@@ -65,11 +65,11 @@ fn head_tail() {
     //     Err(Error::EvalError(EvalError::BlameError {..}))
     // );
     assert_matches!(
-        eval("array.head false"),
+        eval("array.first false"),
         Err(Error::EvalError(EvalError::BlameError { .. }))
     );
     assert_matches!(
-        eval("array.tail 2"),
+        eval("array.drop_first 2"),
         Err(Error::EvalError(EvalError::BlameError { .. }))
     );
 }
diff --git a/tests/integration/typecheck_fail.rs b/tests/integration/typecheck_fail.rs
index 7799256e..6bb6a15d 100644
--- a/tests/integration/typecheck_fail.rs
+++ b/tests/integration/typecheck_fail.rs
@@ -287,8 +287,14 @@ let g : Num = f 0 in
 g"#
         ),
         Err(TypecheckError::TypeMismatch(
-            Types(TypeF::Arrow(_, _)),
-            Types(TypeF::Dyn),
+            Types {
+                types: TypeF::Arrow(_, _),
+                ..
+            },
+            Types {
+                types: TypeF::Dyn,
+                ..
+            },
             _
         ))
     );
@@ -304,8 +310,14 @@ fn locally_different_flat_types() {
              foo : lib.Contract"
         ),
         Err(TypecheckError::TypeMismatch(
-            Types(TypeF::Flat(..)),
-            Types(TypeF::Flat(..)),
+            Types {
+                types: TypeF::Flat(..),
+                ..
+            },
+            Types {
+                types: TypeF::Flat(..),
+                ..
+            },
             _
         ))
     );
diff --git a/tests/integration/typecheck_fail/row_type_unification_variable_mismatch.ncl b/tests/integration/typecheck_fail/row_type_unification_variable_mismatch.ncl
index 0adaf894..49897d99 100644
--- a/tests/integration/typecheck_fail/row_type_unification_variable_mismatch.ncl
+++ b/tests/integration/typecheck_fail/row_type_unification_variable_mismatch.ncl
@@ -1,6 +1,6 @@
 {
   split : forall a. Array { key: Str, value: a } -> { keys: Array Str, values: Array a } = fun pairs =>
-    array.fold (fun pair acc =>
+    array.fold_right (fun pair acc =>
       {
         # Error: `pair.key` should be wrapped in an array before we concat.
         keys = acc.keys @ pair.key,
@@ -8,4 +8,4 @@
       })
       { keys = [], values = [] }
       pairs,
-}
\ No newline at end of file
+}