Incorrect variance annotation discarded

[stedolan]

If I write the following incorrect type:

type +'a t = [> `Foo of 'a -> unit] as 'a

the typechecker accepts it, pretending that I had never written the incorrect variance annotation:

type 'a t = 'a constraint 'a = [> `Foo of 'a -> unit ]

whereas it should reject my type definition.

[garrigue]

This looks like a bug indeed. Thanks for the report.

[garrigue]

Note that one can verify that the type was indeed inferred as invariant:

# let x: 'a t = `Foo (fun _ -> ());;
val x : ([> `Foo of 'a -> unit ] as 'a) t = `Foo <fun>
# (fun x -> x) x;;
- : (_[> `Foo of 'a -> unit ] as 'a) t = `Foo <fun>

So there should definitely be an error message.

[garrigue]

Well, actually I'm no longer sure this is a bug.
Namely, variance is only about type variables, so the questions is what +'a implies.
Since the type bound to 'a is [> Foo of 'a -> unit] as 'a, the row variable (which is the only type variable here) has both co- and contra-variant occurrences. As a a result, even assuming the 'a is covariant, the row-variable is invariant, which is already the strongest possible constraint, so the type checker has no reason to refuse this definition.

I admit this is a bit confusing, but this is a consequence of variance applying only to (non-instantiated) type variables.

For now, I just remove the bug label.

[garrigue]

While this appears not to be a bug, it had me thinking a while before checking it with the debugger, and understanding what was happening.

There are two things that could be done:

• Improve the documentation, explaining the semantics of variance annotations in more detail.
  In particular the fact that annotations on constrained parameters are only requirements on
  the type variables appearing inside these parameters.
  However, applying that semantics to concrete cases may not be so intuitive.
• Add a warning for "ineffective variance annotation", i.e. for a type declaration where
  a (valid) variance annotation is given, but it only ends up requiring all type variables
  to be invariant. Note that it would be by type declaration rather than by individual
  annotation, because inferring which annotation restricts which variable would require
  changes in the algorithm.

Some thoughts?

A more radical approach would be to go further in the direction suggested by @gasche in #8701, and allow annotations on type variables rather than parameters. The trouble is that this means adding them inside the syntax of types themselves (even row variables!), and protect against those annotations being used in unrelated places. That would be a big change.

[gasche]

Namely, variance is only about type variables, so the questions is what +'a implies.

For me the definition of covariance of 'a in t is that if we have two types u1 <: u2, then we have t['a := u1] <: t['a := u2] whenever the latter is well-formed (respects the constraints). I'm not sure what it suggests here.

[stedolan]

Thanks for the analysis @garrigue!

I think the same way as @gasche about variance (as a monotonicity/anti-monotonicity property of type-level functions, rather than a property of type variables). I had a go at translating your explanation into this language, but I'm not sure if it matches yours. Does the following make sense to you?

In +'a t, the covariance annotation means that t is a monotonic type-level function from types to types. Using constraints, the domain of this function can be restricted. In the example where 'a t is defined as [> `Foo of 'a -> unit] as 'a, the type 'a is in fact uniquely specified by the constraint. The type-level function t is therefore a function from the one-point set to types. (That is, the domain is so restricted that it contains only a single type: [> `Foo of 'a -> unit] as 'a).

All functions whose domain is a one-point set are monotonic (and also anti-monotonic, and injective, and order-embeddings). So, when the domain is so restricted as to be only a single type, the covariance annotation is meaningless: +'a and -'a and 'a all mean the same thing in this special case. So the typechecker's not wrong to drop my +'a annotation, as in this case it's equivalent to not having any annotation at all.

[stedolan]

After some discussion with @lpw25, I realise things are a bit more subtle: there are in fact many types of the form [> `Foo of 'a -> unit] as 'a: they differ in the contents of the row variable (at labels other than `Foo). However, while not being a singleton, this domain has the property that the subtyping relation is an equivalence (if a <= b, then b <= a), so as above, monotone and antimonotone coincide and the variance annotations are meaningless.

[github-actions]

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.