IIRC, polymorphic variants are just (open) sum types, which admit equi-recursion. Viz the behavior of the degenerate, one-armed polymorphic variant to "implement" iso-recursion:
# let rec m = `Fold m;;
val m : [> `Fold of 'a ] as 'a = `Fold <cycle>
# let unfold (`Fold v) = v;;
val unfold : [< `Fold of 'a ] -> 'a = <fun>
Yes, I think you are right that equi-recursion is still observable, but this may be the wrong example. I think it merely shows that OCaml’s let-rec is a more general fixpoint, but that also works with ordinary data types:
type t = Fold of t
let rec m = Fold m
let unfold (Fold v) = v
But the following example should reveal the underlying equi-recursive semantics:
# let f (x : [`Foo of [`Foo of 'a]] as ‘a) : [`Foo of 'b] as 'b = x;;
val f : ([ `Foo of 'a ] as 'a) -> 'a = <fun>
So yeah, strike my remark about polymorphic variants. :)
FWIW, some old notes by Crary et al. [1] discuss this very choice, and how it interferes with modules. Moreover, based on their observations, the Harper/Stone semantics for SML actually models data type definitions as opaque abstract types (modules, really) that are merely _implemented_ by an iso-recursive type. That is both to capture their nominal (generative) semantics, but also to be able to express partial abstraction of mutually recursive types:
module type S =
sig
type t
type u = U of t
end
module M : S =
struct
type t = T of u
and u = U of t
end
This is not expressible directly with iso-recursion, as explained in [1].
Thanks for the pointer to this gem!
Just to clarify and expand on my earlier remark, the way the Harper/Stone semantics eventually solved both problems was not by adopting “Shao’s equation” as predicted in those notes (which would require coinductive type equivalence, throwing a major advantage of iso-recursion out the window). Instead, they model the definition
type t = mu t. 1 + t
This explains datatypes as a combination of iso-recursion and the existing semantics for type abstraction (which could in turn be explained as existential quantification, of course :) ).