spec constraint "static type warning if a type parameter is a supertype of its upper bound" is wrong

[chalin]

According to the analyzer, the VM (and my intuition), dynamic is a valid type parameter bound (i.e., no problems are reported over): class C<T extends dynamic> { }.

Consider the following excerpts from the Dart Language Spec (DLS):

• DLS 14, "Generics":

  It is a static type warning if a type parameter is a supertype of its upper bound.

• DLS 19.4, "Interface Types":

  • S is a supertype of T, written S :> T, iff T is a subtype of S.
  • T is a subtype of S, written T <: S, iff [⊥/dynamic]T << S.
  • ⊥ << S.

In the case of class C, a warning should be issued if

T :> dynamic
= dynamic <: T
= [⊥/dynamic]dynamic << T
= ⊥ << T

which is true, hence, according to the spec, a warning should be issued. I think that the tools are correct and the spec needs tuning.

The purpose of the constraint documented in DLS 14 is to prevent << cycles over type parameters (cf. @gbracha's comment in #17275), so the constraint might be better expressed as:

It is a static type warning if a type parameter T:

• extends itself, or
• extends U and U is more specific than T.

Under this revised definition, no problem would be reported for class C above, but an issue would be reported for this example taken from #9555: class D<T extends S, S extends T> { ... }.

[chalin]

For the record, this issue surfaced during work on DEP #30, github.com/chalin/DEP-non-null.

/cc @leafpetersen

[eernstg]

Is there a good reason for using dynamic as an upper bound, ever? Otherwise the clean solution to me looks like: Ban it!

[chalin]

It would be for the same reasons one might use dynamic in any other context: namely, to silence the static checker (usually because it is emitting too many false positives).

Concretely, suppose that you want to declare that T extends A | B. But Dart doesn't support union types (yet), so the best compromise (that avoids false-positive static warnings) is to use dynamic. Using the LUB(A,B) might be ok, except if, e.g., the LUB doesn't define a method named m() but each of A and B do.

[leafpetersen]

Yes, my expectation (given the Dart design philosophy) would be that a type parameter bounded by dynamic would be legal, and would essentially behave as dynamic. I agree that the letter of the spec as written would seem to prohibit this. Your proposed text seems reasonable on brief review - I think the first clause is subsumed by the second (reflexivity).

I think that there is more than just this one issue at play here though - I think the letter of the spec still doesn't really do what you would expect ehre. If we assume that an upper bound of dynamic is legal, then I would expect the following to work with no warnings:

class F<T extends dynamic> {
  int anInt;
  T aT;
  void doer(T f) {
    anInt = f;
    aT = anInt;
    f.hello();
  }
}

And indeed, the analyzer gives no warnings on this code. However, I don't see how the definition of assignment compatibility can be read to make T and int assignable: int << T doesn't hold, since there's nothing you can do with T there, and T << int doesn't hold because the replacement of dynamic with bottom in T is specified to happen before the expansion of T into its upper bound, and hence has no effect. The only thing you can do is check that dynamic << int, which doesn't hold.

I think this is actually more general than the question of something with a direct bound of dynamic. The following code exhibits the same anomaly:

class G<T extends List<dynamic>> {
  List<int> aListOfInt;
  T aT;
  void doer(T f) {
    aListOfInt = f;
    aT = aListOfInt;
    aT[0].hello();
  }
}

The analyzer accepts this code, and it seems reasonable from a certain perspective. But I don't see any way to justify it directly from the spec. It would seem to me that this would require something like replacing the text
T is a type parameter and S is the upper bound of T
with
T is a type parameter with upper bound U, and [bottom/dynamic]U << S

@bwilkerson, @gbracha - any comment? Am I missing anything?

[chalin]

Your proposed text seems reasonable on brief review - I think the first clause is subsumed by the second (reflexivity).

Right. But, if we keep them separate then the second clause can be phrased in terms of <:, or :> (as in the original spec prose).

Here is a simplified version of class F which still can be used to illustrate the issue:

class F<T extends dynamic> { T o = 1; }

I don't see how the definition of assignment compatibility can be read to make T and int assignable

Making Leaf's derivation explicit we have: int ⟺ Tdynamic (where T carries its bound in superscript like in B.3.5)

= int <: T^dynamic ∨ T^dynamic <: int,     by def. of ⟺
= [⊥/dynamic]int << T^dynamic ∨ [⊥/dynamic]T^dynamic << int,      by def. of <:
= int << T^dynamic ∨ T^⊥ << int,      by simplification.

As Leaf points out, the left disjunct is false since int and T^dynamic are incomparable. The key question then is whether we accept that [⊥/dynamic]T^dynamic simplifies to T^⊥ (using this notation or any equivalent one e.g. using a typing context Γ ). A sure way to curb debate would be to formalize Dart's type system in Coq or Isabelle and prove various properties of it. If we do agree that such a simplification is reasonable then T^⊥ << int follows from transitivity applied to

• T^⊥ << ⊥, since a type parameter is more specific than its bound (A.1.4 << property (v)), and
• ⊥ << int (A.1.4 << property (ii))

T is a type parameter with upper bound U, and [bottom/dynamic]U << S

That could work too if we can't agree whether it is reasonable to consider [⊥/dynamic]T^dynamic simplifying to T^⊥ is a derived property.

[eernstg]

At this point we are working on Dart 2 and the Dart 1 specification will not be further developed. In Dart 2 there is no << relation and dynamic is not subject to the substitution that makes it a bottom type on the left hand side of a subtype judgment. Furthermore, we have introduced super-bounded types, and they introduce a whole class of situations where it is no longer a static warning nor an error to use an actual type argument which is a supertype of the specified bound for the corresponding formal type parameter.

In short, everything in this particular part of the language has changed, and hence it seems most reasonable to close this issue.

@chalin, thanks for clarifying this area, sorry about not using the input in time! However, the area has been developed in an interesting and hopefully quite useful manner since then.

With that, I'll close the issue.

[eernstg]

(Forgot to actually close it. Here we go.)