Types
The above grammer describes the concrete syntax of types that can be written in user code. Semantic operations on types in the Scala type system are better defined in terms of internal types, which are desugared from the concrete type syntax.
Internal Types
The following abstract grammar defines the shape of internal types. In this specification, unless otherwise noted, "types" refer to internal types. Internal types abstract away irrelevant details such as precedence and grouping, and contain shapes of types that cannot be directly expressed using the concrete syntax. They also contain simplified, decomposed shapes for complex concrete syntax types, such as refined types.
Translation of Concrete Types into Internal Types
Concrete types are recursively translated, or desugared, into internal types. Most shapes of concrete types have a onetoone translation to shapes of internal types. We elaborate hereafter on the translation of the other ones.
Infix Types
A concrete infix type ´T_1´ op
´T_2´ consists of an infix operator op
which gets applied to two type operands ´T_1´ and ´T_2´.
The type is translated to the internal type application op
´[T_1, T_2]´.
The infix operator op
may be an arbitrary identifier.
Type operators follow the same precedence and associativity as term operators.
For example, A + B * C
parses as A + (B * C)
and A  B & C
parses as A  (B & C)
.
Type operators ending in a colon ‘:’ are rightassociative; all other operators are leftassociative.
In a sequence of consecutive type infix operations ´t_0 \, \mathit{op} \, t_1 \, \mathit{op_2} \, ... \, \mathit{op_n} \, t_n´, all operators ´\mathit{op}_1, ..., \mathit{op}_n´ must have the same associativity. If they are all leftassociative, the sequence is interpreted as ´(... (t_0 \mathit{op_1} t_1) \mathit{op_2} ...) \mathit{op_n} t_n´, otherwise it is interpreted as ´t_0 \mathit{op_1} (t_1 \mathit{op_2} ( ... \mathit{op_n} t_n) ...)´.
Under source:future
, if the type name is alphanumeric and the target type is not marked infix
, a deprecation warning is emitted.
The type operators 
and &
are not really special.
Nevertheless, unless shadowed, they resolve to the fundamental type aliases scala.
and scala.&
, which represent union and intersection types, respectively.
Function Types
The concrete function type ´(T_1, ..., T_n) \Rightarrow R´ represents the set of function values that take arguments of types ´T_1, ..., Tn´ and yield results of type ´R´. The case of exactly one argument type ´T \Rightarrow R´ is a shorthand for ´(T) \Rightarrow R´. An argument type of the form ´\Rightarrow T´ represents a callbyname parameter of type ´T´.
Function types associate to the right, e.g. ´S \Rightarrow T \Rightarrow R´ is the same as ´S \Rightarrow (T \Rightarrow R)´.
Function types are covariant in their result type and contravariant in their argument types.
Function types translate into internal class types that define an apply
method.
Specifically, the ´n´ary function type ´(T_1, ..., T_n) \Rightarrow R´ translates to the internal class type scala.Function´_n´[´T_1´, ..., ´T_n´, ´R´]
.
In particular ´() \Rightarrow R´ is a shorthand for class type scala.Function´_0´[´R´]
.
Such class types behave as if they were instances of the following trait:
Their exact supertype and implementation can be consulted in the function classes section of the standard library page in this document.
Dependent function types are function types whose parameters are named and can referred to in result types. In the concrete type ´(x_1: T_1, ..., x_n: T_n) \Rightarrow R´, ´R´ can refer to the parameters ´x_i´, notably to form pathdependent types. It translates to the internal refined type
where ´S´ is the least super type of ´R´ that does not mention any of the ´x_i´.
Polymorphic function types are function types that take type arguments. Their result type must be a function type. In the concrete type ´[a_1 >: L_1 <: H_1, ..., a_n >: L_1 <: H_1] => (T_1, ..., T_m) => R´, the types ´T_j´ and ´R´ can refer to the type parameters ´a_i´. It translates to the internal refined type
Tuple Types
A tuple type ´(T_1, ..., T_n)´ where ´n \geq 2´ is sugar for the type ´T_1´ *: ... *: ´T_n´ *: scala.EmptyTuple
, which is itself a series of nested infix types which are sugar for *:[´T_1´, *:[´T_2´, ... *:[´T_n´, scala.EmptyTuple]]]
.
The ´T_i´ can be wildcard type arguments.
Notes:
(´T_1´)
is the type ´T_1´, and not´T_1´ *: scala.EmptyTuple
(´T_1´ cannot be a wildcard type argument in that case).()
is not a valid type (i.e. it is not desugared toscala.EmptyTuple
).
Concrete Refined Types
In the concrete syntax of types, refinements can contain several refined definitions.
They must all be abstract.
Moreover, the refined definitions can refer to each other as well as to members of the parent type, i.e., they have access to this
.
In the internal types, each refinement defines exactly one refined definition, and references to this
must be made explicit in a recursive type.
The conversion from the concrete syntax to the abstract syntax works as follows:
 Create a fresh recursive this name ´\alpha´.
 Replace every implicit or explicit reference to
this
in the refinement definitions by ´\alpha´.  Create nested refined types, one for every refined definition.
 Unless ´\alpha´ was never actually used, wrap the result in a recursive type
{ ´\alpha´ => ´...´ }
.
Concrete Type Lambdas
At the top level of concrete type lambda parameters, variance annotations are not allowed. However, in internal types, all type lambda parameters have explicit variance annotations.
When translating a concrete type lambda into an internal one, the variance of each type parameter is inferred from its usages in the body of the type lambda.
Definitions
From here onwards, we refer to internal types by default.
Kinds
The Scala type system is fundamentally higherkinded. Types are either proper types, type constructors or polykinded types.
 Proper types are the types of terms.
 Type constructors are typelevel functions from types to types.
 Polykinded types can take various kinds.
All types live in a single lattice with respect to a conformance relationship ´<:´.
The top type is AnyKind
and the bottom type is Nothing
: all types conform to AnyKind
, and Nothing
conforms to all types.
They can be referred to with the fundamental type aliases scala.AnyKind
and scala.Nothing
, respectively.
Types can be concrete or abstract. An abstract type ´T´ always has lower and upper bounds ´L´ and ´H´ such that ´L >: T´ and ´T <: H´. A concrete type ´T´ is considered to have itself as both lower and upper bound.
The kind of a type is indicated by its (transitive) upper bound:
 A type
