diff --git a/README.md b/README.md
index a825fe90..832cff44 100644
--- a/README.md
+++ b/README.md
@@ -341,14 +341,14 @@ This also shows that implicit functions naturally are first-class values.
 #### Recursive Types
 
 There are no datatype definitions, recursive types have to be defined
-explicitly, and require explicit injection/projection.
+explicitly, and sometimes require explicit annotations.
 
 ```1ml
 type stream = rec t => {hd : int, tl : () ~> opt t} ;; creates rec type
-single x :@ stream = {hd = x, tl = fun () => none}  ;; b :@ t rolls value into t
-({hd = n} :@ stream) = single 5        ;; p :@ t pattern matches on rec value
+single x : stream = {hd = x, tl = fun () => none}  ;; b : t rolls value into t
+{hd = n} = single 5                    ;; pattern match rec value
 do Int.print n                         ;; or:
-do Int.print (single 7 @: stream).hd   ;; e @: t unrolls rec value directly
+do Int.print (single 7).hd             ;; access rec value
 ```
 
 #### Recursive Functions
@@ -359,16 +359,16 @@ The `rec` expression form allows defining recursive functions:
 count = rec self => fun i =>
   if i <> 0 then self (i - 1)
 
-repeat = rec self => fun x =>
-  {hd = x, tl = fun () => some (self x)} :@ stream
+repeat = rec self => fun x : stream =>
+  {hd = x, tl = fun () => some (self x)}
 ```
 
 Mutual recursion is also expressible:
 
 ```1ml
 {even, odd} = rec (self : {even : int ~> stream, odd : int ~> stream}) => {
-  even x :@ stream = {hd = x, tl = fun () => some (self.odd (x + 1))}
-  odd x :@ stream = {hd = x, tl = fun () => some (self.even (x + 1))}
+  even x : stream = {hd = x, tl = fun () => some (self.odd (x + 1))}
+  odd x : stream = {hd = x, tl = fun () => some (self.even (x + 1))}
 }
 ```
 
@@ -392,13 +392,15 @@ Opt :> OPT = {
   ;; Church encoding; it requires the abstract type opt a to be implemented
   ;; with a polymorphic (i.e., large) type. Thus, wrap the type.
   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
-  caseopt (xo :# opt _) = xo _
+  none (b : type) (n : b) (s : _ ~> b) = n
+  some x (b : type) (n : b) (s : _ ~> b) = s x
+  caseopt (xo : opt _) = xo _
 }
 ```
 
-Note how values of type `wrap T` have to be wrapped and unwrapped explicitly.
+Values of type `T` can be implicitly wrapped to `wrap T` and, in case `wrap T`
+contains no abstract types, can be implicitly unwrapped to `T`. In case `wrap T`
+contains abstract types, unwrapping must be done explicitly.
 
 ---
 
diff --git a/elab.ml b/elab.ml
index 37dce93a..474d39e9 100644
--- a/elab.ml
+++ b/elab.ml
@@ -123,24 +123,40 @@ and paths_row ta ps = function
 
 
 let rec_from_extyp typ label s =
-  match s with
-  | ExT([], t) ->
-    let rec find_rec = function
-      | AppT(t, ts) ->
-        let rec_t, unroll_t, roll_t, ak = find_rec t in
-        rec_t, AppT(unroll_t, ts), AppT(roll_t, ts), ak
-      | RecT(ak, unroll_t) as rec_t ->
-        rec_t, unroll_t, rec_t, ak
-      | DotT(t, lab) ->
-        let rec_t, unroll_t, roll_t, ak = find_rec t in
-        rec_t, DotT(unroll_t, lab), DotT(roll_t, lab), ak
-      | _ ->
-        error typ.at ("non-recursive type for " ^ label ^ ":"
-                      ^ " " ^ Types.string_of_extyp s) in
-    find_rec t
-  | _ ->
+  match try_rec_from_extyp s with
+  | Some r -> r
+  | None ->
     error typ.at ("non-recursive type for " ^ label ^ ":"
-                  ^ " " ^ Types.string_of_extyp s)
+                  ^ " " ^ string_of_extyp s)
+
+
+let try_unwrap (t, zs, e) =
+  match t with
+  | WrapT(ExT([], t)) -> Some (t, zs, IL.DotE(e, "wrap"))
+  | _ -> None
+
+let try_unroll (t, zs, e) =
+  try_rec_from_typ t
+   |> Lib.Option.map (fun (unroll_t, roll_t) ->
+      unroll_t, zs, IL.UnrollE(e))
+
+let try_peel r =
+  try_unwrap r |> Lib.Option.orelse (fun () -> try_unroll r)
+
+let avar fn r = fn r
+
+let anexp fn r =
+  match r with
+  | ExT([], t), p, zs, e ->
+    fn (t, zs, e)
+     |> Lib.Option.map (fun (t, zs, e) ->
+        ExT([], t), p, zs, e)
+  | _ -> None
+
+let rec fully fn pre r =
+  match pre fn r with
+  | None -> r
+  | Some r -> fully fn pre r
 
 
 (* Instantiation *)
