Fix joins for row likes with incompatible kinds (#139)

* Revert "Temporary hack for bug in Row_like join (#137)"

This reverts commit c9591dc.

* Prevent joins between products of different kinds.

Row likes now have an assumption on fields kinds related to tags

* Add test for the problematic join

middle_end/flambda2/tests/mlexamples/product_join_with_mixed_kinds.ml

@@ -0,0 +1,22 @@
+
+type float_rec = { a : float; b : float; }
+type (_, _) c =
+  | F : (float_rec, unit) c
+  | B : (int * int, int * int) c
+
+let f (type x) (type y) (b : (x, y) c) w x (y:y) : x * unit =
+  let x : x =
+    match b with
+    | F ->
+      { a = w; b = x }
+    | B ->
+      let (u, v) = y in
+      (* This creates a row_like of type Other ( value, value ) *)
+      let _ = Sys.opaque_identity (u + v) in
+      y
+  in
+  (* Here happens the join of
+     Tag_254 ( float, float ) with Other ( value, value )
+     If nothing was done to prevent it, there would be a join between
+     products with different kinds, which is prohibited *)
+  x, ()

middle_end/flambda2/types/structures/closures_entry.rec.ml

@@ -214,3 +214,5 @@ let map_closure_types
         closure_types;
         closure_var_types;
       })
+
+let fields_kind _ = Flambda_kind.value

middle_end/flambda2/types/structures/closures_entry.rec.mli

@@ -46,6 +46,8 @@ val function_decl_types : t -> Function_declaration_type.t Closure_id.Map.t
 
 val closure_var_types : t -> Type_grammar.t Var_within_closure.Map.t
 
+val fields_kind : t -> Flambda_kind.t
+
 include Type_structure_intf.S
   with type t := t
   with type flambda_type := Type_grammar.t

middle_end/flambda2/types/structures/product.rec.ml

@@ -41,6 +41,8 @@ module Make (Index : Product_intf.Index) = struct
 
   let print_with_cache ~cache:_ ppf t = print ppf t
 
+  let fields_kind t = t.kind
+
   let create kind components_by_index =
     (* CR mshinwell: Check that the types are all of the same kind *)
     { components_by_index;
@@ -186,6 +188,8 @@ module Int_indexed = struct
 
   let print_with_cache ~cache:_ ppf t = print ppf t
 
+  let fields_kind t = t.kind
+
   let create_from_list kind tys = {
     kind;
     fields = Array.of_list tys;
@@ -247,11 +251,9 @@ module Int_indexed = struct
 
   let join env t1 t2 =
     if not (Flambda_kind.equal t1.kind t2.kind) then begin
-      failwith "mismatching kinds" (* XXX temporary *)
-        (*
       Misc.fatal_errorf "Product.Int_indexed.join between mismatching \
                          kinds %a and %a@."
-        Flambda_kind.print t1.kind Flambda_kind.print t2.kind *)
+        Flambda_kind.print t1.kind Flambda_kind.print t2.kind
     end;
     let fields1 = t1.fields in
     let fields2 = t2.fields in

middle_end/flambda2/types/structures/product_intf.ml

@@ -37,6 +37,8 @@ module type S_base = sig
 
   val project : t -> Index.t -> flambda_type Or_unknown.t
 
+  val fields_kind : t -> Flambda_kind.t
+
   include Type_structure_intf.S
     with type t := t
     with type flambda_type := flambda_type

middle_end/flambda2/types/structures/row_like.rec.ml

@@ -50,6 +50,9 @@ struct
 
   type case = {
     maps_to : Maps_to.t;
+    (** kinds different than value are only allowed in cases with known tags.
+        Currently tag 254 must have fields of kind float and all other must have
+        fields of kind value. *)
     index : index;
     env_extension : TEE.t;
   }
@@ -279,6 +282,10 @@ struct
         | At_least i1', At_least i2' ->
           At_least (Index.inter i1' i2')
       in
+      let matching_kinds case1 case2 =
+        Flambda_kind.equal (Maps_to.fields_kind case1.maps_to)
+          (Maps_to.fields_kind case2.maps_to)
+      in
       let join_case env case1 case2 =
         let index = join_index case1.index case2.index in
         let maps_to = Maps_to.join env case1.maps_to case2.maps_to in
@@ -289,11 +296,12 @@ struct
         { maps_to; index; env_extension }
       in
       let join_knowns_tags case1 case2 : case option =
+        (* We assume that if tags are equals, the products will
+           contains values of the same kinds. *)
         match case1, case2 with
         | None, None -> None
         | Some case1, None -> begin
-            match other2 with
-            | Bottom ->
+            let only_case1 () =
               (* CF Type_descr.join_head_or_unknown_or_bottom,
                  we need to join those to ensure that free variables not
                  present in the target env are cleaned out of the types.
@@ -307,12 +315,19 @@ struct
               in
               let case1 = join_case env case1 case1 in
               Some case1
+            in
+            match other2 with
+            | Bottom ->
+              only_case1 ()
             | Ok other_case ->
-              Some (join_case env case1 other_case)
+              if matching_kinds case1 other_case then
+                Some (join_case env case1 other_case)
+              else
+                (* If kinds don't match, the tags can't match *)
+                only_case1 ()
           end
         | None, Some case2 -> begin
-            match other1 with
-            | Bottom ->
+            let only_case2 () =
               (* See at the other bottom case *)
               let env =
                 Join_env.create
@@ -322,8 +337,15 @@ struct
               in
               let case2 = join_case env case2 case2 in
               Some case2
+            in
+            match other1 with
+            | Bottom ->
+              only_case2 ()
             | Ok other_case ->
-              Some (join_case env other_case case2)
+              if matching_kinds other_case case2 then
+                Some (join_case env other_case case2)
+              else
+                only_case2 ()
           end
         | Some case1, Some case2 ->
           Some (join_case env case1 case2)

middle_end/flambda2/types/structures/row_like_maps_to_intf.ml

@@ -28,6 +28,8 @@ module type S = sig
 
   type t
 
+  val fields_kind : t -> Flambda_kind.t
+
   include Type_structure_intf.S
     with type t := t
     with type flambda_type := flambda_type

middle_end/flambda2/types/type_of_kind/type_of_kind_value0.rec.ml

@@ -340,9 +340,7 @@ let join_variant env
     Known (Blocks.join env b1 b2)
   in
   let blocks =
-    try (* XXX temporary *)
-      join_unknown blocks_join env blocks1 blocks2
-    with (Failure _) -> Or_unknown.Unknown
+    join_unknown blocks_join env blocks1 blocks2
   in
   let imms =
     join_unknown (T.join ?bound_name:None) env imms1 imms2