Mark datatypes as injective in recursive module approximations (#10029)

testsuite/tests/typing-misc/injectivity.ml

@@ -423,3 +423,15 @@ Line 1, characters 18-21:
                       ^^^
 Error: Unbound module R
 |}]
+
+(* #10028 by Stephen Dolan *)
+
+module rec A : sig
+  type _ t = Foo : 'a -> 'a A.s t
+  type 'a s = T of 'a
+end =
+  A
+;;
+[%%expect{|
+module rec A : sig type _ t = Foo : 'a -> 'a A.s t type 'a s = T of 'a end
+|}]

typing/datarepr.ml

@@ -85,7 +85,7 @@ let constructor_args ~current_unit priv cd_args cd_res path rep =
           type_kind = Type_record (lbls, rep);
           type_private = priv;
           type_manifest = None;
-          type_variance = Variance.unknown_signature ~arity;
+          type_variance = Variance.unknown_signature ~injective:true ~arity;
           type_separability = Types.Separability.default_signature ~arity;
           type_is_newtype = false;
           type_expansion_scope = Btype.lowest_level;

typing/typeclass.ml

@@ -1311,7 +1311,7 @@ let temp_abbrev loc env id arity uid =
        type_kind = Type_abstract;
        type_private = Public;
        type_manifest = Some ty;
-       type_variance = Variance.unknown_signature ~arity;
+       type_variance = Variance.unknown_signature ~injective:false ~arity;
        type_separability = Types.Separability.default_signature ~arity;
        type_is_newtype = false;
        type_expansion_scope = Btype.lowest_level;
@@ -1490,7 +1490,7 @@ let class_infos define_class kind
 
   (* Class and class type temporary definitions *)
   let cty_variance =
-    Variance.unknown_signature ~arity:(List.length params) in
+    Variance.unknown_signature ~injective:false ~arity:(List.length params) in
   let cltydef =
     {clty_params = params; clty_type = class_body typ;
      clty_variance = cty_variance;
@@ -1572,7 +1572,7 @@ let class_infos define_class kind
      type_kind = Type_abstract;
      type_private = Public;
      type_manifest = Some obj_ty;
-     type_variance = Variance.unknown_signature ~arity;
+     type_variance = Variance.unknown_signature ~injective:false ~arity;
      type_separability = Types.Separability.default_signature ~arity;
      type_is_newtype = false;
      type_expansion_scope = Btype.lowest_level;
@@ -1596,7 +1596,7 @@ let class_infos define_class kind
      type_kind = Type_abstract;
      type_private = Public;
      type_manifest = Some cl_ty;
-     type_variance = Variance.unknown_signature ~arity;
+     type_variance = Variance.unknown_signature ~injective:false ~arity;
      type_separability = Types.Separability.default_signature ~arity;
      type_is_newtype = false;
      type_expansion_scope = Btype.lowest_level;

typing/typedecl.ml

@@ -114,7 +114,7 @@ let enter_type rec_flag env sdecl (id, uid) =
       type_manifest =
         begin match sdecl.ptype_manifest with None -> None
         | Some _ -> Some(Ctype.newvar ()) end;
-      type_variance = Variance.unknown_signature ~arity;
+      type_variance = Variance.unknown_signature ~injective:false ~arity;
       type_separability = Types.Separability.default_signature ~arity;
       type_is_newtype = false;
       type_expansion_scope = Btype.lowest_level;
@@ -403,7 +403,7 @@ let transl_declaration env sdecl (id, uid) =
         type_kind = kind;
         type_private = sdecl.ptype_private;
         type_manifest = man;
-        type_variance = Variance.unknown_signature ~arity;
+        type_variance = Variance.unknown_signature ~injective:false ~arity;
         type_separability = Types.Separability.default_signature ~arity;
         type_is_newtype = false;
         type_expansion_scope = Btype.lowest_level;
@@ -1531,7 +1531,7 @@ let transl_with_constraint id row_path ~sig_env ~sig_decl ~outer_env sdecl =
 
 (* Approximate a type declaration: just make all types abstract *)
 
-let abstract_type_decl arity =
+let abstract_type_decl ~injective arity =
   let rec make_params n =
     if n <= 0 then [] else Ctype.newvar() :: make_params (n-1) in
   Ctype.begin_def();
@@ -1541,7 +1541,7 @@ let abstract_type_decl arity =
       type_kind = Type_abstract;
       type_private = Public;
       type_manifest = None;
-      type_variance = Variance.unknown_signature ~arity;
+      type_variance = Variance.unknown_signature ~injective ~arity;
       type_separability = Types.Separability.default_signature ~arity;
       type_is_newtype = false;
       type_expansion_scope = Btype.lowest_level;
@@ -1559,8 +1559,9 @@ let approx_type_decl sdecl_list =
   let scope = Ctype.create_scope () in
   List.map
     (fun sdecl ->
+      let injective = sdecl.ptype_kind <> Ptype_abstract in
       (Ident.create_scoped ~scope sdecl.ptype_name.txt,
-       abstract_type_decl (List.length sdecl.ptype_params)))
+       abstract_type_decl ~injective (List.length sdecl.ptype_params)))
     sdecl_list
 
 (* Variant of check_abbrev_recursion to check the well-formedness

typing/typedecl.mli

@@ -44,7 +44,7 @@ val transl_with_constraint:
     outer_env:Env.t -> Parsetree.type_declaration ->
     Typedtree.type_declaration
 
-val abstract_type_decl: int -> type_declaration
+val abstract_type_decl: injective:bool -> int -> type_declaration
 val approx_type_decl:
     Parsetree.type_declaration list ->
                                   (Ident.t * type_declaration) list

typing/types.ml

@@ -187,8 +187,9 @@ module Variance = struct
   let conjugate v = swap May_pos May_neg (swap Pos Neg v)
   let get_upper v = (mem May_pos v, mem May_neg v)
   let get_lower v = (mem Pos v, mem Neg v, mem Inv v, mem Inj v)
-  let unknown_signature ~arity =
-    Misc.replicate_list unknown arity
+  let unknown_signature ~injective ~arity =
+    let v = if injective then set Inj true unknown else unknown in
+    Misc.replicate_list v arity
 end
 
 module Separability = struct

typing/types.mli

@@ -308,7 +308,7 @@ module Variance : sig
   val conjugate : t -> t                (* exchange positive and negative *)
   val get_upper : t -> bool * bool                  (* may_pos, may_neg   *)
   val get_lower : t -> bool * bool * bool * bool    (* pos, neg, inv, inj *)
-  val unknown_signature : arity:int -> t list
+  val unknown_signature : injective:bool -> arity:int -> t list
   (** The most pessimistic variance for a completely unknown type. *)
 end