Ground coercion is not composable

[samsa1]

I've been looking at type coercion and found some weird behavior.

In the example below, test1 is of type 'a -> (int * 'a) as expected, however test2 is ill typed.

module M : sig
  type t = private int
  val el : t
end = struct
  type t = int
  let el = 0
end

let test1 (x : 'a) = ((M.el :> int), (x :> 'a))

let test2 (x : 'a) = ((M.el, x) :> (int * 'a))

The error message is

File "test.ml", line 11, characters 22-31:
11 | let test2 (x : 'a) = ((M.el, x) :> (int * 'a))
                           ^^^^^^^^^
Error: This expression cannot be coerced to type int * 'a; it has type
         M.t * 'a
       but is here used with type int * 'a
       Type M.t is not compatible with type int

The reason behind this is that coercion with closed types is strictly more expressive than with types containing a free type variable due to the following line in typing/typecore.ml : https://github.com/ocaml/ocaml/blob/564b2db8df9837b0390bcf1ca3249eddc7b69fae/typing/typecore.ml#L4358-L4359

I tried removing this guard and launching the testsuite, but this is never tested in the testsuite. Is the behavior of the example above expected ? If so shouldn't we document this behavior and add a related test ? Or is this a bug ?

PS : Similar problem with a first class module instead of a private type

[garrigue]

This is the intended behavior, and this is documented in the reference manual, section 7.7 (coercions):

As an exception to the above algorithm, if both the inferred type of expr and typ are ground (i.e. do not contain type variables), the former operator behaves as the latter one, taking the inferred type of expr as typ1. In case of failure with the former operator, the latter one should be used.

Adding a related test may be a good idea still.