´T <:´ scala.Any
is a proper type.  A type
´T <: K´
where ´K´ is a type lambda (of the form[´\pm a_1 >: L_1 <: H_1´, ..., ´\pm a_n >: L_n <: H_n´] =>> ´U´
) is a type constructor.  Other types are polykinded; they are neither proper types nor type constructors.
As a consequece, AnyKind
itself is polykinded.
Nothing
is universallykinded: it has all kinds at the same time, since it conforms to all types.
With this representation, it is rarely necessary to explicitly talk about the kinds of types. Usually, the kinds of types are implicit through their bounds.
Another way to look at it is that type bounds are kinds. They represent sets of types: ´>: L <: H´ denotes the set of types ´T´ such that ´L <: T´ and ´T <: H´. A set of types can be seen as a type of types, i.e., as a kind.
Conventions
Type bounds are formally always of the form ´>: L <: H´
.
By convention, we can omit either of both bounds in writing.
 When omitted, the lower bound ´L´ is
Nothing
.  When omitted, the higher bound ´H´ is
Any
(notAnyKind
).
These conventions correspond to the defaults in the concrete syntax.
Proper Types
Proper types are also called value types, as they represent sets of values.
Stable types are value types that contain exactly one nonnull
value.
Stable types can be used as prefixes in named designator types.
The stable types are
 designator types referencing a stable term,
 this types,
 super types,
 literal types,
 recursive this types, and
 skolem types.
Every stable type ´T´ is concrete and has an underlying type ´U´ such that ´T <: U´.
Type Constructors
To each type constructor corresponds an inferred type parameter clause which is computed as follows:
 For a type lambda, its type parameter clause (including variance annotations).
 For a polymorphic class type, the type parameter clause of the referenced class definition.
 For a nonclass type designator, the inferred clause of its upper bound.
Type Definitions
A type definition ´D´ represents the righthandside of a type
member definition or the bounds of a type parameter.
It is either:
 a type alias of the form ´= U´, or
 an abstract type definition with bounds ´>: L <: H´.
All type definitions have a lower bound ´L´ and an upper bound ´H´, which are types. For type aliases, ´L = H = U´.
The type definition of a type parameter is never a type alias.
Types
Type Lambdas
A type lambda of the form [´\pm a_1 >: L_1 <: H_1´, ..., ´\pm a_n >: L_n <: H_n´] =>> ´U´
is a direct representation of a type constructor with ´n´ type parameters.
When applied to ´n´ type arguments that conform to the specified bounds, it produces another type ´U´.
Type lambdas are always concrete types.
The scope of a type parameter extends over the result type ´U´ as well as the bounds of the type parameters themselves.
All type constructors conform to some type lambda.
The type bounds of the parameters of a type lambda are in contravariant position, while its result type is in covariant position.
If some type constructor ´T <:´ [´\pm a_1 >: L_1 <: H_1´, ..., ´\pm a_n >: L_n <: H_n´] =>> ´U´
, then ´T´'s ´i´th type parameter bounds contain the bounds ´>: L_i <: H_i´, and its result type conforms to ´U´.
Note: the concrete syntax of type lambdas does not allow to specify variances for type parameters. Instead, variances are inferred from the body of the lambda to be as general as possible.
Example
Designator Types
A designator type (or designator for short) is a reference to a definition. Term designators refer to term definitions, while type designators refer to type definitions.
In the abstract syntax, the id
retains whether it is a term or type.
In the concrete syntax, an id
refers to a type designator, while id.type
refers to a term designator.
In that context, term designators are often called singleton types.
Designators with an empty prefix ´\epsilon´ are called direct designators. They refer to local definitions available in the scope:
 Local
type
,object
,val
,lazy val
,var
ordef
definitions  Term or type parameters
The id
s of direct designators are protected from accidental shadowing in the abstract syntax.
They retain the identity of the exact definition they refer to, rather than relying on scopebased name resolution. ^{1}
The ´\epsilon´ prefix cannot be written in the concrete syntax.
A bare id
is used instead and resolved based on scopes.
Named designators refer to member definitions of a nonempty prefix:
 Toplevel definitions, including toplevel classes, have a package ref prefix
 Class member definitions and refinements have a type prefix
Term Designators
A term designator ´p.x´ referring to a term definition t
has an underlying type ´U´.
If ´p = \epsilon´ or ´p´ is a package ref, the underlying type ´U´ is the declared type of t
and ´p.x´ is a stable type if an only if t
is a val
or object
definition.
Otherwise, the underlying type ´U´ and whether ´p.x´ is a stable type are determined by memberType
(´p´, ´x´)
.
All term designators are concrete types.
If scala.Null ´<: U´
, the term designator denotes the set of values consisting of null
and the value denoted by ´t´, i.e., the value ´v´ for which t eq v
.
Otherwise, the designator denotes the singleton set only containing ´v´.
Type Designators
A type designator ´p.C´ referring to a class definition (including traits and hidden object classes) is a class type. If the class is monomorphic, the type designator is a value type denoting the set of instances of ´C´ or any of its subclasses. Otherwise it is a type constructor with the same type parameters as the class definition. All class types are concrete, nonstable types.
If a type designator ´p.T´ is not a class type, it refers to a type definition T
(a type parameter or a type
member definition) and has an underlying type definition.
If ´p = \epsilon´ or ´p´ is a package ref, the underlying type definition is the declared type definition of T
.
Otherwise, it is determined by memberType
(´p´, ´T´)
.
A nonclass type designator is concrete (resp. stable) if and only if its underlying type definition is an alias ´U´ and ´U´ is itself concrete (resp. stable).
Parameterized Types
A parameterized type ´T[T_1, ..., T_n]´ consists of a type constructor ´T´ and type arguments ´T_1, ..., T_n´ where ´n \geq 1´. The parameterized type is wellformed if
 ´T´ is a type constructor which takes ´n´ type parameters ´a_1, ..., a_n´, i.e., it must conform to a type lambda of the form ´[\pm a_1 >: L_1 <: H_1, ..., \pm a_n >: L_n <: H_n] => U´, and
 if ´T´ is an abstract type constructor, none of the type arguments is a wildcard type argument, and
 each type argument conforms to its bounds, i.e., given ´\sigma´ the substitution ´[a_1 := T_1, ..., a_n := T_n]´, for each type ´i´:
 if ´T_i´ is a type and ´\sigma L_i <: T_i <: \sigma H_i´, or
 ´T_i´ is a wildcard type argument ´? >: L_{Ti} <: H_{Ti}´ and ´\sigma L_i <: L_{Ti}´ and ´H_{Ti} <: \sigma H_i´.
