Track existentials in constrain_type_jkind

testsuite/tests/typing-jkind-bounds/with_basics.ml

@@ -1187,7 +1187,7 @@ Error: This value is "nonportable" but expected to be "portable".
 
 (*********************************************)
 (* Reduction of error seen in the tree *)
-(* This requires the [is_open] technology in Ctype. *)
+(* This requires the [bound_vars] technology in Ctype. *)
 
 type 'k t1 = T of Obj.t [@@unboxed]
 

testsuite/tests/typing-layouts/basics.ml

@@ -2897,3 +2897,29 @@ let f (x : ('a : value mod uncontended)) = x ()
 val f : (unit -> 'a) -> 'a = <fun>
 val f : (unit -> 'a) -> 'a = <fun>
 |}]
+
+(********************************************************************)
+(* Test 47: not changing the kinds of existentially bound variables *)
+
+(* this uses products only to avoid the separability restriction *)
+type t1 = T1 : ('a : value). #('a * 'a) -> t1 [@@unboxed]
+type ('a : immediate & immediate) t2
+
+[%%expect{|
+type t1 = T1 : #('a * 'a) -> t1 [@@unboxed]
+type ('a : immediate & immediate) t2
+|}]
+
+type t3 = t1 t2  (* it is important to reject this *)
+
+[%%expect{|
+Line 1, characters 10-12:
+1 | type t3 = t1 t2  (* it is important to reject this *)
+              ^^
+Error: This type "t1" should be an instance of type
+         "('a : immediate & immediate)"
+       The kind of t1 is immediate with 'a & immediate with 'a
+         because it is an unboxed tuple.
+       But the kind of t1 must be a subkind of immediate & immediate
+         because of the definition of t2 at line 2, characters 0-36.
+|}]

tools/debug_printers.ml

@@ -23,3 +23,4 @@ let mod_bounds ppf m = Types.Jkind_mod_bounds.debug_print ppf m
 let with_bounds ppf w = Jkind.With_bounds.debug_print ppf w
 let with_bounds_types ppf w = Jkind.With_bounds.debug_print_types ppf w
 let modalities = Mode.Modality.Value.Const.print
+let type_set ppf set = let open Format in fprintf ppf "@[[%a]@]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";@ ") Printtyp.raw_type_expr) (Btype.TypeSet.elements set)

typing/ctype.ml

@@ -2141,13 +2141,66 @@ let expand_head_opt env ty =
 let is_principal ty =
   not !Clflags.principal || get_level ty = generic_level
 
+module Bound_vars : sig
+  type t
+
+  val empty : t
+  val of_list : type_expr list -> t
+  val add : t -> type_expr list -> t
+  val union : t -> t -> t
+  val mem : t -> type_expr -> bool
+  val is_empty : t -> bool
+end = struct
+  (* It is rare to care about which variables have been bound. This
+     implementation prioritizes the common case of caring only about the
+     presence of variables. *)
+  type t = { is_empty : bool; var_set : TypeSet.t Lazy.t }
+
+  let empty = { is_empty = true; var_set = Lazy.from_val TypeSet.empty }
+
+  let of_list = function
+    | [] -> empty
+    | new_ones ->
+      let var_set =
+        lazy (TypeSet.of_list (List.map Transient_expr.repr new_ones))
+      in
+      { is_empty = false; var_set }
+
+  let add t = function
+    | [] -> t
+    | new_ones ->
+      let var_set = lazy begin
+        let new_ones_set =
+          TypeSet.of_list (List.map Transient_expr.repr new_ones)
+        in
+        TypeSet.union new_ones_set (Lazy.force t.var_set)
+      end in
+      { is_empty = false; var_set }
+
+  let union ({ is_empty = empty1; var_set = set1 } as t1)
+        ({ is_empty = empty2; var_set = set2 } as t2) =
+    match empty1, empty2 with
+    | true, true -> empty
+    | true, false -> t2
+    | false, true -> t1
+    | false, false ->
+      let var_set = lazy (TypeSet.union (Lazy.force set1) (Lazy.force set2)) in
+      { is_empty = false; var_set }
+
+  let mem { is_empty; var_set } ty =
+    not is_empty &&
+    TypeSet.mem ty (Lazy.force var_set)
+
+  let is_empty { is_empty } = is_empty
+end
+
 type unwrapped_type_expr =
   { ty : type_expr
-  ; is_open : bool
+  ; bound_vars : Bound_vars.t
   ; modality : Mode.Modality.Value.Const.t }
 
 let mk_unwrapped_type_expr ty =
-  { ty; is_open = false; modality = Mode.Modality.Value.Const.id }
+  { ty; bound_vars = Bound_vars.empty; modality = Mode.Modality.Value.Const.id }
 
 type unbox_result =
   (* unboxing process made a step: either an unboxing or removal of a [Tpoly] *)
@@ -2165,7 +2218,12 @@ let unbox_once env ty =
     begin match Env.find_type p env with
     | exception Not_found -> Missing p
     | decl ->
-      let apply ty2 = apply env decl.type_params ty2 args in
+      let apply ty2 existentials =
+        (* put [existentials] first as they're often empty. This will
+           unify the copied existentials with the originals after the copy, thus
+           preserving their identity. *)
+        apply env (existentials @ decl.type_params) ty2 (existentials @ args)
+      in
       begin match find_unboxed_type decl with
       | Some (ty2, modality) ->
         let ty2 = match get_desc ty2 with Tpoly (t, _) -> t | _ -> ty2 in
@@ -2178,8 +2236,8 @@ let unbox_once env ty =
           | Type_record_unboxed_product _ | Type_open -> []
           | exception Not_found -> (* but we found it earlier! *) assert false
         in
-        Stepped { ty = apply ty2;
-                  is_open = not (Misc.Stdlib.List.is_empty existentials);
+        Stepped { ty = apply ty2 existentials;
+                  bound_vars = Bound_vars.of_list existentials;
                   modality }
       | None -> begin match decl.type_kind with
         | Type_record_unboxed_product ([_], Record_unboxed_product, _) ->
@@ -2188,8 +2246,8 @@ let unbox_once env ty =
         | Type_record_unboxed_product
             ((_::_::_ as lbls), Record_unboxed_product, _) ->
           Stepped_record_unboxed_product
-            (List.map (fun ld -> { ty = apply ld.ld_type;
-                                   is_open = false;
+            (List.map (fun ld -> { ty = apply ld.ld_type [];
+                                   bound_vars = Bound_vars.empty;
                                    modality = ld.ld_modalities }) lbls)
         | Type_record_unboxed_product ([], _, _) ->
           Misc.fatal_error "Ctype.unboxed_once: fieldless record"
@@ -2200,15 +2258,15 @@ let unbox_once env ty =
     end
   | Tpoly (ty, bound_vars) ->
     Stepped { ty;
-              is_open = not (Misc.Stdlib.List.is_empty bound_vars);
+              bound_vars = Bound_vars.of_list bound_vars;
               modality = Mode.Modality.Value.Const.id }
   | _ -> Final_result
 
 let contained_without_boxing env ty =
   match get_desc ty with
   | Tconstr _ ->
     begin match unbox_once env ty with
-    | Stepped { ty; is_open = _; modality = _ } -> [ty]
+    | Stepped { ty; bound_vars = _; modality = _ } -> [ty]
     | Stepped_record_unboxed_product tys ->
       List.map (fun { ty; _ } -> ty) tys
     | Final_result | Missing _ -> []
@@ -2223,28 +2281,30 @@ let contained_without_boxing env ty =
    allowing us to return a type for which a definition was found even if
    we eventually bottom out at a missing cmi file, or otherwise. *)
 let rec get_unboxed_type_representation
-          ~is_open ~modality env ty_prev ty fuel =
-  if fuel < 0 then Error { ty; is_open; modality }
+          ~bound_vars ~modality env ty_prev ty fuel =
+  if fuel < 0 then Error { ty; bound_vars; modality }
   else
     (* We use expand_head_opt version of expand_head to get access
        to the manifest type of private abbreviations. *)
     let ty = expand_head_opt env ty in
     match unbox_once env ty with
-    | Stepped { ty = ty2; is_open = is_open2; modality = modality2 } ->
-      let is_open = is_open || is_open2 in
+    | Stepped { ty = ty2; bound_vars = bound_vars2; modality = modality2 } ->
+      let bound_vars = Bound_vars.union bound_vars bound_vars2 in
       let modality =
         Mode.Modality.Value.Const.concat modality ~then_:modality2
       in
       get_unboxed_type_representation
-        ~is_open ~modality env ty ty2 (fuel - 1)
+        ~bound_vars ~modality env ty ty2 (fuel - 1)
     | Stepped_record_unboxed_product _ | Final_result ->
-      Ok { ty; is_open; modality }
-    | Missing _ -> Ok { ty = ty_prev; is_open; modality }
+      Ok { ty; bound_vars; modality }
+    | Missing _ -> Ok { ty = ty_prev; bound_vars; modality }
 
 let get_unboxed_type_representation env ty =
   (* Do not give too much fuel: PR#7424 *)
   get_unboxed_type_representation
-    ~is_open:false ~modality:Mode.Modality.Value.Const.id env ty ty 100
+    ~bound_vars:Bound_vars.empty
+    ~modality:Mode.Modality.Value.Const.id
+    env ty ty 100
 
 let get_unboxed_type_approximation env ty =
   match get_unboxed_type_representation env ty with
@@ -2275,12 +2335,14 @@ let rec estimate_type_jkind ~expand_component env ty =
   | Tarrow _ -> Jkind.for_arrow
   | Ttuple elts -> Jkind.for_boxed_tuple elts
   | Tunboxed_tuple ltys ->
-     let is_open, tys_modalities =
+     let bound_vars, tys_modalities =
        List.fold_left_map
-         (fun is_open1 (_lbl, ty) ->
-            let { ty; is_open = is_open2; modality } = expand_component ty in
-            (is_open1 || is_open2), (ty, modality))
-         false ltys
+         (fun bound_vars1 (_lbl, ty) ->
+            let { ty; bound_vars = bound_vars2; modality } =
+              expand_component ty
+            in
+            Bound_vars.union bound_vars1 bound_vars2, (ty, modality))
+         Bound_vars.empty ltys
      in
      (* CR layouts v2.8: This pretty ridiculous use of [estimate_type_jkind]
         just to throw most of it away will go away once we get [layout_of]. *)
@@ -2292,7 +2354,7 @@ let rec estimate_type_jkind ~expand_component env ty =
      in
      Jkind.Builtin.product
        ~why:Unboxed_tuple tys_modalities layouts |>
-     close_open_jkind ~expand_component ~is_open env
+     close_open_jkind ~expand_component ~bound_vars env
   | Tconstr (p, args, _) -> begin try
       let type_decl = Env.find_type p env in
       let jkind = type_decl.type_jkind in
@@ -2336,11 +2398,10 @@ let rec estimate_type_jkind ~expand_component env ty =
     Jkind.disallow_right
   | Tpackage _ -> Jkind.Builtin.value ~why:First_class_module
 
-and close_open_jkind ~expand_component ~is_open env jkind =
-  if is_open (* if the type has free variables, we can't let these leak into
-                with-bounds *)
-    (* CR layouts v2.8: Do better, by tracking the actual free variables and
-       rounding only those variables up. *)
+and close_open_jkind ~expand_component ~bound_vars env jkind =
+  if not (Bound_vars.is_empty bound_vars)
+  (* if the type has free variables, we can't let these leak into with-bounds *)
+    (* CR layouts v2.8: Do better, by rounding only the bound variables up. *)
   then
     let jkind_of_type ty =
       Some (estimate_type_jkind ~expand_component env ty)
@@ -2349,9 +2410,9 @@ and close_open_jkind ~expand_component ~is_open env jkind =
   else jkind
 
 let estimate_type_jkind_unwrapped
-      ~expand_component env { ty; is_open; modality } =
+      ~expand_component env { ty; bound_vars; modality } =
   estimate_type_jkind ~expand_component env ty |>
-  close_open_jkind ~expand_component ~is_open env |>
+  close_open_jkind ~expand_component ~bound_vars env |>
   Jkind.apply_modality_l modality
 
 
@@ -2410,15 +2471,19 @@ let constrain_type_jkind ~fixed env ty jkind =
      later).
 
      As this unboxes types, it might unbox an existential type. We thus keep
-     track of whether [ty] [is_open]. EDIT: This is actually pointless and
-     could be removed: #3684.
+     track of the variables bound as we unbox (and look through [Tpoly]s).
+     Comparing these variables in jkinds is fine, and they can't escape from
+     this function (except harmlessly in error messages). However, we must be
+     sure not to change the kinds of these bound variables; that's the only
+     reason we track them here. See Test 47 in typing-layouts/basics.ml for an
+     example.
 
      As this unboxed types, it might also encounter modalities. These modalities
      are accommodated by changing [jkind], the expected jkind of the type.
      Trying to apply the modality to the jkind extracted from [ty] would be
      wrong, as it would incorrectly change the jkind on a [Tvar] to mode-cross
      more than necessary.  *)
-  let rec loop ~fuel ~expanded ty ~is_open ty's_jkind jkind =
+  let rec loop ~fuel ~expanded ty ~bound_vars ty's_jkind jkind =
     (* Just succeed if we're comparing against [any] *)
     if Jkind.is_obviously_max jkind then Ok () else
     if fuel < 0 then
@@ -2430,7 +2495,8 @@ let constrain_type_jkind ~fixed env ty jkind =
     (* The [ty's_jkind] we get here is an **r** jkind, necessary for
        the call to [intersection_or_error]. And even if [ty] has unbound
        variables, [ty's_jkind] can't have any variables in it, so we're OK. *)
-    | Tvar { jkind = ty's_jkind } when not fixed ->
+    | Tvar { jkind = ty's_jkind } when not fixed &&
+                                       not (Bound_vars.mem bound_vars ty) ->
        (* Unfixed tyvars are special in at least two ways:
 
           1) Suppose we're processing [type 'a t = 'a list]. The ['a] on the
@@ -2459,9 +2525,9 @@ let constrain_type_jkind ~fixed env ty jkind =
 
     (* Handle the [Tpoly] case out here so [Tvar]s wrapped in [Tpoly]s can get
        the treatment above. *)
-    | Tpoly (t, bound_vars) ->
-      let is_open = is_open || not (Misc.Stdlib.List.is_empty bound_vars) in
-      loop ~fuel ~expanded:false t ~is_open ty's_jkind jkind
+    | Tpoly (t, bound_vars2) ->
+      let bound_vars = Bound_vars.add bound_vars bound_vars2 in
+      loop ~fuel ~expanded:false t ~bound_vars ty's_jkind jkind
 
     | _ ->
        match
@@ -2486,11 +2552,12 @@ let constrain_type_jkind ~fixed env ty jkind =
              let recur ty's_jkinds jkinds =
                let results =
                  Misc.Stdlib.List.map3
-                   (fun { ty; is_open = _; modality } ty's_jkind jkind ->
+                   (fun { ty; bound_vars = bound_vars2; modality } ty's_jkind jkind ->
+                      let bound_vars = Bound_vars.union bound_vars bound_vars2 in
                       let jkind =
                         Jkind.apply_modality_r modality jkind
                       in
-                      loop ~fuel ~expanded:false ~is_open ty ty's_jkind jkind)
+                      loop ~fuel ~expanded:false ~bound_vars ty ty's_jkind jkind)
                    tys ty's_jkinds jkinds
                in
                if List.for_all Result.is_ok results
@@ -2523,7 +2590,7 @@ let constrain_type_jkind ~fixed env ty jkind =
              if not expanded
              then
                let ty = expand_head_opt env ty in
-               loop ~fuel ~expanded:true ty ~is_open
+               loop ~fuel ~expanded:true ty ~bound_vars
                  (estimate_type_jkind env ty) jkind
              else
                begin match unbox_once env ty with
@@ -2535,10 +2602,10 @@ let constrain_type_jkind ~fixed env ty jkind =
                  Error
                    (Jkind.Violation.of_ ~jkind_of_type
                       (Not_a_subjkind (ty's_jkind, jkind, sub_failure_reasons)))
-               | Stepped { ty; is_open = is_open2; modality } ->
-                 let is_open = is_open || is_open2 in
+               | Stepped { ty; bound_vars = bound_vars2; modality } ->
+                 let bound_vars = Bound_vars.union bound_vars bound_vars2 in
                  let jkind = Jkind.apply_modality_r modality jkind in
-                 loop ~fuel:(fuel - 1) ~expanded:false ty ~is_open
+                 loop ~fuel:(fuel - 1) ~expanded:false ty ~bound_vars
                    (estimate_type_jkind env ty) jkind
                | Stepped_record_unboxed_product tys_modalities ->
                  product ~fuel:(fuel - 1) tys_modalities
@@ -2554,7 +2621,7 @@ let constrain_type_jkind ~fixed env ty jkind =
             Error (Jkind.Violation.of_ ~jkind_of_type
                 (Not_a_subjkind (ty's_jkind, jkind, sub_failure_reasons)))
   in
-  loop ~fuel:100 ~expanded:false ty ~is_open:false
+  loop ~fuel:100 ~expanded:false ty ~bound_vars:Bound_vars.empty
     (estimate_type_jkind env ty) (Jkind.disallow_left jkind)
 
 let type_sort ~why ~fixed env ty =

typing/ctype.mli

@@ -570,12 +570,23 @@ val package_subtype :
 (* Raises [Incompatible] *)
 val mcomp : Env.t -> type_expr -> type_expr -> unit
 
+(* A set of bound variables *)
+module Bound_vars : sig
+  type t
+
+  val is_empty : t -> bool
+  val mem : t -> type_expr -> bool
+end
+
 (* represents a type that has been extracted from wrappers that
    do not change its runtime representation, such as [@@unboxed]
    types and [Tpoly]s *)
 type unwrapped_type_expr =
   { ty : type_expr
-  ; is_open : bool  (* are there any unbound variables in this type? *)
+  ; bound_vars : Bound_vars.t
+  (* vars in scope in [ty] but not in the context to which this
+     [unwrapped_type_expr] is returned. These come from unwrapped existential
+     variables and variables bound in [Tpoly] nodes. *)
   ; modality : Mode.Modality.Value.Const.t }
 
 val get_unboxed_type_representation :