Every value in a Ceylon program is an instance of a type that can be expressed
within the Ceylon language as a *class*. The language does not
define any primitive or compound types that cannot, in principle, be expressed within
the language itself.

A class, fully defined in §4.5 Classes, is a recipe for producing
new values, called *instances*
of the class (or simply *objects*), and defines the operations and
attributes of the resulting values. A class instance may hold references to other
objects, and has an identity distinct from these references.

Each class declaration defines a type. However, not all types are classes. It
is often advantageous to write generic code that abstracts the concrete class of a
value. This technique is called *polymorphism*. Ceylon features
two different kinds of polymorphism:

*subtype polymorphism*, where a subtype`B`inherits a supertype`A`, and*parametric polymorphism*, where a type definition`A<T>`is parameterized by a*generic type parameter*`T`.

Ceylon, like Java and many other object-oriented languages, features a single
inheritance model for classes. A class may directly inherit at most one other class,
and all classes eventually inherit, directly or indirectly, the class
`Anything` defined in the module `ceylon.language`,
which acts as the root of the class hierarchy.

A truly hierarchical type system is much too restrictive for more abstract programming tasks. Therefore, in addition to classes, Ceylon recognizes the following kinds of type:

An

*interface*, defined in §4.4 Interfaces, is an abstract type schema that cannot itself be directly instantiated. An interface may define concrete members, but these members may not hold references to other objects. A class may inherit one or more interfaces. An instance of a class that inherits an interface is also considered an instance of the interface.A

*generic type parameter*, defined in §3.5 Generic type parameters, is considered a type within the declaration that it parameterizes. In fact, it is an abstraction over many types: it generalizes the declaration to all types which could be assigned to the parameter.An

*applied type*, defined in §3.6 Generic type arguments, is formed by specifying arguments for the generic type parameters of a parameterized type.A

*union type*, defined in §3.2.3 Union types, is a type to which each of an enumerated list of types is assignable.An

*intersection type*, defined in §3.2.4 Intersection types, is a type which is assignable to each of an enumerated list of types.

Although we often use the term *parameterized type* or even
*generic type* to refer to a parameterized type definition, it is
important to keep in mind that a parameterized type definition is not itself a type.
Rather, it is a *type constructor*, a function that maps types
to types. Given a list of type arguments, the function yields an applied type.

In light of the fact that Ceylon makes it so easy to construct new types from
existing types *without the use of inheritance*, by forming unions,
intersections, and applied types, it's often useful to assign a name to such a type.

A

*type alias*, defined in §4.6 Type aliases, §4.5.9 Class aliases, and §4.4.5 Interface aliases, is a synonym for an expression involving other types or generic types. A type alias may itself be generic.

The Ceylon type system is much more complete than most other object oriented languages. In Ceylon, it's possible to answer questions that might at first sound almost nonsensical if you're used to languages with more traditional type systems. For example:

What is the type of a variable that may or may not hold a value of type

`Element`?What is the type of a parameter that accepts either an

`Integer`or a`Float`?What is the type of a parameter that accepts values which are instances of both

`Persistent`and`Printable`?What is the type of a function which accepts any non-null value and returns a

`String`?What is the type of a function that accepts one or more

`String`s and returns an iterable object producing at least one`String`?What is the type of a sequence consisting of a

`String`followed by two`Float`s?What is the type of a list with no elements?

The answers, as we shall see, are: `Element?`,
`Integer|Float`, `Persistent&Printable`,
`String(Object)`, `{String+}(String+)`,
`[String,Float,Float]`, and `List<Nothing>`.

It's important that there is always a unique "best" answer to questions
like these in Ceylon. The "best" answer is called the *principal type
of an expression*. Every other type to which the expression is
assignable is a supertype of the principal type.

Thus, every legal Ceylon expression has a unique, well-defined type, representable within the type system, without reference to how the expression is used or to what type it is assigned. This is the case even when type inference or type argument inference comes into play.

Neither this specification nor the internal implementation of the Ceylon compiler itself use any kind of "non-denotable" types. Every type mentioned here or inferred internally by the compiler has a representation within the language itself. Thus, the programmer is never exposed to confusing error messages referring to mysterious types that are not part of the syntax of the language.

The Ceylon compiler enforces identifier naming conventions. Types must be named with an initial uppercase letter. Methods, attributes, parameters, and locals must be named with an initial lowercase letter or underscore. The grammar for identifiers is defined by §2.3 Identifiers and keywords.

TypeName: UIdentifier

MemberName: LIdentifier

A package or module name is a sequence of identifiers, each with an initial lowercase letter or underscore.

PackageName: LIdentifier

Ceylon defines three identifier namespaces:

classes, interfaces, type aliases, and type parameters share a single namespace,

functions, values, and parameters share a single namespace, and

packages have their own dedicated namespace.

The Ceylon parser is able to unambiguously identify which namespace an identifier belongs to.

An identifier that begins with an initial lowercase letter may be
*forced* into the namespace of types by prefixing the
identifier `\I`. An identifier that begins with an initial
uppercase letter may be forced into the namespace of methods and attributes
by prefixing the identifier `\i`. A keyword may be used as
an identifier by prefixing the keyword with either `\i` or
`\I`. This allows interoperation with languages like Java
which do not enforce these naming conventions.

A *type* or *type schema* is a name
(an initial uppercase identifier) and an optional list of type parameters, with
a set of:

value schemas,

function schemas, and

class schemas.

The value, function, and class schemas are called the *members*
of the type.

Speaking formally:

A

*value schema*is a name (an initial lowercase identifier) with a type and mutability.A

*function schema*is a name (an initial lowercase identifier) and an optional list of type parameters, with a type (often called the*return type*) and a sequence of one or more parameter lists.A

*class schema*is a type schema with exactly one parameter list.A

*parameter list*is a list of names (initial lowercase identifiers) with types. The*signature*of a parameter list is formed by discarding the names, leaving the list of types.

Speaking slightly less formally, we usually refer to an *attribute*,
*method*, or *member class* of a type, meaning
a value schema, function schema, or class schema that is a member of the type.

A function or value schema may occur outside of a type schema. If it occurs
directly in a compilation unit, we often call it a *toplevel function*
or *toplevel value*.

A value schema, function schema, or parameter list with a missing type or types
may be defined. A value schema, function schema, or parameter list with a missing type
is called *partially typed*.

Two signatures are considered identical if they have exactly the same types, at exactly the same positions, and missing types at exactly the same positions.

Overloading is illegal in Ceylon. A type may not have:

two attributes with the same name,

a method and an attribute with the same name,

two methods with the same name, or

two member classes with the same name.

A type may be a *subtype* of another type. Subtyping obeys
the following rules:

Identity:

`X`is a subtype of`X`.Transitivity: if

`X`is a subtype of`Y`and`Y`is a subtype of`Z`then`X`is a subtype of`Z`.Noncircularity: if

`X`is a subtype of`Y`and`Y`is a subtype of`X`then`Y`and`X`are the same type.Single root: all types are subtypes of the class

`Anything`defined in the module`ceylon.language`.

Every interface type is a subtype of the class `Object`
defined in `ceylon.language`.

If `X` is a subtype of `Y`, then:

For each non-

`variable`attribute of`Y`,`X`has an attribute with the same name, whose type is assignable to the type of the attribute of`Y`.For each

