different type kinds

Author: zth

compiler/ml/ctype.ml

@@ -88,6 +88,12 @@ type subtype_context =
       right_variant_name: Path.t;
       issue: Variant_coercion.variant_configuration_issue;
     }
+  | Different_type_kinds of {
+      left_typename: Path.t;
+      right_typename: Path.t;
+      left_type_kind: type_kind;
+      right_type_kind: type_kind;
+    }
 
 exception
   Subtype of
@@ -3777,6 +3783,7 @@ let rec subtype_rec env trace t1 t2 cstrs =
                            Variant_coercion.variant_representation_matches
                              c1_attributes c2_attributes
                          then
+                           (* TODO(subtype-errors) Inline record coercion check, piggy back on record coercion check *)
                            let violation, tl1, tl2 =
                              Record_coercion.check_record_fields fields1 fields2
                            in
@@ -3810,6 +3817,7 @@ let rec subtype_rec env trace t1 t2 cstrs =
               else (trace, t1, t2, !univar_pairs, None) :: cstrs)
         | ( (_, _, {type_kind = Type_record (fields1, repr1)}),
             (_, _, {type_kind = Type_record (fields2, repr2)}) ) ->
+          (* TODO(subtype-errors) Record representation *)
           let same_repr =
             match (repr1, repr2) with
             | Record_regular, Record_regular ->
@@ -3826,7 +3834,20 @@ let rec subtype_rec env trace t1 t2 cstrs =
             if violation then (trace, t1, t2, !univar_pairs, None) :: cstrs
             else subtype_list env trace tl1 tl2 cstrs
           else (trace, t1, t2, !univar_pairs, None) :: cstrs
-        | _ -> (trace, t1, t2, !univar_pairs, None) :: cstrs
+        | (p1, _, {type_kind = tk1}), (p2, _, {type_kind = tk2}) ->
+          ( trace,
+            t1,
+            t2,
+            !univar_pairs,
+            Some
+              (Different_type_kinds
+                 {
+                   left_typename = p1;
+                   right_typename = p2;
+                   left_type_kind = tk1;
+                   right_type_kind = tk2;
+                 }) )
+          :: cstrs
         | exception Not_found -> (trace, t1, t2, !univar_pairs, None) :: cstrs)
       (* | (_, Tconstr(p2, _, _)) when generic_private_abbrev false env p2 ->
          subtype_rec env trace t1 (expand_abbrev_opt env t2) cstrs *)

compiler/ml/ctype.mli

@@ -37,6 +37,12 @@ type subtype_context =
       right_variant_name: Path.t;
       issue: Variant_coercion.variant_configuration_issue;
     }
+  | Different_type_kinds of {
+      left_typename: Path.t;
+      right_typename: Path.t;
+      left_type_kind: type_kind;
+      right_type_kind: type_kind;
+    }
 
 exception Unify of (type_expr * type_expr) list
 exception Tags of label * label

compiler/ml/printtyp.ml

@@ -1651,9 +1651,9 @@ let report_subtyping_error ppf env tr1 txt1 tr2 ctx =
            (trace false (mis = None) "is not compatible with type")
            tr2 (explanation true mis));
       match ctx with
-      | Some ctx ->
+      | Some ctx -> (
         fprintf ppf "@,@,@[<v 2>";
-        (match ctx with
+        match ctx with
         | Generic {errorCode} -> fprintf ppf "Error: %s" errorCode
         | Primitive_coercion_target_variant_not_unboxed
             {variant_name; primitive} ->
@@ -1684,8 +1684,22 @@ let report_subtyping_error ppf env tr1 txt1 tr2 ctx =
         | Variant_configurations_mismatch
             {left_variant_name; right_variant_name; issue} ->
           print_variant_configuration_issue ppf issue ~left_variant_name
-            ~right_variant_name);
-        fprintf ppf "@]"
+            ~right_variant_name
+        | Different_type_kinds
+            {left_typename; right_typename; left_type_kind; right_type_kind} ->
+          let type_kind_to_string = function
+            | Type_abstract -> "an abstract type"
+            | Type_record _ -> "a record"
+            | Type_variant _ -> "a variant"
+            | Type_open -> "an open type"
+          in
+          fprintf ppf
+            "@ The types of @{<info>%s@} and @{<info>%s@} are different:"
+            (Path.name left_typename) (Path.name right_typename);
+          fprintf ppf "@ - @{<info>%s@} is %s" (Path.name left_typename)
+            (type_kind_to_string left_type_kind);
+          fprintf ppf "@ - @{<info>%s@} is %s" (Path.name right_typename)
+            (type_kind_to_string right_type_kind))
       | None -> ())
 
 let report_ambiguous_type_error ppf env (tp0, tp0') tpl txt1 txt2 txt3 =

tests/build_tests/super_errors/expected/variant_coercion_mismatching_types.res.expected

@@ -0,0 +1,14 @@
+
+  We've found a bug for you!
+  /.../fixtures/variant_coercion_mismatching_types.res:9:10-15
+
+   7 │ let x: x = One(true)
+   8 │ 
+   9 │ let y = (x :> y)
+  10 │ 
+
+  Type x is not a subtype of y 
+
+  The types of x and y are different:
+  - x is a variant
+  - y is a record

tests/build_tests/super_errors/fixtures/variant_coercion_mismatching_types.res

@@ -0,0 +1,9 @@
+type x = One(bool) | Two | Three | Four | Five
+type y = {
+  x: x,
+  y: int,
+}
+
+let x: x = One(true)
+
+let y = (x :> y)