diff --git a/docs/whitedoc/michelson.rst b/docs/whitedoc/michelson.rst
index ed51b5814..045775913 100644
--- a/docs/whitedoc/michelson.rst
+++ b/docs/whitedoc/michelson.rst
@@ -2265,8 +2265,7 @@ helps users track information in the stack for bare contracts.
 
 For unannotated accesses with ``CAR`` and ``CDR`` to fields that are
 named will be appended (with an additional ``.`` character) to the pair
-variable annotation. If the original pair is not named in the stack, no
-variable annotation will be inferred.
+variable annotation.
 
 ::
 
@@ -2281,6 +2280,14 @@ If fields are not named but the pair is still named in the stack then
    CDAR
    :: @p (pair 'a (pair 'b 'c)) : 'S ->  @p.cdr.car 'b : 'S
 
+If the original pair is not named in the stack, but a field annotation
+is present in the pair type the accessed value will be annotated with a
+variable annotation corresponding to the field annotation alone.
+
+::
+
+   CDAR
+   :: (pair ('a %foo) (pair %bar ('b %x) ('c %y))) : 'S ->  @p.bar.x 'b : 'S
 
 A similar mechanism is used for context dependent instructions:
 
diff --git a/src/proto_alpha/lib_client/michelson_v1_macros.ml b/src/proto_alpha/lib_client/michelson_v1_macros.ml
index 339462f9a..e67340588 100644
--- a/src/proto_alpha/lib_client/michelson_v1_macros.ml
+++ b/src/proto_alpha/lib_client/michelson_v1_macros.ml
@@ -48,16 +48,20 @@ let expand_caddadr original =
         ok None
   | _ -> ok None
 
-let extract_first_field_annot annot =
-  let rec extract_first_field_annot others = function
+let extract_first_annot annot char =
+  let rec extract_first_annot others = function
     | [] -> None, List.rev others
     | a :: rest ->
-        match a.[0] with
-        | '%' -> Some a, List.rev_append others rest
-        | _ -> extract_first_field_annot (a :: others) rest
-        | exception Invalid_argument _ -> extract_first_field_annot (a :: others) rest
+        try
+          if a.[0] = char
+          then Some a, List.rev_append others rest
+          else extract_first_annot (a :: others) rest
+        with Invalid_argument _ -> extract_first_annot (a :: others) rest
   in
-  extract_first_field_annot [] annot
+  extract_first_annot [] annot
+
+let extract_first_field_annot annot = extract_first_annot annot '%'
+let extract_first_bind_annot annot = extract_first_annot annot '$'
 
 let extract_field_annots annot =
   List.partition (fun a ->
@@ -121,13 +125,8 @@ let expand_set_caddadr original =
                           ] in
             let encoding = [ Prim (loc, "CDR", [], []) ;
                              Prim (loc, "SWAP", [], []) ] in
-            let rename = match field_annot with
-              | None -> []
-              | Some f  -> [ Prim (loc, "RENAME", [],
-                                   [ "@" ^ String.sub f 1 (String.length f - 1) ]) ]
-            in
             let pair = [ Prim (loc, "PAIR", [], []) ] in
-            let init = Seq (loc, access_check @ encoding @ rename @ pair) in
+            let init = Seq (loc, access_check @ encoding @ pair) in
             ok (Some (parse (len - 3) init))
         | 'D' ->
             let access_check = match field_annot with
@@ -137,18 +136,8 @@ let expand_set_caddadr original =
                             Prim (loc, "DROP", [], []) ;
                           ] in
             let encoding = [ Prim (loc, "CAR", [], []) ] in
-            let rename = match field_annot with
-              | None -> []
-              | Some f  ->
-                  [ Prim (loc, "DIP", [
-                        Seq (loc, [
-                            Prim (loc, "RENAME", [],
-                                  [ "@" ^ String.sub f 1 (String.length f - 1) ])
-                          ])
-                      ], []) ]
-            in
             let pair = [ Prim (loc, "PAIR", [], []) ] in
-            let init = Seq (loc, access_check @ encoding @ rename @ pair) in
+            let init = Seq (loc, access_check @ encoding @ pair) in
             ok (Some (parse (len - 3) init))
         | _ -> assert false
       else
@@ -170,6 +159,7 @@ let expand_map_caddadr original =
           | [] | _ :: _ :: _ -> error (Invalid_arity (str, List.length args, 1))
         end >>? fun code ->
         let field_annot, annot = extract_first_field_annot annot in
+        let bind_annot, annot = extract_first_bind_annot annot in
         let rec parse i acc =
           if i = 4 then
             acc
@@ -200,14 +190,14 @@ let expand_map_caddadr original =
                          Prim (loc, "PAIR", [], annot) ]) in
                 parse (i - 1) acc
             | _ -> assert false in
