variance for type params and nominal types is broken

[nikomatsakis]

Our treatment of variance is broken for nominal types. We try to be covariant except when in a mutable context: but nominal types hide the way that the type parameter is used, so we end up being covariant all the time. Clearly unsound.

Here is an example test that should not compile but does. It demonstrates the problem for iface and enum types, but the same will apply to class types.

iface box_iface<T> {
    fn get() -> T;
    fn set(t: T);
}

enum box_impl<T> = {
    mut f: T
};

impl<T:copy> of box_iface<T> for box_impl<T> {
    fn get() -> T { ret self.f; }
    fn set(t: T) { self.f = t; }
}

fn set_box_iface<T>(b: box_iface<@const T>, v: @const T) {
    b.set(v);
}

fn set_box_impl<T>(b: box_impl<@const T>, v: @const T) {
    b.set(v);
}

fn main() {
    let b = box_impl({mut f: @3});
    set_box_iface(b as box_iface::<@int>, @mut 5);
    set_box_impl(b, @mut 5);
}

This is not exactly an unknown problem. There are basically three possible answers:

• declaration site variance: you declare the variance when you declare the type parameter. You then check that a type declared as covariant is only used in covariant locations (immutable fields, return types, etc), and similarly for contravariant parameters. Invariant parameters may be used anywhere.
• use site variance: this is what Java does. In practice, few seem to understand it and we should probably not go this route. The way it works is that we you use an instance of the type, you specify the variance on the type parameters, which affects which methods and so forth you can safely use. It's effectively a kind of existential type. The advantage of this is that it is very flexible, particularly when you have container types that include both get() and set() methods but which are commonly used in a read-only fashion. To accommodate this situation with declaration site variance only, you need multiple interfaces: one for reading (which is covariant) and one for reading/writing (which is invariant).
• a combination: some recent papers (such as this one) have shown ways to combine the two techniques, leading hopefully to a system that is at once usable and comprehensible. This is to some extent still a matter of active research.

Probably we want to with the first option.

[pcwalton]

I concur that declaration site variance seems like the way to go here.