Improve error message for failure of generic subtyping of concrete types

[chalcolith]

The following program:

class box B

class box A
  let bs: Array[B] = Array[B]

  new create(bs': Array[B box] box) =>
    bs.append(bs')

actor Main
  new create(env: Env) =>
    let bs: Array[B val] trn = [ recover B end ]
    let bs': Array[B val] val = consume bs
    let a = A(bs')
    env.out.print("done")

https://playground.ponylang.io/?gist=5cdad1a2e82f962b034e277e23d1a91f

Produces the errors:

main.pony:14:15: argument not assignable to parameter
    let a = A(bs')
              ^
    Info:
    main.pony:14:15: argument type is Array[B val] val
        let a = A(bs')
                  ^
    main.pony:7:14: parameter type requires Array[B box] box^
      new create(bs': Array[B box] box) =>
                 ^
    main.pony:7:25: B box is not a subtype of B val: box is not a subcap of val
      new create(bs': Array[B box] box) =>
                            ^
    main.pony:13:14: Array[B val] val has different type arguments than Array[B box] box^
        let bs': Array[B val] val = consume bs
                 ^

Where the compiler is not allowing us to pass an Array[B val] to a parameter of type Array[B box]. It would be nice to allow covariance for type parameters' capabilities so that we could do this.

The code in question seems to be https://github.com/ponylang/ponyc/blob/cb2f814b6c182f7d469d5007aa52885cf24fad34/src/libponyc/type/subtype.c#L836; there is some discussion on Zulip: https://ponylang.zulipchat.com/#narrow/stream/189985-beginner-help/topic/parameter.20subtyping

[SeanTAllen]

The code in question is something under the is_sub_cap_and_ephcheck that happens immediately after the is_eq_typeargs that @chalcolith pointed out.

[SeanTAllen]

So the code is definitely being asked to check if box is a subcap of val just as the error message says. Which is to say, everything is working as intended based on the code that exists.

@jemc can you explain to me how this is correct based on the current type system? I would expect the test to be "is val a subtype of box".

[jemc]

I gave some explanation in the sync call.

For anyone who wants to understand this issue, I recommend reading first this RFC that I made, proposing a new language feature related to this topic. The RFC stalled because Sylvan suggested that this problem is better solved by HKT (higher-kinded types), but there is no RFC for HKT at this time.

To summarize, the key reason why the code from @chalcolith doesn't work is because in Pony, generic classes require identical type parameters for subtyping. In other words, type parameters are always treated as invariant for generic classes/actors/primitives. That's because Pony's type system "assumes the worst" about expecting that the class/actor/primitive can use the type parameter in uses both "covariant positions" (e.g. return types) and "contravariant positions" (e.g. parameter types), meaning that the type parameter is treated as invariant.

And in fact Pony's "assume the worst" expectation turns out to be true for Array - if you're reading values out of an array the element type is being used in a covariant way, but if you're writing values into an array the element type is being used in a contravariant way. For example, if you have an Array[B box], the "stuff you read out of it" can be read as B box or B tag (but not B val!), and "the stuff you write into it" can come from B val or B box (but not B tag!). Therefore I can't subsume either an Array[B tag] or Array[B val] into Array[B box], because the former would make for capability-violating read operations, and the latter would make for capability-violating write operations.

The way to make this work in Pony is to use an interface which only defines the operations that you want to use. For example, if you only need to read from the array, you could use something like ReadSeq (or a similar interface that you define), which only contains the read operations. And then covariance works as desired - both Array[B box] and Array[B val] (but not Array[B tag] are subtypes of ReadSeq[B box].

The RFC I linked above was about a new syntax for automatically "summoning" an interface type which included only the covariant or only the contravariant (or only the bivariant) methods of the relevant class, without you needing to define such an interface by hand.

If that RFC were to be accepted/implemented, you'd be able to use Array[+B box] as a type to imply "an interface composed of the subset of Array methods which can safely be used for a covariant T, where T is set to B box". But as it stands in Pony today, you'll either need to use ReadSeq[B box] or define your own interface which has some different subset of "read-only" operations from Array.

[jemc]

Regarding the error message shown in @chalcolith 's code above, I think the error message is correct and understandable, as long as you know the background about Pony concrete types (classes/actors/primitives) always using their type parameters in an invariant way (never covariant, contravariant, or bivariant). If you want covariance/contravariance/bivariance you need to use a correctly-defined interface type that matches the relevant methods of the class.

To improve the error message I guess we could try to say something to that effect as a "hint" after the current message says "Array[B val] val has different type arguments than Array[B box] box^".

[SeanTAllen]

Can this be closed?

[jemc]

If somebody thinks we should improve the error message for !is_eq_typeargs(sub, super, errorf, opt) then we can keep the ticket open for that purpose.

Otherwise, yes, it can be closed.

[SeanTAllen]

The error isn't coming from the typeargs check. That passes just fine. The error is from the sub cap and ephemeral check.

[jemc]

I'm talking about this error message, which is emitted from the is_eq_typeargs function.