Various fixes

.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

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.

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

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 _ ->
@@ -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))
 
@@ -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
@@ -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 =
@@ -483,7 +485,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) ->

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,41 +357,41 @@ 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";
       t'
     | _ -> 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
       in check_typ env t BaseK "OpenE2"; t
     | _ -> 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";

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 *)