Michelson: do not infer pair field names and fail when fields differ

docs/whitedoc/michelson.rst

@@ -1841,8 +1841,7 @@ X - Annotations
 ---------------
 
 The annotation mechanism of Michelson provides ways to better track
-data on the stack and withing data structures (pairs, unions and
+data on the stack and to give additional type constraints.
-options), as well as to give additional type constraints.
 
 Stack visualization tools like the Michelson’s Emacs mode print
 annotations associated with each type in the program, as propagated by
@@ -1851,8 +1850,8 @@ in the stack. This is useful as a debugging aid.
 
 We distinguish four kinds of annotations:
 - type annotations, written ``:type_annot``,
-- field or constructors annotations, written ``%field_annot``,
 - variable annotations, written ``@var_annot``,
+- field or constructors annotations, written ``%field_annot``,
 - and binding annotations, written ``$bind_annot``.
 
 Type Annotations
@@ -2078,6 +2077,10 @@ can be used to represent the algebraic data type (in OCaml-like syntax):
      | C of { n1 : nat ; n2 : nat }
 
 
+Field annotations are part of the type (at the same level as type name
+annotations), and so types with differing field names (if present) are
+not considered equal.
+
 Instructions that construct elements of composed types can also be
 annotated with one or multiple field annotations (in addition to type
 and variable annotations).

src/proto_alpha/lib_protocol/src/script_ir_annot.ml

@@ -136,8 +136,7 @@ let merge_field_annot
     | Some `Field_annot a1, Some `Field_annot a2 ->
         if String.equal a1 a2
         then ok annot1
-        else ok None (* TODO check this, do we want typechecking here ?
+        else error (Inconsistent_annotations ("%" ^ a1, "%" ^ a2))
-                        error (Inconsistent_annotations ("%" ^ a1, "%" ^ a2)) *)
 
 let merge_var_annot
   : var_annot option -> var_annot option -> var_annot option

src/proto_alpha/lib_protocol/src/script_ir_annot.mli

@@ -72,7 +72,9 @@ val gen_binding_access_annot :
 val merge_type_annot :
   type_annot option -> type_annot option -> type_annot option tzresult
 
-(** Merge field annotations, does not fail ([None] if different). *)
+(** Merge field annotations.
+    @returns an error {!Inconsistent_type_annotations} if they are both present
+    and different *)
 val merge_field_annot :
   field_annot option -> field_annot option -> field_annot option tzresult
 

src/proto_alpha/lib_protocol/src/script_ir_translator.ml

@@ -1502,10 +1502,8 @@ and parse_instr
         return ctxt judgement
     (* pairs *)
     | Prim (loc, I_PAIR, [], annot),
-      Item_t (a, Item_t (b, rest, snd_annot), fst_annot) ->
+      Item_t (a, Item_t (b, rest, _snd_annot), _fst_annot) ->
         parse_constr_annot loc annot >>=? fun (annot, ty_name, l_field, r_field) ->
-        let l_field = default_annot l_field ~default:(var_to_field_annot fst_annot) in
-        let r_field = default_annot r_field ~default:(var_to_field_annot snd_annot) in
         typed ctxt loc Cons_pair
           (Item_t (Pair_t((a, l_field), (b, r_field), ty_name), rest, annot))
     | Prim (loc, I_CAR, [], annot),