Repository: tweag/nickel
Pull request #745 (2022-06-22 10:20:06)

Fix random order of fields in `nickel doc`
Depends on #743. `nickel doc` doesn't sort the fields of records, and because Rust hashmaps are randomized, two invocations of on the same file will order fields in a different way. This PR fixes that by always sorting fields before processing them. Passing by, I replaced a few `sort_by` calls by `sort_by_key` elsewhere, which are arguably simpler.


Patch:
diff --git a/.github/workflows/continuous-integration.yml b/.github/workflows/continuous-integration.yml
index cc60a76c..f287a0bc 100644
--- a/.github/workflows/continuous-integration.yml
+++ b/.github/workflows/continuous-integration.yml
@@ -45,8 +45,8 @@ jobs:
     - name: Setup Cachix
       uses: cachix/cachix-action@v10
       with:
-        name: tweag-nickel
-        authToken: '${{ secrets.CACHIX_TWEAG_NICKEL_AUTH_TOKEN }}'
+        name: nickel
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
 
     - name: Run all checks
       run: |
diff --git a/.github/workflows/deploy-preview.yml b/.github/workflows/deploy-preview.yml
index eda5a9b8..e1434aed 100644
--- a/.github/workflows/deploy-preview.yml
+++ b/.github/workflows/deploy-preview.yml
@@ -8,6 +8,6 @@ jobs:
     with:
       production_deploy: false
     secrets:
-      CACHIX_AUTH_TOKEN: ${{ secrets.CACHIX_TWEAG_NICKEL_AUTH_TOKEN }}
+      CACHIX_AUTH_TOKEN: ${{ secrets.CACHIX_AUTH_TOKEN }}
       NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
       NETLIFY_SITE_ID: ${{ secrets.NETLIFY_SITE_ID }}
diff --git a/.github/workflows/update-flake-lock.yml b/.github/workflows/update-flake-lock.yml
index 647d3610..7cb60c92 100644
--- a/.github/workflows/update-flake-lock.yml
+++ b/.github/workflows/update-flake-lock.yml
@@ -16,4 +16,4 @@ jobs:
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
       - name: Update flake.lock
