Repository: tweag/nickel
Pull request #301 (2021-02-23 16:30:10)

Fill inherited position of evaluated terms
Depend on #300. Following #300, try to keep as much position information as possible during the evaluation.


Patch:
diff --git a/src/error.rs b/src/error.rs
index 43ea4741..9957c17a 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -172,7 +172,7 @@ pub enum TypecheckError {
     /// which deserves a good reporting, that can be caused e.g. by applying a function to an
     /// argument of a wrong type in some cases:
     ///
-    /// ```ignore
+    /// ```
     /// let id_mono = fun x => x in let _ign = id_mono true in id_mono 0 : Num
     /// ```
     ///
@@ -479,7 +479,7 @@ fn secondary(span: &RawSpan) -> Label<FileId> {
 /// For example, if one wants to report an error on a record, `alt_term` may be defined to `{ ...  }`.
 /// Then, if this record has no position (`span_opt` is `None`), the error will be reported as:
 ///
-/// ```ignore
+/// ```
 /// error: some error
 ///   -- <unkown> (generated by evaluation):1:2
 ///   |
diff --git a/src/eval.rs b/src/eval.rs
index 3580a176..4481eef2 100644
--- a/src/eval.rs
+++ b/src/eval.rs
@@ -574,14 +574,15 @@ where
                 }
             },
             Term::Promise(ty, l, t) | Term::Assume(ty, l, t) => {
+                let pos = pos.into_inherited();
                 stack.push_arg(
                     Closure {
                         body: t,
                         env: env.clone(),
                     },
-                    TermPos::None,
+                    pos,
                 );
-                stack.push_arg(Closure::atomic_closure(Term::Lbl(l).into()), TermPos::None);
+                stack.push_arg(Closure::atomic_closure(Term::Lbl(l).into()), pos);
                 Closure {
                     body: ty.contract(),
                     env,
diff --git a/src/label.rs b/src/label.rs
index 10e8bc65..17e7c0bb 100644
--- a/src/label.rs
+++ b/src/label.rs
@@ -11,7 +11,7 @@ pub mod ty_path {
     //!
     //! Checking higher-order contracts can involve a good share of intermediate contract checking.
     //! Take the following example:
-    //! ```ignore
+    //! ```
     //! Assume((Num -> Num) -> Num) -> Num -> Num, fun ev => fun cst => ev (fun x => cst))
     //! ```
     //! Once called, various checks will be performed on the arguments of functions and their return
@@ -22,7 +22,7 @@ pub mod ty_path {
     //! 4. etc.
     //!
     //! Each check can be linked to a base type occurrence (here, a `Num`) in the original type:
-    //! ```ignore
+    //! ```
     //! (Num -> Num) -> Num) -> Num -> Num
     //!  ^^^1   ^^^2    ^^^3    etc.
     //! ```
@@ -202,7 +202,7 @@ pub mod ty_path {
 /// One crucial aspect of first class contracts is to be able to check higher-order types, which
 /// are types with arrows in it. Consider the simplest example:
 ///
-/// ```ignore
+/// ```
 /// Assume(Num -> Num, f)
 /// ```
 ///
diff --git a/src/lib.rs b/src/lib.rs
deleted file mode 100644
index 29914569..00000000
--- a/src/lib.rs
+++ /dev/null
@@ -1,18 +0,0 @@
-pub mod cache;
-pub mod error;
-pub mod eval;
-pub mod identifier;
-pub mod label;
-pub mod merge;
-pub mod operation;
-pub mod parser;
-pub mod position;
-pub mod program;
-pub mod repl;
-pub mod serialize;
-pub mod stack;
-pub mod stdlib;
-pub mod term;
-pub mod transformations;
-pub mod typecheck;
-pub mod types;
diff --git a/src/main.rs b/src/main.rs
index 5512b5dc..2d4e45cd 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,12 +1,32 @@
 //! Entry point of the program.
-use nickel::error::{Error, IOError, SerializationError};
-use nickel::program::Program;
-use nickel::term::{RichTerm, Term};
-use nickel::{repl, repl::rustyline_frontend};
-use nickel::{serialize, serialize::ExportFormat};
+mod cache;
+mod error;
+mod eval;
+mod identifier;
+mod label;
+mod merge;
+mod operation;
+mod parser;
+mod position;
+mod program;
+mod repl;
+mod serialize;
+mod stack;
+mod stdlib;
+mod term;
+mod transformations;
+mod typecheck;
+mod types;
+
+use crate::error::{Error, IOError, SerializationError};
+use crate::program::Program;
+use crate::repl::rustyline_frontend;
+use crate::serialize::ExportFormat;
+use crate::term::{RichTerm, Term};
 use std::io::Write;
 use std::path::PathBuf;
-use std::{fs, io, process};
+use std::str::FromStr;
+use std::{fmt, fs, io, process};
 // use std::ffi::OsStr;
 use structopt::StructOpt;
 
@@ -22,6 +42,46 @@ struct Opt {
     command: Option<Command>,
 }
 
+impl std::default::Default for ExportFormat {
+    fn default() -> Self {
+        ExportFormat::Json
+    }
+}
+
+impl fmt::Display for ExportFormat {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match self {
+            Self::Raw => write!(f, "raw"),
+            Self::Json => write!(f, "json"),
+            Self::Yaml => write!(f, "yaml"),
+            Self::Toml => write!(f, "toml"),
+        }
+    }
+}
+
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub struct ParseFormatError(String);
+
+impl fmt::Display for ParseFormatError {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "unsupported export format {}", self.0)
+    }
+}
+
+impl FromStr for ExportFormat {
+    type Err = ParseFormatError;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        match s.to_lowercase().as_ref() {
+            "raw" => Ok(ExportFormat::Raw),
+            "json" => Ok(ExportFormat::Json),
+            "yaml" => Ok(ExportFormat::Yaml),
+            "toml" => Ok(ExportFormat::Toml),
+            _ => Err(ParseFormatError(String::from(s))),
+        }
+    }
+}
+
 /// Available subcommands.
 #[derive(StructOpt, Debug)]
 enum Command {
diff --git a/src/merge.rs b/src/merge.rs
index 25eaecfd..f0df194d 100644
--- a/src/merge.rs
+++ b/src/merge.rs
@@ -99,7 +99,10 @@ pub fn merge(
         // Merge is idempotent on basic terms
         (Term::Bool(b1), Term::Bool(b2)) => {
             if b1 == b2 {
-                Ok(Closure::atomic_closure(Term::Bool(b1).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Bool(b1),
+                    pos_op.into_inherited(),
+                )))
             } else {
                 Err(EvalError::MergeIncompatibleArgs(
                     RichTerm {
@@ -116,7 +119,10 @@ pub fn merge(
         }
         (Term::Num(n1), Term::Num(n2)) => {
             if (n1 - n2).abs() < f64::EPSILON {
-                Ok(Closure::atomic_closure(Term::Num(n1).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Num(n1),
+                    pos_op.into_inherited(),
+                )))
             } else {
                 Err(EvalError::MergeIncompatibleArgs(
                     RichTerm {
@@ -133,7 +139,10 @@ pub fn merge(
         }
         (Term::Str(s1), Term::Str(s2)) => {
             if s1 == s2 {
-                Ok(Closure::atomic_closure(Term::Str(s1).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Str(s1),
+                    pos_op.into_inherited(),
+                )))
             } else {
                 Err(EvalError::MergeIncompatibleArgs(
                     RichTerm {
@@ -150,7 +159,10 @@ pub fn merge(
         }
         (Term::Lbl(l1), Term::Lbl(l2)) => {
             if l1 == l2 {
-                Ok(Closure::atomic_closure(Term::Lbl(l1).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Lbl(l1),
+                    pos_op.into_inherited(),
+                )))
             } else {
                 Err(EvalError::MergeIncompatibleArgs(
                     RichTerm {
@@ -195,7 +207,11 @@ pub fn merge(
                     let mut env = Environment::new();
                     let mut env1_local = env1.clone();
                     let ty_closure = ty.clone().closurize(&mut env1_local, env2.clone());
-                    let t: RichTerm = Term::Assume(ty_closure, lbl.clone(), t).into();
+                    let pos_t = t.pos;
+                    let t = RichTerm::new(
+                        Term::Assume(ty_closure, lbl.clone(), t),
+                        pos_t.into_inherited(),
+                    );
                     (Some(t.closurize(&mut env, env1_local)), env)
                 }
                 (value1, _) => (value1, env1.clone()),
@@ -207,7 +223,11 @@ pub fn merge(
                     let mut env = Environment::new();
                     let mut env2_local = env2.clone();
                     let ty_closure = ty.clone().closurize(&mut env2_local, env1.clone());
-                    let t: RichTerm = Term::Assume(ty_closure, lbl.clone(), t).into();
+                    let pos_t = t.pos;
+                    let t = RichTerm::new(
+                        Term::Assume(ty_closure, lbl.clone(), t),
+                        pos_t.into_inherited(),
+                    );
                     (Some(t.closurize(&mut env, env2_local)), env)
                 }
                 (value2, _) => (value2, env2.clone()),
@@ -242,7 +262,7 @@ pub fn merge(
             };
 
             Ok(Closure {
-                body: Term::MetaValue(meta).into(),
+                body: RichTerm::new(Term::MetaValue(meta), pos_op.into_inherited()),
                 env,
             })
         }
@@ -274,7 +294,7 @@ pub fn merge(
             }
 
             Ok(Closure {
-                body: Term::Record(m).into(),
+                body: RichTerm::new(Term::Record(m), pos_op.into_inherited()),
                 env,
             })
         }
@@ -328,12 +348,11 @@ fn merge_closurize(
     env2: Environment,
 ) -> RichTerm {
     let mut local_env = HashMap::new();
-    let body: RichTerm = Term::Op2(
+    let body = RichTerm::from(Term::Op2(
         BinaryOp::Merge(),
         t1.closurize(&mut local_env, env1),
         t2.closurize(&mut local_env, env2),
-    )
-    .into();
+    ));
     body.closurize(env, local_env)
 }
 
diff --git a/src/operation.rs b/src/operation.rs
index 4116f115..3f67ece4 100644
--- a/src/operation.rs
+++ b/src/operation.rs
@@ -21,7 +21,6 @@ use crate::{mk_app, mk_fun};
 use crate::{serialize, serialize::ExportFormat};
 use md5::digest::Digest;
 use simple_counter::*;
-use std::collections::HashMap;
 use std::iter::Extend;
 
 generate_counter!(FreshVariableCounter, usize);
@@ -117,6 +116,8 @@ fn process_unary_operation(
         body: RichTerm { term: t, pos },
         mut env,
     } = clos;
+    let pos_op_inh = pos_op.into_inherited();
+
     match u_op {
         UnaryOp::Ite() => {
             if let Term::Bool(b) = *t {
@@ -137,47 +138,30 @@ fn process_unary_operation(
                 ))
             }
         }
-        UnaryOp::IsNum() => {
-            if let Term::Num(_) = *t {
-                Ok(Closure::atomic_closure(Term::Bool(true).into()))
-            } else {
-                Ok(Closure::atomic_closure(Term::Bool(false).into()))
-            }
-        }
-        UnaryOp::IsBool() => {
-            if let Term::Bool(_) = *t {
-                Ok(Closure::atomic_closure(Term::Bool(true).into()))
-            } else {
-                Ok(Closure::atomic_closure(Term::Bool(false).into()))
-            }
-        }
-        UnaryOp::IsStr() => {
-            if let Term::Str(_) = *t {
-                Ok(Closure::atomic_closure(Term::Bool(true).into()))
-            } else {
-                Ok(Closure::atomic_closure(Term::Bool(false).into()))
-            }
-        }
-        UnaryOp::IsFun() => {
-            if let Term::Fun(_, _) = *t {
-                Ok(Closure::atomic_closure(Term::Bool(true).into()))
-            } else {
-                Ok(Closure::atomic_closure(Term::Bool(false).into()))
-            }
-        }
-        UnaryOp::IsList() => {
-            if let Term::List(_) = *t {
-                Ok(Closure::atomic_closure(Term::Bool(true).into()))
-            } else {
-                Ok(Closure::atomic_closure(Term::Bool(false).into()))
-            }
-        }
-        UnaryOp::IsRecord() => match *t {
-            Term::Record(_) | Term::RecRecord(_) => {
-                Ok(Closure::atomic_closure(Term::Bool(true).into()))
-            }
-            _ => Ok(Closure::atomic_closure(Term::Bool(false).into())),
-        },
+        UnaryOp::IsNum() => Ok(Closure::atomic_closure(RichTerm::new(
+            Term::Bool(matches!(*t, Term::Num(..))),
+            pos_op_inh,
+        ))),
+        UnaryOp::IsBool() => Ok(Closure::atomic_closure(RichTerm::new(
+            Term::Bool(matches!(*t, Term::Bool(..))),
+            pos_op_inh,
+        ))),
+        UnaryOp::IsStr() => Ok(Closure::atomic_closure(RichTerm::new(
+            Term::Bool(matches!(*t, Term::Str(..))),
+            pos_op_inh,
+        ))),
+        UnaryOp::IsFun() => Ok(Closure::atomic_closure(RichTerm::new(
+            Term::Bool(matches!(*t, Term::Fun(..))),
+            pos_op_inh,
+        ))),
+        UnaryOp::IsList() => Ok(Closure::atomic_closure(RichTerm::new(
+            Term::Bool(matches!(*t, Term::List(..))),
+            pos_op_inh,
+        ))),
+        UnaryOp::IsRecord() => Ok(Closure::atomic_closure(RichTerm::new(
+            Term::Bool(matches!(*t, Term::Record(..) | Term::RecRecord(..))),
+            pos_op_inh,
+        ))),
         UnaryOp::BoolAnd() =>
         // The syntax should not allow partially applied boolean operators.
         {
@@ -189,7 +173,9 @@ fn process_unary_operation(
                     // efficient, but can make debugging harder. In any case, it should be solved
                     // only once primary operators have better support for laziness in some
                     // arguments.
-                    b @ Term::Bool(false) => Ok(Closure::atomic_closure(b.into())),
+                    b @ Term::Bool(false) => {
+                        Ok(Closure::atomic_closure(RichTerm::new(b, pos_op_inh)))
+                    }
                     _ => Err(EvalError::TypeError(
                         String::from("Bool"),
                         String::from("&&"),
@@ -204,7 +190,9 @@ fn process_unary_operation(
         UnaryOp::BoolOr() => {
             if let Some((next, _)) = stack.pop_arg() {
                 match *t {
-                    b @ Term::Bool(true) => Ok(Closure::atomic_closure(b.into())),
+                    b @ Term::Bool(true) => {
+                        Ok(Closure::atomic_closure(RichTerm::new(b, pos_op_inh)))
+                    }
                     // FIXME: this does not check that the second argument is actually a boolean.
                     // This means `false || 2` silently evaluates to `2`. This is simpler and more
                     // efficient, but can make debugging harder. In any case, it should be solved
@@ -224,7 +212,10 @@ fn process_unary_operation(
         }
         UnaryOp::BoolNot() => {
             if let Term::Bool(b) = *t {
-                Ok(Closure::atomic_closure(Term::Bool(!b).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Bool(!b),
+                    pos_op_inh,
+                )))
             } else {
                 Err(EvalError::TypeError(
                     String::from("Bool"),
@@ -248,7 +239,7 @@ fn process_unary_operation(
         }
         UnaryOp::Embed(_id) => {
             if let en @ Term::Enum(_) = *t {
-                Ok(Closure::atomic_closure(en.into()))
+                Ok(Closure::atomic_closure(RichTerm::new(en, pos_op_inh)))
             } else {
                 Err(EvalError::TypeError(
                     String::from("Enum"),
@@ -317,7 +308,10 @@ fn process_unary_operation(
         UnaryOp::ChangePolarity() => {
             if let Term::Lbl(mut l) = *t {
                 l.polarity = !l.polarity;
-                Ok(Closure::atomic_closure(Term::Lbl(l).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Lbl(l),
+                    pos_op_inh,
+                )))
             } else {
                 Err(EvalError::TypeError(
                     String::from("Label"),
@@ -329,7 +323,10 @@ fn process_unary_operation(
         }
         UnaryOp::Pol() => {
             if let Term::Lbl(l) = *t {
-                Ok(Closure::atomic_closure(Term::Bool(l.polarity).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Bool(l.polarity),
+                    pos_op_inh,
+                )))
             } else {
                 Err(EvalError::TypeError(
                     String::from("Label"),
@@ -342,7 +339,10 @@ fn process_unary_operation(
         UnaryOp::GoDom() => {
             if let Term::Lbl(mut l) = *t {
                 l.path.push(ty_path::Elem::Domain);
-                Ok(Closure::atomic_closure(Term::Lbl(l).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Lbl(l),
+                    pos_op_inh,
+                )))
             } else {
                 Err(EvalError::TypeError(
                     String::from("Label"),
@@ -355,7 +355,10 @@ fn process_unary_operation(
         UnaryOp::GoCodom() => {
             if let Term::Lbl(mut l) = *t {
                 l.path.push(ty_path::Elem::Codomain);
-                Ok(Closure::atomic_closure(Term::Lbl(l).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Lbl(l),
+                    pos_op_inh,
+                )))
             } else {
                 Err(EvalError::TypeError(
                     String::from("Label"),
@@ -368,7 +371,10 @@ fn process_unary_operation(
         UnaryOp::GoList() => {
             if let Term::Lbl(mut l) = *t {
                 l.path.push(ty_path::Elem::List);
-                Ok(Closure::atomic_closure(Term::Lbl(l).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Lbl(l),
+                    pos_op_inh,
+                )))
             } else {
                 Err(EvalError::TypeError(
                     String::from("Label"),
@@ -380,10 +386,9 @@ fn process_unary_operation(
         }
         UnaryOp::Wrap() => {
             if let Term::Sym(s) = *t {
-                Ok(Closure::atomic_closure(mk_fun!(
-                    "x",
-                    Term::Wrapped(s, mk_term::var("x"))
-                )))
+                Ok(Closure::atomic_closure(
+                    mk_fun!("x", Term::Wrapped(s, mk_term::var("x"))).with_pos(pos_op_inh),
+                ))
             } else {
                 Err(EvalError::TypeError(
                     String::from("Sym"),
@@ -422,7 +427,10 @@ fn process_unary_operation(
                 let mut fields: Vec<String> = map.keys().map(|Ident(id)| id.clone()).collect();
                 fields.sort();
                 let terms = fields.into_iter().map(mk_term::string).collect();
-                Ok(Closure::atomic_closure(Term::List(terms).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::List(terms),
+                    pos_op_inh,
+                )))
             } else {
                 Err(EvalError::TypeError(
                     String::from("Record"),
@@ -447,13 +455,13 @@ fn process_unary_operation(
                 let ts = ts
                     .into_iter()
                     .map(|t| {
-                        RichTerm::from(Term::App(f_as_var.clone(), t))
+                        RichTerm::new(Term::App(f_as_var.clone(), t), pos_op_inh)
                             .closurize(&mut shared_env, env.clone())
                     })
                     .collect();
 
                 Ok(Closure {
-                    body: Term::List(ts).into(),
+                    body: RichTerm::new(Term::List(ts), pos_op_inh),
                     env: shared_env,
                 })
             } else {
@@ -479,16 +487,18 @@ fn process_unary_operation(
                     .into_iter()
                     .map(|e| {
                         let (Ident(s), t) = e;
+                        let pos = t.pos.into_inherited();
                         (
                             Ident(s.clone()),
                             mk_app!(f_as_var.clone(), mk_term::string(s), t)
-                                .closurize(&mut shared_env, env.clone()),
+                                .closurize(&mut shared_env, env.clone())
+                                .with_pos(pos),
                         )
                     })
                     .collect();
 
                 Ok(Closure {
-                    body: Term::Record(rec).into(),
+                    body: RichTerm::new(Term::Record(rec), pos_op_inh),
                     env: shared_env,
                 })
             } else {
@@ -513,16 +523,21 @@ fn process_unary_operation(
             /// evaluation of the argument on the top of the stack.
             ///
             /// Requires its first argument to be non-empty.
-            fn seq_terms<I>(mut terms: I, env: Environment) -> Result<Closure, EvalError>
+            fn seq_terms<I>(
+                mut terms: I,
+                env: Environment,
+                pos_op_inh: TermPos,
+            ) -> Result<Closure, EvalError>
             where
                 I: Iterator<Item = RichTerm>,
             {
                 let first = terms
                     .next()
                     .expect("expected the argument to be a non-empty iterator");
-                let body = terms.fold(mk_term::op1(UnaryOp::DeepSeq(), first), |acc, t| {
-                    mk_app!(mk_term::op1(UnaryOp::DeepSeq(), t), acc)
-                });
+                let body = terms.fold(
+                    mk_term::op1(UnaryOp::DeepSeq(), first).with_pos(pos_op_inh),
+                    |acc, t| mk_app!(mk_term::op1(UnaryOp::DeepSeq(), t), acc).with_pos(pos_op_inh),
+                );
 
                 Ok(Closure { body, env })
             };
@@ -530,9 +545,9 @@ fn process_unary_operation(
             match *t {
                 Term::Record(map) if !map.is_empty() => {
                     let terms = map.into_iter().map(|(_, t)| t);
-                    seq_terms(terms, env)
+                    seq_terms(terms, env, pos_op)
                 }
-                Term::List(ts) if !ts.is_empty() => seq_terms(ts.into_iter(), env),
+                Term::List(ts) if !ts.is_empty() => seq_terms(ts.into_iter(), env, pos_op),
                 _ => {
                     if stack.count_args() >= 1 {
                         let (next, _) = stack.pop_arg().expect("Condition already checked.");
@@ -565,7 +580,7 @@ fn process_unary_operation(
                 let mut ts_it = ts.into_iter();
                 if ts_it.next().is_some() {
                     Ok(Closure {
-                        body: Term::List(ts_it.collect()).into(),
+                        body: RichTerm::new(Term::List(ts_it.collect()), pos_op_inh),
                         env,
                     })
                 } else {
@@ -584,8 +599,8 @@ fn process_unary_operation(
             if let Term::List(ts) = *t {
                 // A num does not have any free variable so we can drop the environment
                 Ok(Closure {
-                    body: Term::Num(ts.len() as f64).into(),
-                    env: HashMap::new(),
+                    body: RichTerm::new(Term::Num(ts.len() as f64), pos_op_inh),
+                    env: Environment::new(),
                 })
             } else {
                 Err(EvalError::TypeError(
@@ -623,20 +638,14 @@ fn process_unary_operation(
                     stack.push_str_acc(acc, indent, env_chunks.clone());
 
                     Ok(Closure {
-                        body: RichTerm {
-                            term: Box::new(Term::Op1(UnaryOp::ChunksConcat(), e)),
-                            pos: pos_op,
-                        },
+                        body: RichTerm::new(Term::Op1(UnaryOp::ChunksConcat(), e), pos_op_inh),
                         env: env_chunks,
                     })
                 } else {
-                    Ok(Closure {
-                        body: RichTerm {
-                            term: Box::new(Term::Str(acc)),
-                            pos: pos_op,
-                        },
-                        env: Environment::new(),
-                    })
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Str(acc),
+                        pos_op_inh,
+                    )))
                 }
             } else {
                 // Since the error halts the evaluation, we don't bother cleaning the stack of the
@@ -679,12 +688,16 @@ fn process_binary_operation(
         },
         env: mut env2,
     } = clos;
+    let pos_op_inh = pos_op.into_inherited();
 
     match b_op {
         BinaryOp::Plus() => {
             if let Term::Num(n1) = *t1 {
                 if let Term::Num(n2) = *t2 {
-                    Ok(Closure::atomic_closure(Term::Num(n1 + n2).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Num(n1 + n2),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Num"),
@@ -711,7 +724,10 @@ fn process_binary_operation(
         BinaryOp::Sub() => {
             if let Term::Num(n1) = *t1 {
                 if let Term::Num(n2) = *t2 {
-                    Ok(Closure::atomic_closure(Term::Num(n1 - n2).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Num(n1 - n2),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Num"),
@@ -738,7 +754,10 @@ fn process_binary_operation(
         BinaryOp::Mult() => {
             if let Term::Num(n1) = *t1 {
                 if let Term::Num(n2) = *t2 {
-                    Ok(Closure::atomic_closure(Term::Num(n1 * n2).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Num(n1 * n2),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Num"),
@@ -768,7 +787,10 @@ fn process_binary_operation(
                     if n2 == 0.0 {
                         Err(EvalError::Other(String::from("division by zero"), pos_op))
                     } else {
-                        Ok(Closure::atomic_closure(Term::Num(n1 / n2).into()))
+                        Ok(Closure::atomic_closure(RichTerm::new(
+                            Term::Num(n1 / n2),
+                            pos_op_inh,
+                        )))
                     }
                 } else {
                     Err(EvalError::TypeError(
@@ -796,7 +818,10 @@ fn process_binary_operation(
         BinaryOp::Modulo() => {
             if let Term::Num(n1) = *t1 {
                 if let Term::Num(n2) = *t2 {
-                    Ok(Closure::atomic_closure(Term::Num(n1 % n2).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Num(n1 % n2),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Num"),
@@ -823,7 +848,10 @@ fn process_binary_operation(
         BinaryOp::PlusStr() => {
             if let Term::Str(s1) = *t1 {
                 if let Term::Str(s2) = *t2 {
-                    Ok(Closure::atomic_closure(Term::Str(s1 + &s2).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Str(s1 + &s2),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Str"),
@@ -880,7 +908,10 @@ fn process_binary_operation(
             if let Term::Str(s) = *t1 {
                 if let Term::Lbl(mut l) = *t2 {
                     l.tag = s;
-                    Ok(Closure::atomic_closure(Term::Lbl(l).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Lbl(l),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Label"),
@@ -926,9 +957,15 @@ fn process_binary_operation(
                 EqResult::Bool(b) => match (b, stack.pop_eq()) {
                     (false, _) => {
                         stack.clear_eqs();
-                        Ok(Closure::atomic_closure(Term::Bool(false).into()))
+                        Ok(Closure::atomic_closure(RichTerm::new(
+                            Term::Bool(false),
+                            pos_op_inh,
+                        )))
                     }
-                    (true, None) => Ok(Closure::atomic_closure(Term::Bool(true).into())),
+                    (true, None) => Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Bool(true),
+                        pos_op_inh,
+                    ))),
                     (true, Some((c1, c2))) => {
                         let t1 = c1.body.closurize(&mut env, c1.env);
                         let t2 = c2.body.closurize(&mut env, c2.env);
@@ -952,7 +989,10 @@ fn process_binary_operation(
         BinaryOp::LessThan() => {
             if let Term::Num(n1) = *t1 {
                 if let Term::Num(n2) = *t2 {
-                    Ok(Closure::atomic_closure(Term::Bool(n1 < n2).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Bool(n1 < n2),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Num"),
@@ -979,7 +1019,10 @@ fn process_binary_operation(
         BinaryOp::LessOrEq() => {
             if let Term::Num(n1) = *t1 {
                 if let Term::Num(n2) = *t2 {
-                    Ok(Closure::atomic_closure(Term::Bool(n1 <= n2).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Bool(n1 <= n2),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Num"),
@@ -1006,7 +1049,10 @@ fn process_binary_operation(
         BinaryOp::GreaterThan() => {
             if let Term::Num(n1) = *t1 {
                 if let Term::Num(n2) = *t2 {
-                    Ok(Closure::atomic_closure(Term::Bool(n1 > n2).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Bool(n1 > n2),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Num"),
@@ -1033,7 +1079,10 @@ fn process_binary_operation(
         BinaryOp::GreaterOrEq() => {
             if let Term::Num(n1) = *t1 {
                 if let Term::Num(n2) = *t2 {
-                    Ok(Closure::atomic_closure(Term::Bool(n1 >= n2).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Bool(n1 >= n2),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Num"),
@@ -1061,7 +1110,10 @@ fn process_binary_operation(
             if let Term::Str(field) = *t1 {
                 if let Term::Lbl(mut l) = *t2 {
                     l.path.push(ty_path::Elem::Field(Ident(field)));
-                    Ok(Closure::atomic_closure(Term::Lbl(l).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Lbl(l),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Label"),
@@ -1175,7 +1227,7 @@ fn process_binary_operation(
                             pos_op,
                         )),
                         Some(_) => Ok(Closure {
-                            body: Term::Record(static_map).into(),
+                            body: RichTerm::new(Term::Record(static_map), pos_op_inh),
                             env: env2,
                         }),
                     }
@@ -1205,9 +1257,10 @@ fn process_binary_operation(
         BinaryOp::HasField() => {
             if let Term::Str(id) = *t1 {
                 if let Term::Record(static_map) = *t2 {
-                    Ok(Closure::atomic_closure(
-                        Term::Bool(static_map.contains_key(&Ident(id))).into(),
-                    ))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Bool(static_map.contains_key(&Ident(id))),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Record"),
@@ -1241,7 +1294,7 @@ fn process_binary_operation(
                 ts.extend(ts2.into_iter().map(|t| t.closurize(&mut env, env2.clone())));
 
                 Ok(Closure {
-                    body: Term::List(ts).into(),
+                    body: RichTerm::new(Term::List(ts), pos_op_inh),
                     env,
                 })
             }
@@ -1349,7 +1402,10 @@ fn process_binary_operation(
                         _ => return mk_err_fst(t1),
                     };
 
-                    Ok(Closure::atomic_closure(Term::Str(result).into()))
+                    Ok(Closure::atomic_closure(RichTerm::new(
+                        Term::Str(result),
+                        pos_op_inh,
+                    )))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Str"),
@@ -1410,7 +1466,10 @@ fn process_binary_operation(
                     _ => return mk_err_fst(t1),
                 };
 
-                Ok(Closure::atomic_closure(Term::Str(result).into()))
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Str(result),
+                    pos_op_inh,
+                )))
             } else {
                 mk_err_fst(t1)
             }
@@ -1455,7 +1514,7 @@ fn process_binary_operation(
                         _ => return mk_err_fst(t1),
                     };
 
-                    Ok(Closure::atomic_closure(rt))
+                    Ok(Closure::atomic_closure(rt.with_pos(pos_op_inh)))
                 } else {
                     Err(EvalError::TypeError(
                         String::from("Str"),
@@ -1564,10 +1623,6 @@ mod tests {
     use super::*;
     use crate::eval::{CallStack, Environment};
 
-    fn some_env() -> Environment {
-        HashMap::new()
-    }
-
     #[test]
     fn ite_operation() {
         let cont = OperationCont::Op1(UnaryOp::Ite(), TermPos::None, true);
@@ -1583,7 +1638,7 @@ mod tests {
 
         let mut clos = Closure {
             body: Term::Bool(true).into(),
-            env: some_env(),
+            env: Environment::new(),
         };
 
         stack.push_op_cont(cont, 0, TermPos::None);
@@ -1596,7 +1651,7 @@ mod tests {
             clos,
             Closure {
                 body: Term::Num(46.0).into(),
-                env: some_env()
+                env: Environment::new()
             }
         );
         assert_eq!(0, stack.count_args());
@@ -1608,7 +1663,7 @@ mod tests {
             BinaryOp::Plus(),
             Closure {
                 body: Term::Num(6.0).into(),
-                env: some_env(),
+                env: Environment::new(),
             },
             TermPos::None,
             true,
@@ -1616,7 +1671,7 @@ mod tests {
 
         let mut clos = Closure {
             body: Term::Num(7.0).into(),
-            env: some_env(),
+            env: Environment::new(),
         };
         let mut stack = Stack::new();
         stack.push_op_cont(cont, 0, TermPos::None);
@@ -1629,7 +1684,7 @@ mod tests {
             clos,
             Closure {
                 body: Term::Num(6.0).into(),
-                env: some_env()
+                env: Environment::new()
             }
         );
 
@@ -1640,7 +1695,7 @@ mod tests {
                     BinaryOp::Plus(),
                     Closure {
                         body: Term::Num(7.0).into(),
-                        env: some_env(),
+                        env: Environment::new(),
                     },
                     TermPos::None,
                     TermPos::None,
@@ -1659,7 +1714,7 @@ mod tests {
             BinaryOp::Plus(),
             Closure {
                 body: Term::Num(7.0).into(),
-                env: some_env(),
+                env: Environment::new(),
             },
             TermPos::None,
             TermPos::None,
@@ -1667,7 +1722,7 @@ mod tests {
         );
         let mut clos = Closure {
             body: Term::Num(6.0).into(),
-            env: some_env(),
+            env: Environment::new(),
         };
         let mut stack = Stack::new();
         stack.push_op_cont(cont, 0, TermPos::None);
@@ -1680,7 +1735,7 @@ mod tests {
             clos,
             Closure {
                 body: Term::Num(13.0).into(),
-                env: some_env()
+                env: Environment::new()
             }
         );
     }
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index bd746bfb..ff8ed01c 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -5,7 +5,7 @@
 //! expressions, which is not possible using LALRPOP's generated lexer. To see why, consider the
 //! following string:
 //!
-//! ```ignore
+//! ```
 //! "hello, I have 1 + ${ {a = "40"}.a } + 1 bananas."
 //! ```
 //!
diff --git a/src/program.rs b/src/program.rs
index a7f72b4d..b12e7230 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -8,7 +8,7 @@
 //! Some essential functions required for evaluation, such as builtin contracts, are written in
 //! pure Nickel. Standard library files must be record literals:
 //!
-//! ```ignore
+//! ```
 //! {
 //!     val1 = ...
 //!     val2 = ...
@@ -209,10 +209,12 @@ where
 mod tests {
     use super::*;
     use crate::error::EvalError;
+    use crate::identifier::Ident;
     use crate::parser::{grammar, lexer};
     use crate::position::TermPos;
     use assert_matches::assert_matches;
     use codespan::Files;
+    use serde_json::json;
     use std::io::Cursor;
 
     fn parse(s: &str) -> Option<RichTerm> {
@@ -252,6 +254,62 @@ mod tests {
         p.eval_full()
     }
 
+    /// Assert if a given Nickel expression evaluates to a record, given as a vector of bindings
+    /// Records are lazy, thus we need to force the evaluation of each field. Since `merge`
+    /// replaces subterms with dummy fresh variables, we have to re-evaluate the whole expression
+    /// to verify each field
+    fn assert_eval_to_record(s: &str, res: Vec<(&str, Term)>) {
+        let mut term = eval_string(s);
+
+        //Check that the record does not contain extra keys
+        if let Ok(Term::Record(ref mut m)) = term {
+            for (i, t) in res {
+                m.remove(&Ident::from(i))
+                    .unwrap_or_else(|| panic!(format!("Could not find field {} in result", i)));
+
+                let proj = format!("({}).{}", s, i);
+                if let Ok(proj_res) = eval_string(&proj) {
+                    assert_eq!(proj_res, t);
+                } else {
+                    panic!(format!("evaluation of the projection on {} failed", i));
+                }
+            }
+
+            assert!(m.is_empty());
+        } else if let Err(err) = term {
+            panic!("evaluation failed: {:?}", err);
+        }
+    }
+
+    #[test]
+    fn function_app() {
+        let res = eval_string("(fun h => h) 3");
+
+        assert_eq!(Ok(Term::Num(3.0)), res);
+    }
+
+    #[test]
+    fn let_binding() {
+        let res = eval_string("let f = fun f => fun y => f (f y) in f (fun h => h) 3");
+
+        assert_eq!(Ok(Term::Num(3.0)), res);
+    }
+
+    #[test]
+    fn plus() {
+        let res = eval_string("34 + (if true then 2 else 222)");
+
+        assert_eq!(Ok(Term::Num(36.0)), res);
+    }
+
+    #[test]
+    fn dynamic_if() {
+        let res =
+            eval_string("let g  = fun x => if x then 0 else false in g ((fun x => true) 23 )");
+
+        assert_eq!(Ok(Term::Num(0.0)), res);
+    }
+
     #[test]
     fn parse_error() {
         let res = eval_string("let g  = funky x => x in g true");
@@ -268,6 +326,43 @@ mod tests {
         assert_eq!(Ok(Term::Bool(true)), res);
     }
 
+    #[test]
+    fn fixpoint() {
+        let res = eval_string(
+            "let Y = (fun f => (fun x => f (x x)) (fun x => f (x x))) in
+let g = Y (fun g => (fun x => if x  then (g false) else 4)) in
+g true",
+        );
+
+        assert_eq!(Ok(Term::Num(4.)), res);
+    }
+
+    #[test]
+    fn type_contracts() {
+        let res = eval_string(
+            "let safePlus : Num -> Num -> Num = fun x => fun y => x + y in
+            safePlus (54 : Num) (6 : Num)",
+        );
+
+        assert_eq!(Ok(Term::Num(60.)), res);
+    }
+
+    #[test]
+    fn fibonacci() {
+        let res = eval_string(
+            "let Y = Assume(((Num -> Num) -> Num -> Num) -> Num -> Num, fun f => (fun x => f (x x)) (fun x => f (x x))) in
+            let dec : Num -> Num = fun x => x + (-1) in
+            let or : Bool -> Bool -> Bool = fun x => fun y => if x then x else y in
+
+            let fibo : Num -> Num = Y (fun fibo =>
+                (fun x => if or (x == 0) (dec x == 0) then 1 else (fibo (dec x)) + (fibo (dec (dec x))))) in
+            let val : Num = 4 in
+            fibo val",
+        );
+
+        assert_eq!(Ok(Term::Num(5.)), res);
+    }
+
     #[test]
     fn promise_fail() {
         let res = eval_string("let bool = fun l t => if isBool t then t else blame l in 5 : Bool");
@@ -290,6 +385,33 @@ Assume(#alwaysTrue, false)
         }
     }
 
+    #[test]
+    fn flat_higher_order_contract() {
+        let res = eval_string(
+            "let alwaysTrue = fun l t =>
+              let boolT = Assume(Bool, t) in
+              if boolT then boolT else %blame% l
+            in
+            let alwaysFalse = fun l t =>
+              let boolT = Assume(Bool, t) in
+              if boolT then %blame% l else boolT
+            in
+            let not = fun b => if b then false else true in
+            Assume(#alwaysTrue -> #alwaysFalse, not ) true",
+        );
+
+        assert_eq!(Ok(Term::Bool(false)), res);
+    }
+
+    #[test]
+    fn safe_id() {
+        let res = eval_string(
+            "let id = Assume(forall a. a -> a, fun x => x) in
+            id false",
+        );
+        assert_eq!(Ok(Term::Bool(false)), res);
+    }
+
     #[test]
     fn id_fail() {
         let res = eval_string(
@@ -301,19 +423,77 @@ Assume(#alwaysTrue, false)
         }
     }
 
+    #[test]
+    fn safe_higher_order() {
+        let res = eval_string(
+            "let to_bool = Assume(forall a. (a -> Bool) -> a -> Bool,
+            fun f => fun x => f x) in
+            to_bool (fun x => true) 4 ",
+        );
+        assert_eq!(Ok(Term::Bool(true)), res);
+    }
+
+    #[test]
+    fn apply_twice() {
+        let res = eval_string(
+            "let twice = Assume(forall a. (a -> a) -> a -> a,
+            fun f => fun x => f (f x)) in
+            twice (fun x => x + 1) 3",
+        );
+        assert_eq!(Ok(Term::Num(5.)), res);
+    }
+
+    #[test]
+    fn string_contracts() {
+        let res = eval_string("Assume(Str, \"hello\")");
+        assert_eq!(res, Ok(Term::Str("hello".to_string())));
+
+        let res = eval_string("Assume(Str, \"hello\" ++ \" world!\")");
+        assert_eq!(res, Ok(Term::Str("hello world!".to_string())));
+    }
+
     #[test]
     fn enum_simple() {
+        let res = eval_string("`foo : <foo, bar>");
+        assert_eq!(res, Ok(Term::Enum(Ident("foo".to_string()))));
+
+        let res = eval_string("`bar : forall r. <foo, bar | r>");
+        assert_eq!(res, Ok(Term::Enum(Ident("bar".to_string()))));
+
         eval_string("`far : <foo, bar>").unwrap_err();
     }
 
     #[test]
     fn enum_complex() {
+        let res = eval_string(
+            "let f : forall r. <foo, bar | r> -> Num =
+            fun x => switch { foo => 1, bar => 2, _ => 3, } x in
+            f `bar",
+        );
+        assert_eq!(res, Ok(Term::Num(2.)));
+
+        let res = eval_string(
+            "let f : forall r. <foo, bar | r> -> Num =
+            fun x => switch { foo => 1, bar => 2, _ => 3, } x in
+            f `boo",
+        );
+        assert_eq!(res, Ok(Term::Num(3.)));
+
         eval_string(
             "let f : <foo, bar> -> Num =
             fun x => switch { foo => 1, bar => 2, } x in
             f `boo",
         )
         .unwrap_err();
+
+        // This test checks that the terms of a switch are closured
+        assert_eq!(
+            eval_string(
+                "let x = 3 in
+                switch { foo => 1, _ => x, } (3 + 2)"
+            ),
+            Ok(Term::Num(3.))
+        );
     }
 
     #[test]
@@ -323,15 +503,132 @@ Assume(#alwaysTrue, false)
 
     #[test]
     fn records_accessing() {
-        eval_string("({ $(if false then \"foo\" else \"bar\") = false; bar = true; }).foo")
+        assert_eq!(
+            eval_string("({ foo = 3; bar = true; }).bar"),
+            Ok(Term::Bool(true)),
+        );
+
+        assert_eq!(
+            eval_string("({ \"#{if true then \"foo\" else \"bar\"}\" = false; bar = true; }).foo"),
+            Ok(Term::Bool(false)),
+        );
+
+        assert_eq!(
+            eval_string("({ foo = 3; bar = true; }).\"bar\""),
+            Ok(Term::Bool(true)),
+        );
+
+        assert_eq!(
+            eval_string(
+                "({ \"#{if true then \"foo\" else \"bar\"}\" = false; bar = true; }).\"foo\""
+            ),
+            Ok(Term::Bool(false)),
+        );
+
+        eval_string("({ \"#{if false then \"foo\" else \"bar\"}\" = false; bar = true; }).foo")
             .unwrap_err();
     }
 
+    #[test]
+    fn records_prims() {
+        assert_eq!(
+            eval_string("%hasField% \"foo\" { foo = 1; bar = 2; }"),
+            Ok(Term::Bool(true))
+        );
+        assert_eq!(
+            eval_string("%hasField% \"fop\" { foo = 1; bar = 2; }"),
+            Ok(Term::Bool(false))
+        );
+
+        assert_eq!(
+            eval_string(
+                "(%recordMap% { foo = 1; bar = \"it's lazy\"; } (fun y => fun x => x + 1)).foo"
+            ),
+            Ok(Term::Num(2.)),
+        );
+        assert_eq!(
+            eval_string(
+                "let r = %recordMap%
+                    { foo = 1; bar = \"it's lazy\"; }
+                    (fun y x => if %isNum% x then x + 1 else 0)
+                in
+                (r.foo) + (r.bar)"
+            ),
+            Ok(Term::Num(2.)),
+        );
+
+        assert_eq!(
+            eval_string("%hasField% \"foo\" ( { foo = 2; bar = 3; }-$(\"foo\"))"),
+            Ok(Term::Bool(false))
+        );
+
+        assert_eq!(
+            eval_string("%hasField% \"foo\" ( { bar = 3; }$[\"foo\" = 1])"),
+            Ok(Term::Bool(true))
+        );
+        assert_eq!(
+            eval_string("( { bar = 3; }$[\"foo\" = true]).foo"),
+            Ok(Term::Bool(true))
+        );
+    }
+
+    /// This currently do not check that subexpressions are actually forced,
+    /// just that the evaluation succeeds
+    #[test]
+    fn seq_expressions() {
+        assert_eq!(eval_string("%seq% 1 true"), Ok(Term::Bool(true)));
+        assert_eq!(
+            eval_string("let x = (1 + 1) in %seq% x x"),
+            Ok(Term::Num(2.0))
+        );
+
+        assert_eq!(
+            eval_string("let r = {a=(1 + 1);} in %deepSeq% r (r.a)"),
+            Ok(Term::Num(2.0))
+        );
+        assert_eq!(
+            eval_string("let r = {a=(1 + 1);b=(\"a\" ++ \"b\");} in %deepSeq% r (r.b)"),
+            Ok(Term::Str(String::from("ab")))
+        );
+        assert_eq!(
+            eval_string("let r = {a={b=(1 + 1);};} in %deepSeq% r ((r.a).b)"),
+            Ok(Term::Num(2.0))
+        );
+
+        assert_eq!(
+            eval_string(
+                "let inj = fun x => {b=(x + 2);} in
+                let cat = fun x => fun y => x ++ y in
+                let r = {a=(inj 1);b=(cat \"a\" \"b\");} in %deepSeq% r ((r.a).b)"
+            ),
+            Ok(Term::Num(3.0))
+        )
+    }
+
     #[test]
     fn lists() {
+        assert_eq!(eval_string("%elemAt% [1,2,3] 1"), Ok(Term::Num(2.0)));
+        assert_eq!(
+            eval_string("%elemAt% (%map% [1,2,3] (fun x => x + 1)) 1"),
+            Ok(Term::Num(3.0))
+        );
+
         eval_string("%elemAt% [1,2,3] (-1)").unwrap_err();
         eval_string("%elemAt% [1,2,3] 4").unwrap_err();
 
+        assert_eq!(eval_string("%length% []"), Ok(Term::Num(0.0)));
+        assert_eq!(eval_string("%length% [1,2,3]"), Ok(Term::Num(3.0)));
+
+        assert_eq!(
+            eval_string("%length% ([] @ [1,2] @ [3,4] @ [])"),
+            Ok(Term::Num(4.0))
+        );
+        // Test case added after https://github.com/tweag/nickel/issues/154
+        assert_eq!(
+            eval_string("let x = 1 in let l = [x] @ [2] in %head% l"),
+            Ok(Term::Num(1.0))
+        );
+
         assert_eq!(
             eval_string("%head% [\"a\",\"b\",\"c\"]"),
             Ok(Term::Str(String::from("a")))
@@ -343,6 +640,40 @@ Assume(#alwaysTrue, false)
             Ok(Term::Num(2.0))
         );
         eval_string("%tail% []").unwrap_err();
+
+        assert_eq!(
+            eval_string(
+                "let Y = fun f => (fun x => f (x x)) (fun x => f (x x)) in
+                let foldr_ =
+                    fun self => fun f => fun acc => fun l =>
+                        if %length% l == 0 then acc
+                        else
+                            let h = %head% l in
+                            let t = %tail% l in
+                            let next_acc = self f acc t in
+                            f next_acc h
+                in
+                let foldr = Y foldr_ in
+                let and : Bool -> Bool -> Bool =
+                    fun x => fun y =>
+                        if x then
+                            if y then true else false
+                        else false
+                in
+                let all = fun pred => fun l => foldr and true (%map% l pred) in
+                let isZ = fun x => x == 0 in
+                all isZ [0, 0, 0, 1]"
+            ),
+            Ok(Term::Bool(false))
+        );
+    }
+
+    #[test]
+    fn merge_record_simple() {
+        assert_eval_to_record(
+            "{a=1;} & {b=true;}",
+            vec![("a", Term::Num(1.0)), ("b", Term::Bool(true))],
+        );
     }
 
     #[test]
@@ -351,24 +682,123 @@ Assume(#alwaysTrue, false)
         eval_string("({a=1} & {a=2}).a").unwrap();
     }
 
+    #[test]
+    fn merge_record_intersection() {
+        assert_eval_to_record(
+            "{a=1;b=2;} & {b=2;c=3;}",
+            vec![
+                ("a", Term::Num(1.0)),
+                ("b", Term::Num(2.0)),
+                ("c", Term::Num(3.0)),
+            ],
+        );
+    }
+
+    #[test]
+    fn merge_record_nested() {
+        assert_eval_to_record(
+            "({a={b=1;};} & {a={c=true;};}).a ",
+            vec![("b", Term::Num(1.0)), ("c", Term::Bool(true))],
+        );
+    }
+
+    #[test]
+    fn merge_record_complex() {
+        assert_eval_to_record(
+            "let rec1 = {a=false;b=(if true then (1 + 1) else (2 + 0)); c=(((fun x => x) (fun y => y)) 2);} in
+             let rec2 = {b=(((fun x => x) (fun y => y)) 2); c=(if true then (1 + 1) else (2 + 0)); d=true;} in
+             rec1 & rec2",
+             vec![("a", Term::Bool(false)), ("b", Term::Num(2.0)), ("c", Term::Num(2.0)), ("d", Term::Bool(true))]
+         );
+    }
+
+    #[test]
+    fn merge_record_with_env() {
+        assert_eq!(
+            eval_string("((fun y => ((fun x => {a=y}) 1) & ({b=false})) 2).a"),
+            Ok(Term::Num(2.0))
+        );
+    }
+
+    #[test]
+    fn merge_record_with_env_nested() {
+        assert_eq!(
+            eval_string(
+                "let rec = {b={c=10}} & ((fun x => {a=x; b={c=x}}) 10) in
+                         rec.b.c"
+            ),
+            Ok(Term::Num(10.0))
+        );
+    }
+
     #[test]
     #[should_panic]
     fn enriched_terms_contract_default_fail() {
         eval_string("ContractDefault(Num, true)").unwrap();
     }
 
+    #[test]
+    fn enriched_terms_contract_default() {
+        assert_eq!(eval_string("ContractDefault(Num, 10)"), Ok(Term::Num(10.0)));
+    }
+
+    // Check the correct handling of the update of thunks containing enriched values (see issue
+    // https://github.com/tweag/nickel/issues/123)
+    #[test]
+    fn enriched_terms_thunk_update() {
+        assert_eq!(
+            eval_string("let x = {a=(fun x => Default(1)) 1} in %seq% (x.a) ((x & {a=2}).a)"),
+            Ok(Term::Num(2.0))
+        );
+    }
+
     #[test]
     fn merge_default() {
+        assert_eval_to_record(
+            "{a=2;} & {a=Default(0);b=Default(true);}",
+            vec![("a", Term::Num(2.0)), ("b", Term::Bool(true))],
+        );
+
+        assert_eval_to_record(
+            "({a=Default({x=1;});} & {a=Default({y=\"y\";});}).a",
+            vec![("x", Term::Num(1.0)), ("y", Term::Str(String::from("y")))],
+        );
+
         eval_string("({a=Default(1);} & {a=Default(2);}).a").unwrap_err();
     }
 
     #[test]
     fn merge_contract() {
+        assert_eval_to_record(
+            "{a=2;b=Contract(Bool);} & {a=Contract(Num);b=Default(true);}",
+            vec![("a", Term::Num(2.0)), ("b", Term::Bool(true))],
+        );
+
         eval_string("let r = {a=2;} & {a=Contract(Bool)} in r.a").unwrap_err();
     }
 
     #[test]
     fn merge_default_contract() {
+        assert_eval_to_record(
+            "{a=2;} & {a=ContractDefault(Num, 0);b=Default(true)}",
+            vec![("a", Term::Num(2.0)), ("b", Term::Bool(true))],
+        );
+
+        assert_eval_to_record(
+            "{a=2} & {a=Contract(Num)} & {a=Default(3)}",
+            vec![("a", Term::Num(2.0))],
+        );
+
+        assert_eq!(
+            eval_string("({a=2;} & {b=Contract(Num)} & {b=Default(3);}).b"),
+            Ok(Term::Num(3.0)),
+        );
+
+        assert_eq!(
+            eval_string("({a=Default(1)} & {b=Contract(Num)} & {a=Default(1)}).a"),
+            Ok(Term::Num(1.0)),
+        );
+
         eval_string("({a=2;} & {b=Contract(Num)} & {b=Default(true)}).b").unwrap_err();
     }
 
@@ -412,6 +842,9 @@ Assume(#alwaysTrue, false)
 
     #[test]
     fn merge_compose_contract() {
+        assert_eq!(make_composed_contract("6"), Ok(Term::Num(6.0)));
+        assert_eq!(make_composed_contract("12"), Ok(Term::Num(12.0)));
+
         make_composed_contract("1").unwrap_err();
         make_composed_contract("14").unwrap_err();
         make_composed_contract("27").unwrap_err();
@@ -419,21 +852,296 @@ Assume(#alwaysTrue, false)
         make_composed_contract("35").unwrap_err();
     }
 
+    /// Check that the environments of contracts are correctly saved and restored when merging. See
+    /// issue [#117](https://github.com/tweag/nickel/issues/117).
+    #[test]
+    fn merge_contracts_with_env() {
+        let definitions = "
+            let ctr_num = let x = num in {a = Contract(#x)} in
+            let ctr_id = let x = fun l x => x in {a = Contract(#x)} in
+            let val = let x = 1 in {a = x} in
+            let def = let x = 2 in {a = Default(x)} in
+            let def2 = let x = (1 + 1) in {a = Default(x)} in
+            ";
+
+        // Build a term which recursively merges the elements of `elts` in the environment set by
+        // `definitions`, and then access the `a` field
+        let merge_elts = |elts: Vec<&str>| -> Result<Term, Error> {
+            let term = elts.into_iter().fold(String::from("{}"), |term, op| {
+                format!("({}) & ({})", op, term)
+            });
+            eval_string(&format!("{} ({}).a", definitions, term))
+        };
+
+        // contract/contract -> contract/value -> value/default
+        assert_eq!(
+            merge_elts(vec!["ctr_num", "ctr_id", "val", "def"]),
+            Ok(Term::Num(1.0))
+        );
+        // default/value <- value/contract
+        assert_eq!(merge_elts(vec!["def", "val & ctr_num"]), Ok(Term::Num(1.0)));
+        // default/contract-> contract-default/contract-default <- contract/default
+        assert_eq!(
+            merge_elts(vec!["def & ctr_num", "ctr_id & def2"]),
+            Ok(Term::Num(2.0))
+        );
+        // default/contract -> contract-default/contract -> contract-default/value
+        assert_eq!(
+            merge_elts(vec!["def", "ctr_num", "ctr_id", "val"]),
+            Ok(Term::Num(1.0))
+        );
+        // default/contract -> contract-default/default
+        assert_eq!(
+            merge_elts(vec!["def", "ctr_num", "def2"]),
+            Ok(Term::Num(2.0))
+        );
+        // value/contract-default <- contract/contract-default
+        assert_eq!(merge_elts(vec!["val", "ctr_num & def"]), Ok(Term::Num(1.0)));
+    }
+
     #[test]
     fn string_chunks() {
+        fn assert_eval_str(term: &str, result: &str) {
+            assert_eq!(eval_string(term), Ok(Term::Str(String::from(result))));
+        }
+
+        assert_eval_str(
+            r#""simple #{"interp" ++ "olation"} here""#,
+            "simple interpolation here",
+        );
+        assert_eval_str(r##""#{"alone"}""##, "alone");
+        assert_eval_str(
+            r##""nested #{ "#{(fun x => "#{x}") "expression"}" }""##,
+            "nested expression",
+        );
+        assert_eval_str(
+            r##""#{"some"}#{" " ++ "se" ++ "qu"}#{"#{"ence"}"}""##,
+            "some sequence",
+        );
+        assert_eval_str(
+            r##""nested #{ {str = {a = "braces"}.a}.str } !""##,
+            "nested braces !",
+        );
+        assert_eval_str(
+            r##"let x = "world" in "Hello, #{x}! Welcome in #{let y = "universe" in "the #{x}-#{y}"}""##,
+            "Hello, world! Welcome in the world-universe",
+        );
+
         match eval_string(r##""bad type #{1 + 1}""##) {
             Err(Error::EvalError(EvalError::TypeError(_, _, _, _))) => (),
             _ => assert!(false),
         };
     }
 
+    // The chunk concatenation operator directly uses the stack to store its continuation. Check
+    // that it does not mess up the stack.
+    #[test]
+    fn chunks_nested() {
+        // Generate an non-empty evaluation context to evaluate chunks over a non-empty stack
+        let with_context = |t| format!("let force = fun s => s ++ \"\" in force (force ({}))", t);
+
+        fn assert_eval_str(term: &str, result: &str) {
+            assert_eq!(eval_string(term), Ok(Term::Str(String::from(result))));
+        }
+
+        assert_eval_str(
+            &with_context(r##""nested #{ {str = {a = "braces"}.a}.str } !""##),
+            "nested braces !",
+        );
+
+        assert_eval_str(
+            &with_context(
+                r##"let x = "world" in "Hello, #{x}! Welcome in #{let y = "universe" in "the #{x}-#{y}"}""##,
+            ),
+            "Hello, world! Welcome in the world-universe",
+        );
+    }
+
+    #[test]
+    fn recursive_records() {
+        assert_eq!(
+            eval_string("{a = 1; b = a + 1; c = b + a}.c"),
+            Ok(Term::Num(3.0))
+        );
+        assert_eq!(
+            eval_string("{f = fun x y => if x == 0 then y else f (x + (-1)) (y + 1)}.f 5 5"),
+            Ok(Term::Num(10.0))
+        );
+        assert_eq!(
+            eval_string("
+                let with_res = fun res => { f = fun x => if x == 0 then res else g x; g = fun y => f (y + (-1)) }.f 10 in
+                with_res \"done\""),
+            Ok(Term::Str(String::from("done")))
+        );
+    }
+
+    /// Assert that the polymorphic equality between two terms, given as strings, evaluates to the
+    /// term `true`.
+    ///
+    /// This is made as a macro such that a failure points directly at the failing test line.  With
+    /// a standard function, a failing assertion would always point at this function's body,
+    /// instead of the callsite.
+    macro_rules! assert_peq {
+        ($t1:expr, $t2:expr) => {
+            assert_eq!(
+                eval_string(&format!("({}) == ({})", $t1, $t2)),
+                Ok(Term::Bool(true)),
+            );
+        };
+    }
+
+    /// Same as `assert_peq!`, but succeeds if terms are **not** equal.
+    macro_rules! assert_npeq {
+        ($t1:expr, $t2:expr) => {
+            assert_eq!(
+                eval_string(&format!("({}) == ({})", $t1, $t2)),
+                Ok(Term::Bool(false)),
+            );
+        };
+    }
+
+    #[test]
+    fn poly_eq() {
+        assert_peq!("0", "0 + 0 + 0");
+        assert_peq!("true", "if true then true else false");
+        assert_peq!("\"a\" ++ \"b\" ++ \"c\"", "\"#{\"a\" ++ \"b\"}\" ++ \"c\"");
+        assert_peq!("`Less", "`Less");
+        assert_peq!("`small", "`small");
+        assert_peq!("null", "null");
+
+        assert_npeq!("1 + 1", "0");
+        assert_npeq!("true", "if true then false else true");
+        assert_npeq!("\"a\"", "\"a\" ++ \" \"");
+        assert_npeq!("1", "true");
+        assert_npeq!("\"1\"", "1");
+        assert_npeq!("\"true\"", "true");
+        assert_npeq!("`Less", "`small");
+        assert_npeq!("`Less", "0");
+        assert_npeq!("`Greater", "false");
+        assert_npeq!("`Abc", "null");
+        assert_npeq!("0", "null");
+        assert_npeq!("null", "false");
+    }
+
+    #[test]
+    fn poly_eq_lists() {
+        assert_peq!("[]", "[]");
+        assert_peq!("[(1 + 0), (1 + 1), (1 + 1 + 1)]", "[1, 2, 3]");
+        assert_peq!(
+            "[(1 + 0), (\"a\" ++ \"b\"), (if true then true else false)]",
+            "[1, \"ab\", true]"
+        );
+
+        assert_peq!("[[[]]]", "[[[]]]");
+        assert_peq!("[[1], [[2]]]", "[[2 + (-1)], [[1 + 1]]]");
+        assert_peq!("[[true, false]]", "lists.flatten [[[true, false]]]");
+
+        assert_npeq!("[]", "[1]");
+        assert_npeq!("[]", "1");
+        assert_npeq!("[]", "{}");
+        assert_npeq!("[1, \"a\", true]", "[1, \"a\", false]");
+        assert_npeq!("[[true]]", "[[[true]]]");
+    }
+
+    #[test]
+    fn poly_eq_records() {
+        assert_peq!("{}", "{}");
+        assert_peq!("{}$[\"a\" = 1]$[\"b\" = true]", "{a = 1; b = true}");
+        assert_peq!(
+            "{a = 1 + 0; b = 1 + 1; c = 1 + 1 + 1}",
+            "{ a = 1; b = 2; c = 3 }"
+        );
+        assert_peq!(
+            "{ foo = 1 + 0; bar = \"a\" ++ \"b\"; baz = if true then true else false }",
+            "{ foo = 1; bar = \"ab\"; baz = true}"
+        );
+
+        assert_peq!(
+            "{}$[\"a\" = { a = { a = {} } }]",
+            "{ a = { a = { a = {} } } }"
+        );
+        assert_peq!(
+            "{ foo = { bar = 2 + (-1) }; baz = { foo = { bar = 1 + 1 } } }",
+            "{ foo = { bar = 1 }; baz = { foo = { bar = 2 } } }"
+        );
+
+        assert_npeq!("{}", "{a = true}");
+        assert_npeq!("{a = 1}", "{a = 2}");
+        assert_npeq!("{ a = \"a\"; b = true }", "{ a = true; b = \"a\"}");
+        assert_npeq!("{ a = { a = true } }", "{a = { a = { a = true } } }");
+    }
+
+    // Now that the equality operator directly uses the stack to store its continuation (see
+    // https://github.com/tweag/nickel/pull/247), check that it correctly cleans the stack when
+    // evaluating a subequality to `false`.
+    #[test]
+    fn poly_eq_nested() {
+        // Generate an non-empty evaluation context to evaluate equalities over a non-empty stack
+        let with_context = |t1, t2| {
+            format!("let not = fun b => if b then true else false in not (not (not (not (({}) == ({})))))", t1, t2)
+        };
+
+        assert_peq!(
+            with_context(
+                "{a = 1 + 0; b = 1 + 1; c = 0; d = 0}",
+                "{ a = 1; b = 3; c = 0; d = 0}"
+            ),
+            "false"
+        );
+
+        assert_peq!(
+            with_context(
+                "[[1,2,3,4], [1,0,3,4], [1,2,3,4], [1,2,3,4]]",
+                "[[1,2,3,4], [1,2,3,4], [1,2,3,4], [1,2,3,4]]"
+            ),
+            "false"
+        );
+    }
+
+    #[test]
+    fn fields_of() {
+        assert_peq!("%fieldsOf% {}", "[]");
+        assert_peq!("%fieldsOf% {a = 1; b = 2; c = 3}", "[\"a\", \"b\", \"c\"]");
+        assert_peq!("%fieldsOf% {aAa = 1; Zzz = 2;}", "[\"Zzz\", \"aAa\"]");
+        assert_peq!(
+            "%fieldsOf% {foo = {bar = 0}; baz = Default(true)}",
+            "[\"baz\", \"foo\"]"
+        );
+    }
+
     #[test]
     fn arithmetic_expr() {
+        assert_peq!("1+1", "2");
+        assert_peq!("1-2+3-4", "-2");
+        assert_peq!("2-3-4", "-5");
+        assert_peq!("-1-2", "-3");
+        assert_peq!("2*2 + 2*3 - 2*4", "2");
+        assert_peq!("1/2 + 1/4 - 1/8", "0.625");
+        assert_peq!("(10 + 1/4) % 3", "1.25");
+        assert_peq!("10 + 1/4 % 3", "10.25");
+
         eval_string("1 + 1 / (1 - 1)").unwrap_err();
     }
 
     #[test]
     fn comparisons() {
+        assert_peq!("1 < 1", "false");
+        assert_peq!("1 <= 1", "true");
+        assert_peq!("1 > 1", "false");
+        assert_peq!("1 >= 1", "true");
+        assert_peq!("1 + 1/2 > 1 + 1/4", "true");
+        assert_peq!("1 + 1/2 < 1 + 1/4", "false");
+        assert_peq!("1 + 1/2 + 1/8 > 1 + 1/4 + 1/4", "true");
+        assert_peq!("1 + 1/2 + 1/8 < 1 + 1/4 + 1/4", "false");
+        assert_peq!("-1 - 2 < 3 - 10", "false");
+        assert_peq!("-1 - 2 > 3 - 10", "true");
+        assert_peq!("-1*2 > 1*2", "false");
+        assert_peq!("-1*2 < 1*2", "true");
+        assert_peq!("1/4 + 1/4 - 1/4 + 1/4 <= 1/2", "true");
+        assert_peq!("1/4 + 1/4 - 1/4 + 1/4 < 1/2", "false");
+        assert_peq!("1/4 + 1/4 - 1/4 + 1/4 >= 1/2", "true");
+        assert_peq!("1/4 + 1/4 - 1/4 + 1/4 < 1/2", "false");
+
         eval_string("1 < 2 < 3").unwrap_err();
         eval_string("1 < 2 > 3").unwrap_err();
         eval_string("\"a\" < 2").unwrap_err();
@@ -444,6 +1152,34 @@ Assume(#alwaysTrue, false)
 
     #[test]
     fn boolean_op() {
+        assert_peq!("1+1>1 && %isStr% 0", "false");
+        assert_peq!("-1 < -2 && %isFun% (fun x => x)", "false");
+        assert_peq!(
+            "%isNum% 0 && %isFun% (fun x => x) || 1 == 0 && true",
+            "true"
+        );
+        assert_peq!(
+            "%isNum% 0 && %isFun% false || 1 == 0 && false || 1 > 2 && 2 < 1",
+            "false"
+        );
+        assert_peq!(
+            "!(%isNum% true) && !(%isFun% 0) && !(%isBool% \"a\")",
+            "true"
+        );
+        assert_peq!(
+            "!(%isNum% (fun x => x) || %isBool% (fun x => x) || %isFun% (fun x => x))",
+            "false"
+        );
+
+        // Test laziness
+        assert_peq!(
+            "let throw = Assume(#fail, 0) in true || false || throw",
+            "true"
+        );
+        assert_peq!(
+            "let throw = Assume(#fail, 0) in true && false && throw",
+            "false"
+        );
         eval_string("let throw = Assume(#fail, 0) in false || true && throw").unwrap_err();
         eval_string("0 && true").unwrap_err();
         eval_string("\"a\" || false").unwrap_err();
@@ -451,8 +1187,13 @@ Assume(#alwaysTrue, false)
 
     #[test]
     fn records_contracts_simple() {
+        assert_peq!("Assume({}, {})", "{}");
         eval_string("Assume({}, {a=1})").unwrap_err();
 
+        assert_peq!(
+            "let x = Assume({a: Num, s: Str}, {a = 1; s = \"a\"}) in %deepSeq% x x",
+            "{a = 1; s = \"a\"}"
+        );
         eval_string("let x = Assume({a: Num, s: Str}, {a = 1; s = 2}) in %deepSeq% x x")
             .unwrap_err();
         eval_string("let x = Assume({a: Num, s: Str}, {a = \"a\"; s = \"b\"}) in %deepSeq% x x")
@@ -464,6 +1205,10 @@ Assume(#alwaysTrue, false)
         )
         .unwrap_err();
 
+        assert_peq!(
+            "let x = Assume({a: Num, s: {foo: Bool}}, {a = 1; s = { foo = true}}) in %deepSeq% x x",
+            "{a = 1; s = { foo = true}}"
+        );
         eval_string(
             "let x = Assume({a: Num, s: {foo: Bool} }, {a = 1; s = { foo = 2}}) in %deepSeq% x x",
         )
@@ -475,15 +1220,41 @@ Assume(#alwaysTrue, false)
 
     #[test]
     fn records_contracts_poly() {
+        let id = "let f = Assume(forall a. { | a} -> { | a }, fun x => x) in f";
+        let extd =
+            "let f = Assume(forall a. { | a} -> {foo: Num | a}, fun x => x$[\"foo\"=1]) in f";
+        let remv = "let f = Assume(forall a. {foo: Num | a} -> { | a}, fun x => x-$\"foo\") in f";
+
+        assert_peq!(format!("{} {{}}", id), "{}");
+        assert_peq!(format!("{} {{a=1; b=false}}", id), "{a=1; b=false}");
+
+        assert_peq!(format!("{} {{}}", extd), "{foo = 1}");
+        assert_peq!(
+            format!("{} {{bar = false}}", extd),
+            "{foo = 1; bar = false}"
+        );
         // TODO: this test should ultimately pass (i.e., the program should be rejected)
         // but this is not yet the case.
         // eval_string(&format!("{} {{foo = 2}}", extd)).unwrap_err();
 
-        let remv = "let f = Assume(forall a. {foo: Num | a} -> { | a}, fun x => x-$\"foo\") in f";
+        assert_peq!(format!("{} {{foo = 1}}", remv), "{}");
+        assert_peq!(format!("{} {{foo = 1; bar = 1}}", remv), "{bar = 1}");
         eval_string(&format!("{} {{}}", remv)).unwrap_err();
 
-        let bad_cst = "let f = Assume(forall a. { | a} -> { | a}, fun x => {a=1}) in f";
-        let bad_acc = "let f = Assume(forall a. { | a} -> { | a}, fun x => seq (x.a) x) in f";
+        assert_peq!(format!("{} ({} {{}})", remv, extd), "{}");
+        assert_peq!(format!("{} ({} {{foo = 2}})", extd, remv), "{foo = 1}");
+
+        assert_peq!(
+            "
+            let f = Assume(
+                forall a .(forall b. {f: a -> a, arg: a | b} -> a),
+                fun rec => rec.f (rec.arg)) in
+            f { f = fun x => x ++ \" suffix\"; arg = \"blouh\" }",
+            "\"blouh suffix\""
+        );
+
+        let bad_cst = "let f = Assume(forall a. { | a}} -> { | a}, fun x => {a=1}) in f";
+        let bad_acc = "let f = Assume(forall a. { | a}} -> { | a}, fun x => seq (x.a) x) in f";
         let bad_extd =
             "let f = Assume(forall a. { | a} -> {foo: Num | a}, fun x => x-$\"foo\" in f";
         let bad_rmv =
@@ -506,10 +1277,34 @@ Assume(#alwaysTrue, false)
         .unwrap_err();
     }
 
+    #[test]
+    fn records_contracts_dyn() {
+        assert_peq!(
+            "Assume({a: Num, b: Str | Dyn}, {a = 1; b = \"b\"})",
+            "{a = 1; b = \"b\"}"
+        );
+        assert_peq!(
+            "Assume({a: Num, b: Str | Dyn}, {a = 1; b = \"b\"; c = false})",
+            "{a = 1; b = \"b\"; c = false}"
+        );
+        assert_peq!(
+            "Assume({a: Num | Dyn} -> Dyn, fun r => r.b) {a = 1; b = 2}",
+            "2"
+        );
+        eval_string("Assume({a: Num, b: Str | Dyn}, {a = 1})").unwrap_err();
+    }
+
     #[test]
     fn lists_contracts() {
         use crate::label::ty_path::Elem;
 
+        assert_peq!("[1, \"2\", false] | List", "[1, \"2\", false]");
+        assert_peq!("[1, 2, 3] | List Num", "[1, 2, 3]");
+        assert_peq!(
+            "[\"1\", \"2\", \"false\"] | List Str",
+            "[\"1\", \"2\", \"false\"]"
+        );
+
         assert_matches!(
             eval_string("%deepSeq% ([1, \"a\"] | List Num) 0"),
             Err(Error::EvalError(EvalError::BlameError(..)))
@@ -545,6 +1340,146 @@ Assume(#alwaysTrue, false)
         res.unwrap_err().to_diagnostic(&mut files, None);
     }
 
+    #[test]
+    fn multiline_string_indent() {
+        // /!\ Trailing spaces on the first line are on purpose, don't remove ! /!\
+        assert_peq!(
+            r##"  
+                m#"
+                   this
+                       is an
+                       indented
+                   text
+                "#m
+            "##,
+            "\"this\n    is an\n    indented\ntext\""
+        );
+
+        // /!\ Trailing spaces on the first line are on purpose, don't remove ! /!\
+        assert_peq!(
+            r##"  
+                m#"
+                   this
+                       is an
+                       indented
+                   text"#m
+            "##,
+            "\"this\n    is an\n    indented\ntext\""
+        );
+
+        // /!\ Trailing spaces on the middle line are on purpose, don't remove ! /!\
+        assert_peq!(
+            r##"
+                m#"
+                   ignore
+    
+                    empty line indent
+                "#m
+            "##,
+            "\"ignore\n\n empty line indent\""
+        );
+
+        // /!\ Trailing spaces on the middle line are on purpose, don't remove ! /!\
+        assert_peq!(
+            r##"
+                m#"
+    
+                   ignore
+                    first line indent
+                "#m
+            "##,
+            "\"\nignore\n first line indent\""
+        );
+    }
+
+    #[test]
+    fn multiline_string_delimiters() {
+        // Writing multi-line strings inside Rust raw strings, which have the similar delimiters
+        // is, is not really pretty
+        assert_eq!(
+            eval_string(r###"m##""#m"##a"##m"###),
+            Ok(Term::Str(String::from(r###""#m"##a"###))),
+        );
+
+        assert_eq!(
+            eval_string(r####"m###""##m"###a"###m"####),
+            Ok(Term::Str(String::from(r####""##m"###a"####))),
+        );
+    }
+
+    #[test]
+    fn multiline_interpolation() {
+        assert_peq!(
+            r##"m#"Simple #{"interpolated"} string"#m"##,
+            "\"Simple interpolated string\""
+        );
+        assert_peq!(
+            r###"m##"Double ##{"interpolated"} string"##m"###,
+            "\"Double interpolated string\""
+        );
+        assert_peq!(
+            r###"m##"Not #{"interpolated"}"##m"###,
+            "\"Not \\#{\\\"interpolated\\\"}\""
+        );
+        assert_peq!(
+            r####"m###"###{"Triple"} ##{not} #{interpolated}"###m"####,
+            "\"Triple #\\#{not} \\#{interpolated}\""
+        );
+        assert_peq!(
+            r###"m#"#{m##"##{"Not"} #{interpolated}"##m} ##{"string"}"#m"###,
+            "\"Not \\#{interpolated} #\\#{\\\"string\\\"}\""
+        );
+
+        assert_peq!(
+            r###"
+                m#"
+                   #{m#"thi"#m ++ "s"}
+                       #{"is" ++ " an"}
+                       indented
+                   #{"#{m##"te"##m}xt"}
+                "#m
+            "###,
+            "\"this\n    is an\n    indented\ntext\""
+        );
+
+        assert_peq!(
+            r##"
+                let x = "I\n need\n  indent!" in
+                m#"
+                  base
+                    #{x}
+                  #{x}
+                "#m
+            "##,
+            r#""base
+  I
+   need
+    indent!
+I
+ need
+  indent!""#
+        );
+
+        assert_peq!(
+            r##"
+                let x = "ignore\nmy\nindent" in
+                let y = "me\ntoo" in
+                m#"
+                  strip
+                    #{x} #{y}
+                    #{"not\nme"}
+                "#m
+            "##,
+            r#""strip
+  ignore
+my
+indent me
+too
+  not
+  me""#
+        );
+    }
+
     #[test]
     fn evaluation_full() {
         use crate::mk_record;
@@ -607,4 +1542,75 @@ Assume(#alwaysTrue, false)
             Err(Error::EvalError(EvalError::InfiniteRecursion(..)))
         );
     }
+
+    /// Check that `deserialize (serialize term) == term`.
+    macro_rules! assert_ser_inv {
+        ($t:expr) => {
+            assert_peq!(
+                $t,
+                format!(
+                    "%deserialize% `Json (%serialize% `Json (let x = {} in %deepSeq% x x))",
+                    $t
+                )
+            );
+            assert_peq!(
+                $t,
+                format!(
+                    "%deserialize% `Yaml (%serialize% `Yaml (let x = {} in %deepSeq% x x))",
+                    $t
+                )
+            );
+            assert_peq!(
+                $t,
+                format!(
+                    "%deserialize% `Toml (%serialize% `Toml (let x = {} in %deepSeq% x x))",
+                    $t
+                )
+            );
+        };
+    }
+
+    /// Check that `serialize (deserialize s) == s`.
+    macro_rules! assert_deser_inv {
+        ($data:expr) => {
+            let as_str = serde_json::to_string_pretty(&$data).unwrap();
+            assert_peq!(
+                format!("\"{}\"", as_str.replace("\"", "\\\"")),
+                format!(
+                    "%serialize% `Json (%deserialize% `Json m##\"{}\"##m)",
+                    as_str
+                )
+            );
+            let as_str = serde_yaml::to_string(&$data).unwrap();
+            assert_peq!(
+                format!("\"{}\"", as_str.replace("\"", "\\\"")),
+                format!(
+                    "%serialize% `Yaml (%deserialize% `Yaml m##\"{}\"##m)",
+                    as_str
+                )
+            );
+            let as_str = format!("{}", toml::Value::try_from(&$data).unwrap());
+            assert_peq!(
+                format!("\"{}\"", as_str.replace("\"", "\\\"")),
+                format!(
+                    "%serialize% `Toml (%deserialize% `Toml m##\"{}\"##m)",
+                    as_str
+                )
+            );
+        };
+    }
+
+    #[test]
+    fn serialize_builtin_laws() {
+        assert_ser_inv!("{val = 1 + 1}");
+        assert_ser_inv!("{val = \"Some string\"}");
+        assert_ser_inv!("{val = [\"a\", 3, []]}");
+        assert_ser_inv!("{a = {foo = {bar = \"2\"}}; b = false; c = [{d = \"e\"}, {d = \"f\"}]}");
+
+        assert_deser_inv!(json!({"a": 1.0, "b": 4.0, "c": 3.0}));
+        assert_deser_inv!(json!({"a": {"b": {"c": "richtig"}}}));
+        assert_deser_inv!(
+            json!({"foo": 1.0, "bar": ["str", true], "baz": {"subfoo": true, "subbar": 0.0}})
+        );
+    }
 }
diff --git a/src/serialize.rs b/src/serialize.rs
index 84637f32..85c3e831 100644
--- a/src/serialize.rs
+++ b/src/serialize.rs
@@ -5,8 +5,6 @@ use crate::term::{MetaValue, RichTerm, Term};
 use serde::de::{Deserialize, Deserializer};
 use serde::ser::{Error, Serialize, SerializeMap, Serializer};
 use std::collections::HashMap;
-use std::fmt;
-use std::str::FromStr;
 
 /// Available export formats.
 #[derive(Copy, Clone, Eq, PartialEq, Debug)]
@@ -17,46 +15,6 @@ pub enum ExportFormat {
     Toml,
 }
 
-impl std::default::Default for ExportFormat {
-    fn default() -> Self {
-        ExportFormat::Json
-    }
-}
-
-impl fmt::Display for ExportFormat {
-    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        match self {
-            Self::Raw => write!(f, "raw"),
-            Self::Json => write!(f, "json"),
-            Self::Yaml => write!(f, "yaml"),
-            Self::Toml => write!(f, "toml"),
-        }
-    }
-}
-
-#[derive(Clone, Eq, PartialEq, Debug)]
-pub struct ParseFormatError(String);
-
-impl fmt::Display for ParseFormatError {
-    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "unsupported export format {}", self.0)
-    }
-}
-
-impl FromStr for ExportFormat {
-    type Err = ParseFormatError;
-
-    fn from_str(s: &str) -> Result<Self, Self::Err> {
-        match s.to_lowercase().as_ref() {
-            "raw" => Ok(ExportFormat::Raw),
-            "json" => Ok(ExportFormat::Json),
-            "yaml" => Ok(ExportFormat::Yaml),
-            "toml" => Ok(ExportFormat::Toml),
-            _ => Err(ParseFormatError(String::from(s))),
-        }
-    }
-}
-
 /// Serializer for metavalues.
 pub fn serialize_meta_value<S>(meta: &MetaValue, serializer: S) -> Result<S::Ok, S::Error>
 where
diff --git a/src/term.rs b/src/term.rs
index df1df6a0..d8a58437 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -121,7 +121,7 @@ pub enum Term {
     ///
     /// Wrapped terms are introduced by contracts on polymorphic types. Take the following example:
     ///
-    /// ```ignore
+    /// ```
     /// let f = Assume(forall a. forall b. a -> b -> a, fun x y => y) in
     /// f true "a"
     /// ```
@@ -511,7 +511,7 @@ pub enum UnaryOp {
     /// If the argument is a label with a [type path](../label/enum.TyPath.html) representing some
     /// subtype of the type of the original contract, as in:
     ///
-    /// ```ignore
+    /// ```
     /// (Num -> Num) -> Num
     ///  ^^^^^^^^^^ type path
     /// ------------------- original type
@@ -519,7 +519,7 @@ pub enum UnaryOp {
     ///
     /// Then `GoDom` evaluates to a copy of this label, where the path has gone forward into the domain:
     ///
-    /// ```ignore
+    /// ```
     /// (Num -> Num) -> Num
     ///  ^^^ new type path
     /// ------------------- original type
@@ -659,6 +659,12 @@ impl RichTerm {
             .apply_to_rich_terms(|rt: &mut Self| rt.clean_pos());
     }
 
+    /// Set the position, and return the updated term.
+    pub fn with_pos(mut self, pos: TermPos) -> Self {
+        self.pos = pos;
+        self
+    }
+
     /// Apply a transformation on a whole term by mapping a function `f` on each node in a
     /// bottom-up manner. `f` may return a generic error `E` and use the state `S` which is
     /// passed around.
diff --git a/src/transformations.rs b/src/transformations.rs
index 446bb169..5b7773bf 100644
--- a/src/transformations.rs
+++ b/src/transformations.rs
@@ -20,7 +20,7 @@ generate_counter!(FreshVarCounter, usize);
 /// bindings put at the beginning of the WHNF.
 ///
 /// For example, take the expression
-/// ```ignore
+/// ```
 /// let x = {a = (1 + 1);} in x.a + x.a
 /// ```
 ///
@@ -32,7 +32,7 @@ generate_counter!(FreshVarCounter, usize);
 /// of records and the elements of lists - `(1 + 1)` in our example -, with fresh variables
 /// introduced by `let`  added at the head of the term:
 ///
-/// ```ignore
+/// ```
 /// let x = (let var = 1 + 1 in {a = var;}) in x.a + x.a
 /// ```
 ///
@@ -321,7 +321,7 @@ impl Closurizable for RichTerm {
         };
         env.insert(var.clone(), Thunk::new(closure, IdentKind::Record()));
 
-        RichTerm::new(Term::Var(var), pos)
+        RichTerm::new(Term::Var(var), pos.into_inherited())
     }
 }
 
diff --git a/src/typecheck.rs b/src/typecheck.rs
index cca9fbe2..1f28b777 100644
--- a/src/typecheck.rs
+++ b/src/typecheck.rs
@@ -21,7 +21,7 @@
 //! expressions (the type of `bound_exp` in `let x = bound_exp in body`) is inferred in strict
 //! mode, but it is never implicitly generalized. For example, the following program is rejected:
 //!
-//! ```ignore
+//! ```
 //! // Rejected
 //! let id = fun x => x in seq (id "a") (id 5) : Num
 //! ```
@@ -34,7 +34,7 @@
 //! can interact with other parts of type inference. If polymorphism is required, a simple
 //! annotation is sufficient:
 //!
-//! ```ignore
+//! ```
 //! // Accepted
 //! let id : forall a. a -> a = fun x => x in seq (id "a") (id 5) : Num
 //! ```
@@ -1889,6 +1889,7 @@ mod tests {
     use crate::cache::resolvers::{DummyResolver, SimpleResolver};
     use crate::error::ImportError;
     use crate::label::Label;
+    use crate::mk_app;
     use crate::parser::lexer;
     use crate::term::make as mk_term;
     use crate::transformations::transform;
@@ -1910,6 +1911,25 @@ mod tests {
         }
     }
 
+    #[test]
+    fn simple_no_promises() -> Result<(), TypecheckError> {
+        // It's easy to check these will never fail, that's why we keep them all together
+
+        type_check_no_import(&Term::Bool(true).into())?;
+        type_check_no_import(&Term::Num(45.).into())?;
+        type_check_no_import(&mk_term::id())?;
+        type_check_no_import(&mk_term::let_in("x", Term::Num(3.0), mk_term::var("x")))?;
+
+        type_check_no_import(&mk_app!(Term::Num(5.0), Term::Bool(true)))?;
+        type_check_no_import(&mk_term::op2(
+            BinaryOp::Plus(),
+            Term::Num(4.),
+            Term::Bool(false),
+        ))?;
+
+        Ok(())
+    }
+
     #[test]
     fn unbound_variable_always_throws() {
         type_check_no_import(&mk_term::var("x")).unwrap_err();
@@ -1917,6 +1937,15 @@ mod tests {
 
     #[test]
     fn promise_simple_checks() {
+        type_check_no_import(
+            &Term::Promise(
+                Types(AbsType::Bool()),
+                Label::dummy(),
+                Term::Bool(true).into(),
+            )
+            .into(),
+        )
+        .unwrap();
         type_check_no_import(
             &Term::Promise(
                 Types(AbsType::Num()),
@@ -1946,6 +1975,20 @@ mod tests {
         )
         .unwrap_err();
 
+        type_check_no_import(
+            &Term::Promise(
+                Types(AbsType::Num()),
+                Label::dummy(),
+                Term::Assume(
+                    Types(AbsType::Num()),
+                    Label::dummy(),
+                    Term::Bool(true).into(),
+                )
+                .into(),
+            )
+            .into(),
+        )
+        .unwrap();
         type_check_no_import(
             &Term::Promise(
                 Types(AbsType::Num()),
@@ -1961,32 +2004,69 @@ mod tests {
         )
         .unwrap_err();
 
+        parse_and_typecheck("\"hello\" : Str").unwrap();
         parse_and_typecheck("\"hello\" : Num").unwrap_err();
     }
 
     #[test]
     fn promise_complicated() {
         // Inside Promises we typecheck strictly
+        parse_and_typecheck("(fun x => if x then x + 1 else 34) false").unwrap();
         parse_and_typecheck("let f : Bool -> Num = fun x => if x then x + 1 else 34 in f false")
             .unwrap_err();
 
         // not annotated let bindings type to Dyn
+        parse_and_typecheck(
+            "let id : Num -> Num = fun x => x in
+            (id 4 : Num)",
+        )
+        .unwrap();
         parse_and_typecheck(
             "let id = fun x => x in
             (id 4 : Num)",
         )
         .unwrap_err();
 
+        // lambdas don't annotate to Dyn
+        parse_and_typecheck("(fun id => (id 4 : Num)) (fun x => x)").unwrap();
+
         // But they are not polymorphic
         parse_and_typecheck("(fun id => (id 4 : Num) + (id true : Bool)) (fun x => x)")
             .unwrap_err();
 
+        // Non strict zones don't unify
+        parse_and_typecheck("(fun id => (id 4) + (id true: Bool)) (fun x => x)").unwrap();
+
+        // We can typecheck any contract
+        parse_and_typecheck(
+            "let alwaysTrue = fun l t => if t then t else %blame% l in
+            (fun x => x) : #alwaysTrue -> #alwaysTrue",
+        )
+        .unwrap();
         // Only if they're named the same way
         parse_and_typecheck("(fun x => x) : #(fun l t => t) -> #(fun l t => t)").unwrap_err();
     }
 
     #[test]
     fn simple_forall() {
+        parse_and_typecheck(
+            "let f : forall a. a -> a = fun x => x in
+        (if (f true) then (f 2) else 3) : Num",
+        )
+        .unwrap();
+
+        parse_and_typecheck(
+            "let f : forall a. (forall b. a -> b -> a) = fun x y => x in
+            (if (f true 3) then (f 2 false) else 3) : Num",
+        )
+        .unwrap();
+
+        parse_and_typecheck(
+            "let f : forall a. (forall b. b -> b) -> a -> a = fun f x => f x in
+            f (fun z => z : forall y. y -> y)",
+        )
+        .unwrap();
+
         parse_and_typecheck(
             "let f : forall a. (forall b. a -> b -> a) = fun x y => y in
             f",
@@ -2008,20 +2088,62 @@ mod tests {
         .unwrap_err();
     }
 
+    #[test]
+    fn forall_nested() {
+        parse_and_typecheck(
+            "let f : forall a. a -> a = let g = Assume(forall a. (a -> a), fun x => x) in g in
+            (if (f true) then (f 2) else 3) : Num",
+        )
+        .unwrap();
+
+        parse_and_typecheck(
+            "let f : forall a. a -> a = let g = Assume(forall a. (a -> a), fun x => x) in g g in
+            (if (f true) then (f 2) else 3) : Num",
+        )
+        .unwrap();
+
+        parse_and_typecheck(
+            "let f : forall a. a -> a = let g : forall a. (forall b. (b -> (a -> a))) = fun y x => x in g 0 in
+            (if (f true) then (f 2) else 3) : Num",
+        )
+        .unwrap();
+    }
+
     #[test]
     fn enum_simple() {
+        parse_and_typecheck("`bla : <bla>").unwrap();
         parse_and_typecheck("`blo : <bla>").unwrap_err();
+
+        parse_and_typecheck("`blo : <bla, blo>").unwrap();
+        parse_and_typecheck("`bla : forall r. <bla | r>").unwrap();
+        parse_and_typecheck("`bla : forall r. <bla, blo | r>").unwrap();
+
+        parse_and_typecheck("(switch { bla => 3, } `bla) : Num").unwrap();
         parse_and_typecheck("(switch { bla => 3, } `blo) : Num").unwrap_err();
+
+        parse_and_typecheck("(switch { bla => 3, _ => 2, } `blo) : Num").unwrap();
         parse_and_typecheck("(switch { bla => 3, ble => true, } `bla) : Num").unwrap_err();
     }
 
     #[test]
     fn enum_complex() {
+        parse_and_typecheck("(fun x => switch {bla => 1, ble => 2,} x) : <bla, ble> -> Num")
+            .unwrap();
         parse_and_typecheck(
             "(fun x => switch {bla => 1, ble => 2, bli => 4,} x) : <bla, ble> -> Num",
         )
         .unwrap_err();
+        parse_and_typecheck(
+            "(fun x => switch {bla => 1, ble => 2, bli => 4,} (%embed% bli x)) : <bla, ble> -> Num",
+        )
+        .unwrap();
 
+        parse_and_typecheck(
+            "(fun x =>
+                (switch {bla => 3, bli => 2,} x) +
+                (switch {bli => 6, bla => 20,} x) ) `bla : Num",
+        )
+        .unwrap();
         // TODO typecheck this, I'm not sure how to do it with row variables
         parse_and_typecheck(
             "(fun x =>
@@ -2030,6 +2152,12 @@ mod tests {
         )
         .unwrap_err();
 
+        parse_and_typecheck(
+            "let f : forall r. <blo, ble | r> -> Num =
+            fun x => (switch {blo => 1, ble => 2, _ => 3, } x) in
+            f `bli : Num",
+        )
+        .unwrap();
         parse_and_typecheck(
             "let f : forall r. <blo, ble, | r> -> Num =
                 fun x => (switch {blo => 1, ble => 2, bli => 3, } x) in
@@ -2037,6 +2165,12 @@ mod tests {
         )
         .unwrap_err();
 
+        parse_and_typecheck(
+            "let f : forall r. (forall p. <blo, ble | r> -> <bla, bli | p>) =
+                fun x => (switch {blo => `bla, ble => `bli, _ => `bla, } x) in
+            f `bli",
+        )
+        .unwrap();
         parse_and_typecheck(
             "let f : forall r. (forall p. <blo, ble | r> -> <bla, bli | p>) =
                 fun x => (switch {blo => `bla, ble => `bli, _ => `blo, } x) in
@@ -2047,11 +2181,34 @@ mod tests {
 
     #[test]
     fn static_record_simple() {
+        parse_and_typecheck("{bla = 1} : {bla : Num}").unwrap();
         parse_and_typecheck("{bla = true} : {bla : Num}").unwrap_err();
         parse_and_typecheck("{blo = 1} : {bla : Num}").unwrap_err();
 
+        parse_and_typecheck("{blo = true; bla = 1} : {bla : Num, blo : Bool}").unwrap();
+
+        parse_and_typecheck("{blo = 1}.blo : Num").unwrap();
+        parse_and_typecheck("{bla = true; blo = 1}.blo : Num").unwrap();
         parse_and_typecheck("{blo = 1}.blo : Bool").unwrap_err();
 
+        parse_and_typecheck(
+            "let r : {bla : Bool, blo : Num} = {blo = 1; bla = true; } in
+            (if r.bla then r.blo else 2) : Num",
+        )
+        .unwrap();
+
+        // It worked at first try :O
+        parse_and_typecheck(
+            "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
+                fun r => if r.bla then r.blo else r.ble
+            in
+            (if (f {bla = true; blo = false; ble = true; blip = 1; }) then
+                (f {bla = true; blo = 1; ble = 2; blip = `blip; })
+            else
+                (f {bla = true; blo = 3; ble = 4; bloppo = `bloppop; })) : Num",
+        )
+        .unwrap();
+
         parse_and_typecheck(
             "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
                 fun r => if r.bla then r.blo else r.ble
@@ -2070,14 +2227,36 @@ mod tests {
 
     #[test]
     fn dynamic_record_simple() {
+        parse_and_typecheck("{ \"#{if true then \"foo\" else \"bar\"}\" = 2; } : {_ : Num}")
+            .unwrap();
+
+        parse_and_typecheck("({ \"#{if true then \"foo\" else \"bar\"}\" = 2; }.\"bla\") : Num")
+            .unwrap();
+
         parse_and_typecheck(
             "({ \"#{if true then \"foo\" else \"bar\"}\" = 2; \"foo\" = true; }.\"bla\") : Num",
         )
         .unwrap_err();
+
+        parse_and_typecheck("{ foo = 3; bar = 4; } : {_ : Num}").unwrap();
+    }
+
+    #[test]
+    fn seq() {
+        parse_and_typecheck("%seq% false 1 : Num").unwrap();
+        parse_and_typecheck("(fun x y => %seq% x y) : forall a. (forall b. a -> b -> b)").unwrap();
+        parse_and_typecheck("let xDyn = if false then true else false in let yDyn = 1 + 1 in (%seq% xDyn yDyn : Dyn)").unwrap();
     }
 
     #[test]
     fn simple_list() {
+        parse_and_typecheck("[1, \"2\", false]").unwrap();
+        //TODO: the type system may accept the following test at some point.
+        // parse_and_typecheck("[1, \"2\", false] : List").unwrap();
+        parse_and_typecheck("[\"a\", \"b\", \"c\"] : List Str").unwrap();
+        parse_and_typecheck("[1, 2, 3] : List Num").unwrap();
+        parse_and_typecheck("fun x => [x] : forall a. a -> List a").unwrap();
+
         parse_and_typecheck("[1, 2, false] : List Num").unwrap_err();
         parse_and_typecheck("[(1 : String), true, \"b\"] : List").unwrap_err();
         parse_and_typecheck("[1, 2, \"3\"] : List Str").unwrap_err();
@@ -2085,6 +2264,14 @@ mod tests {
 
     #[test]
     fn lists_operations() {
+        parse_and_typecheck("fun l => %tail% l : forall a. List a -> List a").unwrap();
+        parse_and_typecheck("fun l => %head% l : forall a. List a -> a").unwrap();
+        parse_and_typecheck("fun f l => %map% l f : forall a b. (a -> b) -> List a -> List b")
+            .unwrap();
+        parse_and_typecheck("(fun l1 => fun l2 => l1 @ l2) : forall a. List a -> List a -> List a")
+            .unwrap();
+        parse_and_typecheck("(fun i l => %elemAt% l i) : forall a. Num -> List a -> a").unwrap();
+
         parse_and_typecheck("(fun l => %head% l) : forall a b. (List a -> b)").unwrap_err();
         parse_and_typecheck(
             "(fun f l => %elemAt% (%map% l f) 0) : forall a. (forall b. (a -> b) -> List -> b)",
@@ -2128,16 +2315,24 @@ mod tests {
 
     #[test]
     fn recursive_records() {
+        parse_and_typecheck("{a : Num = 1; b = a + 1} : {a : Num, b : Num}").unwrap();
         parse_and_typecheck("{a : Num = true; b = a + 1} : {a : Num, b : Num}").unwrap_err();
         parse_and_typecheck("{a = 1; b : Bool = a} : {a : Num, b : Bool}").unwrap_err();
+        parse_and_typecheck("{a : Num = 1 + a} : {a : Num}").unwrap();
     }
 
     #[test]
     fn let_inference() {
+        parse_and_typecheck("(let x = 1 + 2 in let f = fun x => x + 1 in f x) : Num").unwrap();
         parse_and_typecheck("(let x = 1 + 2 in let f = fun x => x ++ \"a\" in f x) : Num")
             .unwrap_err();
 
         // Fields in recursive records are treated in the type environment in the same way as let-bound expressions
+        parse_and_typecheck("{a = 1; b = 1 + a} : {a : Num, b : Num}").unwrap();
+        parse_and_typecheck(
+            "{ f = fun x => if x == 0 then 1 else 1 + (f (x + (-1)));} : {f : Num -> Num}",
+        )
+        .unwrap();
         parse_and_typecheck(
             "{ f = fun x => if x == 0 then false else 1 + (f (x + (-1)))} : {f : Num -> Num}",
         )
@@ -2171,6 +2366,12 @@ mod tests {
         );
         assert_row_conflict(res);
 
+        parse_and_typecheck(
+            "let extend = Assume(forall c. { | c} -> {a: Str | c}, 0) in
+           let remove = Assume(forall c. {a: Str | c} -> { | c}, 0) in
+           (let good = remove (extend {}) in 0) : Num",
+        )
+        .unwrap();
         res = parse_and_typecheck(
             "let remove = Assume(forall c. {a: Str | c} -> { | c}, 0) in
            (let bad = remove (remove {a = \"a\"}) in 0) : Num",
@@ -2180,6 +2381,9 @@ mod tests {
 
     #[test]
     fn dynamic_row_tail() {
+        parse_and_typecheck("let r = Assume({a: Num | Dyn}, {a = 1; b = 2}) in (r.a : Num)")
+            .unwrap();
+        parse_and_typecheck("Assume({a: Num | Dyn}, {a = 1; b = 2}) : {a: Num | Dyn}").unwrap();
         // Currently, typechecking is conservative wrt the dynamic row type, meaning it can't to a
         // less precise type with a dynamic tail.
         parse_and_typecheck("{a = 1; b = 2} : {a: Num | Dyn}").unwrap_err();
@@ -2188,12 +2392,28 @@ mod tests {
         parse_and_typecheck("{a = 1} : {a: Num | Dyn}").unwrap_err();
     }
 
+    /// Regression test following [#270](https://github.com/tweag/nickel/issues/270). Check that
+    /// unifying a variable with itself doesn't introduce a loop. The failure of this test results
+    /// in a stack overflow.
+    #[test]
+    fn unification_graph_cycle() {
+        parse_and_typecheck("{gen_ = fun acc x => if x == 0 then acc else gen_ (acc @ [x]) (x - 1)}.gen_ : List Num -> Num -> List Num").unwrap();
+        parse_and_typecheck("{f = fun x => f x}.f : forall a. a -> a").unwrap();
+    }
+
     #[test]
     fn shallow_type_inference() {
+        parse_and_typecheck("let x = 1 in (x + 1 : Num)").unwrap();
         assert_matches!(
             parse_and_typecheck("let x = (1 + 1) in (x + 1 : Num)"),
             Err(TypecheckError::TypeMismatch(..))
         );
+
+        parse_and_typecheck("let x = \"a\" in (x ++ \"a\" : Str)").unwrap();
+        parse_and_typecheck("let x = \"a#{\"some str inside\"}\" in (x ++ \"a\" : Str)").unwrap();
+
+        parse_and_typecheck("let x = false in (x || true : Bool)").unwrap();
+        parse_and_typecheck("let x = false in let y = x in let z = y in (z : Bool)").unwrap();
     }
 
     /// Regression test following, see [#297](https://github.com/tweag/nickel/pull/297). Check that
diff --git a/src/types.rs b/src/types.rs
index cb22ce71..285252b8 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -25,7 +25,7 @@
 //! can be abstracted over, leaving the row open for future extension. A simple and demonstrative
 //! example is field access:
 //!
-//! ```ignore
+//! ```
 //! let f = Promise(forall a. { myField : Num, a} -> Num, fun rec => rec.myField)
 //! ```
 //!


Test patch:
diff --git a/tests/pass.rs b/tests/pass.rs
deleted file mode 100644
index 37c2a0a2..00000000
--- a/tests/pass.rs
+++ /dev/null
@@ -1,98 +0,0 @@
-use nickel::program::Program;
-use nickel::term::Term;
-use std::ffi::OsString;
-use std::path::PathBuf;
-use std::thread;
-
-// By default, tests are run with 2MB stack size, which can overflow in debug mode. We run the
-// tests with an increased stack size.
-const STACK_SIZE: usize = 4 * 1024 * 1024;
-
-fn run(path: impl Into<OsString>) {
-    let path = path.into();
-    let mut p = Program::new_from_file(path.clone()).expect("could not load file as a program");
-    assert_eq!(
-        p.eval(),
-        Ok(Term::Bool(true)),
-        "error evaluating {}",
-        path.to_string_lossy(),
-    );
-}
-
-fn check_file(file: &str) {
-    let mut path = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
-    path.push(format!("tests/pass/{}", file));
-
-    thread::Builder::new()
-        .name(String::from(file))
-        .stack_size(STACK_SIZE)
-        .spawn(|| run(path))
-        .unwrap()
-        .join()
-        .unwrap();
-}
-
-#[test]
-fn basics() {
-    check_file("basics.ncl");
-}
-
-#[test]
-fn builtins() {
-    check_file("builtins.ncl");
-}
-
-#[test]
-fn complete() {
-    check_file("complete.ncl");
-}
-
-#[test]
-fn contracts() {
-    check_file("contracts.ncl");
-}
-
-#[test]
-fn eq() {
-    check_file("eq.ncl")
-}
-
-#[test]
-fn functions() {
-    check_file("functions.ncl");
-}
-
-#[test]
-fn lists() {
-    check_file("lists.ncl");
-}
-
-#[test]
-fn metavalues() {
-    check_file("metavalues.ncl");
-}
-
-#[test]
-fn records() {
-    check_file("records.ncl");
-}
-
-#[test]
-fn strings() {
-    check_file("strings.ncl");
-}
-
-#[test]
-fn typechecking() {
-    check_file("typechecking.ncl");
-}
-
-#[test]
-fn types() {
-    check_file("types.ncl");
-}
-
-#[test]
-fn serialize() {
-    check_file("serialize.ncl");
-}
diff --git a/tests/pass/basics.ncl b/tests/pass/basics.ncl
deleted file mode 100644
index d5b746b5..00000000
--- a/tests/pass/basics.ncl
+++ /dev/null
@@ -1,37 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-// basic arithmetic
-(1+1 == 2 | #Assert) &&
-(1-2+3-4 == -2 | #Assert) &&
-(2-3-4 == -5 | #Assert) &&
-(-1-2 == -3 | #Assert) &&
-(2*2 + 2*3 - 2*4 == 2 | #Assert) &&
-(1/2 + 1/4 - 1/8 == 0.625 | #Assert) &&
-((10 + 1/4) % 3 == 1.25 | #Assert) &&
-(10 + 1/4 % 3 == 10.25 | #Assert) &&
-(34 + (if true then 2 else 222)
-  == 36
-  | #Assert) &&
-
-// comparisons
-(1 < 1 == false | #Assert) &&
-(1 <= 1 == true | #Assert) &&
-(1 > 1 == false | #Assert) &&
-(1 >= 1 == true | #Assert) &&
-(1 + 1/2 > 1 + 1/4 == true | #Assert) &&
-(1 + 1/2 < 1 + 1/4 == false | #Assert) &&
-(1 + 1/2 + 1/8 > 1 + 1/4 + 1/4 == true | #Assert) &&
-(1 + 1/2 + 1/8 < 1 + 1/4 + 1/4 == false | #Assert) &&
-(-1 - 2 < 3 - 10 == false | #Assert) &&
-(-1 - 2 > 3 - 10 == true | #Assert) &&
-(-1*2 > 1*2 == false | #Assert) &&
-(-1*2 < 1*2 == true | #Assert) &&
-(1/4 + 1/4 - 1/4 + 1/4 <= 1/2 == true | #Assert) &&
-(1/4 + 1/4 - 1/4 + 1/4 < 1/2 == false | #Assert) &&
-(1/4 + 1/4 - 1/4 + 1/4 >= 1/2 == true | #Assert) &&
-(1/4 + 1/4 - 1/4 + 1/4 < 1/2 == false | #Assert) &&
-
-// This test checks that the terms of a switch are closured
-(let x = 3 in (switch { foo => 1, _ => x, } (3 + 2)) == 3) &&
-
-true
diff --git a/tests/pass/builtins.ncl b/tests/pass/builtins.ncl
deleted file mode 100644
index 3795a036..00000000
--- a/tests/pass/builtins.ncl
+++ /dev/null
@@ -1,22 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-// is_record
-(builtins.isRecord {} | #Assert) &&
-
-/// This currently do not check that subexpressions are actually forced,
-/// just that the evaluation succeeds
-(%seq% 1 true | #Assert) &&
-(let x = (1 + 1) in %seq% x x == 2 | #Assert) &&
-(let r = {a=(1 + 1);} in
-  %deepSeq% r (r.a) == 2 | #Assert) &&
-(let r = {a=(1 + 1);b=("a" ++ "b");} in
-  %deepSeq% r (r.b) == "ab" | #Assert) &&
-(let r = {a = {b = 1 + 1}} in
-  %deepSeq% r (r.a.b) == 2 | #Assert) &&
-
-(let inj = fun x => {b=(x + 2)} in
-  let cat = fun x => fun y => x ++ y in
-  let r = {a=(inj 1);b=(cat "a" "b")} in
-  %deepSeq% r (r.a.b) == 3 | #Assert) &&
-
-true
diff --git a/tests/pass/complete.ncl b/tests/pass/complete.ncl
deleted file mode 100644
index 9b546ea9..00000000
--- a/tests/pass/complete.ncl
+++ /dev/null
@@ -1,11 +0,0 @@
-let AssertEq = fun val l x => val == x || %blame% l in
-
-let Y = Assume(((Num -> Num) -> Num -> Num) -> Num -> Num, fun f => (fun x => f (x x)) (fun x => f (x x))) in
-  let dec : Num -> Num = fun x => x + (-1) in
-  let or : Bool -> Bool -> Bool = fun x => fun y => if x then x else y in
-  let fibo : Num -> Num = Y (fun fibo =>
-      (fun x => if or (x == 0) (dec x == 0) then 1 else (fibo (dec x)) + (fibo (dec (dec x))))) in
-  let val : Num = 4 in
-  (fibo val | #(AssertEq 5)) &&
-
-true 
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
deleted file mode 100644
index 6467bbbb..00000000
--- a/tests/pass/contracts.ncl
+++ /dev/null
@@ -1,89 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-(let AlwaysTrue = fun l t =>
-  let boolT = Assume(Bool, t) in
-  if boolT then boolT else %blame% l in
-let AlwaysFalse = fun l t =>
-  let boolT = Assume(Bool, t) in
-  if boolT then %blame% l else boolT
-in let not | #AlwaysTrue -> #AlwaysFalse = fun b => if b then false else true in
-not true == false) &&
-
-// id_polymorphic_contract
-(let id | forall a. a -> a = fun x => x in id true) &&
-
-// higher_order_contract
-(let to_bool | forall a. (a -> Bool) -> a -> Bool =
-  fun f => fun x => f x in
-  to_bool (fun x => true) 4) &&
-
-// apply_twice
-(let twice | forall a. (a -> a) -> a -> a =
-  fun f => fun x => f (f x) in
-twice (fun x => x + 1) 3 == 5) &&
-
-// strings
-("hello" | Str) == "hello" &&
-("hello" ++ " world" | Str) == "hello world" &&
-
-// enums_simple
-(`foo | <foo, bar>) == `foo &&
-(`bar | forall r. <foo, bar | r>) == `bar &&
-
-// enums_complex
-(let f : forall r. <foo, bar | r> -> Num =
-  fun x => switch { foo => 1, bar => 2, _ => 3, } x in
-f `bar == 2) &&
-
-(let f : forall r. <foo, bar | r> -> Num =
-  fun x => switch { foo => 1, bar => 2, _ => 3, } x in
-f `boo == 3) &&
-
-// records_simple
-(({} | {}) == {} | #Assert) &&
-(let x | {a: Num, s: Str} = {a = 1; s = "a"} in
-  %deepSeq% x x == {a = 1; s = "a"}
-  | #Assert) &&
-
-(let x | {a: Num, s: {foo: Bool}} = {a = 1; s = { foo = true}} in
-  %deepSeq% x x == {a = 1; s = { foo = true}}
-  | #Assert) &&
-
-// polymorphism
-(let id | forall a. { | a} -> { | a} = fun x => x in
-  let extend | forall a. { | a} -> {foo: Num | a} = fun x =>
-    x & {foo = 1} in
-  let remove | forall a. {foo: Num | a} -> { | a} = fun x =>
-    x -$ "foo" in
-
-  (id {} == {} | #Assert) &&
-  (id {a = 1; b = false} == {a = 1; b = false} | #Assert) &&
-  (extend {} == {foo = 1} | #Assert) &&
-  (extend {bar = false} == {foo = 1; bar = false} | #Assert) &&
-  (remove {foo = 1} == {} | #Assert) &&
-  (remove {foo = 1; bar = 1} == {bar = 1} | #Assert) &&
-  (remove (extend {}) == {} | #Assert) &&
-  (extend (remove {foo = 2}) == {foo =1} | #Assert) &&
-  (let f | forall a b. {f: a -> a, arg: a | b} -> a =
-      fun rec => rec.f (rec.arg) in
-    f { f = fun x => x ++ " suffix"; arg = "foo" }
-    == "foo suffix"
-    | #Assert)
-) &&
-
-// records_dynamic_tail
-(({a = 1; b = "b"} | {a: Num, b: Str | Dyn}) == {a = 1; b = "b"}
-  | #Assert) &&
-(({a = 1; b = "b"; c = false} | {a: Num, b: Str | Dyn})
-  == {a = 1; b = "b"; c = false}
-  | #Assert) &&
-((fun r => r.b | {a: Num | Dyn} -> Dyn) {a = 1; b = 2} == 2
-  | #Assert) &&
-
-
-// lists
-(([1, "2", false] | List) == [1, "2", false] | #Assert) &&
-(([1, 2, 3] | List Num) == [1, 2, 3] | #Assert) &&
-((["1", "2", "false"] | List Str) == ["1", "2", "false"] | #Assert) &&
-
-true
diff --git a/tests/pass/eq.ncl b/tests/pass/eq.ncl
deleted file mode 100644
index da314768..00000000
--- a/tests/pass/eq.ncl
+++ /dev/null
@@ -1,83 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-// basic
-(0 == 0 + 0 + 0 | #Assert) &&
-(true == (if true then true else false) | #Assert) &&
-("a" ++ "b" ++ "c" == "#{"a" ++ "b"}" ++ "c" | #Assert) &&
-(`Less == `Less | #Assert) &&
-(`small == `small | #Assert) &&
-
-(1 + 1 != 0 | #Assert) &&
-(true != (if true then false else true) | #Assert) &&
-("a" != "a" ++ " " | #Assert) &&
-(1 != true | #Assert) &&
-("1" != 1 | #Assert) &&
-("true" != true | #Assert) &&
-(`Less != `small | #Assert) &&
-(`Less != 0 | #Assert) &&
-(`Greater != false | #Assert) &&
-
-// lists
-([] == [] | #Assert) &&
-([(1 + 0), (1 + 1), (1 + 1 + 1)] == [1, 2, 3] | #Assert) &&
-([(1 + 0), ("a" ++ "b"), (if true then true else false)]
-  == [1, "ab", true]
-  | #Assert) &&
-([[[]]] == [[[]]] | #Assert) &&
-([[1], [[2]]] == [[2 + (-1)], [[1 + 1]]] | #Assert) &&
-([[true, false]] == lists.flatten [[[true, false]]] | #Assert) &&
-
-([] != [1] | #Assert) &&
-([] != 1 | #Assert) &&
-([] != {} | #Assert) &&
-([1, "a", true] != [1, "a", false] | #Assert) &&
-([[true]] != [[[true]]] | #Assert) &&
-
-// records
-({} == {} | #Assert) &&
-({}$["a" = 1]$["b" = true]
-  == {a = 1; b = true}
-  | #Assert) &&
-({a = 1 + 0; b = 1 + 1; c = 1 + 1 + 1}
-  == { a = 1; b = 2; c = 3 }
-  | #Assert) &&
-({
-    foo = 1 + 0;
-    bar = "a" ++ "b";
-    baz = if true then true else false
-  } == {foo = 1; bar = "ab"; baz = true}
-  | #Assert) &&
-
-({}$["a" = { a = { a = {} } }]
-  == { a = { a = { a = {} } } }
-  | #Assert) &&
-({
-    foo = {bar = 2 + (-1)};
-    baz = {foo = {bar = 1 + 1}}
-  }
-  == {foo = {bar = 1}; baz = {foo = {bar = 2}}}
-  | #Assert) &&
-({} != {a = true} | #Assert) &&
-({a = 1} != {a = 2} | #Assert) &&
-({ a = "a"; b = true } != { a = true; b = "a"} | #Assert) &&
-({ a = { a = true } } != {a = { a = { a = true } } } | #Assert) &&
-
-// Now that the equality operator directly uses the stack to store its continuation (see
-// https://github.com/tweag/nickel/pull/247), check that it correctly cleans the stack when
-// evaluating a subequality to `false`.
-// Generate an non-empty evaluation context to evaluate equalities over a non-empty stack
-(let eq_with_ctxt = fun x y =>
-    let not = fun b =>
-      if b then true else false in
-    not (not (not (not ((x) == (y))))) in
-  (eq_with_ctxt
-      {a = 1 + 0; b = 1 + 1 + a; c = 0; d = 0}
-      { a = 1; b = 3; c = 0; d = 0}
-    | #Assert) &&
-  (eq_with_ctxt
-      [[1,2,3,4], [1,0,3,4], [1,2,3,4], [1,2,3,4]]
-      [[1,2,3,4], [1,2,3,4], [1,2,3,4], [1,2,3,4]]
-    == false 
-    | #Assert)) &&
-
-true
diff --git a/tests/pass/functions.ncl b/tests/pass/functions.ncl
deleted file mode 100644
index 1e885053..00000000
--- a/tests/pass/functions.ncl
+++ /dev/null
@@ -1,20 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-((fun x => x) 3 == 3 | #Assert) &&
-((fun x y => x) 1 2 == 1 | #Assert) &&
-((fun x y => y) 1 2 == 2 | #Assert) &&
-((fun f x => f 0) (fun x => x+2) 2 == 2 | #Assert) &&
-
-(let f = fun f y => f (f y) in f (fun x => x+1) 3 == 5 | #Assert) &&
-(let g  = fun x => if x then 0 else false in g ((fun x => true) 23)
-  == 0
-  | #Assert) &&
-// Y fixpont combinator
-(let Y = (fun f => (fun x => f (x x)) (fun x => f (x x))) in
-  let g = Y (fun g => (fun x => if x  then (g false) else 4)) in
-  g true
-  == 4
-  | #Assert) &&
-
-
-true
diff --git a/tests/pass/lists.ncl b/tests/pass/lists.ncl
deleted file mode 100644
index 1233c4fb..00000000
--- a/tests/pass/lists.ncl
+++ /dev/null
@@ -1,38 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-// accesses
-(lists.elemAt [1,2,3] 1 == 2 | #Assert) &&
-(lists.elemAt (lists.map (fun x => x + 1) [1,2,3]) 1 == 3 | #Assert) &&
-
-// length
-(lists.length [] == 0 | #Assert) &&
-(lists.length [1,2,3] == 3 | #Assert) &&
-(lists.length ([] @ [1,2] @ [3,4] @ []) == 4 | #Assert) &&
-
-// Test case added after https://github.com/tweag/nickel/issues/154
-(let x = 1 in let l = [x] @ [2] in %head% l == 1 | #Assert) &&
-
-(let Y = fun f => (fun x => f (x x)) (fun x => f (x x)) in
-  let foldr_ =
-    fun self => fun f => fun acc => fun l =>
-      if %length% l == 0 then acc
-      else
-        let h = %head% l in
-        let t = %tail% l in
-        let next_acc = self f acc t in
-        f next_acc h in
-  let foldr = Y foldr_ in
-  let and : Bool -> Bool -> Bool =
-      fun x => fun y =>
-          if x then
-              if y then true else false
-          else false
-  in
-  let all = fun pred => fun l => foldr and true (%map% l pred) in
-  let isZ = fun x => x == 0 in
-  all isZ [0, 0, 0, 1]
-  == false
-  | #Assert) &&
-
-
- true
diff --git a/tests/pass/metavalues.ncl b/tests/pass/metavalues.ncl
deleted file mode 100644
index faf130e7..00000000
--- a/tests/pass/metavalues.ncl
+++ /dev/null
@@ -1,61 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-((10 | default | Num) == 10 | #Assert) &&
-
-// Check the correct handling of the update of thunks containing enriched values (see issue
-// https://github.com/tweag/nickel/issues/123)
-(let x = {a = (fun x => (1 | default)) 1} in
-  builtins.seq (x.a) ((x & {a=2}).a) == 2 | #Assert) &&
-
-// merge_default
-(({a = 2} & {a | default = 0; b | default = true}) == {a = 2; b = true}
-  | #Assert) &&
-({a | default = {x = 1}} & {a | default = {y = "y"}} == {a = {x = 1; y = "y"}}
-  | #Assert) &&
-
-// merge_contract
-({a = 2; b | Bool} & {a | Num; b | default = true}
-  == {a = 2; b = true}
-  | #Assert) &&
-
-// merge_default_contract
-({a = 2} & {a | default | Num = 0; b | default = true}
-  == {a = 2; b = true}
-  | #Assert) &&
-
-({a=2} & {a | Num} & {a | default = 3} == {a = 2} | #Assert) &&
-({a=2} & {b | Num} & {b | default = 3} == {a = 2; b = 3} | #Assert) &&
-(({a=Default(1)} & {b=Contract(Num)} & {a=Default(1)}).a
-  == 1
-  | #Assert) &&
-
-// composed
-(let Even = fun l x => if x % 2 == 0 then x else %blame% l in
-  let DivBy3 = fun l x => if x % 3 ==  0 then x else %blame% l in
-  let composed = {a | #Even} & {a | #DivBy3} in
-  (composed & {a = 6} == {a = 6} | #Assert) &&
-  (composed & {a = 12} == {a = 12} | #Assert)) &&
-
-
-// Check that the environments of contracts are correctly saved and restored when merging. See
-// issue [#117](https://github.com/tweag/nickel/issues/117)
-(let ctr_num = let x = num in {a | #x} in
-  let ctr_id = let x = fun l x => x in {a | #x} in
-  let val = let x = 1 in {a = x} in
-  let def = let x = 2 in {a | default = x} in
-  let def2 = let x = (1 + 1) in {a | default = x} in
-// contract/contract -> contract/value -> value/default
-((ctr_num & ctr_id & val & def).a == 1 | #Assert) &&
-// default/value <- value/contract
-((def & (val & ctr_num)).a == 1 | #Assert) &&
-// default/contract-> contract-default/contract-default <- contract/default
-(((def & ctr_num) & (ctr_id & def2)).a == 2 | #Assert) &&
-// default/contract -> contract-default/contract -> contract-default/value
-((def & ctr_num & ctr_id & val).a == 1 | #Assert) &&
-// default/contract -> contract-default/default
-((def & ctr_num & def2).a == 2 | #Assert) &&
-// value/contract-default <- contract/contract-default
-((val & (ctr_num & def)).a == 1 | #Assert)) &&
-
-
-true
diff --git a/tests/pass/records.ncl b/tests/pass/records.ncl
deleted file mode 100644
index c4c1e437..00000000
--- a/tests/pass/records.ncl
+++ /dev/null
@@ -1,97 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-// accesses
-(({foo = 3; bar = true}).bar == true | #Assert) &&
-({"#{if true then "foo" else "bar"}" = false; bar = true}.foo
-  == false
-  | #Assert) &&
-
-(({foo = 3; bar = true})."bar" == true | #Assert) &&
-({"#{if true then "foo" else "bar"}" = false; bar = true}."#{"foo"}"
- == false 
- | #Assert) &&
-
-(({bar = 3}$["foo" = true]).foo == true
-  | #Assert) &&
-
-// primitive_ops
-(records.hasField "foo" {foo = 1; bar = 2} | #Assert) &&
-(records.hasField "fop" {foo = 1; bar = 2} == false | #Assert) &&
-(records.hasField "foo" ({foo = 2; bar = 3} -$ "foo")
-  == false
-  | #Assert) &&
-
-(records.hasField "foo" ({bar = 3}$["foo" = 1]) | #Assert) &&
-
-// lazyness of map
-((records.map (fun x y => y + 1) {foo = 1; bar = "it's lazy"}).foo
-  == 2
-  | #Assert) &&
-
-(let r = records.map
-    (fun y x => if %isNum% x then x + 1 else 0)
-    {foo = 1; bar = "it's lazy"} in
-  (r.foo) + (r.bar) == 2
-  | #Assert) &&
-
-// merging
-({a = 1} & {b=true} == {a = 1; b = true} | #Assert) &&
-({a = 1; b = 2} & {b = 2; c = 3}
-  == {a = 1; b = 2; c = 3}
-  | #Assert) &&
-
-({a = {b = 1}} & {a = {c = true}}
-  == {a = {b = 1; c = true}}
-  | #Assert) &&
-
-// merge_complex
-(let rec1 = {
-    a = false;
-    b = if true then (1 + 1) else (2 + 0);
-    c= ((fun x => x) (fun y => y)) 2;
-  } in
-  let rec2 = {
-    b = ((fun x => x) (fun y => y)) 2;
-    c = if true then (1 + 1) else (2 + 0);
-    d = true;
-  } in
-  let result = {
-    a = false;
-    b = 2;
-    c = 2;
-    d = true;
-  } in
-  rec1 & rec2 == result
-  | #Assert) &&
-
-// merge_with_env
-((fun y => ((fun x => {a=y}) 1) & ({b=false})) 2
-  == {a = 2; b = false}
-  | #Assert) &&
-
-// merge_with_env_nested
-({b={c=10}} & ((fun x => {a=x; b={c=x}}) 10)
-  == {a=10; b = {c = 10}}
-  | #Assert) &&
-
-// recursive_records
-({a = 1; b = a + 1; c = b + a} == {a = 1; b = 2; c = 3} | #Assert) &&
-({f = fun x y =>
-    if x == 0 then y else f (x + (-1)) (y + 1)
-  }.f 5 5
-  == 10
-  | #Assert) &&
-
-(let with_res = fun res =>
-  {
-    f = fun x =>
-      if x == 0 then
-        res
-      else g x;
-    g = fun y => f (y + (-1))
-  }.f 10 in
-  with_res "done" == "done"
-  | #Assert) &&
-
-
-true
diff --git a/tests/pass/serialize.ncl b/tests/pass/serialize.ncl
deleted file mode 100644
index 54cbfc79..00000000
--- a/tests/pass/serialize.ncl
+++ /dev/null
@@ -1,33 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-let assertSerInv = fun x =>
-    let assertAux = fun format x =>
-      %deserialize% format (%serialize% format (%deepSeq% x x)) == x in
-    assertAux `Json x &&
-    assertAux `Yaml x &&
-    assertAux `Toml x in
-
-let assertDeserInv = fun x =>
-    let assertAux = fun format x =>
-      let s = %serialize% format (%deepSeq% x x) in
-      %serialize% format (%deserialize% format s) == s in
-    assertAux `Json x &&
-    assertAux `Yaml x &&
-    assertAux `Toml x in
-
-(assertSerInv {val = 1 + 1} | #Assert) &&
-(assertSerInv {val = "Some string"} | #Assert) &&
-(assertSerInv {val = ["a", 3, []]} | #Assert) &&
-(assertSerInv {a.foo.bar = "2"; b = false; c = [{d = "e"}, {d = "f"}]}
-  | #Assert) &&
-
-(assertDeserInv {a = 1; b = 4; c = 3} | #Assert) &&
-(assertDeserInv {a.b.c = "richtig"} | #Assert) &&
-(assertDeserInv {
-    foo = 1;
-    bar = ["str", true];
-    baz = {subfoo = true; subbar = 0}
-  } | #Assert) &&
-
-
-true
diff --git a/tests/pass/strings.ncl b/tests/pass/strings.ncl
deleted file mode 100644
index 7f96a6fa..00000000
--- a/tests/pass/strings.ncl
+++ /dev/null
@@ -1,17 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-// interpolation
-("simple #{"interp" ++ "olation"} here" == "simple interpolation here"
-  | #Assert) &&
-("#{"alone"}" == "alone" | #Assert) &&
-("nested #{ "#{(fun x => "#{x}") "expression"}" }"
-  == "nested expression" | #Assert) &&
-("#{"some"}#{" " ++ "se" ++ "qu"}#{"#{"ence"}"}"
-  == "some sequence" | #Assert) &&
-("nested #{ {str = {a = "braces"}.a}.str } !"
-  == "nested braces !" | #Assert) &&
-((let x = "world" in
-  "Hello, #{x}! Welcome in #{let y = "universe" in "the #{x}-#{y}"}")
-  == "Hello, world! Welcome in the world-universe" | #Assert) &&
-true
-
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
deleted file mode 100644
index 3087263b..00000000
--- a/tests/pass/typechecking.ncl
+++ /dev/null
@@ -1,162 +0,0 @@
-let typecheck = [
-  // basics
-  true : Bool,
-  false : Bool,
-  0 : Num,
-  45 : Num,
-  fun x => x : forall a. a -> a,
-  let x = 3 in (x : Num),
-  4 + false,
-  (true | Num) : Num,
-  "hello" : Str,
-
-  // functions
-  (fun x => if x then x + 1 else 34) false,
-  let id : Num -> Num = fun x => x in (id 4 : Num),
-  // the id parameter is inferred
-  (fun id => (id 4 : Num)) (fun x => x),
-  // non strict zones don't unify
-  (fun id => (id 4) + (id true: Bool)) (fun x => x),
-  // contracts are opaque types
-  (let AlwaysTrue = fun l t => if t then t else %blame% l in
-  ((fun x => x) : #alwaysTrue -> #alwaysTrue)),
-
-  // simple_polymorphism
-  let f : forall a. a -> a = fun x => x in
-    ((if (f true) then (f 2) else 3) : Num),
-
-  let f : forall a. (forall b. a -> b -> a) = fun x y => x in
-    ((if (f true 3) then (f 2 false) else 3) : Num),
-
-  let f : forall a. (forall b. b -> b) -> a -> a = fun f x => f x in
-    f (fun z => z : forall y. y -> y),
-
-  // forall nested
-  let f : forall a. a -> a =
-      let g | forall a. (a -> a) = fun x => x in
-      g in
-    ((if (f true) then (f 2) else 3) : Num),
-
-  let f : forall a. a -> a =
-      let g | forall a. (a -> a) = fun x => x in
-      g g in
-    ((if (f true) then (f 2) else 3) : Num),
-
-
-  let f : forall a. a -> a =
-      let g : forall a. (forall b. (b -> (a -> a))) = fun y x => x in
-      g 0 in
-    ((if (f true) then (f 2) else 3) : Num),
-
-  // enums_simple
-  (`bla : <bla>),
-  (`blo : <bla, blo>),
-  (`bla : forall r. <bla | r>),
-  (`bla : forall r. <bla, blo | r>),
-  ((switch {bla => 3} `bla) : Num),
-  ((switch {bla => 3, _ => 2} `blo) : Num),
-
-  // enums_complex
-  ((fun x => switch {bla => 1, ble => 2} x) : <bla, ble> -> Num),
-  ((fun x => switch {bla => 1, ble => 2, bli => 4} (%embed% bli x))
-    : <bla, ble> -> Num),
-  ((fun x =>
-      (switch {bla => 3, bli => 2} x)
-      + (switch {bli => 6, bla => 20} x))
-    `bla
-    : Num),
-
-  let f : forall r. <blo, ble | r> -> Num = fun x =>
-    switch {blo => 1, ble => 2, _ => 3} x in
-            (f `bli : Num),
-
-  let f : forall r. (forall p. <blo, ble | r> -> <bla, bli | p>) =
-    fun x => switch {blo => `bla, ble => `bli, _ => `bla, } x in
-    f `bli,
-
-  // static records
-  ({bla = 1} : {bla : Num}),
-  ({blo = true; bla = 1} : {bla : Num, blo : Bool}),
-  ({blo = 1}.blo : Num),
-  ({bla = true; blo = 1}.blo : Num),
-  let r : {bla : Bool, blo : Num} = {blo = 1; bla = true} in
-    ((if r.bla then r.blo else 2) : Num),
-
-  let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
-      fun r => if r.bla then r.blo else r.ble in
-    (if (f {bla = true; blo = false; ble = true; blip = 1; }) then
-      (f {bla = true; blo = 1; ble = 2; blip = `blip; })
-    else
-      (f {bla = true; blo = 3; ble = 4; bloppo = `bloppop; }) : Num),
-
-  ({ "#{if true then "foo" else "bar"}" = 2; } : {_ : Num}),
-  ({ "#{if true then "foo" else "bar"}" = 2; }."bla" : Num),
-  ({ foo = 3; bar = 4; } : {_ : Num}),
-
-  // seq
-  (%seq% false 1 : Num),
-  ((fun x y => %seq% x y) : forall a. (forall b. a -> b -> b)),
-  let xDyn = if false then true else false in
-    let yDyn = 1 + 1 in (%seq% xDyn yDyn : Dyn),
-
-  // lists_simple
-  [1, "2", false],
-  //TODO: the type system may accept the following test at some point.
-  //([1, "2", false] : List),
-  (["a", "b", "c"] : List Str),
-  ([1, 2, 3] : List Num),
-  (fun x => [x] : forall a. a -> List a),
-
-  // lists_ops
-  fun l => %tail% l : forall a. List a -> List a,
-  fun l => %head% l : forall a. List a -> a,
-  fun f l => %map% l f : forall a b. (a -> b) -> List a -> List b,
-  fun l1 => fun l2 => l1 @ l2 : forall a. List a -> List a -> List a,
-  fun i l => %elemAt% l i : forall a. Num -> List a -> a,
-
-  // recursive_records
-  {a : Num = 1; b = a + 1} : {a : Num, b : Num},
-  {a : Num = 1 + a} : {a : Num},
-  {a : Num = 1 + a} : {a : Num},
-
-  // let_inference
-  (let x = 1 + 2 in let f = fun x => x + 1 in f x) : Num, 
-  // (let x = 1 + 2 in let f = fun x => x ++ "a" in f x) : Num,
-  {a = 1; b = 1 + a} : {a : Num, b : Num},
-  {f = fun x => if x == 0 then 1 else 1 + (f (x + (-1)));}
-    : {f : Num -> Num},
-
-  { f = fun x => if x == 0 then 1 else 1 + (f (x + (-1)));}
-    : {f : Num -> Num},
-
-  // polymorphic_row_constraints
-  let extend = Assume(forall c. { | c} -> {a: Str | c}, 0) in
-    let remove = Assume(forall c. {a: Str | c} -> { | c}, 0) in
-    (let good = remove (extend {}) in 0) : Num,
-
-  let r | {a: Num | Dyn} = {a = 1; b = 2} in (r.a : Num),
-  ({a = 1; b = 2} | {a: Num | Dyn}) : {a: Num | Dyn},
-
-  //Regression test following [#270](https://github.com/tweag/nickel/issues/270). Check that
-  //unifying a variable with itself doesn't introduce a loop. The failure of this test results
-  //in a stack overflow.
-  {gen_ = fun acc x =>
-    if x == 0 then
-      acc
-    else
-      gen_ (acc @ [x]) (x - 1)
-    }.gen_
-    : List Num -> Num -> List Num,
-
-  {f = fun x => f x}.f : forall a. a -> a,
-
-  // shallow_inference
-  let x = 1 in (x + 1 : Num),
-  let x = "a" in (x ++ "a" : Str),
-  let x = "a#{"some str inside"}" in (x ++ "a" : Str),
-  let x = false in (x || true : Bool),
-  let x = false in let y = x in let z = y in (z : Bool),
-] in
-
-
-true
diff --git a/tests/pass/types.ncl b/tests/pass/types.ncl
deleted file mode 100644
index 76015ace..00000000
--- a/tests/pass/types.ncl
+++ /dev/null
@@ -1,6 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-(let plus : Num -> Num -> Num = fun x => fun y => x + y in
- plus (54 : Num) (6 : Num) == 60 | #Assert) &&
-
- true