@@ -418,9 +434,8 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
 
   | EL.RollE(var, typ) ->
     let s, zs1 = elab_typ env typ l in
-    let rec_t, unroll_t, roll_t, ak = rec_from_extyp typ "rolling" s in
+    let unroll_t, roll_t = rec_from_extyp typ "rolling" s in
     let var_t = lookup_var env var in
-    let unroll_t = subst_typ (subst [ak] [rec_t]) unroll_t in
     let _, zs2, f =
       try sub_typ env var_t unroll_t []
       with Sub e ->
@@ -432,7 +447,7 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
     IL.RollE(IL.AppE(f, IL.VarE(var.it)), erase_typ roll_t)
 
   | EL.IfE(var, exp1, exp2) ->
-    let t0, zs0, ex = elab_instvar env var in
+    let t0, zs0, ex = fully try_peel avar (elab_instvar env var) in
     let _ =
       match t0 with
       | PrimT(Prim.BoolT) -> ()
@@ -451,7 +466,8 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
     IL.IfE(ex, IL.AppE(f1, e1), IL.AppE(f2, e2))
 
   | EL.DotE(exp1, var) ->
-    let ExT(aks, t), p, zs1, e1 = elab_instexp env exp1 "" in
+    let ExT(aks, t), p, zs1, e1 =
+      fully try_peel anexp (elab_instexp env exp1 "") in
     let tr, zs2 =
       match t with
       | StrT(tr) -> tr, []
@@ -476,7 +492,7 @@ Trace.debug (lazy ("[DotE] s = " ^ string_of_extyp s));
         IL.DotE(IL.VarE("x"), var.it), erase_extyp s))
 
   | EL.AppE(var1, var2) ->
-    let tf, zs1, ex1 = elab_instvar env var1 in
+    let tf, zs1, ex1 = fully try_peel avar (elab_instvar env var1) in
 Trace.debug (lazy ("[AppE] tf = " ^ string_of_norm_typ tf));
     let aks1, t1, s, p, zs =
       match freshen_typ env tf with
@@ -509,7 +525,7 @@ Trace.debug (lazy ("[AppE] ts = " ^ String.concat ", " (List.map string_of_norm_
         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 t1, zs1, ex = fully try_unroll avar (elab_instvar env var) in
     let s1 =
       match t1 with
       | WrapT(s1) -> s1
@@ -526,14 +542,13 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
 
   | EL.UnrollE(var, typ) ->
     let s, zs1 = elab_typ env typ l in
-    let rec_t, unroll_t, roll_t, ak = rec_from_extyp typ "unrolling" s in
+    let unroll_t, roll_t = rec_from_extyp typ "unrolling" s in
     let var_t = lookup_var env var 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 ^ " "
                     ^ "<"
                     ^ "  " ^ Types.string_of_typ roll_t) in
-    let unroll_t = subst_typ (subst [ak] [rec_t]) unroll_t in
     ExT([], unroll_t), Pure, zs1 @ zs2,
     IL.UnrollE(IL.AppE(f, IL.VarE(var.it)))
 
@@ -631,7 +646,8 @@ and elab_bind env bind l =
         erase_extyp s))
 
   | EL.InclB(exp) ->
