From 14e8a24dbf6bef43d2318af67cde2fe49e4b5118 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sun, 15 Mar 2020 13:19:34 +0200
Subject: [PATCH 01/17] Remove unused file `extract.ml`

---
 extract.ml | 175 -----------------------------------------------------
 1 file changed, 175 deletions(-)
 delete mode 100644 extract.ml

diff --git a/extract.ml b/extract.ml
deleted file mode 100644
index 94164696..00000000
--- a/extract.ml
+++ /dev/null
@@ -1,175 +0,0 @@
-(*
- * (c) 2014 Andreas Rossberg
- *)
-
-open Fomega
-
-type kind =
-  | BaseK
-  | ArrK of kind * kind
-  | ProdK of kind row
-
-type typ =
-  | VarT of var
-  | PrimT of Prim.typ
-  | ArrT of typ * typ
-  | ProdT of typ row
-  | AllT of var * kind * typ
-  | AnyT of var * kind * typ
-  | FunT of var * kind * typ
-  | AppT of typ * typ
-  | StrT of typ row
-  | DotT of typ * lab
-  | RecT of var * kind * typ
-  | InferT of typ lazy_t * int
-
-let rec print_typ' prec = function
-  | VarT(a, k, n) ->
-    let s = string_of_var a n in
-    if k <> BaseK && !verbose_vars_flag then
-      print_paren base_prec prec (fun () ->
-        print_string s;
-        print_string ":";
-        print_break 0 2;
-        print_kind' base_prec ctxt k
-      )
-    else
-      print_string s
-  | PrimT(t) ->
-    print_string (Prim.string_of_typ t)
-  | StrT(tr) ->
-    (match as_tup_row tr with
-    | Some ts ->
-      print_brack "(" ")" (fun () ->
-        print_list' print_typ' base_prec ctxt ts;
-      )
-    | None ->
-      print_brack "{" "}" (fun () ->
-        print_row' ":" print_typ' base_prec ctxt tr;
-      )
-    )
-  | FunT(a, k, t, s, p) ->
-    print_binder prec "!" a k (fun () ->
-      open_box 0;
-      print_typ' (binder_prec + 1) ([a]::ctxt) t;
-      close_box ();
-      print_string " ";
-      print_string
-        (match p with Impure -> "->" | Pure -> "=>" | Implicit -> "'=>");
-      print_break 1 2;
-      open_box 0;
-      print_extyp' binder_prec (enter "()" ctxt) s;
-      close_box ()
-    )
-  | TypT(s) ->
-    print_brack "[= " "]" (fun () -> print_extyp' base_prec ctxt s);
-  | PackT(s) ->
-    print_brack "[" "]" (fun () -> print_extyp' base_prec ctxt s);
-  | ProdT(tr) ->
-    print_brack "{" "}" (fun () ->
-      print_row' "=" print_typ' base_prec ctxt tr;
-    )
-  | LamT(a, k, t) ->
-    print_binder prec "\\" a k (fun () ->
-      print_typ' binder_prec ctxt t
-    )
-  | DotT(t, l) ->
-    if String.contains l '$' then
-      print_typ' prec ctxt t
-    else if matches_ctxt t ctxt then
-      print_string l
-    else
-      print_paren dot_prec prec (fun () ->
-        print_typ' dot_prec ctxt t;
-        print_string ".";
-        print_string l
-      )
-  | AppT(t1, t2) ->
-    print_paren app_prec prec (fun () ->
-      print_typ' app_prec ctxt t1;
-      print_string "(";
-      print_break 0 2;
-      print_typ' base_prec ctxt t2;
-      print_string ")"
-    )
-  | RecT(a, k, t) ->
-    print_binder prec "@" a k (fun () ->
-      print_typ' binder_prec ctxt t
-    )
-  | InferT(z) ->
-    match !z with
-    | Det t -> print_typ' prec ctxt t
-    | Undet u -> print_string (string_of_var ("'" ^ string_of_int u.id) u.level)
-
-let rec print_exp' prec = function
-  | VarE(x) -> print_var x
-  | PrimE(c) -> print_const c
-  | IfE(e1, e2, e3) ->
-    print_paren pre_prec prec (fun () ->
-      open_box 0;
-      print_string "if ";
-      print_exp' prec e1;
-      print_break 1 0;
-      print_string "then ";
-      print_exp' base_prec e2;
-      print_break 1 0;
-      print_string "then ";
-      print_exp' pre_prec e3;
-      close_box ()
-    )
-  | FunE(x, t, e) ->
-    print_paren pre_prec prec (fun () ->
-      open_box 0;
-      print_string "fun (";
-      print_var x;
-      print_string " : ";
-      print_typ' base_prec t;
-      print_string ")";
-      print_break 1 0;
-      print_string "-> ";
-      print_exp' pre_prec e;
-      close_box ()
-    )
-  | AppE(e1, e2) ->
-    print_paren app_prec prec (fun () ->
-      open_box 0;
-      print_exp' app_prec e1;
-      print_break 1 0;
-      print_exp' (app_prec + 1) e2;
-      close_box ()
-    )
-  | StrE(er) ->
-    print_paren tup_prec prec (fun () ->
-      print_list' print_exp' (tup_prec + 1) (List.map snd er)
-    )
-  | DotE(e, l) ->
-    print_paren pre_prec prec (fun () ->
-      open_box 0;
-      print_string "let ";
-      print_list' print_exp' tup_prec (List.map snd er)
- (* TODO *)
-      print_string " =";
-      print_break 1 2;
-      open_box 0;
-      print_exp' base_prec e;
-      close_box ();
-      print_break 1 0;
-      print_string "in";
-      print_break 1 0;
-      print_var l;
-      close_box ()
-    )
-  | GenE(a, k, e) ->
-    print_brack "(" ")" (fun () ->
-      open_box 0;
-      print_string "module ";
-      close_box ()
-    )
-  | InstE of exp * typ
-  | PackE(t1, e, t2) ->
-    
-  | OpenE of exp * var * var * exp
-  | RollE of exp * typ
-  | UnrollE of exp
-  | RecE of var * typ * exp
-  | LetE of exp * var * exp

From c90284b3c088e8adb22d7a70a9899c9148689368 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Mon, 16 Dec 2019 03:17:55 +0200
Subject: [PATCH 02/17] Add Travis CI integration

---
 .travis.yml | 22 ++++++++++++++++++++++
 travis.sh   | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 54 insertions(+)
 create mode 100644 .travis.yml
 create mode 100755 travis.sh

diff --git a/.travis.yml b/.travis.yml
new file mode 100644
index 00000000..f8d08c91
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,22 @@
+language: bash
+
+matrix:
+  include:
+    - os: linux
+      dist: bionic
+      addons:
+        apt:
+          packages:
+            - ocaml
+    - os: osx
+      osx_image: xcode12
+
+git:
+  depth: 5
+  submodules: false
+
+before_install:
+  - export -f travis_nanoseconds travis_time_start travis_time_finish
+
+script:
+  - ./travis.sh
diff --git a/travis.sh b/travis.sh
new file mode 100755
index 00000000..445b207d
--- /dev/null
+++ b/travis.sh
@@ -0,0 +1,32 @@
+#!/bin/bash -e
+
+if [ "$TRAVIS" = true ]; then
+  folded() {
+    FOLD=$((FOLD+1))
+    echo -e "travis_fold:start:cppsm.$FOLD\033[33;1m$1\033[0m"
+    travis_time_start
+    shift
+    echo "$@"
+    "$@"
+    travis_time_finish
+    echo -e "\ntravis_fold:end:cppsm.$FOLD\r"
+  }
+
+  case "$TRAVIS_OS_NAME" in
+    osx)
+      folded "Installing Ocaml" brew install ocaml;;
+  esac
+else
+  folded() {
+    echo
+    echo "RUNNING: $1"
+    shift
+    "$@"
+  }
+fi
+
+folded "Build 1ML" make
+
+for f in *.1ml; do
+  folded "$f" ./1ml -c prelude.1ml "$f"
+done

From 0197d949acaf43caffef18f551472d05296f85e7 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sat, 1 Feb 2020 22:50:24 +0200
Subject: [PATCH 03/17] Fix TRUE and FALSE are not keywords

---
 parser.mly | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/parser.mly b/parser.mly
index 1c8edd19..d5dd76c3 100644
--- a/parser.mly
+++ b/parser.mly
@@ -25,7 +25,7 @@ let ati i =
 let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %}
 
