eclipse-archived / ceylon

The Ceylon compiler, language module, and command line tools
http://ceylon-lang.org
Apache License 2.0
395 stars 62 forks source link

Coverage is unsound for contravariant self types #7395

Closed jvasileff closed 5 years ago

jvasileff commented 5 years ago

This is a legal expression of type Nothing:

("" of Comparable<Nothing>) of Nothing

given the type Comparable with a contravariant self type:

shared interface Comparable<in Other>
        of Other
        given Other satisfies Comparable<Other> {}
jvasileff commented 5 years ago

Contravariant self types are useful since, for example, in the case of Comparable<in Self> they allow smallest() to operate on subtypes of a type that defines comparability:

shared void run() {
    class A() satisfies Comparable<A> {
        compare(A a) => equal;
    }
    class ASub() extends A() {}

    // this currently works:
    ASub result1 = smallest(ASub(), ASub());

    // but without contravariance, we'd have to settle
    // for a result of type `A`
    A result2 = smallest<A>(ASub(), ASub());
}

Another example is the toplevel function sort.

Two options to fix the unsoundness while preserving functionality seem to be:

  1. define coverage to exclude contravariant self types, or
  2. disallow self types that are contravariant, but relax the restriction on use-site variance annotations in upper bound constraints.

For (2), section §3.3.3 of the spec currently has:

A type occurring in the satisfies clause may not involve variance annotations in or out, defined below in §3.6.1 Type arguments and variance.

which disallows an alternate implementation of smallest that would work with an invariant Comparable:

shared Element smallest<Element>(Element x, Element y) 
        given Element satisfies Comparable<in Element> 
        => ...

It's not clear to me why the restriction exists, perhaps decidability?

gavinking commented 5 years ago

Ouch. This is really embarrassing.

gavinking commented 5 years ago

Thanks, @jvasileff. I have disallowed contravariant self types.