Exact types

[eernstg]

This issue is intended to clarify the approach to exact types in Dart.

An expression e has an exact type if it is statically known that the result v yielded from an evaluation of e will have a specific type T, and there is no proper subtype S of T such that v has type S. Examples are literals (42, true, <int>[2, 3]) instance creations denoting generative constructors (C("Hello, world!")), and constant expressions in general.

Exact types have been on the table many times; they play a role in the following Dart SDK issues, at least:

• VM: Very confusing error on invalid constant assignment (VM: Very confusing error on invalid const assignment #33303).
• Does the Kernel Instantiation node check the type arguments (Does the Kernel Instantiation node check the type arguments. #31953).
• In front end, do not relax override rules when overridden parameter is covariant (In front end, do not relax override rules when overridden parameter is covariant #31596).
• Consider making strong mode read check less eager area-language strong-mode-future-work (Consider making strong mode read check less eager #31391).
• DDC strong mode and exact types (DDC strong mode and exact types #30546).
• isAssignableTo is not symmetric, but used in some checks where that is expected (isAssignableTo is not symmetric, but used in some checks where that is expected #30544).
• Analyzer doesn't catch that method argument has wrong signature (Analyzer doesn't catch that method argument has wrong signature #30052)
• Customer request: Wildcard generics area-language (Customer request: Wildcard generics #29777).
• Add keyword that refers to a class' type for use in type parameters area-language (Add keyword that refers to a class' type for use in type parameters #28477).
• Strong mode const semantics don't allow for compile time canonicalization (Strong mode const semantics don't allow for compile time canonicalization #26291).
• Instantiate-to-bounds process produces different results depending on the nesting level of type variable for function return value (Instantiate-to-bounds process produces different results depending on the nesting level of type variable for function return value. #33606).

The language specification does not take this concept into account, there are no "exact types" and hence no expressions are considered to have such a type. However, the actual dynamic semantics ensures that certain expressions (such as the ones mentioned above) will indeed satisfy the requirement associated with an exact type, so we already have the dynamic semantics in place for using this concept.

We could handle exact types outside the language: A lint could characterize any set of expressions as having an exact type (along with a careful argument that each of those expressions will actually evaluate to a value of exactly that type). We could also introduce the notion of exact types in the language specification (based on a similar careful soundness argument) and make exact types part of the language.

In both cases, we could then flag situations (as a lint violation respectively a compile-time error) where a dynamic type check will be performed, but it is guaranteed to fail at run time because the value under scrutiny will never have the requested type (e.g., List<int> xs = <num>[];).

Note that List<int> xs = <num>[]; is flagged as an error by the analyzer already today, which illustrates that the concept of exact types is already being used in some sense.

The purpose of this issue is to handle the discussion about whether to introduce such a concept, at which level to do it (lint/language), how to define the concept itself in more detail, and exactly which situations to flag as wrong with some kind of diagnostic message.

[lrhn]

The concept of exact types are part of strong mode, so they are, de-facto, introduced in the Dart 2 language.

Specifying it is a separate issue. We could take the vague approach and say that tools may make anything that is a guaranteed run-time type error if evaluated into a compile-time error. That would leave the implementations open to improve their analyses over time.
Or we could make a definitive list of the expressions that have exact types, and just say that we don't allow implicit down-cast on those expressions. (We can also warn about explicit down-casts, but that should probably only be a warning).