`variable`attribute of`Y`,`X`has a`variable`attribute with the same name and the same type.For each method of

`Y`,`X`has a method with the same name, with the same number of parameter lists, with the same signatures, and whose return type is assignable to the return type of the method of`Y`.For each member class of

`Y`,`X`has a member class of the same name, with a parameter list with the same signature, that is a subtype of the member class of`Y`.

Furthermore, we say that `X` is *assignable*
to `Y`.

For any types `X` and `Y`, the
*union*, or *disjunction*, `X|Y`,
of the types may be formed. A union type is a supertype of both of the given types
`X` and `Y`, and an instance of either type is an
instance of the union type.

The union type constructor `|` is associative, so the union
of three types, `X`, `Y`, and `Z`,
may be written `X|Y|Z`.

UnionType: IntersectionType ("|" IntersectionType)*

If `X` and `Y` are both subtypes of a third type
`Z`, then `X|Y` inherits all members of `Z`.

void write(String|Integer|Float printable) { ... }

Union types satisfy the following rules, for any types `X`,
`Y`, and `Z`:

Commutativity:

`X|Y`is the same type as`Y|X`.Associativity:

`X|(Y|Z)`is the same type as`(X|Y)|Z`.Simplification: if

`X`is a subtype of`Y`, then`X|Y`is the same type as`Y`.Subtypes:

`X`is a subtype of`X|Y`.Supertypes: if both

`X`and`Y`are subtypes of`Z`, then`X|Y`is also a subtype of`Z`.

The following results follow from these rules:

`X|Nothing`is the same type as`X`for any type`X`, and`X|Anything`is the same type as`Anything`for any type`X`.

Finally:

If

`X<T>`is covariant in the type parameter`T`, then`X<U>|X<V>`is a subtype of`X<U|V>`for any types`U`and`V`that satisfy the type constraints on`T`.If

`X<T>`is contravariant in the type parameter`T`, then`X<U>|X<V>`is a subtype of`X<U&V>`for any types`U`and`V`that satisfy the type constraints on`T`.

For any types `X` and `Y`, the
*intersection*, or *conjunction*,
`X&Y`, of the types may be formed. An intersection type is a
subtype of both of the given types `X` and `Y`,
and any object which is an instance of both types is an instance of the intersection
type.

The intersection type constructor `&` is associative,
so the intersection of three types, `X`, `Y`,
and `Z`, may be written `X&Y&Z`.

IntersectionType: PrimaryType ("&" PrimaryType)*

The intersection `X&Y` inherits all members of both
`X` and `Y`.

void store(Persistent&Printable&Identifiable storable) { ... }

Intersection types satisfy the following rules, for any types `X`,
`Y`, and `Z`:

Commutativity:

`X&Y`is the same type as`Y&X`.Associativity:

`X&(Y&Z)`is the same type as`(X&Y)&Z`.Simplification: if

`X`is a subtype of`Y`, then`X&Y`is the same type as`X`.Supertypes:

`X`is a supertype of`X&Y`.Subtypes: if both

`X`and`Y`are supertypes of`Z`, then`X&Y`is also a supertype of`Z`.Distributivity over union:

`X&(Y|Z)`is the same type as`(X&Y)|(X&Z)`.

The following results follow from these rules:

`X&Nothing`is the same type as`Nothing`for any type`X`, and`X&Anything`is the same type as`X`for any type`X`.

Finally:

If

`X<T>`is covariant in the type parameter`T`, then`X<U>&X<V>`is a supertype of`X<U&V>`for any types`U`and`V`that satisfy the type constraints on`T`.If

`X<T>`is contravariant in the type parameter`T`, then`X<U>&X<V>`is a supertype of`X<U|V>`for any types`U`and`V`that satisfy the type constraints on`T`.

The special type `Nothing`, sometimes called the
*bottom type*, represents:

the intersection of all types, or, equivalently

the empty set.

`Nothing` is assignable to all other types, but has
no instances.

The type schema for `Nothing` is empty, that is, it
is considered to have no members.

`Nothing` is considered to belong to the module
`ceylon.language`. However, it cannot be defined within
the language.

Because of the restrictions imposed by Ceylon's mixin inheritance model:

If

`X`and`Y`are classes, and`X`is not a subclass of`Y`, and`Y`is not a subclass of`X`, then the intersection type`X&Y`is equivalent to`Nothing`.If

`X`is an interface, the intersection type`X&Null`is equivalent to`Nothing`.If

`X`is an interface, and`Y`is a`final`class, and`Y`is not a subtype of`X`, then the intersection type`X&Y`is equivalent to`Nothing`.If

`X<T>`is invariant in its type parameter`T`, and the distinct types`A`and`B`do not involve type parameters, then`X<A>&X<B>`is equivalent to`Nothing`.

Note: an expression of type `Nothing` results
in a compiler warning.

An expression, as defined in Chapter 6, *Expressions*, occurring at a
certain location, may be *assignable* to a type. In this case,
every evaluation of the expression at runtime produces an instance of a class that
is a subtype of the type, or results in a thrown exception, as defined in
Chapter 8, *Execution*.

Given an expression occurring at a certain location, a type `T`
is the *principal type* of the expression if, given any type
`U` to which the expression is assignable, `T`
is a subtype of `U`. Thus, the principal type is the "most precise"
type for the expression. The type system guarantees that every expression has a
principal type. Thus, we refer uniquely to *the type of an expression*,
meaning its principal type at the location at which it occurs.

Function and value declarations usually declare a type, by specifying
a *type expression*.

Type: UnionType | EntryType

Type expressions are formed by combining types using union, intersection, and type abbreviations.

Type expressions support grouping using angle brackets:

GroupedType: "<" Type ">"

Applied types are identified by the name of the type (a class, interface, type alias, or type parameter), together with a list of type arguments if the type declaration is generic.

TypeNameWithArguments: TypeName TypeArguments?

Type names are resolved to type declarations according to §5.1.7 Unqualified reference resolution and §5.1.8 Qualified reference resolution.

The type argument list, if any, must conform, as defined by §3.6.1 Type arguments and type constraints, to the type parameter list of the realization of the type declaration, as defined by §3.7.6 Realizations.

Note: this is too heavy-handed. There is no reason to enforce
types constraint in any place other than generic class instantiations, generic
function invocations, `extends`, and `satisfies`.
However, this restriction makes interoperation with Java generics more
straightforward.

If the type is a class, interface, or type alias nested inside a containing class or interface, the type must be fully qualified by its containing types, except when used inside the body of a containing type.

BaseType: TypeNameWithArguments | GroupedType

QualifiedType: BaseType ("." TypeNameWithArguments)*

If a type declaration is generic, a type argument list must be specified. If a type declaration is not generic, no type argument list may be specified.

BufferedReader.Buffer

Entry<Integer,Element>

Note: the name of a type may not be qualified by its package name. Alias imports, as defined in §4.2.3 Alias imports may be used to disambiguate type names.

Certain important types may be written using an abbreviated syntax.

PrimaryType: AtomicType | OptionalType | SequenceType | CallableType

AtomicType: QualifiedType | EmptyType | TupleType | IterableType

First, there are postfix-style abbreviations for *optional types*,
*sequence types*, and *callable types*.

