Repository: tweag/nickel
Pull request #713 (2022-05-29 00:11:02)

flake.lock: Update
Automated changes by the [update-flake-lock](https://github.com/DeterminateSystems/update-flake-lock) GitHub Action.

```
Flake lock file updates:

• Updated input 'flake-utils':
    'github:numtide/flake-utils/04c1b180862888302ddfb2e3ad9eaa63afc60cf8' (2022-05-17)
  → 'github:numtide/flake-utils/bee6a7250dd1b01844a2de7e02e4df7d8a0a206c' (2022-06-24)
• Updated input 'nixpkgs':
    'github:NixOS/nixpkgs/48037fd90426e44e4bf03e6479e88a11453b9b66' (2022-05-18)
  → 'github:NixOS/nixpkgs/6141b8932a5cf376fe18fcd368cecd9ad946cb68' (2022-06-23)
• Updated input 'pre-commit-hooks':
    'github:cachix/pre-commit-hooks.nix/521a524771a8e93caddaa0ac1d67d03766a8b0b3' (2022-05-16)
  → 'github:cachix/pre-commit-hooks.nix/db3bd555d3a3ceab208bed48f983ccaa6a71a25e' (2022-06-25)
• Updated input 'rust-overlay':
    'github:oxalica/rust-overlay/3bc2619665745f5e6f2efc3d0664edad4f62201b' (2022-05-21)
  → 'github:oxalica/rust-overlay/59a3a304c987dc65d2a33de0a77a1ae6ae777cd4' (2022-06-25)
```

### Running GitHub Actions on this PR

GitHub Actions will not run workflows on pull requests which are opened by a GitHub Action.

To run GitHub Actions workflows on this PR, run:

```sh
git branch -D update_flake_lock_action
git fetch origin
git checkout update_flake_lock_action
git commit --amend --no-edit
git push origin update_flake_lock_action --force
```


Patch:
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/flake.lock b/flake.lock
index a622b8f8..a3e05ff5 100644
--- a/flake.lock
+++ b/flake.lock
@@ -2,11 +2,11 @@
   "nodes": {
     "flake-utils": {
       "locked": {
-        "lastModified": 1652776076,
-        "narHash": "sha256-gzTw/v1vj4dOVbpBSJX4J0DwUR6LIyXo7/SuuTJp1kM=",
+        "lastModified": 1656065134,
+        "narHash": "sha256-oc6E6ByIw3oJaIyc67maaFcnjYOz1mMcOtHxbEf9NwQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "04c1b180862888302ddfb2e3ad9eaa63afc60cf8",
+        "rev": "bee6a7250dd1b01844a2de7e02e4df7d8a0a206c",
         "type": "github"
       },
       "original": {
@@ -32,11 +32,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1652885393,
-        "narHash": "sha256-YIgvvlk4iQ1Hi7KD9o5gsojc+ApB+jiH1d5stK8uXiw=",
+        "lastModified": 1655983783,
+        "narHash": "sha256-0h1FzkYWei24IdKNpCX93onkF/FMiXQG8SdEbTc0r8A=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "48037fd90426e44e4bf03e6479e88a11453b9b66",
+        "rev": "6141b8932a5cf376fe18fcd368cecd9ad946cb68",
         "type": "github"
       },
       "original": {
@@ -55,11 +55,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1652714503,
-        "narHash": "sha256-qQKVEfDe5FqvGgkZtg5Pc491foeiDPIOeycHMqnPDps=",
+        "lastModified": 1656169028,
+        "narHash": "sha256-y9DRauokIeVHM7d29lwT8A+0YoGUBXV3H0VErxQeA8s=",
         "owner": "cachix",
         "repo": "pre-commit-hooks.nix",
-        "rev": "521a524771a8e93caddaa0ac1d67d03766a8b0b3",
+        "rev": "db3bd555d3a3ceab208bed48f983ccaa6a71a25e",
         "type": "github"
       },
       "original": {
@@ -87,11 +87,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1653118478,
-        "narHash": "sha256-K9fG0VT/Wi/QJpXJd6d1QrWL5ulAhy1S67n5OGBwbcE=",
+        "lastModified": 1656125323,
+        "narHash": "sha256-Ckez1NOVyPLOEI2zbSok6oDCm/xJxX/pietAWukEwoo=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "3bc2619665745f5e6f2efc3d0664edad4f62201b",
+        "rev": "59a3a304c987dc65d2a33de0a77a1ae6ae777cd4",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index f7442169..be4259d2 100644
--- a/flake.nix
+++ b/flake.nix
@@ -176,9 +176,11 @@
           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;
 
@@ -262,6 +264,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
@@ -286,21 +306,7 @@
         src = ./doc/manual;
         installPhase = ''
           mkdir -p $out
-          cp -r ./ $out
-        '';
-      };
-
-      stdlibDoc = pkgs.stdenv.mkDerivation {
-        name = "nickel-stdlib-doc-${version}";
-        src = ./stdlib;
-        installPhase = ''
-          mkdir -p $out
-          for file in *
-          do
-            module=$(basename $file .ncl)
-            ${self.defaultPackage."${system}"}/bin/nickel doc -f "$module.ncl" \
-              --output "$out/$module.md"
-          done
+          cp -r ./ "$out"
         '';
       };
 
@@ -313,7 +319,6 @@
         dockerImage = buildDocker packages.build; # TODO: docker image should be a passthru
         inherit vscodeExtension;
         inherit userManual;
-        inherit stdlibDoc;
       };
 
       devShell = devShells.stable;
@@ -326,6 +331,8 @@
       checks = {
         # wasm-opt can take long: eschew optimizations in checks
         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/src/bin/nickel.rs b/src/bin/nickel.rs
index 2cd20e67..c6d7fec4 100644
--- a/src/bin/nickel.rs
+++ b/src/bin/nickel.rs
@@ -6,15 +6,11 @@ use nickel_lang::repl::query_print;
 use nickel_lang::repl::rustyline_frontend;
 use nickel_lang::term::{RichTerm, Term};
 use nickel_lang::{serialize, serialize::ExportFormat};
-use std::path::{Path, PathBuf};
-use std::{
-    fs::{self, File},
-    process,
-};
+use std::path::PathBuf;
+use std::{fs, process};
 // use std::ffi::OsStr;
 use directories::BaseDirs;
 use structopt::StructOpt;
-
 /// Command-line options and subcommands.
 #[derive(StructOpt, Debug)]
 /// The interpreter of the Nickel language.
@@ -75,13 +71,7 @@ enum Command {
     },
     /// Generates the documentation files for the specified nickel file
     #[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.
-        #[structopt(short = "o", long, parse(from_os_str))]
-        output: Option<PathBuf>,
-    },
+    Doc {},
 }
 
 fn main() {
@@ -106,7 +96,6 @@ fn main() {
     } else {
         let mut program = opts
             .file
-            .clone()
             .map(Program::new_from_file)
             .unwrap_or_else(Program::new_from_stdin)
             .unwrap_or_else(|err| {
@@ -120,7 +109,7 @@ fn main() {
         }
 
         let result = match opts.command {
-            Some(Command::PprintAst { transform }) => program.pprint_ast(
+            Some(Command::PprintAst { transform }) => program.expand(
                 &mut std::io::BufWriter::new(Box::new(std::io::stdout())),
                 transform,
             ),
@@ -153,51 +142,7 @@ fn main() {
             Some(Command::Typecheck) => program.typecheck(),
             Some(Command::Repl { .. }) => unreachable!(),
             #[cfg(feature = "doc")]
-            Some(Command::Doc { ref output }) => output
-                .as_ref()
-                .map(|output| {
-                    fs::File::create(output.clone()).map_err(|e| {
-                        Error::IOError(IOError(format!(
-                            "when opening or creating output file `{}`: {}",
-                            output.to_string_lossy(),
-                            e.to_string()
-                        )))
-                    })
-                })
-                .unwrap_or_else(|| {
-                    let docpath = Path::new(".nickel/doc/");
-                    fs::create_dir_all(docpath).map_err(|e| {
-                        Error::IOError(IOError(format!(
-                            "when creating output path `{}`: {}",
-                            docpath.to_string_lossy(),
-                            e.to_string()
-                        )))
-                    })?;
-                    let mut markdown_file = docpath.to_path_buf();
-
-                    let mut has_file_name = false;
-
-                    if let Some(path) = opts.file {
-                        if let Some(file_stem) = path.file_stem() {
-                            markdown_file.push(file_stem);
-                            has_file_name = true;
-                        }
-                    }
-
-                    if !has_file_name {
-                        markdown_file.push("out");
-                    }
-
-                    markdown_file.set_extension("md");
-                    File::create(markdown_file.clone().into_os_string()).map_err(|e| {
-                        Error::IOError(IOError(format!(
-                            "when opening or creating output file `{}`: {}",
-                            markdown_file.to_string_lossy(),
-                            e.to_string()
-                        )))
-                    })
-                })
-                .and_then(|mut out| program.output_doc(&mut out)),
+            Some(Command::Doc { .. }) => program.output_doc(),
             None => program
                 .eval_full()
                 .map(|t| println!("{}", Term::from(t).deep_repr())),
diff --git a/src/eval/operation.rs b/src/eval/operation.rs
index 1e442e8a..e39557d8 100644
--- a/src/eval/operation.rs
+++ b/src/eval/operation.rs
@@ -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() => {
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..79bbb71d 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(),
@@ -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 11f2d4fe..176d24c4 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_key(|(k, _)| *k);
+    ret.sort_by(|x, y| x.0.cmp(&y.0));
     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 dfdb86fa..652736ae 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -128,8 +128,8 @@ impl Program {
 
     /// Create a markdown file with documentation for the specified program in `.nickel/doc/program_main_file_name.md`
     #[cfg(feature = "doc")]
-    pub fn output_doc(&mut self, out: &mut dyn std::io::Write) -> Result<(), Error> {
-        doc::output_doc(&mut self.cache, self.main_id, out)
+    pub fn output_doc(&mut self) -> Result<(), Error> {
+        doc::output_doc(&mut self.cache, self.main_id)
     }
 
     #[cfg(debug_assertions)]
@@ -137,7 +137,7 @@ impl Program {
         self.cache.skip_stdlib = true;
     }
 
-    pub fn pprint_ast(
+    pub fn expand(
         &mut self,
         out: &mut std::io::BufWriter<Box<dyn std::io::Write>>,
         apply_transforms: bool,
@@ -244,28 +244,43 @@ mod doc {
     use comrak::arena_tree::NodeEdge;
     use comrak::nodes::{Ast, AstNode, NodeCode, NodeHeading, NodeValue};
     use comrak::{format_commonmark, parse_document, Arena, ComrakOptions};
-    use std::io::Write;
+    use std::fs::{self, File};
+    use std::path::Path;
 
     /// Create a markdown file with documentation for the specified FileId.
-    pub fn output_doc(
-        cache: &mut Cache,
-        file_id: FileId,
-        out: &mut dyn Write,
-    ) -> Result<(), Error> {
+    pub fn output_doc(cache: &mut Cache, file_id: FileId) -> Result<(), Error> {
         cache.parse(file_id)?;
-        // unwrap(): at this point the term was correctly parsed and should exist in cache
-        let term = cache.get_ref(file_id).unwrap();
-        let document = AstNode::from(NodeValue::Document);
 
-        // Our nodes in the Markdown document are owned by this arena
-        let arena = Arena::new();
+        for (file_id, term) in cache.terms() {
+            let document = AstNode::from(NodeValue::Document);
+
+            // Our nodes in the Markdown document are owned by this arena
+            let arena = Arena::new();
+
+            // The default ComrakOptions disables all extensions (essentially reducing to CommonMark)
+            let options = ComrakOptions::default();
 
-        // The default ComrakOptions disables all extensions (essentially reducing to CommonMark)
-        let options = ComrakOptions::default();
+            // Populate the document with the documentation
+            to_markdown(&term.term, 0, &arena, &document, &options)?;
 
-        to_markdown(term, 0, &arena, &document, &options)?;
-        format_commonmark(&document, &options, out)
-            .map_err(|e| Error::IOError(IOError(e.to_string())))?;
+            // Create markdown file and write resulting markdown to it
+            let file_path: &Path = cache.files().name(*file_id).as_ref();
+            let file_name = file_path.file_name().ok_or_else(|| {
+                Error::IOError(IOError(format!(
+                    "Could not get file name of: {}",
+                    file_path.display()
+                )))
+            })?;
+            let docpath: &Path = Path::new(".nickel/doc/");
+            fs::create_dir_all(docpath).map_err(|e| Error::IOError(IOError(e.to_string())))?;
+            let mut markdown_file = docpath.to_path_buf();
+            markdown_file.push(file_name);
+            markdown_file.set_extension("md");
+            let mut file = File::create(markdown_file.clone().into_os_string())
+                .map_err(|e| Error::IOError(IOError(e.to_string())))?;
+            format_commonmark(&document, &options, &mut file)
+                .map_err(|e| Error::IOError(IOError(e.to_string())))?;
+        }
 
         Ok(())
     }
@@ -283,12 +298,8 @@ mod doc {
             Term::MetaValue(MetaValue { doc: Some(md), .. }) => {
                 document.append(&mut parse_documentation(header_level, arena, &md, options))
             }
-            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 {
+            Term::Record(hm, _) | Term::RecRecord(hm, _, _, _) => {
+                for (ident, rt) in hm {
                     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/serialize.rs b/src/serialize.rs
index d1c30e23..063a1e34 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_key(|(k, _)| *k);
+    entries.sort_by(|(k1, _), (k2, _)| k1.cmp(k2));
 
     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..598580f5 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.
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..2e6dfded 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -670,13 +670,13 @@ fn type_check_<L: Linearizer>(
                 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))
+            type_check_(state, envs, lin, linearizer, exp, mk_tyw_enum!(row))
         }
         Term::Var(x) => {
             let x_ty = envs
@@ -688,7 +688,7 @@ fn type_check_<L: Linearizer>(
         }
         Term::Enum(id) => {
             let row = state.table.fresh_unif_var();
-            unify(state, ty, mk_tyw_enum!(id.clone(); row))
+            unify(state, 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}`
@@ -1277,13 +1277,13 @@ 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),
             },
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index 816d424f..0d67b94b 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,7 +170,7 @@ pub fn get_uop_type(
         // Str -> < | Dyn>
         UnaryOp::EnumFromStr() => (
             mk_typewrapper::str(),
-            mk_tyw_enum!(; mk_typewrapper::dynamic()),
+            mk_tyw_enum!(mk_typewrapper::dynamic()),
         ),
         // Str -> Str -> Bool
         UnaryOp::StrIsMatch() => (
@@ -320,7 +325,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 +339,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(),
         ),
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..526eaa7e 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
@@ -43,7 +43,7 @@
     = 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_str% s then
           if is_num_literal s then
             s
           else
@@ -68,7 +68,7 @@
       ```
       "%m
     = fun l s =>
-      if %typeof% s == `Str then
+      if %is_str% s then
         if length s == 1 then
           s
         else
@@ -76,53 +76,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 +91,7 @@
       ```
       "%m
     = fun l s =>
-      if %typeof% s == `Str then
+      if %is_str% s then
         if %str_length% s > 0 then
           s
         else
@@ -399,36 +352,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 +372,7 @@
         "MyEnum"
       ```
       "%m
-    = from,
+    = fun tag => %to_str% tag,
 
     from_bool | Bool -> Str
     | doc m%"
@@ -450,7 +384,7 @@
           "true"
       ```
       "%m
-    = from,
+    = fun b => %to_str% b,
 
     to_num | NumLiteral -> Num
     | doc m%"
@@ -481,7 +415,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,