-%token TRUE FALSE HOLE PRIMITIVE
+%token HOLE PRIMITIVE
 %token FUN REC LET LOCAL IN DO WRAP UNWRAP TYPE INCLUDE END
 %token IF THEN ELSE OR AND AS
 %token EQUAL COLON SEAL ARROW DARROW

From 1a0fd06d33353c52f3bdc686ed956617691e5c4a Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Thu, 20 Feb 2020 21:55:52 +0200
Subject: [PATCH 04/17] Fix to remove duplicate `HOLE` rule of type expressions

The `HOLE` rule is now only a part of path expressions.  Removing the duplicate
rule resolves a ton of reduce-reduce conflicts in the grammar.
---
 parser.mly | 2 --
 1 file changed, 2 deletions(-)

diff --git a/parser.mly b/parser.mly
index d5dd76c3..0d368713 100644
--- a/parser.mly
+++ b/parser.mly
@@ -129,8 +129,6 @@ attyp :
     { PrimT($2)@@at() }
   | TYPE
     { TypT@@at() }
-  | HOLE
-    { HoleT@@at() }
   | LBRACE dec RBRACE
     { StrT($2)@@at() }
   | LPAR RPAR

From 1443ff9e17b7c72dc09448a39ef60c29bef53f52 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sat, 28 Dec 2019 15:40:19 +0200
Subject: [PATCH 05/17] Fix check_typ label for RollE

---
 fomega.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/fomega.ml b/fomega.ml
index 9b27b942..3e5c88c8 100644
--- a/fomega.ml
+++ b/fomega.ml
@@ -395,7 +395,7 @@ let rec infer_exp env = function
     | _ -> raise (Error "OpenE")
     )
   | RollE(e, t) ->