´T[T_1, ..., T_n]´ is a parameterized class type if and only if ´T´ is a class type. All parameterized class types are value types.
In the concrete syntax of wildcard type arguments, if both bounds are omitted, the real bounds are inferred from the bounds of the corresponding type parameter in the target type constructor (which must be concrete).
If only one bound is omitted, Nothing
or Any
is used, as usual.
Also in the concrete syntax, _
can be used instead of ?
for compatibility reasons, with the same meaning.
This alternative will be deprecated in the future, and is already deprecated under source:future
.
Simplification Rules
Wildcard type arguments used in covariant or contravariant positions can always be simplified to regular types.
Let ´T[T_1, ..., T_n]´ be a parameterized type for a concrete type constructor. Then, applying a wildcard type argument ´? >: L <: H´ at the ´i´'th position obeys the following equivalences:
 If the type parameter ´T_i´ is declared covariant, then ´T[..., ? >: L <: H, ...] =:= T[..., H, ...]´.
 If the type parameter ´T_i´ is declared contravariant, then ´T[..., ? >: L <: H, ...] =:= T[..., L, ...]´.
Example Parameterized Types
Given the partial type definitions:
the following parameterized types are wellformed:
and the following types are illformed:
The following code also contains an illformed type:
This Types
A this type ´C´.this
denotes the this
value of class ´C´ within ´C´.
This types often appear implicitly as the prefix of designator types referring to members of ´C´. They play a particular role in the type system, since they are affected by the as seen from operation on types.
This types are stable types.
The underlying type of ´C´.this
is the self type of ´C´.
Super Types
A super type ´C´.super[´D´]
denotes the this
value of class C
within C
, but "widened" to only see members coming from a parent class or trait ´D´.
Super types exist for compatibility with Scala 2, which allows shadowing of inner classes. In a Scala 3only context, a super type can always be replaced by the corresponding this type. Therefore, we omit further discussion of super types in this specification.
Literal Types
A literal type lit
denotes the single literal value lit
.
Thus, the type ascription 1: 1
gives the most precise type to the literal value 1
: the literal type 1
.
At run time, an expression e
is considered to have literal type lit
if e == lit
.
Concretely, the result of e.isInstanceOf[lit]
and e match { case _ : lit => }
is determined by evaluating e == lit
.
Literal types are available for all primitive types, as well as for String
.
However, only literal types for Int
, Long
, Float
, Double
, Boolean
, Char
and String
can be expressed in the concrete syntax.
Literal types are stable types. Their underlying type is the primitive type containing their value.
Example
ByName Types
A byname type ´=> T´ denotes the declared type of a byname term parameter. Byname types can only appear as the types of parameters in method types, and as type arguments in parameterized types.
Annotated Types
An annotated type ´T a´ attaches the annotation ´a´ to the type ´T´.
Example
The following type adds the @suspendable
annotation to the type String
:
Refined Types
A refined type ´T { R }´ denotes the set of values that belong to ´T´ and also have a member conforming to the refinement ´R´.
The refined type ´T { R }´ is wellformed if:
 ´T´ is a proper type, and
 if ´R´ is a term (
def
orval
) refinement, the refined type is a proper type, and  if ´R´ overrides a member of ´T´, the usual rules for overriding apply, and
 if ´R´ is a
def
refinement with a polymorphic method type, then ´R´ overrides a member definition of ´T´.
As an exception to the last rule, a polymorphic method type refinement is allowed if ´T <:´ scala.PolyFunction
and ´id´ is the name apply
.
If the refinement ´R´ overrides no member of ´T´ and is not an occurrence of the scala.PolyFunction
exception, the refinement is said to be “structural” ^{2}.
Note: since a refinement does not define a class, it is not possible to use a this type to reference term and type members of the parent type ´T´ within the refinement. When the surface syntax of refined types makes such references, a recursive type wraps the refined type, given access to members of self through a recursivethis type.
Example
Given the following class definitions:
We get the following conformance relationships:
U <: T { def foo: Int }
U <: T { def fooPoly[A](x: A): A }
U <: (T { def foo: Int }) { def fooPoly[A](x: A): A }
(we can chain refined types to refine multiple members)V <: T { type X <: Some[Any] }
V <: T { type X >: Some[Nothing] }
V <: T { type X = Some[Int] }
V <: T { def bar: Any }
(a structural refinement)
The following refined types are not wellformed:
T { def barPoly[A](x: A): A }
(structural refinement for a polymorphic method type)T { type X <: List[Any] }
(does not satisfy overriding rules)List { def head: Int }
(the parent typeList
is not a proper type)T { def foo: List }
(the refined typeList
is not a proper type)T { def foo: T.this.X }
(T.this
is not allowed outside the body ofT
)
Recursive Types
A recursive type of the form { ´\alpha´ => ´T´ }
represents the same values as ´T´, while offering ´T´ access to its recursive this type ´\alpha´
.
Recursive types cannot directly be expressed in the concrete syntax.
They are created as needed when a refined type in the concrete syntax contains a refinement that needs access to the this
value.
Each recursive type defines a unique selfreference ´\alpha´
, distinct from any other recursive type in the system.
Recursive types can be unfolded during subtyping as needed, replacing references to its ´\alpha´
by a stable reference to the other side of the conformance relationship.
Example
Given the class definitions in the refined types section, we can write the following refined type in the source syntax:
This type is not directly expressible as a refined type alone, as the refinement cannot access the this
value.
Instead, in the abstract syntax of types, it is translated to { ´\alpha´ => ´T´ { def foo: ´\alpha´.X } }
.
Given the following definitions:
we can check that z ´<:´ { ´\alpha´ => ´T´ { def foo: ´\alpha´.X } }
.
We first unfold the recursive type, substituting ´z´ for ´\alpha´, resulting in z ´<:´ T { def foo: z.X }
.
Since the underlying type of ´z´ is ´Z´, we can resolve z.X
to mean Option[Int]
, and then validate that z ´<:´ T
and that z
has a member def foo: Option[Int]
.
Union and Intersection Types
Syntactically, the types S  T
and S & T
are infix types, where the infix operators are 
and &
, respectively (see infix types).
However, in this specification, ´S ｜ T´ and ´S ＆ T´ refer to the underlying core concepts of union and intersection types, respectively.
 The type ´S ｜ T´ represents the set of values that are represented by either ´S´ or ´T´.
 The type ´S ＆ T´ represents the set of values that are represented by both ´S´ and ´T´.
