Change to attempt to infer wrapped and folded types

elab.ml

@@ -417,13 +417,18 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
     IL.genE(erase_bind aks, IL.LamE(var.it, erase_typ t, e2))
 
   | EL.WrapE(var, typ) ->
+    let var_t = lookup_var env var in
     let s, zs1 =
       match elab_typ env typ "" with
       | ExT([], WrapT(s)), zs1 -> s, zs1
+      | ExT([], InferT(z)), zs1 ->
+        let s = ExT([], var_t) in
+        resolve_always z (WrapT(s));
+        s, zs1
       | _ -> error typ.at "non-wrapped type for wrap"
     in
     let _, zs2, f =
-      try sub_extyp env (ExT([], lookup_var env var)) s []
+      try sub_extyp env (ExT([], var_t)) s []
       with Sub e -> error exp.at
         ("wrapped type does not match annotation: " ^ Sub.string_of_error e)
     in
@@ -517,13 +522,20 @@ Trace.debug (lazy ("[AppE] ts = " ^ String.concat ", " (List.map string_of_norm_
     IL.AppE(IL.instE(ex1, List.map erase_typ ts), IL.AppE(f, IL.VarE(var2.it)))
 
   | EL.UnwrapE(var, typ) ->
+    let t1, zs1, ex = fully try_unroll avar (elab_instvar env var) in
     let aks, t, s2, zs2 =
       match elab_typ env typ l with
       | ExT([], WrapT(s2)), zs2 ->
         let ExT(aks, t) as s2 = freshen_extyp env s2 in
         aks, t, s2, zs2
+      | ExT([], InferT(z)), zs2 ->
+        (match t1 with
+         | WrapT(s2) ->
+           resolve_always z t1;
+           [], t1, s2, zs2
+         | _ ->
+           error typ.at "could not infer type for unwrap")
       | _ -> error typ.at "non-wrapped type for unwrap" in
-    let t1, zs1, ex = fully try_unroll avar (elab_instvar env var) in
     let s1 =
       match t1 with
       | WrapT(s1) -> s1
@@ -539,9 +551,16 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
     IL.AppE(f, IL.DotE(ex, "wrap"))
 
   | EL.UnrollE(var, typ) ->
-    let s, zs1 = elab_typ env typ l in
-    let unroll_t, roll_t = rec_from_extyp typ "unrolling" s in
     let var_t = lookup_var env var in
+    let s, zs1 =
+      match elab_typ env typ l with
+      | ExT([], InferT(z)), zs1 ->
+        let s = ExT([], var_t) in
+        resolve_always z var_t;
+        s, zs1
+      | s, zs1 ->
+        s, zs1 in
+    let unroll_t, roll_t = rec_from_extyp typ "unrolling" s in
     let _, zs2, f = try sub_typ env var_t roll_t [] with Sub e ->
       error var.at ("unrolled value does not match annotation:"
                     ^ "  " ^ Types.string_of_typ var_t ^ " "

paper.1ml

@@ -266,7 +266,7 @@ type OPT = {
 }
 Opt :> OPT = {
   type opt a = wrap (b : type) -> b -> (a ~> b) ~> b
-  none 'a :# opt a = fun (b : type) (n : b) (s : a ~> b) => n
-  some 'a x :# opt a = fun (b : type) (n : b) (s : a ~> b) => s x
+  none 'a :# _ = fun (b : type) (n : b) (s : a ~> b) => n
+  some 'a x :# _ = fun (b : type) (n : b) (s : a ~> b) => s x
   caseopt 'a 'b (xo :# opt a) = xo b
 }

prelude.1ml

@@ -112,8 +112,8 @@ type OPT = {
 }
 Opt :> OPT = {
   type opt a = wrap (b : type) -> (() ~> b) -> (a ~> b) ~> b
-  none 'a :# opt a = fun (b : type) (n : () ~> b) (s : a ~> b) => n ()
-  some 'a x :# opt a = fun (b : type) (n : () ~> b) (s : a ~> b) => s x
+  none 'a :# _ = fun (b : type) (n : () ~> b) (s : a ~> b) => n ()
+  some 'a x :# _ = fun (b : type) (n : () ~> b) (s : a ~> b) => s x
   caseopt (xo :# opt _) = xo _
 }
 ...Opt
@@ -129,9 +129,9 @@ type ALT = {
 }
 Alt :> ALT = {
   type alt a b = wrap (c : type) -> (a ~> c) -> (b ~> c) ~> c
-  left 'a 'b x :# alt a b =
+  left 'a 'b x :# _ =
     fun (c : type) (l : a ~> c) (r : b ~> c) => l x
-  right 'a 'b x :# alt a b =
+  right 'a 'b x :# _ =
     fun (c : type) (l : a ~> c) (r : b ~> c) => r x
   casealt (xy :# alt _ _) = xy _
 }
@@ -163,8 +163,8 @@ type LIST = {
 List :> LIST = {
   ...{
     type list a = wrap (b : type) -> b -> (a ~> b ~> b) ~> b
-    nil 'a :# list _ = fun (b : type) (n : b) (c : a ~> b ~> b) => n
-    cons x (xs :# list _) :# list _ =
+    nil 'a :# _ = fun (b : type) (n : b) (c : a ~> b ~> b) => n
+    cons x (xs :# list _) :# _ =
       fun (b : type) (n : b) (c : _ ~> b ~> b) =>
         c x (xs b n c)
     foldr (xs :# list _) = xs _

regression.1ml

@@ -184,6 +184,12 @@ Both = {
   ({x, y = _} as {x = _, y}) = {x = 1, y = 2}
 }
 
+type_error {
+  cannot_infer_unwrap t = t #: _
+}
+
+type_error {cannot_infer_unroll t = t @: _}
+
 ;;
 
 type_error { type_error 101 }

test.1ml

@@ -83,8 +83,8 @@ type OPT = {
 }
 Opt :> OPT = {
   type opt a = wrap (b : type) -> b -> (a ~> b) ~> b
-  none :# opt _ = fun (b : type) (n : b) (s : _ ~> b) => n
-  some x :# opt _ = fun (b : type) (n : b) (s : _ ~> b) => s x
+  none :# _ = fun (b : type) (n : b) (s : _ ~> b) => n
+  some x :# _ = fun (b : type) (n : b) (s : _ ~> b) => s x
   caseopt (xo :# opt _) = xo _
 }
 ...Opt
@@ -99,8 +99,8 @@ type ALT = {
 }
 Alt :> ALT = {
   type alt a b = wrap (c : type) -> (a ~> c) -> (b ~> c) ~> c
-  left x :# alt _ _ = fun (c : type) (l : _ ~> c) (r : _ ~> c) => l x
-  right x :# alt _ _ = fun (c : type) (l : _ ~> c) (r : _ ~> c) => r x
+  left x :# _ = fun (c : type) (l : _ ~> c) (r : _ ~> c) => l x
+  right x :# _ = fun (c : type) (l : _ ~> c) (r : _ ~> c) => r x
   casealt (xy :# alt _ _) = xy _
 }
 ...Alt
@@ -130,8 +130,8 @@ type LIST = {
 List :> LIST = {
   ...{
     type list a = wrap (b : type) -> b -> (a ~> b ~> b) ~> b
-    nil :# list _ = fun (b : type) (n : b) (c : _ ~> b ~> b) => n
-    cons x (xs :# list _) :# list _ =
+    nil :# _ = fun (b : type) (n : b) (c : _ ~> b ~> b) => n
+    cons x (xs :# list _) :# _ =
       fun (b : type) (n : b) (c : _ ~> b ~> b) =>
         c x (xs b n c)
     foldr (xs :# list _) = xs _
@@ -277,10 +277,10 @@ in {
 type int = primitive "int"
 type t = rec a => int
 v = 3 :@ t
-n = v @: t
+n = v @: _
 (m :@ t) = v
 type u a = rec _ => a
 w = 4 :@ u int
 (x :@ u int) = w
-((x :@ t, y) :@ u (_, _)) = (6 :@ t, 7) :@ u (_, _)
+((x :@ t, y) :@ u _) = (6 :@ t, 7) :@ u _
 ((x' :@ t, y') :@ u _) = (6 :@ t, 7) :@ u _