-        let cr_annot = match field_annot with
-          | None -> []
-          | Some f -> [ f ] in
-        let rename_op =  match field_annot with
-          | None -> []
-          | Some f ->
-              [ Prim (loc, "RENAME", [],
-                      [ "@" ^ String.sub f 1 (String.length f - 1) ]) ] in
+        let cr_annot =
+          let f = match field_annot with
+            | None -> []
+            | Some f -> [ f ] in
+          let b = match bind_annot with
+            | None -> []
+            | Some b -> [ "@" ^ String.sub b 1 (String.length b - 1) ] in
+          f @ b in
         match String.get str (len - 2) with
         | 'A' ->
             let init =
@@ -215,8 +205,7 @@ let expand_map_caddadr original =
                    [ Prim (loc, "DUP", [], []) ;
                      Prim (loc, "CDR", [], []) ;
                      Prim (loc, "DIP",
-                           [ Seq (loc, [ Prim (loc, "CAR", [], cr_annot) ; code ] @
-                                       rename_op ) ], []) ;
+                           [ Seq (loc, [ Prim (loc, "CAR", [], cr_annot) ; code ]) ], []) ;
                      Prim (loc, "SWAP", [], []) ;
                      Prim (loc, "PAIR", [], []) ]) in
             ok (Some (parse (len - 3) init))
@@ -225,9 +214,7 @@ let expand_map_caddadr original =
               Seq (loc,
                    [ Prim (loc, "DUP", [], []) ;
                      Prim (loc, "CDR", [], cr_annot) ;
-                     code ] @
-                   rename_op @
-                   [
+                     code ;
                      Prim (loc, "SWAP", [], []) ;
                      Prim (loc, "CAR", [], []) ;
                      Prim (loc, "PAIR", [], []) ]) in
@@ -674,7 +661,6 @@ let unexpand_set_caddadr expanded =
              Prim (_, "DROP", [], []) ;
              Prim (_, "CDR", [], []) ;
              Prim (_, "SWAP", [], []) ;
-             Prim (_, "RENAME", [], _) ;
              Prim (_, "PAIR", [], []) ]) ->
         Some (loc, "A" :: acc, field_annot :: annots)
     | Seq (loc,
@@ -686,7 +672,6 @@ let unexpand_set_caddadr expanded =
              Prim (_, "CDR", [], [ field_annot ]) ;
              Prim (_, "DROP", [], []) ;
              Prim (_, "CAR", [], []) ;
-             Prim (_, "DIP", [ Seq (_, [ Prim (_, "RENAME", [], _) ]) ], []);
              Prim (_, "PAIR", [], []) ]) ->
         Some (loc, "D" :: acc, field_annot :: annots)
     | Seq (_,
@@ -734,8 +719,7 @@ let unexpand_map_caddadr expanded =
              Prim (_, "DIP",
                    [ Seq (_,
                           [ Prim (_, "CAR", [], [ field_annot ]) ;
-                            code ;
-                            Prim (_, "RENAME", [], _) ]) ], []) ;
+                            code ]) ], []) ;
              Prim (_, "PAIR", [], []) ]) ->
         Some (loc, "A" :: acc, field_annot :: annots, code)
     | Seq (loc,
@@ -750,7 +734,6 @@ let unexpand_map_caddadr expanded =
            [ Prim (_, "DUP", [], []) ;
              Prim (_, "CDR", [], [ field_annot ]) ;
              code ;
-             Prim (_, "RENAME", [], _) ;
              Prim (_, "SWAP", [], []) ;
              Prim (_, "CAR", [], []) ;
              Prim (_, "PAIR", [], []) ]) ->
