Improve type variable name generation and recursive type detection when printing type errors (#10488)

* Separate type variable naming and loop marking when printing errors

Improve type variable name generation and recursive type detection
when printing type errors by

1. Iterating over the whole trace and reserving type variable names
   once, to ensure that type variable names aren't reused in confusing
   ways between types.

2. Detecting recursive types (i.e., marking loops) for each type
   individually during printing, ensuring that spurious `as 'a`
   clauses aren't generated and that `as`-bound names can't be
   referred to across different types.

This involved updating the `Printtyp` module: first refactoring
`mark_loops_rec` into a general case analysis
`iter_type_expr_for_printing`, and then implementing both
`reserve_names` and `mark_loops` in terms of it (via
`Names.add_named_vars` and a new `mark_loops_rec` that only handles
marking loops and not generating names).

As a result, the API for printing types also changed:

* `type_expr` still does what it always did.

* To handle multiple types simultaneously, use `prepare_for_printing`
  and `prepared_type_expr` (replacing `marked_type_expr` and the
  associated marking facilities).

* Within `Printtyp`, we use `named_type_expr`, which is in-between the
  other formatters and assumes names have been generated but does its
  own loop marking.

1 files changed, 188 insertions, 134 deletions

diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 9b0d227304..3203c80903 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -780,6 +780,8 @@ let best_type_path p =
 
 (* Print a type expression *)
 
+let proxy ty = Transient_expr.repr (proxy ty)
+
 (* When printing a type scheme, we print weak names.  When printing a plain
    type, we do not.  This type controls that behavior *)
 type type_or_scheme = Type | Type_scheme
@@ -789,14 +791,56 @@ let is_non_gen mode ty =
   | Type_scheme -> is_Tvar ty && get_level ty <> generic_level
   | Type        -> false
 
+let nameable_row row =
+  row_name row <> None &&
+  List.for_all
+    (fun (_, f) ->
+       match row_field_repr f with
+       | Reither(c, l, _, _) ->
+           row_closed row && if c then l = [] else List.length l = 1
+       | _ -> true)
+    (row_fields row)
+
+(* This specialized version of [Btype.iter_type_expr] normalizes and
+   short-circuits the traversal of the [type_expr], so that it covers only the
+   subterms that would be printed by the type printer. *)
+let printer_iter_type_expr f ty =
+  match get_desc ty with
+  | Tconstr(p, tyl, _) ->
+      let (_p', s) = best_type_path p in
+      List.iter f (apply_subst s tyl)
+  | Tvariant row -> begin
+      match row_name row with
+      | Some(_p, tyl) when nameable_row row ->
+          List.iter f tyl
+      | _ ->
+          iter_row f row
+    end
+  | Tobject (fi, nm) -> begin
+      match !nm with
+      | None ->
+          let fields, _ = flatten_fields fi in
+          List.iter
+            (fun (_, kind, ty) ->
+               if field_kind_repr kind = Fpresent then
+                 f ty)
+            fields
+      | Some (_, l) ->
+          List.iter f (List.tl l)
+    end
+  | Tfield(_, kind, ty1, ty2) ->
+      if field_kind_repr kind = Fpresent then
+        f ty1;
+      f ty2
+  | _ ->
+      Btype.iter_type_expr f ty
+
 module Names : sig
   val reset_names : unit -> unit
 
-  val add_named_var : transient_expr -> unit
+  val add_named_vars : type_expr -> unit
   val add_subst : (type_expr * type_expr) list -> unit
 
-  val has_name : transient_expr -> bool
-
   val new_name : unit -> string
   val new_weak_name : type_expr -> unit -> string
 
@@ -819,21 +863,38 @@ end = struct
   let name_subst = ref ([] : (transient_expr * transient_expr) list)
   let name_counter = ref 0
   let named_vars = ref ([] : string list)
+  let visited_for_named_vars = ref ([] : transient_expr list)
 
   let weak_counter = ref 1
   let weak_var_map = ref TypeMap.empty
   let named_weak_vars = ref String.Set.empty
 
   let reset_names () =
-    names := []; name_subst := []; name_counter := 0; named_vars := []
+    names := [];
+    name_subst := [];
+    name_counter := 0;
+    named_vars := [];
+    visited_for_named_vars := []
 
-  let add_named_var ty =
-    match ty.desc with
+  let add_named_var tty =
+    match tty.desc with
       Tvar (Some name) | Tunivar (Some name) ->
         if List.mem name !named_vars then () else
         named_vars := name :: !named_vars
     | _ -> ()
 
+  let rec add_named_vars ty =
+    let tty = Transient_expr.repr ty in
+    let px = proxy ty in
+    if not (List.memq px !visited_for_named_vars) then begin
+      visited_for_named_vars := px :: !visited_for_named_vars;
+      match tty.desc with
+      | Tvar _ | Tunivar _ ->
+          add_named_var tty
+      | _ ->
+          printer_iter_type_expr add_named_vars ty
+    end
+
   let rec substitute ty =
     match List.assq ty !name_subst with
     | ty' -> substitute ty'
@@ -845,9 +906,6 @@ end = struct
         subst
       @ !name_subst
 
-  let has_name ty =
-    List.mem_assq (substitute ty) !names
-
   let name_is_already_used name =
     List.mem name !named_vars
     || List.exists (fun (_, name') -> name = name') !names
@@ -933,24 +991,36 @@ end = struct
     weak_var_map := m
 end
 
+let reserve_names ty =
+  normalize_type ty;
+  Names.add_named_vars ty
+
 let visited_objects = ref ([] : transient_expr list)
 let aliased = ref ([] : transient_expr list)
 let delayed = ref ([] : transient_expr list)
+let printed_aliases = ref ([] : transient_expr list)
+
+(* [printed_aliases] is a subset of [aliased] that records only those aliased
+   types that have actually been printed; this allows us to avoid naming loops
+   that the user will never see. *)
 
 let add_delayed t =
   if not (List.memq t !delayed) then delayed := t :: !delayed
 
-let proxy ty = Transient_expr.repr (proxy ty)
+let is_aliased_proxy px = List.memq px !aliased
 
-let is_aliased_proxy px =
-  List.memq px !aliased
 let add_alias_proxy px =
-  if not (List.memq px !aliased) then begin
-    aliased := px :: !aliased;
-    Names.add_named_var px
-  end
+  if not (is_aliased_proxy px) then
+    aliased := px :: !aliased
+
 let add_alias ty = add_alias_proxy (proxy ty)
 
+let add_printed_alias_proxy px =
+  Names.check_name_of_type px;
+  printed_aliases := px :: !printed_aliases
+
+let add_printed_alias ty = add_printed_alias_proxy (proxy ty)
+
 let aliasable ty =
   match get_desc ty with
     Tvar _ | Tunivar _ | Tpoly _ -> false
@@ -958,77 +1028,39 @@ let aliasable ty =
       not (is_nth (snd (best_type_path p)))
   | _ -> true
 
-let namable_row row =
-  row_name row <> None &&
-  List.for_all
-    (fun (_, f) ->
-       match row_field_repr f with
-       | Reither(c, l, _, _) ->
-           row_closed row && if c then l = [] else List.length l = 1
-       | _ -> true)
-    (row_fields row)
+let should_visit_object ty =
+  match get_desc ty with
+  | Tvariant row -> not (static_row row)
+  | Tobject _ -> opened_object ty
+  | _ -> false
 
 let rec mark_loops_rec visited ty =
   let px = proxy ty in
   if List.memq px visited && aliasable ty then add_alias_proxy px else
-    let visited = px :: visited in
     let tty = Transient_expr.repr ty in
+    let visited = px :: visited in
     match tty.desc with
-    | Tvar _ -> Names.add_named_var tty
-    | Tarrow(_, ty1, ty2, _) ->
-        mark_loops_rec visited ty1; mark_loops_rec visited ty2
-    | Ttuple tyl -> List.iter (mark_loops_rec visited) tyl
-    | Tconstr(p, tyl, _) ->
-        let (_p', s) = best_type_path p in
-        List.iter (mark_loops_rec visited) (apply_subst s tyl)
-    | Tpackage (_, fl) ->
-        List.iter (fun (_n, ty) -> mark_loops_rec visited ty) fl
-    | Tvariant row ->
-        if List.memq px !visited_objects then add_alias_proxy px else
-         begin
-          if not (static_row row) then
+    | Tvariant _ | Tobject _ ->
+        if List.memq px !visited_objects then add_alias_proxy px else begin
+          if should_visit_object ty then
             visited_objects := px :: !visited_objects;
-          match row_name row with
-          | Some(_p, tyl) when namable_row row ->
-              List.iter (mark_loops_rec visited) tyl
-          | _ ->
-              iter_row (mark_loops_rec visited) row
-         end
-    | Tobject (fi, nm) ->
-        if List.memq px !visited_objects then add_alias_proxy px else
-         begin
-          if opened_object ty then
-            visited_objects := px :: !visited_objects;
-          begin match !nm with
-          | None ->
-              let fields, _ = flatten_fields fi in
-              List.iter
-                (fun (_, kind, ty) ->
-                  if field_kind_repr kind = Fpresent then
-                    mark_loops_rec visited ty)
-                fields
-          | Some (_, l) ->
-              List.iter (mark_loops_rec visited) (List.tl l)
-          end
+          printer_iter_type_expr (mark_loops_rec visited) ty
         end
-    | Tfield(_, kind, ty1, ty2) when field_kind_repr kind = Fpresent ->
-        mark_loops_rec visited ty1; mark_loops_rec visited ty2
-    | Tfield(_, _, _, ty2) ->
-        mark_loops_rec visited ty2
-    | Tnil -> ()
-    | Tsubst _ -> ()  (* we do not print arguments *)
-    | Tlink _ -> fatal_error "Printtyp.mark_loops_rec (2)"
-    | Tpoly (ty, tyl) ->
-        List.iter (fun t -> add_alias t) tyl;
+    | Tpoly(ty, tyl) ->
+        List.iter add_alias tyl;
         mark_loops_rec visited ty
-    | Tunivar _ -> Names.add_named_var tty
+    | _ ->
+        printer_iter_type_expr (mark_loops_rec visited) ty
 
 let mark_loops ty =
-  normalize_type ty;
   mark_loops_rec [] ty;;
 
+let prepare_type ty =
+  reserve_names ty;
+  mark_loops ty;;
+
 let reset_loop_marks () =
-  visited_objects := []; aliased := []; delayed := []
+  visited_objects := []; aliased := []; delayed := []; printed_aliases := []
 
 let reset_except_context () =
   Names.reset_names (); reset_loop_marks ()
@@ -1037,18 +1069,15 @@ let reset () =
   reset_naming_context (); Conflicts.reset ();
   reset_except_context ()
 
-let reset_and_mark_loops ty =
-  reset_except_context (); mark_loops ty
-
-let reset_and_mark_loops_list tyl =
-  reset_except_context (); List.iter mark_loops tyl
+let prepare_for_printing tyl =
+  reset_except_context (); List.iter prepare_type tyl
 
 (* Disabled in classic mode when printing an unification error *)
 let print_labels = ref true
 
 let rec tree_of_typexp mode ty =
   let px = proxy ty in
-  if Names.has_name px && not (List.memq px !delayed) then
+  if List.memq px !printed_aliases && not (List.memq px !delayed) then
    let mark = is_non_gen mode ty in
    let name = Names.name_of_type
                 (if mark then Names.new_weak_name ty else Names.new_name)
@@ -1102,7 +1131,7 @@ let rec tree_of_typexp mode ty =
             fields in
         let all_present = List.length present = List.length fields in
         begin match name with
-        | Some(p, tyl) when namable_row row ->
+        | Some(p, tyl) when nameable_row row ->
             let (p', s) = best_type_path p in
             let id = tree_of_path Type p' in
             let args = tree_of_typlist mode (apply_subst s tyl) in
@@ -1164,7 +1193,7 @@ let rec tree_of_typexp mode ty =
   in
   if List.memq px !delayed then delayed := List.filter ((!=) px) !delayed;
   if is_aliased_proxy px && aliasable ty then begin
-    Names.check_name_of_type px;
+    add_printed_alias_proxy px;
     Otyp_alias (pr_typ (), Names.name_of_type Names.new_name px) end
   else pr_typ ()
 
@@ -1227,17 +1256,28 @@ and tree_of_typfields mode rest = function
 let typexp mode ppf ty =
   !Oprint.out_type ppf (tree_of_typexp mode ty)
 
-let marked_type_expr ppf ty = typexp Type ppf ty
+let prepared_type_expr ppf ty = typexp Type ppf ty
 
 let type_expr ppf ty =
   (* [type_expr] is used directly by error message printers,
      we mark eventual loops ourself to avoid any misuse and stack overflow *)
-  reset_and_mark_loops ty;
-  marked_type_expr ppf ty
+  prepare_for_printing [ty];
+  prepared_type_expr ppf ty
+
+(* "Half-prepared" type expression: [ty] should have had its names reserved, but
+   should not have had its loops marked. *)
+let type_expr_with_reserved_names ppf ty =
+  reset_loop_marks ();
+  mark_loops ty;
+  prepared_type_expr ppf ty
 
-and type_sch ppf ty = typexp Type_scheme ppf ty
+let shared_type_scheme ppf ty =
+  prepare_type ty;
+  typexp Type_scheme ppf ty
 
-and type_scheme ppf ty = reset_and_mark_loops ty; typexp Type_scheme ppf ty
+let type_scheme ppf ty =
+  prepare_for_printing [ty];
+  typexp Type_scheme ppf ty
 
 let type_path ppf p =
   let (p', s) = best_type_path p in
@@ -1245,14 +1285,8 @@ let type_path ppf p =
   let t = tree_of_path Type p in
   !Oprint.out_ident ppf t
 
-(* Maxence *)
-let type_scheme_max ?(b_reset_names=true) ppf ty =
-  if b_reset_names then Names.reset_names () ;
-  typexp Type_scheme ppf ty
-(* End Maxence *)
-
 let tree_of_type_scheme ty =
-  reset_and_mark_loops ty;
+  prepare_for_printing [ty];
   tree_of_typexp Type_scheme ty
 
 (* Print one type declaration *)
@@ -1281,9 +1315,9 @@ let filter_params tyl =
       [] tyl
   in List.rev params
 
-let mark_loops_constructor_arguments = function
-  | Cstr_tuple l -> List.iter mark_loops l
-  | Cstr_record l -> List.iter (fun l -> mark_loops l.ld_type) l
+let prepare_type_constructor_arguments = function
+  | Cstr_tuple l -> List.iter prepare_type l
+  | Cstr_record l -> List.iter (fun l -> prepare_type l.ld_type) l
 
 let rec tree_of_type_decl id decl =
 
@@ -1303,8 +1337,8 @@ let rec tree_of_type_decl id decl =
   end;
 
   List.iter add_alias params;
-  List.iter mark_loops params;
-  List.iter Names.check_name_of_type (List.map proxy params);
+  List.iter prepare_type params;
+  List.iter add_printed_alias params;
   let ty_manifest =
     match decl.type_manifest with
     | None -> None
@@ -1320,7 +1354,7 @@ let rec tree_of_type_decl id decl =
               end
           | _ -> ty
         in
-        mark_loops ty;
+        prepare_type ty;
         Some ty
   in
   begin match decl.type_kind with
@@ -1328,11 +1362,11 @@ let rec tree_of_type_decl id decl =
   | Type_variant (cstrs, _rep) ->
       List.iter
         (fun c ->
-           mark_loops_constructor_arguments c.cd_args;
-           Option.iter mark_loops c.cd_res)
+           prepare_type_constructor_arguments c.cd_args;
+           Option.iter prepare_type c.cd_res)
         cstrs
   | Type_record(l, _rep) ->
-      List.iter (fun l -> mark_loops l.ld_type) l
+      List.iter (fun l -> prepare_type l.ld_type) l
   | Type_open -> ()
   end;
 
@@ -1473,10 +1507,10 @@ let tree_of_extension_constructor id ext es =
   let ty_name = Path.name ext.ext_type_path in
   let ty_params = filter_params ext.ext_type_params in
   List.iter add_alias ty_params;
-  List.iter mark_loops ty_params;
-  List.iter Names.check_name_of_type (List.map proxy ty_params);
-  mark_loops_constructor_arguments ext.ext_args;
-  Option.iter mark_loops ext.ext_ret_type;
+  List.iter prepare_type ty_params;
+  List.iter add_printed_alias ty_params;
+  prepare_type_constructor_arguments ext.ext_args;
+  Option.iter prepare_type ext.ext_ret_type;
   let type_param =
     function
     | Otyp_var (_, id) -> id
@@ -1556,7 +1590,7 @@ let method_type priv ty =
 
 let prepare_method _lab (priv, _virt, ty) =
   let ty, _ = method_type priv ty in
-  mark_loops ty
+  prepare_type ty
 
 let tree_of_method mode (lab, priv, virt, ty) =
   let (ty, tyl) = method_type priv ty in
@@ -1573,16 +1607,16 @@ let rec prepare_class_type params = function
       || not (List.for_all is_Tvar params)
       || List.exists (deep_occur row) tyl
       then prepare_class_type params cty
-      else List.iter mark_loops tyl
+      else List.iter prepare_type tyl
   | Cty_signature sign ->
       (* Self may have a name *)
       let px = proxy sign.csig_self_row in
       if List.memq px !visited_objects then add_alias_proxy px
       else visited_objects := px :: !visited_objects;
-      Vars.iter (fun _ (_, _, ty) -> mark_loops ty) sign.csig_vars;
+      Vars.iter (fun _ (_, _, ty) -> prepare_type ty) sign.csig_vars;
       Meths.iter prepare_method sign.csig_meths
   | Cty_arrow (_, ty, cty) ->
-      mark_loops ty;
+      prepare_type ty;
       prepare_class_type params cty
 
 let rec tree_of_class_type mode params =
@@ -1673,10 +1707,10 @@ let tree_of_class_declaration id cl rs =
   List.iter add_alias params;
   prepare_class_type params cl.cty_type;
   let px = proxy (Btype.self_type_row cl.cty_type) in
-  List.iter mark_loops params;
+  List.iter prepare_type params;
 
-  List.iter Names.check_name_of_type (List.map proxy params);
-  if is_aliased_proxy px then Names.check_name_of_type px;
+  List.iter add_printed_alias params;
+  if is_aliased_proxy px then add_printed_alias_proxy px;
 
   let vir_flag = cl.cty_new = None in
   Osig_class
@@ -1695,10 +1729,10 @@ let tree_of_cltype_declaration id cl rs =
   List.iter add_alias params;
   prepare_class_type params cl.clty_type;
   let px = proxy (Btype.self_type_row cl.clty_type) in
-  List.iter mark_loops params;
+  List.iter prepare_type params;
 
-  List.iter Names.check_name_of_type (List.map proxy params);
-  if is_aliased_proxy px then Names.check_name_of_type px;
+  List.iter add_printed_alias params;
+  if is_aliased_proxy px then add_printed_alias_proxy px;
 
   let sign = Btype.signature_of_class_type cl.clty_type in
   let has_virtual_vars =
@@ -1986,9 +2020,12 @@ let same_path t t' =
 type 'a diff = Same of 'a | Diff of 'a * 'a
 
 let trees_of_type_expansion mode Errortrace.{ty = t; expanded = t'} =
+  reset_loop_marks ();
+  mark_loops t;
   if same_path t t'
   then begin add_delayed (proxy t); Same (tree_of_typexp mode t) end
-  else
+  else begin
+    mark_loops t';
     let t' = if proxy t == proxy t' then unalias t' else t' in
     (* beware order matter due to side effect,
        e.g. when printing object types *)
@@ -1996,6 +2033,7 @@ let trees_of_type_expansion mode Errortrace.{ty = t; expanded = t'} =
     let second = tree_of_typexp mode t' in
     if first = second then Same first
     else Diff(first,second)
+  end
 
 let type_expansion ppf = function
   | Same t -> !Oprint.out_type ppf t
@@ -2097,14 +2135,14 @@ let hide_variant_name t =
 
 let prepare_expansion Errortrace.{ty; expanded} =
   let expanded = hide_variant_name expanded in
-  mark_loops ty;
-  if not (same_path ty expanded) then mark_loops expanded;
+  reserve_names ty;
+  if not (same_path ty expanded) then reserve_names expanded;
   Errortrace.{ty; expanded}
 
 let may_prepare_expansion compact (Errortrace.{ty; expanded} as ty_exp) =
   match get_desc expanded with
     Tvariant _ | Tobject _ when compact ->
-      mark_loops ty; Errortrace.{ty; expanded = ty}
+      reserve_names ty; Errortrace.{ty; expanded = ty}
   | _ -> prepare_expansion ty_exp
 
 let print_path p = Format.dprintf "%a" !Oprint.out_ident (tree_of_path Type p)
@@ -2155,8 +2193,9 @@ let explain_fixed_row pos expl = match expl with
   | Fixed_private ->
     dprintf "The %a variant type is private" Errortrace.print_pos pos
   | Univar x ->
+    reserve_names x;
     dprintf "The %a variant type is bound to the universal type variable %a"
-      Errortrace.print_pos pos type_expr x
+      Errortrace.print_pos pos type_expr_with_reserved_names x
   | Reified p ->
     dprintf "The %a variant type is bound to %t"
       Errortrace.print_pos pos (print_path p)
@@ -2200,9 +2239,11 @@ let explain_variant (type variety) : variety Errortrace.variant -> _ = function
              Errortrace.print_pos (Errortrace.swap_position pos))
 
 let explain_escape pre = function
-  | Errortrace.Univ u -> Some(
-      dprintf "%t@,The universal variable %a would escape its scope"
-        pre type_expr u)
+  | Errortrace.Univ u ->
+      reserve_names u;
+      Some(
+        dprintf "%t@,The universal variable %a would escape its scope"
+          pre type_expr_with_reserved_names u)
   | Errortrace.Constructor p -> Some(
       dprintf
         "%t@,@[The type constructor@;<1 2>%a@ would escape its scope@]"
@@ -2213,11 +2254,13 @@ let explain_escape pre = function
         "%t@,@[The module type@;<1 2>%a@ would escape its scope@]"
         pre path p
     )
-  | Errortrace.Equation Errortrace.{ty = _; expanded = t} -> Some(
-      dprintf "%t @,@[<hov>This instance of %a is ambiguous:@ %s@]"
-        pre type_expr t
-        "it would escape the scope of its equation"
-    )
+  | Errortrace.Equation Errortrace.{ty = _; expanded = t} ->
+      reserve_names t;
+      Some(
+        dprintf "%t @,@[<hov>This instance of %a is ambiguous:@ %s@]"
+          pre type_expr_with_reserved_names t
+          "it would escape the scope of its equation"
+      )
   | Errortrace.Self ->
       Some (dprintf "%t@,Self type cannot escape its class" pre)
   | Errortrace.Constraint ->
@@ -2244,11 +2287,16 @@ let explanation (type variety) intro prev env
     let pre =
       match context, kind, prev with
       | Some ctx, _, _ ->
-        dprintf "@[%t@;<1 2>%a@]" intro type_expr ctx
+        reserve_names ctx;
+        dprintf "@[%t@;<1 2>%a@]" intro type_expr_with_reserved_names ctx
       | None, Univ _, Some(Errortrace.Incompatible_fields {name; diff}) ->
+        reserve_names diff.got;
+        reserve_names diff.expected;
         dprintf "@,@[The method %s has type@ %a,@ \
                  but the expected method type was@ %a@]"
-          name type_expr diff.got type_expr diff.expected
+          name
+          type_expr_with_reserved_names diff.got
+          type_expr_with_reserved_names diff.expected
       | _ -> ignore
     in
     explain_escape pre kind
@@ -2259,11 +2307,17 @@ let explanation (type variety) intro prev env
   | Errortrace.Obj o ->
     explain_object o
   | Errortrace.Rec_occur(x,y) ->
-    reset_and_mark_loops y;
+    reserve_names x;
+    reserve_names y;
     begin match get_desc x with
     | Tvar _ | Tunivar _  ->
-        Some(dprintf "@,@[<hov>The type variable %a occurs inside@ %a@]"
-               type_expr x type_expr y)
+        Some(fun ppf ->
+          reset_loop_marks ();
+          mark_loops x;
+          mark_loops y;
+          dprintf "@,@[<hov>The type variable %a occurs inside@ %a@]"
+            prepared_type_expr x prepared_type_expr y
+            ppf)
     | _ ->
         (* We had a delayed unification of the type variable with
            a non-variable after the occur check. *)