OptionalType: PrimaryType "?"

SequenceType: PrimaryType "[" "]"

CallableType: PrimaryType "(" TypeList? ")"

`X?`means`Null|X`for any type`X`,`X[]`means`Sequential<X>`for any type`X`, and`X(Y,Z)`means`Callable<X,[Y,Z]>`where`Y,Z`is a list of types of any length.

More precisely, the type meant by a callable type abbreviation is
`Callable<X,T>` where `X` is the type
outside the parentheses in the the callable type abbreviation, and
`T` is the tuple type formed by the types listed inside the
parentheses.

Next, abbreviations for *iterable types* are written
using braces.

IterableType: "{" UnionType ("*"|"+") "}"

`{X*}`means`Iterable<X,Null>`for any type`X`, and`{X+}`means`Iterable<X,Nothing>`for any type`X`.

Next, abbreviations for *sequence types* and
*tuple types* may be written using brackets.

EmptyType: "[" "]"

TupleType: "[" TypeList "]"

TypeList: (DefaultedType ",")* (DefaultedType | VariadicType)

DefaultedType: Type "="?

VariadicType: UnionType ("*" | "+")

`[]`means`Empty`,`[X*]`means`Sequential<X>`for any type`X`,`[X+]`means`Sequence<X>`for any type`X`,`[X,Y]`means`Tuple<X|Y,X,Tuple<Y,Y,[]>>`for any types`X,Y`,`[X,Y*]`means`Tuple<X|Y,X,Sequential<Y>>`for any types`X,Y`,`[X,Y+]`means`Tuple<X|Y,X,Sequence<Y>>`for any types`X,Y`, and`[X,Y=]`means`Tuple<X|Y,X,Tuple<Y,Y,[]>>|Tuple<X,X,[]>`for any types`X,Y`.

More precisely:

A tuple type abbreviation of form

`[X, ... ]`means the type`Tuple<X|Y,X,T>`where`T`is the type meant by the type abbreviation formed by removing the first type`X`from the list of types in the original tuple type abbreviation, and`T`has the principal instantiation`Y[]`, as defined in §3.7 Principal instantiations and polymorphism.A tuple type abbreviation of form

`[ ..., Y= ]`means the type`U|V`where`U`is the type meant by the whole tuple type abbreviation, and`V`is the type meant by the type abbreviation formed by removing the last type`Y`from the list of types in the whole tuple type abbreviation.

In a tuple type or callable type expression:

an

*defaulted element*is indicated with a postfix`=`or`*`, anda

*required element*is indicated with a postfix`+`or no special marker.

In a tuple type or callable type expression, every defaulted element must occur after every required element.

Finally, an *entry type* may be abbreviated using an
arrow.

EntryType: UnionType "->" UnionType

`X->Y`means`Entry<X,Y>`, for any types`X`,`Y`.

Note: the abbreviations `T[]` and
`[T*]` are synonyms. The syntax `T[]` is
supported for reasons of nostalgia.

Abbreviations may be combined:

String?[] words = { "hello", "world", null }; String? firstWord = words[0]; String->[Integer,Integer] onetwo = "onetwo"->[1, 2]; [Float+](Float x, Float[] xs) add = (Float x, Float[] xs) => [x, *xs];

When a type appears in a value expression, these abbreviations cannot be used (they cannot be disambiguated from operator expressions).

Certain declarations which usually require an explicit type may omit the type,
forcing the compiler to infer it, by specifying the keyword `value`,
as defined in §4.8.4 Value type inference, or `function`,
as defined in §4.7.4 Function return type inference, where the type usually appears.

value names = people*.name;

function parse(String text) => text.split(" .!?,:;()\n\f\r\t".contains);

Type inference is only allowed for declarations which are referred to only by
statements and declarations that occur within the lexical scope of the declaration,
as specified by §5.1.6 Type inference and block structure. A
`value` or `function` declaration may not:

be annotated

`shared`, as defined in §5.1.3 Visibility,occur as a toplevel declaration in a compilation unit, as defined in §4.1.1 Toplevel and nested declarations, or

be referred to by statements or declarations that occur earlier in the body containing of the declaration, as defined in §5.1 Block structure and references.

Nor may a parameter or forward-declared value, as defined in §4.8.5 Forward declaration of values, or of a forward-declared function, as defined in §4.7.5 Forward declaration of functions, have an inferred type.

These restrictions allow the compiler to infer undeclared types in a single pass of the code.

Note: in future releases of the language, the inferred type will be context-dependent, that is, in program elements immediately following an assignment or specification, the inferred type will be the type just assigned. When conditional execution results in definite assignment, the inferred type will be the union of the conditionally assigned types. This will allow us to to relax the restriction that forward-declared functions and values can't have their type inferred. For example:

value one; if (float) { one = 1.0; Float float = one; } else { one = 1; Integer int = one; } Float|Integer num = one;

An inferred type never involves an anonymous class, as defined in §4.5.7 Anonymous classes. When an inferred type would involve an anonymous class type, the anonymous class is replaced by the intersection of the class type it extends with all interface types it satisfies.

TODO: properly define how expressions with no type occurring
in a `dynamic` block affect type inference.

A *type alias* is a synonym for another type. A
generic type alias is a type constructor that produces a type alias, given
a list of type arguments.

Every type alias must be reducible to an equivalent type that does not involve any type aliases by recursive replacement of type aliases with the types they alias. Thus, circular type alias definitions, as in the following example, are illegal:

alias X => List<Y>; alias Y => List<X>;

Replacement of type aliases with the types they alias occurs at compile time, so type aliases are not reified types, as specified in §8.1.2 Type argument reification.

Inheritance is a static relationship between classes, interfaces, and type parameters:

a class may

*extend*another class, as defined by §4.5.4 Class inheritance,a class may

*satisfy*one or more interfaces, as defined by §4.5.4 Class inheritance,an interface may

*satisfy*one or more other interfaces, as defined by §4.4.2 Interface inheritance, ora type parameter may

*satisfy*a class and/or one or more interfaces or type parameters, as defined by §3.5.3 Generic type constraints.

If a type declaration extends or satisfies a type, we say it
*inherits* the type.

Inheritance relationships may not produce cycles, since that would violate the noncircularity rule for subtyping. Thus, a class, interface, or type parameter may not, directly or indirectly, inherit itself.

Note: when a type declaration specifies a relationship to other types,
Ceylon visually distinguishes between a list of types which conceptually
represents a combination of (intersection of) the types, and a list of types
which represents a choice between (union of) the types. For example, when a
class `C` satisfies multiple interfaces, they are written as
`X&Y&Z`. On the other hand, the cases of an
enumerated class `E` are written as `X|Y|Z`.
This syntax emphasizes that `C` is also a subtype of the
intersection type `X&Y&Z`, and that `E`
may be narrowed to the union type `X|Y|Z` using a
`switch` statement or the `of` operator.

Inheritance relationships between classes, interfaces, and type parameters result in subtyping relationships between types.

If a type

`X`inherits a type`Y`, then`X`is a subtype of`Y`.If a generic type

`X`inherits a type`Y`that might involve the type parameters of`X`, then for any instantiation`U`of`X`we can construct a type`V`by, for every type parameter`T`of`X`, substituting the corresponding type argument of`T`given in`U`everywhere`T`occurs in`Y`, and then`U`is a subtype of`V`.