From the conformance rules rules on union and intersection types, we can show that ´＆´ and ´｜´ are commutative and associative.
Moreover, ＆
is distributive over ｜
.
For any type ´A´, ´B´ and ´C´, all of the following relationships hold:
 ´A ＆ B =:= B ＆ A´,
 ´A ｜ B =:= B ｜ A´,
 ´(A ＆ B) ＆ C =:= A ＆ (B ＆ C)´,
 ´(A ｜ B) ｜ C =:= A ｜ (B ｜ C)´, and
 ´A ＆ (B ｜ C) =:= (A ＆ B) ｜ (A ＆ C)´.
If ´C´ is a co or contravariant type constructor, ´C[A] ＆ C[B]´ can be simplified using the following rules:
 If ´C´ is covariant, ´C[A] ＆ C[B] =:= C[A ＆ B]´
 If ´C´ is contravariant, ´C[A] ＆ C[B] =:= C[A  B]´
The righttoleft validity of the above two rules can be derived from the definition of covariance and contravariance and the conformance rules of union and intersection types:
 When ´C´ is covariant, we can derive ´C[A ＆ B] <: C[A] ＆ C[B]´.
 When ´C´ is contravariant, we can derive ´C[A ｜ B] <: C[A] ＆ C[B]´.
Join of a union type
In some situations, a union type might need to be widened to a nonunion type. For this purpose, we define the join of a union type ´T_1 ｜ ... ｜ T_n´ as the smallest intersection type of base class instances of ´T_1, ..., T_n´. Note that union types might still appear as type arguments in the resulting type, this guarantees that the join is always finite.
For example, given
The join of ´A ｜ B´ is ´C[A ｜ B] ＆ D´
Skolem Types
Skolem types cannot directly be written in the concrete syntax.
Moreover, although they are proper types, they can never be inferred to be part of the types of term definitions (val
s, var
s and def
s).
They are exclusively used temporarily during subtyping derivations.
Skolem types are stable types. A skolem type of the form ´∃ \alpha : T´ represents a stable reference to unknown value of type ´T´. The identifier ´\alpha´ is chosen uniquely every time a skolem type is created. However, as a skolem type is stable, it can be substituted in several occurrences in other types. When "copied" through substitution, all the copies retain the same ´\alpha´, and are therefore equivalent.
Methodic Types
Methodic types are not real types. They are not part of the type lattice.
However, they share some metaproperties with types. In particular, when contained within other types that undertake some substitution, the substitution carries to the types within methodic types. It is therefore often convenient to think about them as types themselves.
Methodic types are used as the "declared type" of def
definitions that have at least one term or type parameter list.
Method Types
A method type is denoted internally as ´(\mathit{Ps})U´, where ´(\mathit{Ps})´ is a sequence of parameter names and types ´(p_1:T_1, ..., p_n:T_n)´ for some ´n \geq 0´ and ´U´ is a (value or method) type. This type represents named methods that take arguments named ´p_1, ..., p_n´ of types ´T_1, ..., T_n´ and that return a result of type ´U´.
Method types associate to the right: ´(\mathit{Ps}_1)(\mathit{Ps}_2)U´ is treated as ´(\mathit{Ps}_1)((\mathit{Ps}_2)U)´.
Method types do not exist as types of values. If a method name is used as a value, its type is implicitly converted to a corresponding function type.
Example
The definitions
produce the typings
Polymorphic Method Types
A polymorphic method type, or poly type for short, is denoted internally as [´\mathit{tps}\,´]´T´
where [´\mathit{tps}\,´]
is a type parameter section [´a_1´ >: ´L_1´ <: ´U_1, ..., a_n´ >: ´L_n´ <: ´U_n´]
for some ´n \geq 0´ and ´T´ is a (value or method) type.
This type represents named methods that take type arguments ´S_1, ..., S_n´
which conform to the lower bounds ´L_1, ..., L_n´
and the upper bounds ´U_1, ..., U_n´
and that yield results of type ´T´.
Example
The definitions
produce the typings
Operations on Types
This section defines a few metafunctions on types and methodic types.
baseType(´T´, ´C´)
: computes the smallest type ´U´ of the form´p´.´C´[´T_1, ..., T_n´]
such that ´T <: U´.asSeenFrom(´T´, ´C´, ´p´)
: rebases the type ´T´ visible inside the class ´C´ "as seen from" the prefix ´p´.memberType(´T´, ´id´)
: finds a member of a type (T.id
) and computes its underlying type or bounds.
These metafunctions are mutually recursive.
Base Type
The metafunction baseType(´T´, ´C´)
, where ´T´ is a proper type and ´C´ is a class identifier, computes the smallest type ´U´ of the form ´p.C´
or ´p.C´[´U_1, ..., U_n´]
such that ´T <: U´.
If no such type exists, the function is not defined.
The main purpose of baseType
is to substitute prefixes and class type parameters along the inheritance chain.
We define baseType(´T´, ´C´)
as follows.
For brevity, we write ´p.X´[´U_1, ..., U_n´]
instead of ´p.X´
with ´n = 0´.
baseType(´T = p.C´[´T_1, ..., T_n´], ´C´) ´≜ T´
baseType(´p.D´[´T_1, ..., T_n´], ´C´)
with´D´ ≠ ´C ≜ \sigma W´
if ´Q´ is defined where ´D´ is declared as
´D[\pm a_1 >: L_1 <: H_1, ..., \pm a_n >: L_n <: H_n]´ extends ´P_1, ..., P_m´
´Q =´ meet(baseType(´P_i´, ´C´)
for all ´i´ such thatbaseType(´P_i´, ´C´)
is defined)
´W = Q´
if ´p = \epsilon´ or if ´p´ is a package ref; otherwise,´W =´ asSeenFrom(´Q´, ´D´, ´p´)
(in that case, ´p´ is a stable type and ´D´ must be declared inside another class ´B´)´\sigma = [a_1 := T_1, ..., a_n := T_n]´
the substitution of the declared type parameters of ´D´ by the actual type arguments
 ´D´ is declared as