-        uses: DeterminateSystems/update-flake-lock@v10
+        uses: DeterminateSystems/update-flake-lock@v9
diff --git a/.gitignore b/.gitignore
index 0ead4b15..6c79d83a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,6 +12,8 @@
 # rustfmt Backup file
 **/*.rs.bk
 
+# Makam cache
+/.makam-cache/
 /node_modules
 /lsp/client-extension/node_modules
 /lsp/client-extension/out
diff --git a/Cargo.lock b/Cargo.lock
index e7421261..ad98cd45 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1244,13 +1244,6 @@ dependencies = [
  "nickel-lang",
 ]
 
-[[package]]
-name = "nickel-repl"
-version = "0.1.0"
-dependencies = [
- "nickel-lang",
-]
-
 [[package]]
 name = "nix"
 version = "0.23.1"
diff --git a/Cargo.toml b/Cargo.toml
index f0617a68..ad5b165f 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -72,7 +72,6 @@ members = [
     ".",
     "lsp/nls",
     "utilities",
-    "nickel-wasm-repl",
 ]
 
 # Enable this to use flamegraphs
diff --git a/HACKING.md b/HACKING.md
index a1224d07..2100f2c8 100644
--- a/HACKING.md
+++ b/HACKING.md
@@ -79,12 +79,12 @@ nickel-lang-lsp 0.1.0
 ## WebAssembly REPL
 
 There is a WebAssembly (WASM) version of the REPL, which is used for the online
-playground on [nickel-lang.org][nickel-lang.org]. To ease the build, we use the
-`nickel-repl` located in `nickel-wasm-repl`, which just wraps and re-export
-the `nickel-lang` with the right settings for building to WebAssembly.
+playground on [nickel-lang.org][nickel-lang.org]. Using Cargo directly to build
+the WASM REPL is possible but is not a trivial procedure. The Cargo way requires
+installing new tools and patching `Cargo.toml`.
 
-The Nix flake has also an output to do the whole build, but incremental
-compilation is not as good as with direct usage of `cargo`.
+On the other hand, Nix can do the whole build in one simple command, but
+incremental compilation is not as good as with direct usage of `cargo`.
 
 Both methods are described below.
 
@@ -101,15 +101,43 @@ LICENSE  package.json nickel_lang_bg.js  nickel_lang_bg.wasm [..]
 ### Using Cargo
 
 1. [Install `wasm-pack`][install-wasm-pack]
-2. Run `wasm-pack` on the `nickel-repl` crate:
+2. Add the following line to `Cargo.toml` under the `[lib]` heading:
+
+   ```diff
+   [lib]
+   +crate-type = ["cdylib", "rlib"]
+   ```
+
+3. Remove the following line from `Cargo.toml` (dependency on
+   `nickel-lang-utilities`):
+
+   ```diff
+   -nickel-lang-utilities = {path = "utilities", version = "0.1.0"}
+   ```
+
+4. Run `wasm-pack`:
 
    ```shell
-   cd nickel-repl-wasm
    wasm-pack build -- --no-default-features --features repl-wasm
    ```
 
    A `pkg` directory, containing the corresponding NPM package, should now be
    available.
+5. (Optional) the generated NPM package is named `nickel`, but this name is not
+   very descriptive, and is already in use in the NPM registry. You can patch
+   the name of the NPM package using `jq` to be `nickel-repl` instead:
+
+   ```shell
+   $ jq '.name = "nickel-repl"' pkg/package.json > package.json.patched \
+     && rm -f pkg/package.json \
+     && mv package.json.patched pkg/package.json
+   ```
+
+   If you don't have `jq`, you can do it by hand: replace the `name` attribute
+   in `pkg/package.json` by `"nickel-repl"`.
+
+The `pkg` directory now contains a `nickel-repl` NPM package that can be used
+from JavaScript.
 
 # Testing
 
diff --git a/benches/mantis/lib.ncl b/benches/mantis/lib.ncl
index 78f39856..69a6a9a2 100644
--- a/benches/mantis/lib.ncl
+++ b/benches/mantis/lib.ncl
@@ -14,9 +14,8 @@
     Smaller = fun x => contract.from_predicate (fun y => y < x),
     SmallerEq = fun x => contract.from_predicate (fun y => y <= x),
     MatchRegexp = fun regex label value =>
-      let match = string.is_match regex in
       if builtin.is_str value then
-        if match value then
+        if string.is_match regex value then
           value
         else
           contract.blame_with "no match" label
diff --git a/benches/mantis/schemas/nomad/types.ncl b/benches/mantis/schemas/nomad/types.ncl
index d9f3d347..2671f0d8 100644
--- a/benches/mantis/schemas/nomad/types.ncl
+++ b/benches/mantis/schemas/nomad/types.ncl
@@ -63,7 +63,7 @@ let time = {
       Weight | lib.contracts.Nullable (lib.contracts.AllOf [
                  num.Nat,
                  lib.contracts.GreaterEq -100,
-                 lib.contracts.LesserEq 100])
+                 LesserEq 100])
              | default = null,
       SpreadTarget | Array SpreadTargetElem
                    | default = [],
@@ -73,7 +73,7 @@ let time = {
       Value | Str,
       Percent | lib.contracts.Nullable (lib.contracts.AllOf [
                  num.PosNat,
-                 lib.contracts.LesserEq 100])
+                 LesserEq 100])
               | default = null,
     },
 
@@ -161,7 +161,7 @@ let time = {
       Spreads | Array Spread
               | default = [],
       Count | num.Nat
-            | lib.contracts.Greater 0,
+            | Greater 0,
       # TODO: Meta  [string]  string
       Name  | Str,
       RestartPolicy  | lib.contracts.Nullable json.RestartPolicy
@@ -877,7 +877,7 @@ let time = {
       check_restart | lib.contracts.Nullable stanza.check_restart
                     | default = null,
       header | {_: Array Str} | default = {},
-      body | lib.contracts.Nullable Str
+      body | lib.contracts.Nullable str
            | default = null,
       initial_status | (lib.contracts.OneOf ["passing", "warning", "critical", ""])
                      | default = "",
@@ -999,7 +999,7 @@ let time = {
       #  kill_signal: "SIGTERM"
       #}
 
-      kill_timeout | lib.contracts.Nullable Duration
+      kill_timeout | lib.contracts.Nullable duration
                    | default = null,
 
       lifecycle | lib.contracts.Nullable stanza.lifecycle
diff --git a/benches/nixpkgs/lists.ncl b/benches/nixpkgs/lists.ncl
index 987b1d7c..78e89332 100644
--- a/benches/nixpkgs/lists.ncl
+++ b/benches/nixpkgs/lists.ncl
@@ -220,7 +220,7 @@
   "%m
   = fun pred => foldr (fun x y => if pred x then y else false) true,
 
-  count: forall a. (a -> Bool) -> Array a -> Num
+  count: (a -> Bool) -> Array a -> Num
   | doc m%"
       Count how many elements of `list` match the supplied predicate
      function.
diff --git a/flake.nix b/flake.nix
index db4bcfd6..33bbb2ba 100644
--- a/flake.nix
+++ b/flake.nix
@@ -176,14 +176,16 @@
           name = "nickel-${version}";
 
           buildInputs =
-            [ rust ]
-            ++ missingSysPkgs
-            ++ (if !isDevShell then [ cargoHome ] else [ ]);
+            [
+              rust
+            ] ++ missingSysPkgs
+            ++ (if isDevShell then [ pkgs.nodePackages.makam ]
+            else [ cargoHome ]);
 
           src = if isDevShell then null else self;
 
           buildPhase = ''
-            cargo build --workspace --exclude nickel-repl --release --frozen --offline
+            cargo build --workspace --release --frozen --offline
           '';
 
           doCheck = true;
@@ -211,7 +213,7 @@
           RUST_SRC_PATH = "${rust}/lib/rustlib/src/rust/library";
         };
 
-      buildNickelWasm =
+      buildNickelWASM =
         { channel ? "stable"
         , optimize ? true
         }:
@@ -226,6 +228,8 @@
 
           src = self;
 
+          nativeBuildInputs = [ pkgs.jq ];
+
           buildInputs = [
             rust
             pkgs.wasm-pack
@@ -234,14 +238,42 @@
             cargoHome
           ] ++ missingSysPkgs;
 
+          preBuild = ''
+            # Wasm-pack requires to change the crate type. Cargo doesn't yet
+            # support having different crate types depending on the target, so
+            # we switch there
+            sed -i 's/\[lib\]/[lib]\ncrate-type = ["cdylib", "rlib"]/' Cargo.toml
+
+            # This is a hack to prevent the fs2 crate from being compiled on wasm.
+            # This may be able to be removed once one or more of these issues are resolved:
+            # https://github.com/bheisler/criterion.rs/issues/461
+            # https://github.com/rust-lang/cargo/issues/1596
+            # https://github.com/rust-lang/cargo/issues/1197
+            # https://github.com/rust-lang/cargo/issues/5777
+            sed -i '/nickel-lang-utilities/d' Cargo.toml
+          '';
+
           buildPhase = ''
-            cd nickel-wasm-repl
-            wasm-pack build --mode no-install -- --no-default-features --frozen --offline
+            runHook preBuild
+
+            wasm-pack build --mode no-install -- --no-default-features --features repl-wasm --frozen --offline
             # Because of wasm-pack not using existing wasm-opt
             # (https://github.com/rustwasm/wasm-pack/issues/869), we have to
             # run wasm-opt manually
-            echo "[Nix build script] Manually running wasm-opt..."
-            wasm-opt ${if optimize then "-O4 " else "-O0"} pkg/nickel_repl_bg.wasm -o pkg/nickel_repl.wasm
+            echo "[Nix build script]Manually running wasm-opt..."
+            wasm-opt ${if optimize then "-O4 " else "-O0"} pkg/nickel_lang_bg.wasm -o pkg/nickel_lang_bg.wasm
+
+            runHook postBuild
+          '';
+
+          postBuild = ''
+            # Wasm-pack forces the name of both the normal crate and the
+            # generated NPM package to be the same. Unfortunately, there already
+            # exists a nickel package in the NPM registry, so we use nickel-repl
+            # instead
+            jq '.name = "nickel-repl"' pkg/package.json > package.json.patched \
+              && rm -f pkg/package.json \
+              && mv package.json.patched pkg/package.json
           '';
 
           installPhase = ''
@@ -262,6 +294,24 @@
         };
       };
 
+      makamSpecs = pkgs.stdenv.mkDerivation {
+        name = "nickel-makam-specs-${version}";
+        src = ./makam-spec/src;
+        buildInputs =
+          [
+            pkgs.nodePackages.makam
+          ];
+        buildPhase = ''
+          # For some reason (bug) the first time I use makam here it doesn't generate any output
+          # That's why I'm "building" before testing
+          makam init.makam
+          makam --run-tests testnickel.makam
+        '';
+        installPhase = ''
+          echo "WORKS" > $out
+        '';
+      };
+
       vscodeExtension =
         let node-package = (pkgs.callPackage ./lsp/client-extension { }).package;
         in
@@ -295,7 +345,7 @@
       defaultPackage = packages.build;
       packages = {
         build = buildNickel { };
-        buildWasm = buildNickelWasm { optimize = true; };
+        buildWasm = buildNickelWASM { optimize = true; };
         dockerImage = buildDocker packages.build; # TODO: docker image should be a passthru
         inherit vscodeExtension;
         inherit userManual;
@@ -310,7 +360,9 @@
 
       checks = {
         # wasm-opt can take long: eschew optimizations in checks
-        wasm = buildNickelWasm { channel = "stable"; optimize = false; };
+        wasm = buildNickelWASM { channel = "stable"; optimize = false; };
+        # out of sync, disabling for now -> https://github.com/tweag/nickel/issue/552
+        #specs = makamSpecs;
         pre-commit = defaultPackage.pre-commit;
       } // (forEachRustChannel (channel:
         {
diff --git a/makam-spec/README.md b/makam-spec/README.md
new file mode 100644
index 00000000..fac83a9d
--- /dev/null
+++ b/makam-spec/README.md
@@ -0,0 +1,16 @@
+### Using Makam
+
+Makam is a dialect of lambda Prolog created and maintained by Antonis Stampoulis, more information [here](https://github.com/astampoulis/makam).
+This is an attempt to use it to define the semantics of the **Nickel** language.
+
+He distributes it through [NPM](https://www.npmjs.com/package/makam), and on the [repo](https://github.com/astampoulis/makam) there's information on how to get it working.
+
+#### Using it on Nix
+
+We use the `node2nix` helper, there's a [PR](https://github.com/NixOS/nixpkgs/pull/67703) to add it to nixpkgs, but for now this simple config should help.
+
+Just `nix-build -A makam` and then `result/bin/makam ./src/init.makam -`. Or run `result/bin/makam src/init.makam src/examples.makam` to run the examples.
+
+###### To update it
+
+Run `node2nix --nodejs-12 -c makam-composition.nix` on the `makam-spec` directory
diff --git a/makam-spec/src/ast.makam b/makam-spec/src/ast.makam
new file mode 100644
index 00000000..91691fe5
--- /dev/null
+++ b/makam-spec/src/ast.makam
@@ -0,0 +1,91 @@
+%use "row".
+%use "utils".
+
+(* The AST expressed here is a subset of the whole AST, 
+ * this is what the result of parsing can be as well as
+ * what the typechecker can type. On eval we extend it.
+ *)
+
+expr : type.
+typ : type.
+
+(* Lambda constructs *)
+let : bindone expr expr -> bindone expr expr -> expr.
+lam : bindone expr expr -> expr.
+app : expr -> expr -> expr.
+
+(* Constants *)
+eint : int -> expr.
+ebool : bool -> expr.
+estr : string -> expr.
+
+(* Records *)
+
+(* The type of record fields 
+ * They can be either static or dynamic.
+ *)
+rec_field : type.
+static_field : string -> expr -> rec_field.
+dyn_field : expr -> expr -> rec_field.
+
+(* The constructor of a record (just a list of fields) *)
+erec : (list rec_field) -> expr.
+
+(* The different accesses for records.
+ * They can be either static or dynamic.
+ *)
+static_access : expr -> string -> expr.
+dyn_access : expr -> expr -> expr.
+
+(* Enumerations *)
+enum_var : string -> expr.
+enum_case : expr -> (list (tuple string expr)) -> option expr -> expr.
+
+(* Operations *)
+ite : expr -> expr -> expr -> expr.
+
+unop : type.
+eunop : unop -> expr -> expr.
+blame : unop.
+isNum : unop.
+isBool : unop.
+isStr : unop.
+isRec : unop.
+isFun : unop.
+isEnumIn : (list string) -> unop.
+
+binop : type.
+ebinop : expr -> binop -> expr -> expr.
+add : binop.
+sub : binop.
+mul : binop.
+
+(* Typing *)
+promise : typ -> expr -> expr.
+assume : typ -> expr -> expr -> expr.
+
+(* Blame label
+ * It has a boolean to indicate the polarity and 3 different
+ * actual labels: Positive, Negative and Contract.
+ *)
+label : bool -> string -> string -> string -> expr.
+
+(* Variables *)
+named : string -> expr.
+
+(* Types *)
+tdyn : typ.
+tnum : typ.
+tbool : typ.
+tstr : typ.
+
+tarrow : typ -> typ -> typ.
+forall : (bindone typ typ) -> typ.
+
+tlbl : typ.
+fromExpr : expr -> typ.
+
+open_rec : typ -> (list (tuple string typ)) -> typ.
+clos_rec : (list (tuple string typ)) -> typ.
+
+tenum : row string -> typ.
diff --git a/makam-spec/src/eval.makam b/makam-spec/src/eval.makam
new file mode 100644
index 00000000..d7f90dcc
--- /dev/null
+++ b/makam-spec/src/eval.makam
@@ -0,0 +1,290 @@
+%use "ast".
+%use "row".
+%use "utils".
+
+(* We extend the AST to terms related to the execution,
+ * and add some operations on them
+ *)
+
+(* Negation of the label *)
+neg : expr -> expr.
+contractify : expr -> expr.
+pos : expr -> expr.
+
+(* Record value
+ * Since an erec can have dynamic tags, records get evaluated
+ * to a rec_val where all tags are evaluated to strings (first argument).
+ * It also has a default function (second argument)
+ * to call in case a tag is not found.
+ *)
+rec_val : (list (tuple string expr)) -> (string -> expr) -> expr.
+(* Record types contracts
+ * These primitives take a default contract (only open_rec), a list of
+ * (string, contract) the term and the label.
+ *)
+open_rec_contr : expr -> (list (tuple string expr)) -> expr -> expr -> expr.
+clos_rec_contr : (list (tuple string expr)) -> expr -> expr -> expr.
+
+(* Used for lazy evaluation *)
+thunk : string -> expr -> expr -> expr.
+recThunk : string -> (expr -> expr) -> expr -> expr.
+
+(* wrapping of values *)
+wrapper : expr -> A -> expr.
+unwrap : expr -> A -> expr -> expr.
+
+(* Get the expression contract of a given type *)
+typToExpr : typ -> expr -> prop.
+typToExpr tdyn (lam (bind _ (fun l => lam (bind _ 
+  (fun t => t))))).
+typToExpr tnum (lam (bind _ (fun l => lam (bind _ 
+  (fun t => ite (eunop isNum t) t (eunop blame l)))))).
+typToExpr tbool (lam (bind _ (fun l => lam (bind _ 
+  (fun t => ite (eunop isBool t) t (eunop blame l)))))).
+typToExpr tstr (lam (bind _ (fun l => lam (bind _ 
+  (fun t => ite (eunop isStr t) t (eunop blame l)))))).
+
+(* TODO Simple implementation
+ * On positive positions this is ok, but if it's an open enum, it
+ * shouldn't fail negatively
+ *)
+typToExpr (tenum R) (lam (bind _ (fun l => lam (bind _ (fun t => 
+  ite (eunop (isEnumIn L) t) t (eunop blame l)))))) :-
+    row.toList R L.
+
+typToExpr (tarrow S T) (lam (bind _ (fun l => lam (bind _ 
+  (fun t => ite (eunop isFun t) (lam (bind _ (fun x => app (app Ct l) (app t (app (app Cs (neg l)) x))))) (eunop blame l)))))) :-
+    typToExpr S Cs,
+    typToExpr T Ct.
+
+(* forall contract
+ * We have two versions of the contract, TyTrue and TyFalse, which one is used
+ * depends on the polarity relative to the polarity at the point the forall is at.
+ * They do the opposite of the other, unwrap or wrap the value depending whether the
+ * polarity has changed or not.
+ * Keep in mind TyTrue and TyFalse is not the instantiation of the variable a to a contract,
+ * but the body of the forall applied to different instantiation, and then converted to a contract.
+ * A simpler implementation should be possible at the expense of extending Nickel,
+ * for now this is the simplest way to proceed.
+ *)
+typToExpr (forall (bind _ F)) (lam (bind _ (fun l => ite (pos l) (app TyTrue l) (app TyFalse l))))   :-
+  typToExpr (F (fromExpr (lam (bind _ (fun lp => lam (bind _ (fun t => 
+    ite (pos lp) 
+      (unwrap t X (eunop blame lp))
+      (wrapper t X)
+  ))))))) TyTrue,
+  typToExpr (F (fromExpr (lam (bind _ (fun lp => lam (bind _ (fun t => 
+    ite (pos lp)
+      (wrapper t X)
+      (unwrap t X (eunop blame lp))
+  ))))))) TyFalse.
+
+typToExpr (clos_rec L) (lam (bind _ (fun lp => lam (bind _ (fun t =>
+  clos_rec_contr Lc t lp
+))))) :-
+  map (pfun (Tag, Type) (Tag', TypeC) => typToExpr Type TypeC, eq Tag Tag') L Lc.
+
+typToExpr (open_rec D L) (lam (bind _ (fun l => lam (bind _ (fun t =>
+  open_rec_contr Dc Lc t l
+))))) :-
+  typToExpr D Dc,
+  map (pfun (Tag, Type) (Tag', TypeC) => typToExpr Type TypeC, eq Tag Tag') L Lc.
+
+typToExpr (fromExpr E) E.
+
+eval : expr -> expr -> prop.
+
+(* label *)
+(* The negation and contract labeling are non standard, we keep
+ * track of the polarity, without switching, so the forall contract
+ * keeps working. This means the contractify function will change
+ * whichever label is supposed to be the context. This corresponds
+ * to the indy strategy presented by Dimoulas et al., just a
+ * different implementation.
+ *)
+eval (neg L) (label false N P C) :-
+  eval L (label true N P C).
+eval (neg L) (label true N P C) :-
+  eval L (label false N P C).
+eval (contractify L) (label true P C C) :-
+  eval L (label true P _ C).
+eval (contractify L) (label false C N C) :-
+  eval L (label false _ N C).
+
+eval (pos L) (ebool P) :-
+  eval L (label P _ _ _).
+
+(* Lazy evaluation *)
+eval (thunk _ E V) V' when refl.isunif V :-
+  eval E V,
+  eq V V'.
+eval (thunk _ E V) V' when not (refl.isunif V) :-
+  eq V V'.
+
+eval (recThunk S E V) V' when refl.isunif V :-
+  eval (E (recThunk S E R)) V,
+  eq V V'.
+eval (recThunk _ E V) V' when not (refl.isunif V) :-
+  eq V V'.
+
+(* wrapping *)
+eval (wrapper E A) (wrapper E A).
+
+eval (unwrap X B _) V :-
+  eval X (wrapper E A),
+  refl.sameunif A B,
+  eval E V.
+eval (unwrap X B E) V :-
+  eval X (wrapper _ A),
+  not (refl.sameunif A B),
+  eval E V.
+eval (unwrap X B E) V :-
+  not (eval X (wrapper _ A)),
+  eval E V.
+
+(* Lambda constructs *)
+eval (let (bind Name E) (bind Name T)) V :-  
+  eval (T (recThunk Name E V')) V. 
+
+eval (lam X_Body) (lam X_Body).
+
+eval (app E1 E2) V :-
+  eval E1 (lam (bind Name Body)),
+  eval (Body (thunk Name E2 Shr)) V.
+
+(* Constants *)
+eval (eint N) (eint N).
+eval (ebool B) (ebool B).
+eval (estr S) (estr S).
+eval (label P Pos N C) (label P Pos N C).
+
+(* Records *)
+(* TODO check there are no repeated fields and the 
+ * catch all function should check that as well.
+ *)
+eval (rec_val L C) (rec_val L C).
+
+eval (open_rec_contr D Lt R Lbl) (rec_val Lv' C) :-
+  eval R (rec_val Lv C),
+  map (pfun (Tag, Type) => find Lv Tag _) Lt,
+  map (pfun (Tag, Value) (Tag, (app (app Contract Lbl') Value)) => 
+    eq Lbl' Lbl,
+    ifte (find Lt Tag (Contr, _))
+      (eq Contract Contr)
+      (eq Contract D)
+  ) Lv Lv'.
+eval (open_rec_contr D Lt R Lbl) V :-
+  or
+  (not (eval R (rec_val _ _)))
+  (not (map (pfun (Tag, Type) => find Lv Tag _) Lt)),
+  eval (eunop blame Lbl) V.
+
+eval (clos_rec_contr Lt R Lbl) (rec_val Lv' (fun s => eunop blame (neg Lbl))) :-
+  eval R (rec_val Lv C),
+  map (pfun (Tag, Type) => find Lv Tag _) Lt,
+  map (pfun (Tag, Value) (Tag, (app (app Contr Lbl') Value)) => 
+    eq Lbl' Lbl,
+    find Lt Tag (Contr, _)
+  ) Lv Lv'.
+eval (clos_rec_contr Lt R Lbl) V :-
+  or
+  (not (eval R (rec_val _ _)))
+  (or
+  (not (map (pfun (Tag, Type) => find Lv Tag _) Lt))
+  (not (map (pfun (Tag, Type) => find Lt Tag _) Lv))  
+  ),
+  eval (eunop blame Lbl) V.
+
+eval (erec []) 
+  (rec_val [] (pfun S => eunop blame (label false _ "Attempted to access a non existent field." _))).
+eval (erec ((static_field S E) :: TL)) (rec_val ((tuple S E) :: TL') F) :-
+  eval (erec TL) (rec_val TL' F),
+  not (find TL' S _).
+eval (erec ((dyn_field S E) :: TL)) V :-
+  eval S (estr S'),
+  eval (erec ((static_field S' E) :: TL)) V.
+
+eval (static_access E S) V :-
+  eval E (rec_val L _),
+  find L S (R, _),
+  eval R V.
+eval (static_access E S) V :-
+  eval E (rec_val L F),
+  not (find L S (_, _)),
+  eval (F S) V.
+
+eval (dyn_access E S) V :-
+  eval S (estr S'),
+  eval (static_access E S') V.
+
+(* Enumerations *)
+
+eval (enum_var S) (enum_var S).
+
+eval (enum_case E L _) V :-
+  eval E (enum_var S),
+  find L S (R, _),
+  eval R V.
+eval (enum_case E L (some D)) V :-
+  eval E (enum_var S),
+  not (find L S _),
+  eval D V.
+
+
+(* Operations *)
+eval (ite C T E) V :-
+  eval C (ebool true),
+  eval T V.
+eval (ite C T E) V :-
+  eval C (ebool false),
+  eval E V.
+
+eval_binop : binop -> expr -> expr -> expr -> prop.
+
+eval (ebinop E1 Op E2) V :-
+  map eval [E1, E2] [V1, V2],
+  eval_binop Op V1 V2 V.
+
+eval_binop add (eint N1) (eint N2) (eint N) :- plus N1 N2 N.
+eval_binop sub (eint N1) (eint N2) (eint N) :- plus N2 N N1.
+eval_binop mul (eint N1) (eint N2) (eint N) :- mult N1 N2 N.
+
+eval_unop : unop -> expr -> expr -> prop.
+
+eval (eunop Op E) V :-
+  eval E E',
+  eval_unop Op E' V.
+
+eval_unop blame (label true S _ _) _ :- 
+  print S,
+  failure.
+eval_unop blame (label false _ S _) _ :- 
+  print S,
+  failure.
+
+eval_unop isNum (eint _) (ebool true).
+eval_unop isBool (ebool _) (ebool true).
+eval_unop isStr (estr _) (ebool true).
+eval_unop isRec (rec_val _ _) (ebool true). 
+eval_unop isFun (lam _) (ebool true).
+eval_unop (isEnumIn L) (enum_var S) (ebool true) :- member L S.
+
+eval_unop isNum V (ebool false) :- not (eq V (eint _)).
+eval_unop isBool V (ebool false) :- not (eq V (ebool _)).
+eval_unop isStr V (ebool false) :- not (eq V (estr _)).
+eval_unop isRec V (ebool false) :- not (eq V (rec_val _ _)).
+eval_unop isFun V (ebool false) :- not (eq V (lam _)).
+eval_unop (isEnumIn L) (enum_var S) (ebool false) :- not (member L S).
+eval_unop (isEnumIn _) V (ebool false) :- not (eq V (enum_var _)).
+
+(* Typing *)
+(* Promises don't perform any computation *)
+eval (promise _ T) V :-
+  eval T V.
+
+eval (assume Ty L T) V :-
+  typToExpr Ty CTy,
+  eval (app (app CTy L) T) V.
+
+(* Variables *)
+eval (named X) _ :- print `unknown variable ${X}`, failure.
diff --git a/makam-spec/src/examples.makam b/makam-spec/src/examples.makam
new file mode 100644
index 00000000..bfd806e3
--- /dev/null
+++ b/makam-spec/src/examples.makam
@@ -0,0 +1,16 @@
+print "Lets try side effects!" ?
+
+print "Return 3 -- Lets are lazy" ?
+side_effect : expr.
+eval (side_effect) (eint 1) :- 
+    print "Side Effect!!".
+
+(isocast "
+fun se => let (f = se) in (f + f) + f
+" (E: expr), eval (app E side_effect) Res) ?
+
+print "Return 2 -- functions as well" ?
+
+(isocast "
+fun se => (fun x => x + x) se
+" (E: expr), eval (app E side_effect) Res) ?
diff --git a/makam-spec/src/init.makam b/makam-spec/src/init.makam
new file mode 100644
index 00000000..ce20e041
--- /dev/null
+++ b/makam-spec/src/init.makam
@@ -0,0 +1,54 @@
+%use "ast".
+%use "syntax".
+%use "eval".
+%use "typecheck".
+%use "utils".
+
+cleanTypedName, cleanTyp_ : dyn -> dyn -> prop.
+
+cleanTypedName X Y :-
+  unless (cleanTyp_ X Y) (structural_map cleanTypedName X Y).
+
+cleanTyp_ (dyn X) (dyn N) :-
+  not (refl.isunif X), eq X (typedName Name _), eq N (named Name).
+
+changeToDyn : typ -> typ -> prop.
+changeToDyn A tdyn when refl.isunif A.
+changeToDyn (tarrow S T) (tarrow CS CT) :-
+  changeToDyn S CS,
+  changeToDyn T CT.
+changeToDyn A A when not (refl.isunif A).
+
+removeThunks, removeThunks_ : dyn -> dyn -> prop.
+
+removeThunks X Y :- demand.case_otherwise (removeThunks_  X Y) (structural_map removeThunks X Y).
+
+removeThunks_ (dyn (thunk S A B)) (dyn (named S)) .
+removeThunks_ (dyn (recThunk S A B)) (dyn (named S)) .
+
+(* Parse, typecheck and interpret *)
+raw_interpreter : string -> expr -> typ -> prop.
+raw_interpreter S V Ty :-
+  either (isocast S (E: expr)) (log_error S `Parse error in Nickel program`),
+  once (ifte (and (typecheck E Ty') (cleanTypedName (dyn Ty') (dyn Ty))) 
+    (print "Typechecked!")
+    (and (print `Could not typecheck`) (failure))),
+  eval E V,
+  print "Evaluated".
+
+(* Parse, typecheck, interpret and pretty print *)
+interpreter : string -> string -> string -> prop.
+interpreter S S' STy :-
+  raw_interpreter S V T',
+  once (changeToDyn T' T), (* The printer will fail if any uninstantiated variable is in the Type *)
+  removeThunks (dyn V) (dyn V'),
+  isocast V' (S': string),
+  isocast T (STy: string).
+
+(* Parse and typecheck *)
+p_typecheck : string -> typ -> prop.
+p_typecheck S Ty :-
+  either (isocast S (E: expr)) (log_error S `Parse error in Nickel program`),
+  once (ifte (and (typecheck E Ty') (cleanTypedName (dyn Ty') (dyn Ty))) 
+    (print "Typechecked!")
+    (and (print `Could not typecheck`) (failure))).
diff --git a/makam-spec/src/row.makam b/makam-spec/src/row.makam
new file mode 100644
index 00000000..4a0a36d2
--- /dev/null
+++ b/makam-spec/src/row.makam
@@ -0,0 +1,95 @@
+row : type -> type.
+
+(* A row is like a set, but extendable on the back,
+ * and lazy, in some sense of lazyness *)
+
+extend : A -> row A -> row A.
+closed : row A.
+
+%extend row.
+(* This forall doesn't eagerly instantiate the back of the row *)
+forall : (A -> prop) -> row A -> prop.
+forall F R :-
+    guard R (ifte (eq (extend X R') R) (and (F X) (forall F R')) (eq closed R)).
+
+
+(* An empty, extendable, row *)
+empty : row A -> prop.
+empty A :- refl.isunif A.
+
+(* To close a row, can't use forall, must be eager *)
+close : row A -> prop.
+close closed.
+close R :-
+    not (empty R),
+    eq (extend _ R') R,
+    close R'.
+
+lacks : A -> row A -> prop.
+lacks A R :-
+    forall (pfun X => not (eqv X A)) R.
+
+(* Notice that member and add are not the same *)
+member : row A -> A -> prop.
+member R A :-
+  not (empty R),
+  eq (extend A' R') R,
+  unless (eqv A A') (member R' A).
+
+add : A -> row A -> prop.
+add A R :-
+    member R A.
+add A R :-
+    empty R,
+    eq (extend A R') R,
+    lacks A R'.
+add A R :-
+    not (empty R),
+    eq (extend A' R') R,
+    not (eqv A A'),
+    add A R'.
+
+remove : A -> row A -> row A -> prop.
+remove A R R' :-
+    member R A,
+    not (empty R),
+    eq (extend A' R'') R,
+    ifte (eqv A A')
+        (eq R' R'')
+        (and (remove A R'' R''') (eq R' (extend A' R'''))).
+
+(* fromList gives you the non-closed version, use close to close it *)
+fromList : list A -> row A -> prop.
+fromList [] R :-
+    empty R.
+fromList (HD :: TL) RTL :-
+    fromList TL RTL,
+    once (add HD RTL). (* TODO, I dont remember why this has once *)
+
+toList : row A -> list A -> prop.
+toList R [] :-
+    empty R.
+toList closed [].
+toList (extend A R) (A :: TL) :-
+    toList R TL.
+
+%end.
+
+(* This disables the builtin eqv relation for rows *)
+without_eqv_refl (_: row A).
+
+(* This unifies their definitions by expanding them *)
+eqv (R: row A) S :-
+    row.empty R, row.empty S, eq R S.
+eqv (R: row A) S :-
+    row.empty R, not (row.empty S), eqv S R.
+eqv (R: row A) S :-
+    not (row.empty R),
+    eq R closed,
+    eq S closed.
+eqv (R: row B) S :-
+    not (row.empty R),
+    eq (extend A R') R,
+    row.add A S, (* If S doesnt have A and it's closed, this line fails *)
+    row.remove A S S',
+    eqv R' S'.
diff --git a/makam-spec/src/syntax.makam b/makam-spec/src/syntax.makam
new file mode 100644
index 00000000..2b455b95
--- /dev/null
+++ b/makam-spec/src/syntax.makam
@@ -0,0 +1,157 @@
+%use "ast".
+%use "row".
+
+%open syntax.
+
+expr_, baseexpr : syntax expr.
+expr_concrete : syntax (concrete expr).
+id : syntax (concrete.name expr).
+idTy : syntax (concrete.name typ).
+binop, binopC : syntax binop.
+unop, unopC : syntax unop.
+
+typ, typC, baseTyp: syntax typ.
+ctenum : (list string) -> typ.
+
+rec_field : syntax rec_field.
+rec_field_typ : syntax (tuple string typ).
+
+switch_def : syntax (tuple string expr).
+
+exprvar : concrete.namespace expr.
+typvar : concrete.namespace typ.
+
+token_ARROW : syntax unit.
+token_FATARROW : syntax unit.
+token_PROD : syntax unit.
+
+`( syntax_rules {{
+
+token_ARROW -> { <token "→"> } / { <token "->"> }
+token_FATARROW -> { <token "⇒"> } / { <token "=>"> }
+token_PROD -> { <token "×"> } / { <token "*"> }
+
+binop ->
+        (fun u => add) { <token "+"> }
+      / (fun u => sub) { <token "-"> }
+      / (fun u => mul) { <token "*"> }
+
+unop ->
+        blame { "blame" }
+      / isNum { "isNum" }
+      / isBool { "isBool" }
+      / isStr { "isStr" }
+      / isRec { "isRec" }
+      / isFun { "isFun" }
+      / isEnumIn { "is<" <list_sep (token ",") makam.ident> ">" }
+
+}} ).
+
+`( syntax.def_js binopC binop ).
+`( syntax.def_js unopC unop ).
+
+`( syntax_rules {{
+
+expr_concrete -> concrete { <expr_> }
+
+expr_ -> ite 
+        { "Ifte(" <expr_> "," <expr_> "," <expr_> ")" }
+      / (fun id => fun body => lam (concrete.bindone id body))
+        { "fun" <id> token_FATARROW <expr_> }
+      / fun id => fun def => fun body => 
+        let (concrete.bindone id def) (concrete.bindone id body)
+        { "let" "(" <id> "=" <expr_> ")" "in" <expr_> }
+      / ebinop
+        { <baseexpr> <binopC> <baseexpr> }
+      / eunop
+        { <unopC> <baseexpr> }
+      / static_access
+        { <baseexpr> "." <makam.ident> }
+      / dyn_access
+        { <baseexpr> ".$" <baseexpr> }
+      / fun e => fun defs => enum_case e defs none
+        { "switch" <baseexpr> "{" <list_sep (token ",") switch_def> "}"}
+      / fun e => fun defs => fun default => enum_case e defs (some default)
+        { "switch" <baseexpr> "{" <list_sep (token ",") switch_def> "," "@" "=>" <baseexpr> "}"}
+      / app
+        { <baseexpr>  <expr_> }
+      / { <baseexpr> }
+
+baseexpr ->
+        promise
+        { "Promise(" <typ> "," <expr_> ")"}
+      / fun ty => assume ty (label true "Assume Positive" "Assume Negative" "The contract itself (Negative)")
+        { "Assume(" <typ> "," <expr_> ")"}
+      / ebool true { "true" }
+      / ebool false { "false" }
+      / erec 
+        {"{" <list_sep (token ";") rec_field> "}"}
+      / estr { <makam.string_literal> }
+      / concrete.var
+        { <id> }
+      / enum_var
+        { "`" <makam.ident> }
+      / eint
+        { <makam.int_literal> }
+      / named 
+        { <makam.ident> }
+      / { "(" <expr_> ")" }
+
+rec_field ->
+        static_field
+        { <makam.ident> ":" <expr_>}
+      / dyn_field
+        { "$" <expr_> ":" <expr_>}
+
+switch_def -> tuple
+            { <makam.ident> "=>" <baseexpr>}
+
+id -> concrete.name exprvar
+        { <makam.ident> }
+
+idTy -> concrete.name typvar
+        { <makam.ident> }
+
+
+typ -> (fun idT => fun body => forall (concrete.bindone idT body))
+        { "forall" <idTy> "." <typ> }
+      / tarrow
+        { <baseTyp> "->" <typ> }
+      / { <baseTyp> }
+
+baseTyp ->  
+        tnum 
+        { "Num" }
+      / tbool
+        { "Bool" }
+      / tdyn
+        { "Dyn" }
+      / tstr
+        { "String" }
+      / ctenum 
+        { "<" <list_sep (token ",") makam.ident> ">" }
+      / concrete.var
+        { <idTy> }
+      / open_rec
+        {"{" "_" ":" <typ> "," <list_sep (token ",") rec_field_typ> "}"}
+      / clos_rec
+        {"{" <list_sep (token ",") rec_field_typ> "}"}
+      / fromExpr
+        { "#" <expr_> }
+      / { "(" <typ> ")" }
+
+rec_field_typ ->
+        tuple
+        {<makam.ident> ":" <typ>}
+
+}} ).
+
+`( syntax.def_toplevel_js expr_concrete ).
+
+concrete.pick_namespace_userdef (_: expr) exprvar.
+concrete.pick_namespace_userdef (_: typ) typvar.
+
+concrete.handle_unresolved_name (concrete.name exprvar ID) (named ID).
+
+concrete.resolve_conversion (ctenum L) (tenum R) :-
+    row.fromList L R, row.close R.
diff --git a/makam-spec/src/typecheck.makam b/makam-spec/src/typecheck.makam
new file mode 100644
index 00000000..58f8dd14
--- /dev/null
+++ b/makam-spec/src/typecheck.makam
@@ -0,0 +1,186 @@
+%use "ast".
+%use "utils".
+
+typecheck : expr -> typ -> prop.
+typecheckTypes : typ -> prop.
+
+(* instantiates all the head forall *)
+instantiate : typ -> typ -> prop.
+
+instantiate Ty Ty' :-
+    not (refl.isunif Ty),
+    eq Ty (forall (bind _ F)),
+    instantiate (F X) Ty'.
+instantiate Ty Ty :-
+    or 
+        (refl.isunif Ty)
+        (not (eq Ty (forall _))).
+
+(* This is hack to quickly fix 
+ * https://github.com/astampoulis/makam/issues/66
+ * The idea is to introduce a new kind of expr (typedName : string -> typ -> expr)
+ * that stores the type given to a particular bound variable, rather than introducing
+ * new rules to the program context.
+ *)
+typedName : string -> typ -> expr.
+
+typecheck (typedName _ Ty) Ty'' :-
+    instantiate Ty Ty',
+    eqv Ty' Ty''.
+
+(* End of hack *)
+
+typecheck (let (bind Name E) (bind Name B)) T :-
+    typecheck (E (typedName Name T')) T'',
+    eqv T' T'',
+    typecheck (B (typedName Name T')) T''',
+    eqv T T'''.
+    
+typecheck (lam (bind Name B)) (tarrow S T) :-
+    typecheck (B (typedName Name S)) T',
+    eqv T T'.
+
+typecheck (app A B) T :-
+    typecheck A (tarrow S T),
+    typecheck B S',
+    eqv S S'.
+
+typecheck (eint _) tnum.
+typecheck (ebool _) tbool.
+typecheck (estr _) tstr.
+
+(* I'm not checking for uniqueness still *)
+typecheck (erec []) (clos_rec []).
+typecheck (erec ((static_field K V) :: TL)) (clos_rec L) :-
+    find L K (TyV, L'),
+    typecheck V TyV,
+    typecheck (erec TL) (clos_rec L').
+
+
+typecheck (erec []) (open_rec _ []).
+typecheck (erec ((static_field K V) :: TL)) (open_rec DT L) :-
+    find L K (TyV, L'),
+    typecheck V TyV,
+    typecheck (erec TL) (open_rec DT L').
+typecheck (erec ((static_field K V) :: TL)) (open_rec DT L) :-
+    not (find L K _),
+    typecheck V DT,
+    typecheck (erec TL) (open_rec DT L).
+typecheck (erec ((dyn_field K V) :: TL)) (open_rec DT L) :-
+    typecheck K tstr,
+    typecheck V DT,
+    typecheck (erec TL) (open_rec DT L).
+
+typecheck (static_access E S) T :-
+    typecheck E (open_rec _ L),
+    find L S (T, _).
+typecheck (static_access E S) T :-
+    typecheck E (open_rec T L).
+typecheck (static_access E S) T :-
+    typecheck E (clos_rec L),
+    find L S (T', _),
+    eqv T' T.
+
+typecheck (dyn_access E _) T :-
+    typecheck E (open_rec T _).
+
+(* Enumerations *)
+
+typecheck (enum_var S) (tenum R) :-
+    row.empty R,
+    row.add S R.
+
+typecheck (enum_case E L D) Ty :-
+    row.empty R,
+    map (pfun (Tag, Ex) => row.add Tag R, typecheck Ex Ty) L,
+    ifte (eq D (some DEx))
+        (typecheck DEx Ty)
+        (row.close R),
+    typecheck E (tenum RE),
+    eqv RE R.
+
+typecheck (ite C T E) Ty :-
+    typecheck C tbool,
+    typecheck T Ty',
+    typecheck E Ty'',
+    eqv Ty Ty',
+    eqv Ty Ty''.
+
+typecheck (eunop blame L) _ :-
+    typecheck L tlbl.
+    
+typecheck (eunop isNum _) tbool.
+typecheck (eunop isBool _) tbool.
+typecheck (eunop isStr _) tbool.
+typecheck (eunop isRec _) tbool.
+typecheck (eunop isFun _) tbool.
+typecheck (eunop (isEnumIn _) _) tbool.
+
+typecheck (ebinop A _ B) tnum :-
+    typecheck A tnum,
+    typecheck B tnum.
+
+typecheck E Ty :-
+    not (refl.isunif Ty),
+    eq Ty (forall (bind _ F)),
+    (x: typ ->
+        typecheck E (F x)).
+
+(* A forall is only typechecked when explicitely asked for it, via a promise *)
+typecheck (promise Ty E) Ty :-
+    eq Ty (forall _),
+    typecheckTypes Ty,
+    typecheck E Ty.
+typecheck (promise Ty E) Ty :-
+    not (eq Ty (forall _)),
+    typecheckTypes Ty,
+    typecheck E Ty',
+    eqv Ty' Ty.
+typecheck (promise Ty E) _ :-
+    typecheckTypes Ty,
+    not (typecheck E Ty),
+    log_error Ty `Couldnt check Promise(...)`,
+    failure.
+
+(* The type of an Assume construct doesn't depend on the term *)
+typecheck (assume Ty L E) Ty :- 
+    typecheckTypes Ty,
+    typecheck L tlbl,
+    typecheck E _.
+
+typecheck (label _ _ _ _) tlbl.
+
+typecheck_dyn : dyn -> prop.
+typecheck_dyn (dyn A) :-
+    typecheck A _.
+typecheck_dyn (dyn A) :-
+    not (typeq A (X: typ)),
+    structural_map0 typecheck_dyn (dyn A).
+
+typecheck A tdyn :-
+    not (eq A (promise _ _)),
+    (* Still traverse *)
+    structural_map0 typecheck_dyn (dyn A).
+
+typecheckTypes_ : dyn -> prop.
+
+typecheckTypes A :- typecheckTypes_ (dyn A).
+
+typecheckTypes_ (dyn A) :-
+    case A [
+        (fromExpr E, typecheck E (tarrow tlbl (tarrow S S))),
+        (Other, structural_map0 typecheckTypes_ (dyn Other))
+    ].
+typecheckTypes_ (dyn B) :-
+    not (typeq B (X: typ)),
+    structural_map0 typecheckTypes_ (dyn B).
+
+(* This disables the builtin eqv relation for typs *)
+without_eqv_refl (_: typ).
+
+(* This unifies their definitions by expanding them *)
+eqv (T: typ) S when or (not(refl.isunif T)) (not(refl.isunif S)):-
+    structural_map (pfun (dyn A) (dyn B) => eqv A B) (dyn T) (dyn S).
+
+eqv (T: typ) S when refl.isunif T, refl.isunif S :-
+    eq S T.
diff --git a/makam-spec/src/utils.makam b/makam-spec/src/utils.makam
new file mode 100644
index 00000000..00f8c933
--- /dev/null
+++ b/makam-spec/src/utils.makam
@@ -0,0 +1,87 @@
+typeq : [B] A -> B -> prop.
+typeq (X : A) (Y : A).
+
+map0 : (A -> prop) -> list A -> prop.
+map0 P nil.
+map0 P (cons HD TL) <- P HD, map0 P TL.
+
+(* TODO: For some reason I can't make the stdlib structural work.
+I tried finding the error, but I couldn't, copying this implementation
+solves the problem for now, but eventually it would make sense to do it with th builtin one.
+*)
+structural_map : (dyn -> dyn -> prop) -> dyn -> dyn -> prop.
+
+(* defer if both input and output are uninstantiated metavariables *)
+(structural_map Rec (dyn (X : A)) (dyn (Y : A))) when refl.isunif X, refl.isunif Y <-
+  guardmany [ X , Y ] (Rec (dyn X) (dyn Y)).
+
+(* deal with built-in types *)
+structural_map Rec (dyn (X : string)) (dyn (X : string)).
+structural_map Rec (dyn (X : int)) (dyn (X : int)).
+structural_map Rec (dyn (X : A -> B)) (dyn (Y : A -> B)) <-
+  (x:A -> Rec (dyn (X x)) (dyn (Y x))).
+
+(* the essence: forward and backward destructuring *)
+
+(structural_map Rec (dyn (X : A)) (dyn (Y : A)))
+when not(typeq X (B : C -> D)), not(refl.isunif X), refl.isunif Y <-
+  refl.headargs X Hd Args,
+  map Rec Args Args',
+  refl.headargs Y Hd Args'.
+
+(structural_map Rec (dyn (X : A)) (dyn (Y : A)))
+when not(typeq X (B : C -> D)), refl.isunif X, not(refl.isunif Y) <-
+  refl.headargs Y Hd Args',
+  map Rec Args Args',
+  refl.headargs X Hd Args.
+
+(structural_map Rec (dyn (X : A)) (dyn (Y : A)))
+when not(typeq X (B : C -> D)), not(refl.isunif X), not(refl.isunif Y) <-
+  refl.headargs X Hd Args,
+  refl.headargs Y Hd Args',
+  map Rec Args Args'.
+
+structural_map0 : (dyn -> prop) -> dyn -> prop.
+
+(* defer if both input and output are uninstantiated metavariables *)
+(structural_map0 Rec (dyn (X : A))) when refl.isunif X <-
+  guard X (Rec (dyn X)).
+
+(* deal with built-in types *)
+structural_map0 Rec (dyn (X : string)).
+structural_map0 Rec (dyn (X : int)).
+structural_map0 Rec (dyn (X : A -> B)) <-
+  (x:A -> Rec (dyn (X x))).
+
+(* the essence: forward and backward destructuring *)
+
+(structural_map0 Rec (dyn (X : A)))
+when not(typeq X (B : C -> D)), not(refl.isunif X) <-
+  refl.headargs X Hd Args,
+  map0 Rec Args.
+
+case : A -> (list (tuple A prop)) -> prop.
+case Scrutinee ( (Pattern, Body) :: Rest ) <-
+  if eq Scrutinee Pattern then Body else case Scrutinee Rest.
+
+(* List *)
+
+find : (list (tuple A B)) -> A -> (tuple B (list (tuple A B))) -> prop.
+find ((K, V) :: TL) K (V, TL).
+find ((K, V) :: TL) K' (V', (K, V) :: TL') :-
+  not (eq K K'),
+  find TL K' (V', TL').
+
+member : (list A) -> A -> prop.
+member (X :: _) X.
+member (X :: TL) Y :-
+  not (eq X Y), member TL Y.
+
+keys : (list (tuple A B)) -> (list A) -> prop.
+keys L K :-
+  map (pfun (X, Y) X => success) L K.
+
+eq_unord : (list A) -> (list A) -> prop.
+eq_unord X Y :-
+  map (fun e => find (eq e) Y _) X,
+  map (fun e => find (eq e) X _) Y.
diff --git a/nickel-wasm-repl/Cargo.toml b/nickel-wasm-repl/Cargo.toml
deleted file mode 100644
index 080243f5..00000000
--- a/nickel-wasm-repl/Cargo.toml
+++ /dev/null
@@ -1,17 +0,0 @@
-[package]
-name = "nickel-repl"
-version = "0.1.0"
-authors = ["Nickel team"]
-license = "MIT"
-readme = "README.md"
-description = "WebAssembly REPL for the Nickel programming language."
-homepage = "https://nickel-lang.org"
-repository = "https://github.com/tweag/nickel"
-keywords = ["configuration", "language", "nix", "nickel"]
-edition = "2018"
-
-[dependencies]
-nickel-lang = {default-features = false, path = "../", version = "0.1.0", features=["repl-wasm"]}
-
-[lib]
-crate-type = ["cdylib", "rlib"]
diff --git a/nickel-wasm-repl/src/lib.rs b/nickel-wasm-repl/src/lib.rs
deleted file mode 100644
index 01a59956..00000000
--- a/nickel-wasm-repl/src/lib.rs
+++ /dev/null
@@ -1,1 +0,0 @@
-pub use nickel_lang::*;
diff --git a/src/bin/nickel.rs b/src/bin/nickel.rs
index 2cd20e67..a0eafc44 100644
--- a/src/bin/nickel.rs
+++ b/src/bin/nickel.rs
@@ -77,8 +77,8 @@ enum Command {
     #[cfg(feature = "doc")]
     Doc {
         /// Specify the path of the generated documentation file. Default to
-        /// `~/.nickel/doc/<input-file>.md` for input `<input-file>.ncl`, or to
-        /// `~/.nickel/doc/out.md` if the input is read from stdin.
+        /// `~/.nickel/doc/<input-file>.md` for input `<input-file>.ncl`. `<input-file>.md` is set
+        /// to `out.md` when the input comes from stdin.
         #[structopt(short = "o", long, parse(from_os_str))]
         output: Option<PathBuf>,
     },
diff --git a/src/cache.rs b/src/cache.rs
index 7bd574a4..abac08a3 100644
--- a/src/cache.rs
+++ b/src/cache.rs
@@ -6,7 +6,7 @@ use crate::position::TermPos;
 use crate::stdlib as nickel_stdlib;
 use crate::term::{RichTerm, SharedTerm, Term};
 use crate::transform::import_resolution;
-use crate::typecheck::{self, Wildcards};
+use crate::typecheck::{self, TypeCheckingOutput, Wildcards};
 use crate::typecheck::{linearization::StubHost, type_check};
 use crate::types::UnboundTypeVariableError;
 use crate::{eval, parser, transform};
@@ -440,7 +440,7 @@ impl Cache {
             }
             Some(CachedTerm { term, state, .. }) if *state >= EntryState::Parsed => {
                 if *state < EntryState::Typechecking {
-                    let (wildcards, _) =
+                    let (TypeCheckingOutput { wildcards, .. }, _) =
                         type_check(term, global_env, self, StubHost::<(), (), _>::new())?;
                     self.update_state(file_id, EntryState::Typechecking);
                     self.wildcards.insert(file_id, wildcards);
@@ -698,7 +698,8 @@ impl Cache {
             return Err(Error::ParseErrors(errs));
         }
         let (term, pending) = import_resolution::resolve_imports(term, self)?;
-        let (wildcards, _) = type_check(&term, global_env, self, StubHost::<(), (), _>::new())?;
+        let (TypeCheckingOutput { wildcards, .. }, _) =
+            type_check(&term, global_env, self, StubHost::<(), (), _>::new())?;
         let term = transform::transform(term, Some(&wildcards))
             .map_err(|err| Error::ParseErrors(err.into()))?;
         Ok((term, pending))
diff --git a/src/eval/operation.rs b/src/eval/operation.rs
index 1e442e8a..d1c72cda 100644
--- a/src/eval/operation.rs
+++ b/src/eval/operation.rs
@@ -23,7 +23,7 @@ use crate::{
     serialize::ExportFormat,
     term::{make as mk_term, ArrayAttrs},
     term::{BinaryOp, NAryOp, RichTerm, StrChunk, Term, UnaryOp},
-    transform::{fresh_var, Closurizable},
+    transform::Closurizable,
 };
 use md5::digest::Digest;
 use simple_counter::*;
@@ -180,23 +180,30 @@ fn process_unary_operation(
                 ))
             }
         }
-        UnaryOp::Typeof() => {
-            let result = match *t {
-                Term::Num(_) => "Num",
-                Term::Bool(_) => "Bool",
-                Term::Str(_) => "Str",
-                Term::Enum(_) => "Enum",
-                Term::Fun(..) => "Fun",
-                Term::Array(..) => "Array",
-                Term::Record(..) | Term::RecRecord(..) => "Record",
-                Term::Lbl(..) => "Lbl",
-                _ => "Other",
-            };
-            Ok(Closure::atomic_closure(RichTerm::new(
-                Term::Enum(Ident::from(result)),
-                pos_op_inh,
-            )))
-        }
+        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::IsArray() => Ok(Closure::atomic_closure(RichTerm::new(
+            Term::Bool(matches!(*t, Term::Array(..))),
+            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.
         {
@@ -932,21 +939,19 @@ fn process_unary_operation(
             }
         }
         UnaryOp::ToStr() => {
-            let result = match_sharedterm! {t, with {
+            let result = match &*t {
                 Term::Num(n) => Ok(Term::Str(n.to_string())),
-                Term::Str(s) => Ok(Term::Str(s)),
+                Term::Str(s) => Ok(Term::Str(s.clone())),
                 Term::Bool(b) => Ok(Term::Str(b.to_string())),
                 Term::Enum(id) => Ok(Term::Str(id.to_string())),
-                Term::Null => Ok(Term::Str(String::from("null"))),
-            } else {
-                Err(EvalError::Other(
+                t => Err(EvalError::Other(
                     format!(
                         "strFrom: can't convert the argument of type {} to string",
                         t.type_of().unwrap()
                     ),
                     pos,
-                ))
-            }}?;
+                )),
+            }?;
             Ok(Closure::atomic_closure(RichTerm::new(result, pos_op_inh)))
         }
         UnaryOp::NumFromStr() => {
@@ -982,116 +987,6 @@ fn process_unary_operation(
                 ))
             }
         }
-        UnaryOp::StrIsMatch() => {
-            if let Term::Str(s) = &*t {
-                let re = regex::Regex::new(s)
-                    .map_err(|err| EvalError::Other(err.to_string(), pos_op))?;
-
-                let param = fresh_var();
-                let matcher = Term::Fun(
-                    param.clone(),
-                    RichTerm::new(
-                        Term::Op1(
-                            UnaryOp::StrIsMatchCompiled(re.into()),
-                            RichTerm::new(Term::Var(param), pos_op_inh),
-                        ),
-                        pos_op_inh,
-                    ),
-                );
-
-                Ok(Closure::atomic_closure(RichTerm::new(matcher, pos)))
-            } else {
-                Err(EvalError::TypeError(
-                    String::from("Str"),
-                    String::from("str_is_match"),
-                    arg_pos,
-                    RichTerm { term: t, pos },
-                ))
-            }
-        }
-        UnaryOp::StrMatch() => {
-            if let Term::Str(s) = &*t {
-                let re = regex::Regex::new(s)
-                    .map_err(|err| EvalError::Other(err.to_string(), pos_op))?;
-
-                let param = fresh_var();
-                let matcher = Term::Fun(
-                    param.clone(),
-                    RichTerm::new(
-                        Term::Op1(
-                            UnaryOp::StrMatchCompiled(re.into()),
-                            RichTerm::new(Term::Var(param), pos_op_inh),
-                        ),
-                        pos_op_inh,
-                    ),
-                );
-
-                Ok(Closure::atomic_closure(RichTerm::new(matcher, pos)))
-            } else {
-                Err(EvalError::TypeError(
-                    String::from("Str"),
-                    String::from("str_match"),
-                    arg_pos,
-                    RichTerm { term: t, pos },
-                ))
-            }
-        }
-        UnaryOp::StrIsMatchCompiled(regex) => {
-            if let Term::Str(s) = &*t {
-                Ok(Closure::atomic_closure(RichTerm::new(
-                    Term::Bool(regex.is_match(s)),
-                    pos_op_inh,
-                )))
-            } else {
-                Err(EvalError::TypeError(
-                    String::from("Str"),
-                    String::from("str_is_match_compiled"),
-                    arg_pos,
-                    RichTerm { term: t, pos },
-                ))
-            }
-        }
-        UnaryOp::StrMatchCompiled(regex) => {
-            if let Term::Str(s) = &*t {
-                let capt = regex.captures(s);
-                let result = if let Some(capt) = capt {
-                    let first_match = capt.get(0).unwrap();
-                    let groups: Vec<RichTerm> = capt
-                        .iter()
-                        .skip(1)
-                        .map(|s_opt| {
-                            s_opt.map(|s| RichTerm::from(Term::Str(String::from(s.as_str()))))
-                        })
-                        .flatten()
-                        .collect();
-
-                    mk_record!(
-                        ("match", Term::Str(String::from(first_match.as_str()))),
-                        ("index", Term::Num(first_match.start() as f64)),
-                        (
-                            "groups",
-                            Term::Array(groups, ArrayAttrs { closurized: true })
-                        )
-                    )
-                } else {
-                    //FIXME: what should we return when there's no match?
-                    mk_record!(
-                        ("match", Term::Str(String::new())),
-                        ("index", Term::Num(-1.)),
-                        ("groups", Term::Array(Vec::new(), Default::default()))
-                    )
-                };
-
-                Ok(Closure::atomic_closure(result))
-            } else {
-                Err(EvalError::TypeError(
-                    String::from("Str"),
-                    String::from("str_match_compiled"),
-                    arg_pos,
-                    RichTerm { term: t, pos },
-                ))
-            }
-        }
     }
 }
 
@@ -2147,6 +2042,92 @@ fn process_binary_operation(
                 },
             )),
         },
+        BinaryOp::StrIsMatch() => match (&*t1, &*t2) {
+            (Term::Str(s1), Term::Str(s2)) => {
+                let re = regex::Regex::new(s2)
+                    .map_err(|err| EvalError::Other(err.to_string(), pos_op))?;
+
+                Ok(Closure::atomic_closure(RichTerm::new(
+                    Term::Bool(re.is_match(s1)),
+                    pos_op_inh,
+                )))
+            }
+            (Term::Str(_), _) => Err(EvalError::TypeError(
+                String::from("Str"),
+                String::from("strIsMatch, 2nd argument"),
+                snd_pos,
+                RichTerm {
+                    term: t2,
+                    pos: pos2,
+                },
+            )),
+            (_, _) => Err(EvalError::TypeError(
+                String::from("Str"),
+                String::from("strIsMatch, 1st argument"),
+                fst_pos,
+                RichTerm {
+                    term: t1,
+                    pos: pos1,
+                },
+            )),
+        },
+        BinaryOp::StrMatch() => {
+            match (&*t1, &*t2) {
+                (Term::Str(s1), Term::Str(s2)) => {
+                    let re = regex::Regex::new(s2)
+                        .map_err(|err| EvalError::Other(err.to_string(), pos_op))?;
+                    let capt = re.captures(s1);
+
+                    let result = if let Some(capt) = capt {
+                        let first_match = capt.get(0).unwrap();
+                        let groups: Vec<RichTerm> = capt
+                            .iter()
+                            .skip(1)
+                            .map(|s_opt| {
+                                s_opt.map(|s| RichTerm::from(Term::Str(String::from(s.as_str()))))
+                            })
+                            .flatten()
+                            .collect();
+
+                        mk_record!(
+                            ("match", Term::Str(String::from(first_match.as_str()))),
+                            ("index", Term::Num(first_match.start() as f64)),
+                            (
+                                "groups",
+                                Term::Array(groups, ArrayAttrs { closurized: true })
+                            )
+                        )
+                    } else {
+                        //FIXME: what should we return when there's no match?
+                        mk_record!(
+                            ("match", Term::Str(String::new())),
+                            ("index", Term::Num(-1.)),
+                            ("groups", Term::Array(Vec::new(), Default::default()))
+                        )
+                    };
+
+                    Ok(Closure::atomic_closure(result))
+                }
+                (Term::Str(_), _) => Err(EvalError::TypeError(
+                    String::from("Str"),
+                    String::from("strMatch, 2nd argument"),
+                    snd_pos,
+                    RichTerm {
+                        term: t2,
+                        pos: pos2,
+                    },
+                )),
+                (_, _) => Err(EvalError::TypeError(
+                    String::from("Str"),
+                    String::from("strMatch, 1st argument"),
+                    fst_pos,
+                    RichTerm {
+                        term: t1,
+                        pos: pos1,
+                    },
+                )),
+            }
+        }
     }
 }
 
diff --git a/src/eval/stack.rs b/src/eval/stack.rs
index a3043df7..bb7588cb 100644
--- a/src/eval/stack.rs
+++ b/src/eval/stack.rs
@@ -346,7 +346,7 @@ mod tests {
     }
 
     fn some_cont() -> OperationCont {
-        OperationCont::Op1(UnaryOp::Typeof(), TermPos::None)
+        OperationCont::Op1(UnaryOp::IsNum(), TermPos::None)
     }
 
     fn some_arg_marker() -> Marker {
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index da72053f..16093a2c 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -502,15 +502,6 @@ StaticString: String = StringStart <s: ChunkLiteral?> StringEnd => s.unwrap_or_d
 EnumTag: Ident = {
     <Ident>,
     <StaticString> => <>.into(),
-    // Allow tags of the form `Str, `Bool, etc. This is ad-hoc and should
-    // eventually be replaced with a proper lexing of enum tags, but this is not
-    // a trivial task. For now, to make builtin.typeof usable, we just
-    // special-case builtin types.
-    "Dyn" => "Dyn".into(),
-    "Num" => "Num".into(),
-    "Bool" => "Bool".into(),
-    "Str" => "Str".into(),
-    "Array" => "Array".into(),
 }
 
 ChunkLiteralPart: ChunkLiteralPart<'input> = {
@@ -520,7 +511,12 @@ ChunkLiteralPart: ChunkLiteralPart<'input> = {
 };
 
 UOp: UnaryOp = {
-    "typeof" => UnaryOp::Typeof(),
+    "is_num" => UnaryOp::IsNum(),
+    "is_bool" => UnaryOp::IsBool(),
+    "is_str" => UnaryOp::IsStr(),
+    "is_fun" => UnaryOp::IsFun(),
+    "is_array" => UnaryOp::IsArray(),
+    "is_record" => UnaryOp::IsRecord(),
     "blame" => UnaryOp::Blame(),
     "chng_pol" => UnaryOp::ChangePolarity(),
     "polarity" => UnaryOp::Pol(),
@@ -549,8 +545,6 @@ UOp: UnaryOp = {
     "str_from" => UnaryOp::ToStr(),
     "num_from" => UnaryOp::NumFromStr(),
     "enum_from" => UnaryOp::EnumFromStr(),
-    "str_is_match" => UnaryOp::StrIsMatch(),
-    "str_match" => UnaryOp::StrMatch(),
 };
 
 SwitchCase: SwitchCase = {
@@ -728,6 +722,8 @@ BOpPre: BinaryOp = {
     "pow" => BinaryOp::Pow(),
     "str_split" => BinaryOp::StrSplit(),
     "str_contains" => BinaryOp::StrContains(),
+    "str_match" => BinaryOp::StrMatch(),
+    "str_is_match" => BinaryOp::StrIsMatch(),
     "record_insert" => BinaryOp::DynExtend(),
     "record_remove" => BinaryOp::DynRemove(),
 }
@@ -845,7 +841,12 @@ extern {
         "Array" => Token::Normal(NormalToken::Array),
 
         "tag" => Token::Normal(NormalToken::Tag),
-        "typeof" => Token::Normal(NormalToken::Typeof),
+        "is_num" => Token::Normal(NormalToken::IsNum),
+        "is_bool" => Token::Normal(NormalToken::IsBool),
+        "is_str" => Token::Normal(NormalToken::IsStr),
+        "is_fun" => Token::Normal(NormalToken::IsFun),
+        "is_array" => Token::Normal(NormalToken::IsArray),
+        "is_record" => Token::Normal(NormalToken::IsRecord),
         "assume" => Token::Normal(NormalToken::Assume),
         "blame" => Token::Normal(NormalToken::Blame),
         "chng_pol" => Token::Normal(NormalToken::ChangePol),
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 5ef17e70..17e9e857 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -147,8 +147,18 @@ pub enum NormalToken<'input> {
 
     #[token("%tag%")]
     Tag,
-    #[token("%typeof%")]
-    Typeof,
+    #[token("%is_num%")]
+    IsNum,
+    #[token("%is_bool%")]
+    IsBool,
+    #[token("%is_str%")]
+    IsStr,
+    #[token("%is_fun%")]
+    IsFun,
+    #[token("%is_array%")]
+    IsArray,
+    #[token("%is_record%")]
+    IsRecord,
 
     #[token("%assume%")]
     Assume,
diff --git a/src/pretty.rs b/src/pretty.rs
index 8707a9d1..c8c46483 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -26,7 +26,7 @@ fn min_interpolate_sign(text: &str) -> usize {
 
 fn sorted_map<'a, K: Ord, V>(m: &'a HashMap<K, V>) -> Vec<(&'a K, &'a V)> {
     let mut ret: Vec<(&K, &V)> = m.iter().collect();
-    ret.sort_by(|x, y| x.0.cmp(&y.0));
+    ret.sort_by_key(|(k, _)| *k);
     ret
 }
 
@@ -126,7 +126,11 @@ where
             ArrayTail() => allocator.text("%tail%").append(allocator.space()),
             ArrayHead() => allocator.text("%head%").append(allocator.space()),
             DeepSeq(_) => allocator.text("%deep_seq%").append(allocator.space()),
-            Typeof() => allocator.text("%typeof%").append(allocator.space()),
+            IsNum() => allocator.text("%is_num%").append(allocator.space()),
+            IsFun() => allocator.text("%is_fun%").append(allocator.space()),
+            IsStr() => allocator.text("%is_str%").append(allocator.space()),
+            IsArray() => allocator.text("%is_array%").append(allocator.space()),
+            IsRecord() => allocator.text("%is_record%").append(allocator.space()),
             BoolNot() => allocator.text("!"),
             BoolAnd() => allocator.space().append(allocator.text("&&")),
             BoolOr() => allocator.space().append(allocator.text("||")),
diff --git a/src/program.rs b/src/program.rs
index 551e4efa..dfdb86fa 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -283,8 +283,12 @@ mod doc {
             Term::MetaValue(MetaValue { doc: Some(md), .. }) => {
                 document.append(&mut parse_documentation(header_level, arena, &md, options))
             }
-            Term::Record(hm, _) | Term::RecRecord(hm, _, _, _) => {
-                for (ident, rt) in hm {
+            Term::Record(map, _) | Term::RecRecord(map, _, _, _) => {
+                // Sorting fields for a determinstic output
+                let mut entries: Vec<(_, _)> = map.iter().collect();
+                entries.sort_by_key(|(k, _)| *k);
+
+                for (ident, rt) in entries {
                     let header = mk_header(&ident.label, header_level + 1, arena);
                     document.append(header);
                     to_markdown(rt, header_level + 1, arena, document, options)?;
diff --git a/src/repl/mod.rs b/src/repl/mod.rs
index 47b28d49..49522d35 100644
--- a/src/repl/mod.rs
+++ b/src/repl/mod.rs
@@ -12,6 +12,7 @@ use crate::identifier::Ident;
 use crate::parser::{grammar, lexer, ExtendedTerm};
 use crate::term::{RichTerm, Term};
 use crate::transform::import_resolution;
+use crate::typecheck::TypeCheckingOutput;
 use crate::types::Types;
 use crate::{eval, transform, typecheck};
 use codespan::FileId;
@@ -134,7 +135,7 @@ impl ReplImpl {
                 repl_impl.cache.resolve_imports(*id).unwrap();
             }
 
-            let wildcards =
+            let TypeCheckingOutput { wildcards, .. } =
                 typecheck::type_check_in_env(&t, &repl_impl.env.type_env, &repl_impl.cache)?;
 
             if let Some(id) = id {
@@ -232,7 +233,8 @@ impl Repl for ReplImpl {
         for id in &pending {
             self.cache.resolve_imports(*id).unwrap();
         }
-        let wildcards = typecheck::type_check_in_env(&term, &self.env.type_env, &self.cache)?;
+        let TypeCheckingOutput { wildcards, .. } =
+            typecheck::type_check_in_env(&term, &self.env.type_env, &self.cache)?;
         // Substitute the wildcard types for their inferred types
         // We need to `traverse` the term, in case the type depends on inner terms that also contain wildcards
         let term = term
diff --git a/src/serialize.rs b/src/serialize.rs
index 063a1e34..d1c30e23 100644
--- a/src/serialize.rs
+++ b/src/serialize.rs
@@ -102,7 +102,7 @@ where
     S: Serializer,
 {
     let mut entries: Vec<(_, _)> = map.iter().collect();
-    entries.sort_by(|(k1, _), (k2, _)| k1.cmp(k2));
+    entries.sort_by_key(|(k, _)| *k);
 
     let mut map_ser = serializer.serialize_map(Some(entries.len()))?;
     for (id, t) in entries.iter() {
diff --git a/src/term.rs b/src/term.rs
index 96ce7bbb..6babdc9d 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -709,8 +709,18 @@ pub enum UnaryOp {
     /// If-then-else.
     Ite(),
 
-    /// Return an enum tag representing the type of the term.
-    Typeof(),
+    /// Test if a term is a numeral.
+    IsNum(),
+    /// Test if a term is a boolean.
+    IsBool(),
+    /// Test if a term is string literal.
+    IsStr(),
+    /// Test if a term is a function.
+    IsFun(),
+    /// Test if a term is an array.
+    IsArray(),
+    /// Test if a term is a record.
+    IsRecord(),
 
     // Boolean AND and OR operator are encoded as unary operators so that they can be lazy in their
     // second argument.
@@ -835,43 +845,6 @@ pub enum UnaryOp {
     NumFromStr(),
     /// Transform a string to an enum.
     EnumFromStr(),
-    /// Test if a regex matches a string.
-    /// Like [`StrMatch`], this is a unary operator because we would like a way to share the
-    /// same "compiled regex" for many matching calls. This is done by returning functions
-    /// wrapping [`StrIsMatchCompiled`] and [`StrMatchCompiled`]
-    StrIsMatch(),
-    /// Match a regex on a string, and returns the captured groups together, the index of the
-    /// match, etc.
-    StrMatch(),
-    /// Version of `StrIsMatch` which remembers the compiled regex.
-    StrIsMatchCompiled(CompiledRegex),
-    /// Version of `StrMatch` which remembers the compiled regex.
-    StrMatchCompiled(CompiledRegex),
-}
-
-// See: https://github.com/rust-lang/regex/issues/178
-/// [`regex::Regex`] which implements [`PartialEq`].
-#[derive(Debug, Clone)]
-pub struct CompiledRegex(regex::Regex);
-
-impl PartialEq for CompiledRegex {
-    fn eq(&self, other: &Self) -> bool {
-        self.0.as_str() == other.0.as_str()
-    }
-}
-
-impl Deref for CompiledRegex {
-    type Target = regex::Regex;
-
-    fn deref(&self) -> &Self::Target {
-        &self.0
-    }
-}
-
-impl From<regex::Regex> for CompiledRegex {
-    fn from(item: regex::Regex) -> Self {
-        CompiledRegex(item)
-    }
 }
 
 /// position of a unary operator
@@ -970,6 +943,11 @@ pub enum BinaryOp {
     StrSplit(),
     /// Determine if a string is a substring of another one.
     StrContains(),
+    /// Test if a regex matches a string.
+    StrIsMatch(),
+    /// Match a regex on a string, and returns the captured groups together, the index of the
+    /// match, etc.
+    StrMatch(),
 }
 
 impl BinaryOp {
diff --git a/src/typecheck/mk_typewrapper.rs b/src/typecheck/mk_typewrapper.rs
index 0bdb30b8..38a367ac 100644
--- a/src/typecheck/mk_typewrapper.rs
+++ b/src/typecheck/mk_typewrapper.rs
@@ -18,24 +18,21 @@ macro_rules! mk_tyw_arrow {
 }
 
 /// Multi-ary enum row constructor for types implementing `Into<TypeWrapper>`.
-/// `mk_tyw_enum_row!(id1, .., idn; tail)` correspond to `<id1, .., idn | tail>.
+/// `mk_tyw_enum_row!(id1, .., idn, tail)` correspond to `<id1, .., idn | tail>.
 #[macro_export]
 macro_rules! mk_tyw_enum_row {
-    () => {
-        $crate::typecheck::TypeWrapper::from(AbsType::RowEmpty())
-    };
-    (; $tail:expr) => {
-        $crate::typecheck::TypeWrapper::from($tail)
-    };
-    ( $id:expr $(, $ids:expr )* $(; $tail:expr)?) => {
+    ($id:expr, $tail:expr) => {
         $crate::typecheck::TypeWrapper::Concrete(
             $crate::types::AbsType::RowExtend(
                 Ident::from($id),
                 None,
-                Box::new(mk_tyw_enum_row!($( $ids ),* $(; $tail)?))
+                Box::new($crate::typecheck::TypeWrapper::from($tail))
             )
         )
     };
+    ( $fst:expr, $snd:expr , $( $rest:expr ),+ ) => {
+        mk_tyw_enum_row!($fst, mk_tyw_enum_row!($snd, $( $rest),+))
+    };
 }
 
 /// Multi-ary record row constructor for types implementing `Into<TypeWrapper>`.
@@ -63,13 +60,16 @@ macro_rules! mk_tyw_row {
 /// Wrapper around `mk_tyw_enum_row!` to build an enum type from an enum row.
 #[macro_export]
 macro_rules! mk_tyw_enum {
-    ($( $ids:expr ),* $(; $tail:expr)?) => {
+    ( $rows:expr ) => {
         $crate::typecheck::TypeWrapper::Concrete(
             $crate::types::AbsType::Enum(
-                Box::new(mk_tyw_enum_row!($( $ids ),* $(; $tail)?))
+                Box::new($rows.into())
             )
         )
     };
+    ( $fst:expr, $( $rest:expr ),+ ) => {
+        mk_tyw_enum!(mk_tyw_enum_row!($fst, $( $rest),+))
+    };
 }
 
 /// Wrapper around `mk_tyw_record!` to build a record type from a record row.
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index a37fe306..584341f0 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -3,29 +3,25 @@
 //! # Mode
 //!
 //! Typechecking can be made in to different modes:
-//! - **Strict**: correspond to traditional typechecking in statically typed languages. This
-//!   happens inside a statically typed block. Statically typed blocks are introduced by the type
-//!   ascription operator `:`, as in `1 + 1 : Num` or `let f : Num -> Num = fun x => x + 1 in ..`. This is
-//!   implemented by [`type_check_`] and variants.
-//! - **Non strict**: do not enforce any typing but continue to traverse the AST looking for other
-//!   typed blocks to typecheck and store the annotations of let bindings in the environment. This is
-//!   implemented by the [`walk`] function.
+//! - **Strict**: correspond to traditional typechecking in strongly, statically typed languages.
+//! This happens inside a `Promise` block. Promise block are introduced by the typing operator `:`,
+//! as in `1 + 1 : Num` or `let f : Num -> Num = fun x => x + 1 in ..`.
+//! - **Non strict**: do not enforce any typing, but still store the annotations of let bindings in
+//! the environment, and continue to traverse the AST looking for other `Promise` blocks to
+//! typecheck.
 //!
 //! The algorithm starts in non strict mode. It is switched to strict mode when entering a
-//! statically typed block (an expression annotated with a type), and is switched back to
-//! non-strict mode when entering an expression annotated with a contract. Type and contract
-//! annotations thus serve both another purpose beside enforcing a type or a contract, which is to
-//! switch the typechecking mode.
+//! `Promise` block, and is switched to non-strict mode when entering an `Assume` block.  `Promise`
+//! and `Assume` thus serve both two purposes: annotate a term with a type, and set the
+//! typechecking mode.
 //!
 //! # Type inference
 //!
-//! Type inference is done via a form of bidirectional typechecking coupled with unification, in
-//! the same spirit as GHC (Haskell), albeit the type system of Nickel is much simpler. The type of
-//! un-annotated let-bound 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:
+//! Type inference is done via a standard unification algorithm. The type of unannotated let-bound
+//! 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:
 //!
-//! ```nickel
+//! ```text
 //! # Rejected
 //! let id = fun x => x in seq (id "a") (id 5) : Num
 //! ```
@@ -35,18 +31,16 @@
 //! call site the typechecker complains that `5` is not of type `Str`.
 //!
 //! This restriction is on purpose, as generalization is not trivial to implement efficiently and
-//! more importantly can interact with other components of the type system and type inference. If
-//! polymorphism is required, the user can simply add annotation:
+//! can interact with other parts of type inference. If polymorphism is required, a simple
+//! annotation is sufficient:
 //!
-//! ```nickel
+//! ```text
 //! # Accepted
 //! let id : forall a. a -> a = fun x => x in seq (id "a") (id 5) : Num
 //! ```
 //!
-//! In non-strict mode, the type of let-bound expressions is inferred in a shallow way (see
-//! [`apparent_type`]).
+//! In non-strict mode, all let-bound expressions are given type `Dyn`, unless annotated.
 use crate::cache::ImportResolver;
-use crate::destruct::*;
 use crate::environment::Environment as GenericEnvironment;
 use crate::error::TypecheckError;
 use crate::identifier::Ident;
@@ -188,6 +182,14 @@ pub struct State<'a> {
     wildcard_vars: &'a mut Vec<TypeWrapper>,
 }
 
+/// The result of type checking a term.
+pub struct TypeCheckingOutput {
+    /// Inferred type of the term.
+    pub types: Types,
+    /// Inferred types of wildcards within the term.
+    pub wildcards: Wildcards,
+}
+
 /// Typecheck a term.
 ///
 /// Return the inferred type in case of success. This is just a wrapper that calls `type_check_`
@@ -195,20 +197,19 @@ pub struct State<'a> {
 ///
 /// Note that this function doesn't recursively typecheck imports (anymore), but just the current
 /// file. It however still needs the resolver to get the apparent type of imports.
-///
-/// Return the type inferred for type wildcards.
 pub fn type_check<LL>(
     t: &RichTerm,
     global_env: &Environment,
     resolver: &impl ImportResolver,
     mut linearizer: LL,
-) -> Result<(Wildcards, LL::Completed), TypecheckError>
+) -> Result<(TypeCheckingOutput, LL::Completed), TypecheckError>
 where
     LL: Linearizer<CompletionExtra = (UnifTable, HashMap<usize, Ident>)>,
 {
     let (mut table, mut names) = (UnifTable::new(), HashMap::new());
     let mut building = Linearization::new(LL::Building::default());
-    let mut wildcard_vars = Vec::new();
+    let ty = table.fresh_unif_var();
+    let mut wildcard_vars = vec![];
 
     {
         let mut state: State = State {
@@ -219,16 +220,21 @@ where
             wildcard_vars: &mut wildcard_vars,
         };
 
-        walk(
+        type_check_(
             &mut state,
             Envs::from_global(global_env),
             &mut building,
             linearizer.scope(),
+            false,
             t,
+            ty.clone(),
         )?;
     }
 
-    let result = wildcard_vars_to_type(wildcard_vars, &table);
+    let result = TypeCheckingOutput {
+        types: to_type(&table, ty),
+        wildcards: wildcard_vars_to_type(wildcard_vars, &table),
+    };
     let lin = linearizer.complete(building, (table, names)).into_inner();
 
     Ok((result, lin))
@@ -242,256 +248,41 @@ where
 /// to the original term environment anymore, and hence cannot call `type_check` directly, but we
 /// already have built a global typing environment.
 ///
-/// Return the type inferred for type wildcards. This is just a wrapper that calls `type_check_`
+/// Return the inferred type in case of success. This is just a wrapper that calls `type_check_`
 /// with a fresh unification variable as goal.
 pub fn type_check_in_env(
     t: &RichTerm,
     global: &Environment,
     resolver: &dyn ImportResolver,
-) -> Result<Wildcards, TypecheckError> {
+) -> Result<TypeCheckingOutput, TypecheckError> {
     let mut table = UnifTable::new();
-    let mut wildcard_vars = Vec::new();
-
-    let mut state = State {
-        resolver,
-        table: &mut table,
-        constr: &mut RowConstr::new(),
-        names: &mut HashMap::new(),
-        wildcard_vars: &mut wildcard_vars,
-    };
-
-    walk(
-        &mut state,
-        Envs::from_global(global),
-        &mut Linearization::new(()),
-        StubHost::<()>::new(),
-        t,
-    )?;
-
-    Ok(wildcard_vars_to_type(wildcard_vars, &table))
-}
-
-/// Walk the AST of a term looking for statically typed block to check. Fill the linearization
-/// alongside and store the apparent type of variable inside the typing environment.
-fn walk<L: Linearizer>(
-    state: &mut State,
-    mut envs: Envs,
-    lin: &mut Linearization<L::Building>,
-    mut linearizer: L,
-    rt: &RichTerm,
-) -> Result<(), TypecheckError> {
-    let RichTerm { term: t, pos } = rt;
-    linearizer.add_term(lin, t, *pos, mk_typewrapper::dynamic());
+    let ty = table.fresh_unif_var();
+    let mut wildcard_vars = vec![];
 
-    match t.as_ref() {
-        Term::ParseError
-        | Term::Null
-        | Term::Bool(_)
-        | Term::Num(_)
-        | Term::Str(_)
-        | Term::Lbl(_)
-        | Term::Enum(_)
-        | Term::Sym(_)
-        // This function doesn't recursively typecheck imports: this is the responsibility of the
-        // caller.
-        | Term::Import(_)
-        | Term::ResolvedImport(_) => Ok(()),
-        Term::Var(x) => envs
-            .get(x)
-            .ok_or_else(|| TypecheckError::UnboundIdentifier(x.clone(), *pos))
-            .map(|_| ()),
-        Term::StrChunks(chunks) => {
-            chunks
-                .iter()
-                .try_for_each(|chunk| -> Result<(), TypecheckError> {
-                    match chunk {
-                        StrChunk::Literal(_) => Ok(()),
-                        StrChunk::Expr(t, _) => {
-                            walk(state, envs.clone(), lin, linearizer.scope(), t)
-                        }
-                    }
-                })
-        }
-        Term::Fun(id, t) => {
-            // The parameter of an un-annotated function is assigned the type `Dyn`.
-            envs.insert(id.clone(), mk_typewrapper::dynamic());
-            walk(state, envs, lin, linearizer, t)
-        }
-        Term::FunPattern(id, pat, t) => {
-            if let Some(id) = id {
-                envs.insert(id.clone(), binding_type(state, t.as_ref(), &envs, false));
-            }
-
-            inject_pat_vars(pat, &mut envs);
-            walk(state, envs, lin, linearizer, t)
-        }
-        Term::Array(terms, _) => terms
-            .iter()
-            .try_for_each(|t| -> Result<(), TypecheckError> {
-                walk(state, envs.clone(), lin, linearizer.scope(), t)
-            }),
-        Term::Let(x, re, rt, attrs) => {
-            let ty_let = binding_type(state, re.as_ref(), &envs, false);
-
-            if attrs.rec {
-                envs.insert(x.clone(), ty_let.clone());
-            }
-
-            linearizer.retype_ident(lin, x, ty_let.clone());
-            walk(state, envs.clone(), lin, linearizer.scope(), re)?;
-
-            if !attrs.rec {
-                envs.insert(x.clone(), ty_let);
-            }
-
-            walk(state, envs, lin, linearizer, rt)
-        }
-        Term::LetPattern(x, pat, re, rt) => {
-            let ty_let = binding_type(state, re.as_ref(), &envs, false);
-            walk(state, envs.clone(), lin, linearizer.scope(), re)?;
-
-            if let Some(x) = x {
-                linearizer.retype_ident(lin, x, ty_let.clone());
-                envs.insert(x.clone(), ty_let);
-            }
-
-            inject_pat_vars(pat, &mut envs);
-
-            walk(state, envs, lin, linearizer, rt)
-        }
-        Term::App(e, t) => {
-            walk(state, envs.clone(), lin, linearizer.scope(), e)?;
-            walk(state, envs, lin, linearizer, t)
-        }
-        Term::Switch(exp, cases, default) => {
-            cases.values().chain(default.iter()).try_for_each(|case| {
-                walk(state, envs.clone(), lin, linearizer.scope(), case)
-            })?;
-
-            walk(state, envs, lin, linearizer, exp)
-        }
-        Term::RecRecord(stat_map, dynamic, ..) => {
-            for id in stat_map.keys() {
-                let binding_type = binding_type(
-                    state,
-                    stat_map.get(id).unwrap().as_ref(),
-                    &envs,
-                    false,
-                );
-                envs.insert(id.clone(), binding_type.clone());
-                linearizer.retype_ident(lin, id, binding_type);
-            }
-
-            stat_map
-                .iter()
-                .map(|(_, t)| t)
-                .chain(dynamic.iter().map(|(_, t)| t))
-                .try_for_each(|t| -> Result<(), TypecheckError> {
-                    walk(state, envs.clone(), lin, linearizer.scope(), t)
-                })
-        }
-        Term::Record(stat_map, _) => {
-            stat_map
-                .iter()
-                .try_for_each(|(_, t)| -> Result<(), TypecheckError> {
-                    walk(state, envs.clone(), lin, linearizer.scope(), t)
-                })
-        }
-        Term::Op1(_, t) => walk(state, envs.clone(), lin, linearizer.scope(), t),
-        Term::Op2(_, t1, t2) => {
-            walk(state, envs.clone(), lin, linearizer.scope(), t1)?;
-            walk(state, envs, lin, linearizer, t2)
-        }
-        Term::OpN(_, args) => {
-           args.iter().try_for_each(|t| -> Result<(), TypecheckError> {
-                    walk(
-                        state,
-                        envs.clone(),
-                        lin,
-                        linearizer.scope(),
-                        t,
-                    )
-                },
-            )
-        }
-        // An type annotation switches mode to check.
-        Term::MetaValue(meta) => {
-            meta.contracts.iter().chain(meta.types.iter()).try_for_each(|ty| walk_type(state, envs.clone(), lin, linearizer.scope(), &ty.types))?;
-
-            match meta {
-                MetaValue {
-                types: Some(Contract { types: ty2, .. }),
-                value: Some(t),
-                ..
-                } => {
-                    let tyw2 = TypeWrapper::from(ty2.clone());
-                    let instantiated = instantiate_foralls(state, tyw2.clone(), ForallInst::Constant);
-                    type_check_(state, envs, lin, linearizer, t, instantiated)
-                }
-                MetaValue {value: Some(t), .. } =>  walk(state, envs, lin, linearizer, t),
-                // A metavalue without a body nor a type annotation is a record field without definition.
-                _ => Ok(()),
-            }
-        }
-        Term::Wrapped(_, t) => walk(state, envs, lin, linearizer, t),
-   }
-}
+    {
+        let mut state: State = State {
+            resolver,
+            table: &mut table,
+            constr: &mut RowConstr::new(),
+            names: &mut HashMap::new(),
+            wildcard_vars: &mut wildcard_vars,
+        };
 
-/// Same as [`walk`] but operate on a type, which can contain terms as contracts (`AbsType::Flat`),
-/// instead of a term.
-fn walk_type<L: Linearizer>(
-    state: &mut State,
-    envs: Envs,
-    lin: &mut Linearization<L::Building>,
-    mut linearizer: L,
-    ty: &Types,
-) -> Result<(), TypecheckError> {
-    match &ty.0 {
-       AbsType::Dyn()
-       | AbsType::Num()
-       | AbsType::Bool()
-       | AbsType::Str()
-       | AbsType::Sym()
-       // Currently, the parser can't generate unbound type variables by construction. Thus we
-       // don't check here for unbound type variables again.
-       | AbsType::Var(_)
-       | AbsType::Wildcard(_)
-       | AbsType::RowEmpty() => Ok(()),
-       AbsType::Arrow(ty1, ty2) => {
-           walk_type(state, envs.clone(), lin, linearizer.scope(), ty1.as_ref())?;
-           walk_type(state, envs, lin, linearizer, ty2.as_ref())
-       }
-       AbsType::RowExtend(_, ty_row, tail) => {
-         if let Some(ty_row) = ty_row { walk_type(state, envs.clone(), lin, linearizer.scope(), ty_row)? };
-         walk_type(state, envs, lin,linearizer, tail)
-       }
-       AbsType::Flat(t) => walk(state, envs, lin, linearizer, t),
-       AbsType::Enum(ty2)
-       | AbsType::DynRecord(ty2)
-       | AbsType::StaticRecord(ty2)
-       | AbsType::Array(ty2)
-       | AbsType::Forall(_, ty2) => walk_type(state, envs, lin, linearizer, ty2),
+        type_check_(
+            &mut state,
+            Envs::from_global(global),
+            &mut Linearization::new(()),
+            StubHost::<()>::new(),
+            false,
+            t,
+            ty.clone(),
+        )?;
     }
-}
 
-// TODO: The insertion of values in the type environment is done but everything is
-// typed as `Dyn`.
-fn inject_pat_vars(pat: &Destruct, envs: &mut Envs) {
-    if let Destruct::Record { matches, rest, .. } = pat {
-        if let Some(id) = rest {
-            envs.insert(id.clone(), TypeWrapper::Concrete(AbsType::Dyn()));
-        }
-        matches.iter().for_each(|m| match m {
-            Match::Simple(id, ..) => envs.insert(id.clone(), TypeWrapper::Concrete(AbsType::Dyn())),
-            Match::Assign(id, _, (bind_id, pat)) => {
-                let id = bind_id.as_ref().unwrap_or(id);
-                envs.insert(id.clone(), TypeWrapper::Concrete(AbsType::Dyn()));
-                if !pat.is_empty() {
-                    inject_pat_vars(&pat, envs);
-                }
-            }
-        });
-    }
+    Ok(TypeCheckingOutput {
+        types: to_type(&table, ty),
+        wildcards: wildcard_vars_to_type(wildcard_vars, &table),
+    })
 }
 
 /// Typecheck a term against a specific type.
@@ -502,6 +293,7 @@ fn inject_pat_vars(pat: &Destruct, envs: &mut Envs) {
 /// - `env`: the typing environment, mapping free variable to types.
 /// - `lin`: The current building linearization of building state `S`
 /// - `linearizer`: A linearizer that can modify the linearization
+/// - `strict`: the typechecking mode.
 /// - `t`: the term to check.
 /// - `ty`: the type to check the term against.
 ///
@@ -512,25 +304,49 @@ fn type_check_<L: Linearizer>(
     mut envs: Envs,
     lin: &mut Linearization<L::Building>,
     mut linearizer: L,
+    strict: bool,
     rt: &RichTerm,
     ty: TypeWrapper,
 ) -> Result<(), TypecheckError> {
+    use crate::destruct::*;
+    // TODO: The insertion of values in the type environment is done but everything is
+    // typed as `Dyn`.
+    fn inject_pat_vars(pat: &Destruct, envs: &mut Envs) {
+        if let Destruct::Record { matches, rest, .. } = pat {
+            if let Some(id) = rest {
+                envs.insert(id.clone(), TypeWrapper::Concrete(AbsType::Dyn()));
+            }
+            matches.iter().for_each(|m| match m {
+                Match::Simple(id, ..) => {
+                    envs.insert(id.clone(), TypeWrapper::Concrete(AbsType::Dyn()))
+                }
+                Match::Assign(id, _, (bind_id, pat)) => {
+                    let id = bind_id.as_ref().unwrap_or(id);
+                    envs.insert(id.clone(), TypeWrapper::Concrete(AbsType::Dyn()));
+                    if !pat.is_empty() {
+                        inject_pat_vars(&pat, envs);
+                    }
+                }
+            });
+        }
+    }
+
     let RichTerm { term: t, pos } = rt;
     linearizer.add_term(lin, t, *pos, ty.clone());
 
     match t.as_ref() {
         Term::ParseError => Ok(()),
         // null is inferred to be of type Dyn
-        Term::Null => unify(state, ty, mk_typewrapper::dynamic())
+        Term::Null => unify(state, strict, ty, mk_typewrapper::dynamic())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
-        Term::Bool(_) => unify(state, ty, mk_typewrapper::bool())
+        Term::Bool(_) => unify(state, strict, ty, mk_typewrapper::bool())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
-        Term::Num(_) => unify(state, ty, mk_typewrapper::num())
+        Term::Num(_) => unify(state, strict, ty, mk_typewrapper::num())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
-        Term::Str(_) => unify(state, ty, mk_typewrapper::str())
+        Term::Str(_) => unify(state, strict, ty, mk_typewrapper::str())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
         Term::StrChunks(chunks) => {
-            unify(state, ty, mk_typewrapper::str())
+            unify(state, strict, ty, mk_typewrapper::str())
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
 
             chunks
@@ -543,6 +359,7 @@ fn type_check_<L: Linearizer>(
                             envs.clone(),
                             lin,
                             linearizer.scope(),
+                            strict,
                             t,
                             mk_typewrapper::str(),
                         ),
@@ -553,14 +370,15 @@ fn type_check_<L: Linearizer>(
             let src = state.table.fresh_unif_var();
             // TODO what to do here, this makes more sense to me, but it means let x = foo in bar
             // behaves quite different to (\x.bar) foo, worth considering if it's ok to type these two differently
+            // let src = TypeWrapper::The(AbsType::Dyn());
             let trg = state.table.fresh_unif_var();
             let arr = mk_tyw_arrow!(src.clone(), trg.clone());
             linearizer.retype_ident(lin, x, src.clone());
 
-            unify(state, ty, arr).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
+            unify(state, strict, ty, arr).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
 
             envs.insert(x.clone(), src);
-            type_check_(state, envs, lin, linearizer, t, trg)
+            type_check_(state, envs, lin, linearizer, strict, t, trg)
         }
         Term::FunPattern(x, pat, t) => {
             let src = state.table.fresh_unif_var();
@@ -573,13 +391,13 @@ fn type_check_<L: Linearizer>(
                 envs.insert(x.clone(), src);
             }
             inject_pat_vars(pat, &mut envs);
-            unify(state, ty, arr).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
-            type_check_(state, envs, lin, linearizer, t, trg)
+            unify(state, strict, ty, arr).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
+            type_check_(state, envs, lin, linearizer, strict, t, trg)
         }
         Term::Array(terms, _) => {
             let ty_elts = state.table.fresh_unif_var();
 
-            unify(state, ty, mk_typewrapper::array(ty_elts.clone()))
+            unify(state, strict, ty, mk_typewrapper::array(ty_elts.clone()))
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
 
             terms
@@ -590,6 +408,7 @@ fn type_check_<L: Linearizer>(
                         envs.clone(),
                         lin,
                         linearizer.scope(),
+                        strict,
                         t,
                         ty_elts.clone(),
                     )
@@ -597,11 +416,18 @@ fn type_check_<L: Linearizer>(
         }
         Term::Lbl(_) => {
             // TODO implement lbl type
-            unify(state, ty, mk_typewrapper::dynamic())
+            unify(state, strict, ty, mk_typewrapper::dynamic())
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Let(x, re, rt, attrs) => {
-            let ty_let = binding_type(state, re.as_ref(), &envs, true);
+            let ty_let = binding_type(
+                re.as_ref(),
+                &envs,
+                state.table,
+                state.wildcard_vars,
+                strict,
+                state.resolver,
+            );
             if attrs.rec {
                 envs.insert(x.clone(), ty_let.clone());
             }
@@ -612,6 +438,7 @@ fn type_check_<L: Linearizer>(
                 envs.clone(),
                 lin,
                 linearizer.scope(),
+                strict,
                 re,
                 ty_let.clone(),
             )?;
@@ -619,15 +446,23 @@ fn type_check_<L: Linearizer>(
             if !attrs.rec {
                 envs.insert(x.clone(), ty_let);
             }
-            type_check_(state, envs, lin, linearizer, rt, ty)
+            type_check_(state, envs, lin, linearizer, strict, rt, ty)
         }
         Term::LetPattern(x, pat, re, rt) => {
-            let ty_let = binding_type(state, re.as_ref(), &envs, true);
+            let ty_let = binding_type(
+                re.as_ref(),
+                &envs,
+                state.table,
+                state.wildcard_vars,
+                strict,
+                state.resolver,
+            );
             type_check_(
                 state,
                 envs.clone(),
                 lin,
                 linearizer.scope(),
+                strict,
                 re,
                 ty_let.clone(),
             )?;
@@ -637,14 +472,14 @@ fn type_check_<L: Linearizer>(
                 envs.insert(x.clone(), ty_let);
             }
             inject_pat_vars(pat, &mut envs);
-            type_check_(state, envs, lin, linearizer, rt, ty)
+            type_check_(state, envs, lin, linearizer, strict, rt, ty)
         }
         Term::App(e, t) => {
             let src = state.table.fresh_unif_var();
             let arr = mk_tyw_arrow!(src.clone(), ty);
 
-            type_check_(state, envs.clone(), lin, linearizer.scope(), e, arr)?;
-            type_check_(state, envs, lin, linearizer, t, src)
+            type_check_(state, envs.clone(), lin, linearizer.scope(), strict, e, arr)?;
+            type_check_(state, envs, lin, linearizer, strict, t, src)
         }
         Term::Switch(exp, cases, default) => {
             // Currently, if it has a default value, we typecheck the whole thing as
@@ -657,6 +492,7 @@ fn type_check_<L: Linearizer>(
                     envs.clone(),
                     lin,
                     linearizer.scope(),
+                    strict,
                     case,
                     res.clone(),
                 )?;
@@ -664,19 +500,27 @@ fn type_check_<L: Linearizer>(
 
             let row = match default {
                 Some(t) => {
-                    type_check_(state, envs.clone(), lin, linearizer.scope(), t, res.clone())?;
+                    type_check_(
+                        state,
+                        envs.clone(),
+                        lin,
+                        linearizer.scope(),
+                        strict,
+                        t,
+                        res.clone(),
+                    )?;
                     state.table.fresh_unif_var()
                 }
                 None => cases.iter().try_fold(
                     mk_typewrapper::row_empty(),
                     |acc, x| -> Result<TypeWrapper, TypecheckError> {
-                        Ok(mk_tyw_enum_row!(x.0.clone(); acc))
+                        Ok(mk_tyw_enum_row!(x.0.clone(), acc))
                     },
                 )?,
             };
 
-            unify(state, ty, res).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
-            type_check_(state, envs, lin, linearizer, exp, mk_tyw_enum!(; row))
+            unify(state, strict, ty, res).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
+            type_check_(state, envs, lin, linearizer, strict, exp, mk_tyw_enum!(row))
         }
         Term::Var(x) => {
             let x_ty = envs
@@ -684,11 +528,12 @@ fn type_check_<L: Linearizer>(
                 .ok_or_else(|| TypecheckError::UnboundIdentifier(x.clone(), *pos))?;
 
             let instantiated = instantiate_foralls(state, x_ty, ForallInst::Ptr);
-            unify(state, ty, instantiated).map_err(|err| err.into_typecheck_err(state, rt.pos))
+            unify(state, strict, ty, instantiated)
+                .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Enum(id) => {
             let row = state.table.fresh_unif_var();
-            unify(state, ty, mk_tyw_enum!(id.clone(); row))
+            unify(state, strict, ty, mk_tyw_enum!(id.clone(), row))
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         // If some fields are defined dynamically, the only potential type that works is `{_ : a}`
@@ -709,12 +554,13 @@ fn type_check_<L: Linearizer>(
                         envs.clone(),
                         lin,
                         linearizer.scope(),
+                        strict,
                         t,
                         ty_dyn.clone(),
                     )
                 })?;
 
-            unify(state, ty, mk_typewrapper::dyn_record(ty_dyn))
+            unify(state, strict, ty, mk_typewrapper::dyn_record(ty_dyn))
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Record(stat_map, _) | Term::RecRecord(stat_map, ..) => {
@@ -723,7 +569,14 @@ fn type_check_<L: Linearizer>(
             // Fields defined by interpolation are ignored.
             if let Term::RecRecord(..) = t.as_ref() {
                 for (id, rt) in stat_map {
-                    let tyw = binding_type(state, rt.as_ref(), &envs, true);
+                    let tyw = binding_type(
+                        rt.as_ref(),
+                        &envs,
+                        state.table,
+                        state.wildcard_vars,
+                        strict,
+                        state.resolver,
+                    );
                     envs.insert(id.clone(), tyw.clone());
                     linearizer.retype_ident(lin, id, tyw);
                 }
@@ -745,6 +598,7 @@ fn type_check_<L: Linearizer>(
                             envs.clone(),
                             lin,
                             linearizer.scope(),
+                            strict,
                             t,
                             (*rec_ty).clone(),
                         )
@@ -767,6 +621,7 @@ fn type_check_<L: Linearizer>(
                             envs.clone(),
                             lin,
                             linearizer.scope(),
+                            strict,
                             field,
                             ty.clone(),
                         )?;
@@ -775,95 +630,118 @@ fn type_check_<L: Linearizer>(
                     },
                 )?;
 
-                unify(state, ty, mk_tyw_record!(; row))
+                unify(state, strict, ty, mk_tyw_record!(; row))
                     .map_err(|err| err.into_typecheck_err(state, rt.pos))
             }
         }
         Term::Op1(op, t) => {
             let (ty_arg, ty_res) = get_uop_type(state, op)?;
 
-            type_check_(state, envs.clone(), lin, linearizer.scope(), t, ty_arg)?;
+            type_check_(
+                state,
+                envs.clone(),
+                lin,
+                linearizer.scope(),
+                strict,
+                t,
+                ty_arg,
+            )?;
 
             let instantiated = instantiate_foralls(state, ty_res, ForallInst::Ptr);
-            unify(state, ty, instantiated).map_err(|err| err.into_typecheck_err(state, rt.pos))
+            unify(state, strict, ty, instantiated)
+                .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Op2(op, t1, t2) => {
             let (ty_arg1, ty_arg2, ty_res) = get_bop_type(state, op)?;
 
-            unify(state, ty, ty_res).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
-            type_check_(state, envs.clone(), lin, linearizer.scope(), t1, ty_arg1)?;
-            type_check_(state, envs, lin, linearizer, t2, ty_arg2)
+            unify(state, strict, ty, ty_res)
+                .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
+            type_check_(
+                state,
+                envs.clone(),
+                lin,
+                linearizer.scope(),
+                strict,
+                t1,
+                ty_arg1,
+            )?;
+            type_check_(state, envs, lin, linearizer, strict, t2, ty_arg2)
         }
         Term::OpN(op, args) => {
             let (tys_op, ty_ret) = get_nop_type(state, op)?;
 
-            unify(state, ty, ty_ret).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
+            unify(state, strict, ty, ty_ret)
+                .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
 
             tys_op.into_iter().zip(args.iter()).try_for_each(
                 |(ty_t, t)| -> Result<_, TypecheckError> {
-                    type_check_(state, envs.clone(), lin, linearizer.scope(), t, ty_t)?;
+                    type_check_(
+                        state,
+                        envs.clone(),
+                        lin,
+                        linearizer.scope(),
+                        strict,
+                        t,
+                        ty_t,
+                    )?;
                     Ok(())
                 },
             )?;
 
             Ok(())
         }
-        Term::MetaValue(meta) => {
-            meta.contracts
-                .iter()
-                .chain(meta.types.iter())
-                .try_for_each(|ty| {
-                    walk_type(state, envs.clone(), lin, linearizer.scope(), &ty.types)
-                })?;
+        Term::MetaValue(MetaValue {
+            types: Some(Contract { types: ty2, .. }),
+            value: Some(t),
+            ..
+        }) => {
+            let tyw2 = TypeWrapper::from(ty2.clone());
 
-            match meta {
-                MetaValue {
-                    types: Some(Contract { types: ty2, .. }),
-                    value: Some(t),
-                    ..
-                } => {
-                    let tyw2 = TypeWrapper::from(ty2.clone());
-                    let instantiated =
-                        instantiate_foralls(state, tyw2.clone(), ForallInst::Constant);
-
-                    unify(state, tyw2, ty).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
-                    type_check_(state, envs, lin, linearizer, t, instantiated)
-                }
-                // A metavalue without a type annotation but with a contract annotation switches
-                // the typechecker back to walk mode. If there are several contracts, we
-                // arbitrarily chose the first one as the apparent type.
-                MetaValue {
-                    contracts, value, ..
-                } if !contracts.is_empty() => {
-                    let ctr = contracts.get(0).unwrap();
-                    let Contract { types: ty2, .. } = ctr;
-
-                    unify(state, ty, ty2.clone().into())
-                        .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
-
-                    // if there's an inner value, we still have to walk it, as it may contain
-                    // statically typed block.
-                    if let Some(t) = value {
-                        walk(state, envs, lin, linearizer, t)
-                    } else {
-                        Ok(())
-                    }
-                }
-                // A non-empty metavalue without a type or a contract annotation is typechecked in
-                // the same way as its inner value
-                MetaValue { value: Some(t), .. } => {
-                    type_check_(state, envs, lin, linearizer, t, ty)
-                }
-                // A metavalue without a body nor a type annotation is a record field without definition.
-                // We infer it to be of type `Dyn` for now.
-                _ => unify(state, ty, mk_typewrapper::dynamic())
-                    .map_err(|err| err.into_typecheck_err(state, rt.pos)),
+            let instantiated = instantiate_foralls(state, tyw2.clone(), ForallInst::Constant);
+
+            unify(state, strict, tyw2, ty).map_err(|err| err.into_typecheck_err(state, rt.pos))?;
+            type_check_(state, envs, lin, linearizer, true, t, instantiated)
+        }
+        // A metavalue with at least one contract is an assume. If there's several
+        // contracts, we arbitrarily chose the first one as the type annotation.
+        Term::MetaValue(MetaValue {
+            contracts, value, ..
+        }) if !contracts.is_empty() => {
+            let ctr = contracts.get(0).unwrap();
+            let Contract { types: ty2, .. } = ctr;
+
+            unify(state, strict, ty, ty2.clone().into())
+                .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
+
+            // if there's an inner value, we have to recursively typecheck it, but in non strict
+            // mode.
+            if let Some(t) = value {
+                type_check_(
+                    state,
+                    envs,
+                    lin,
+                    linearizer,
+                    false,
+                    t,
+                    mk_typewrapper::dynamic(),
+                )
+            } else {
+                Ok(())
             }
         }
-        Term::Sym(_) => unify(state, ty, mk_typewrapper::sym())
+        Term::Sym(_) => unify(state, strict, ty, mk_typewrapper::sym())
+            .map_err(|err| err.into_typecheck_err(state, rt.pos)),
+        Term::Wrapped(_, t) => type_check_(state, envs, lin, linearizer, strict, t, ty),
+        // A non-empty metavalue without a type or contract annotation is typechecked in the same way as its inner value
+        Term::MetaValue(MetaValue { value: Some(t), .. }) => {
+            type_check_(state, envs, lin, linearizer, strict, t, ty)
+        }
+        // A metavalue without a body nor a type annotation is a record field without definition.
+        // This should probably be non representable in the syntax, as it doesn't really make
+        // sense. In any case, we infer it to be of type `Dyn` for now.
+        Term::MetaValue(_) => unify(state, strict, ty, mk_typewrapper::dynamic())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
-        Term::Wrapped(_, t) => type_check_(state, envs, lin, linearizer, t, ty),
-        Term::Import(_) => unify(state, ty, mk_typewrapper::dynamic())
+        Term::Import(_) => unify(state, strict, ty, mk_typewrapper::dynamic())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
         // We use the apparent type of the import for checking. This function doesn't recursively
         // typecheck imports: this is the responsibility of the caller.
@@ -878,7 +756,7 @@ fn type_check_<L: Linearizer>(
                 Some(state.resolver),
             )
             .into();
-            unify(state, ty, ty_import).map_err(|err| err.into_typecheck_err(state, rt.pos))
+            unify(state, strict, ty, ty_import).map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
     }
 }
@@ -899,14 +777,21 @@ fn type_check_<L: Linearizer>(
 ///     * in non strict mode, wildcards are assigned `Dyn`.
 ///     * in strict mode, the wildcard is typechecked, and we return the unification variable
 ///       corresponding to it.
-fn binding_type(state: &mut State, t: &Term, envs: &Envs, strict: bool) -> TypeWrapper {
-    let ty_apt = apparent_type(t, Some(envs), Some(state.resolver));
+fn binding_type(
+    t: &Term,
+    envs: &Envs,
+    table: &mut UnifTable,
+    wildcard_vars: &mut Vec<TypeWrapper>,
+    strict: bool,
+    resolver: &dyn ImportResolver,
+) -> TypeWrapper {
+    let ty_apt = apparent_type(t, Some(envs), Some(resolver));
 
     match ty_apt {
         ApparentType::Annotated(ty) if strict => {
-            replace_wildcards_with_var(state.table, state.wildcard_vars, ty)
+            replace_wildcards_with_var(table, wildcard_vars, ty)
         }
-        ApparentType::Approximated(_) if strict => state.table.fresh_unif_var(),
+        ApparentType::Approximated(_) if strict => table.fresh_unif_var(),
         ty_apt => ty_apt.into(),
     }
 }
@@ -1219,7 +1104,28 @@ fn row_add(
 }
 
 /// Try to unify two types.
-pub fn unify(state: &mut State, mut t1: TypeWrapper, mut t2: TypeWrapper) -> Result<(), UnifError> {
+///
+/// A wrapper around `unify_` which just checks if `strict` is set to true. If not, it directly
+/// returns `Ok(())` without unifying anything.
+pub fn unify(
+    state: &mut State,
+    strict: bool,
+    t1: TypeWrapper,
+    t2: TypeWrapper,
+) -> Result<(), UnifError> {
+    if strict {
+        unify_(state, t1, t2)
+    } else {
+        Ok(())
+    }
+}
+
+/// Try to unify two types.
+pub fn unify_(
+    state: &mut State,
+    mut t1: TypeWrapper,
+    mut t2: TypeWrapper,
+) -> Result<(), UnifError> {
     if let TypeWrapper::Ptr(pt1) = t1 {
         t1 = state.table.root(pt1);
     }
@@ -1233,24 +1139,24 @@ pub fn unify(state: &mut State, mut t1: TypeWrapper, mut t2: TypeWrapper) -> Res
         (TypeWrapper::Concrete(AbsType::Wildcard(id)), ty2)
         | (ty2, TypeWrapper::Concrete(AbsType::Wildcard(id))) => {
             let ty1 = get_wildcard_var(state.table, state.wildcard_vars, id);
-            unify(state, ty1, ty2)
+            unify_(state, ty1, ty2)
         }
         (TypeWrapper::Concrete(s1), TypeWrapper::Concrete(s2)) => match (s1, s2) {
             (AbsType::Dyn(), AbsType::Dyn()) => Ok(()),
             (AbsType::Num(), AbsType::Num()) => Ok(()),
             (AbsType::Bool(), AbsType::Bool()) => Ok(()),
             (AbsType::Str(), AbsType::Str()) => Ok(()),
-            (AbsType::Array(tyw1), AbsType::Array(tyw2)) => unify(state, *tyw1, *tyw2),
+            (AbsType::Array(tyw1), AbsType::Array(tyw2)) => unify_(state, *tyw1, *tyw2),
             (AbsType::Sym(), AbsType::Sym()) => Ok(()),
             (AbsType::Arrow(s1s, s1t), AbsType::Arrow(s2s, s2t)) => {
-                unify(state, (*s1s).clone(), (*s2s).clone()).map_err(|err| {
+                unify_(state, (*s1s).clone(), (*s2s).clone()).map_err(|err| {
                     UnifError::DomainMismatch(
                         TypeWrapper::Concrete(AbsType::Arrow(s1s.clone(), s1t.clone())),
                         TypeWrapper::Concrete(AbsType::Arrow(s2s.clone(), s2t.clone())),
                         Box::new(err),
                     )
                 })?;
-                unify(state, (*s1t).clone(), (*s2t).clone()).map_err(|err| {
+                unify_(state, (*s1t).clone(), (*s2t).clone()).map_err(|err| {
                     UnifError::CodomainMismatch(
                         TypeWrapper::Concrete(AbsType::Arrow(s1s, s1t)),
                         TypeWrapper::Concrete(AbsType::Arrow(s2s, s2t)),
@@ -1277,15 +1183,15 @@ pub fn unify(state: &mut State, mut t1: TypeWrapper, mut t2: TypeWrapper) -> Res
                     if r1.is_row_type() && r2.is_row_type() =>
                 {
                     unify_rows(state, r1.clone(), r2.clone())
-                        .map_err(|err| err.into_unif_err(mk_tyw_enum!(; r1), mk_tyw_enum!(; r2)))
+                        .map_err(|err| err.into_unif_err(mk_tyw_enum!(r1), mk_tyw_enum!(r2)))
                 }
                 (TypeWrapper::Concrete(r), _) if !r.is_row_type() => {
-                    Err(UnifError::IllformedType(mk_tyw_enum!(; r)))
+                    Err(UnifError::IllformedType(mk_tyw_enum!(r)))
                 }
                 (_, TypeWrapper::Concrete(r)) if !r.is_row_type() => {
-                    Err(UnifError::IllformedType(mk_tyw_enum!(; r)))
+                    Err(UnifError::IllformedType(mk_tyw_enum!(r)))
                 }
-                (tyw1, tyw2) => unify(state, tyw1, tyw2),
+                (tyw1, tyw2) => unify_(state, tyw1, tyw2),
             },
             (AbsType::StaticRecord(tyw1), AbsType::StaticRecord(tyw2)) => match (*tyw1, *tyw2) {
                 (TypeWrapper::Concrete(r1), TypeWrapper::Concrete(r2))
@@ -1304,14 +1210,14 @@ pub fn unify(state: &mut State, mut t1: TypeWrapper, mut t2: TypeWrapper) -> Res
                 {
                     Err(UnifError::IllformedType(mk_tyw_record!(; r)))
                 }
-                (tyw1, tyw2) => unify(state, tyw1, tyw2),
+                (tyw1, tyw2) => unify_(state, tyw1, tyw2),
             },
-            (AbsType::DynRecord(t), AbsType::DynRecord(t2)) => unify(state, *t, *t2),
+            (AbsType::DynRecord(t), AbsType::DynRecord(t2)) => unify_(state, *t, *t2),
             (AbsType::Forall(i1, t1t), AbsType::Forall(i2, t2t)) => {
                 // Very stupid (slow) implementation
                 let constant_type = state.table.fresh_const();
 
-                unify(
+                unify_(
                     state,
                     t1t.subst(i1, constant_type.clone()),
                     t2t.subst(i2, constant_type),
@@ -1373,7 +1279,7 @@ pub fn unify_rows(
             let (ty2, t2_tail) = row_add(state, &id, ty.clone(), TypeWrapper::Concrete(r2))?;
             match (ty, ty2) {
                 (None, None) => Ok(()),
-                (Some(ty), Some(ty2)) => unify(state, *ty, *ty2)
+                (Some(ty), Some(ty2)) => unify_(state, *ty, *ty2)
                     .map_err(|err| RowUnifError::RowMismatch(id.clone(), Box::new(err))),
                 (ty1, ty2) => Err(RowUnifError::RowKindMismatch(
                     id,
@@ -1393,7 +1299,7 @@ pub fn unify_rows(
                 // since we are unifying types with a constant or a unification variable somewhere,
                 // the only unification errors that should be possible are related to constants or
                 // row constraints.
-                (t1_tail, t2_tail) => unify(state, t1_tail, t2_tail).map_err(|err| match err {
+                (t1_tail, t2_tail) => unify_(state, t1_tail, t2_tail).map_err(|err| match err {
                     UnifError::ConstMismatch(c1, c2) => RowUnifError::ConstMismatch(c1, c2),
                     UnifError::WithConst(c1, tyw) => RowUnifError::WithConst(c1, tyw),
                     UnifError::RowConflict(id, tyw_opt, _, _) => {
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index 816d424f..572493b2 100644
--- a/src/typecheck/operation.rs
+++ b/src/typecheck/operation.rs
@@ -22,11 +22,16 @@ pub fn get_uop_type(
                 mk_tyw_arrow!(branches.clone(), branches.clone(), branches),
             )
         }
-        // Dyn -> [| Num, Bool, Str, Enum, Fun, Array, Record, Lbl, Other |]
-        UnaryOp::Typeof() => (
-            mk_typewrapper::dynamic(),
-            mk_tyw_enum!("Num", "Bool", "Str", "Enum", "Fun", "Array", "Record", "Lbl", "Other"),
-        ),
+        // forall a. a -> Bool
+        UnaryOp::IsNum()
+        | UnaryOp::IsBool()
+        | UnaryOp::IsStr()
+        | UnaryOp::IsFun()
+        | UnaryOp::IsArray()
+        | UnaryOp::IsRecord() => {
+            let inp = TypeWrapper::Ptr(state.table.fresh_var());
+            (inp, mk_typewrapper::bool())
+        }
         // Bool -> Bool -> Bool
         UnaryOp::BoolAnd() | UnaryOp::BoolOr() => (
             mk_typewrapper::bool(),
@@ -47,7 +52,7 @@ pub fn get_uop_type(
             let row = TypeWrapper::Ptr(state.table.fresh_var());
             // Constraining a freshly created variable should never fail.
             constraint(state, row.clone(), id.clone()).unwrap();
-            (mk_tyw_enum!(; row.clone()), mk_tyw_enum!(id.clone(); row))
+            (mk_tyw_enum!(row.clone()), mk_tyw_enum!(id.clone(), row))
         }
         // This should not happen, as Switch() is only produced during evaluation.
         UnaryOp::Switch(_) => panic!("cannot typecheck Switch()"),
@@ -165,35 +170,7 @@ pub fn get_uop_type(
         // Str -> < | Dyn>
         UnaryOp::EnumFromStr() => (
             mk_typewrapper::str(),
-            mk_tyw_enum!(; mk_typewrapper::dynamic()),
-        ),
-        // Str -> Str -> Bool
-        UnaryOp::StrIsMatch() => (
-            mk_typewrapper::str(),
-            mk_tyw_arrow!(mk_typewrapper::str(), mk_typewrapper::bool()),
-        ),
-        // Str -> Str -> {match: Str, index: Num, groups: Array Str}
-        UnaryOp::StrMatch() => (
-            mk_typewrapper::str(),
-            mk_tyw_arrow!(
-                mk_typewrapper::str(),
-                mk_tyw_record!(
-                    ("match", AbsType::Str()),
-                    ("index", AbsType::Num()),
-                    ("groups", mk_typewrapper::array(AbsType::Str()))
-                )
-            ),
-        ),
-        // Str -> Bool
-        UnaryOp::StrIsMatchCompiled(_) => (mk_typewrapper::str(), mk_typewrapper::bool()),
-        // Str -> {match: Str, index: Num, groups: Array Str}
-        UnaryOp::StrMatchCompiled(_) => (
-            mk_typewrapper::str(),
-            mk_tyw_record!(
-                ("match", AbsType::Str()),
-                ("index", AbsType::Num()),
-                ("groups", mk_typewrapper::array(AbsType::Str()))
-            ),
+            mk_tyw_enum!(mk_typewrapper::dynamic()),
         ),
     })
 }
@@ -320,7 +297,13 @@ pub fn get_bop_type(
         ),
         // <Md5, Sha1, Sha256, Sha512> -> Str -> Str
         BinaryOp::Hash() => (
-            mk_tyw_enum!("Md5", "Sha1", "Sha256", "Sha512"),
+            mk_tyw_enum!(
+                "Md5",
+                "Sha1",
+                "Sha256",
+                "Sha512",
+                mk_typewrapper::row_empty()
+            ),
             mk_typewrapper::str(),
             mk_typewrapper::str(),
         ),
@@ -328,14 +311,14 @@ pub fn get_bop_type(
         BinaryOp::Serialize() => {
             let ty_input = TypeWrapper::Ptr(state.table.fresh_var());
             (
-                mk_tyw_enum!("Json", "Yaml", "Toml"),
+                mk_tyw_enum!("Json", "Yaml", "Toml", mk_typewrapper::row_empty()),
                 ty_input,
                 mk_typewrapper::str(),
             )
         }
         // <Json, Yaml, Toml> -> Str -> Dyn
         BinaryOp::Deserialize() => (
-            mk_tyw_enum!("Json", "Yaml", "Toml"),
+            mk_tyw_enum!("Json", "Yaml", "Toml", mk_typewrapper::row_empty()),
             mk_typewrapper::str(),
             mk_typewrapper::dynamic(),
         ),
@@ -351,6 +334,22 @@ pub fn get_bop_type(
             mk_typewrapper::str(),
             mk_typewrapper::bool(),
         ),
+        // Str -> Str -> Bool
+        BinaryOp::StrIsMatch() => (
+            mk_typewrapper::str(),
+            mk_typewrapper::str(),
+            mk_typewrapper::bool(),
+        ),
+        // Str -> Str -> {match: Str, index: Num, groups: Array Str}
+        BinaryOp::StrMatch() => (
+            mk_typewrapper::str(),
+            mk_typewrapper::str(),
+            mk_tyw_record!(
+                ("match", AbsType::Str()),
+                ("index", AbsType::Num()),
+                ("groups", mk_typewrapper::array(AbsType::Str()))
+            ),
+        ),
         // Str -> Str -> Array Str
         BinaryOp::StrSplit() => (
             mk_typewrapper::str(),
diff --git a/stdlib/array.ncl b/stdlib/array.ncl
index 0a79d06e..dd4971d0 100644
--- a/stdlib/array.ncl
+++ b/stdlib/array.ncl
@@ -30,7 +30,7 @@
         ```
         "%m
       = fun label value =>
-       if %typeof% value == `Array then
+       if %is_array% value then
          if %length% value != 0 then
            value
          else
diff --git a/stdlib/builtin.ncl b/stdlib/builtin.ncl
index d151a8ed..6fada500 100644
--- a/stdlib/builtin.ncl
+++ b/stdlib/builtin.ncl
@@ -5,33 +5,29 @@
         Possible dynamic type for a value. Must be one of the tags:
 
         ```
-         `Num
-         `Bool
-         `Str
-         `Enum
-         `Fun
-         `Array
-         `Record
-         `Lbl
+         `TypeNum
+         `TypeBool
+         `TypeStr
+         `TypeFun
+         `TypeArray
+         `TypeRecord
          `Other
         ```
         "%m
       = fun label =>
         label
         |> contract.tag m%"
-          must be one of `Num, `Bool, `Str, `Enum, `Fun, `Array`, `Record, `Lbl or `Other
+          must be one of `TypeNum, `TypeBool, `TypeStr, `TypeFun, `TypeArray`, `TypeRecord or `Other
         "%m
         # The enum type syntax [| ... |] is not stable. Do not rely on it in
         # your own Nickel programs.
-        |> contract.apply [|
-            Num,
-            Bool,
-            Str,
-            Enum,
-            Lbl,
-            Fun,
-            Array,
-            Record,
+        | contract.apply [|
+            TypeNum,
+            TypeBool,
+            TypeStr,
+            TypeFun,
+            TypeArray,
+            TypeRecord,
             Other
           |],
 
@@ -82,7 +78,7 @@
           false
       ```
       "%m
-    = fun x => %typeof% x == `Num,
+    = fun x => %is_num% x,
 
     is_bool : Dyn -> Bool
     | doc m%"
@@ -96,7 +92,7 @@
           false
       ```
       "%m
-    = fun x => %typeof% x == `Bool,
+    = fun x => %is_bool% x,
 
     is_str : Dyn -> Bool
     | doc m%"
@@ -104,28 +100,13 @@
 
       For example:
       ```nickel
-        is_str true =>
+        is_bool true =>
           false
-        is_str "Hello, World!" =>
+        is_bool "Hello, World!" =>
           true
       ```
       "%m
-    = fun x => %typeof% x == `Str,
-
-    is_enum : Dyn -> Bool
-    | doc m%"
-      Checks if the given value is an enum tag.
-
-      For example:
-      ```nickel
-        is_enum true =>
-          false
-        is_enum `false =>
-          true
-      ```
-      "%m
-
-    = fun x => %typeof% x == `Enum,
+    = fun x => %is_str% x,
 
     is_fun : Dyn -> Bool
     | doc m%"
@@ -139,7 +120,7 @@
           false
       ```
       "%m
-    = fun x => %typeof% x == `Fun,
+    = fun x => %is_fun% x,
 
     is_array : Dyn -> Bool
     | doc m%"
@@ -153,7 +134,7 @@
           false
       ```
       "%m
-    = fun x => %typeof% x == `Array,
+    = fun x => %is_array% x,
 
     is_record : Dyn -> Bool
     | doc m%"
@@ -167,7 +148,7 @@
           true
       ```
       "%m
-    = fun x => %typeof% x == `Record,
+    = fun x => %is_record% x,
 
     typeof | Dyn -> ValueType
     | doc m%"
@@ -176,12 +157,19 @@
       For example:
       ```nickel
         typeof [ 1, 2 ] =>
-          `Array
+          `TypeArray
         typeof (fun x => x) =>
-          `Fun
+          `TypeFun
       ```
       "%m
-    = fun x => %typeof% x,
+    = fun x =>
+      if %is_num% x then `TypeNum
+      else if %is_bool% x then `TypeBool
+      else if %is_str% x then `TypeStr
+      else if %is_fun% x then `TypeFun
+      else if %is_array% x then `TypeArray
+      else if %is_record% x then `TypeRecord
+      else `Other,
 
     seq : forall a. Dyn -> a -> a
     | doc m%"
@@ -253,22 +241,5 @@
       ```
       "%m
     = fun format x => %deserialize% format x,
-
-    to_str | string.Stringable -> Str
-    | doc m%"
-      Converts a stringable value to a string representation. Same as
-      `string.from`.
-
-      For example:
-      ```nickel
-      from 42 =>
-        "42"
-      from `Foo =>
-        "Foo"
-      from null =>
-        "null"
-      "%m
-    = fun x => %to_str% x,
-
   }
 }
diff --git a/stdlib/contract.ncl b/stdlib/contract.ncl
index 14835f18..f5ab54fd 100644
--- a/stdlib/contract.ncl
+++ b/stdlib/contract.ncl
@@ -1,21 +1,21 @@
 {
   "$dyn" = fun l t => t,
 
-  "$num" = fun l t => if %typeof% t == `Num then t else %blame% l,
+  "$num" = fun l t => if %is_num% t then t else %blame% l,
 
-  "$bool" = fun l t => if %typeof% t == `Bool then t else %blame% l,
+  "$bool" = fun l t => if %is_bool% t then t else %blame% l,
 
-  "$string" = fun l t => if %typeof% t == `Str then t else %blame% l,
+  "$string" = fun l t => if %is_str% t then t else %blame% l,
 
   "$fail" = fun l t => %blame% l,
 
   "$array" = fun elt l t =>
-    if %typeof% t == `Array then
+    if %is_array% t then
       %map% t (fun value => %assume% elt (%go_array% l) value)
     else %blame% l,
 
   "$func" = fun s t l e =>
-      if %typeof% e == `Fun then
+      if %is_fun% e then
           (fun x => %assume% t (%go_codom% l) (e (%assume% s (%chng_pol% (%go_dom% l)) x)))
       else
           %blame% l,
@@ -34,13 +34,13 @@
           %assume% contr l t,
 
   "$record" = fun cont l t =>
-      if %typeof% t == `Record then
+      if %is_record% t then
           %assume% (cont {}) l t
       else
           %blame% (%tag% "not a record" l),
 
   "$dyn_record" = fun contr l t =>
-      if %typeof% t == `Record then
+      if %is_record% t then
           %record_map% t (fun _field value => %assume% contr l value)
       else
           %blame% (%tag% "not a record" l),
diff --git a/stdlib/num.ncl b/stdlib/num.ncl
index fc22f50a..ddd71612 100644
--- a/stdlib/num.ncl
+++ b/stdlib/num.ncl
@@ -13,7 +13,7 @@
       ```
       "%m
     = fun label value =>
-      if %typeof% value == `Num then
+      if %is_num% value then
         if value % 1 == 0 then
           value
         else
@@ -36,7 +36,7 @@
       ```
       "%m
     = fun label value =>
-      if %typeof% value == `Num then
+      if %is_num% value then
         if value % 1 == 0 && value >= 0 then
           value
         else
@@ -59,7 +59,7 @@
       ```
       "%m
     = fun label value =>
-      if %typeof% value == `Num then
+      if %is_num% value then
         if value % 1 == 0 && value > 0 then
           value
         else
@@ -80,7 +80,7 @@
       ```
       "%m
     = fun label value =>
-      if %typeof% value == `Num then
+      if %is_num% value then
         if value != 0 then
           value
         else
@@ -100,7 +100,7 @@
           false
       ```
       "%m
-    = fun x => x % 1 == 0,
+    = fun x => %is_num% x && (x % 1 == 0),
 
     min : Num -> Num -> Num
     | doc m%"
diff --git a/stdlib/string.ncl b/stdlib/string.ncl
index 9ef115ef..c392b3ea 100644
--- a/stdlib/string.ncl
+++ b/stdlib/string.ncl
@@ -16,7 +16,7 @@
       ```
       "%m
     = fun l s =>
-      if %typeof% s == `Str then
+      if %is_str% s then
         if s == "true" || s == "True" then
           "true"
         else if s == "false" || s == "False" then
@@ -41,10 +41,9 @@
       ```
       "%m
     = let pattern = m%"^[+-]?(\d+(\.\d*)?(e[+-]?\d+)?|\.\d+(e[+-]?\d+)?)$"%m in
-      let is_num_literal = %str_is_match% pattern in
       fun l s =>
-        if %typeof% s == `Str then
-          if is_num_literal s then
+        if %is_str% s then
+          if %str_is_match% s pattern then
             s
           else
             %blame% (%tag% "invalid num literal" l)
@@ -68,7 +67,7 @@
       ```
       "%m
     = fun l s =>
-      if %typeof% s == `Str then
+      if %is_str% s then
         if length s == 1 then
           s
         else
@@ -76,53 +75,6 @@
       else
         %blame% (%tag% "not a string" l),
 
-    EnumTag
-    | doc m%"
-      Contract to enforce the value is an enum tag.
-
-      For example:
-      ```nickel
-        (`foo | EnumTag) =>
-          `foo
-        (`FooBar | EnumTag) =>
-          `FooBar
-        ("tag" | EnumTag) =>
-          error
-      ```
-      "%m
-    = contract.from_predicate builtin.is_enum,
-
-    Stringable
-    | doc m%"
-      Contract to enforce the value is convertible to a string via
-      `builtin.to_string` or `string.from`. Accepted values are:
-
-      - numbers
-      - booleans
-      - strings
-      - enum tags
-      - null
-
-      For example:
-      ```nickel
-        (`Foo | Stringable) =>
-          `Foo
-        (false | Stringable) =>
-          false
-        ("bar" ++ "foo" | Stringable) =>
-          "barfoo"
-        ({foo = "baz"} | Stringable) =>
-          error
-      ```
-      "%m
-    = contract.from_predicate (fun value =>
-      let type = builtin.typeof value in
-      value == null
-      || type == `Num
-      || type == `Bool
-      || type == `Str
-      || type == `Enum),
-
     NonEmpty
     | doc m%"
       Contract to enforce the value is a non-empty string.
@@ -138,7 +90,7 @@
       ```
       "%m
     = fun l s =>
-      if %typeof% s == `Str then
+      if %is_str% s then
         if %str_length% s > 0 then
           s
         else
@@ -326,29 +278,8 @@
         is_match "\\d{4}" "123" =>
           false
       ```
-
-      For example, in the following program, the whole call to
-      `string.is_match "[0-9]*\\.?[0-9]+ x"` is re-evaluated at each invocation of
-      `is_number`. The regexp will be recompiled 3 times in total:
-
-      ```nickel
-      let is_number = fun x => string.is_match "[0-9]*\\.?[0-9]+" x in
-      ["0", "42", "0.5"] |> array.all is_number =>
-        true
-      ```
-
-      On the other hand, in the version below, the partial application of
-      `string.is_match "[0-9]*\\.?[0-9]+"` is evaluated once, returning a
-      function capturing the compiled regexp. The regexp will only be compiled
-      once and for all:
-
-      ```nickel
-      let is_number' = string.is_match "[0-9]*\\.?[0-9]+" in
-      ["0", "42", "0.5"] |> array.all is_number' =>
-        true
-      ```
       "%m
-    = fun regex => %str_is_match% regex,
+    = fun regex s => %str_is_match% s regex,
 
     match : Str -> Str -> {match: Str, index: Num, groups: Array Str}
     | doc m%"
@@ -362,12 +293,8 @@
         match "3" "01234" =>
           { match = "3", index = 3, groups = [ ] }
       ```
-
-      Note that this function may perform better by sharing its partial application between multiple calls,
-      because in this case the underlying regular expression will only be compiled once (See the documentation
-      of `string.is_match` for more details).
       "%m
-    = fun regex => %str_match% regex,
+    = fun regex s => %str_match% s regex,
 
     length : Str -> Num
     | doc m%"
@@ -399,36 +326,17 @@
       "%m
     = fun start end s => %str_substr% s start end,
 
-    from | Stringable -> Str
-    | doc m%"
-      Converts a correct value to a string representation. Same as
-      `builtin.to_str`.
-
-      For example:
-      ```nickel
-      from 42 =>
-        "42"
-      from `Foo =>
-        "Foo"
-      from null =>
-        "null"
-      "%m
-    = fun x => %to_str% x,
-
     from_num | Num -> Str
     | doc m%"
       Converts a number to its string representation.
 
-      For example:
-      ```nickel
       from_num 42 =>
         "42"
-      ```
       "%m
-    = from,
+    = fun n => %to_str% n,
 
     # from_enum | < | Dyn> -> Str = fun tag => %to_str% tag,
-    from_enum | EnumTag -> Str
+    from_enum | Dyn -> Str
     | doc m%"
       Converts an enum variant to its string representation.
 
@@ -438,7 +346,7 @@
         "MyEnum"
       ```
       "%m
-    = from,
+    = fun tag => %to_str% tag,
 
     from_bool | Bool -> Str
     | doc m%"
@@ -450,7 +358,7 @@
           "true"
       ```
       "%m
-    = from,
+    = fun b => %to_str% b,
 
     to_num | NumLiteral -> Num
     | doc m%"
@@ -481,7 +389,7 @@
     = fun s => s == "true",
 
     # to_enum | Str -> < | Dyn> = fun s => %enum_from_str% s,
-    to_enum | Str -> EnumTag
+    to_enum | Str -> Dyn
     | doc m%"
       Converts any string that represents an enum variant to that enum variant.
 


Test patch:
diff --git a/makam-spec/src/testnickel.makam b/makam-spec/src/testnickel.makam
new file mode 100644
index 00000000..e6a27fd9
--- /dev/null
+++ b/makam-spec/src/testnickel.makam
@@ -0,0 +1,489 @@
+%use "init".
+%use "row".
+
+(* This file defines a bunch of tests across many features
+ * of the Makam implementation of the Nickel language.
+ *
+ * They don't follow any particular organization and should be treated
+ * as a minimal set of expected behaviour. Also as examples.
+ *)
+
+nickel : testsuite. 
+
+testcase nickel :-
+    raw_interpreter "(fun x => x + x) 3" (eint 6) tnum.
+
+testcase nickel :-
+    raw_interpreter "let (x = true) in Ifte(x, 34, false)" (eint 34) tdyn.
+
+testcase nickel :-
+    not (
+        raw_interpreter "
+        let ( id = fun t => t ) in
+        Promise(Num,
+            Ifte( ( Promise(Bool -> Bool, id) ) true, 3, Promise(Num, true)) 
+        ) " _ _).
+
+testcase nickel :-
+    raw_interpreter "
+        let ( id = fun t => t ) in
+
+        Promise(Num,
+        Ifte( ( Promise(Bool -> Bool, id) ) true, 3, Assume(Num, true))
+        )
+    " (eint 3) tnum.
+
+testcase nickel :-
+    not (
+        raw_interpreter "
+        let ( id = fun t => t ) in
+
+        Promise(Num,
+        Ifte( ( Promise(Bool -> Bool, id) ) false, 3, Assume(Num, true))
+        )
+        " _ _
+    ).
+
+testcase nickel :-
+    raw_interpreter "
+    let ( id = fun t => t ) in
+
+    Promise(Num,
+    Ifte( ( Promise(Bool -> Bool, id) ) false, 3, Assume(Num, 5))
+    )
+    " (eint 5) tnum.
+
+testcase nickel :-
+    not (
+        interpreter "
+        let (id = fun x => x) in
+        Ifte(true, Promise(Num, id 3), Promise(Bool, id true))
+        " _ _
+    ).
+
+testcase nickel :-
+    raw_interpreter "
+        let (id = fun x => x) in
+        Ifte(true, Promise(Num, id 3), Assume(Bool, id true))
+        " (eint 3) tdyn.
+
+testcase nickel :-
+    raw_interpreter "
+    let (id = fun x => x) in
+    Ifte(false, Promise(Num, id 3), Assume(Bool, id true))
+    " (ebool true) tdyn.
+
+testcase nickel :-
+    raw_interpreter "
+    let (id = fun x => x) in
+    Ifte(false, Promise(Num, id 3), Assume(Bool, id true))
+    " (ebool true) tdyn.
+
+testcase nickel :-
+    raw_interpreter "
+    let (id = fun x => x) in
+    Ifte(true, Assume(Bool, id true), Promise(Num, id 3))
+    "
+    (ebool true)
+    tdyn.
+
+testcase nickel :-
+    raw_interpreter "
+    let (id = fun x => x) in
+    Ifte(true, Promise( Num , id 3), Promise( Bool, Assume( Bool -> Bool , id ) true))
+    " (eint 3) tdyn.
+
+testcase nickel :-
+    not (
+        raw_interpreter "
+        let (void = fun l => fun t => blame l) in
+        Assume(#void, 3)
+        " _ _
+    ).
+
+testcase nickel :-
+    not (
+        raw_interpreter "
+        let (alwaysTrue = fun l => fun t => Ifte(t, t, blame l)) in
+        Assume(#alwaysTrue, false)
+        " _ _
+    ).
+
+testcase nickel :-
+    raw_interpreter "
+    let (alwaysTrue = fun l => fun t => Ifte(t, t, blame l)) in
+    Assume(#alwaysTrue, true)
+    " (ebool true) (fromExpr (named "alwaysTrue")).
+
+testcase nickel :-
+    raw_interpreter "
+    let (void = fun l => fun t => blame l) in
+    Promise( #void -> #void, fun x => x)" V T,
+    eq V (lam (bind "x" (fun x => x))),
+    eq T (tarrow (fromExpr (named "void")) (fromExpr (named "void"))).
+
+testcase nickel :-
+    raw_interpreter "
+    let (f = fun x => Ifte(x, f false, 3)) in
+    f true
+    " (eint 3) tnum.
+
+testcase nickel :-
+    raw_interpreter "
+    let (f = (let (f = fun x => 3 - x) in f 1)) in f + f
+    " (eint 4) tnum.
+
+testcase nickel :-
+    raw_interpreter "
+    let (f = fun x => x + 1) in
+    fun y => f y" 
+    (lam (bind "y" (fun y => app (recThunk "f" (fun f => lam (bind "x" (fun x => ebinop x add (eint 1)))) V') y))) 
+    (tarrow tnum tnum).
+
+
+nickel_typing : testsuite.
+
+testcase nickel_typing :-
+    p_typecheck
+    "true"
+    tbool.
+
+testcase nickel_typing :-
+    p_typecheck
+    "34"
+    tnum.
+
+testcase nickel_typing :-
+    p_typecheck
+    "34"
+    tdyn.
+
+testcase nickel_typing :-
+    p_typecheck
+    "\"hola\""
+    tstr.
+
+testcase nickel_typing :-
+    p_typecheck
+    "fun x => x"
+    (tarrow A A).
+
+testcase nickel_typing :-
+    p_typecheck
+    "fun x => x"
+    (tarrow tdyn tdyn).
+
+testcase nickel_typing :-
+    p_typecheck
+    "fun x => x"
+    tdyn.
+
+testcase nickel_typing :-
+    p_typecheck
+    "let (x = 34) in x + 2"
+    tnum.
+
+testcase nickel_typing :-
+    p_typecheck
+    "(fun x => x) 3"
+    tnum.
+
+testcase nickel_typing :-
+    p_typecheck
+    "Promise(Bool -> Bool, fun x => x) 3"
+    tdyn.
+
+testcase nickel_typing :-
+    p_typecheck
+    "Promise(Num -> Num, fun x => x) 3"
+    tnum.
+
+testcase nickel_typing :-
+    not (p_typecheck
+        "Promise(Num -> Bool, fun x => x) 3"
+        _
+    ).
+(* forall *)
+
+testcase nickel :-
+    raw_interpreter "
+    Promise(forall a . a -> a, fun x => x) "
+    (lam (bind "x" (fun x => x)))
+    (forall (bind "a" (fun a => tarrow a a))).
+
+testcase nickel :-
+    raw_interpreter "
+    Promise(forall a . a -> a, fun x => x) 3 "
+    (eint 3)
+    (tdyn).
+
+testcase nickel :-
+    raw_interpreter "
+    Assume(forall a . a -> a, fun x => x) 3 "
+    (eint 3) tdyn.
+
+testcase nickel :-
+    not (raw_interpreter "
+    Assume(forall a . a -> a, fun x => 2) 3 "
+    _ _).
+
+testcase nickel :-
+    raw_interpreter 
+    "(Assume(forall a . a -> (a -> a) ->  a, fun x => fun f => f x) 3) (fun y => 2 + y)"
+    (eint 5)
+    tdyn.
+
+testcase nickel :-
+    raw_interpreter
+    "(Assume(forall a . a -> (a -> a) ->  a, fun x => fun f => f (f x)) 3) (fun y => 2 + y)"
+    (eint 7)
+    tdyn.
+
+testcase nickel :-
+    not (raw_interpreter
+        "(Assume(forall a . a -> (a -> a) ->  a, fun x => fun f => f 2) 34) (fun y => 25 + y)"
+        _ _
+    ).
+
+testcase nickel :-
+    raw_interpreter
+    "(Assume(forall a . a -> (a -> Num) ->  Num, fun x => fun f => f x) 3) (fun y => Ifte(isNum y, y, 0))"
+    (eint 3)
+    tdyn.
+
+testcase nickel :-
+    raw_interpreter
+    "(Assume(forall a . a -> (a -> Num) ->  Num, fun x => fun f => f x) true) (fun y => Ifte(isNum y, y, 0))"
+    (eint 0)
+    tdyn.
+
+testcase nickel :-
+    raw_interpreter
+    "(Assume(forall a . forall b . (a -> b) -> a -> b, fun f => f) (fun x => 34)) true"
+    (eint 34)
+    tdyn.
+
+testcase nickel :-
+(* No impredicative polymorphism, no matter how bad you want it *)
+    raw_interpreter
+    "(Assume(Num -> (forall a. a -> a) -> Num, fun n => fun f => f n) 34) (fun x => x)"
+    (eint 34)
+    tdyn.
+
+testcase nickel :-
+    raw_interpreter
+        "let (f = Promise(forall a . a -> a, fun x => x)) in
+        Promise((Num -> Num) -> Num, fun f => f 2) f"
+        (eint 2) tnum.
+
+testcase nickel :-
+    not (raw_interpreter
+        "let (f = Promise(forall a . a -> a, fun x => x)) in
+        Promise(Num, Promise((Bool -> Num) -> Num, fun f => f true) f)"
+        _ _ ).
+
+testcase nickel :-
+    raw_interpreter
+        "let (f = Promise(forall a . a -> a, fun x => x)) in
+        (Promise((Bool -> Num) -> Num, fun f => f true) f)"
+        (ebool true) tdyn.
+
+testcase nickel :-
+    not (raw_interpreter
+        "(Assume(Num -> (forall a. a -> a) -> Num, fun n => fun f => f n) 34) (fun x => 2)"
+        _ _
+    ).
+
+(* Records *)
+
+testcase nickel :-
+    isocast 
+    "{ hello : 3 ; chau : \"4\" ; $(Ifte(true, \"hello\", \"chau\")) : 5 ; $(Ifte(true, \"hello\", \"chau\")) : 4 }" 
+    (E: expr),
+    typecheck E (open_rec tnum [ ("hello", tnum) , ("chau", tstr)]).
+
+testcase nickel :-
+    isocast 
+    "Promise({ _:Bool, hello: Num}, 3)" 
+    (E: expr), 
+    not (typecheck E _).
+
+testcase nickel :-
+    raw_interpreter "{$(\"bla\"): 5 }"
+    (rec_val [ (tuple "bla" (eint 5)) ] (fun s => eunop blame (label false _ _ _)))
+    (open_rec tnum []).
+
+testcase nickel :-
+    raw_interpreter 
+    "{$(Ifte(true, \"hello\", \"chau\")) : false; $(\"bla\"): true; blop : true }.blop"
+    (ebool true)
+    tbool.
+
+testcase nickel :-
+    raw_interpreter 
+    "{$(Ifte(true, \"hello\", \"chau\")) : false; $(\"bla\"): true; blop : true }.hello"
+    (ebool false)
+    tbool.
+
+testcase nickel :-
+    raw_interpreter 
+    "{$(Ifte(true, \"hello\", \"chau\")) : false; $(\"bla\"): 3; blop : true }.hello"
+    (ebool false)
+    tdyn.
+
+(* TODO: Still not checking that there are no extra fields *)
+testcase nickel :-
+    raw_interpreter
+    "let (f = Assume({hello: Bool} -> Bool, fun x => (x).hello)) in
+    f {hello: false }"
+    (ebool false)
+    tbool.
+
+testcase nickel :-
+    not (
+        raw_interpreter
+        "let (f = Assume({hello: Bool} -> Bool, fun x => (x).hello)) in
+        f {$\"hello\": true; $\"hola\": 42 ; chau : 3}"
+        _ _
+    ).
+
+testcase nickel :-
+    not (
+        raw_interpreter
+        "let (f = Assume({hello: Bool} -> Bool, fun x => (x).hello)) in
+        f {hola: false ; chau : 3}"
+        _ _
+    ).
+
+testcase nickel :-
+    raw_interpreter
+    "let (f = Promise({hello: Bool} -> Bool, fun x => (x).hello)) in
+    f {hello: false ; chau : 3}"
+    (ebool false)
+    tdyn.
+
+testcase nickel :-
+    p_typecheck
+    "Promise({hello: Bool} -> Bool, fun x => (x).hello)"
+    (tarrow (clos_rec [("hello", tbool)]) tbool).
+
+testcase nickel :-
+    not(
+        raw_interpreter
+        "Assume( { _ : Bool , } , {blop : 3; blip : false}).blop"
+        _ _
+    ).
+
+testcase nickel :-
+    raw_interpreter
+    "Assume({_: Bool ,}, {blop : 3; blip : false}).blip"
+    (ebool false)
+    tbool.
+
+testcase nickel :-
+    not (raw_interpreter
+    "{blop: 3; blop: false}"
+    _ _).
+
+(* Rows *)
+
+testcase nickel :-
+    row.empty A, row.add 2 A, row.add 3 A,
+    row.member A 2, row.member A 3, not(row.member A 1).
+
+testcase nickel :-
+    row.empty A, row.add 2 A, row.add 3 A, row.add 2 A,
+    row.toList A [2, 3].
+
+testcase nickel :-
+    row.fromList [1, 2, 3, 1] R,
+    row.member R 1, row.member R 2, row.member R 3,
+    row.remove 1 R A, not(row.member A 1).
+
+testcase nickel :-
+    row.empty A, row.add 2 A, row.remove 2 A R,
+    not (row.add 2 R).
+
+testcase nickel :-
+    row.empty A, row.add 2 A, row.close A,
+    row.member A 2, not(row.add 3 A), row.add 2 A.
+
+testcase nickel :-
+    row.fromList [1,2 ,3] R, row.close R, row.fromList [1,2] RR, eqv RR R.
+
+testcase nickel :-
+    row.fromList [1,2 ,3] R, row.fromList [1,2] RR, row.close RR, not(eqv RR R).
+
+
+(* Enums *)
+
+testcase nickel :-
+    isocast "`ble" (enum_var "ble").
+
+testcase nickel :-
+    isocast 
+        "switch (`ble) { blu => 2 , ble => 0}"
+        (enum_case
+            (enum_var "ble")
+            [("blu", eint 2), ("ble", eint 0)]
+            none
+        ).
+
+testcase nickel :-
+    isocast 
+        "switch (`ble) { blu => 2 , ble => 0 , @ => 4}"
+        (enum_case
+            (enum_var "ble")
+            [("blu", eint 2), ("ble", eint 0)]
+            (some (eint 4))
+        ).
+
+testcase nickel :-
+    isocast
+        "is<blop, blap> 3"
+        (eunop (isEnumIn ["blop", "blap"]) (eint 3)).
+
+testcase nickel :-
+    isocast
+        "Assume(<bla>, 2)"
+        (assume (tenum R) _ (eint 2)),
+    row.fromList ["bla"] R', row.close R', eqv R R'.
+
+testcase nickel :-
+    raw_interpreter
+        "Assume(<bla>, `bla)"
+        (enum_var "bla")
+        _.
+
+testcase nickel :-
+    not(raw_interpreter
+        "Assume(<bla>, `ble)"
+        _ _).
+
+testcase nickel :-
+    raw_interpreter
+    "switch (`ble) {bli => 0, ble => 1, blo => 34}"
+    (eint 1)
+    tnum.
+
+testcase nickel :-
+    not(raw_interpreter
+    "switch (`ble) {bli => 1, blo => 34}"
+    _ _).
+
+testcase nickel :-
+    p_typecheck
+    "`ble"
+    (tenum R),
+    row.fromList ["ble"] R', eqv R R'.
+
+testcase nickel :-
+    p_typecheck 
+    "fun x => switch x {bla => 2, ble => 1}"
+    (tarrow (tenum (extend "bla" (extend "ble" closed))) tnum).
+
+(*
+This is why ocaml has upper/lower bounds
+p_typecheck
+"fun x => (switch x {bla => 2, ble => 1}) + (switch x {bla => 3})" (`bla) ?
+*)
diff --git a/src/eval/tests.rs b/src/eval/tests.rs
index 8f86e747..b0338b3f 100644
--- a/src/eval/tests.rs
+++ b/src/eval/tests.rs
@@ -85,17 +85,17 @@ fn simple_plus() {
 
 #[test]
 fn asking_for_various_types() {
-    let num = mk_term::op1(UnaryOp::Typeof(), Term::Num(45.3));
-    assert_eq!(Ok(Term::Enum("Num".into())), eval_no_import(num));
+    let num = mk_term::op1(UnaryOp::IsNum(), Term::Num(45.3));
+    assert_eq!(Ok(Term::Bool(true)), eval_no_import(num));
 
-    let boolean = mk_term::op1(UnaryOp::Typeof(), Term::Bool(true));
-    assert_eq!(Ok(Term::Enum("Bool".into())), eval_no_import(boolean));
+    let boolean = mk_term::op1(UnaryOp::IsBool(), Term::Bool(true));
+    assert_eq!(Ok(Term::Bool(true)), eval_no_import(boolean));
 
     let lambda = mk_term::op1(
-        UnaryOp::Typeof(),
+        UnaryOp::IsFun(),
         mk_fun!("x", mk_app!(mk_term::var("x"), mk_term::var("x"))),
     );
-    assert_eq!(Ok(Term::Enum("Fun".into())), eval_no_import(lambda));
+    assert_eq!(Ok(Term::Bool(true)), eval_no_import(lambda));
 }
 
 fn mk_default(t: RichTerm) -> Term {
diff --git a/src/parser/tests.rs b/src/parser/tests.rs
index 9cc61100..1f63e4fc 100644
--- a/src/parser/tests.rs
+++ b/src/parser/tests.rs
@@ -140,13 +140,13 @@ fn lets() {
 #[test]
 fn unary_op() {
     assert_eq!(
-        parse_without_pos("%typeof% x"),
-        mk_term::op1(UnaryOp::Typeof(), mk_term::var("x"))
+        parse_without_pos("%is_num% x"),
+        mk_term::op1(UnaryOp::IsNum(), mk_term::var("x"))
     );
     assert_eq!(
-        parse_without_pos("%typeof% x y"),
+        parse_without_pos("%is_num% x y"),
         mk_app!(
-            mk_term::op1(UnaryOp::Typeof(), mk_term::var("x")),
+            mk_term::op1(UnaryOp::IsNum(), mk_term::var("x")),
             mk_term::var("y")
         ),
     );
diff --git a/tests/pass/records.ncl b/tests/pass/records.ncl
index c1a1b0c7..67785eb1 100644
--- a/tests/pass/records.ncl
+++ b/tests/pass/records.ncl
@@ -29,7 +29,7 @@ let Assert = fun l x => x || %blame% l in
     == 2,
 
   let r = record.map
-      (fun y x => if %typeof% x == `Num then x + 1 else 0)
+      (fun y x => if %is_num% x then x + 1 else 0)
       {foo = 1, bar = "it's lazy"} in
     (r.foo) + (r.bar) == 2,
 
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index 7c325a85..3afe8a3c 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -13,6 +13,10 @@ let typecheck = [
   # 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)),
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index 4cab24e0..2117dec3 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -4,14 +4,15 @@ use nickel_lang::cache::resolvers::DummyResolver;
 use nickel_lang::error::TypecheckError;
 use nickel_lang::parser::{grammar, lexer};
 use nickel_lang::term::RichTerm;
-use nickel_lang::typecheck::{type_check_in_env, Environment};
+use nickel_lang::typecheck::{type_check_in_env, Environment, TypeCheckingOutput};
 use nickel_lang::types::{AbsType, Types};
 
-fn type_check(rt: &RichTerm) -> Result<(), TypecheckError> {
-    type_check_in_env(rt, &Environment::new(), &mut DummyResolver {}).map(|_| ())
+fn type_check(rt: &RichTerm) -> Result<Types, TypecheckError> {
+    type_check_in_env(rt, &Environment::new(), &mut DummyResolver {})
+        .map(|TypeCheckingOutput { types, .. }| types)
 }
 
-fn type_check_expr(s: impl std::string::ToString) -> Result<(), TypecheckError> {
+fn type_check_expr(s: impl std::string::ToString) -> Result<Types, TypecheckError> {
     let s = s.to_string();
     let id = Files::new().add("<test>", s.clone());
     type_check(
@@ -170,7 +171,7 @@ fn let_inference() {
 fn polymorphic_row_constraints() {
     // Assert that the result of evaluation is either directly a `RowConflict` error, or a
     // `RowConflict` wrapped in an `ArrowTypeMismatch`.
-    fn assert_row_conflict(res: Result<(), TypecheckError>) {
+    fn assert_row_conflict(res: Result<Types, TypecheckError>) {
         assert!(match res.unwrap_err() {
             TypecheckError::RowConflict(_, _, _, _, _) => true,
             TypecheckError::ArrowTypeMismatch(_, _, _, err_boxed, _) => {