Don't try to put Tof_kind in a row variable

Author: glittershark

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

@@ -358,3 +358,48 @@ Error: The kind of type "box" is immutable_data with _
        But the kind of type "box" must be a subkind of immediate
          because of the annotation on the declaration of the type box.
 |}]
+
+(* Existential row variables *)
+
+type exist_row1 = Mk : ([< `A | `B of int ref] as 'a) -> exist_row1
+[%%expect{|
+type exist_row1 = Mk : [< `A | `B of int ref ] -> exist_row1
+|}]
+
+let foo (x : exist_row1 @ nonportable) = use_portable x
+(* CR layouts v2.8: This should be accepted *)
+[%%expect{|
+Line 1, characters 54-55:
+1 | let foo (x : exist_row1 @ nonportable) = use_portable x
+                                                          ^
+Error: This value is "nonportable" but expected to be "portable".
+|}]
+
+let foo (x : exist_row1 @ contended) = use_uncontended x
+[%%expect{|
+Line 1, characters 55-56:
+1 | let foo (x : exist_row1 @ contended) = use_uncontended x
+                                                           ^
+Error: This value is "contended" but expected to be "uncontended".
+|}]
+
+type exist_row2 = Mk : ([> `A | `B of int ref] as 'a) -> exist_row2
+[%%expect{|
+type exist_row2 = Mk : [> `A | `B of int ref ] -> exist_row2
+|}]
+
+let foo (x : exist_row1 @ nonportable) = use_portable x
+[%%expect{|
+Line 1, characters 54-55:
+1 | let foo (x : exist_row1 @ nonportable) = use_portable x
+                                                          ^
+Error: This value is "nonportable" but expected to be "portable".
+|}]
+
+let foo (x : exist_row1 @ contended) = use_uncontended x
+[%%expect{|
+Line 1, characters 55-56:
+1 | let foo (x : exist_row1 @ contended) = use_uncontended x
+                                                           ^
+Error: This value is "contended" but expected to be "uncontended".
+|}]

typing/btype.ml

@@ -256,8 +256,7 @@ let set_static_row_name decl path =
                   (*  Utilities for type traversal  *)
                   (**********************************)
 
-let fold_row f init row =
-  let result =
+let fold_row_fields f init row =
     List.fold_left
       (fun init (_, fi) ->
          match row_field_repr fi with
@@ -266,7 +265,9 @@ let fold_row f init row =
          | _ -> init)
       init
       (row_fields row)
-  in
+
+let fold_row f init row =
+  let result = fold_row_fields f init row in
   match get_desc (row_more row) with
   | Tvar _ | Tunivar _ | Tsubst _ | Tconstr _ | Tnil | Tof_kind _ ->
     begin match
@@ -277,6 +278,9 @@ let fold_row f init row =
     end
   | _ -> assert false
 
+let iter_row_fields f row =
+  fold_row_fields (fun () v -> f v) () row
+
 let iter_row f row =
   fold_row (fun () v -> f v) () row
 

typing/btype.mli

@@ -138,6 +138,9 @@ val fold_type_expr: ('a -> type_expr -> 'a) -> 'a -> type_expr -> 'a
 val iter_row: (type_expr -> unit) -> row_desc -> unit
         (* Iteration on types in a row *)
 val fold_row: ('a -> type_expr -> 'a) -> 'a -> row_desc -> 'a
+val iter_row_fields: (type_expr -> unit) -> row_desc -> unit
+        (* Iteration on fields in a row, excluding row variable *)
+val fold_row_fields: ('a -> type_expr -> 'a) -> 'a -> row_desc -> 'a
 val iter_abbrev: (type_expr -> unit) -> abbrev_memo -> unit
         (* Iteration on types in an abbreviation list *)
 val iter_type_expr_kind: (type_expr -> unit) -> (type_decl_kind -> unit)

typing/datarepr.ml

@@ -21,20 +21,22 @@ open Types
 open Btype
 
 (* Simplified version of Ctype.free_vars *)
-let free_vars ?(param=false) ty =
+let free_vars ?(param=false) ?(include_row_variables=true) ty =
   let ret = ref TypeSet.empty in
   let rec loop ty =
     if try_mark_node ty then
       match get_desc ty with
       | Tvar _ ->
           ret := TypeSet.add ty !ret
       | Tvariant row ->
-          iter_row loop row;
-          if not (static_row row) then begin
-            match get_desc (row_more row) with
-            | Tvar _ when param -> ret := TypeSet.add ty !ret
-            | _ -> loop (row_more row)
-          end
+        if include_row_variables
+        then iter_row loop row
+        else iter_row_fields loop row;
+        if not (static_row row) && include_row_variables then begin
+          match get_desc (row_more row) with
+          | Tvar _ when param -> ret := TypeSet.add ty !ret
+          | _ -> loop (row_more row)
+        end
       (* XXX: What about Tobject ? *)
       | _ ->
           iter_type_expr loop ty
@@ -316,7 +318,7 @@ let unboxed_labels_of_type ty_path decl =
   | Type_record _
   | Type_variant _ | Type_abstract _ | Type_open -> []
 
-let constructor_unbound_type_vars cstr =
+let constructor_unbound_type_vars_excluding_row_variables cstr =
   match cstr.cd_res with
   | None -> TypeSet.empty
   | Some res_ty ->
@@ -332,15 +334,8 @@ let constructor_unbound_type_vars cstr =
       | _ -> Misc.fatal_error "cd_res must be Tconstr"
     in
     let arg_vars_set =
-      free_vars (newgenty (Ttuple (List.map (fun ty -> None, ty) tyl)))
+      free_vars
+        ~include_row_variables:false
+        (newgenty (Ttuple (List.map (fun ty -> None, ty) tyl)))
     in
     TypeSet.diff arg_vars_set bound_vars
-
-let unbound_type_vars decl =
-  match decl.type_kind with
-  | Type_variant (cstrs, _, _) ->
-    List.fold_left (fun res cstr ->
-      TypeSet.union res (constructor_unbound_type_vars cstr))
-      TypeSet.empty
-      cstrs
-  | _  -> TypeSet.empty

typing/datarepr.mli

@@ -47,6 +47,5 @@ val constructor_existentials :
     - the existential variables introduced by the constructor
  *)
 
-val constructor_unbound_type_vars : constructor_declaration -> Btype.TypeSet.t
-
-val unbound_type_vars : type_declaration -> Btype.TypeSet.t
+val constructor_unbound_type_vars_excluding_row_variables
+  : constructor_declaration -> Btype.TypeSet.t

typing/typedecl.ml

@@ -2028,7 +2028,7 @@ let rec update_decl_jkind env dpath decl =
                    | None -> `Args (decl.type_params @ ret_args), `Params (decl.type_params @ params), seen
                    | Some res ->
                      let existentials =
-                       Datarepr.constructor_unbound_type_vars cstr
+                       Datarepr.constructor_unbound_type_vars_excluding_row_variables cstr
                        |> Btype.TypeSet.to_seq
                        |> Seq.map Types.Transient_expr.type_expr
                        |> List.of_seq