Improve type variable name generation and recursive type detection wh…

…en 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.

Changes

@@ -170,6 +170,12 @@ Working version
   (Armaël Guéneau, review by Gabriel Scherer,
    split off from #9118 by Kate Deplaix, report by Ricardo M. Correia)
 
+- #10488: Improve type variable name generation and recursive type detection
+  when printing type errors; this ensures that the names given to type variables
+  are always reused in the following portion of the trace and also removes
+  spurious `as 'a`s in types.
+  (Antal Spector-Zabusky, review by Florian Angeletti)
+
 ### Internal/compiler-libs changes:
 
 - #1599: add unset directive to ocamltest to clear environment variables before

ocamldoc/.depend

@@ -280,15 +280,13 @@ odoc_dot.cmx : \
     odoc_info.cmx
 odoc_env.cmo : \
     ../typing/types.cmi \
-    ../typing/printtyp.cmi \
     ../typing/predef.cmi \
     ../typing/path.cmi \
     odoc_name.cmi \
     ../typing/btype.cmi \
     odoc_env.cmi
 odoc_env.cmx : \
     ../typing/types.cmx \
-    ../typing/printtyp.cmx \
     ../typing/predef.cmx \
     ../typing/path.cmx \
     odoc_name.cmx \
@@ -816,15 +814,13 @@ odoc_types.cmi : \
     ../parsing/location.cmi
 odoc_value.cmo : \
     ../typing/types.cmi \
-    ../typing/printtyp.cmi \
     odoc_types.cmi \
     odoc_parameter.cmo \
     odoc_name.cmi \
     odoc_misc.cmi \
     ../parsing/asttypes.cmi
 odoc_value.cmx : \
     ../typing/types.cmx \
-    ../typing/printtyp.cmx \
     odoc_types.cmx \
     odoc_parameter.cmx \
     odoc_name.cmx \

ocamldoc/odoc_env.ml

@@ -163,7 +163,6 @@ let subst_type env t =
   print_env_types env ;
   print_newline ();
 *)
-  Printtyp.mark_loops t;
   let deja_vu = ref [] in
   let rec iter t =
     if List.memq t !deja_vu then () else begin

ocamldoc/odoc_print.ml

@@ -39,8 +39,7 @@ let (modtype_fmt, flush_modtype_fmt) = new_fmt ()
 
 
 let string_of_type_expr t =
-  Printtyp.mark_loops t;
-  Printtyp.type_scheme_max ~b_reset_names: false type_fmt t;
+  Printtyp.shared_type_scheme type_fmt t;
   flush_type_fmt ()
 
 exception Use_code of string

ocamldoc/odoc_str.ml

@@ -52,17 +52,16 @@ let raw_string_of_type_list sep type_list =
     | Types.Tsubst _ -> assert false
   in
   let print_one_type variance t =
-    Printtyp.mark_loops t;
     if need_parent t then
       (
        Format.fprintf fmt "(%s" variance;
-       Printtyp.type_scheme_max ~b_reset_names: false fmt t;
+       Printtyp.shared_type_scheme fmt t;
        Format.fprintf fmt ")"
       )
     else
       (
        Format.fprintf fmt "%s" variance;
-       Printtyp.type_scheme_max ~b_reset_names: false fmt t
+       Printtyp.shared_type_scheme fmt t
       )
   in
   begin match type_list with

ocamldoc/odoc_value.ml

@@ -99,7 +99,6 @@ let parameter_list_from_arrows typ =
    parameter names from the .ml and the type from the .mli file. *)
 let dummy_parameter_list typ =
   let normal_name = Odoc_misc.label_name in
-  Printtyp.mark_loops typ;
   let liste_param = parameter_list_from_arrows typ in
   let rec iter (label, t) =
     match Types.get_desc t with

testsuite/tests/typing-gadts/pr5689.ml

@@ -103,10 +103,10 @@ type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2
 Line 7, characters 35-43:
 7 |     | (Kind _, Ast_Text txt)    -> Text txt
                                        ^^^^^^^^
