Track bound_vars in constrain_type_jkind

Author: goldfirere

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

@@ -2913,5 +2913,13 @@ type ('a : immediate & immediate) t2
 type t3 = t1 t2  (* it is important to reject this *)
 
 [%%expect{|
-type t3 = t1 t2
+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.
 |}]

typing/ctype.ml

@@ -1466,6 +1466,14 @@ let instance_parameterized_type ?keep_names sch_args sch =
     (ty_args, ty)
   )
 
+let instance_parameterized_type_ex ?keep_names sch_args sch ~existentials =
+  For_copy.with_scope (fun copy_scope ->
+    let ty_args = List.map (fun t -> copy ?keep_names copy_scope t) sch_args in
+    let ty = copy copy_scope sch in
+    let existentials = List.map (copy copy_scope) existentials in
+    (ty_args, ty, existentials)
+  )
+
 let instance_parameterized_kind args jkind =
   For_copy.with_scope (fun copy_scope ->
     let ty_args = List.map (fun t -> copy copy_scope t) args in
@@ -1812,7 +1820,7 @@ let instance_prim (desc : Primitive.description) ty =
 let unify_var' = (* Forward declaration *)
   ref (fun _env _ty1 _ty2 -> assert false)
 
-let subst env level priv abbrev oty params args body =
+let subst env level priv abbrev oty params args body ~existentials =
   if List.length params <> List.length args then raise Cannot_subst;
   let old_level = !current_level in
   current_level := level;
@@ -1829,14 +1837,16 @@ let subst env level priv abbrev oty params args body =
         | _ -> assert false
   in
   abbreviations := abbrev;
-  let (params', body') = instance_parameterized_type params body in
+  let (params', body', existentials') =
+    instance_parameterized_type_ex params body ~existentials
+  in
   abbreviations := ref Mnil;
   let uenv = Expression {env; in_subst = true} in
   try
     !unify_var' uenv body0 body';
     List.iter2 (!unify_var' uenv) params' args;
     current_level := old_level;
-    body'
+    (body', existentials')
   with Unify _ ->
     current_level := old_level;
     undo_abbrev ();
@@ -1892,11 +1902,11 @@ let jkind_subst env level params args jkind =
    it ensures invariants on types are enforced (decreasing levels), and we don't
    care about efficiency here.
 *)
-let apply ?(use_current_level = false) env params body args =
+let apply ?(use_current_level = false) env params body args ~existentials =
   simple_abbrevs := Mnil;
   let level = if use_current_level then !current_level else generic_level in
   try
-    subst env level Public (ref Mnil) None params args body
+    subst env level Public (ref Mnil) None params args body ~existentials
   with
     Cannot_subst -> raise Cannot_apply
 
@@ -1975,9 +1985,10 @@ let expand_abbrev_gen kind find_type_expansion env ty =
       | (params, body, lv) ->
           (* prerr_endline
              ("add a "^string_of_kind kind^" expansion for "^Path.name path);*)
-          let ty' =
+          let ty', _existentials =
             try
               subst env level kind abbrev (Some ty) params args body
+                ~existentials:[]
             with Cannot_subst -> raise_escape_exn Constraint
           in
           (* For gadts, remember type as non exportable *)
@@ -2118,11 +2129,14 @@ let is_principal ty =
 
 type unwrapped_type_expr =
   { ty : type_expr
-  ; is_open : bool
+  ; bound_vars : TypeSet.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 = TypeSet.empty; modality = Mode.Modality.Value.Const.id }
+
+let mk_bound_vars vars_list =
+  TypeSet.of_list (List.map Transient_expr.repr vars_list)
 
 type unbox_result =
   (* unboxing process made a step: either an unboxing or removal of a [Tpoly] *)
@@ -2140,7 +2154,9 @@ 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 =
+        apply env decl.type_params ty2 args ~existentials
+      in
       begin match find_unboxed_type decl with
       | Some (ty2, modality) ->
         let ty2 = match get_desc ty2 with Tpoly (t, _) -> t | _ -> ty2 in
@@ -2153,8 +2169,9 @@ 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);
+        let substed_ty, substed_existentials = apply ty2 existentials in
+        Stepped { ty = substed_ty;
+                  bound_vars = mk_bound_vars substed_existentials;
                   modality }
       | None -> begin match decl.type_kind with
         | Type_record_unboxed_product ([_], Record_unboxed_product, _) ->
@@ -2163,8 +2180,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 = fst (apply ld.ld_type []);
+                                   bound_vars = TypeSet.empty;
                                    modality = ld.ld_modalities }) lbls)
         | Type_record_unboxed_product ([], _, _) ->
           Misc.fatal_error "Ctype.unboxed_once: fieldless record"
@@ -2175,15 +2192,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 = mk_bound_vars 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 _ -> []
@@ -2198,28 +2215,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 = TypeSet.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:TypeSet.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
@@ -2250,12 +2269,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
+            TypeSet.union bound_vars1 bound_vars2, (ty, modality))
+         TypeSet.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]. *)
@@ -2267,7 +2288,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
@@ -2311,11 +2332,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 (TypeSet.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)
@@ -2324,9 +2344,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 modality
 
 
@@ -2385,15 +2405,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
@@ -2405,7 +2429,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 (TypeSet.mem ty bound_vars) ->
        (* Unfixed tyvars are special in at least two ways:
 
           1) Suppose we're processing [type 'a t = 'a list]. The ['a] on the
@@ -2434,9 +2459,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 = TypeSet.union bound_vars (mk_bound_vars bound_vars2) in
+      loop ~fuel ~expanded:false t ~bound_vars ty's_jkind jkind
 
     | _ ->
        match
@@ -2461,11 +2486,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 = TypeSet.union bound_vars bound_vars2 in
                       let jkind =
                         Jkind.apply_modality_to_expected 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
@@ -2498,7 +2524,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
@@ -2510,10 +2536,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 = TypeSet.union bound_vars bound_vars2 in
                  let jkind = Jkind.apply_modality_to_expected 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
@@ -2529,7 +2555,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:TypeSet.empty
     (estimate_type_jkind env ty) jkind
 
 let type_sort ~why ~fixed env ty =
@@ -6163,10 +6189,10 @@ let rec build_subtype env (visited : transient_expr list)
       begin try match get_desc t' with
         Tobject _ when posi && not (opened_object t') ->
           let cl_abbr, body = find_cltype_for_path env p in
-          let ty =
+          let ty, _existentials =
             try
               subst env !current_level Public abbrev None
-                cl_abbr.type_params tl body
+                cl_abbr.type_params tl body ~existentials:[]
             with Cannot_subst -> assert false in
           let ty1, tl1 =
             match get_desc ty with
@@ -7142,6 +7168,9 @@ let print_global_state fmt global_state =
   in
   Format.fprintf fmt "@[<1>{@;%a}@]" print_fields global_state
 
+let apply ?use_current_level env params body args =
+  fst (apply ?use_current_level env params body args ~existentials:[])
+
               (*******************************)
               (* checking declaration jkinds *)
               (* this is down here so it can use [is_equal] *)

typing/ctype.mli

@@ -574,7 +574,10 @@ val mcomp : Env.t -> type_expr -> type_expr -> unit
    types and [Tpoly]s *)
 type unwrapped_type_expr =
   { ty : type_expr
-  ; is_open : bool  (* are there any unbound variables in this type? *)
+  ; bound_vars : Btype.TypeSet.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 :