Merge pull request #12974 from gasche/stray_try_expand_once

typing: fix a try_expand_once forgotten from #10170
(cherry picked from commit 166c91f)

Changes

@@ -39,6 +39,10 @@ OCaml 4.14 maintenance version
 - #12878: fix incorrect treatment of injectivity for private recursive types.
   (Jeremy Yallop, review by Gabriel Scherer and Jacques Garrigue)
 
+- #12971, #12974: fix an uncaught Ctype.Escape exception on some
+  invalid programs forming recursive types.
+  (Gabriel Scherer, review by Florian Angeletti, report by Neven Villani)
+
 - #12264, #12289: Fix compact_allocate to avoid a pathological case
   that causes very slow compaction.
   (Damien Doligez, report by Arseniy Alekseyev, review by Sadiq Jaffer)

testsuite/tests/typing-misc/occur_check.ml

@@ -15,6 +15,7 @@ Error: This expression has type 'a list
        but an expression was expected of type 'a t = 'a
        The type variable 'a occurs inside 'a list
 |}];;
+
 let f (g : 'a * 'b -> 'a t -> 'a) s = g s s;;
 [%%expect{|
 Line 1, characters 42-43:
@@ -24,3 +25,68 @@ Error: This expression has type 'a * 'b
        but an expression was expected of type 'a t = 'a
        The type variable 'a occurs inside 'a * 'b
 |}];;
+
+(* #12971 *)
+
+module Seq : sig
+  type 'a t = unit -> 'a node
+  and 'a node
+
+  val empty : 'a t
+  val cons : 'a -> 'a t -> 'a t
+end = struct
+  type 'a t = unit -> 'a node
+  and 'a node = unit
+
+  let empty () = ()
+  let cons x xs () = ()
+end;;
+[%%expect{|
+module Seq :
+  sig
+    type 'a t = unit -> 'a node
+    and 'a node
+    val empty : 'a t
+    val cons : 'a -> 'a t -> 'a t
+  end
+|}];;
+
+type 'a t = T of 'a;;
+let wrong_to_seq (xt : 'a t) : 'a Seq.t =
+  let T x = xt in
+  Seq.cons Seq.empty x
+;;
+(* Note: the current behavior of this function is believed to be
+   a bug, in the sense that it creates an equi-recursive type even in
+   absence of the -rectypes flag. On the other hand, it does not fail
+   with the Ctype.Escape exception, as it did from 4.13 to 5.1. *)
+[%%expect{|
+type 'a t = T of 'a
+Lines 3-4, characters 2-22:
+3 | ..let T x = xt in
+4 |   Seq.cons Seq.empty x
+Error: This expression has type ('a Seq.t as 'a) Seq.t Seq.t
+       but an expression was expected of type 'b
+       The type variable 'b occurs inside ('a Seq.t as 'a) Seq.t Seq.t
+|}, Principal{|
+type 'a t = T of 'a
+Lines 2-4, characters 29-22:
+2 | .............................: 'a Seq.t =
+3 |   let T x = xt in
+4 |   Seq.cons Seq.empty x
+Error: This expression has type ('a Seq.t as 'a) Seq.t Seq.t
+       but an expression was expected of type 'b
+       The type variable 'b occurs inside ('a Seq.t as 'a) Seq.t Seq.t
+|}];;
+
+let strange x = Seq.[cons x empty; cons empty x];;
+[%%expect{|
+val strange : ('a Seq.t as 'a) Seq.t -> 'a Seq.t Seq.t list = <fun>
+|}, Principal{|
+Line 1, characters 16-48:
+1 | let strange x = Seq.[cons x empty; cons empty x];;
+                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This expression has type ('a Seq.t as 'a) Seq.t Seq.t list
+       but an expression was expected of type 'b
+       The type variable 'b occurs inside ('a Seq.t as 'a) Seq.t Seq.t list
+|}];;

typing/ctype.ml

@@ -1746,7 +1746,7 @@ let rec occur_rec env allow_recursive visited ty0 ty =
         let visited = TypeSet.add ty visited in
         iter_type_expr (occur_rec env allow_recursive visited ty0) ty
       with Occur -> try
-        let ty' = try_expand_head try_expand_once env ty in
+        let ty' = try_expand_head try_expand_safe env ty in
         (* This call used to be inlined, but there seems no reason for it.
            Message was referring to change in rev. 1.58 of the CVS repo. *)
         occur_rec env allow_recursive visited ty0 ty'