baseType(´T_1 ＆ T_2´, ´C´) ´≜´ meet´(´baseType(´T_1´, ´C´), baseType(´T_2´, ´C´)´)´
baseType(´T_1 ｜ T_2´, ´C´) ´≜´ join´(´baseType(´T_1´, ´C´), baseType(´T_2´, ´C´)´)´
baseType(´T´, ´C´) ´≜´ baseType(superType(´T´), ´C´)
ifsuperType(´T´)
is defined
The definition above uses the following helper functions.
superType(´T´)
computes the "next upper bound" of ´T´, if it exists:
superType(´T´)
where ´T´ is a stable type is its underlying typesuperType(´p.X´)
where ´p.X´ is a nonclass type designator is the upper bound of its underlying type definitionsuperType(´([a_1 >: L_1 <: H_1, ..., a_n >: L_n <: H_n]´ =>> ´U)[T_1, ..., T_n]´)
is´[a_1 =: T_1, ..., a_n := T_n]U´
(i.e., the betareduction of the type lambda redex)superType(´T[T_1, ..., T_n]´)
issuperType(´T´)´[T_1, ..., T_n]´
ifsuperType(´T´)
is defined
Note that the cases of superType
do not overlap with each other nor with any baseType
case other than the superType
based one.
The cases of baseType
therefore do not overlap with each other either.
That makes baseType
an algorithmic partial function.
meet(´p.C[T_1, ..., T_n]´, ´q.C[U_1, ..., U_n]´)
computes an intersection of two (parameterized) class types for the same class, and join
computes a union:
 if
´p =:= q´
is false, then it is not defined  otherwise, let ´W_i´ for ´i \in 1, ..., n´ be:
 ´T_i ＆ U_i´ for
meet
(resp. ´T_i ｜ U_i´ forjoin
) if the ´i´th type parameter of ´C´ is covariant  ´T_i ｜ U_i´ for
meet
(resp. ´T_i ＆ U_i´ forjoin
) if the ´i´th type parameter of ´C´ is contravariant  ´T_i´ if ´T_i =:= U_i´ and the ´i´th type parameter of ´C´ is invariant
 not defined otherwise
 ´T_i ＆ U_i´ for
 if any of the ´W_i´ are not defined, the result is not defined
 otherwise, the result is
´p.C[W_1, ..., W_n]´
We generalize meet(´T_1, ..., T_n´)
for a sequence as:
 not defined for ´n = 0´
 ´T_1´ if ´n = 1´
meet(meet(´T_1, ..., T_{n1}´), ´T_n´)
ifmeet(´T_1, ..., T_{n1}´)
is defined not defined otherwise
Examples
Given the following definitions:
we have the following baseType
results:
baseType(List[Int], List) = List[Int]
baseType(List[Int], Iterable) = Iterable[Int]
baseType(List[A] & Iterable[B], Iterable) = meet(Iterable[A], Iterable[B]) = Iterable[A & B]
baseType(List[A] & Foo, Iterable) = Iterable[A]
(becausebaseType(Foo, Iterable)
is not defined)baseType(Int, Iterable)
is not definedbaseType(Map[Int, String], Iterable) = Iterable[(Int, String)]
baseType(Map[Int, String] & Map[String, String], Map)
is not defined (becauseK
is invariant)
As Seen From
The metafunction asSeenFrom(´T´, ´C´, ´p´)
, where ´T´ is a type or methodic type visible inside the class ´C´ and ´p´ is a stable type, rebases the type ´T´ "as seen from" the prefix ´p´.
Essentially, it substitutes thistypes and class type parameters in ´T´ to appropriate types visible from outside.
Since T
is visible inside ´C´, it can contain thistypes and class type parameters of ´C´ itself as well as of all its enclosing classes.
Thistypes of enclosing classes must be mapped to appropriate subprefixes of ´p´, while class type parameters must be mapped to appropriate concrete type arguments.
asSeenFrom(´T´, ´C´, ´p´)
only makes sense if ´p´ has a base type for ´C´, i.e., if baseType(´p´, ´C´)
is defined.
We define asSeenFrom(´T´, ´C´, ´p´)
where baseType(´p´, ´C´) = ´q.C[U_1, ..., U_n]´
as follows:
 If ´T´ is a reference to the ´i´th class type parameter of some class ´D´:
 If
baseType(´p´, ´D´) ´= r.D[W_1, ..., W_m]´
is defined, then ´W_i´  Otherwise, if ´q = \epsilon´ or ´q´ is a package ref, then ´T´
 Otherwise, ´q´ is a type, ´C´ must be defined in another class ´B´ and
baseType(´q´, ´B´)
must be defined, thenasSeenFrom(´T´, ´B´, ´q´)
 If
 Otherwise, if ´T´ is a thistype
´D´.this
: If ´D´ is a subclass of ´C´ and
baseType(´p´, ´D´)
is defined, then ´p´ (this is always the case when ´D = C´)  Otherwise, if ´q = \epsilon´ or ´q´ is a package ref, then ´T´
 Otherwise, ´q´ is a type, ´C´ must be defined in another class ´B´ and
baseType(´q´, ´B´)
must be defined, thenasSeenFrom(´T´, ´B´, ´q´)
 If ´D´ is a subclass of ´C´ and
 Otherwise, ´T´ where each if of its type components ´T_i´ is mapped to
asSeenFrom(´T_i´, ´C´, ´p´)
.
For convenience, we generalize asSeenFrom
to type definitions ´D´.
 If ´D´ is an alias ´= U´, then
asSeenFrom(´D´, ´C´, ´p´) = asSeenFrom(´U´, ´C´, ´p´)
.  If ´D´ is an abstract type definition with bounds ´>: L <: H´, then
asSeenFrom(´D´, ´C´, ´p´) = ´>:´ asSeenFrom(´L´, ´C´, ´p´) ´<:´ asSeenFrom(´H´, ´C´, ´p´)
.
Member Type
The metafunction memberType(´T´, ´id´, ´p´)
, where ´T´ is a proper type, ´id´ is a term or type identifier, and ´p´ is a stable type, finds a member of a type (T.id
) and computes its underlying type (for a term) or type definition (for a type) as seen from the prefix ´p´.
For a term, it also computes whether the term is stable.
memberType
is the fundamental operation that computes the underlying type or underlying type definition of a named designator type.
The result ´M´ of a memberType
is one of:
 undefined,
 a term result with underlying type or methodic type ´U´ and a stable flag,
 a class result with class ´C´, or
 a type result with underlying type definition ´D´.
As shorthand, we define memberType(´T´, ´id´)
to be the same as memberType(´T´, ´id´, ´T´)
when ´T´ is a stable type.
We define memberType(´T´, ´id´, ´p´)
as follows:
 If ´T´ is a possibly parameterized class type of the form ´q.C[T_1, ..., T_n]´ (with ´n \geq 0´):
 Let ´m´ be the class member of ´C´ with name ´id´.
 If ´m´ is not defined, the result is undefined.
 If ´m´ is a class definition, the result is a class result with class ´m´.
 If ´m´ is a term definition in class ´D´ with declared type ´U´, the result is a term result with underlying type
