> Unless you are talking about some other kind of hack, in which case I'd 
> be very grateful to hear more details.

Probably I was talking about something else.
(Please bear in mind that I've got this way of understanding the type checker 
via hacking the implementation; so it is likely that my understanding 
is incorrect.)

Let me consider:

module rec M : sig type t val x: t end = struct type t = int let x = M.x end

The type checker type checks the body of M, 
i.e., struct type t = int let x = M.x end, while the type environment records
M's signature as "sig type t val x: t end". But in fact one could perhaps 
enrich the signature to "sig type t = t val x: t end", 
where the right-hand side of the abbreviation t = t is the type t 
in the structure, not in the signature. 
As you may know, the type checker can distinguish the two types named t, 
since they internally carry different identities.
Since the type environments used to type check the body of M 
and the rest of the program are distinct, there is no possibility that 
type abstraction can be broken. 

This is not beautiful, since the type t in the right side of "t = t" 
escapes from its scope. 

I should note that this is not my original idea :-)

Thank you for the program. I will take it back home and look at it 
during the coming new year holidays.

Best,
Keiko