refining module doesn't respect type parameter variance

[tjhance]

This file goes through without issue, when I would expect it to complain about a variance mismatch:

module M {
  type T<X>
}

module M' refines M {
  type T<!X> = X -> nat
}

Related to the previous issue #1216 (I came across this issue while filing the previous one) but it's probably a different bug.

[keyboardDrummer]

Can you elaborate what you think the ! should do and why it should cause an error here? ! does not denote covariance like + or *, so why would you expect a variance mismatch?

Actually I'm not sure what ! does. In compiler terms it changes the variance from strict to lax, but I have no idea what effect that should have, maybe you or @RustanLeino can elaborate?

[tjhance]

Yes you're right, this is actually a relaxed/strictness mismatch, not a variance mismatch.

According to the Dafny 3 release notes, ! indicates non-variant relaxed:

+ (co-variance, strict)
Enclosing type is monotonic in the type parameter.
The parameter is not used in expanding positions (that is, it is not used left of any arrow).

* (co-variance, relaxed)
Enclosing type is monotonic in the type parameter.
Other than that, use of the parameter is unrestricted (in particular, it may be used to the left of an arrow).

(default variance, denoted by not giving any of the other variance indicators explicitly) (non-variance, strict)
Different given parameters produce non-comparable types.
The parameter is not used in expanding positions (that is, it is not used left of any arrow).

! (non-variance, relaxed)
Different given parameters produce non-comparable types.
Other than that, use of the parameter is unrestricted (in particular, it may be used to the left of an arrow).

- (contra-variance)
Enclosing type is anti-monotonic in the type parameter.
Consequentially, every use of the parameter is to the left of some arrow.

If I understand, !X is a weaker condition than <no marker>X, because !X allows X to be used to the left of an arrow.

So for example, the declaration type T<X> is a guarantee that the type definition doesn't use X to the left of an arrow. By refining the module and writing type T<!X> = X -> nat I instantiate T with a type that does use X to the left of an arrow, so I expect it to give some kind of error. This is a similar reason to why you can't add requires clauses or remove ensures clauses when refining a method.

[keyboardDrummer]

I agree something is wrong here. The program

module M {
  type T<X>

  datatype R = Head | Tail(value: T<R>)
}

compiles without error, while the program

module M {
  type T<X>

  datatype R = Head | Tail(value: T<R>) // Error on this line
}

module M' refines M {
  type T<!X> = X -> nat
}

Throws an error in module M in the datatype R declaration. The technical reason is that the refines M causes the datatype R declaration to be copied over to module M', which is where it errors. Seems like this bug doesn't effect soundness, but it does cause an error is the wrong place since the real error is indeed relaxing the variance in M'.