make Printtyp.type_expr safer to use

testsuite/tests/typing-misc/printing.ml

@@ -51,3 +51,37 @@ type (+' a', -' a'b, 'cd') t = ' a'b -> ' a'  * 'cd';;
 [%%expect{|
 type (' a', ' a'b, 'cd') t = ' a'b -> ' a' * 'cd'
 |}];;
+
+
+(* #8856: cycles in types expressions could trigger stack overflows
+   when printing subpart of error messages *)
+type ('a,'b) eq = Refl: ('a,'a) eq
+type t = <m : int * 't> as 't
+let f (x:t) (type a) (y:a) (witness:(a,t) eq) = match witness with
+  | Refl -> if true then x else y
+[%%expect {|
+type ('a, 'b) eq = Refl : ('a, 'a) eq
+type t = < m : int * 'a > as 'a
+Line 4, characters 32-33:
+4 |   | Refl -> if true then x else y
+                                    ^
+Error: This expression has type a but an expression was expected of type t
+       This instance of < m : int * 'a > as 'a is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+
+type t1 = <m : 'b. 'b * ('b * <m:'c. 'c * 'bar> as 'bar)>
+type t2 = <m : 'a. 'a * ('a * 'foo)> as 'foo
+let f (x : t1) : t2 = x;;
+[%%expect {|
+type t1 = < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) >
+type t2 = < m : 'a. 'a * ('a * 'b) > as 'b
+Line 3, characters 22-23:
+3 | let f (x : t1) : t2 = x;;
+                          ^
+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. 'd >) as 'd
+       The universal variable 'a would escape its scope
+|}]

testsuite/tests/typing-poly/poly.ml

@@ -1110,7 +1110,7 @@ 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 * 'd, but the expected method type was
-       'c. 'c * 'd
+       'c. 'c * 'd as 'e
        The universal variable 'a would escape its scope
 |}];;
 

typing/printtyp.ml

@@ -1097,7 +1097,12 @@ and tree_of_typfields sch rest = function
 let typexp sch ppf ty =
   !Oprint.out_type ppf (tree_of_typexp sch ty)
 
-let type_expr ppf ty = typexp false 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 stackoverflow *)
+  reset_loop_marks ();
+  mark_loops ty;
+  typexp false ppf ty
 
 and type_sch ppf ty = typexp true ppf ty
 
@@ -2012,7 +2017,6 @@ let explanation intro prev env = function
   | Trace.Variant v -> explain_variant v
   | Trace.Obj o -> explain_object o
   | Trace.Rec_occur(x,y) ->
-      mark_loops y;
       Some(dprintf "@,@[<hov>The type variable %a occurs inside@ %a@]"
             type_expr x type_expr y)