-Error: This expression has type ([< inkind > `Nonlink ] as 'a) inline_t
+Error: This expression has type [< inkind > `Nonlink ] inline_t
        but an expression was expected of type a inline_t
-       Type 'a = [< `Link | `Nonlink > `Nonlink ] is not compatible with type
-         a = [< `Link | `Nonlink ]
+       Type [< inkind > `Nonlink ] = [< `Link | `Nonlink > `Nonlink ]
+       is not compatible with type a = [< `Link | `Nonlink ]
        The second variant type is bound to $'a,
        it may not allow the tag(s) `Nonlink
 |}];;

testsuite/tests/typing-gadts/pr5948.ml

@@ -42,9 +42,9 @@ type _ wrapPoly =
 Line 25, characters 23-27:
 25 |     | WrapPoly ATag -> intA
                             ^^^^
-Error: This expression has type ([< `TagA of 'b ] as 'a) -> 'b
+Error: This expression has type [< `TagA of 'a ] -> 'a
        but an expression was expected of type a -> int
-       Type [< `TagA of 'b ] as 'a is not compatible with type
+       Type [< `TagA of 'a ] is not compatible with type
          a = [< `TagA of int | `TagB ]
        The first variant type does not allow tag(s) `TagB
 |}];;

testsuite/tests/typing-misc/pr7103.ml

@@ -24,8 +24,8 @@ Line 1, characters 27-28:
 1 | let _ = fun (x : a t) -> f x;;
                                ^
 Error: This expression has type a t but an expression was expected of type
-         (< .. > as 'a) t
-       Type a is not compatible with type < .. > as 'a
+         < .. > t
+       Type a is not compatible with type < .. >
 |}];;
 
 let _ = fun (x : a t) -> g x;;
@@ -34,8 +34,8 @@ Line 1, characters 27-28:
 1 | let _ = fun (x : a t) -> g x;;
                                ^
 Error: This expression has type a t but an expression was expected of type
-         ([< `b ] as 'a) t
-       Type a is not compatible with type [< `b ] as 'a
+         [< `b ] t
+       Type a is not compatible with type [< `b ]
 |}];;
 
 let _ = fun (x : a t) -> h x;;
@@ -44,6 +44,6 @@ Line 1, characters 27-28:
 1 | let _ = fun (x : a t) -> h x;;
                                ^
 Error: This expression has type a t but an expression was expected of type
-         ([> `b ] as 'a) t
-       Type a is not compatible with type [> `b ] as 'a
+         [> `b ] t
+       Type a is not compatible with type [> `b ]
 |}];;

testsuite/tests/typing-misc/pr7668_bad.ml

