Comment author: @garrigue

I'm not sure this would be sound.
And if it is in this precise case, I'm not sure what the condition is to make it sound in general.
This may be related to @gache's work on subtyping for GADTs.

Comment author: @Drup

That was my initial reaction as well, but I was not able to find a counter example. @gasche, do you have one?

Comment author: @gasche

I don't understand the type-checking of "constraints" very well. When are they applied?

When experimenting with this question, in general it looks safe because the constraint is substituted for the type. For example, if you write

module type Get = sig
type +'a t = [< `A of int ] as 'a
val get : 'a t -> int
end

then the inferred signature is actually

val get : [< `A of int ] t -> int

(instead of a polymorphic ('a . 'a t -> int)) so there is no way to cause mischief by injecting a `B later.

On the other hand, the following would be unsound and must be rejected:

module Test : sig
type +'a t = [< A of int | B ] as 'a
val get : 'a t -> int
end
= struct
type +'a t = [< A of int ] as 'a let get = function A n -> n
end

Checking the implementation of get against its specification must happen after the constraints have been substituted in the signature of get -- if this happens, then it should be rejected.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

Without any feedback, I propose we keep rejecting such forms and close this.

Closing as suggested.