A class may extend another class, in which case the first class is a subtype of the second class and inherits its members.

ExtendedType: "extends" ("super" ".")? TypeNameWithArguments PositionalArguments

The `extends` clause must specify exactly one superclass.

If the superclass is a parameterized type, the

`extends`clause must also explicitly specify type arguments.The

`extends`clause must specify arguments for the initializer parameters of the superclass.

The type arguments may *not* be inferred from the
initializer arguments.

extends Person(name, org)

A member class annotated `actual` may use the qualifier
`super` in the `extends` clause to refer to the
member class it refines. When the qualifier `super` appears, the
following class name refers to a member class of the superclass of the class that
contains the member class annotated `actual`.

extends super.Buffer()

The root class `Anything` defined in
`ceylon.language` does not have a superclass.

The `satisfies` clause does double duty. It's used to
specify that a class or interface is a direct subtype of one or more interfaces,
and to specify upper bound type constraints applying to a type parameter.

Note: for this reason the keyword is not named
"`implements`". It can't reasonably be said that a type
parameter "implements" its upper bounds. Nor can it be reasonably said that
an interface "implements" its super-interfaces.

A class or interface may satisfy one or more interfaces, in which case the class or interface is a subtype of the satisfied interfaces, and inherits their members.

A type parameter may satisfy one or more interfaces, optionally, a class, and optionally, another type parameter. In this case, the satisfied types are interpreted as upper bound type constraints on arguments to the type parameter.

Note: currently, a type parameter upper bound may not be specified in combination with other upper bounds. This restriction will likely be removed in future.

SatisfiedTypes: "satisfies" PrimaryType ("&" PrimaryType)*

The `satisfies` clause may specify multiple types. If a
satisfied type is a parameterized type, the `satisfies` clause
must specify type arguments.

satisfies Sequence<Element> & Collection<Element>

A `satisfies` clause may not contain two types produced from
the same type declaration.

*Coverage* is a static relationship between classes,
interfaces, and type parameters, produced through the use of *case
enumeration*:

An

`abstract`class or interface may be an*enumerated type*, with an enumerated list of disjoint subtypes called*cases*, as defined by §4.5.8 Classes with enumerated cases and §4.4.4 Interfaces with enumerated cases.A type parameter may have an

*enumerated bound*, with an enumerated list possible type arguments, as defined by §3.5.3 Generic type constraints.An

`abstract`class or interface may have a*self type*, a type parameter representing the concrete type of an instance.

Coverage is a strictly weaker relationship than assignability:

If a type is a subtype of a second type, then the second type covers the first type.

If a type has a self type, then its self type covers the type.

If a type

`X`enumerates its cases`X1`,`X2`, etc, then the union`X1|X2|...`of its cases covers the type.If a generic type

`X`enumerates its cases,`X1`,`X2`, etc, which might involve the type parameters of`X`, then for any instantiation`U`of`X`, and for each case`Xi`, we can construct a type`Ui`by, for every type parameter`T`of`X`, substituting the corresponding type argument of`T`given in`U`everywhere`T`occurs in`Xi`, and then the union type`U1|U2|...`of all the resulting types`Ui`covers`Y`.If a type

`X`covers two types`A`and`B`, then`X`also covers their union`A|B`.Coverage is transitive. If

`X`covers`Y`and`Y`covers`Z`, then`X`covers`Z`.

It follows that coverage obeys the identity property of assignability:
a type covers itself. However, coverage does not obey the noncircularity property
of assignability. It is possible to have distinct types `A` and
`B` where `A` covers `B` and
`B` covers `A`.

Case enumeration allows safe use of a type in a `switch`
statement, or as the subject of the `of` operator. The
compiler is able to statically validate that the `switch`
contains an exhaustive list of all cases of the type, by checking that the
union of cases enumerated in the `switch` covers the type,
or that the second operand of `of` covers the type.

Note: however, a type is *not* considered automatically
assignable to the union of its cases, or to its self type. Instead, the type
must be *explicitly* narrowed to the union of its cases,
or to its self type, using either the `of` operator or the
`switch` construct. This narrowing type conversion can be
statically checked—if `X` covers `Y`
then `Y of X` is guaranteed to succeed at runtime.
Unfortunately, and quite unintuitively, the compiler is not able to analyse
coverage implicitly at the same time as assignability, because that results in
undecidability!

The `of` clause does triple duty. It's used to define
self types and type families, enumerated types, and enumerated type
constraints. The `of` clause may specify multiple types,
called *cases*.

CaseTypes: "of" CaseType ("|" CaseType)*

CaseType: MemberName | PrimaryType

If an interface or `abstract` class with an
`of` clause has exactly one case, and it is a type parameter
of the interface or `abstract` class, or of the immediately
containing type, if any, then that type parameter is a
*self type* of the interface or `abstract`
class, and:

the self type parameter covers the declared type within the body of the declaration,

the type argument to the self type parameter in an instantiation of the declared type covers the instantiation, and

every type which extends or satisfies an instantiation of the declared type must also be covered by the type argument to the self type parameter in the instantiation.

shared abstract class Comparable<Other>() of Other given Other satisfies Comparable<Other> { shared formal Integer compare(Other that); shared Integer reverseCompare(Other that) => that.compare(this) of Other; }

Comparable<Item> comp = ... ; Item item = comp of Item;

Otherwise, an interface or `abstract` class with an
`of` clause may have multiple cases, but each case must be
either:

a subtype of the interface or

`abstract`class, ora value reference to a toplevel anonymous class that is a subtype of the interface or

`abstract`class.

Then the interface or `abstract` class is an
*enumerated type*, and every subtype of the interface
or `abstract` class must be a subtype of exactly one of
the enumerated subtypes. A class or interface may not be a subtype of more
than one case of an enumerated type.

of larger | smaller | equal

of Root<Element> | Leaf<Element> | Branch<Element>

A type parameter with an `of` clause may specify
multiple cases, as defined in §3.5.3 Generic type constraints.

An `of` clause may not contain:

two types produced from the same type declaration, or

two value references to a single toplevel anonymous class.

If a generic enumerated type `X` has a case type
`C`, then `C` must directly extend or
satisfy an instantiation `Y` of `X`, and
for each type parameter `T` of `X` and
corresponding argument `A` of `T` given
in `Y`, either:

`X`is covariant in`T`and`A`is exactly`Nothing`,`X`is contravariant in`T`and`A`is exactly the intersection of all upper bounds on`T`, or`Anything`if`T`has no upper bounds, or`C`is an instantiation of a generic type`G`and`A`is exactly`S`for some type parameter`S`of`G`, and`S`must have the same variance as`T`.

For example, the following covariant enumerated type is legal:

interface List<out Element> of Cons<Element> | nil { ... } class Cons<out Element>(Element element) satisfies List<Element> { ... } object nil satisfies List<Nothing> { ... }

As is the following contravariant enumerated type:

interface Consumer<in Event> of Logger | Handler<Event> given Event satisfies AbstractEvent { ... } interface Logger satisfies Consumer<AbstractEvent> { ... } interface Handler<in Event> satisfies Consumer<AbstractEvent> given Event satisfies AbstractEvent { ... }