asSeenFrom
(´U´, ´D´, ´p´)
and stable flag true if and only if ´m´ is stable.  If ´m´ is a type member definition in class ´D´, the result is a type result with underlying type definition
asSeenFrom
(´U´, ´D´, ´p´)
where ´U´ is defined as follows: If ´m´ is an opaque type alias member definition with declared definition ´>: L <: H = V´, then
 ´U´ is ´= V´ if
´p = D.´this
or if we are computingmemberType
in a transparent mode,  ´U´ is ´>: L <: H´ otherwise.
 ´U´ is ´= V´ if
 ´U´ is the declared type definition of ´m´ otherwise.
 If ´m´ is an opaque type alias member definition with declared definition ´>: L <: H = V´, then
 If ´T´ is another monomorphic type designator of the form ´q.X´:
 Let ´U´ be
memberType(´q´, ´X´)
 Let ´H´ be the upper bound of ´U´
 The result is
memberType(´H´, ´id´, ´p´)
 Let ´U´ be
 If ´T´ is another parameterized type designator of the form ´q.X[T_1, ..., T_n]´ (with ´n \geq 0´):
 Let ´U´ be
memberType(´q´, ´X´)
 Let ´H´ be the upper bound of ´U´
 The result is
memberType(´H[T_1, ..., T_n]´, ´id´, ´p´)
 Let ´U´ be
 If ´T´ is a parameterized type lambda of the form
´([\pm a_1 >: L_1 <: H_1, ..., \pm a_n >: L_n <: H_n]´ =>> ´U)[T_1, ..., T_n]´
: The result is
memberType(´[a_1 := T_1, ..., a_n := T_n] U´, ´id´, ´p´)
, i.e., we betareduce the type redex.
 The result is
 If ´T´ is a refined type of the form
´T_1´ { ´R´ }
: Let ´M_1´ be the result of
memberType(´T_1´, ´id´, ´p´)
.  If the name of the refinement ´R´ is not ´id´, let ´M_2´ be undefined.
 Otherwise, let ´M_2´ be the type or type definition of the refinement ´R´, as well as whether it is stable.
 The result is
mergeMemberType(´M_1´, ´M_2´)
.
 Let ´M_1´ be the result of
 If ´T´ is a union type of the form ´T_1 ｜ T_2´:
 Let ´J´ be the join of ´T´.
 The result is
memberType(´J´, ´id´, ´p´)
.
 If ´T´ is an intersection type of the form ´T_1 ＆ T_2´:
 Let ´M_1´ be the result of
memberType(´T_1´, ´id´, ´p´)
.  Let ´M_2´ be the result of
memberType(´T_2´, ´id´, ´p´)
.  The result is
mergeMemberType(´M_1´, ´M_2´)
.
 Let ´M_1´ be the result of
 If ´T´ is a recursive type of the form
{ ´\alpha´ => ´T_1´ }
: The result is
memberType(´T_1´, ´id´, ´p ´)
.
 The result is
 If ´T´ is a stable type:
 Let ´U´ be the underlying type of ´T´.
 The result is
memberType(´U´, ´id´, ´p´)
.
 Otherwise, the result is undefined.
We define the helper function mergeMemberType(´M_1´, ´M_2´)
as:
 If either ´M_1´ or ´M_2´ is undefined, the result is the other one.
 Otherwise, if either ´M_1´ or ´M_2´ is a class result, the result is that one.
 Otherwise, ´M_1´ and ´M_2´ must either both be term results or both be type results.
 If they are term results with underlying types ´U_1´ and ´U_2´ and stable flags ´s_1´ and ´s_2´, the result is a term result whose underlying type is
meet(´U_1´, ´U_2´)
and whose stable flag is ´s_1 \lor s_2´.  If they are type results with underlying type definitions ´D_1´ and ´D_2´, the result is a type result whose underlying type definition is
intersect(´D_1´, ´D_2´)
.
 If they are term results with underlying types ´U_1´ and ´U_2´ and stable flags ´s_1´ and ´s_2´, the result is a term result whose underlying type is
Relations between types
We define the following relations between types.
Name  Symbolically  Interpretation 

Conformance  ´T <: U´  Type ´T´ conforms to ("is a subtype of") type ´U´. 
Equivalence  ´T =:= U´  ´T´ and ´U´ conform to each other. 
Weak Conformance  ´T <:_w U´  Augments conformance for primitive numeric types. 
Compatibility  Type ´T´ conforms to type ´U´ after conversions. 
Conformance
The conformance relation ´(<:)´ is the smallest relation such that ´S <: T´ is true if any of the following conditions hold. Note that the conditions are not all mutually exclusive.
 ´S = T´ (i.e., conformance is reflexive by definition).
 ´S´ is
Nothing
.  ´T´ is
AnyKind
.  ´S´ is a stable type with underlying type ´S_1´ and ´S_1 <: T´.
 ´S = p.x´ and ´T = q.x´ are term designators and
isSubPrefix(´p´, ´q´)
.
 ´S = p.X[S_1, ..., S_n]´ and ´T = q.X[T_1, ..., T_n]´ are possibly parameterized type designators with ´n \geq 0´ and:
isSubPrefix(´p´, ´q´)
, and it is not the case that ´p.x´ and ´q.X´ are class type designators for different classes, and
 for each ´i \in { 1, ..., n }´:
 the ´i´th type parameter of ´q.X´ is covariant and ´S_i <: T_i´ ^{3}, or
 the ´i´th type parameter of ´q.X´ is contravariant and ´T_i <: S_i´ ^{3}, or
 the ´i´th type parameter of ´q.X´ is invariant and:
 ´S_i´ and ´T_i´ are types and ´S_i =:= T_i´, or
 ´S_i´ is a type and ´T_i´ is a wildcard type argument of the form ´? >: L_2 <: H_2´ and ´L_2 <: S_i´ and ´S_i <: H_2´, or
 ´S_i´ is a wildcard type argument of the form ´? >: L_1 <: H_1´ and ´T_i´ is a wildcard type argument of the form ´? >: L_2 <: H_2´ and ´L_2 <: L_1´ and ´H_1 <: H_2´ (i.e., the ´S_i´ "interval" is contained in the ´T_i´ "interval").
 ´T = q.C[T_1, ..., T_n]´ with ´n \geq 0´ and
baseType(´S´, ´C´)
is defined andbaseType(´S´, ´C´) ´<: T´
.  ´S = p.X[S_1, ..., S_n]´ and ´p.X´ is nonclass type designator and ´H <: T´ where ´H´ is the upper bound of the underlying type definition of ´p.X´.
 ´S = p.C´ and