@@ -91,9 +91,9 @@ Error: Signature mismatch:
          val a : t -> t
        The type
          [ `A of int | `B of [ `BA | `BB of unit list ] | `C of unit ] ->
-         ([> `B of [> `BA | `BB of int list ] | `C of unit ] as 'a)
+         [> `B of [> `BA | `BB of int list ] | `C of unit ]
        is not compatible with the type t -> t
-       Type [> `B of [> `BA | `BB of int list ] | `C of unit ] as 'a
+       Type [> `B of [> `BA | `BB of int list ] | `C of unit ]
        is not compatible with type
          t = [ `A of int | `B of [ `BA | `BB of unit list ] | `C of unit ]
        Types for tag `BB are incompatible

testsuite/tests/typing-misc/printing.ml

@@ -96,7 +96,7 @@ Line 3, characters 22-23:
                           ^
 Error: This expression has type t1 but an expression was expected of type t2
        The method m has type 'c. 'c * ('a * < m : 'c. 'b >) as 'b,
-       but the expected method type was 'a. 'a * ('a * < m : 'a. 'b >) as 'b
+       but the expected method type was 'a. 'a * ('a * < m : 'a. 'd >) as 'd
        The universal variable 'a would escape its scope
 |}]
 

testsuite/tests/typing-modules/inclusion_errors.ml

@@ -97,8 +97,8 @@ Error: Signature mismatch:
          type t = < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) >
        The type < m : 'a. 'a * ('a * 'd) > as 'd is not equal to the type
          < m : 'b. 'b * ('b * < m : 'c. 'c * 'e > as 'e) >
-       The method m has type 'a. 'a * ('a * < m : 'a. 'b >) as 'b,
-       but the expected method type was 'c. 'c * ('b * < m : 'c. 'a >) as 'a
+       The method m has type 'a. 'a * ('a * < m : 'a. 'f >) as 'f,
+       but the expected method type was 'c. 'c * ('b * < m : 'c. 'g >) as 'g
        The universal variable 'b would escape its scope
 |}];;
 
@@ -586,8 +586,8 @@ Error: Signature mismatch:
        The type (< m : 'a. 'a * 'd > as 'd) -> unit
        is not compatible with the type
          < m : 'b. 'b * < m : 'c. 'c * 'e > as 'e > -> unit
-       The method m has type 'a. 'a * < m : 'a. 'b > as 'b,
-       but the expected method type was 'c. 'c * ('b * < m : 'c. 'a >) as 'a
+       The method m has type 'a. 'a * < m : 'a. 'f > as 'f,
+       but the expected method type was 'c. 'c * ('b * < m : 'c. 'g >) as 'g
        The universal variable 'b would escape its scope
 |}];;
 

testsuite/tests/typing-objects-bugs/pr4018_bad.compilers.reference

@@ -3,18 +3,20 @@ File "pr4018_bad.ml", line 42, characters 11-17:
                 ^^^^^^
 Error: This type entity = < destroy_subject : id subject; entity_id : id >
        should be an instance of type
-         < destroy_subject : < add_observer : 'a entity_container -> 'c; .. >
-                             as 'b;
+         < destroy_subject : < add_observer : 'a entity_container -> 'b; .. >;
            .. >
          as 'a
        Type
          id subject =
            < add_observer : (id subject, id) observer -> unit;
              notify_observers : id -> unit >
        is not compatible with type
-         < add_observer : 'a entity_container -> 'c; .. > as 'b 
+         < add_observer : < destroy_subject : 'c; .. > entity_container -> 'b;
+           .. >
+         as 'c 
        Type (id subject, id) observer = < notify : id subject -> id -> unit >
        is not compatible with type
-         'a entity_container =
-           < add_entity : 'a -> 'c; notify : 'a -> id -> unit > 
+         (< destroy_subject : < add_observer : 'd -> 'b; .. >; .. > as 'a)
+         entity_container as 'd =
+           < add_entity : 'a -> 'b; notify : 'a -> id -> unit > 
        Types for method add_observer are incompatible

testsuite/tests/typing-objects/Exemples.ml

@@ -588,7 +588,8 @@ Error: This expression has type
        but an expression was expected of type
          #comparable as 'a = < cmp : 'a -> int; .. >
        Type int_comparable = < cmp : int_comparable -> int; x : int >
-       is not compatible with type 'a = < cmp : 'a -> int; .. >
+       is not compatible with type
+         #comparable as 'a = < cmp : 'a -> int; .. >
        The first object type has no method setx
 |}];;   (* Error; strange message with -principal *)
 

testsuite/tests/typing-objects/Tests.ml

@@ -699,10 +699,9 @@ Error: Signature mismatch:
          val f : (#c as 'a) -> 'a
        is not included in
          val f : #c -> #c
-       The type (#c as 'a) -> 'a is not compatible with the type
-         'a -> (#c as 'b)
-       Type 'a = < m : 'a; .. > is not compatible with type
-         'b = < m : 'b; .. >
+       The type (#c as 'a) -> 'a is not compatible with the type #c -> #c
+       Type #c as 'a = < m : 'a; .. > is not compatible with type
+         #c as 'b = < m : 'b; .. >
        Type 'a is not compatible with type 'b
 |}];;
 
@@ -1013,12 +1012,12 @@ Lines 3-5, characters 8-3:
 3 | ........object (self)
 4 |   method m = self
 5 | end..
-Error: The class type object ('a) method m : 'a end
+Error: The class type object ('a) method m : < m : 'a; .. > as 'a end
        is not matched by the class type
          object method m : < m : 'a > as 'a end
        The method m has type < m : 'a; .. > as 'a
        but is expected to have type < m : 'b > as 'b
-       Type 'a is not compatible with type <  > as 'b
+       Type 'a is not compatible with type <  >
 |}];;
 
 class c :
@@ -1071,7 +1070,8 @@ class c : object('self) method m : < m : 'a; x : int; ..> -> unit as 'a end =
 Line 2, characters 4-52:
 2 |     object (_ : 'self) method m (_ : 'self) = () end;;
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The class type object ('a) method m : 'a -> unit end
+Error: The class type
+         object ('a) method m : (< m : 'a -> unit; .. > as 'a) -> unit end
        is not matched by the class type
          object method m : < m : 'a; x : int; .. > -> unit as 'a end
        The method m has type (< m : 'a -> unit; .. > as 'a) -> unit

testsuite/tests/typing-objects/dummy.ml

@@ -196,9 +196,9 @@ Line 3, characters 36-41:
 Error: This expression has type
          < redrawWidget : parameter_contains_self -> unit; .. >
        but an expression was expected of type
-         < redrawWidget : (< invalidate : unit; .. > as 'a) -> unit; .. >
+         < redrawWidget : < invalidate : unit; .. > -> unit; .. >
        Type parameter_contains_self = < invalidate : unit >
-       is not compatible with type < invalidate : unit; .. > as 'a
+       is not compatible with type < invalidate : unit; .. >
        Self type cannot be unified with a closed object type
 |}]
 
@@ -212,9 +212,9 @@ Line 3, characters 26-31:
 Error: This expression has type
          < redrawWidget : parameter_contains_self -> unit; .. >
        but an expression was expected of type
-         < redrawWidget : (< invalidate : unit; .. > as 'a) -> unit; .. >
+         < redrawWidget : < invalidate : unit; .. > -> unit; .. >
        Type parameter_contains_self = < invalidate : unit >
-       is not compatible with type < invalidate : unit; .. > as 'a
+       is not compatible with type < invalidate : unit; .. >
        Self type cannot be unified with a closed object type
 |}]
 
@@ -259,9 +259,9 @@ Line 3, characters 36-41:
 Error: This expression has type
          < redrawWidget : parameter_contains_self -> unit; .. >
        but an expression was expected of type
-         < redrawWidget : (< invalidate : unit; .. > as 'a) -> unit; .. >
+         < redrawWidget : < invalidate : unit; .. > -> unit; .. >
        Type parameter_contains_self = < invalidate : unit >
-       is not compatible with type < invalidate : unit; .. > as 'a
+       is not compatible with type < invalidate : unit; .. >
        Self type cannot be unified with a closed object type
 |}]
 

testsuite/tests/typing-poly/error_messages.ml

@@ -38,8 +38,8 @@ Line 4, characters 49-50:
                                                      ^
 Error: This expression has type < a : 'a; b : 'a >
        but an expression was expected of type < a : 'a; b : 'a0. 'a0 >
-       The method b has type 'a, but the expected method type was 'a. 'a
-       The universal variable 'a would escape its scope
+       The method b has type 'a, but the expected method type was 'a0. 'a0
+       The universal variable 'a0 would escape its scope
 |}]
 
 
@@ -58,9 +58,9 @@ Lines 5-7, characters 10-5:
 5 | ..........(object
 6 |     method f _ = 0
 7 |  end)..
-Error: This expression has type < f : 'a -> int >
+Error: This expression has type < f : 'b -> int >
        but an expression was expected of type t_a
-       The method f has type 'a -> int, but the expected method type was
+       The method f has type 'b -> int, but the expected method type was
        'a. 'a -> int
        The universal variable 'a would escape its scope
 |}
@@ -77,9 +77,9 @@ val f : uv -> int = <fun>
 Line 4, characters 11-49:
 4 | let () = f ( `A (object method f _ = 0 end): _ v);;
                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This expression has type 'a v but an expression was expected of type
