Fix to allow pure unwrap for non-existentials

See EUNWRAP rule in fig 9 in section 5.1 of JFP (draft) paper:

    Γ⊢X :P [Ξ′]􏰁e Γ⊢T 􏰁[Ξ] Γ⊢Ξ′ ≤Ξ􏰁 f
    ------------------------------------- EUNWRAP
     Γ ⊢ unwrap X:T :η(Ξ) Ξ 􏰁 f (e.val)

elab.ml

@@ -493,7 +493,7 @@ Trace.debug (lazy ("[AppE] ts = " ^ String.concat ", " (List.map string_of_norm_
       | ExT([], WrapT(ExT(aks, t) as s2)), zs2 -> aks, t, s2, zs2
       | _ -> error typ.at "non-wrapped type for unwrap" in
     let t1, zs1, ex = elab_instvar env var in
-    let s1 =
+    let ExT(aks1, _) as s1 =
       match t1 with
       | WrapT(s1) -> s1
       | InferT(z) ->
@@ -502,9 +502,10 @@ Trace.debug (lazy ("[AppE] ts = " ^ String.concat ", " (List.map string_of_norm_
       | _ -> error var.at "expression is not a wrapped value" in
 Trace.debug (lazy ("[UnwrapE] s1 = " ^ string_of_norm_extyp s1));
 Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
+    let p = if aks1 = [] then Pure else Impure in
     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, p, lift_warn exp.at t (add_typs aks env) (zs1 @ zs2 @ zs3),
     IL.AppE(f, IL.DotE(ex, "wrap"))
 
   | EL.UnrollE(var, typ) ->

regression.1ml

@@ -22,6 +22,16 @@ Equivalence: {
     wr (fun (type p _) => un eq (fun (type b) => type p b -> p a) id);
 };
 
+;;
+
+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};
+
+;;
+
 Hungry = {
   type eat a = rec eat_a => a -> eat_a;