´T = C´.this
and ´C´ is the hidden class of anobject
and: ´p = \epsilon´ or ´p´ is a package ref, or
isSubPrefix(´p´, ´D´.this)
where ´D´ is the enclosing class of ´C´.
´S = C´.this
and ´T = q.C´ and ´C´ is the hidden class of anobject
and: either ´q = \epsilon´ or ´q´ is a package ref, or
isSubPrefix(´D´.this, ´q´)
where ´D´ is the enclosing class of ´C´.
 ´S = S_1 ｜ S_2´ and ´S_1 <: T´ and ´S_2 <: T´.
 ´T = T_1 ｜ T_2´ and either ´S <: T_1´ or ´S <: T_2´.
 ´T = T_1 ＆ T_2´ and ´S <: T_1´ and ´S <: T_2´.
 ´S = S_1 ＆ S_2´ and either ´S_1 <: T´ or ´S_2 <: T´.
´S = S_1´ @a
and ´S_1 <: T´.´T = T_1´ @a
and ´S <: T_1´ (i.e., annotations can be dropped). ´T = q.X´ and ´q.X´ is a nonclass type designator and ´S <: L´ where ´L´ is the lower bound of the underlying type definition of ´q.X´.
 ´S = p.X´ and ´p.X´ is a nonclass type designator and ´H <: T´ where ´H´ is the upper bound of the underlying type definition of ´p.X´.
´S = [\pm a_1 >: L_1 <: H_1, ..., \pm a_n >: L_n <: H_n]´ =>> ´S_1´
and´T = [\pm b_1 >: M_1 <: G_1, ..., \pm b_n >: M_n <: G_n]´ =>> ´T_1´
, and given ´\sigma = [b_1 := a_1, ..., b_n := a_n]´: ´S_1 <: \sigma T_1´, and
 for each ´i \in { 1, ..., n }´:
 the variance of ´a_i´ conforms to the variance of ´b_i´ (´+´ conforms to ´+´ and ´\epsilon´, ´´ conforms to ´´ and ´\epsilon´, and ´\epsilon´ conforms to ´\epsilon´), and
 ´\sigma (>: M_i <: G_i)´ is contained in ´>: L_i <: H_i´ (i.e., ´L_i <: \sigma M_i´ and ´\sigma G_i <: H_i´).
 ´S = p.X´ and
´T = [\pm b_1 >: M_1 <: G_1, ..., \pm b_n >: M_n <: G_n]´ =>> ´T_1´
and ´S´ is a type constructor with ´n´ type parameters and:´([\pm a_1 >: L_1 <: H_1, ..., \pm a_n >: L_n <: H_n]´ =>> ´S[a_1, ..., a_n]) <: T´
where the ´a_i´ are copies of the type parameters of ´S´ (i.e., we can etaexpand ´S´ to compare it to a type lambda).
´T = T_1´ { ´R´ }
and ´S <: T_1´ and, given ´p = S´ if ´S´ is a stable type and ´p = ∃ \alpha : S´ otherwise:´R =´ type ´X >: L <: H´
andmemberType(´p´, ´X´)
is a class result for ´C´ and ´L <: p.C´ and ´p.C <: H´, or´R =´ type ´X >: L_2 <: H_2´
andmemberType(´p´, ´X´)
is a type result with bounds ´>: L_1 <: H_1´ and ´L_2 <: L_1´ and ´H_1 <: H_2´, or´R =´ val ´X: T_2´
andmemberType(´p´, ´X´)
is a stable term result with type ´S_2´ and ´S_2 <: T_2´, or´R =´ def ´X: T_2´
andmemberType(´p´, ´X´)
is a term result with type ´S_2´ and ´T_2´ is a type and ´S_2 <: T_2´, or´R =´ def ´X: T_2´
andmemberType(´p´, ´X´)
is a term result with methodic type ´S_2´ and ´T_2´ is a methodic type andmatches(´S_2´, ´T_2´)
.
´S = S_1´ { ´R´ }
and ´S_1 <: T´.´S =´ { ´\alpha´ => ´S_1´ }
and´T =´ { ´\beta´ => ´T_1´ }
and ´S_1 <: [\beta := \alpha]T_1´.´T =´ { ´\beta´ => ´T_1´ }
and ´S´ is a proper type but not a recursive type and ´p' <: [\beta := p]T_1´ where: ´p´ is ´S´ if ´S´ is a stable type and ´∃ \alpha : S´ otherwise, and
 ´p'´ is the result of replacing any toplevel recursive type
{ ´\gamma´ => ´Z´ }
in ´p´ with ´[\gamma := p]Z´ (TODO specify this better).
´S = (´=> ´S_1)´
and´T = (´=> ´T_1)´
and ´S_1 <: T_1´.´S =´ scala.Null
and: ´T = q.C[T_1, ..., T_n]´ with ´n \geq 0´ and ´C´ does not derive from
scala.AnyVal
and ´C´ is not the hidden class of anobject
, or  ´T = q.x´ is a term designator with underlying type ´U´ and
scala.Null ´<: U´
, or ´T = T_1´ { ´R´ }
andscala.Null ´<: T_1´
, or´T =´ { ´\beta´ => ´T_1´ }
andscala.Null ´<: T_1´
.
 ´T = q.C[T_1, ..., T_n]´ with ´n \geq 0´ and ´C´ does not derive from
 ´S´ is a stable type and ´T = q.x´ is a term designator with underlying type ´T_1´ and ´T_1´ is a stable type and ´S <: T_1´.
´S = S_1´ { ´R´ }
and ´S_1 <: T´.´S =´ { ´\alpha´ => ´S_1´ }
and ´S_1 <: T´.´T =´ scala.Tuple´_n[T_1, ..., T_n]´
with ´1 \leq n \leq 22´, and´S <: T_1´ *: ... *: ´T_n´ *: scala.EmptyTuple
.
We define isSubPrefix(´p´, ´q´)
where ´p´ and ´q´ are prefixes as:
 If both ´p´ and ´q´ are types, then ´p <: q´.
 Otherwise, ´p = q´ (for empty prefixes and package refs).
We define matches(´S´, ´T´)
where ´S´ and ´T´ are types or methodic types as:
 If ´S´ and ´T´ are types, then ´S <: T´.
 If ´S´ and ´T´ are method types ´(a_1: S_1, ..., a_n: S_n)S'´ and ´(b_1: T_1, ..., b_n: T_n)T'´, then ´\sigma S_i =:= T_i´ for each ´i´ and
