Incorrect annotations lead to `Fatal error: exception Ctype.Escape(_)` on 5.1.1

[Vanille-N]

Incorrect annotations lead to `Fatal error: exception Ctype.Escape(_)` on 5.1.1

[gasche]

@Octachron and myself have now fixed this issue -- the uncaught exception. The fix will be included in next release of 4.14, and in OCaml 5.2 and later releases. We found some independent issues with the same or related test cases, that have yet to be fixed.

[Vanille-N]

trace.txt

[gasche]

Nice find!

This is related to the handling of the (equi)-recursive types built by this incorrect program. The failure is reproducible starting with OCaml 4.13, but 4.12 and 4.11 (older versions don't have Seq) fail with a proper error:

File "test.ml", lines 4-5, characters 2-22:
4 | ..let T x = xt in
5 |   Seq.cons Seq.empty x
Error: This expression has type
         ('a Seq.t as 'a) Seq.t Seq.t = unit -> 'a Seq.t Seq.node
       but an expression was expected of type 'b
       Type 'c is not compatible with type 'a = unit -> 'c Seq.node 
       The type variable 'c occurs inside 'a

The program also gets accepted when -rectypes is used, including on recent versions.

val to_seq : ('a Seq.t as 'a) Seq.t t -> 'a Seq.t Seq.t

[gasche]

Testing indicates that this failure was introduced by #10170 .

[gasche]

Minimal repro case (does not rely on an external module):

type 'a t = T of 'a

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 

let to_seq (xt : 'a t) : 'a Seq.t =
  let T x = xt in
  Seq.cons Seq.empty x

[gasche]

I proposed a one-line fix in #10170 (comment) . But in fact, it looks like this error cannot be reproduced in trunk and in the 5.2 release branch, thanks to another change in 52 ( #12691 ). So in a sense it is "already fixed", even though we may still want to apply the proper one-line fix.

[Octachron]

I think I might prefer to backport the expand_gen_abbrev cleanup from #12691 to 4.14 (to have the same behavior on 4.14.2+ and 5.2+).

[gasche]

My impression is that the one-line change makes the code more consistent. I don't understand if the expand_gen_abbrev change makes all of that code inconsistent again (maybe there is no need to use the _safe variant anymore in most cases?), but I would be inclined to make all callsites look the same independently of that change -- which we could also backtrack to 4.14, even if it is noticeably more invasive.

[gasche]

I proposed my one-liner with the repro case as a PR in #12974.

[Octachron]

Further testing indicates that the rectype bug is quite old:

(* core.mli *)
type 'a pre = Nil | Cons of 'a * 'a pre
type 'a t = unit -> 'a pre
val cons: 'a -> 'a t -> 'a t
val empty: 'a t

(* main.ml *)
let cons_empty (x : 'a) : 'a Core.t = Core.(cons empty x)

has been broken since 4.01 .

[gasche]

Thanks for the report!