3. Type syntax

Type       = Union .
Annot      = Inter .
Union      = Inter { "|" Inter } .
Inter      = Diff { "&" Diff } .
Diff       = Prim { "-" Prim } .
Prim       = FnType | DataType | NamedType | TypeCall | ValueType | Literal | "_" | "{" Type "}" .
FnType     = [ TypeParams ] FnParam [ "<-" Needs ] "->" Union .
TypeParams = "<" UpName { "," UpName } [ "," ] ">" .
FnParam    = DataType | "{" Type "}" .
Needs      = UpName | "(" [ NItem { "," NItem } [ "," ] ] ")" .
NItem      = NamedType | ".." UpName .
DataType   = "(" [ TItem { "," TItem } [ "," ] ] ")" .
TItem      = [ name "=" ] Type .
NamedType  = [ name "." ] UpName [ "(" Type { "," Type } [ "," ] ")" ] .
ValueType  = [ name "." ] name .
TypeCall   = [ name "." ] name "(" [ TypeArg { "," TypeArg } [ "," ] ] ")" .
TypeArg    = Type .
Literal    = int_lit | "-" IntPart | string_lit .
IntPart    = int_lit | "{" IntPart "}" .

An UpName with no module name before it is a type parameter when one with that name is in scope where the type is written (§4.7, §5), and a type when not. _ is a hole that type inference fills in.
A Literal is a literal type (§4.2): "a", 0, -1. A - followed by an integer literal, also inside groups, where a Prim begins, is part of the literal: -{1} is -1. Every other - is a difference. So Int - -1 is Int without -1, Int - 1 is Int without 1, and -1 | 1 is a union of two literal types. A float literal is not a type, because Float has no literal types.
A type parameter takes no arguments: A(Int), where A is a type parameter, is a compile error.
A lowercase x in a type, without ( after it, means the type of the value named x at that place. The name follows value scope (§5). m.x means an exported value of module m, never a key of a value. If m names a value, it is a compile error. { x } groups the same type. A lowercase name or member followed by ( is a macro call, not a value type or a type application.
A type may not name a value bound by that same pattern; a name of a parameter group in the types of that function’s own head, including its <- and -> parts; or its own binding’s name inside that binding’s value. A distinct inner binder that has entered scope may cover that name. This is a compile error even if an outer value has the same name. Those names may be named in types in the body. For example, (x, y : x) and (x) -> x { x } are errors, but (x : Int) { y : x = x y } is allowed.
A value type is not its known type (§4.8). It follows the scheme, instantiation and completion rules of §4.7. It never makes a monomorphic value polymorphic.
A value type, directly or through names, may not occur in the data of a labelled type, an external or host declaration, or a need. Those types must be complete before inference.
A lowercase name, or a.m with a lowercase m, whatever a is, followed by ( is a TypeCall. It is a macro call in the position of a type (§14.5), and a compile error when its name is not a macro. It is in the grammar, so a type with it is read in full.
A | B is a union, A & B is an intersection, and A - B is a difference (§4.4). - is stronger than &, and & is stronger than |.
( … ) is a data type (§4.1). Its items are T, the next position, and name = T, a label. Positions come before labels, and a label may not occur twice. () is the data type of the empty data. A : in a type is a compile error: labels are written name = T, and a function type has no parameter names.
( … ) -> R is a function type whose parameter is that data type. { T } -> R is a function type whose parameter is T: every member of T, after expanding names, must be a data type, and two members may not have one shape. This is the type of a function with several shapes (§4.6).
After every : that introduces a type, the grammar reads Annot, not Type: the annotation ends at any | outside brackets (( ), { }, < >). In an Annot, an unbracketed function type also reads Inter for its result, recursively, instead of Union. Bracket contents read the full Type grammar. A union annotation is written x : { A | B }; a union result is written f : (Int) -> { Int | String }. In f : (Int) -> Int | String = e, the | ends the annotation, so this is a compile error. & and - keep their precedence. This one rule applies to declarations (§2.5), pattern annotations (§7.1), and service items (§6.8), whose types are further restricted there. In bit-array value and pattern segments, : introduces a Format, not a type (§8.1), and this rule does not apply.
In type positions that do not follow :, a function type goes as far to the right as it can: (A) -> B | C gives B | C. Type definitions T = A | B, List((Int) -> Int | String), and data-type items (x = Int | String) are unchanged. { } puts a type in a group: { (A) -> B } | C, (A) -> { (B) -> C } | D.
<- N is the need of a function type (§4.6, §9.2). <- (T1, …, Tn) lists named service types, in any order; at most one item is ..N, a row variable. <- N with a bare UpName is the same as <- (..N), and N must be a type parameter in scope. A missing <- part means “needs nothing”, in every place where a type is written; <- () is not written. Two items with one type constructor are merged as §9.2 says.
<A, N> before the parameter part binds type parameters for the rest of that function type (§4.7). <> is one token, so an empty list of type parameters cannot be written.
Opaque is not a type. It is only the right side of a type definition (§4.3).
A { } in a type groups exactly one type. Breaks in data types separate items; breaks directly in type groups are compile errors.