diff --git a/src/proto_alpha/lib_protocol/src/script_ir_annot.ml b/src/proto_alpha/lib_protocol/src/script_ir_annot.ml
index 5b39922df..53f20c3ef 100644
--- a/src/proto_alpha/lib_protocol/src/script_ir_annot.ml
+++ b/src/proto_alpha/lib_protocol/src/script_ir_annot.ml
@@ -94,10 +94,10 @@ let gen_access_annot
   : var_annot option -> ?default:field_annot option -> field_annot option -> var_annot option
   = fun value_annot ?(default=None) field_annot ->
     match value_annot, field_annot, default with
-    | None, None, _ | Some _, None, None -> None
+    | None, None, _ | Some _, None, None | None, Some `Field_annot "", _ -> None
     | None, Some `Field_annot f, _ ->
         Some (`Var_annot f)
-    | Some `Var_annot v, None, Some `Field_annot f ->
+    | Some `Var_annot v, (None | Some `Field_annot ""), Some `Field_annot f ->
         Some (`Var_annot (String.concat "." [v; f]))
     | Some `Var_annot v, Some `Field_annot f, _ ->
         Some (`Var_annot (String.concat "." [v; f]))
@@ -106,10 +106,10 @@ let gen_binding_access_annot
   : var_annot option -> ?default:binding_annot option -> binding_annot option -> binding_annot option
   = fun value_annot ?(default=None) binding_annot ->
     match value_annot, binding_annot, default with
-    | None, None, _ | Some _, None, None -> None
+    | None, None, _ | Some _, None, None | None, Some `Binding_annot "", _ -> None
     | None, Some `Binding_annot b, _ ->
         Some (`Binding_annot b)
-    | Some `Var_annot v, None, Some `Binding_annot b ->
+    | Some `Var_annot v, (None | Some `Binding_annot ""), Some `Binding_annot b ->
         Some (`Binding_annot (String.concat "." [v; b]))
     | Some `Var_annot v, Some `Binding_annot b, _ ->
         Some (`Binding_annot (String.concat "." [v; b]))
diff --git a/src/proto_alpha/lib_protocol/src/script_ir_translator.ml b/src/proto_alpha/lib_protocol/src/script_ir_translator.ml
index 466ac4ae7..29b6f4503 100644
--- a/src/proto_alpha/lib_protocol/src/script_ir_translator.ml
+++ b/src/proto_alpha/lib_protocol/src/script_ir_translator.ml
@@ -1828,10 +1828,10 @@ and parse_instr
     | Prim (loc, I_LOOP_LEFT, [ body ], annot),
       (Item_t (Union_t ((tl, l_field), (tr, _), _), rest, union_annot) as stack) ->
         check_kind [ Seq_kind ] body >>=? fun () ->
-        fail_unexpected_annot loc annot >>=? fun () ->
-        parse_var_field_annot loc annot >>=? fun (r_annot, l_annot) ->
-        let l_annot = default_annot (field_to_var_annot l_annot)
-            ~default:(gen_access_annot union_annot l_field) in
+        parse_binding_annot loc annot >>=? fun l_bind_annot ->
+        let l_bind_annot = default_annot l_bind_annot
+            ~default:(gen_binding_access_annot union_annot (field_to_binding_annot l_field)) in
+        let l_annot = binding_to_var_annot l_bind_annot in
         parse_instr ?type_logger tc_context ctxt body
           (Item_t (tl, rest, l_annot)) >>=? begin fun (judgement, ctxt) -> match judgement with
           | Typed ibody ->
@@ -1839,10 +1839,10 @@ and parse_instr
               trace unmatched_branches
                 (Lwt.return (stack_ty_eq 1 ibody.aft stack) >>=? fun Eq ->
                  Lwt.return (merge_stacks loc ibody.aft stack) >>=? fun _stack ->
-                 typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, r_annot)))
+                 typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, None)))
           | Failed { descr } ->
               let ibody = descr stack in
-              typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, r_annot))
+              typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, None))
         end
     | Prim (loc, I_LAMBDA, [ arg ; ret ; code ], annot),
       stack ->