Currently the regression test checks type a . a option ref, which is unsoundly accepted in trunk, and { foo : 'a . 'a option ref }, which is correctly rejected. I would be in favor of adding two other tests to cover different forms of explicit polymorphism:

let test : 'a . 'a list ref = ref [] 
(* unsound in trunk *)

let test (type a) : a list ref = ref []
(* accepted in trunk, with a weak polymorphic type, which I find surprising *)

(Note: arguably type a . a list ref is a combination of both those features, but I prefer to (also) test the simpler forms. I didn't expect that the (type a) version would type-check, for example.)

Locally abstract types are quite orthogonal to explicit polymorphism, and thus these two tests seem quite redundant too me?

I had the impression that the use of a locally abstract type would guarantee that the definition would be (strongly) polymorphic under the corresponding type variable, so clearly the two features are not orthogonal to me. I have no idea whether it was just me thinking this, or whether this is a wide-spread assumption.

I think that my impression partly comes from the similarity between let t (type a) .. and the System F syntax for abstraction over a type variable. I read this code as if a was a name for a type (treated abstractly in the definition) that can be chosen by each user of t, sort of like a lightweight functor notation. With this interpretation the currently-accepted behavior let foo (type a) : a list ref = [] is wrong.

(Another way to object to this behavior is to say that a weak type variable is scoped outside the declaration that contains it, so unifying it with a locally abstract type could be treated as an escape of that local type.)

I just checked, and the documentation does not say that (type a) will be replaced by a a generalizable type variable, just a type variable, so the documentation is not contradicted by this example. I still find it surprising. (But this is orthogonal to the present bug.)

Actually, the paragraph Polymorphic syntax is quite explicit about this behavior:

The (type typeconstr-name) syntax construction by itself does not make polymorphic the type variable it introduces, but it can be combined with explicit polymorphic annotations where needed.