-    let ExT(aks, t) as s, p, zs, e = elab_instexp env exp l in
+    let ExT(aks, t) as s, p, zs, e =
+      fully try_peel anexp (elab_instexp env exp l) in
     (match t with
     | StrT(tr) -> ()
     | InferT(z) -> resolve_always z (StrT[])  (* TODO: row polymorphism *)
diff --git a/examples/fc.1ml b/examples/fc.1ml
index 0c1f759b..a1bb894e 100644
--- a/examples/fc.1ml
+++ b/examples/fc.1ml
@@ -17,16 +17,13 @@ GADTs = {
         Succ       :      t int ~> case int
         Pair 'a 'b : t a ~> t b ~> case (a, b)
       }
-      type T (type t _) a = (m: I t) ~> m.case a
-      ...rec {type t _} => {type t a = wrap T t a}
-      T = T t
+      ...rec {type t _} => {type t a = wrap (m: I t) ~> m.case a}
       I = I t
-      mk (fn: T _) = fn :# wrap T _ :@ t _
     t
-    case (m: I) (e :# wrap T _ :@ t _) = e m
-    Zero     : t _ = mk fun (m: I) => m.Zero
-    Succ x   : t _ = mk fun (m: I) => m.Succ x
-    Pair l r : t _ = mk fun (m: I) => m.Pair l r
+    case (m: I) (e: t _) = e m
+    Zero     : t _ = fun (m: I) => m.Zero
+    Succ x   : t _ = fun (m: I) => m.Succ x
+    Pair l r : t _ = fun (m: I) => m.Pair l r
   }
 
   eval = rec (eval 'a: Exp.t a ~> a) =>
diff --git a/examples/hoas.1ml b/examples/hoas.1ml
index 6a7bb763..a958a343 100644
--- a/examples/hoas.1ml
+++ b/examples/hoas.1ml
@@ -18,9 +18,8 @@ let
   type T (type t _) x = (c: J t) ~> c.case x
   ...{
     ...rec {type t _} => {type t x = wrap T t x}
-    case 'x (type case _) (cs: I case t) (e :# wrap T t x :@ t _) =
-      e {case, ...cs}
-    mk 'x (fn: T t x) = fn :# wrap T t x :@ t _
+    case 'x (type case _) (cs: I case t) (e: t _) = e {case, ...cs}
+    mk (fn: T t _) = fn
   } :> {
     type t _
     case 'x: (type case _) -> I case t -> t x ~> case x
diff --git a/examples/trie.1ml b/examples/trie.1ml
index acae5c2e..c1173329 100644
--- a/examples/trie.1ml
+++ b/examples/trie.1ml
@@ -8,17 +8,14 @@ FunctionalTrie = {
       alt  'v 'k1 'k2 : t k1 v ~> t k2 v ~> case (alt k1 k2) v
       pair 'v 'k1 'k2 : t k1 (t k2 v)    ~> case (k1, k2) v
     }
-    type T (type t _ _) k v = (m: I t) ~> m.case k v
-    ...rec {type t _ _} => {type t k v = wrap T t k v}
-    T = T t
+    ...rec {type t _ _} => {type t k v = wrap (m: I t) ~> m.case k v}
     I = I t
-    mk (fn: T _ _) = fn :# wrap T _ _ :@ t _ _
 
   t
-  case (m: I) (e :# wrap T _ _ :@ t _ _) = e m
-  unit vO : t _ _ = mk fun (m: I) => m.unit vO
-  alt l r : t _ _ = mk fun (m: I) => m.alt l r
-  pair lr : t _ _ = mk fun (m: I) => m.pair lr
+  case (m: I) (e: t _ _) = e m
+  unit vO : t _ _ = fun (m: I) => m.unit vO
+  alt l r : t _ _ = fun (m: I) => m.alt l r
+  pair lr : t _ _ = fun (m: I) => m.pair lr
 
   lookup = rec (lookup 'k 'v: t k v ~> k ~> opt v) =>
     case {
diff --git a/import.ml b/import.ml
index 59dea177..17b2a20a 100644
--- a/import.ml
+++ b/import.ml
@@ -9,11 +9,6 @@ let sig_ext = ".1mls"
 let index_file = "index"
 let modules_dir = "node_modules"
 
-let (<|>) xO uxO =
-  match xO with
-  | None -> uxO ()
-  | some -> some
-
 let finish path =
   if Lib.Sys.file_exists_at path
      || Lib.Sys.file_exists_at (Lib.Filename.replace_ext mod_ext sig_ext path)
@@ -29,12 +24,13 @@ let complete path =
     finish (path ^ mod_ext)
 
 let rec search_modules prefix suffix =
-  complete (Filename.concat prefix modules_dir ^ "/" ^ suffix) <|> fun () ->
-  let parent = Filename.dirname prefix in
-  if parent = prefix then
-    None
-  else
-    search_modules parent suffix
+  complete (Filename.concat prefix modules_dir ^ "/" ^ suffix)
+   |> Lib.Option.orelse (fun () ->
+      let parent = Filename.dirname prefix in
+      if parent = prefix then
+        None
+      else
+        search_modules parent suffix)
 
 let resolve parent path =
   let path = Lib.Filename.canonic path in
@@ -50,5 +46,6 @@ let resolve parent path =
           || Lib.Sys.directory_exists_at parent then
     complete (Lib.Filename.canonic (Filename.dirname parent ^ "/" ^ path))
   else
-    search_modules (Filename.dirname parent) path <|> fun () ->
-    complete (std_dir ^ "/" ^ path)
+    search_modules (Filename.dirname parent) path
+     |> Lib.Option.orelse (fun () ->
+        complete (std_dir ^ "/" ^ path))
diff --git a/lib.ml b/lib.ml
index f242e9eb..8abadd26 100644
--- a/lib.ml
+++ b/lib.ml
@@ -113,4 +113,8 @@ struct
       | [] -> Some ys
       | x::xs -> bind (xyO x) @@ fun y -> loop (y::ys) xs in
     loop [] xs |> map List.rev
+
+  let orelse alt = function
+    | None -> alt ()
+    | some -> some
 end
diff --git a/lib.mli b/lib.mli
index b5057822..4a74a7f6 100644
--- a/lib.mli
+++ b/lib.mli
@@ -43,4 +43,5 @@ sig
   val map: ('a -> 'b) -> 'a option -> 'b option
   val bind: 'a option -> ('a -> 'b option) -> 'b option
   val traverse: ('a -> 'b option) -> 'a list -> 'b list option
+  val orelse: (unit -> 'a option) -> 'a option -> 'a option
 end
diff --git a/prelude/index.1ml b/prelude/index.1ml
index 92d1e067..2804afa7 100644
--- a/prelude/index.1ml
+++ b/prelude/index.1ml
@@ -26,10 +26,10 @@ Alt :> {
   inr 'a 'b: b -> t a b
   case 'a 'b 'o: {inl: a ~> o, inr: b ~> o} -> t a b ~> o
 } = {
-  type t a b = wrap 'o -> {inl: a ~> o, inr: b ~> o} ~> o
-  inl x :# t _ _ = fun c => c.inl x
-  inr x :# t _ _ = fun c => c.inr x
-  case c (x :# t _ _) = x c
+  type t a b = wrap (type o) -> {inl: a ~> o, inr: b ~> o} ~> o
+  inl x (type o) c : o = c.inl x
+  inr x (type o) c : o = c.inr x
+  case c (x : t _ _) = x _ c
 }
 
 Alt = {
@@ -55,11 +55,10 @@ Pair = {
 }
 
 List = {
-  local ...Opt, ...Fun
   ...rec {type t _} => {type t x = Opt.t (x, t x)}
-  nil :@ t _ = none
-  hd :: tl :@ t _ = some (hd, tl)
-  case {nil, (::)} (x :@ t _) = x |> Opt.case {
+  nil = Opt.none
+  hd :: tl = Opt.some (hd, tl)
+  case {nil, (::)} = Opt.case {
     none = nil
     some (hd, tl) = hd :: tl
   }
diff --git a/readme.1ml b/readme.1ml
index 314cecf2..c1b0b30b 100644
--- a/readme.1ml
+++ b/readme.1ml
@@ -47,10 +47,10 @@ p = f (fun x => x)
 
 
 type stream = rec t => {hd : int, tl : () ~> opt t} ;; creates rec type
-single x :@ stream = {hd = x, tl = fun () => none}  ;; b :@ t rolls value into t
-({hd = n} :@ stream) = single 5        ;; p :@ t pattern matches on rec value
+single x : stream = {hd = x, tl = fun () => none}  ;; b : t rolls value into t
+{hd = n} = single 5                    ;; pattern match rec value
 do Int.print n                         ;; or:
-do Int.print (single 7 @: stream).hd   ;; e @: t unrolls rec value directly
+do Int.print (single 7).hd             ;; access rec value
 
 
 
@@ -58,14 +58,14 @@ do Int.print (single 7 @: stream).hd   ;; e @: t unrolls rec value directly
 count = rec self => fun i =>
   if i <> 0 then self (i - 1)
 
-repeat = rec self => fun x =>
-  {hd = x, tl = fun () => some (self x)} :@ stream
+repeat = rec self => fun x : stream =>
+  {hd = x, tl = fun () => some (self x)}
 
 
 
 {even, odd} = rec (self : {even : int ~> stream, odd : int ~> stream}) => {
-  even x :@ stream = {hd = x, tl = fun () => some (self.odd (x + 1))}
-  odd x :@ stream = {hd = x, tl = fun () => some (self.even (x + 1))}
+  even x : stream = {hd = x, tl = fun () => some (self.odd (x + 1))}
+  odd x : stream = {hd = x, tl = fun () => some (self.even (x + 1))}
 }
 
 
@@ -80,7 +80,7 @@ Opt :> OPT = {
   ;; Church encoding; it requires the abstract type opt a to be implemented
   ;; with a polymorphic (i.e., large) type. Thus, wrap the type.
   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
-  caseopt (xo :# opt _) = xo _
+  none (b : type) (n : b) (s : _ ~> b) = n
+  some x (b : type) (n : b) (s : _ ~> b) = s x
+  caseopt (xo : opt _) = xo _
 }
diff --git a/regression.1ml b/regression.1ml
index a3731e47..795653f2 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -44,17 +44,12 @@ Equivalence: {
   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 _ _) :# t _ _ = eq
-  un (eq :# t _ _) = eq
-  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 (type fun x => x) a
-  from 'a 'b (eq: t a b) b = un eq (type fun b => b ~> a) id b
-  symmetry 'a 'b (eq: t a b) : t b a =
-    wr fun (type p _) => un eq (type fun b => p b ~> p a) id
+  type t a b = wrap (type p _) ~> p a ~> p b
+  transitivity (ab: t _ _) (bc: t _ _) (type p _) = bc p << ab p
+  reflexivity (type p _) = id
+  to (eq: t _ _) a = eq (type fun x => x) a
+  from (eq: t _ _) b = eq (type fun b => b ~> _) id b
+  symmetry (eq: t _ _) (type p _) = eq (type fun b => p b ~> p _) id
 }
 
 ;;
@@ -220,7 +215,7 @@ type_error rec (R: {}) => {
   kaboom () = R
 }
 
-Kaboom = rec (R: rec R => {kaboom: () ~> R}) :@ (= R) => {kaboom () = R}
+Kaboom = rec (R: rec R => {kaboom: () ~> R}) : (= R) => {kaboom () = R}
 
 ;;
 
@@ -247,14 +242,14 @@ in {
   }) => {
     Even = {
       ...T.Even
-      make 'x (head: x) (tail: T.Odd.t x) :@ T.Even.t x =
+      make 'x (head: x) (tail: T.Odd.t x) : T.Even.t x =
         {head, tail}
-      size 'x (v :@ T.Even.t x) = 1 + R.Odd.size v.tail
+      size 'x (v: T.Even.t x) = 1 + R.Odd.size v.tail
     }
     Odd = {
       ...T.Odd
-      make 'x (v: opt (T.Even.t x)) :@ T.Odd.t x = v
-      size 'x (v :@ T.Odd.t x) =
+      make 'x (v: opt (T.Even.t x)) : T.Odd.t x = v
+      size 'x (v: T.Odd.t x) =
         v |> Opt.case {
           none = 0
           some e = R.Even.size e
@@ -291,11 +286,10 @@ AnnotRecType = {
 Hungry = {
   type eat a = rec eat_a => a ~> eat_a
 
-  eater 'a = rec (eater: eat a) :@ eat a => fun a => eater
+  eater 'a = rec (eater: eat a) : eat a => fun a => eater
 
-  (eater :@ eat _) <+ x = eater x
-
-  do eater <+ 1 <+ 2
+  do eater 1 2
+  do eater 1 2 3
 }
 
 type_error rec {type t _, type u _} => {
@@ -310,9 +304,9 @@ PolyRec = {
 
   t_int = t int
 
-  hmm (x :@ t int) = flip Alt.case x
+  hmm (x : t int) = flip Alt.case x
 
-  t0 = inr (inl (0, 0) :@ t (int, int)) :@ t int
+  t0 = inr (inl (0, 0) : t (int, int)) : t int
 }
 
 N :> {
@@ -327,17 +321,14 @@ ListN = let
     nil     :               p N.Z
     (::) 'n : x ~> t x n ~> p (N.S n)
   }
-  type T x n (type t _ _) = (type p _) -> I x p t ~> p n
 in {
-  ...rec {type t _ _} => {type t x n = wrap T x n t}
+  ...rec {type t _ _} => {type t x n = wrap (type p _) -> I x p t ~> p n}
 
-  case 'x 'n (type p _) (cs: I x p t) (e :# wrap T x n t :@ t x n) =
+  case 'x 'n (type p _) (cs: I x p t) (e : t _ _) =
     e p cs
 
-  let mk 'x 'n (c: T x n t) = c :# wrap T x n t :@ t x n in {
-    nil  'x                     = mk fun (type p _) (r: I x p t) => r.nil
-    'x (v: x) :: 'n (vs: t x n) = mk fun (type p _) (r: I x p t) => r.:: v vs
-  }
+  nil  'x                       (type p _) (r: I x p t) = r.nil
+  ('x (v: x) :: 'n (vs: t x n)) (type p _) (r: I x p t) = r.:: v vs
 } :> {
   type t _ _
 
diff --git a/russo.1ml b/russo.1ml
index 3af08418..90133049 100644
--- a/russo.1ml
+++ b/russo.1ml
@@ -82,13 +82,13 @@ sift (S : STREAM) :> STREAM = {
 
 Sieve :> STREAM = {
   type state = wrap STREAM
-  start :# state = {
+  start = {
     type state = int
     start = 2
     next n = n + 1
     value s = s
   }
-  next (S :# state) :# state = sift S
+  next (S :# state) = sift S
   value (S :# state) = S.value S.start
 }
 
diff --git a/sub.ml b/sub.ml
index 54eed403..fe1c8ddf 100644
--- a/sub.ml
+++ b/sub.ml
@@ -180,8 +180,19 @@ let rec sub_typ oneway env t1 t2 ps =
   Trace.sub (lazy ("[sub_typ] ps = " ^
     String.concat ", " (List.map string_of_norm_typ ps)));
   let e1 = IL.VarE("x") in
+  let t1' = norm_typ t1 in
+  let t2' = freshen_typ env (norm_typ t2) in
   let ts, zs, e =
-    match norm_typ t1, freshen_typ env (norm_typ t2) with
+    match (if oneway then try_rec_from_typ t1' else None),
+          (if oneway then try_rec_from_typ t2' else None) with
+    | Some (unroll_t, roll_t), None when not (is_undet t2') ->
+       let ts, zs, f = sub_typ oneway env unroll_t t2' ps in
+       ts, lift env zs, IL.AppE(f, IL.UnrollE(e1))
+    | None, Some (unroll_t, roll_t) when not (is_undet t1') ->
+       let ts, zs, f = sub_typ oneway env t1' unroll_t ps in
+       ts, lift env zs, IL.RollE(IL.AppE(f, e1), erase_typ roll_t)
+    | _ ->
+    match t1', t2' with
     | t1, FunT(aks21, t21, ExT(aks22, t22), Implicit) ->
       assert (aks22 = []);
       let ts, zs, f = sub_typ oneway (add_typs aks21 env) t1 t22 ps in
@@ -238,6 +249,18 @@ let rec sub_typ oneway env t1 t2 ps =
         with Sub e -> raise (Sub (Wrap e)) in
       [], zs, IL.TupE["wrap", IL.AppE(f, IL.DotE(e1, "wrap"))]
 
+    | t1, WrapT(s2) when oneway && not (is_undet t1) ->
+      let _, zs, f =
+        try sub_extyp oneway env (ExT([], t1)) s2 []
+        with Sub e -> raise (Sub (Wrap e)) in
+      [], zs, IL.TupE["wrap", IL.AppE(f, e1)]
+
+    | WrapT(ExT([], _) as s1), t2 when oneway && not (is_undet t2) ->
+      let _, zs, f =
+        try sub_extyp oneway env s1 (ExT([], t2)) []
+        with Sub e -> raise (Sub (Wrap e)) in
+      [], zs, IL.DotE(e1, "wrap")
+
     | AppT(t1', ts1), AppT(t2', ts2) ->
       (try
         let zs1 = equal_typ env t1' t2' in
diff --git a/syntax.ml b/syntax.ml
index cc0dffb7..80b64e27 100644
--- a/syntax.ml
+++ b/syntax.ml
@@ -301,10 +301,7 @@ let wrapP(p, t2) =
       patB(p, VarE("$"@@t2.at)@@t2.at)@@span[p.at; t2.at]
     )@@span[p.at; t2.at];
    infer = None;
-   annot =
-    match p.it.annot with
-    | None -> Some t2
-    | Some t1 -> Some (AsT(t2, WrapT(t1)@@t1.at)@@span[p.at; t2.at])}
+   annot = None}
 
 let strP(xps, region) =
   match xps with
diff --git a/talk.1ml b/talk.1ml
index 8fb050e1..f4486fc3 100644
--- a/talk.1ml
+++ b/talk.1ml
@@ -109,14 +109,14 @@ do map : 'a -> 'b -> (m: type -> type) -> (M: MONAD m) -> (a ~> b) ~> m a ~> m b
   }
 }
 
-newpoint = rec (newpoint : int -> int -> point) => fun x y :@ point => {
+newpoint = rec (newpoint : int -> int -> point) => fun x y : point => {
   getX () = x
   getY () = y
   move dx dy = newpoint (x + dx) (y + dy)
 }
 
 p = newpoint 3 4
-p' @: point = (p @: point).move 1 2
+p' = p.move 1 2
 do Int.print (p'.getX ())
 do print " "
 do Int.print (p'.getY ())
diff --git a/types.ml b/types.ml
index 9c271049..80cdb667 100644
--- a/types.ml
+++ b/types.ml
@@ -537,6 +537,39 @@ and unify_row r1 r2 =
   with Invalid_argument _ -> false
 
 
+(* rec *)
+
+let is_undet = function
+  | InferT _ -> true
+  | _ -> false
+
+let rec try_rec_from_typ' t =
+  match t with
+  | RecT(ak, unroll_t) as rec_t ->
+    Some (rec_t, unroll_t, rec_t, ak)
+  | AppT(t, ts) ->
+    try_rec_from_typ' t
+     |> Lib.Option.map (fun (rec_t, unroll_t, roll_t, ak) ->
+        rec_t, AppT(unroll_t, ts), AppT(roll_t, ts), ak)
+  | DotT(t, lab) ->
+    try_rec_from_typ' t
+     |> Lib.Option.map (fun (rec_t, unroll_t, roll_t, ak) ->
+            rec_t, DotT(unroll_t, lab), DotT(roll_t, lab), ak)
+  | _ ->
+    None
+
+let try_rec_from_typ t =
+  try_rec_from_typ' t
+   |> Lib.Option.map (fun (rec_t, unroll_t, roll_t, ak) ->
+      subst_typ (subst [ak] [rec_t]) unroll_t, roll_t)
+
+let try_rec_from_extyp = function
+  | ExT([], t) ->
+    try_rec_from_typ t
+  | _ ->
+    None
+
+
 (* String conversion *)
 
 let verbose_binders_flag = ref false
diff --git a/types.mli b/types.mli
index 66532b62..da4ff720 100644
--- a/types.mli
+++ b/types.mli
@@ -169,6 +169,14 @@ val unify_typ : typ -> typ -> bool
 val undecidable_flag : bool ref
 
 
+(* rec *)
+
+val is_undet : typ -> bool
+
+val try_rec_from_typ : typ -> (typ * typ) option
+val try_rec_from_extyp : extyp -> (typ * typ) option
+
+
 (* String conversion *)
 
 val verbose_binders_flag : bool ref