matches(´\sigma S'´, ´T'´)
, where ´\sigma = [a_1 := b_1, ..., a_n := b_n]´.  If ´S´ and ´T´ are poly types ´[a_1 >: L_{s1} <: H_{s1}, ..., a_n >: L_{sn} <: H_{sn}]S'´ and ´[b_1 >: L_{t1} <: H_{t1}, ..., b_n >: L_{tn} <: H_{tn}]T'´, then ´\sigma L_{si} =:= L_{ti}´ and ´\sigma H_{si} =:= H_{ti}´ for each ´i´ and
matches(´\sigma S'´, ´T'´)
, where ´\sigma = [a_1 := b_1, ..., a_n := b_n]´.
Note that conformance in Scala is not transitive.
Given two abstract types ´A´ and ´B´, and one abstract type ´C >: A <: B´
available on prefix ´p´, we have ´A <: p.C´ and ´C <: p.B´ but not necessarily ´A <: B´.
Least upper bounds and greatest lower bounds
The ´(<:)´ relation forms preorder between types, i.e. it is transitive and reflexive. This allows us to define least upper bounds and greatest lower bounds of a set of types in terms of that order.
 the least upper bound of
A
andB
is the smallest typeL
such thatA
<:L
andB
<:L
.  the greatest lower bound of
A
andB
is the largest typeG
such thatG
<:A
andG
<:B
.
By construction, for all types A
and B
, the least upper bound of A
and B
is A ｜ B
, and their greatest lower bound is A ＆ B
.
Equivalence
Equivalence is defined as mutual conformance.
´S =:= T´ if and only if both ´S <: T´ and ´T <: S´.
Weak Conformance
In some situations Scala uses a more general conformance relation. A type ´S´ weakly conforms to a type ´T´, written ´S <:_w T´, if ´S <: T´ or both ´S´ and ´T´ are primitive number types and ´S´ precedes ´T´ in the following ordering.
A weak least upper bound is a least upper bound with respect to weak conformance.
Compatibility
A type ´T´ is compatible to a type ´U´ if ´T´ (or its corresponding function type) weakly conforms to ´U´ after applying etaexpansion. If ´T´ is a method type, it's converted to the corresponding function type. If the types do not weakly conform, the following alternatives are checked in order:
 dropping byname modifiers: if ´U´ is of the shape
´=> U'´
(and ´T´ is not),´T <:_w U'´
;  SAM conversion: if ´T´ corresponds to a function type, and ´U´ declares a single abstract method whose type corresponds to the function type ´U'´,
´T <:_w U'´
.  implicit conversion: there's an implicit conversion from ´T´ to ´U´ in scope;
Examples
Function compatibility via SAM conversion
Given the definitions
The application foo((x: Int) => x.toString)
resolves to the first overload, as it's more specific:
Int => String
is compatible toToString
 when expecting a value of typeToString
, you may pass a function literal fromInt
toString
, as it will be SAMconverted to said function;ToString
is not compatible toInt => String
 when expecting a function fromInt
toString
, you may not pass aToString
.
Realizability
A type ´T´ is realizable if and only if it is inhabited by nonnull values. It is defined as:
 A term designator ´p.x´ with underlying type ´U´ is realizable if ´p´ is ´\epsilon´ or a package ref or a realizable type and
memberType(´p´, ´x´)
has the stable flag, or the type returned by
memberType(´p´, ´x´)
is realizable.
 A stable type that is not a term designator is realizable.
 Another type ´T´ is realizable if
 ´T´ is concrete, and
 ´T´ has good bounds.
A concrete type ´T´ has good bounds if all of the following apply:
 all its nonclass type members have good bounds, i.e., their bounds ´L´ and ´H´ are such that ´L <: H´,
 all its type refinements have good bounds, and
 for all base classes ´C´ of ´T´:
baseType(´T´, ´C´)
is defined with some result ´p.C[T_1, ..., T_n]´, and for all ´i \in { 1, ..., n }´, ´T_i´ is a real type or (when it is a wildcard type argument) it has good bounds.
Note: it is possible for baseType(´T´, ´C´)
not to be defined because of the meet
computation, which may fail to merge prefixes and/or invariant type arguments.
Type Erasure
A type is called generic if it contains type arguments or type variables.
Type erasure is a mapping from (possibly generic) types to nongeneric types.
We write ´T´ for the erasure of type ´T´.
The erasure mapping is defined as follows.
Internal computations are performed in a transparent mode, which has an effect on how memberType
behaves for opaque type aliases.
 The erasure of
AnyKind
isObject
.  The erasure of a nonclass type designator is the erasure of its underlying upper bound.
 The erasure of a term designator is the erasure of its underlying type.
 The erasure of the parameterized type
scala.Array´[T_1]´
isscala.Array´[T_1]´
.  The erasure of every other parameterized type ´T[T_1, ..., T_n]´ is ´T´.
 The erasure of a stable type
´p´
is the erasure of the underlying type of ´p´.  The erasure of a byname type
=> ´T_1´
isscala.Function0
.  The erasure of an annotated type ´T_1 a´ is ´T_1´.
 The erasure of a refined type
´T_1´ { ´R´ }
is ´T_1´.  The erasure of a recursive type
{ ´\alpha´ => ´T_1´ }
and the associated recursive this type ´\alpha´ is ´T_1´.  The erasure of a union type ´S ｜ T´ is the erased least upper bound (elub) of the erasures of ´S´ and ´T´.
 The erasure of an intersection type ´S ＆ T´ is the eglb (erased greatest lower bound) of the erasures of ´S´ and ´T´.
The erased LUB is computed as follows:
 if both argument are arrays of objects, an array of the erased LUB of the element types
 if both arguments are arrays of same primitives, an array of this primitive
 if one argument is array of primitives and the other is array of objects,
Object
 if one argument is an array,
Object
 otherwise a common superclass or trait S of the argument classes, with the following two properties:
 S is minimal: no other common superclass or trait derives from S, and
 S is last: in the linearization of the first argument type ´A´ there are no minimal common superclasses or traits that come after S. The reason to pick last is that we prefer classes over traits that way, which leads to more predictable bytecode and (?) faster dynamic dispatch.
The rules for ´eglb(A, B)´ are given below in pseudocode:

In the literature, this is often achieved through De Bruijn indices or through alpharenaming when needed. In a concrete implementation, this is often achieved through retaining symbolic references in a symbol table. ↩

A reference to a structurally defined member (method call or access to a value or variable) may generate binary code that is significantly slower than an equivalent code to a nonstructural member. ↩

In these cases, if
T_i
and/orU_i
are wildcard type arguments, the simplification rules for parameterized types allow to reduce them to real types. ↩