Owner: [email protected]
Status: Draft
2022.05.12
- Define the notions of "constraint solution for a set of type variables" and "Grounded constraint solution for a set of type variables". These definitions capture how type inference handles type variable bounds, as well as how inferred types become "frozen" once they are fully known.
2019.09.01
- Fix incorrect placement of left top rule in constraint solving.
2019.09.01
- Add left top rule to constraint solving.
- Specify inference constraint solving.
2020.07.20
- Clarify that some rules are specific to code without/with null safety. 'Without null safety, ...' respectively 'with null safety, ...' is used to indicate such rules, and the remaining text is applicable in both cases.
2020.07.14:
- Infer return type
void
from context with function literals.
2020.06.04:
- Make conflict resolution for override inference explicit.
2020.06.02
- Account for the special treatment of bottom types during function literal inference.
2020.05.27
- Update function literal return type inference to use futureValueTypeSchema.
2019.12.03:
- Update top level inference for non-nullability, function expression inference.
Type inference in Dart takes three different forms. The first is mixin inference, which is specified elsewhere. The second and third forms are local type inference and top-level inference. These two forms of inference are mutually interdependent, and are specified here.
Top-level inference is the process by which the types of top-level variables and several kinds of class members are inferred when type annotations are omitted, based on the types of overridden members and initializing expressions. Since some top-level declarations have their types inferred from initializing expressions, top-level inference involves local type inference as a sub-procedure.
Local type inference is the process by which the types of local variables and closure parameters declared without a type annotation are inferred; and by which missing type arguments to list literals, map literals, set literals, constructor invocations, and generic method invocations are inferred.
Top-level inference derives the type of declarations based on two sources of information: the types of overridden declarations, and the types of initializing expressions. In particular:
- Method override inference
- If you omit a return type or parameter type from an overridden or implemented method, inference will try to fill in the missing type using the signature of the methods you are overriding.
- Static variable and field inference
- If you omit the type of a field, setter, or getter, which overrides a corresponding member of a superclass, then inference will try to fill in the missing type using the type of the corresponding member of the superclass.
- Otherwise, declarations of static variables and fields that omit a type will be inferred from their initializer if present.
As a general principle, when inference fails it is an error. Tools are free to behave in implementation specific ways to provide a graceful user experience, but with respect to the language and its semantics, programs for which inference fails are unspecified.
Some broad principles for type inference that the language team has agreed to, and which this proposal is designed to satisfy:
- Type inference should be free to fail with an error, rather than being required to always produce some answer.
- It should not be possible for a programmer to observe a declaration as having two different types at difference points in the program (e.g. dynamic for recursive uses, but subsequently int). Some consistent answer (or an error) should always be produced. See the example below for an approach that violates this principle.
- The inference for local variables, top-level variables, and fields, should either agree or error out. The same expression should not be inferred differently at different syntactic positions. It’s ok for an expression to be inferrable at one level but not at another.
- Obvious types should be inferred.
- Inferred and annotated types should be treated the same.
- As much as possible, there should be a simple intuition for users as to how inference proceeds.
- Inference should be as efficient to implement as possible.
- Type arguments should be mostly inferred.
For simplicity of specification, inference of method signatures and inference of signatures of other declaration forms are specified uniformly. Note however that method inference never depends on inference for any other form of declaration, and hence can validly be performed independently before inferring other declarations.
Because of the possibility of inference dependency cycles between top-level declarations, the inference procedure relies on the set of available variables (which are the variables for which a type is known). A variable is available iff:
- The variable was explicitly annotated with a type by the programmer.
- A type for the variable was previously inferred.
Any variable which is not available is said to be unavailable. If the
inference process requires the type of an unavailable variable in order to
proceed, it is an error. If there is any order of inference of declarations
which avoids such an error, the inference procedure is required to find it. A
valid implementation strategy for finding such an order is to explicitly
maintain the set of variables which are in the process of being inferred, and to
then recursively infer the types of any variables which are: required for
inference to proceed, but are not available, but are also not in the process
of being inferred. To see this, note that if the type of a variable x
which
is in the process of being inferred is required during the process of inferring
the type of a variable y
, then inferring the type of x
must have directly or
indirectly required inferring the type of y
. Any order of inference of
declarations must either have chosen to infer x
or y
first, and in either
case, the type of the other is both required, and unavailable, and hence will
be an error.
The general inference procedure is as follows.
- Mark every top level, static or instance declaration (fields, setters, getters, constructors, methods) which is completely type annotated (that is, which has all parameters, return types and field types explicitly annotated) as available.
- For each declaration
D
which is not available:- If
D
is a method, setter or getter declaration with namex
:- If
D
overrides another method, field, setter, or getter- Perform override inference on
D
. - Record the type of
x
and markx
as available.
- Perform override inference on
- Otherwise record the type of
x
as the type obtained by replacing an omitted setter return type withvoid
and replacing any other omitted types withdynamic
, and markx
as available.
- If
- If
D
is a declaration of a top-level variable or a static field declaration or an instance field declaration, declaring the namex
:- if
D
overrides another field, setter, or getter- Perform override inference on
D
. - Record the type of
x
and markx
as available.
- Perform override inference on
- Otherwise, if
D
has an initializing expressione
:- Perform local type inference on
e
. - Let
T
be the inferred type ofe
, ordynamic
if the inferred type ofe
is a subtype ofNull
. Record the type ofx
to beT
and markx
as available.
- Perform local type inference on
- Otherwise record the type of
x
to bedynamic
and markx
as available.
- if
- If
D
is a constructor declarationC(...)
for which one or more of the parameters is declared as an initializing formal without an explicit type:- Perform top-level inference on each of the fields used as an initializing
formal for
C
. - Record the inferred type of
C
, and mark it as available.
- Perform top-level inference on each of the fields used as an initializing
formal for
- If
If override inference is performed on a declaration D
, and any member which is
directly overridden by D
is not available, it is an error. As noted above,
the inference algorithm is required to find an ordering which avoids such an
error if there is such an ordering. Note that method override inference is
independent of non-override inference, and hence can be completed prior to the
rest of top level inference if desired.
A method m
of a class C
is subject to override inference if it is
missing one or more component types of its signature, and one or more of
the direct superinterfaces of C
has a member named m
(that is, C.m
overrides one or more declarations). Each missing type is filled in with
the corresponding type from the combined member signature s
of m
in the
direct superinterfaces of C
.
A compile-time error occurs if s
does not exist. E.g., one
superinterface could have signature void m([int])
and another one could
have signature void m(num)
, such that none of them is most specific.
There may still exist a valid override of both (e.g., void m([num])
). In
this situation C.m
can be declared with a complete signature, it just
cannot use override inference.
If there is no corresponding parameter in s
for a parameter of the
declaration of m
in C
, it is treated as dynamic
(e.g., this occurs
when overriding a one parameter method with a method that takes a second
optional parameter).
Note that override inference does not provide other properties of a
parameter than the type. E.g., it does not make a parameter required
based on overridden declarations. This property must then be specified
explicitly if needed.
The inferred type of a getter, setter, or field is computed as follows. Note that we say that a setter overrides a getter if there is a getter of the same name in some superclass or interface (explicitly declared or induced by an instance variable declaration), and similarly for getters overriding setters, fields, etc.
The return type of a getter, parameter type of a setter or type of a field which overrides/implements only one or more getters is inferred to be the return type of the combined member signature of said getter in the direct superinterfaces.
The return type of a getter, parameter type of a setter or type of a field which overrides/implements only one or more setters is inferred to be the parameter type of the combined member signature of said setter in the direct superinterfaces.
The return type of a getter which overrides/implements both a setter and a getter is inferred to be the return type of the combined member signature of said getter in the direct superinterfaces.
The parameter type of a setter which overrides/implements both a setter and a getter is inferred to be the parameter type of the combined member signature of said setter in the direct superinterfaces.
The type of a final field which overrides/implements both a setter and a getter is inferred to be the return type of the combined member signature of said getter in the direct superinterfaces.
The type of a non-final field which overrides/implements both a setter and a getter is inferred to be the parameter type of the combined member signature of said setter in the direct superinterfaces, if this type is the same as the return type of the combined member signature of said getter in the direct superinterfaces. If the types are not the same then inference fails with an error.
Note that overriding a field is addressed via the implicit induced getter/setter pair (or just getter in the case of a final field).
Note that late
fields are inferred exactly as non-late
fields. However,
unlike normal fields, the initializer for a late
field may reference this
.
Function literals which are inferred in an empty typing context (see below) are
inferred using the declared type for all of their parameters. If a parameter
has no declared type, it is treated as if it was declared with type dynamic
.
Inference for each returned expression in the body of the function literal is
done in an empty typing context (see below).
Function literals which are inferred in an non-empty typing context where the context type is a function type are inferred as described below.
Each parameter is assumed to have its declared type if present. If no type is
declared for a parameter and there is a corresponding parameter in the context
type schema with type schema K
, the parameter is given an inferred type T
where T
is derived from K
as follows. If the greatest closure of K
is S
and S
is a subtype of Null
, then without null safety T
is dynamic
, and
with null safety T
is Object?
. Otherwise, T
is S
. If there is no
corresponding parameter in the context type schema, the variable is treated as
having type dynamic
.
The return type of the context function type is used at several points during
inference. We refer to this type as the imposed return type
schema. Inference for each returned or yielded expression in the body of the
function literal is done using a context type derived from the imposed return
type schema S
as follows:
- If the function expression is neither
async
nor a generator, then the context type isS
. - If the function expression is declared
async*
andS
is of the formStream<S1>
for someS1
, then the context type isS1
. - If the function expression is declared
sync*
andS
is of the formIterable<S1>
for someS1
, then the context type isS1
. - Otherwise, without null safety, the context type is
FutureOr<flatten(T)>
whereT
is the imposed return type schema; with null safety, the context type isFutureOr<futureValueTypeSchema(S)>
.
The function futureValueTypeSchema is defined as follows:
- futureValueTypeSchema(
S?
) = futureValueTypeSchema(S
), for allS
. - futureValueTypeSchema(
S*
) = futureValueTypeSchema(S
), for allS
. - futureValueTypeSchema(
Future<S>
) =S
, for allS
. - futureValueTypeSchema(
FutureOr<S>
) =S
, for allS
. - futureValueTypeSchema(
void
) =void
. - futureValueTypeSchema(
dynamic
) =dynamic
. - futureValueTypeSchema(
_
) =_
. - Otherwise, for all
S
, futureValueTypeSchema(S
) =Object?
.
Note that it is a compile-time error unless the return type of an asynchronous
non-generator function is a supertype of Future<Never>
, which means that
the last case will only be applied when S
is Object
or a top type.
In order to infer the return type of a function literal, we first infer the actual returned type of the function literal.
The actual returned type of a function literal with an expression body is the inferred type of the expression body, using the local type inference algorithm described below with a typing context as computed above.
The actual returned type of a function literal with a block body is computed as
follows. Let T
be Never
if every control path through the block exits the
block without reaching the end of the block, as computed by the definite
completion analysis specified elsewhere. Let T
be Null
if any control
path reaches the end of the block without exiting the block, as computed by the
definite completion analysis specified elsewhere. Let K
be the typing
context for the function body as computed above from the imposed return type
schema.
- For each
return e;
statement in the block, letS
be the inferred type ofe
, using the local type inference algorithm described below with typing contextK
, and updateT
to beUP(flatten(S), T)
if the enclosing function isasync
, orUP(S, T)
otherwise. - For each
return;
statement in the block, updateT
to beUP(Null, T)
. - For each
yield e;
statement in the block, letS
be the inferred type ofe
, using the local type inference algorithm described below with typing contextK
, and updateT
to beUP(S, T)
. - If the enclosing function is marked
sync*
, then for eachyield* e;
statement in the block, letS
be the inferred type ofe
, using the local type inference algorithm described below with a typing context ofIterable<K>
; letE
be the type such thatIterable<E>
is a super-interface ofS
; and updateT
to beUP(E, T)
. - If the enclosing function is marked
async*
, then for eachyield* e;
statement in the block, letS
be the inferred type ofe
, using the local type inference algorithm described below with a typing context ofStream<K>
; letE
be the type such thatStream<E>
is a super-interface ofS
; and updateT
to beUP(E, T)
.
The actual returned type of the function literal is the value of T
after
all return
and yield
statements in the block body have been considered.
Let T
be the actual returned type of a function literal as computed above.
Let R
be the greatest closure of the typing context K
as computed above.
With null safety: if R
is void
, or the function literal is marked async
and R
is FutureOr<void>
, let S
be void
(without null-safety: no special
treatment is applicable to void
).
Otherwise, if T <: R
then let S
be T
. Otherwise, let S
be R
. The
inferred return type of the function literal is then defined as follows:
- If the function literal is marked
async
then the inferred return type isFuture<flatten(S)>
. - If the function literal is marked
async*
then the inferred return type isStream<S>
. - If the function literal is marked
sync*
then the inferred return type isIterable<S>
. - Otherwise, the inferred return type is
S
.
Without null safety, a local function definition which has no explicit return
type is subject to the same return type inference as a function expression with
no typing context. During inference of the function body, any recursive calls
to the function are treated as having return type dynamic
.
With null safety, local function body inference is changed so that the local
function name is not considered available for inference while performing
inference on the body. As a result, any recursive calls to the function for
which the result type is required for inference to complete will no longer be
treated as having return type dynamic
, but will instead result in an inference
failure.
When type annotations are omitted on local variable declarations and function literals, or when type arguments are omitted from literal expressions, constructor invocations, or generic function invocations, then local type inference is used to fill in the missing type information. Local type inference is also used as part of top-level inference as described above, in order to infer types for initializer expressions. In order to uniformly treat use of local type inference in top-level inference and in method body inference, it is defined with respect to a set of available variables as defined above. Note however that top-level inference never depends on method body inference, and so method body inference can be performed as a subsequent step. If this order of inference is followed, then method body inference should never fail due to a reference to an unavailable variable, since local variable declarations can always be traversed in an appropriate statically pre-determined order.
We define inference using types as defined in the informal specification of subtyping, with the same meta-variable conventions. Specifically:
The meta-variables X
, Y
, and Z
range over type variables.
The meta-variable L
ranges over lists or sets of type variables.
The meta-variables T
, S
, U
, and V
range over types.
The meta-variable C
ranges over classes.
The meta-variable B
ranges over types used as bounds for type variables.
For convenience, we generally write function types with all named parameters in an unspecified canonical order, and similarly for the named fields of record types. In all cases unless otherwise specifically called out, order of named parameters and fields is semantically irrelevant: any two types with the same named parameters (named fields, respectively) are considered the same type.
Similarly, function and method invocations with named arguments and records with named field entries are written with their named entries in an unspecified canonical order and position. Unless otherwise called out, position of named entries is semantically irrelevant, and all invocations and record literals with the same named entries (possibly in different orders or locations) and the same positional entries are considered equivalent.
Local type inference uses a notion of type schema
, which is a slight
generalization of the normal Dart type syntax. The grammar of Dart types is
extended with an additional construct _
which can appear anywhere that a type
is expected. The intent is that _
represents a component of a type which has
not yet been fixed by inference. Type schemas cannot appear in programs or in
final inferred types: they are purely part of the specification of the local
inference process. In this document, we sometimes refer to _
as "the unknown
type".
It is an invariant that a type schema will never appear as the right hand
component of a promoted type variable X & T
.
The meta-variables P
and Q
range over type schemas.
We define the notion of the covariant, contravariance, and invariant occurrences
of a type T
in another type S
inductively as follows. Note that this
definition of variance treats type aliases transparently: that is, the variance
of a type which is used as an argument to a type alias is computed by first
expanding the type alias (substituting actuals for formals) and then computing
variance on the result. This means that the only invariant positions in any
type (given the current Dart type system) are in the bounds of generic function
types.
The covariant occurrences of a type (schema) T
in another type (schema) S
are:
- if
S
andT
are the same type,S
is a covariant occurrence ofT
.
- if
S
isFuture<U>
- the covariant occurrences of
T
inU
- the covariant occurrences of
- if
S
isFutureOr<U>
- the covariant occurrencs of
T
inU
- the covariant occurrencs of
- if
S
is an interface typeC<T0, ..., Tk>
- the union of the covariant occurrences of
T
inTi
fori
in0, ..., k
- the union of the covariant occurrences of
- if
S
isU Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn, [Tn+1 xn+1, ..., Tm xm])
, the union of:- the covariant occurrences of
T
inU
- the contravariant occurrences of
T
inTi
fori
in0, ..., m
- the covariant occurrences of
- if
S
isU Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
the union of:- the covariant occurrences of
T
inU
- the contravariant occurrences of
T
inTi
fori
in0, ..., m
- the covariant occurrences of
- if
S
is(T0, ..., Tn, {Tn+1 xn+1, ..., Tm xm})
,- the covariant occurrences of
T
inTi
fori
in0, ..., m
- the covariant occurrences of
The contravariant occurrences of a type T
in another type S
are:
- if
S
isFuture<U>
- the contravariant occurrences of
T
inU
- the contravariant occurrences of
- if
S
isFutureOr<U>
- the contravariant occurrencs of
T
inU
- the contravariant occurrencs of
- if
S
is an interface typeC<T0, ..., Tk>
- the union of the contravariant occurrences of
T
inTi
fori
in0, ..., k
- the union of the contravariant occurrences of
- if
S
isU Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn, [Tn+1 xn+1, ..., Tm xm])
, the union of:- the contravariant occurrences of
T
inU
- the covariant occurrences of
T
inTi
fori
in0, ..., m
- the contravariant occurrences of
- if
S
isU Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
the union of:- the contravariant occurrences of
T
inU
- the covariant occurrences of
T
inTi
fori
in0, ..., m
- the contravariant occurrences of
- if
S
is(T0, ..., Tn, {Tn+1 xn+1, ..., Tm xm})
,- the contravariant occurrences of
T
inTi
fori
in0, ..., m
- the contravariant occurrences of
The invariant occurrences of a type T
in another type S
are:
- if
S
isFuture<U>
- the invariant occurrences of
T
inU
- the invariant occurrences of
- if
S
isFutureOr<U>
- the invariant occurrencs of
T
inU
- the invariant occurrencs of
- if
S
is an interface typeC<T0, ..., Tk>
- the union of the invariant occurrences of
T
inTi
fori
in0, ..., k
- the union of the invariant occurrences of
- if
S
isU Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn, [Tn+1 xn+1, ..., Tm xm])
, the union of:- the invariant occurrences of
T
inU
- the invariant occurrences of
T
inTi
fori
in0, ..., m
- all occurrences of
T
inBi
fori
in0, ..., k
- the invariant occurrences of
- if
S
isU Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
the union of:- the invariant occurrences of
T
inU
- the invariant occurrences of
T
inTi
fori
in0, ..., m
- all occurrences of
T
inBi
fori
in0, ..., k
- the invariant occurrences of
- if
S
is(T0, ..., Tn, {Tn+1 xn+1, ..., Tm xm})
,- the invariant occurrences of
T
inTi
fori
in0, ..., m
- the invariant occurrences of
Given a type S
and a set of type variables L
consisting of the variables
X0, ..., Xn
, we define the least and greatest closure of S
with respect to
L
as follows.
We define the least closure of a type M
with respect to a set of type
variables X0, ..., Xn
to be M
with every covariant occurrence of Xi
replaced with Never
, and every contravariant occurrence of Xi
replaced with
Object?
. The invariant occurrences are treated as described explicitly below.
We define the greatest closure of a type M
with respect to a set of type
variables X0, ..., Xn
to be M
with every contravariant occurrence of Xi
replaced with Never
, and every covariant occurrence of Xi
replaced with
Object?
. The invariant occurrences are treated as described explicitly below.
- If
S
isX
whereX
is inL
- The least closure of
S
with respect toL
isNever
- The greatest closure of
S
with respect toL
isObject?
- The least closure of
- If
S
is a base type (or in general, if it does not contain any variable fromL
)- The least closure of
S
isS
- The greatest closure of
S
isS
- The least closure of
- if
S
isT?
- The least closure of
S
with respect toL
isU?
whereU
is the least closure ofT
with respect toL
- The greatest closure of
S
with respect toL
isU?
whereU
is the greatest closure ofT
with respect toL
- The least closure of
- if
S
isFuture<T>
- The least closure of
S
with respect toL
isFuture<U>
whereU
is the least closure ofT
with respect toL
- The greatest closure of
S
with respect toL
isFuture<U>
whereU
is the greatest closure ofT
with respect toL
- The least closure of
- if
S
isFutureOr<T>
- The least closure of
S
with respect toL
isFutureOr<U>
whereU
is the least closure ofT
with respect toL
- The greatest closure of
S
with respect toL
isFutureOr<U>
whereU
is the greatest closure ofT
with respect toL
- The least closure of
- if
S
is an interface typeC<T0, ..., Tk>
- The least closure of
S
with respect toL
isC<U0, ..., Uk>
whereUi
is the least closure ofTi
with respect toL
- The greatest closure of
S
with respect toL
isC<U0, ..., Uk>
whereUi
is the greatest closure ofTi
with respect toL
- The least closure of
- if
S
isT Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn, [Tn+1 xn+1, ..., Tm xm])
and no type variable inL
occurs in any of theBi
:- The least closure of
S
with respect toL
isU Function<X0 extends B0, ..., Xk extends Bk>(U0 x0, ..., Un1 xn, [Un+1 xn+1, ..., Um xm])
where:U
is the least closure ofT
with respect toL
Ui
is the greatest closure ofTi
with respect toL
- with the usual capture avoiding requirement that the
Xi
do not appear inL
.
- The greatest closure of
S
with respect toL
isU Function<X0 extends B0, ..., Xk extends Bk>(U0 x0, ..., Un1 xn, [Un+1 xn+1, ..., Um xm])
where:U
is the greatest closure ofT
with respect toL
Ui
is the least closure ofTi
with respect toL
- with the usual capture avoiding requirement that the
Xi
do not appear inL
.
- The least closure of
- if
S
isT Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
and no type variable inL
occurs in any of theBi
:- The least closure of
S
with respect toL
isU Function<X0 extends B0, ..., Xk extends Bk>(U0 x0, ..., Un1 xn, {Un+1 xn+1, ..., Um xm})
where:U
is the least closure ofT
with respect toL
Ui
is the greatest closure ofTi
with respect toL
- with the usual capture avoiding requirement that the
Xi
do not appear inL
.
- The greatest closure of
S
with respect toL
isU Function<X0 extends B0, ..., Xk extends Bk>(U0 x0, ..., Un1 xn, {Un+1 xn+1, ..., Um xm})
where:U
is the greatest closure ofT
with respect toL
Ui
is the least closure ofTi
with respect toL
- with the usual capture avoiding requirement that the
Xi
do not appear inL
.
- The least closure of
- if
S
isT Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn, [Tn+1 xn+1, ..., Tm xm])
orT Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
andL
contains any free type variables from any of theBi
:- The least closure of
S
with respect toL
isNever
- The greatest closure of
S
with respect toL
isFunction
- The least closure of
- if
S
is(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
:- The least closure of
S
with respect toL
is(U0 x0, ..., Un1 xn, {Un+1 xn+1, ..., Um xm})
where:Ui
is the least closure ofTi
with respect toL
- The greatest closure of
S
with respect toL
is(U0 x0, ..., Un1 xn, {Un+1 xn+1, ..., Um xm})
where:Ui
is the greatest closure ofTi
with respect toL
- The least closure of
We define the greatest and least closure of a type schema P
with respect to
_
in the same way as we define the greatest and least closure with respect to
a type variable X
above, where _
is treated as a type variable in the set
L
.
Note that the least closure of a type schema is always a subtype of any type which matches the schema, and the greatest closure of a type schema is always a supertype of any type which matches the schema.
We write UP(T0, T1)
for the upper bound of T0
and T1
and DOWN(T0, T1)
for
the lower bound of T0
and T1
. This extends to type schema as follows:
- We add the axiom that
UP(T, _) == T
and the symmetric version. - We replace all uses of
T1 <: T2
in theUP
algorithm byS1 <: S2
whereSi
is the least closure ofTi
with respect to_
. - We add the axiom that
DOWN(T, _) == T
and the symmetric version. - We replace all uses of
T1 <: T2
in theDOWN
algorithm byS1 <: S2
whereSi
is the greatest closure ofTi
with respect to_
.
The following example illustrates the effect of taking the least/greatest closure in the subtyping algorithm.
class C<X> {
C(void Function(X) x);
}
T check<T>(C<List<T>> f) {
return null as T;
}
void test() {
var x = check(C((List<int> x) {})); // Should infer `int` for `T`
String s = x; // Should be an error, `T` should be int.
}
Type constraints take the form Pb <: X <: Pt
for type schemas Pb
and Pt
and type variables X
. Constraints of that form indicate a requirement that
any choice that inference makes for X
must satisfy both Tb <: X
and X <: Tt
for some type Tb
which satisfies schema Pb
, and some type Tt
which
satisfies schema Pt
. Constraints in which X
appears free in either Pb
or
Pt
are ill-formed.
The closure of a type constraint Pb <: X <: Pt
with respect to a set of type
variables L
is the subtype constraint Qb <: X <: Qt
where Qb
is the
greatest closure of Pb
with respect to L
, and Qt
is the least closure of
Pt
with respect to L
.
Note that the closure of a type constraint implies the original constraint: that
is, any solution to the original constraint that is closed with respect to L
,
is a solution to the new constraint.
The motivation for these operations is that constraint generation may produce a
constraint on a type variable from an outer scope (say S
) that refers to a
type variable from an inner scope (say T
). For example, <T>(T) -> List<T> <: <T>(T) -> S
constrains List<T>
to be a subtype of S
. But this
constraint is ill-formed outside of the scope of T
, and hence if inference
requires this constraint to be generated and moved out of the scope of T
, we
must approximate the constraint to the nearest constraint which does not mention
T
, but which still implies the original constraint. Choosing the greatest
closure of List<T>
(i.e. List<Object?>
) as the new supertype constraint on
S
results in the constraint List<Object?> <: S
, which implies the original
constraint.
Example:
class C<T> {
C(T Function<X>(X x));
}
List<Y> foo<Y>(Y y) => [y];
void main() {
var x = C(foo); // Should infer C<List<Object?>>
}
Inference works by collecting lists of type constraints for type variables of
interest. We write a list of constraints using the meta-variable C
, and use
the meta-variable c
for a single constraint. Inference relies on various
operations on constraint sets.
The merge of constraint set C
for a type variable X
is a type constraint Mb <: X <: Mt
defined as follows:
- let
Mt
be the lower bound of theMti
such thatMbi <: X <: Mti
is inC
(and_
if there are no constraints forX
inC
) - let
Mb
be the upper bound of theMbi
such thatMbi <: X <: Mti
is inC
(and_
if there are no constraints forX
inC
)
Note that the merge of a constraint set C
summarizes all of the constraints in
the set in the sense that any solution for the merge is a solution for each
constraint individually.
The constraint solution for a type variable X
with respect to a constraint set
C
is the type schema defined as follows:
- let
Mb <: X <: Mt
be the merge ofC
with respect toX
. - If
Mb
is known (that is, it does not contain_
) then the solution isMb
- Otherwise, if
Mt
is known (that is, it does not contain_
) then the solution isMt
- Otherwise, if
Mb
is not_
then the solution isMb
- Otherwise the solution is
Mt
Note that the constraint solution is a type schema, and hence may contain occurences of the unknown type.
The constraint solution for a set of type variables {X0, ..., Xn}
with respect
to a constraint set C
and partial solution {T0, ..., Tn}
, is defined to be
the set of type schemas {U0, ..., Un}
such that:
- If
Ti
is known (that is, does not contain_
), thenUi = Ti
. (Note that the upcoming "variance" feature will relax this rule so that it only applies to type variables without an explicitly declared variance.) - Otherwise, let
Vi
be the constraint solution for the type variableXi
with respect to the constraint setC
. - If
Vi
is not known (that is, it contains_
), thenUi = Vi
. - Otherwise, if
Xi
does not have an explicit bound, thenUi = Vi
. - Otherwise, let
Mb <: Xi <: Mt
be the merge ofC
with respect toXi
. IfMb
is not_
, letC1
be the constraint set produced by the subtype constraint generation algorithm forP = Mb
,Q = B
,L = {X0, ..., Xn}
. ThenUi
is the constraint solution for the type variableXi
with respect to the constraint setC + C1
. Note thatX
is inL
and thatMb
doesn't contain any ofX0, ..., Xn
. - Otherwise, let
Bi
be the bound ofXi
. Then, letBi'
be the type schema formed by substituting type schemas{U0, ..., Ui-1, Ti, ..., Tn}
in place of the type variables{X0, ..., Xn}
inBi
. (That is, we substituteUj
forXj
whenj < i
andTj
forXj
whenj >= i
). ThenUi
is the constraint solution for the type variableXi
with respect to the constraint setC + (X <: Bi')
.
This definition can perhaps be better understood in terms of the practical consequences it has on type inference:
- Once type inference has determined a known type for a type variable (that
is, a type that does not contain
_
), that choice is frozen and is not affected by later type inference steps. (Type inference accomplishes this by passing in any frozen choices as part of the partial solution). - The bound of a type variable participates in additional constraint generation when the choice of type for that type variable is about to be frozen.
- During each round of type inference, type variables are inferred left to right. If the bound of one type variable refers to one or more type variables, then at the time the bound is included as a constraint, the type variables it refers to are assumed to take on the type schemas most recently assigned to them by type inference.
The grounded constraint solution for a type variable X
with respect to a
constraint set C
is define as follows:
- let
Mb <: X <: Mt
be the merge ofC
with respect toX
. - If
Mb
is known (that is, it does not contain_
) then the solution isMb
- Otherwise, if
Mt
is known (that is, it does not contain_
) then the solution isMt
- Otherwise, if
Mb
is not_
then the solution is the least closure ofMb
with respect to_
- Otherwise the solution is the greatest closure of
Mt
with respect to_
.
Note that the grounded constraint solution is a type, and hence may not contain occurences of the unknown type.
The grounded constraint solution for a set of type variables {X0, ..., Xn}
with respect to a constraint set C
, with partial solution {T0, ..., Tn}
, is
defined to be the set of types {U0, ..., Un}
such that:
- If
Ti
is known (that is, does not contain_
), thenUi = Ti
. (Note that the upcoming "variance" feature will relax this rule so that it only applies to type variables without an explicitly declared variance.) - Otherwise, if
Xi
does not have an explicit bound, thenUi
is the grounded constraint solution for the type variableXi
with respect to the constraint setC
. - Otherwise, let
Mb <: Xi <: Mt
be the merge ofC
with respect toXi
. IfMb
is not_
, letC1
be the constraint set produced by the subtype constraint generation algorithm forP = Mb
,Q = B
,L = {X0, ..., Xn}
. ThenUi
is the grounded constraint solution for the type variableXi
with respect to the constraint setC + C1
. Note thatX
is inL
and thatMb
doesn't contain any ofX0, ..., Xn
. - Otherwise, let
Bi
be the bound ofXi
. Then, letBi'
be the type schema formed by substituting type schemas{U0, ..., Ui-1, Ti, ..., Tn}
in place of the type variables{X0, ..., Xn}
inBi
. (That is, we substituteUj
forXj
whenj < i
andTj
forXj
whenj >= i
). ThenUi
is the grounded constraint solution for the type variableXi
with respect to the constraint setC + (X <: Bi')
.
This definition parallels the definition of the (non-grounded) constraint solution for a set of type variables.
A constraint set C
constrains a type variable X
if there exists a c
in C
of the form Pb <: X <: Pt
where either Pb
or Pt
is not _
.
A constraint set C
partially constrains a type variable X
if the constraint
solution for X
with respect to C
is a type schema (that is, it contains
_
).
A constraint set C
fully constrains a type variable X
if the constraint
solution for X
with respect to C
is a proper type (that is, it does not
contain _
).
Subtype constraint generation is an operation on two type schemas P
and Q
and a list of type variables L
, producing a list of subtype
constraints C
.
We write this operation as a relation as follows:
P <# Q [L] -> C
where P
and Q
are type schemas, L
is a list of type variables X0, ..., Xn
, and C
is a list of subtype and supertype constraints on the Xi
.
This relation can be read as "P
is a subtype match for Q
with respect to the
list of type variables L
under constraints C
". Not all schemas P
and Q
are in the relation: the relation may fail to hold, which is distinct from the
relation holding but producing no constraints.
By invariant, at any point in constraint generation, only one of P
and Q
may
be a type schema (that is, contain _
), only one of P
and Q
may contain any
of the Xi
, and neither may contain both. That is, constraint generation is a
relation on type-schema/type pairs and type/type-schema pairs, only the type
element of which may refer to the Xi
. The presentation below does not
explicitly track which side of the relation currently contains a schema and
which currently contains the variables being solved for, but it does at one
point rely on being able to recover this information. This information can be
tracked explicitly in the relation by (for example) adding a boolean to the
relation which is negated at contravariant points.
- For convenience, ordering matters in this presentation: where any two clauses overlap syntactically, the first match is preferred.
- This presentation is assuming appropriate well-formedness conditions on the input types (e.g. non-cyclic class hierarchies)
C0 + C1
is the concatenation of constraint listsC0
andC1
.
For two type schemas P
and Q
, a set of type variables L
, and a set of
constraints C
, we define P <# Q [L] -> C
via the following algorithm.
Note that the order matters: we consider earlier clauses first.
Note that the rules are written assuming that if the conditions of a particular case (including the sub-clauses) fail to hold, then they "fall through" to try subsequent cluases except in the case that a subclause is prefixed with "Only if", in which case a failure of the prefixed clause implies that no subsequent clauses need be tried.
-
If
P
is_
then the match holds with no constraints. -
If
Q
is_
then the match holds with no constraints. -
If
P
is a type variableX
inL
, then the match holds:- Under constraint
_ <: X <: Q
.
- Under constraint
-
If
Q
is a type variableX
inL
, then the match holds:- Under constraint
P <: X <: _
.
- Under constraint
-
If
P
andQ
are identical types, then the subtype match holds under no constraints. -
If
P
is a legacy typeP0*
then the match holds under constraint setC
:- Only if
P0
is a subtype match forQ
under constraint setC
.
- Only if
-
If
Q
is a legacy typeQ0*
then the match holds under constraint setC
:- If
P
isdynamic
orvoid
andP
is a subtype match forQ0
under constraint setC
. - Or if
P
is a subtype match forQ0?
under constraint setC
.
- If
-
If
Q
isFutureOr<Q0>
the match holds under constraint setC
:- If
P
isFutureOr<P0>
andP0
is a subtype match forQ0
under constraint setC
. - Or if
P
is a subtype match forFuture<Q0>
under non-empty constraint setC
- Or if
P
is a subtype match forQ0
under constraint setC
- Or if
P
is a subtype match forFuture<Q0>
under empty constraint setC
- If
-
If
Q
isQ0?
the match holds under constraint setC
:- If
P
isP0?
andP0
is a subtype match forQ0
under constraint setC
. - Or if
P
isdynamic
orvoid
andObject
is a subtype match forQ0
under constraint setC
. - Or if
P
is a subtype match forQ0
under non-empty constraint setC
. - Or if
P
is a subtype match forNull
under constraint setC
. - Or if
P
is a subtype match forQ0
under empty constraint setC
.
- If
-
If
P
isFutureOr<P0>
the match holds under constraint setC1 + C2
:- If
Future<P0>
is a subtype match forQ
under constraint setC1
- And if
P0
is a subtype match forQ
under constraint setC2
- If
-
If
P
isP0?
the match holds under constraint setC1 + C2
:- If
P0
is a subtype match forQ
under constraint setC1
- And if
Null
is a subtype match forQ
under constraint setC2
- If
-
If
Q
isdynamic
,Object?
, orvoid
then the match holds under no constraints. -
If
P
isNever
then the match holds under no constraints. -
If
Q
isObject
, then the match holds under no constraints:- Only if
P
is non-nullable.
- Only if
-
If
P
isNull
, then the match holds under no constraints:- Only if
Q
is nullable.
- Only if
-
If
P
is a type variableX
with boundB
(or a promoted type variableX & B
), the match holds with constraint setC
:- If
B
is a subtype match forQ
with constraint setC
- Note that we have already eliminated the case that
X
is a variable inL
.
- Note that we have already eliminated the case that
- If
-
If
P
isC<M0, ..., Mk>
andQ
isC<N0, ..., Nk>
, and the corresponding type parameters declared by the classC
areT0, ..., Tk
, then the match holds under constraintsC0 + ... + Ck
, if for eachi
:- If
Ti
is a covariant type variable, andMi
is a subtype match forNi
with respect toL
under constraintsCi
, - Or
Ti
is a contravariant type variable,Ni
is a subtype match forMi
with respect toL
under constraintsCi
, - Or
Ti
is an invariant type variable, and:Mi
is a subtype match forNi
with respect toL
under constraintsCi0
,- And
Ni
is a subtype match forMi
with respect toL
under constraintsCi1
, - And
Ci
isCi0 + Ci1
.
- If
-
If
P
isC0<M0, ..., Mk>
andQ
isC1<N0, ..., Nj>
then the match holds with respect toL
under constraintsC
:- If
C1<B0, ..., Bj>
is a superinterface ofC0<M0, ..., Mk>
andC1<B0, ..., Bj>
is a subtype match forC1<N0, ..., Nj>
with respect toL
under constraintsC
. - Or
R<B0, ..., Bj>
is one of the interfaces implemented byP<M0, ..., Mk>
(considered in lexical order) andR<B0, ..., Bj>
is a subtype match forQ<N0, ..., Nj>
with respect toL
under constraintsC
. - Or
R<B0, ..., Bj>
is a mixin intoP<M0, ..., Mk>
(considered in lexical order) andR<B0, ..., Bj>
is a subtype match forQ<N0, ..., Nj>
with respect toL
under constraintsC
.
- If
-
A type
P
is a subtype match forFunction
with respect toL
under no constraints:- If
P
is a function type.
- If
-
A function type
(M0,..., Mn, [M{n+1}, ..., Mm]) -> R0
is a subtype match for a function type(N0,..., Nk, [N{k+1}, ..., Nr]) -> R1
with respect toL
under constraintsC0 + ... + Cr + C
- If
R0
is a subtype match for a typeR1
with respect toL
under constraintsC
: - If
n <= k
andr <= m
. - And for
i
in0...r
,Ni
is a subtype match forMi
with respect toL
under constraintsCi
.
- If
-
Function types with named parameters are treated analogously to the positional parameter case above.
-
A generic function type
<T0 extends B00, ..., Tn extends B0n>F0
is a subtype match for a generic function type<S0 extends B10, ..., Sn extends B1n>F1
with respect toL
under constraint setC2
- If
B0i
is a subtype match forB1i
with constraint setCi0
- And
B1i
is a subtype match forB0i
with constraint setCi1
- And
Ci2
isCi0 + Ci1
- And
Z0...Zn
are fresh variables with boundsB20, ..., B2n
- Where
B2i
isB0i[Z0/T0, ..., Zn/Tn]
ifP
is a type schema - Or
B2i
isB1i[Z0/S0, ..., Zn/Sn]
ifQ
is a type schema- In other words, we choose the bounds for the fresh variables from
whichever of the two generic function types is a type schema and does
not contain any variables from
L
.
- In other words, we choose the bounds for the fresh variables from
whichever of the two generic function types is a type schema and does
not contain any variables from
- Where
- And
F0[Z0/T0, ..., Zn/Tn]
is a subtype match forF1[Z0/S0, ..., Zn/Sn]
with respect toL
under constraintsC0
- And
C1
isC02 + ... + Cn2 + C0
- And
C2
isC1
with each constraint replaced with its closure with respect to[Z0, ..., Zn]
.
- If
-
A type
P
is a subtype match forRecord
with respect toL
under no constraints:- If
P
is a record type orRecord
.
- If
-
A record type
(M0,..., Mk, {M{k+1} d{k+1}, ..., Mm dm])
is a subtype match for a record type(N0,..., Nk, {N{k+1} d{k+1}, ..., Nm dm])
with respect toL
under constraintsC0 + ... + Cm
- If for
i
in0...m
,Mi
is a subtype match forNi
with respect toL
under constraintsCi
.
- If for
Expression inference is a recursive process of elaborating an expression in Dart source code, transforming it into a form in which all types and type coercions are explicit. An expression that has not yet undergone type inference is referred to as an unelaborated expression, and an expression that has completed type inference is referred to as an elaborated expression.
To aid in distinguishing unelaborated and elaborated expressions, the text
below will typically denote an unelaborated expression by letter e
(often with
a suffix, e.g. e_1
), and an elaborated expression by the letter m
(again,
often with a suffix).
Expression inference always takes place with respect to a type schema known as
the expression's "context", which captures certain pieces of type information
about the code surrounding the expression. Contexts are specified as part of the
recursive rules for type inference; that is, when the rules for type inferring a
certain kind of expression, statement, or pattern require that a subexpression
be type inferred, they will specify the context in which that inference should
be performed, using a phrase like "let m
be the result of performing
expression inference on e
, in context K
".
Often, an expression's context can be understood as the static type the
expression must have (or be coercible to) in order to avoid a compile-time
error. For example, in the statement num n = f();
, the result of type
inferring f()
needs to be a subtype of num
(or a type that's coercible to
num
) in order to avoid a compile-time error. Accordingly, f()
is type
inferred in the context num
.
However, there are some exceptions. For example, in the code Object? x = ...; if (x is num) { x = f(); }
, the variable x
is promoted to the type num
within the body of the if
statement. Accordingly, f()
is type inferred in
the context num
, in an effort to reduce the likelihood that the assignment x = f()
will cause the type promotion to be lost. However, if the static type of
f()
doesn't wind up being a subtype of num
, there is no compile-time error;
x
is simply demoted back to Object?
as a side effect of the assignment.
Every elaborated expression has an associated static type, which is produced
as a by-product of the expression inference process. These static types are
specified in this document using language such as: "inference of e
produces an
elaborated expression m
with static type T
". The specification of static
types in this document should be understood to supersede the specification of
static types in the existing Dart language specification.
Informally, we may sometimes speak of the static type of an unelaborated
expression e
; when we do, what is meant by this is the static type of the
elaborated expression m
that results from performing expression inference on
e
in some context K
, where K
depends on where e
appears in the broader
program. Note in particular that a given expression might have a different
static type at different points in the code, since the behavior of expression
inference depends on the context K
, as well as the flow analysis state.
A property of expression inference, known as soundness, is that when an
elaborated expression is executed, it is guaranteed either to diverge, throw an
exception, or evaluate to a value that is an instance satisfying its static
type. Instance satisfying is defined as follows: a value v
is an instance
satisfying type T
iff the runtime type of v
is a subtype of the extension
type erasure of T
. So, for example, every value is considered an instance
satisfying type dynamic
, and all values except null
are considered an
instance satisfying type Object
.
This stands in contrast to the notion of "instance of"; a value v
is an
instance of a type T
only if the runtime type of v
is precisely T
.
The type inference rules below include informal sketches of a proof that soundness holds for each expression type. These are non-normative, so they are typeset in italics.
The elaboration process sometimes introduces new operations that are not easily expressible using the syntax of Dart. To allow these operations to be specified succintly, the syntax of Dart is extended to allow the following forms:
-
@AWAIT_WITH_TYPE_CHECK(m_1)
represents the following operation:-
Let
T_1
be the static type ofm_1
. -
Let
T
beflatten(T_1)
. -
Evaluate
m_1
, and letv
denote the result. Note that sincem_1
has static typeT_1
, by soundness,v
must be an instance satisfyingT_1
. SinceT_1 <: FutureOr<flatten(T_1)>
for allT_1
, it follows thatv
must be an instance satisfyingFutureOr<flatten(T_1)>
, or equivalently, satisfyingFutureOr<T>
. Therefore,v
must either be an instance satisfyingFuture<T>
, or if not, it must be an instance satisfyingT
. We consider the two cases below. -
If
v
is an instance satisfying typeFuture<T>
, then let@AWAIT_WITH_TYPE_CHECK(m_1)
evaluate tov
. -
Otherwise, let
@AWAIT_WITH_TYPE_CHECK(m_1)
evaluate to a future satisfying typeFuture<T>
that will complete to the valuev
at some later point. Such a future could, for instance, be created by executingFuture<T>.value(v)
, which is sound because in this casev
is an instance satisfyingT
. It also could be created using a more efficient implementation-specific mechanism.
Note that the two cases here may imply a runtime implementation doing an actual
is Future<T>
type check and branching on the result, or a compiler may be able to optimize away the check in some cases. This where the name@AWAIT_WITH_TYPE_CHECK
comes from. -
-
@CONCAT(m_1, m_2, ..., m_n)
, where eachm_i
is an elaborated expression whose static type is a subtype ofString
, represents the operation of evaluating eachm_i
in sequence and then concatenating the results into a single string. -
@DOUBLE(d)
represents a literal double with numeric valued
. The runtime behavior of this construct is to evaluate to an instance of the typedouble
representingd
. This is used to explicitly mark integer literals that have been converted, by type inference, to doubles. -
@IMPLICIT_CAST<T>(m)
represents an implicit cast of the expressionm
to typeT
. The runtime behavior of this construct is the same as that ofm as T
, except that in the case where the cast fails, the exception thrown is aTypeError
rather than aCastError
. -
@INT(i)
represents a literal integer with numeric valuei
. The runtime behavior of this construct is to evaluate to an instance of the typeint
representingi
. This is used to explicitly mark integer literals that have not been converted, by type inference, to doubles. -
@LET(T v = m_1 in m_2)
represents the operation of first evaluatingm_1
, whose static type must be a subtype ofT
, storing the result in temporary storage, then evaluatingm_2
in a scope in whichv
has static typeT
and evaluates to the stored value.- When this specification specifies that a
@LET
expression should be created using a variablev
that does not appear in the source code, it should be understood that a fresh variable is created that does not match any variable that exists in the user's program. TODO(paulberry): give an example to clarify.
- When this specification specifies that a
-
@PROMOTED_TYPE<T>(m)
represents an elaborated expression whose runtime behavior is the same as that ofm
, but where it is known that whenever the elaborated expression executes, the resulting value is an instance satisfying typeT
. This is used in situations where additional reasoning, beyond the static type ofm
, is required to establish soundness. Wherever this construct is used, the additional reasoning follows in italics. Note that sincem
and@PROMOTED_TYPE<T>(m)
have the same runtime behavior, implementations can most likely elide@PROMOTED_TYPE<T>(m)
tom
without any loss of functionality, provided they are not trying to construct a proof of soundness.
The rules below ensure that elaborated expressions will satisfy the following properties:
-
An elaborated expression will never contain one of the tokens
?.
,??
, or??=
. The type inference process converts expressions containing these tokens into simpler forms. -
Elaborated expressions will never contain any implicit type checks. This means, in particular, that:
-
If an elaborated expression ever takes the form
m_1 ? m_2 : m_3
, it is guaranteed that the static type ofm_1
will be a subtype ofbool
. That is, all the situations in which the compiler needs to check that a condition is a proper boolean are spelled out in the type inference rules. -
If an elaborated expression ever takes the form
m_1 && m_2
orm_1 || m_2
, it is guaranteed that the static type ofm_1
andm_2
will both be a subtype ofbool
. That is, all the situations in which the compiler needs to check that the argument of a logical boolean expression is a proper boolean are spelled out in the type inference rules. -
If an elaborated expression ever takes the form
throw m_1
, it is guaranteed that the static type ofm_1
will be a subtype ofObject
. That is,null
will never be thrown.` -
If an elaborated expression ever takes the form of an invocation whose target is not
dynamic
, then it is guaranteed that:-
Each invocation argument has a corresponding formal parameter in the invocation target, and the static type of the argument is a subtype of the corresponding formal parameter's static type (with appropriate generic substitutions).
-
All of the invocation target's required formal parameters have corresponding arguments.
-
-
The type inference rules below include informal sketches of a proof that the output of type inference satisfies these additional properties. These are non-normative, so they are typeset in italics.
Before considering the specific rules for type inferring each type of
expression, it is useful to define an operation known as coercion. Coercion
is a type inference step that is applied to an elaborated expression m_1
and a
target type T
, and produces a new elaborated expression m_2
.
The coercion operation satisfies the following soundness property: the static
type of m_2
is guaranteed to be a subtype of T
. A proof of this is sketched
below.
Coercions are used in most situations where the existing spec calls for an assignability check.
Coercion of an elaborated expression m_1
to type T
produces m_2
, with
static type T_2
, where m_2
and T_2
are determined as follows:
-
Let
T_1
be the static type ofm_1
. -
If
T_1 <: T
, then letm_2
bem_1
andT_2
beT_1
. SinceT_1 <: T
, soundness is satisfied. -
Otherwise, if
T_1
isdynamic
, then letm_2
be@IMPLICIT_CAST<T>(m_1)
andT_2
beT
. SinceT <: T
, soundness is satisfied. -
Otherwise, if
T_1
is an interface type that contains a method calledcall
with typeU
, andU <: T
, then letm_2
bem_1.call
, and letT_2
beU
. SinceU <: T
, soundness is satisfied. -
TODO(paulberry): add more cases to handle implicit instantiation of generic function types, and
call
tearoff with implicit instantiation. -
Otherwise, there is a compile-time error. We have an expression of type
T_1
in a situation that requiresT
, which isn't a supertype, nor is there a coercion available, so it's a type error.
In the text that follows, we will sometimes say something like "let m
be the
result of performing expression inference on e
, in context K
, and then
coercing the result to type T
." This is shorthand for the following sequence
of steps:
-
Let
m_1
be the result of performing expression inference one
, in contextK
. -
Let
m
be the result of performing coercion ofm_1
to typeT
.
It follows, from the soundness of coercions, that the static type of m
is
guaranteed to be a subtype of T
.
The following sections detail the specific type inference rules for each valid Dart expression.
Expression inference of the literal null
, regardless of context, produces the
elaborated expression null
, with static type Null
.
The runtime behavior of null
is to evaluate to an instance of the type
Null
, so soundness is satisfied.
Expression inference of an integer literal l
, in context K
, produces an
elaborated expression m
with static type T
, where m
and T
are determined
as follows:
-
Let
i
be the numeric value ofl
. -
Let
S
be the greatest closure ofK
. -
If
double
is a subtype ofS
andint
is not a subtype ofS
, then:-
If
i
cannot be represented precisely by an instance ofdouble
, then there is a compile-time error. -
Otherwise, let
T
be the typedouble
, and letm
be@DOUBLE(i)
. Soundness follows from the fact that@DOUBLE(i)
always evaluates to an instance ofdouble
.
-
-
Otherwise, if
l
is a hexadecimal integer literal, 263 ≤i
< 264, and theint
class is represented as signed 64-bit two's complement integers:-
Let
T
be the typeint
, and letm
be@INT(i
- 264)
. -
Soundness follows from the fact that the
@INT(j)
always evaluates to an instance ofint
.
-
-
Otherwise, if
i
cannot be represented precisely by an instance ofint
, then there is a compile-time error. -
Otherwise, let
T
be the typeint
, and letm
be@INT(i)
. Soundness follows from the fact that@INT(i)
always evaluates to an instance ofint
.
Expression inference of a double literal l
, regardless of context, produces
the elaborated expression l
, with static type double
.
The runtime behavior of a double literal is to evaluate to an instance of the
type double
, so soundness is satisfied.
Expression inference of a boolean literal e
(true
or false
), regardless of
context, produces the elaborated expression e
, with static type bool
.
The runtime behavior of a boolean literal is to evaluate to an instance of the
type bool
, so soundness is satisfied.
Expression inference of a string literal s
, regardless of context, produces an
elaborated expression m
with static type String
, where m
is determined as
follows:
-
If
s
contains no stringInterpolations, then letm
bes
. The runtime behavior of a string literal with no stringInterpolations is to evaluate to an instance of the typeString
, so soundness is satisfied. -
Otherwise:
-
For each stringInterpolation
s_i
insides
, in source order:-
Define
m_i
as follows:-
If
s_i
takes the form '${
'e
'}
':- Let
m_i
be the result of performing expression inference one
, in context_
.
- Let
-
Otherwise,
s_i
takes the form '$e
', wheree
is eitherthis
or an identifier that doesn't contain$
, so:- Let
m_i
be the result of performing expression inference one
, in context_
.
- Let
-
-
Let
n_i
bem_i.toString()
. Since bothObject.toString
andNull.toString
are declared with a return type ofString
, it follows that the static type ofn_i
isString
.
-
-
Let
m
be@CONCAT(parts)
, whereparts
is composed of simple string literals representing the portions ofs
that are not stringInterpolations, interleaved with then_i
. -
The runtime behavior of
@CONCAT(parts)
is to evaluate to an instance of the typeString
, so soundness is satisfied.
-
Expression inference of a symbol literal e
, regardless of context, produces
the elaborated expression e
, with static type Symbol
.
The runtime behavior of a symbol literal is to evaluate to an instance of the
type Symbol
, so soundness is satisfied.
Expression inference of a throw expression throw e_1
, regardless of context,
produces an elaborated expression m
with static type Never
, where m
is
determined as follows:
-
Let
m_1
be the result of performing expression inference one_1
, in context_
, and then coercing the result to typeObject
. -
It follows, from the soundness of coercions, that the static type of
m_1
is guaranteed to be a subtype ofObject
. That is,null
will never be thrown. -
Let
m
bethrow m_1
. Soundness follows from the fact thatthrow m_1
never evaluates to a value.
Expression inference of this
, regardless of context, produces the elaborated
expression this
with static type T
, where T
is the interface type of the
immediately enclosing class, enum, mixin, or extension type, or the "on" type of
the immediately enclosing extension.
The runtime behavior of this
is to evaluate to the target of the current
instance member invocation, which is guaranteed to be an instance satisfying
this type. So soundness is satisfied.
Expression inference of a logical "and" expression (e_1 && e_2
) or a logical
"or" expression (e_1 || e_2
), regardless of context, produces an elaborated
expression m
with static type bool
, where m
is determined as follows:
-
Let
m_1
be the result of performing expression inference one_1
, in contextbool
, and then coercing the result to typebool
. -
Let
m_2
be the result of performing expression inference one_2
, in contextbool
, and then coercing the result to typebool
. -
It follows, from the soundness of coercions, that the static type of
m_1
andm_2
are both guaranteed to be a subtype ofbool
. -
If
e
is of the forme_1 && e_2
, letm
bem_1 && m_2
. It is valid to form this elaborated expression because the static type ofm_1
andm_2
are guaranteed to be a subtype ofbool
. -
Otherwise,
e
is of the forme_1 || e_2
, so letm
bem_1 || m_2
. It is valid to form this elaborated expression because the static type ofm_1
andm_2
are guaranteed to be a subtype ofbool
.
The runtime behavior of logical boolean expressions is to evaluate to a value
equal to their first argument (in the case of a short-cut) or their second
argument (in the case of no short-cut). Since the static type of m_1
and m_2
are guaranteed to be a subtype of bool
, it follows that the the logical
boolean expression will evaluate to an instance satisfying type bool
, so
soundness is satisfied.
Expression inference of an await expression await e_1
, in context K
,
produces an elaborated expression m
with static type T
, where m
and T
are determined as follows:
-
Define
K_1
as follows:-
If
K
isFutureOr<S>
orFutureOr<S>?
for some type schemaS
, then letK_1
beK
. -
Otherwise, if
K
isdynamic
, then letK_1
beFutureOr<_>
. -
Otherwise, let
K_1
beFutureOr<K>
.
-
-
Let
m_1
be the result of performing expression inference one_1
, in contextK_1
. -
Let
T_1
be the static type ofm_1
. -
If
T_1
is incompatible with await (as defined in the extension types specification), then there is a compile-time error. -
Let
T_2
beflatten(T_1)
. -
Let
m_2
be@AWAIT_WITH_TYPE_CHECK(m_1)
, with static typeFuture<T_2>
. This is sound because@AWAIT_WITH_TYPE_CHECK(m_1)
always evaluates to an instance satisfying typeFuture<T_2>
.- Note that in many circumstances, it will be trivial for the compiler to
establish that
m_1
always evaluates to an instancev
that satisfies typeFuture<T_2>
, in which casem_2
can be optimized to@PROMOTED_TYPE<Future<T_2>>(m_1)
.
- Note that in many circumstances, it will be trivial for the compiler to
establish that
-
Let
T
beT_2
, and letm
beawait m_2
. Sincem_2
has static typeFuture<T_2>
, the value ofawait m_2
must necessarily be an instance satisfying typeT_2
, so soundness is satisfied.