But the following enumerated type is not legal, since it is possible
to choose a legal argument `T` of the type parameter
`Type` of `Expression`, such that the case
types `StringLiteral` and `NumberLiteral`
aren't subtypes of the instantiation `Expression<T>`:

interface Expression<out Type> of Function<Type> | StringLiteral | NumberLiteral { ... } interface Function<out Type> satisfies Expression<Type> { ... } interface StringLiteral satisfies Expression<String> { ... } interface NumberLiteral satisfies Expression<Integer|Float> { ... }

Note: these rules could be relaxed to allow the definition of generic enumerated types where the list of cases of an instantiation of a generic type depends upon the given type arguments (a "generalized" algebraic type).

Two types are said to be *disjoint* if it is impossible
to have a value that is an instance of both types. If `X` and
`Y` are disjoint, then their intersection `X&Y`
is the bottom type `Nothing`.

Two types `X` and `Y` are disjoint if
either:

`X`and`Y`are both classes and`X`is not a subclass of`Y`and`Y`is not a subclass of`X`,`X`is the class`Null`and`Y`is an interface,`X`is an anonymous class or an instantiation of a`final`class and`Y`is an instantiation of a class of interface, and`X`does not inherit`Y`,`X`is an anonymous class or a`final`class with no type parameters and`Y`is a type in which no type parameter reference occurs, and`X`is not a suptype of`Y`,`X`is a type parameter and`Y`and the intersection of the upper bounds of`X`are disjoint,`X`is an union type`A|B`and both`Y`and`A`are disjoint and`Y`and`B`are disjoint,`X`is an intersection type`A&B`and either`Y`and`A`are disjoint or`Y`and`B`are disjoint, or`X`and`Y`inherit disjoint instantiations of a generic type`Z`, that is, two instantiations of`Z`that have the intersection`Nothing`, as defined below, in §3.7.2 Principal instantiation inheritance.

Furthermore, as a special case, the types `X` and
`Y` are disjoint if:

`X`is an invariant subtype of`Sequence<A>`,`Y`is an invariant subtype of`Sequence<B>`, and`A`and`B`are disjoint,`X`is an invariant subtype of`Sequential<A>`,`Y`is an invariant subtype of`Tuple<J,B,V>`, and`A`and`B`are disjoint or`X`and`V`are disjoint, or`X`is an invariant subtype of`Tuple<I,A,U>`,`Y`is an invariant subtype of`Tuple<J,B,V>`, and`A`and`B`are disjoint or`U`and`C`are disjoint.

Note: the soundness of these rules is guaranteed by the implementations of the
`sealed` types `Sequence`, `Sequential`, and
`Tuple` in the module `ceylon.language`.

Function, class, and interface schemas may be parameterized by one or more generic type parameters. A parameterized type schema defines a type constructor, a function that produces a type given a tuple of compatible type arguments. A parameterized class or function schema defines a function that produces the signature of an invokable operation given a tuple of compatible type arguments.

TypeParameters: "<" (TypeParameter ",")* TypeParameter ">"

A declaration with type parameters is called *generic* or
*parameterized*.

A type schema with no type parameters defines exactly one type. A parameterized type schema defines a template for producing types: one type for each possible combination of type arguments that satisfy the type constraints specified by the type. The types of members of the this type are determined by replacing every appearance of each type parameter in the schema of the parameterized type definition with its type argument.

A function schema with no type parameters defines exactly one operation per type. A parameterized function declaration defines a template for producing overloaded operations: one operation for each possible combination of type arguments that satisfy the type constraints specified by the method declaration.

A class schema with no type parameters defines exactly one instantiation operation. A parameterized class schema defines a template for producing overloaded instantiation operations: one instantiation operation for each possible combination of type arguments that satisfy the type constraints specified by the class declaration. The type of the object produced by an instantiation operation is determined by substituting the same combination of type arguments for the type parameters of the parameterized class schema.

Note: by convention, type parameter names should be constructed from
meaningful words. The use of single-letter type parameter names is discouraged. The
name of a type parameter should be chosen so that declarations within the body of
the parameterized declaration read naturally. For example,
`class Entry<Key,Item>` is reasonable, since
`Key key` and `Item item` read naturally within
the body of the `Entry` class. The following identifier names
usually refer to a type parameter: `Element`, `Other`,
`This`, `Value`, `Key`,
`Item`, `Argument`, `Args` and
`Result`. Avoid, where reasonable, using these names for interfaces
and classes.

A *type parameter* allows a declaration to be abstracted
over a constrained set of types.

TypeParameter: Variance? TypeName ("=" Type)

Every type parameter has a name and a *variance*.

Variance: "out" | "in"

A

*covariant*type parameter is indicated using the keyword`out`.A

*contravariant*type parameter is indicated using the keyword`in`.By default, a type parameter is

*invariant*.

A type parameter may, optionally, have a *default type argument*.
A type parameter with a default type argument must occur after every type parameter
with no default type argument in the type parameter list.

The default type argument for a type parameter must satisfy the constraints on the type parameter.

TODO: this restriction could be relaxed, and the assignability of the default type argument to the type constraints checked at use-sites where the default type argument is used in type expressions.

A default type argument expression for a type parameter of a generic declaration may not involve:

the type parameter itself,

any type parameter of the declaration that occurs later in the list of type parameters, nor

the generic declaration.

Within the body of the schema it parameterizes, a type parameter is itself a type. The type parameter is a subtype of every upper bound of the type parameter. However, a class or interface may not extend or satisfy a type parameter.

<Key, out Item>

<in Message>

<out Element=Object>

<in Left, in Right, out Result>

A covariant type parameter may only appear in *covariant positions*
of the parameterized schema. A contravariant type parameter may only appear in
*contravariant positions* of the parameterized schema. An
invariant type parameter may appear in any position.

Furthermore, a type with a contravariant type parameter may only appear in a covariant position in an extended type, satisfied type, case type, or upper bound type constraint.

Note: this restriction exists to eliminate certain undecidable cases described in the paper Taming Wildcards in Java's Type System, by Tate et al.

To determine if a type expression occurs in a covariant or contravariant position, we first consider how the type occurs syntactically.

For a generic function we examine the return type of the function, which is a covariant position.

For a generic type schema we examine each `shared`
member, along with extended/satisfied types and case types.

Note: since the visibility rules are purely lexical in nature, it is
legal for a member expression occurring in the body of a class or interface to have
a receiver expression other that is not a self-reference, as defined in
§6.3 Self references and the current package reference, and refer to an un-`shared` member
of the class or interface. In this special case, the member is treated as if it were
`shared` for the purposes of the following variance validation
rules.

An extended type, satisfied type, or case type of the type schema itself is a covariant position.

In a `shared` method declaration of the parameterized
type schema:

The return type of the method is a covariant position.

Any parameter type of the method is a contravariant position.

Any upper bound of a type parameter of the method is a contravariant position.

In a `shared` attribute declaration that is not
variable:

The type of the attribute is a covariant position.

In a `shared` reference declaration that is
variable:

The type of the attribute is an invariant position.

In a `shared` nested class declaration of the
parameterized type schema:

Any initializer parameter type of the class is a contravariant position.

Any upper bound of a type parameter of the class is a contravariant position.

An extended type, satisfied type, or case type of the nested class is a covariant position.