+Error: This expression has type 'b v but an expression was expected of type
          uv
-       The method f has type 'a -> int, but the expected method type was
+       The method f has type 'b -> int, but the expected method type was
        'a. 'a -> int
        The universal variable 'a would escape its scope
 |}]

testsuite/tests/typing-poly/poly.ml

@@ -1129,9 +1129,9 @@ Error: This expression has type < m : 'a. 'a * < m : 'a * 'b > > as 'b
        but an expression was expected of type
          < m : 'a. 'a * (< m : 'a * < m : 'c. 'c * 'd > > as 'd) >
        The method m has type
-       'a. 'a * (< m : 'a * < m : 'c. 'c * 'b > > as 'b),
+       'a. 'a * (< m : 'a * < m : 'c. 'c * 'd > > as 'd),
        but the expected method type was
-       'c. 'c * < m : 'a * < m : 'c. 'b > > as 'b
+       'c. 'c * < m : 'a * < m : 'c. 'e > > as 'e
        The universal variable 'a would escape its scope
 |}];;
 
@@ -1179,8 +1179,8 @@ Error: Signature mismatch:
        The type (< m : 'a. 'a * ('a * 'd) > as 'd) -> unit
        is not compatible with the type
          < m : 'b. 'b * ('b * < m : 'c. 'c * 'e > as 'e) > -> unit
-       The method m has type 'a. 'a * ('a * < m : 'a. 'b >) as 'b,
-       but the expected method type was 'c. 'c * ('b * < m : 'c. 'a >) as 'a
+       The method m has type 'a. 'a * ('a * < m : 'a. 'f >) as 'f,
+       but the expected method type was 'c. 'c * ('b * < m : 'c. 'g >) as 'g
        The universal variable 'b would escape its scope
 |}];;
 
@@ -1254,8 +1254,7 @@ Lines 2-3, characters 2-47:
 3 |     :> <m:'b. (<p:int;q:int;..> as 'b) -> int>)..
 Error: Type < m : 'a. (< p : int; .. > as 'a) -> int > is not a subtype of
          < m : 'b. (< p : int; q : int; .. > as 'b) -> int >
-       Type < p : int; q : int; .. > as 'c is not a subtype of
-         < p : int; .. > as 'd
+       Type < p : int; q : int; .. > is not a subtype of < p : int; .. >
 |}];;
 
 (* Keep sharing the epsilons *)
