unification trace: properly track universal variable renaming (#2135)

* unification trace: track univar renaming

This PR fixes an inconsistency introduced by #2047 : when an universal type variable was renamed in Printtyp, the explanation part of the error message kept the original name leading to potentially confusing error messages.

This PR fixes this inconsistency by keeping the whole type expression in the explanation part of the unification message instead of just its original name (and add a test for this behavior).

Author: Octachron

testsuite/tests/typing-poly/error_messages.ml

@@ -26,3 +26,17 @@ Line 1, characters 21-33:
 Error: The universal type variable 'a cannot be generalized:
        it escapes its scope.
 |}]
+
+
+(** Check that renaming universal type variable is properly tracked
+    in printtyp *)
+
+let f (x:<a:'a; b:'a. 'a>) (y:<a:'a;b:'a>) = x = y
+[%%expect {|
+Line 4, characters 49-50:
+4 | let f (x:<a:'a; b:'a. 'a>) (y:<a:'a;b:'a>) = x = y
+                                                     ^
+Error: This expression has type < a : 'a; b : 'a >
+       but an expression was expected of type < a : 'a; b : 'a0. 'a0 >
+       The universal variable 'a0 would escape its scope
+|}]

typing/ctype.ml

@@ -66,7 +66,9 @@ module Unification_trace = struct
 
   type 'a escape =
     | Constructor of Path.t
-    | Univ of string option
+    | Univ of type_expr
+    (* The type_expr argument of [Univ] is always a [Tunivar _],
+       we keep a [type_expr] to track renaming in {!Printtyp} *)
     | Self
     | Module_type of Path.t
     | Equation of 'a
@@ -1826,9 +1828,9 @@ let occur_univar env ty =
         true
     then
       match ty.desc with
-        Tunivar u ->
+        Tunivar _ ->
           if not (TypeSet.mem ty bound) then
-            raise Trace.(Unify [escape (Univ u)])
+            raise Trace.(Unify [escape (Univ ty)])
       | Tpoly (ty, tyl) ->
           let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in
           occur_rec bound  ty
@@ -1879,8 +1881,8 @@ let univars_escape env univar_pairs vl ty =
         Tpoly (t, tl) ->
           if List.exists (fun t -> TypeSet.mem (repr t) family) tl then ()
           else occur t
-      | Tunivar u ->
-          if TypeSet.mem t family then raise Trace.(Unify [escape(Univ u)])
+      | Tunivar _ ->
+          if TypeSet.mem t family then raise Trace.(Unify [escape(Univ t)])
       | Tconstr (_, [], _) -> ()
       | Tconstr (p, tl, _) ->
           begin try

typing/ctype.mli

@@ -29,7 +29,9 @@ module Unification_trace: sig
    (** Scope escape related errors *)
     type 'a escape =
     | Constructor of Path.t
-    | Univ of string option
+    | Univ of type_expr
+    (** The type_expr argument of [Univ] is always a [Tunivar _],
+        we keep a [type_expr] to track renaming in {!Printtyp} *)
     | Self
     | Module_type of Path.t
     | Equation of 'a

typing/printtyp.ml

@@ -1814,11 +1814,9 @@ let explain_escape intro ctx e =
     | None -> ignore
     | Some ctx ->  dprintf "@[%t@;<1 2>%a@]" intro type_expr ctx in
   match e with
-  | Trace.Univ Some u ->  Some(
-      dprintf "%t@,The universal variable '%s would escape its scope"
-        pre u)
-  | Trace.Univ None ->
-      Some(dprintf "%t@,An universal variable would escape its scope" pre)
+  | Trace.Univ u ->  Some(
+      dprintf "%t@,The universal variable %a would escape its scope"
+        pre type_expr u)
   | Trace.Constructor p -> Some(
       dprintf
         "%t@,@[The type constructor@;<1 2>%a@ would escape its scope@]"