Every covariant position of the nested class schema is a covariant position of the containing type schema. Every contravariant position of the nested class schema is a contravariant position of the containing type schema.

In a `shared` nested interface declaration of the
parameterized type schema:

An extended type, satisfied type, or case type of the nested interface is a covariant position.

Every covariant position of the nested interface schema is a covariant position of the containing type schema. Every contravariant position of the nested interface schema is a contravariant position of the containing type schema.

For parameters of callable parameters, we first determine if the callable parameter itself is covariant or contravariant:

A callable parameter of a method or nested class is contravariant.

A callable parameter of a covariant parameter is contravariant.

A callable parameter of a contravariant parameter is covariant.

Then:

The return type of a covariant callable parameter is a covariant position.

The return type of a contravariant callable parameter is a contravariant position.

The type of a parameter of a covariant callable parameter is a contravariant position.

The type of a parameter of a contravariant callable parameter is a covariant position.

Finally, to determine if a type parameter that occurs as a type argument occurs in a covariant or contravariant position, we must consider the declared variance of the corresponding type parameter:

A type argument of a covariant type parameter of a type in a covariant position is a covariant position.

A type argument of a contravariant type parameter of a type in a covariant position is a contravariant position.

A type argument of a covariant type parameter of a type in a contravariant position is a contravariant position.

A type argument of a contravariant type parameter of a type in a contravariant position is a covariant position.

A type argument of an invariant type parameter of a type in any position is an invariant position.

A type argument of any type parameter of a type in an invariant position is an invariant position.

A parameterized method, class, or interface declaration may declare constraints
upon ordinary type parameters using the `given` clause.

TypeConstraints: TypeConstraint+

There may be at most one `given` clause per type parameter.

TypeConstraint: "given" TypeName TypeConstraintInheritance

TypeConstraintInheritance: CaseTypes? SatisfiedTypes?

Note that the syntax for a type constraint is essentially the same syntax used for other type declarations such as class and interface declarations.

There are two different kinds of type constraint:

An

*upper bound*,`given X satisfies T`, specifies that the type parameter`X`is a subtype of a given type`T`.An

*enumerated bound*,`given X of T|U|V`specifies that the type parameter`X`represents one of the enumerated types.

The types listed in an enumerated bound must be mutually disjoint, and each type must be a class or interface type.

TODO: Should we allow unions in upper bounds? Should we allow intersections in enumerated bounds?

A single `given` clause may specify multiple constraints on
a certain type parameter. In particular, it may specify multiple upper bounds
together with an enumerated bound. If multiple upper bounds are specified, at most
one upper bound may be a class, and at most one upper bound may be a type parameter.

Note: in Ceylon 1.0, a type parameter with multiple upper bounds may not have an upper bound which is another type parameter.

given Value satisfies Ordinal & Comparable<Value>

given Quantities satisfies Correspondence<Key,Decimal>

given Argument of String | Integer | Float

A type parameter is a subtype of its upper bounds.

class Holder<Value>(shared Value value) extends Object given Value satisfies Object { shared actual Boolean equals(Object that) { if (is Holder<Value> that) { return value==that.value; } else { return false; } } shared actual Integer hash => value.hash; }

Every type parameter has an implicit upper bound of type
`Anything`.

An enumerated bound allows the use of an exhaustive `switch`
with expressions of the parameter type.

Characters uppercase<Characters>(Characters chars) given Characters of String | Range<Character> { switch (Characters) case (satisfies String) { return chars.uppercased; } case (satisfies Range<Character>) { return chars.first.uppercased..chars.last.uppercased; } }

TODO: Do we need lower bound type constraints? The syntax would be:

given T abstracts One|Two

With union types they don't appear to be anywhere near as useful. However, perhaps they are useful when combined with contravariant types. (A lower bound on a parameter which occurs as the argument of a contravariant type is more like an upper bound).

Note: since we have reified types, it would be possible to support a type constraint that allows instantiation of the type parameter.

given T(Object arg)

The problem with this is that then inferring `T` is fragile.
And if we don't let it be inferred, we may as well pass `T` as an
ordinary parameter. So Ceylon, unlike C#, doesn't support this.

A list of *type arguments* produces a new type schema
from a parameterized type schema, or a new function schema from a from a
parameterized function schema. In the case of a type schema, this new schema is
the schema of an applied type.

A type argument list is a list of types.

TypeArguments: "<" (Type ",")* Type ">"

A type argument may itself be an applied type, or type parameter, or may involve unions and intersections.

<Key, List<Item>>

<String, Person?>

<String[], [{Object*}]>

Type arguments are assigned to type parameters according to the positions they occur in the list.

Given the schema of a generic declaration, we form the new schema by
*type argument substitution*. Each type argument is substituted
for every appearance of the corresponding type parameter in the schema of the
generic declaration, including:

attribute types,

method return types,

method parameter types,

initializer parameter types, and

type arguments of extended classes and satisfied interfaces.

A generic type constraint affects the type arguments that can be assigned to a type parameter:

A type argument to a type parameter

`T`with an upper bound must be a type which is a subtype of all upper bounds of`T`.A type argument to a type parameter

`T`with an enumerated type bound must be a subtype of one of the enumerated types of`T`, or it must be a type parameter`A`with an enumerated type bound where every enumerated type of`A`is also an enumerated type of`T`.

A type argument list *conforms* to a type parameter list
if, for every type parameter in the list, either:

there is a type argument that satisfies the constraints of the type parameter, or

there is no explicit type argument but the type parameter has a default type argument, in which case the type argument is defaulted by substituting the arguments of all type parameters that occur earlier in the list of type parameters of the declaration into this default type argument.

There must be at least as many type parameters as type arguments. There must be at least as many type arguments as type parameters without default values.

If a type argument list conforms to a type parameter list, the combination
of the parameterized type together with the type argument list is itself a type,
called an *applied type*. We also call the applied type an
*instantiation* of the generic type.

For a generic type `X`, the instantiations `Y`
and `Z` of `X` represent the same type if and
only if for every `A` in the list of type arguments specified
in `Y` and corresponding `B` in the list of type
arguments specified in `Z`, `A` is exactly the
same type as `B`.

For a generic type `X`, and instantiations
`Y` and `Z` of `X`,
`Y` is a subtype of `Z` if and only if, for
every type parameter `T` of `X`, and
corresponding arguments `A` specified in `Y`
and `B` specified in `Z`:

`T`is a covariant type parameter, and`A`is a subtype of`B`, or`T`is a contravariant type parameter, and`B`is a subtype of`A`, or`T`is an invariant type parameter (neither covariant nor contravariant), and`A`and`B`are exactly the same type.

Note that if `T` is an invariant type parameter
of `X<T>`, then a type `Z` is a subtype
of `X<A>` if and only if `Z` has the
principal instantiation `X<A>`.

When a direct invocation expression, as defined by
§6.6 Invocation expressions, for a generic function or a direct
instantiation expression for a generic class does not explicitly specify type
arguments, the type arguments are inferred from the argument expression types.
The types of the argument expressions and the declared types of the corresponding
parameters determine an *inferred lower bound* or
*inferred upper bound* for each type parameter.

If a list of argument expressions has types `A1,A2,...`
and the corresponding list of parameters has declared types `P1,P2,...`,
the inferred lower bound for a type parameter `T` of the generic
declaration is the conjunction of:

