Comment author: @lpw25

This is not a bug, since neither of these examples is intended to be allowed.

external id : ([< A | B ] as 'a) -> [> 'a ] = "%identity"

in this example 'a is a polymorphic variant type, however only type constructors that are defined as polymorphic variants are supposed to be allowed. The problem here is that the error message is very confusing.

EDIT: Actually, it doesn't have to be a type constructor, but it does have to be an exact polymorphic variant type.

type 'a test = unit constraint 'a = [>]
let test : [< 'a test ] -> [> 'a ] = fun x -> x

In the second example 'a test is defined as equal to unit, which is not a polymorphic variant type, and the error message is fine. Also note that the [> 'a] would also be rejected by the type checker.

Comment author: jpdeplaix

Oh yes, the second is false. But even if we replace « fun x -> x » into « Obj.magic », is fails with the same error.

For the first one, I don't see why it shouldn't be allowed. Because if we remove the « < » in « [< A | B ] », it compiles and works fine.

Comment author: @lpw25

Oh yes, the second is false. But even if we replace « fun x -> x » into « Obj.magic », is fails with the same error.

The "fun x -> x" isn't causing the error. The error is cause by the fact that 'a test is defined as unit, and so is not a polymorphic variant type. This means that [< 'a test] does not make any sense.

For the first one, I don't see why it shouldn't be allowed. Because if we remove the « < » in « [< A | B ] », it compiles and works fine.

It can't be accepted because 'a is not an exact polymorphic variant type.

Note that [> foo] is translated by checking that foo is a polymorphic variant type, and then copying the constructors from that type. So the constructors must be known at compile-time.

([< A | B ] as 'a) -> [> 'a ]

cannot work because we do not know the constructors of 'a at compile-time.

Comment author: jpdeplaix

Mmmh I don't see the difference between [< A | B ] and the closed type [A | B] in the compilation process in this context :/

Why allowing to give lower type changes the ability to know the constructors of 'a ?

Comment author: @lpw25

Why allowing to give lower type changes the ability to know the constructors of 'a ?

Because a lower type will have fewer constructors.

The thing to bear in mind is that using type expressions within polymorphic variants is not really part of the type system.

val f : ([A | B] as 'a) -> [> 'a]

is just a convenient short-hand for:

val f : [A | B] -> [> A | B]

OCaml's row polymorphism does not have a way to express the type:

[< A | B] as 'a -> [> 'a]

and it cannot expand it out like it did for the type of f because it does not know exactly what constructors 'a has.

More sophisticated forms of row polymorphism can express types like the one above, but OCaml's can't.

Comment author: @alainfrisch

Downgrading severity, since this is only about providing a better error message.

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.

I understand this issue is technically about clarifying error messages, but I would really like to see this underlying limitation of the type system (the inability to expand the type), at least for closed polymorphic variants. I have no idea what that would mean in terms of effort, but it would be a really nice feature to have. This greatly improve our ability to compose types & subtypes with polymorphic variant constraints.

I don't know if there are any other GH issues which raise this specific issue, but if there is, I would love to chime in there. Otherwise, I think it would be great to formalize this a bit more in a separate issue.

I am not familiar with the compiler internals, so please let me know if any of you think this is infeasible, or even undesirable for some reason.

You are more or less asking to completely redesign row-polymorphism in OCaml. This is not really a reasonable scale for a feature wish.

@Octachron you’re right, that’s such a big change, and would probably break a lot of things.