@@ -1886,7 +1885,7 @@ Line 1, characters 17-18:
                      ^
 Error: This expression has type u but an expression was expected of type v
        The method m has type 'a s list * < m : 'b > as 'b,
-       but the expected method type was 'a. 'a s list * < m : 'a. 'b > as 'b
+       but the expected method type was 'a. 'a s list * < m : 'a. 'c > as 'c
        The universal variable 'a would escape its scope
 |}]
 

testsuite/tests/typing-polyvariants-bugs/pr7817_bad.ml

@@ -26,9 +26,8 @@ Error: Signature mismatch:
          val write : _[< `A of '_weak2 | `B of '_weak3 ] -> unit
        is not included in
          val write : [< `A of string | `B of int ] -> unit
-       The type (_[< `A of '_weak2 | `B of '_weak3 ] as 'a) -> unit
-       is not compatible with the type
-         ([< `A of string | `B of int ] as 'b) -> unit
-       Type _[< `A of '_weak2 | `B of '_weak3 ] as 'a
-       is not compatible with type [< `A of string | `B of int ] as 'b
+       The type _[< `A of '_weak2 | `B of '_weak3 ] -> unit
+       is not compatible with the type [< `A of string | `B of int ] -> unit
+       Type _[< `A of '_weak2 | `B of '_weak3 ] is not compatible with type
+         [< `A of string | `B of int ]
 |}]