all inferred lower bounds

`Ai`on`Pi`for`T`.

The inferred upper bound for a type parameter `T` of the generic
declaration is the conjunction of:

all upper bounds

`Xi`explicitly declared by a type constraint on`T`of form`given T satisfies Xi`, if any, withall inferred upper bounds

`Ai`on`Pi`for`T`.

TODO: What should we do about upper bound constraints that involve other type parameters? Currently the typechecker simply ignores any upper bound that involves any type parameter.

Given types `A` and `P`, we determine
the *inferred lower bound* `A` on
`P` for `T` according to the nature of
`A` and `P`:

If

`P`is exactly`T`, and the location at which`P`occurs in the parameter list is not a contravariant location, the inferred lower bound`A`on`P`for`T`is`T abstracts A`.If

`P`is a union type`Q|R`, the lower bound`A`on`P`for`T`is the disjunction of the lower bound`A`on`Q`for`T`with the lower bound`A`on`R`for`T`.*Note: this case is special.*If

`P`is an intersection type`Q&R`, the lower bound`A`on`P`for`T`is the conjunction of the lower bound`A`on`Q`for`T`with the lower bound`A`on`R`for`T`.If

`A`is a union type`B|C`, the lower bound`A`on`P`for`T`is the conjunction of the lower bound`B`on`P`for`T`with the lower bound`C`on`P`for`T`.If

`A`is an intersection type`B&C`, the lower bound`A`on`P`for`T`is the disjunction of the lower bound`B`on`P`for`T`with the lower bound`C`on`P`for`T`.If

`P`is an applied type`Q<P1,P2,...>`of a parameterized type`Q`, and`A`is a subtype of an applied type`Q<A1,A2,..>`, the lower bound`A`on`P`for`T`is the conjunction of all lower bounds`Ai`on`Pi`for`T`.Otherwise, if

`A`is not a union or intersection, and if`P`is neither an applied type, a union, or an intersection, nor exactly`T`, the lower bound`A`on`P`for`T`is*null*.

Where:

the conjunction of a lower bound

`T abstracts A`with a lower bound`T abstracts B`is the lower bound`T abstracts A|B`,the disjunction of a lower bound

`T abstracts A`with a lower bound`T abstracts B`is the lower bound`T abstracts A&B`,the conjunction or disjunction of a lower bound

`T abstracts A`with a null lower bound is`T abstracts A`, andthe conjunction or disjunction of two null lower bounds is null.

Given types `A` and `P`, we determine
the *inferred upper bound* `A` on
`P` for `T` according to the nature of
`A` and `P`:

If

`P`is exactly`T`, and the location at which`P`occurs in the parameter list is not a covariant location, the inferred upper bound`A`on`P`for`T`is`T satisfies A`.If

`P`is a union type`Q|R`, the upper bound`A`on`P`for`T`is the disjunction of the upper bound`A`on`Q`for`T`with the upper bound`A`on`R`for`T`.*Note: this case is special.*If

`P`is an intersection type`Q&R`, the upper bound`A`on`P`for`T`is the conjunction of the upper bound`A`on`Q`for`T`with the upper bound`A`on`R`for`T`.If

`A`is a union type`B|C`, the upper bound`A`on`P`for`T`is the disjunction of the upper bound`B`on`P`for`T`with the upper bound`C`on`P`for`T`.If

`A`is an intersection type`B&C`, the upper bound`A`on`P`for`T`is the conjunction of the upper bound`B`on`P`for`T`with the upper bound`C`on`P`for`T`.If

`P`is an applied type`Q<P1,P2,...>`of a parameterized type`Q`, and`A`is a subtype of an applied type`Q<A1,A2,..>`, the upper bound`A`on`P`for`T`is the conjunction of all upper bounds`Ai`on`Pi`for`T`.Otherwise, if

`A`is not a union or intersection, and if`P`is neither an applied type, a union, or an intersection, nor exactly`T`, the upper bound`A`on`P`for`T`is*null*.

Where:

the conjunction of an upper bound

`T satisfies A`with an upper bound`T satisfies B`is the upper bound`T satisfies A&B`,the disjunction of an upper bound

`T satisfies A`with an upper bound`T satisfies B`is the upper bound`T satisfies A|B`,the conjunction or disjunction of an upper bound

`T satisfies A`with a null upper bound is`T satisfies A`, andthe conjunction or disjunction of two null upper bounds is null.

The inferred type argument to a covariant or invariant type parameter
`T` of the generic declaration is:

`Nothing`, if the inferred lower bound for`T`is null, or, otherwise,the type

`A`, where the inferred lower bound for`T`is`T abstracts A`.

The inferred type argument to a contravariant type parameter
`T` of the generic declaration is:

`Anything`, if the inferred upper bound for`T`is null, or, otherwise,the type

`A`, where the inferred upper bound for`T`is`T satisfies A`.

An argument expression with no type occurring in a `dynamic`
block, as defined in §5.3.12 Dynamic blocks, may cause type argument inference
to fail. When combining bounds using union, any constituent bound with no type results
in a bound with no type. When combining bounds using intersection, any constituent
bound with no type is eliminated. If the resulting inferred upper or lower bound has no
type, type argument inference is impossible for the type argument, and type arguments
must be specified explicitly.

If the inferred type argument does not satisfy the generic type
constraints on `T`, a compilation error results.

Consider the following invocation:

[Element+] prepend<Element>(Element head, Element[] sequence) { ... } value result = prepend(null, {"hello", "world"});

The inferred type of `Element` is the union type
`String?`.

Now consider:

class Bag<out Element>(Element* elements) { shared Bag<ExtraElement> with<ExtraElement>(ExtraElement* elements) given ExtraElement abstracts Element { ... } } Bag<String> bag = Bag("hello", "world"); value biggerBag = bag.with(1, 2, 5.0);

The inferred type of `ExtraElement` is the union
type `Integer|Float|String`.

Finally consider:

interface Delegate<in Value> { ... } class Consumer<in Value>(Delegate<Value>* delegates) { ... } Delegate<String> delegate1 = ... ; Delegate<Object> delegate2 = ... ; value consumer = Consumer(delegate1, delegate2);

The inferred type of `Value` is
`Consumer<String>`.

TODO: What about upper bounds in which the type parameter
itself appears (the infamous self-type problem with
`Comparable` and `Numeric`) or in which
another type parameter appears?

Inheritance interacts with type parameterization to produce subtyping
relationships between instantiations of generic types. The notion of an
*inherited instantiation* and the notion of a
*principal instantation* help us reason about these
relationships.

Warning: this section is not for the faint of heart. Feel
free to skip to Chapter 4, *Declarations*, unless you're really, really
interested in precisely how the compiler reasons about inheritance of generic
types.

For a generic type `Y`, inheritance produces subtypes
with *inherited instantiations* of the generic type.

If a type

`X`directly extends or satisfies an instantiation`V`of`Y`, then`X`has the inherited instantiation`V`of`Y`.If a generic type

`X`extends or satisfies an instantiation`V`of`Y`, that may involve the type parameters of`X`, then for any instantiation`U`of`X`, we can construct an instantiation`W`of`Y`by, for every type parameter`T`of`X`, substituting the type argument of`T`given in`U`everywhere`T`occurs in`V`, and then`U`has the inherited instantiation`W`of`Y`.If a type

