Fix inclusion checks for primitives

ocaml/lambda/translcore.ml

@@ -298,7 +298,7 @@ let rec iter_exn_names f pat =
 let transl_ident loc env ty path desc kind =
   match desc.val_kind, kind with
   | Val_prim p, Id_prim pmode ->
-      let poly_mode = transl_alloc_mode pmode in
+      let poly_mode = Option.map transl_alloc_mode pmode in
       Translprim.transl_primitive loc p env ty ~poly_mode (Some path)
   | Val_anc _, Id_value ->
       raise(Error(to_location loc, Free_super_var))
@@ -373,7 +373,7 @@ and transl_exp0 ~in_new_scope ~scopes e =
         if extra_args = [] then transl_apply_position pos
         else Rc_normal
       in
-      let prim_mode = transl_alloc_mode pmode in
+      let prim_mode = Option.map transl_alloc_mode pmode in
       let lam =
         Translprim.transl_primitive_application
           (of_location ~scopes e.exp_loc) p e.exp_env prim_type prim_mode

ocaml/lambda/translmod.ml

@@ -97,7 +97,7 @@ let rec apply_coercion loc strict restr arg =
       let carg = apply_coercion loc Alias cc_arg (Lvar param) in
       apply_coercion_result loc strict arg [param, Pgenval] [carg] cc_res
   | Tcoerce_primitive { pc_desc; pc_env; pc_type; pc_poly_mode } ->
-      let poly_mode = Translcore.transl_alloc_mode pc_poly_mode in
+      let poly_mode = Option.map Translcore.transl_alloc_mode pc_poly_mode in
       Translprim.transl_primitive loc pc_desc pc_env pc_type ~poly_mode None
   | Tcoerce_alias (env, path, cc) ->
       let lam = transl_module_path loc env path in
@@ -613,7 +613,8 @@ and transl_structure ~scopes loc fields cc rootpath final_env = function
                       | Tcoerce_primitive p ->
                           let loc = of_location ~scopes p.pc_loc in
                           let poly_mode =
-                            Translcore.transl_alloc_mode p.pc_poly_mode
+                            Option.map
+                              Translcore.transl_alloc_mode p.pc_poly_mode
                           in
                           Translprim.transl_primitive
                             loc p.pc_desc p.pc_env p.pc_type ~poly_mode None
@@ -1039,7 +1040,7 @@ let field_of_str loc str =
   fun (pos, cc) ->
     match cc with
     | Tcoerce_primitive { pc_desc; pc_env; pc_type; pc_poly_mode } ->
-        let poly_mode = Translcore.transl_alloc_mode pc_poly_mode in
+        let poly_mode = Option.map Translcore.transl_alloc_mode pc_poly_mode in
         Translprim.transl_primitive loc pc_desc pc_env pc_type ~poly_mode None
     | Tcoerce_alias (env, path, cc) ->
         let lam = transl_module_path loc env path in
@@ -1380,7 +1381,9 @@ let transl_store_structure ~scopes glob map prims aliases str =
     List.fold_right (add_ident may_coerce) idlist subst
 
   and store_primitive (pos, prim) cont =