-    check_typ env t BaseK "PackE";
+    check_typ env t BaseK "RollE";
     (match unroll_typ t with
     | Some t' ->
       check_exp env e t' "RollE";

From c121c987820fc14ccf1bf589c21bce63043121b9 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sat, 21 Dec 2019 03:45:04 +0200
Subject: [PATCH 06/17] Fix to normalise types in compile and F-omega type
 check...

...so that they can be pattern matched.
---
 compile.ml     |  8 ++++----
 fomega.ml      | 14 +++++---------
 fomega.mli     |  2 --
 regression.1ml | 23 +++++++++++++++++++++++
 4 files changed, 32 insertions(+), 15 deletions(-)
 create mode 100644 regression.1ml

diff --git a/compile.ml b/compile.ml
index 620fe983..78b98852 100644
--- a/compile.ml
+++ b/compile.ml
@@ -30,7 +30,7 @@ let rec compile_exp env = function
   | F.AppE(e1, e2) ->
     let e1', t1 = compile_exp env e1 in
     let e2', _ = compile_exp env e2 in
-    (match F.force_typ t1 with
+    (match F.norm_typ t1 with
     | F.ArrT(_, t) -> L.AppE(e1', e2'), t
     | _ -> assert false
     )
@@ -41,7 +41,7 @@ let rec compile_exp env = function
     F.ProdT(tr)
   | F.DotE(e, l) ->
     let e', t = compile_exp env e in
-    (match F.force_typ t with
+    (match F.norm_typ t with
     | F.ProdT(tr) ->
       let i, t' = lookup_row l 0 (sort_row tr) in
       L.DotE(e', i), t'
@@ -52,7 +52,7 @@ let rec compile_exp env = function
     e', F.AllT(a, k, t)
   | F.InstE(e, t) ->
     let e', t' = compile_exp env e in
-    (match F.force_typ t' with
+    (match F.norm_typ t' with
     | F.AllT(a, k, t'') -> e', F.subst_typ [a, t] t''
     | _ -> assert false
     )
@@ -61,7 +61,7 @@ let rec compile_exp env = function
     e', t'
   | F.OpenE(e1, a, x, e2) ->
     let e1', t1 = compile_exp env e1 in
-    (match F.force_typ t1 with
+    (match F.norm_typ t1 with
     | F.AnyT(a, k, t) ->
       let e2', t2 = compile_exp (F.add_val x t (F.add_typ a k env)) e2 in
       L.LetE(e1', x, e2'), t2
diff --git a/fomega.ml b/fomega.ml
index 3e5c88c8..77eb324b 100644
--- a/fomega.ml
+++ b/fomega.ml
@@ -57,10 +57,6 @@ let tup_row xs = List.mapi (fun i x -> lab (i + 1), x) xs
 let lookup_lab l row =
   try List.assoc l row with Not_found -> raise (Error ("label " ^ l))
 
-let rec force_typ = function
-  | InferT(t', _) -> force_typ (Lazy.force t')
-  | t -> t
-
 let string_of_typ_fwd = ref (fun _ -> failwith "string_of_typ_fwd")
 let string_of_typ t = !string_of_typ_fwd t
 let string_of_kind_fwd = ref (fun _ -> failwith "string_of_kind_fwd")
@@ -361,25 +357,25 @@ let rec infer_exp env = function
     t
   | LamE(x, t, e) -> ArrT(t, infer_exp (add_val x t env) e)
   | AppE(e1, e2) ->
-    (match force_typ (infer_exp env e1) with
+    (match norm_typ (infer_exp env e1) with
     | ArrT(t2, t) -> check_exp env e2 t2 "AppE2"; t
     | _ -> raise (Error "AppE1")
     )
   | TupE(er) -> ProdT(infer_row infer_exp env er)
   | DotE(e, l) ->
-    (match force_typ (infer_exp env e) with
+    (match norm_typ (infer_exp env e) with
     | ProdT(tr) -> lookup_lab l tr
     | _ -> raise (Error "DotE1")
     )
   | GenE(a, k, e) -> AllT(a, k, infer_exp (add_typ a k env) e)
   | InstE(e, t) ->
-    (match force_typ (infer_exp env e) with
+    (match norm_typ (infer_exp env e) with
     | AllT(a, k, t') -> check_typ env t k "InstE"; subst_typ [a, t] t'
     | _ -> raise (Error "InstE")
     )
   | PackE(t, e, t') ->
     check_typ env t' BaseK "PackE";
-    (match force_typ t' with
+    (match norm_typ t' with
     | AnyT(a, k, t'') ->
       check_typ env t k "PackE1";
       check_exp env e (subst_typ [a, t] t'') "PackE2";
@@ -387,7 +383,7 @@ let rec infer_exp env = function
     | _ -> raise (Error "PackE")
     )
   | OpenE(e1, a, x, e2) ->
-    (match force_typ (infer_exp env e1) with
+    (match norm_typ (infer_exp env e1) with
     | AnyT(a1, k, t1) ->
       let t =
         infer_exp (add_val x (subst_typ [a1, VarT(a)] t1) (add_typ a k env)) e2
diff --git a/fomega.mli b/fomega.mli
index 8b8d3689..090d823c 100644
--- a/fomega.mli
+++ b/fomega.mli
@@ -86,8 +86,6 @@ val norm_exp : exp -> exp (* raise Error *)
 
 val equal_typ : typ -> typ -> bool (* raise Error *)
 
-val force_typ : typ -> typ
-
 
 (* Checking *)
 
diff --git a/regression.1ml b/regression.1ml
new file mode 100644
index 00000000..a948545e
--- /dev/null
+++ b/regression.1ml
@@ -0,0 +1,23 @@
+Equivalence: {
+  type t a b;
+
+  transitivity 'a 'b 'c: t a b => t b c -> t a c;
+  reflexivity 'a: t a a;
+
+  symmetry 'a 'b: t a b -> t b a;
+
+  to   'a 'b: t a b => a -> b;
+  from 'a 'b: t a b => b -> a;
+} = {
+  type T a b = (type p _) -> p a -> p b;
+  type t a b = wrap T a b;
+  wr (eq: T _ _) = wrap eq: t _ _;
+  un eq = unwrap eq: t _ _;
+  transitivity 'a 'b 'c (ab: t a b) (bc: t b c) =
+    wr (fun (type p _) => un bc p << un ab p);
+  reflexivity = wr (fun (type p _) => id);
+  to eq a = un eq (fun (type x) => x) a;
+  from 'a 'b (eq: t a b) b = un eq (fun (type b) => type b -> a) id b;
+  symmetry 'a 'b (eq: t a b) : t b a =
+    wr (fun (type p _) => un eq (fun (type b) => type p b -> p a) id);
+};

From 7f60b4c25b625c7fff7301bcc186f148d945ae0f Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sat, 11 Apr 2020 21:04:01 +0300
Subject: [PATCH 07/17] Fix substitution of semantic types

When determining whether a type contains a variable any undetermined inferred
type may end up containing the variable.
---
 regression.1ml | 20 ++++++++++++++++++++
 types.ml       |  5 ++++-
 2 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/regression.1ml b/regression.1ml
index a948545e..072060a4 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -21,3 +21,23 @@ Equivalence: {
   symmetry 'a 'b (eq: t a b) : t b a =
     wr (fun (type p _) => un eq (fun (type b) => type p b -> p a) id);
 };
+
+;;
+
+AmateurOptics = {
+  type FUNCTOR = {
+    type t a;
+    map 'a 'b: (a -> b) => t a -> t b;
+  };
+
+  type lens a b s t = (F: FUNCTOR) => (a -> F.t b) => s -> F.t t;
+
+  ;; NOTE: It is important that the following do not have more type annotations,
+  ;; because the bug that this triggered was due to treatment of inferred types.
+
+  (<-<) (l1: lens _ _ _ _, l2: lens _ _ _ _) (F: FUNCTOR) toF = l1 F (l2 F toF);
+
+  e1 (F: FUNCTOR) abF (l, r) = F.map (fun l => (l, r)) (abF l);
+
+  e11 = e1 <-< e1;
+};
diff --git a/types.ml b/types.ml
index 9bf30af8..5063d305 100644
--- a/types.ml
+++ b/types.ml
@@ -180,7 +180,10 @@ let rec contains_typ a = function
   | TupT(r) -> contains_row a r
   | DotT(t, l) -> contains_typ a t
   | RecT(ak, t) -> not (contains_bind a [ak]) && contains_typ a t
-  | InferT(z) -> false
+  | InferT(z) ->
+    match !z with
+    | Det t -> contains_typ a t
+    | Undet _ -> true
 
 and contains_extyp a = function
   | ExT(aks, t) -> not (contains_bind a aks) && contains_typ a t

From e67a7d622207545b9968a58eb88abef19c9d66e2 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Wed, 19 Feb 2020 20:14:04 +0200
Subject: [PATCH 08/17] Fix structure/record inference

The original code simply used a wrong variable in place of the field name.
---
 elab.ml        | 2 +-
 regression.1ml | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/elab.ml b/elab.ml
index d98ae02b..d3c683fb 100644
--- a/elab.ml
+++ b/elab.ml
@@ -422,7 +422,7 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
       | InferT(z) ->
         (* TODO: row polymorphism *)
         let t, zs = guess_typ (Env.domain_typ (add_typs aks env)) BaseK in
-        let tr = [l, t] in
+        let tr = [var.it, t] in
         resolve_always z (StrT(tr)); tr, zs
       | _ -> error exp1.at "expression is not a structure"
     in
diff --git a/regression.1ml b/regression.1ml
index 072060a4..a9dc0ff7 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -1,3 +1,7 @@
+record_inference x = x.works_a_little;
+
+;;
+
 Equivalence: {
   type t a b;
 

From 9d6f3c66ab9326745906a101bc2d10ebd2950d15 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sat, 4 Jan 2020 15:03:56 +0200
Subject: [PATCH 09/17] Fix to drop unused bindings to avoid warnings

---
 elab.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/elab.ml b/elab.ml
index d3c683fb..54705a6b 100644
--- a/elab.ml
+++ b/elab.ml
@@ -186,8 +186,8 @@ let rec elab_typ env typ l =
     elab_dec env dec l
 
   | EL.FunT(var, typ1, typ2, eff, impl) ->
-    let ExT(aks1, t1) as s1, zs1 = elab_typ env typ1 var.it in
-    let ExT(aks2, t2) as s2, zs2 =
+    let ExT(aks1, t1), zs1 = elab_typ env typ1 var.it in
+    let ExT(aks2, t2), zs2 =
       elab_typ (add_val var.it t1 (add_typs aks1 env)) typ2 l in
     (match elab_eff env eff, elab_impl env impl with
     | Impure, Explicit _ ->

From 753a64c51d2d9674a80d8f46907418d8eacec56b Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sun, 12 Jan 2020 14:14:28 +0200
Subject: [PATCH 10/17] Fix to allow pure unwrap for non-existentials and
 impure for if-else

See rule EUNWRAP in fig 9 in section 5.1 of JFP (draft) paper
and rule EIF in fig 8 in section 4.2 of JFP (draft) paper.
---
 elab.ml        |  4 ++--
 regression.1ml | 15 +++++++++++++++
 types.ml       |  2 ++
 types.mli      |  1 +
 4 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/elab.ml b/elab.ml
index 54705a6b..2b0d2af3 100644
--- a/elab.ml
+++ b/elab.ml
@@ -410,7 +410,7 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
       ("branch type does not match annotation: " ^ Sub.string_of_error e) in
     let _, zs4, f2 = try sub_extyp env s2 s [] with Sub e -> error exp2.at
       ("branch type does not match annotation: " ^ Sub.string_of_error e) in
-    s, join_eff p1 p2,
+    s, join_eff (join_eff p1 p2) (extyp_eff s),
     lift_warn exp.at t (add_typs aks env) (zs0 @ zs @ zs1 @ zs2 @ zs3 @ zs4),
     IL.IfE(ex, IL.AppE(f1, e1), IL.AppE(f2, e2))
 
@@ -483,7 +483,7 @@ Trace.debug (lazy ("[UnwrapE] s1 = " ^ string_of_norm_extyp s1));
 Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
     let _, zs3, f = try sub_extyp env s1 s2 [] with Sub e -> error exp.at
       ("wrapped type does not match annotation: " ^ Sub.string_of_error e) in
-    s2, Impure, lift_warn exp.at t (add_typs aks env) (zs1 @ zs2 @ zs3),
+    s2, extyp_eff s2, lift_warn exp.at t (add_typs aks env) (zs1 @ zs2 @ zs3),
     IL.AppE(f, IL.DotE(ex, "wrap"))
 
   | EL.UnrollE(var, typ) ->
diff --git a/regression.1ml b/regression.1ml
index a9dc0ff7..80acc15c 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -45,3 +45,18 @@ AmateurOptics = {
 
   e11 = e1 <-< e1;
 };
+
+;; Impure : () => {type t} = fun () =>
+;;   if true then {type t = int} else {type t = bool} : {type t};
+
+ImpureIf : () -> {type t} = fun () =>
+  if true then {type t = int} else {type t = bool} : {type t};
+
+PureIf : () => ('a => a => a) = fun () =>
+  if true then id else id : 'a => a => a;
+
+Pure : () => {type t = bool; existentials: t} = fun () =>
+  {type t = bool; existentials = false} :> {type t = bool; existentials: t};
+
+;; Impure : () => {type t; existentials: t} = fun () =>
+;;   {type t = bool; existentials = true} :> {type t = bool; existentials: t};
diff --git a/types.ml b/types.ml
index 5063d305..e4708ee2 100644
--- a/types.ml
+++ b/types.ml
@@ -82,6 +82,8 @@ let join_eff p1 p2 =
   | Pure, Pure -> Pure
   | _, _ -> Impure
 
+let extyp_eff (ExT(aks, _)) = if aks = [] then Pure else Impure
+
 
 (* Rows *)
 
diff --git a/types.mli b/types.mli
index 9863a82a..66532b62 100644
--- a/types.mli
+++ b/types.mli
@@ -81,6 +81,7 @@ val rename_vars : (var -> var) -> (var * kind) list -> (var * kind) list
 (* Effects *)
 
 val join_eff : eff -> eff -> eff
+val extyp_eff : extyp -> eff
 
 
 (* Rows *)

From 4a5622a12bfc269a4bcc5ddef9b24ef0442bcecf Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Thu, 27 Feb 2020 07:52:34 +0200
Subject: [PATCH 11/17] Fix empty structs `{}` and tuples `()` to include a
 source region

---
 parser.mly | 6 +++---
 syntax.ml  | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/parser.mly b/parser.mly
index 0d368713..21af1a24 100644
--- a/parser.mly
+++ b/parser.mly
@@ -376,11 +376,11 @@ atpat :
   | head
     { if $1.it = "_" then holeP@@at() else varP($1)@@at() }
   | LBRACE decon RBRACE
-    { strP($2)@@at() }
+    { strP($2, at())@@at() }
   | LPAR RPAR
-    { strP([])@@at() }
+    { strP([], at())@@at() }
   | LPAR patlist RPAR
-    { match $2 with [p] -> p | ps -> tupP(ps)@@at() }
+    { match $2 with [p] -> p | ps -> tupP(ps, at())@@at() }
   | LPAR TYPE name typparamlist RPAR
     { annotP(varP($3.it@@ati 3)@@ati 3,
         funT($4, TypT@@ati 2, Pure@@ati 2)@@at())@@at() }
diff --git a/syntax.ml b/syntax.ml
index 88542732..409c6abe 100644
--- a/syntax.ml
+++ b/syntax.ml
@@ -281,10 +281,10 @@ let wrapP(p, t2) =
   | None -> Some t2
   | Some t1 -> Some (AsT(t2, WrapT(t1)@@t1.at)@@span[p.at; t2.at])
 
-let strP(xps) =
+let strP(xps, region) =
   match xps with
   | [] ->
-    EmptyB@@nowhere_region, Some (StrT(EmptyD@@nowhere_region)@@nowhere_region)
+    EmptyB@@region, Some (StrT(EmptyD@@region)@@region)
   | xp::_ ->
     let b, d =
       List.fold_right (fun xp (b, d) ->
@@ -296,7 +296,7 @@ let strP(xps) =
       ) xps (EmptyB@@xp.at, EmptyD@@xp.at)
     in b, Some (StrT(d)@@d.at)
 
-let rec tupP(ps) = strP(tupP' 1 ps)
+let rec tupP(ps, region) = strP(tupP' 1 ps, region)
 and tupP' n = function
   | [] -> []
   | p::ps -> (((index n)@@p.at, p)@@p.at) :: tupP' (n + 1) ps

From 2f88b83032d1aac31b738fffff4e83bfcda179d9 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Fri, 28 Feb 2020 07:50:33 +0200
Subject: [PATCH 12/17] Fix `annotP` such that it always equates the types

Previously `annotP` only equated the types in the case when there was a sequence
of bindings produced by the nested patterns.  This meant that inconsistent
patterns would type check.  For example, before this PR, the REPL interaction

    1ML> ({}: int) = 1;

    1ML> ((x: int): text) = "1";
    x : text

would not give errors.  After this PR, the same interaction

    1ML> ({}: int) = 1;
    stdin:1.2-1.9: inconsistent types equated by `as': () vs int
    1ML> ((x: int): text) = "1";
    stdin:1.6-1.16: inconsistent types equated by `as': int vs text

gives reasonable errors.
---
 syntax.ml | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/syntax.ml b/syntax.ml
index 409c6abe..c20df3ac 100644
--- a/syntax.ml
+++ b/syntax.ml
@@ -263,13 +263,15 @@ let asP(p1, p2) =
 
 let annotP(p, t2) =
   let b, to1 = p.it in
-  match b.it with
-  | EmptyB | VarB(_, {it = VarE({it = "$"})}) -> b, Some t2
-  | _ ->
-    let t =
-      match asTopt(to1, Some t2) with Some t -> t | None -> assert false in
-    patB(p, annotE(VarE("$"@@t2.at)@@t2.at, t)@@t2.at)@@span[p.at; t2.at],
-    Some t
+  let t = match asTopt(to1, Some t2) with Some t -> t | None -> assert false in
+  let toE e = annotE(e, t)@@t2.at in
+  let b' =
+    match b.it with
+    | EmptyB -> doB(toE(VarE("$"@@b.at)@@b.at))
+    | VarB(x, e) -> VarB(x, toE e)
+    | _ ->
+      letB(VarB("$"@@b.at, toE(VarE("$"@@b.at)@@b.at))@@b.at, b.it@@p.at) in
+  b'@@span[p.at; t2.at], Some t
 
 let wrapP(p, t2) =
   let _, to1 = p.it in

From 08b2885dc31ebfa33173841a757535e44e3891f7 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sat, 22 Feb 2020 14:52:51 +0200
Subject: [PATCH 13/17] Fix prim defs to use an internal GADT to avoid warnings

---
 prim.ml | 166 ++++++++++++++++++++++++++++----------------------------
 1 file changed, 84 insertions(+), 82 deletions(-)

diff --git a/prim.ml b/prim.ml
index f174d7b9..d11dce3b 100644
--- a/prim.ml
+++ b/prim.ml
@@ -54,90 +54,92 @@ let is_poly {typ = ts1, ts2} = List.mem VarT ts1 || List.mem VarT ts2
 
 let typs = [BoolT; IntT; CharT; TextT]
 
+type 'a def =
+  | VoidD: unit def
+  | BoolD: bool def
+  | IntD: int def
+  | CharD: char def
+  | TextD: string def
+  | VarD: const def
+  | ProdD: 'a def * 'b def -> ('a * 'b) def
+
+let (&) l r = ProdD (l, r)
+
+let rec typs_of: type a. a def -> typ list = function
+  | VoidD -> []
+  | BoolD -> [BoolT]
+  | IntD -> [IntT]
+  | CharD -> [CharT]
+  | TextD -> [TextT]
+  | VarD -> [VarT]
+  | ProdD (l, r) -> typs_of l @ typs_of r
+
+let rec inj: type a. a def -> a -> const list -> const list = function
+  | VoidD -> fun () vs -> vs
+  | BoolD -> fun v vs -> BoolV v :: vs
+  | IntD -> fun v vs -> IntV v :: vs
+  | CharD -> fun v vs -> CharV v :: vs
+  | TextD -> fun v vs -> TextV v :: vs
+  | VarD -> fun v vs -> v :: vs
+  | ProdD (lD, rD) ->
+    let injL = inj lD and injR = inj rD in fun (l, r) vs -> injL l (injR r vs)
+
+let rec prj: type a. a def -> const list -> a * const list = function
+  | VoidD -> fun vs -> ((), vs)
+  | BoolD -> (function (BoolV v :: vs) -> (v, vs) | _ -> failwith "bool")
+  | IntD -> (function (IntV v :: vs) -> (v, vs) | _ -> failwith "int")
+  | CharD -> (function (CharV v :: vs) -> (v, vs) | _ -> failwith "char")
+  | TextD -> (function (TextV v :: vs) -> (v, vs) | _ -> failwith "text")
+  | VarD -> (function (v :: vs) -> (v, vs) | _ -> failwith "var")
+  | ProdD (lD, rD) ->
+    let prjL = prj lD and prjR = prj rD in
+    fun vs -> let (l, vs) = prjL vs in let (r, vs) = prjR vs in ((l, r), vs)
+
+let def name inD outD fn = {
+    name = name;
+    typ = typs_of inD, typs_of outD;
+    fn = let inj = inj outD and prj = prj inD in
+         fun vs -> let (v, vs) = prj vs in assert (vs = []); inj (fn v) []
+  }
+
 let funs =
   [
-    {name = "==";
-      typ = [VarT; VarT], [BoolT];
-      fn = fun [x1; x2] -> [BoolV(x1 = x2)]};
-    {name = "<>";
-      typ = [VarT; VarT], [BoolT];
-      fn = fun [x1; x2] -> [BoolV(x1 <> x2)]};
-
-    {name = "true";
-      typ = [], [BoolT];
-      fn = fun [] -> [BoolV(true)]};
-    {name = "false";
-      typ = [], [BoolT];
-      fn = fun [] -> [BoolV(false)]};
-
-    {name = "Int.+";
-      typ = [IntT; IntT], [IntT];
-      fn = fun [IntV i1; IntV i2] -> [IntV(i1 + i2)]};
-    {name = "Int.-";
-      typ = [IntT; IntT], [IntT];
-      fn = fun [IntV i1; IntV i2] -> [IntV(i1 - i2)]};
-    {name = "Int.*";
-      typ = [IntT; IntT], [IntT];
-      fn = fun [IntV i1; IntV i2] -> [IntV(i1 * i2)]};
-    {name = "Int./";
-      typ = [IntT; IntT], [IntT];
-      fn = fun [IntV i1; IntV i2] -> [IntV(i1 / i2)]};
-    {name = "Int.%";
-      typ = [IntT; IntT], [IntT];
-      fn = fun [IntV i1; IntV i2] -> [IntV(i1 mod i2)]};
-    {name = "Int.<";
-      typ = [IntT; IntT], [BoolT];
-      fn = fun [x1; x2] -> [BoolV(x1 < x2)]};
-    {name = "Int.>";
-      typ = [IntT; IntT], [BoolT];
-      fn = fun [x1; x2] -> [BoolV(x1 > x2)]};
-    {name = "Int.<=";
-      typ = [IntT; IntT], [BoolT];
-      fn = fun [x1; x2] -> [BoolV(x1 <= x2)]};
-    {name = "Int.>=";
-      typ = [IntT; IntT], [BoolT];
-      fn = fun [x1; x2] -> [BoolV(x1 >= x2)]};
-    {name = "Int.print";
-      typ = [IntT], [];
-      fn = fun [IntV i] -> print_int i; flush_all (); []};
-
-    {name = "Char.toInt";
-      typ = [CharT], [IntT];
-      fn = fun [CharV c] -> [IntV(Char.code c)]};
-    {name = "Char.fromInt";
-      typ = [IntT], [CharT];
-      fn = fun [IntV i] -> [CharV(Char.chr i)]};
-    {name = "Char.print";
-      typ = [CharT], [];
-      fn = fun [CharV c] -> print_char c; flush_all (); []};
-
-    {name = "Text.++";
-      typ = [TextT; TextT], [TextT];
-      fn = fun [TextV t1; TextV t2] -> [TextV(t1 ^ t2)]};
-    {name = "Text.<";
-      typ = [TextT; TextT], [BoolT];
-      fn = fun [x1; x2] -> [BoolV(x1 < x2)]};
-    {name = "Text.>";
-      typ = [TextT; TextT], [BoolT];
-      fn = fun [x1; x2] -> [BoolV(x1 > x2)]};
-    {name = "Text.<=";
-      typ = [TextT; TextT], [BoolT];
-      fn = fun [x1; x2] -> [BoolV(x1 <= x2)]};
-    {name = "Text.>=";
-      typ = [TextT; TextT], [BoolT];
-      fn = fun [x1; x2] -> [BoolV(x1 >= x2)]};
-    {name = "Text.length";
-      typ = [TextT], [IntT];
-      fn = fun [TextV t] -> [IntV(String.length t)]};
-    {name = "Text.sub";
-      typ = [TextT; IntT], [CharT];
-      fn = fun [TextV t; IntV i] -> [CharV(t.[i])]};
-    {name = "Text.fromChar";
-      typ = [CharT], [TextT];
-      fn = fun [CharV c] -> [TextV(String.make 1 c)]};
-    {name = "Text.print";
-      typ = [TextT], [];
-      fn = fun [TextV t] -> print_string t; flush_all (); []};
+    def "==" (VarD & VarD) BoolD (fun (x1, x2) -> x1 = x2);
+    def "<>" (VarD & VarD) BoolD (fun (x1, x2) -> x1 <> x2);
+
+    def "true" VoidD BoolD (fun () -> true);
+    def "false" VoidD BoolD (fun () -> false);
+
+    def "Int.+" (IntD & IntD) IntD (fun (i1, i2) -> i1 + i2);
+    def "Int.-" (IntD & IntD) IntD (fun (i1, i2) -> i1 - i2);
+    def "Int.*" (IntD & IntD) IntD (fun (i1, i2) -> i1 * i2);
+    def "Int./" (IntD & IntD) IntD (fun (i1, i2) -> i1 / i2);
+    def "Int.%" (IntD & IntD) IntD (fun (i1, i2) -> i1 mod i2);
+
+    def "Int.<" (IntD & IntD) BoolD (fun (i1, i2) -> i1 < i2);
+    def "Int.>" (IntD & IntD) BoolD (fun (i1, i2) -> i1 > i2);
+    def "Int.<=" (IntD & IntD) BoolD (fun (i1, i2) -> i1 <= i2);
+    def "Int.>=" (IntD & IntD) BoolD (fun (i1, i2) -> i1 >= i2);
+
+    def "Int.print" IntD VoidD (fun i -> print_int i; flush_all ());
+
+    def "Char.toInt" CharD IntD Char.code;
+    def "Char.fromInt" IntD CharD Char.chr;
+
+    def "Char.print" CharD VoidD (fun c -> print_char c; flush_all ());
+
+    def "Text.++" (TextD & TextD) TextD (fun (t1, t2) -> t1 ^ t2);
+
+    def "Text.<" (TextD & TextD) BoolD (fun (i1, i2) -> i1 < i2);
+    def "Text.>" (TextD & TextD) BoolD (fun (i1, i2) -> i1 > i2);
+    def "Text.<=" (TextD & TextD) BoolD (fun (i1, i2) -> i1 <= i2);
+    def "Text.>=" (TextD & TextD) BoolD (fun (i1, i2) -> i1 >= i2);
+
+    def "Text.length" TextD IntD String.length;
+    def "Text.sub" (TextD & IntD) CharD (fun (t, i) -> t.[i]);
+    def "Text.fromChar" CharD TextD (String.make 1);
+
+    def "Text.print" TextD VoidD (fun t -> print_string t; flush_all ());
   ]
 
 let fun_of_string name =

From 51ef71f9a41accbbff82dc03662eeb95f7261c92 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sun, 23 Feb 2020 19:07:12 +0200
Subject: [PATCH 14/17] Fix to not allow anonymous declarations

---
 parser.mly | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/parser.mly b/parser.mly
index 21af1a24..3727ab07 100644
--- a/parser.mly
+++ b/parser.mly
@@ -175,14 +175,14 @@ typlist :
 ;
 
 atdec :
-  | head typparamlist COLON typ
+  | name typparamlist COLON typ
     { VarD($1, funT($2, $4, Pure@@ati 2)@@span[ati 2; ati 4])@@at() }
-  | TYPE head typparamlist
+  | TYPE name typparamlist
     { VarD($2, funT($3, TypT@@ati 1, Pure@@ati 3)@@at())@@at() }
-  | head typparamlist EQUAL exp
+  | name typparamlist EQUAL exp
     { VarD($1, funT($2, EqT($4)@@ati 4, Pure@@ati 3)@@span[ati 2; ati 4])
         @@at() }
-  | TYPE head typparamlist EQUAL typ
+  | TYPE name typparamlist EQUAL typ
     { VarD($2, funT($3, EqT(TypE($5)@@ati 5)@@ati 5, Pure@@ati 4)@@at())
         @@at() }
   | INCLUDE typ

From 36519a7da37b5795a72fbfc8ea073f27484e8f11 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sun, 28 Jun 2020 13:52:51 +0300
Subject: [PATCH 15/17] Fix to not use polymorphic equality in examples

Especially in the case of Set and Map abstractions that are supposed to use
given ordering.
---
 prelude.1ml | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/prelude.1ml b/prelude.1ml
index 07003054..5abff9a1 100644
--- a/prelude.1ml
+++ b/prelude.1ml
@@ -29,9 +29,15 @@ true = Bool.true;
 false = Bool.false;
 not = Bool.not;
 
-(==) 'a (x : a, y : a) = primitive "==" a (x, y);
-(<>) 'a (x : a, y : a) = not (x == y);
+PolyEq (type t) = {
+  (==) (x : t, y : t) = primitive "==" t (x, y);
+  (<>) (x : t, y : t) = not (x == y);
+};
 
+Bool = {
+  include Bool;
+  include PolyEq t;
+};
 
 ;; Int
 
@@ -49,6 +55,7 @@ Int =
   (<=) = primitive "Int.<=";
   (>=) = primitive "Int.>=";
   print = primitive "Int.print";
+  include PolyEq t;
 };
 type int = Int.t;
 (+) = Int.+;
@@ -60,6 +67,8 @@ type int = Int.t;
 (>) = Int.>;
 (<=) = Int.<=;
 (>=) = Int.>=;
+(==) = Int.==;
+(<>) = Int.<>;
 
 
 ;; Char
@@ -71,6 +80,7 @@ Char =
   toInt = primitive "Char.toInt";
   fromInt = primitive "Char.fromInt";
   print = primitive "Char.print";
+  include PolyEq t;
 };
 type char = Char.t;
 
@@ -90,6 +100,7 @@ Text =
   sub t i = primitive "Text.sub" (t, i);
   fromChar c = primitive "Text.fromChar" c;
   print = primitive "Text.print";
+  include PolyEq t;
 };
 type text = Text.t;
 (++) = Text.++;
@@ -215,6 +226,7 @@ type SET =
 Set (Elem : ORD) :> SET with (elem = Elem.t) =
 {
   type elem = Elem.t;
+  (==) (x, y) = let include Elem in (x <= y) and (y <= x);
   type set = (int, elem -> bool);
   type t = set;
   empty = (0, fun (x : elem) => false);
@@ -241,6 +253,7 @@ type MAP =
 Map (Key : ORD) :> MAP with (key = Key.t) =
 {
   type key = Key.t;
+  (==) (x, y) = let include Key in (x <= y) and (y <= x);
   type map a = key -> opt a;
   t = map;
   empty x = none;

From 5462198297cfb80569b77e48321bf601fb3fb86c Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sun, 28 Jun 2020 14:10:20 +0300
Subject: [PATCH 16/17] Fix first-class implicit example

---
 README.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.txt b/README.txt
index b761a748..248b7186 100644
--- a/README.txt
+++ b/README.txt
@@ -267,7 +267,7 @@ or even more explicitly,
 
 Generalisation can also take place as part of subtyping (a.k.a. signature matching), e.g. in the following example:
 
-  f (id : ‘a => id -> id) = (id 5, id “”)
+  f (id : ‘a => a -> a) = (id 5, id “”)
   p = f (fun x => x)
 
 This also shows that implicit functions naturally are first-class values.

From e9bd7e762719c40b75c756d4e08343d6ff30de8c Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sun, 28 Jun 2020 13:23:50 +0300
Subject: [PATCH 17/17] Fix to freshen unwrap target type

---
 elab.ml        | 4 +++-
 regression.1ml | 6 ++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/elab.ml b/elab.ml
index 2b0d2af3..1798839f 100644
--- a/elab.ml
+++ b/elab.ml
@@ -469,7 +469,9 @@ Trace.debug (lazy ("[AppE] ts = " ^ String.concat ", " (List.map string_of_norm_
   | EL.UnwrapE(var, typ) ->
     let aks, t, s2, zs2 =
       match elab_typ env typ l with
-      | ExT([], WrapT(ExT(aks, t) as s2)), zs2 -> aks, t, s2, zs2
+      | ExT([], WrapT(s2)), zs2 ->
+        let ExT(aks, t) as s2 = freshen_extyp env s2 in
+        aks, t, s2, zs2
       | _ -> error typ.at "non-wrapped type for unwrap" in
     let t1, zs1, ex = elab_instvar env var in
     let s1 =
diff --git a/regression.1ml b/regression.1ml
index 80acc15c..c63e1647 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -28,6 +28,12 @@ Equivalence: {
 
 ;;
 
+type B = wrap type => type;
+
+both f g (x: type) = (unwrap f: B) ((unwrap g: B) x);
+
+;;
+
 AmateurOptics = {
   type FUNCTOR = {
     type t a;