`X`is a subtype of a type`Y`, and`Y`has an inherited instantiation`W`of a generic type`Z`, then`X`also has this inherited instantiation.

If a class or interface type `X` has the inherited
instantiations `V` and `W` of some
generic type `Y`, then:

for every invariant type parameter

`T`of`Y`, the type argument`A`of`T`given in`V`and the type argument`B`of`T`given in`W`must be exactly the same type, and, furthermore,`X`is a subtype of an instantiation`U`of`Y`such that`U`is a subtype of`V&W`.

Therefore, if a type `X` is a subtype of the
instantiations `V` and `W` of some generic
type `Y`, then either:

for some invariant type parameter

`T`of`Y`, the argument of`A`of`T`given in`V`and the argument`B`of`T`given in`W`are distinct types, and either`A`or`B`involves a type parameter, orif, for some invariant type parameter

`T`of`Y`, the argument of`A`of`T`given in`V`and the argument`B`of`T`given in`W`are distinct types, and neither`A`nor`B`involve a type parameter, then the type`V&W`is the bottom type`Nothing`, and we say that`V`and`W`are*disjoint instantiations*of`Y`, or, otherwise,`X`must be a subtype of an instantiation`P`of`Y`formed by taking each type parameter`T`of`Y`, and constructing a type argument`C`for`T`from the type arguments`A`of`T`given in`V`and`B`of`T`given in`W`:if

`Y`is invariant in`T`, then`C`is the same type as`A`and`B`,if

`Y`is covariant in`T`, then`C`is`A&B`, orif

`Y`is contravariant in`T`, then`C`is`A|B`.

Finally, the following identities result from principal instantiation
inheritance. For any generic type `X<T>`, and for any given
types `A` and `B`:

`X<A>&X<B>`is exactly equivalent to`X<A&B>`if`X<T>`is covariant in`T`, unless either`A`or`B`involves type parameters, and`X<A>&X<B>`is exactly equivalent to`X<A|B>`if`X<T>`is contravariant in`T`, unless either`A`or`B`involves type parameters.

If a type `X` is a subtype of some instantiation
`V` of a generic type `Y`, then, as a
result of the principal instantiation inheritance restriction, we can
form a unique instantiation of `Y` that is a subtype of
every instantiation of `Y` to which `X`
is assignable. We call this type the *principal instantiation of
Y for X*.

We compute principal instantiations by making use of the identities
observed above in §3.2.3 Union types, §3.2.4 Intersection types,
and §3.7.2 Principal instantiation inheritance.
For any generic type `X`:

The principal instantiation of the union

`U|V`of two instantiations of`X`,`U`and`V`, is an instantiation`P`of`X`formed by taking each type parameter`T`of`X`and constructing a type argument`C`for`T`from the type arguments`A`of`T`given in`U`and`B`of`T`given in`V`:if

`X`is covariant in`T`, then`C`is`A|B`,if

`X`is contravariant in`T`, then`C`is`A&B`, orif

`X`is invariant in`T`, and`A`and`B`are exactly the same type, then`C`is this type.

The principal instantiation of the intersection

`U&V`of two instantiations of`X`,`U`and`V`, is an instantiation`P`of`X`formed by taking each type parameter`T`of`X`and constructing a type argument`C`for`T`from the type arguments`A`of`T`given in`U`and`B`of`T`given in`V`:if

`X`is covariant in`T`, then`C`is`A&B`,if

`X`is contravariant in`T`, then`C`is`A|B`, orif

`X`is invariant in`T`, and`A`and`B`are exactly the same type, then`C`is this type.

Finally, the principal instantiation of a generic type

`X`for a type`Y`which has one or more inherited instantiations of`X`is the principal instantiation of the intersection of all the inherited instantiations of`X`.

Note: an intersection `X<A>&X<P>`
of two instantiations of an invariant type, `X<T>` where
one type argument `P` is a type parameter introduces a known
hole in our type system. It is impossible to form a principal instantiation of
`X` for this intersection type without resorting to use-site
covariance, so we don't allow references to members of the intersection type.

A class or interface may declare an `actual` member
with the same name as a member that it inherits from a supertype if the supertype
member is declared `formal` or `default`.
Then we say that the first member *refines* the second
member, and it must obey restrictions defined in
§4.5.6 Member class refinement, §4.7.8 Method refinement, or
§4.8.7 Attribute refinement.

A declaration may not be annotated both `formal`
and `default`.

If a declaration is annotated `formal`,
`default`, or `actual` then it must
also be annotated `shared`.

For any class or interface `X`, and for every declared
or inherited member of `X` that is not refined by some other
declared or inherited member of `X`, and for every other member
declared or inherited by `X` that directly or indirectly refines
a declaration that the first member itself directly or indirectly refines, the
principal instantiation for `X` of the type that declares the
first member must be a subtype of the principal instantiation for `X`
of the type that declares the second member.

Note: a related restriction is defined in §5.1.1 Declaration name uniqueness.

A type declaration that directly occurs in the body of another type
is called a *nested type*. If a nested type is annotated
`shared`, it may be used in a type expression outside the
body in which it is declared, if and only if it occurs as a
*qualified type*, as specified in
§3.2.7 Type expressions.

The qualified types `X.U` and `Y.V`
are exactly the same types if and only if `U` is exactly
the same type as `V`, and in the case that this type is
a member of a generic type `Z`, then the principal
instantiation of `Z` for `X` is exactly
the same type as the principal instantiation of `Z` for
`Y`.

A qualified type `X.U` is a subtype of a qualified
type `Y.V` if `U` is a subtype of
`V`, and in the case that `V` is a member
of a generic type `Z`, then `X` is a
subtype of the principal instantiation of `Z` for
`Y`.

Given a member declared by `Y`, and a declaration that
refines it, we can construct a *refined realization* of
the member or nested type:

first determine the principal instantiation of

`Y`for the class or interface which refines the member, and thensubstitute the type arguments in this principal instantiation into the member schema.

Given an unqualified reference, as defined in
§5.1.7 Unqualified reference resolution, to a declaration, and, in
the case of a generic declaration, a list of type arguments for the type
parameters of the declaration, we can construct an *unqualified
realization* of the declaration:

if the declaration is a member declared by a type

`Y`, first determine the principal instantiation of`Y`for the inheriting or declaring class or interface, and thenagain, only if the declaration is a member declared by a type, substitute the type arguments in this principal instantiation into the declaration schema, and, finally,

substitute the type arguments into the declaration schema.

Given a qualified reference, as defined in
§5.1.8 Qualified reference resolution, with a qualifying type
`X`, to a member or nested type declared by `Y`,
and, in the case of a generic member or generic nested type, a list of
type arguments for the type parameters of the member, we can construct a
*qualified realization* of the member or nested type:

first determining the principal instantiation of

`Y`for`X`, and thensubstituting the type arguments in this principal instantiation into the declaration schema, and, finally,

in the case of a generic member or generic nested type, substituting the type arguments into the declaration schema.

If, for any given qualified or unqualified reference, it is impossible to form the principal instantiation of the type that declares the referenced declaration, due to the hole described above in §3.7.3 Principal instantiation of a supertype, it is impossible to form a realization, and the reference to the declaration is illegal.