-    let poly_mode = Translcore.transl_alloc_mode prim.pc_poly_mode in
+    let poly_mode =
+      Option.map Translcore.transl_alloc_mode prim.pc_poly_mode
+    in
     Lsequence(Lprim(mod_setfield pos,
                     [Lprim(Pgetglobal glob, [], Loc_unknown);
                      Translprim.transl_primitive Loc_unknown

ocaml/lambda/translprim.ml

@@ -112,7 +112,10 @@ let prim_sys_argv =
 let to_alloc_mode ~poly = function
   | Prim_global, _ -> alloc_heap
   | Prim_local, _ -> alloc_local
-  | Prim_poly, _ -> poly
+  | Prim_poly, _ ->
+    match poly with
+    | None -> assert false
+    | Some mode -> mode
 
 let lookup_primitive loc poly pos p =
   let mode = to_alloc_mode ~poly p.prim_native_repr_res in
@@ -714,8 +717,8 @@ let lambda_of_prim prim_name prim loc args arg_exps =
 let check_primitive_arity loc p =
   let mode =
     match p.prim_native_repr_res with
-    | Prim_global, _ | Prim_poly, _ -> alloc_heap
-    | Prim_local, _ -> alloc_local
+    | Prim_global, _ | Prim_poly, _ -> Some alloc_heap
+    | Prim_local, _ -> Some alloc_local
   in
   let prim = lookup_primitive loc mode Rc_normal p in
   let ok =

ocaml/lambda/translprim.mli

@@ -35,13 +35,13 @@ val check_primitive_arity :
 val transl_primitive :
   Lambda.scoped_location -> Primitive.description -> Env.t ->
   Types.type_expr ->
-  poly_mode:Lambda.alloc_mode ->
+  poly_mode:Lambda.alloc_mode option ->
   Path.t option ->
   Lambda.lambda
 
 val transl_primitive_application :
   Lambda.scoped_location -> Primitive.description -> Env.t ->
-  Types.type_expr -> Lambda.alloc_mode -> Path.t ->
+  Types.type_expr -> Lambda.alloc_mode option -> Path.t ->
   Typedtree.expression option ->
   Lambda.lambda list -> Typedtree.expression list ->
   Lambda.region_close -> Lambda.lambda

ocaml/testsuite/tests/typing-local/local.ml

@@ -1711,6 +1711,17 @@ Error: Signature mismatch:
        is not included in
          val add : local_ int32 -> local_ int32 -> int32
 |}]
+
+module Contravariant_instantiation : sig
+  external to_int_trunc : Int64.t -> int = "%int64_to_int"
+end = struct
+  external to_int_trunc : (Int64.t [@local_opt]) -> int = "%int64_to_int"
+end
+[%%expect{|
+module Contravariant_instantiation :
+  sig external to_int_trunc : Int64.t -> int = "%int64_to_int" end
+|}]
+
 (* Return modes *)
 let zx : int ref -> (int -> unit) = (:=)
 let zz : local_ (int ref) -> int -> unit = (:=)

ocaml/typing/btype.ml

@@ -966,6 +966,12 @@ module Alloc_mode = struct
     | Ok (), Ok () -> Ok ()
     | Error (), _ | _, Error () -> Error ()
 
+  let make_global_exn t =
+    submode_exn t global
+
+  let make_local_exn t =
+    submode_exn local t
+
   let next_id = ref (-1)
   let fresh () =
     incr next_id;

ocaml/typing/btype.mli

@@ -278,6 +278,10 @@ module Alloc_mode : sig
 
   val equate : t -> t -> (unit, unit) result
 
+  val make_global_exn : t -> unit
+
+  val make_local_exn : t -> unit
+
   val join_const : const -> const -> const
 
   val join : t list -> t

ocaml/typing/ctype.ml

@@ -1543,12 +1543,15 @@ let instance_label fixed lbl =
 let prim_mode mvar = function
   | Primitive.Prim_global, _ -> Alloc_mode.global
   | Primitive.Prim_local, _ -> Alloc_mode.local
-  | Primitive.Prim_poly, _ -> mvar
+  | Primitive.Prim_poly, _ ->
+    match mvar with
+    | Some mvar -> mvar
+    | None -> assert false
 
 let rec instance_prim_locals locals mvar macc finalret ty =
   match locals, (repr ty).desc with
   | l :: locals, Tarrow ((lbl,_,mret),arg,ret,commu) ->
-     let marg = prim_mode mvar l in
+     let marg = prim_mode (Some mvar) l in
      let macc = Alloc_mode.join [marg; mret; macc] in
      let mret =
        match locals with
@@ -1566,12 +1569,12 @@ let instance_prim_mode (desc : Primitive.description) ty =
   if is_poly desc.prim_native_repr_res ||
        List.exists is_poly desc.prim_native_repr_args then
     let mode = Alloc_mode.newvar () in
-    let finalret = prim_mode mode desc.prim_native_repr_res in
+    let finalret = prim_mode (Some mode) desc.prim_native_repr_res in
     instance_prim_locals desc.prim_native_repr_args
       mode Alloc_mode.global finalret ty,
-    mode
+    Some mode
   else
-    ty, Alloc_mode.global
+    ty, None
 
 (**** Instantiation with parameter substitution ****)
 

ocaml/typing/ctype.mli

@@ -239,9 +239,10 @@ val instance_label:
         bool -> label_description -> type_expr list * type_expr * type_expr
         (* Same, for a label *)
 val prim_mode :
-        alloc_mode -> (Primitive.mode * Primitive.native_repr) -> alloc_mode
+        alloc_mode option -> (Primitive.mode * Primitive.native_repr)
+        -> alloc_mode
 val instance_prim_mode:
-        Primitive.description -> type_expr -> type_expr * alloc_mode
+        Primitive.description -> type_expr -> type_expr * alloc_mode option
 
 val apply:
         Env.t -> type_expr list -> type_expr -> type_expr list -> type_expr

ocaml/typing/includecore.ml

@@ -20,10 +20,62 @@ open Path
 open Types
 open Typedtree
 
+type position = Ctype.Unification_trace.position = First | Second
+
 (* Inclusion between value descriptions *)
 
 exception Dont_match
 
+type primitive_mismatch =
+  | Name
+  | Arity
+  | No_alloc of position
+  | Builtin
+  | Effects
+  | Coeffects
+  | Native_name
+  | Result_repr
+  | Argument_repr of int
+
+let native_repr_args nra1 nra2 =
+  let rec loop i nra1 nra2 =
+    match nra1, nra2 with
+    | [], [] -> None
+    | [], _ :: _ -> assert false
+    | _ :: _, [] -> assert false
+    | (_, nr1) :: nra1, (_, nr2) :: nra2 ->
+      if not (Primitive.equal_native_repr nr1 nr2) then Some (Argument_repr i)
+      else loop (i+1) nra1 nra2
+  in
+  loop 1 nra1 nra2
+
+let primitive_descriptions pd1 pd2 =
+  let open Primitive in
+  if not (String.equal pd1.prim_name pd2.prim_name) then
+    Some Name
+  else if not (Int.equal pd1.prim_arity pd2.prim_arity) then
+    Some Arity
+  else if (not pd1.prim_alloc) && pd2.prim_alloc then
+    Some (No_alloc First)
+  else if pd1.prim_alloc && (not pd2.prim_alloc) then
+    Some (No_alloc Second)
+  else if pd1.prim_c_builtin && pd2.prim_c_builtin then
+    Some Builtin
+  else if not (Primitive.equal_effects pd1.prim_effects pd2.prim_effects) then
+    Some Effects
+  else if not
+    (Primitive.equal_coeffects
+       pd1.prim_coeffects pd2.prim_coeffects) then
+    Some Coeffects
+  else if not (String.equal pd1.prim_native_name pd2.prim_native_name) then
+    Some Native_name
+  else if not
+    (Primitive.equal_native_repr
+       (snd pd1.prim_native_repr_res) (snd pd2.prim_native_repr_res)) then
+    Some Result_repr
+  else
+    native_repr_args pd1.prim_native_repr_args pd2.prim_native_repr_args
+
 let value_descriptions ~loc env name
     (vd1 : Types.value_description)
     (vd2 : Types.value_description) =
@@ -34,22 +86,31 @@ let value_descriptions ~loc env name
     vd1.val_attributes vd2.val_attributes
     name;
   match vd1.val_kind with
-  | Val_prim p1 ->
-     let ty1, mode1 = Ctype.instance_prim_mode p1 vd1.val_type in
-     begin match vd2.val_kind with
-     | Val_prim p2 ->
-        let ty2, _mode2 = Ctype.instance_prim_mode p2 vd2.val_type in
-        if not (Ctype.moregeneral env true ty1 ty2) then
-          raise Dont_match;
-        let mode1 : Primitive.mode =
-          match Btype.Alloc_mode.check_const mode1 with
-          | Some Global -> Prim_global
-          | Some Local -> Prim_local
-          | None -> Prim_poly
-        in
-        let p1 = Primitive.inst_mode mode1 p1 in
-        if p1 = p2 then Tcoerce_none else raise Dont_match
+  | Val_prim p1 -> begin
+     match vd2.val_kind with
+     | Val_prim p2 -> begin
+         let ty1_global, _ = Ctype.instance_prim_mode p1 vd1.val_type in
+         let ty2_global =
+           let ty2, mode2 = Ctype.instance_prim_mode p2 vd2.val_type in
+           Option.iter Btype.Alloc_mode.make_global_exn mode2;
+           ty2
+         in
+         if not (Ctype.moregeneral env true ty1_global ty2_global) then
+           raise Dont_match;
+         let ty1_local, _ = Ctype.instance_prim_mode p1 vd1.val_type in
+         let ty2_local =
+           let ty2, mode2 = Ctype.instance_prim_mode p2 vd2.val_type in
+           Option.iter Btype.Alloc_mode.make_local_exn mode2;
+           ty2
+         in
+         if not (Ctype.moregeneral env true ty1_local ty2_local) then
+           raise Dont_match;
+         match primitive_descriptions p1 p2 with
+         | None -> Tcoerce_none
+         | Some _ -> raise Dont_match
+       end
      | _ ->
+        let ty1, mode1 = Ctype.instance_prim_mode p1 vd1.val_type in
         if not (Ctype.moregeneral env true ty1 vd2.val_type) then
           raise Dont_match;
         let pc =
@@ -141,8 +202,6 @@ let type_manifest env ty1 params1 ty2 params2 priv2 =
 
 (* Inclusion between type declarations *)
 
-type position = Ctype.Unification_trace.position = First | Second
-
 let choose ord first second =
   match ord with
   | First -> first

ocaml/typing/primitive.ml

@@ -276,19 +276,50 @@ let native_name p =
 let byte_name p =
   p.prim_name
 
+let equal_boxed_integer bi1 bi2 =
+  match bi1, bi2 with
+  | Pnativeint, Pnativeint
+  | Pint32, Pint32
+  | Pint64, Pint64 ->
+    true
+  | (Pnativeint | Pint32 | Pint64), _ ->
+    false
+
+let equal_native_repr nr1 nr2 =
+  match nr1, nr2 with
+  | Same_as_ocaml_repr, Same_as_ocaml_repr -> true
+  | Same_as_ocaml_repr,
+    (Unboxed_float | Unboxed_integer _ | Untagged_int) -> false
+  | Unboxed_float, Unboxed_float -> true
+  | Unboxed_float,
+    (Same_as_ocaml_repr | Unboxed_integer _ | Untagged_int) -> false
+  | Unboxed_integer bi1, Unboxed_integer bi2 -> equal_boxed_integer bi1 bi2
+  | Unboxed_integer _,
+    (Same_as_ocaml_repr | Unboxed_float | Untagged_int) -> false
+  | Untagged_int, Untagged_int -> true
+  | Untagged_int,
+    (Same_as_ocaml_repr | Unboxed_float | Unboxed_integer _) -> false
+
+let equal_effects ef1 ef2 =
+  match ef1, ef2 with
+  | No_effects, No_effects -> true
+  | No_effects, (Only_generative_effects | Arbitrary_effects) -> false
+  | Only_generative_effects, Only_generative_effects -> true
+  | Only_generative_effects, (No_effects | Arbitrary_effects) -> false
+  | Arbitrary_effects, Arbitrary_effects -> true
+  | Arbitrary_effects, (No_effects | Only_generative_effects) -> false
+
+let equal_coeffects cf1 cf2 =
+  match cf1, cf2 with
+  | No_coeffects, No_coeffects -> true
+  | No_coeffects, Has_coeffects -> false
+  | Has_coeffects, Has_coeffects -> true
+  | Has_coeffects, No_coeffects -> false
+
 let native_name_is_external p =
   let nat_name = native_name p in
   nat_name <> "" && nat_name.[0] <> '%'
 
-let inst_mode mode p =
-  let inst_repr = function
-    | Prim_poly, r -> mode, r
-    | (Prim_global|Prim_local) as m, r -> m, r
-  in
-  { p with
-    prim_native_repr_args = List.map inst_repr p.prim_native_repr_args;
-    prim_native_repr_res = inst_repr p.prim_native_repr_res }
-
 let report_error ppf err =
   match err with
   | Old_style_float_with_native_repr_attribute ->

ocaml/typing/primitive.mli

@@ -87,13 +87,16 @@ val print
 val native_name: description -> string
 val byte_name: description -> string
 
+val equal_boxed_integer : boxed_integer -> boxed_integer -> bool
+val equal_native_repr : native_repr -> native_repr -> bool
+val equal_effects : effects -> effects -> bool
+val equal_coeffects : coeffects -> coeffects -> bool
+
 (** [native_name_is_externa] returns [true] iff the [native_name] for the
     given primitive identifies that the primitive is not implemented in the
     compiler itself. *)
 val native_name_is_external : description -> bool
 
-val inst_mode : mode -> description -> description
-
 type error =
   | Old_style_float_with_native_repr_attribute
   | Old_style_noalloc_with_noalloc_attribute

ocaml/typing/typecore.ml

@@ -4712,8 +4712,8 @@ and type_ident env ?(recarg=Rejected) lid =
     match desc.val_kind with
     | Val_prim prim ->
        let ty, mode = instance_prim_mode prim (instance desc.val_type) in
-       begin match prim.prim_native_repr_res with
-       | Prim_poly, _ -> register_allocation_mode mode
+       begin match prim.prim_native_repr_res, mode with
+       | (Prim_poly, _), Some mode -> register_allocation_mode mode
        | _ -> ()
        end;
        ty, Id_prim mode