4. Types

4.1 Types denote sets of valuesCopy Anchor Link

Every type denotes a set of values. The union of two members of one type constructor is their least upper bound (a join) in the lattice of types ordered by subtyping (§4.5), subject to the merging rules of §4.4. Its set of values can be larger than the exact union of the two sets.

• Values of different type constructors are never the same.
• Values of different forms of one type constructor, such as List(Int) and List(String), may not be told apart at run time (§7.1).
• Data is a finite map from keys to parts. A key is a position, counting from 0, or a label, a name. The shape of data is its number of positions and its set of labels. Data of one shape is one type constructor; data of different shapes are different type constructors. () is the empty data, of the empty shape.
• Each labelled type (§4.3) is a type constructor of its own. Its values are never data, and data is never a value of a labelled type.
• The values of a function type are functions. All function types are one type constructor.

A member of a type (§4.4) is a type constructor, its type arguments, and a value set: the values of that type constructor that are in the member. Only Int and String may have a value set that is not all of their values (§4.2). For every other type constructor, the value set is all of its values.

Inhabitance. A type is empty when it has no values, and every empty type is equal to Never. Data is inhabited exactly when every required part is inhabited. A non-opaque labelled type is inhabited exactly when its data is inhabited. Apply these rules after substituting its type arguments. Thus (Never, Int) and Box(Never) with Box(A) = (A) are Never. List(Never) is inhabited: it contains [].

Recursive labelled data denotes finite values. Its inhabitance is the least fixed point of these rules: start recursive members as empty, then admit a member when its data can be made from already inhabited parts, until no new member is admitted. Thus Loop = (Loop) is empty, whereas a recursive union with a nonrecursive base can be inhabited. A function field requires a function value, not a value of its result type; a function that stops or diverges can inhabit () -> Never. Do not infer emptiness of an opaque or built-in handle type merely from an empty type argument.

Coverage, usefulness, subtyping and the empty match (§6.12) use this same inhabitance rule; destructuring an impossible value first is not required.

4.2 Built-in typesCopy Anchor Link

These types may be used in every module and named through i/core, for example core.Int after (core = i/core). So a module that defines a type with the name of a built-in type can still name the built-in type. The prelude types may be named through i/prelude.

These prelude types are normal type definitions (§4.3):

True = ()
False = ()
Bool = True | False
Nil = ()
Ok(A) = (A)
Error(E) = (E)
Result(A, E) = Ok(A) | Error(E)

The types Fail (§9.3), Assert and AssertionFailure (§9.6) are prelude types too. The types Boundary and Continuation are in §9.4. The types Key and Keyed are in §9.8. Request(A) and Ticket are built-in types, with operations in i/request (§9.11). Request(A) contains request handles whose answer belongs to A. Ticket is an answer-erased handle. Neither has public constructors.

Literal typesCopy Anchor Link

Every value of Int and of String is also a type, the literal type with only that value. It is written as the literal: 1, -1, "a". 1 <: Int, and "a" <: String. Two Int literal types are the same when their numbers are equal, so 0x10 is 16 and -0 is 0. Two String literal types are the same when their scalar values are equal (§11.4).

The value set (§4.1) of an Int or String member is one of these:

• all the values: Int, String;
• a finite set of values: "a" | "b";
• all the values but a finite set: String - "a" - "b".

Union, intersection and difference of these sets give a set of the same kind, so the rules of §4.4 and §4.5 always have an answer, and inference still finds principal types (§4.7). Float, BitArray and UtfCodepoint have no literal types.

Values are never changed, so a literal type is never made wider: x = "a" gives x the type "a", and [200, 404] has the type List(200 | 404). Such a value may be used where a String or an Int is needed, because "a" <: String. Operators give the whole type: 1 + 1 has the type Int (§6.9).

4.3 Type definitionsCopy Anchor Link

TypeDef     = UpName [ TypeHead ] "=" TypeRhs .
TypeHead    = "(" TypePattern { "," TypePattern } [ "," ] ")" .
TypeRhs     = "Opaque" | Type .
TypePattern = UpName | "_"
            | [ name "." ] UpName "(" TypePattern { "," TypePattern } [ "," ] ")"
            | name "." UpName
            | "(" [ TPItem { "," TPItem } [ "," ] ] ")" .
TPItem      = [ name "=" ] TypePattern .

A type definition has one form, Name [ (params) ] = right side. Its kind is decided by the outermost written form of the right side, before any expansion, in this order:

1. Alias pattern. The right side, after removing groups, is a value type (§3).
2. Opaque type. The right side is the word Opaque, not in a group.
3. Labelled type with data. The whole right side is one data type, not in a group.
4. Name. Any other right side.

• For kinds 2 to 4 the head is a list of type parameters: distinct, unqualified UpNames with no arguments, which do not already name an accessible type.
• T = Opaque defines a new opaque type, a labelled type whose values i code cannot make or take apart. They come from the host (§10), including @js declarations (§10.1.1). Opaque anywhere else, and a type named Opaque, are compile errors.
• T = D, where D is a data type, defines a new labelled type with the data D, and its one constructor, also named T. The constructor is the function { D } -> T(P1, …) (§4.6), or, when D is (), the value T. Two labelled types are different types even when their data is the same. The module defines the constructor name T in its space of value names (§2.3).
• Any other right side defines a name: a transparent alias for the type on its right. A name may not occur in its own expansion, directly or through other names or alias patterns. The data of a labelled type is not part of the expansion of a name, so a name may reach itself through the data of a labelled type: Tree(A) = Leaf | Node(A) with Node(A) = (Tree(A), A, Tree(A)) and Leaf = () is correct, but T = List(T) is not.
• In a name, every parameter must be used, and every type parameter on the right must be a parameter of the head. In a labelled type, a parameter need not be used. A parameter of a labelled type that its data does not use, and every parameter of an opaque type, does not change (§4.5 rule 6); the other parameters change as the data says.
• A sum is a name for a union, or a labelled type whose data is one item of a union type. Its members may be any types, labelled or not, also built-in types and data types. Values of a sum are told apart by type tests and constructor patterns (§7.1), so every two members of a sum must have different type constructors (§4.4). Members that would share a type constructor are each wrapped in a labelled type. One labelled type may be a member of several sums.
• { D }, a data type in a group, is a name for that data type: Point = { (Int, Int) } makes Point mean (Int, Int), while Pair = (Int, Int) makes a new labelled type.
• An item T(P1, …, Pn) = v is an alias pattern exactly when its written right side is a value type (§3), after removing groups. This classification is made before expanding the right side; it never depends on imports or on what a macro returns there.
• In an alias pattern, the unqualified head names an existing type, with the written arity; the item does not define that head. It may be a labelled or built-in type, or a name expanding to one named type or data type. In a head name each parameter is used at most once, only as a named argument or a data part. Constant subtrees of that name require an equal, fully determined source part.
• A bare unqualified UpName in a pattern always defines a new zero-parameter name. Its part of the source type must be fully determined (§4.7). It may not duplicate a definition or conflict with an imported or built-in type. It never tests an existing type with that name.
• _ in an alias pattern skips a part and binds nothing; it is not an inference hole. For a new read after source completion, the whole source type must first be closed (§4.7); a skip cannot hide an open argument from that check. Elsewhere in a type, _ remains a hole. Shared type variables remain shared even if one occurrence is skipped.
• A named pattern with arguments, or a qualified named pattern, requires exactly one member with that type constructor and matches its arguments. A data pattern requires one member that is data of the same shape and matches its parts at their keys. No union member is discarded to make a match. A mismatch is a compile error. Function, literal, union, intersection, difference, value-type and macro-call patterns are compile errors.
• Every pattern and every value-dependent name is checked, also when unused. Its demands are processed at the completion of their source (§4.7), and its results are assembled after its name dependencies are complete. A new read after source completion follows the closed-source rule in §4.7. A definition read may not choose an instance of a generalized variable to make its pattern fit.
• Blocks have no type definitions. An item beginning with ( or { is a value binding; m.T(…) = v is also a value binding under §2.2. Import T to use it as an alias-pattern head.

Some(A) = (A)
None = ()
Option(A) = Some(A) | None
User = (name = String, age = Int)
Pair(A, B) = (A, B)
Point = { (Int, Int) }
Meters = Int
Element = Opaque

Codec(D, E) = (decode = (String) -> D, encode = (E) -> String)
size = Codec(
	decode = (s) { string.length(s) },
	encode = (n : Int) { int.to_string(n) },
)
Codec(Size, _) = size

A type application must leave every occurrence in its definition well formed. This requirement follows arguments through aliases and other type applications. In particular, an argument used as a function need must describe services as §9.2 requires; being passed through a named type does not make a scalar value type a valid need. Check this requirement on each instance, including unused type definitions, before solving value-subtyping constraints. The type-parameter uses themselves obey §4.7.

Here Pair(Int, Int) is a labelled type, not (Int, Int); Point is (Int, Int); and the alias pattern makes Size the type Int, leaving the encode part unread.

4.4 Union, intersection, and differenceCopy Anchor Link

• A | B is the least upper bound (join) of A and B under subtyping (§4.5). It contains every value of either type, and merging members of one type constructor can add values beyond the exact union of their sets. Order has no effect, A | A is A, and A | Never is A.
• Members of a union with the same type constructor are put together into one. For Int and String, the value set of the member is the union of their value sets: "a" | "b" is one member, and "a" | String is String. T(A1, …) | T(B1, …) is T(C1, …), where for each parameter of T (§4.5 rules 6 and 7), Ci is Ai | Bi when the parameter goes in the same direction as the type, and Ai & Bi when it goes in the other direction. When the parameter does not change, Ai and Bi must be equal, and Ci is that type; if they cannot be equal, it is a compile error. Data of one shape is one type constructor, whose part under each key goes in the same direction as the data. All function types are one type constructor: (P) <- N -> R | (Q) <- M -> S is (P & Q) <- N ∧ M -> R | S, where N ∧ M is the merge of the two needs (§9.2). When P and Q have no shape in common, P & Q is Never, and the function cannot be called. So List(Int) | List(String) is List(Int | String).
• The members of a type are the types that make it up as a union, after these rules are used. So no two members of a type have the same type constructor. A type variable may be a member.
• The values of A & B are the values that are in both A and B. { A | B } & C is A & C | B & C. When T and U are not type variables, T & U is Never when they have different type constructors; when they have the same one, it is that type constructor with each pair of arguments put together the other way round: & where the parameter goes in the same direction, | where it goes in the other direction, and equal where it does not change. If an invariant pair is unequal, the intersection is Never; unlike a union of unequal invariant forms, this is not a compile error and does not force the arguments to be equal. For Int and String, the value set is the values in both; when there are none, T & U is Never. So "a" & String is "a", and "a" & "b" is Never. a & T, with a type variable a, stays as it is.
• Intersections come from inference. (x) { x + 1 x } has the type (a & Int) -> a: the value that comes in is given back, and it must be an Int.
• A - B takes out of A every member whose type constructor is the type constructor of a member of B. For Int and String, it takes out only the values of the value set of that member of B (below). These rules work it out:
  • { A | B } - C is A - C | B - C, and A - { B | C } is A - B - C.
  • When T and U are not type variables: T - U is T when they have different type constructors. When they are both Int or both String, T - U has the values of the value set of T that are not in the value set of U, and is Never when none are left: String - "a" is every string but "a", {"a" | "b"} - "a" is "b", and "a" - String is Never. For every other type constructor that is the same in both, T - U is Never.
  • The right side of a written - may not have a type variable as a member. Every type argument of a named member there, and every part of a data member there, must be a hole _, after aliases are expanded. List(_) can remove lists; List(Int) cannot select just lists of Int. The holes describe the constructor or shape being removed and impose no new bound on the left side’s arguments. Inferred exclusions use this same constructor-only operation; their arguments do not add constraints. a - U, with a type variable a, stays as it is until a is known.
• So { Int | String | Nil } - String is Int | Nil, List(A) - List(_) is Never, and { Yield(a) | n } - Yield(_) is n - Yield(_).
• { Int | String | Nil } - "a" - 1 is Int - 1 | String - "a" | Nil.
• Unions, intersections, and differences may be used in every place where a type may be used. In a written type, a union with two or more type variables as members may only be in an output place, and an intersection with a type variable only in an input place (§4.5 rule 6), because inference cannot choose between them in the other places. The parameter of a function is an input place; its -> part, the type at the top of a binding pattern, and the data of a type are output places. The parts of data keep the direction of the place of the data. The restrictions on variable members apply to expanded annotations and shown types, including after substitution and completion.

Merging loses correlations between parts of data of one shape and between arguments of one type constructor. Thus (Int, String) | (String, Int) is (Int | String, Int | String), which also contains (1, 2). If Pair(A, B) = (A, B), then Pair(Int, String) | Pair(String, Int) likewise admits Pair(1, 2). List(Int) | List(String) admits [1, "a"], even though neither original list type does.

Keep a correlation by giving each alternative a distinct labelled constructor (§4.3):

IntString = (Int, String)
StringInt = (String, Int)
Correlated = IntString | StringInt

The two members of Correlated have different type constructors and do not merge: IntString(1, "a") belongs to it, while IntString(1, 2) does not.

4.5 SubtypesCopy Anchor Link

A <: B says that every value of A is a value of B. These are the rules:

1. Never <: A, and A <: A.
2. A <: A | B. A | B <: C when A <: C and B <: C. A & B <: A. C <: A & B when C <: A and C <: B.
3. A - B <: A. X <: A - B when X <: A and X and B are disjoint: every member of X and every member of B have different type constructors, or are both Int or both String with value sets that have no value in common. So "a" and "b" are disjoint, and "a" and String - "b" are not. Only the members themselves are compared, not their type arguments: (1, 2) and (3, 4) are not disjoint. A type variable as a member is never disjoint from anything.
4. {P} <- N -> R <: {Q} <- M -> S when Q <: P, R <: S, and N fits in M: for every type constructor C with an entry in N, M has an entry for C and M_C <: N_C, or N and M have the same row variable and it carries C. Here {P} is the parameter type, a data type or a union of data types. A need is the intersection of its services, so needs are compared in the reverse direction of values.
5. Data of the same shape: D1 <: D2 when the part under every key of D1 is a subtype of the part under the same key of D2. Data of different shapes are disjoint.
6. A type parameter of a labelled type changes in the same direction as the type, in the other direction, or not at all. This is decided from the definition: a parameter that is only in output places goes in the same direction; one that is only in input places goes in the other direction; one that is in both does not change. The data of a labelled type is an output place, the parameter of a function type is an input place, and a place inside an input place is the other way round. A parameter that the data does not use, and a parameter of an opaque type, does not change.
7. List(a) goes in the same direction as a. In Continuation(A, R, N), A goes in the other direction and R and N in the same direction. Boundary(R, N) does not change.
8. A member of Int or String is a subtype of a member with the same type constructor when every value of its value set is in the value set of the other. So "a" <: "a" | "b" <: String, and String - "a" <: String, but String is not a subtype of "a" | "b", and String - "a" is not a subtype of "b".

For recursive definitions, determine variance for all definitions together, independently of declaration order. A parameter is bivariant when changing its argument does not change the type at all: T(A) and T(B) are equal for any A and B at that parameter. Such an argument adds no constraint to subtyping, union or intersection. It differs from an invariant parameter, whose arguments must be equal.

Use the greatest fixed point of the variance constraints. Start recursively determined parameters as bivariant. Propagate the output and input places of rule 6 through data, functions, and the current variances of named arguments; an invariant argument propagates both places and a bivariant argument propagates neither. Repeat for all definitions until no variance changes, retaining only directions allowed by their data. Opaque parameters and parameters not used in the written data remain invariant throughout. An unused parameter of a labelled type is legal (§4.3); it is not a reason to reject the definition. For example, Chain(A) = (next = Chain(A) | Nil) is bivariant in A, while Phantom(A) = () has the explicitly unused, invariant parameter.

Two types are equal when each is a subtype of the other. A value of a subtype may be used in every place where a value of the type is needed.

Key(A) (§9.8) does not change. Request(A) (§9.11) goes in the same direction as A. The variance of task types follows their definitions (§9.9).

4.6 Function typesCopy Anchor Link

The function type { D } <- N -> A has one parameter, the complete argument data type D; a need N after <-, the services that it takes from where it is called (§9.2); and a value A after ->, the type of the value that it gives back. Errors are the need entry Fail(E) (§9.3), so Effect<A, E, R> of Effect-TS is () <- (..R, Fail(E)) -> A. A missing <- part means “needs nothing”.

The shape of D is part of the type: its positions and its labels. There is no currying and there are no default parameters. { D1 | … | Dn } <- N -> A, where the Di have different shapes, is the type of a function with several shapes (§6.12): calling it with data of the shape of Di needs that data to be in Di, and gives A. Such a type is a subtype of each of its shapes, { (Int) | (Int, Int) } -> R <: (Int) -> R, so a function with several shapes may be given where a function of one of them is needed.

When a metavariable already denotes complete argument data, braces put that type in a group; parentheses would add a position. Thus with D = (Int, Int), { D } -> Int means (Int, Int) -> Int, whereas (D) -> Int means ((Int, Int)) -> Int. Typing formulas use { P } or { B } for complete parameter data for this reason.

f = (a : Int, b : Int) { a + b }
main = () { f(1, 2) }

<A, N> before the parameter part makes the type polymorphic (§4.7).

A written polymorphic type binds its parameters universally. Bound names are local to that type and may be renamed without changing it. They are not free variables for the variance of an enclosing labelled type; free variables in the quantified body still follow the ordinary input and output places.

To check subtyping against a polymorphic type, first replace its bound parameters with fresh rigid types. Instantiate a polymorphic source with fresh inference variables, then check the bodies by §4.5. An instance may use the rigid types in scope, but none may escape its comparison. An instantiation is a monotype: it does not introduce a new universal binder. Invariant places require subtyping both ways. This is the same rigid check used when a value is checked against a written polymorphic type (§4.7).

A union or intersection of polymorphic types keeps each complete quantified type as an operand. Do not instantiate their binders to merge them as ordinary function members, or move a binder across | or &. The unquantified function merge of §4.4 applies within their bodies, not across the quantifiers. Equal operands, including renamed bound parameters, coalesce; subtyping can remove a redundant operand by the join and meet laws of §4.4. These operations never infer a new polymorphic parameter type that was not written.

4.7 Type inferenceCopy Anchor Link

Types are worked out by inference with subtypes (algebraic subtyping).

• Type annotations may be left out everywhere for inference, but not on @external or @js declarations. Some uses of a name need a known type, which may need an annotation (§4.8).
• Foreign linking (§10.1.2) does not change inferred source types or remove inferred needs.
• For every binding, the compiler must find the principal type: the most general type, of which every other possible type is an instance; where it cannot, it must report a compile error. This is a requirement on the compiler, not an established guarantee for every feature of i. MLsub (Dolan and Mycroft, POPL 2017) and MLstruct (Parreaux and Chau, OOPSLA 2022) give ways to do this for their respective calculi; the argument for i and its unproven parts are in Principality in i.
• A type is made simpler before it is shown: equal parts are put together, and type variables that have no effect on the meaning are taken out. This never changes which programs are correct or what they do. A type scheme that is used as a known type (§4.8) is in this simpler form. A type variable that is not generalized is shown as the union of the types that come to it. A union that is the expansion of a declared name is shown by that name.
• Annotations are used in inference, and the inferred type must agree with them. A type variable in an annotation may become a more exact type.

Type parameters.

• A function expression may begin with <A, N, …> before its parameter group (§6.8), and a function type may begin with it before its parameter part (§3). The names are distinct unqualified UpNames that do not name a type that may be written with no module name in the module (a type of the module, an imported UpName, or a built-in type). A type definition declares type parameters in its head (§4.3). The parts of an alias pattern are not type parameters: its bare UpNames define names.
• On a function expression, the type parameters may be used in its parameter group, its service pattern, its -> part and its body, also in nested functions and annotations there. On a function type, they may be used in the rest of that type.
• A type parameter used where a need is written (<- N, <- (..N, …)) is a row variable: it stands for a whole set of services. Any other use makes it an ordinary type variable. Using one name both ways is a compile error.
• On a function expression, a type parameter is a type variable of that function, and it is generalized with it. Inference may make it more exact: id = <A>(x : A) -> A { 1 } is correct.
• A written function type with type parameters in a parameter, in the data of a type, in a type definition, or in an annotation is a polymorphic type, as Show = (write = <A>(A) -> Nil). Its comparisons and quantified lattice operations use §4.6; each use instantiates it again. Inference never guesses a polymorphic type: a parameter gets one only from a written type.
• An UpName in a type that is neither a type nor a type parameter in scope is a compile error. The message says how to declare it.
• A bound on a type variable is written as an intersection where it is used, as x : A & Show. Capabilities are passed as parameters or as services; none is passed implicitly.

Generalization.

• A binding is generalized when its value is a direct value (§6.10): the type variables of its type that are not in the types of names from outside it become general, so each use of the name may give them different types. A binding whose value is not a direct value is not generalized, because working out its value runs code, and that code may make a value for one type only (for example with control.suspend). This is the value restriction of ML, which is known to be safe. Functions are direct values, so every function binding is generalized.
• A type variable that is not generalized is one type for all uses of the binding.
• Parameter groups (§6.11) are matched like bindings, but they are not generalized. Their values are not known where they are written, so each of their names has one type in the whole branch. So (f) { (f(1), f("a")) } needs f to take both Int and String.
• Inside its own value (§6.10), a name of a binding is not general: all its uses there have one type. It becomes general when the binding is generalized.
• A group is a set of top-level bindings that use one another, directly or through other bindings of the group. The bindings of a group are worked out together and then generalized together, after the groups that they use. Inside the group, their names are not general.
• A type that has itself inside it, through a type variable, is a compile error. The parts of data count as places inside a type constructor.
• Simplification and type display preserve type variables that affect invariant arguments, even when their input and output forms print alike. Reading a type never generalizes a weak variable.
• A long union of literal types may be shortened in messages and hovers, as "a" | "b" | … (40 more), but never in a type scheme or in the interface of a package. An inferred type may have literal types in it, also in the interface: an exported constant or an unannotated exported function whose value is a literal has that literal type, so giving one more literal as a value changes the interface. Exported functions should have written types, as the standard library has.

Reading types of values.

• In an annotation, a completed generalized value is read as a fresh instance of its scheme (§4.8 rule 3), separately for each occurrence. A parameter name or local monomorphic value shares its one type. Generalized local schemes also keep their non-general variables shared. A completed top-level value uses its fixed non-general parts; reading an unfixed part is a compile error. Reading through a local does not copy such a part or allow a name to escape from it. A value type never generalizes its source or its annotated binder.
• In a name or alias pattern, every used value-derived part must be closed: it has no generalized variable, unresolved type variable, unknown top type or hole. The name’s own declared parameters remain parameters. A skip demands no contents, but the shapes needed to reach the used parts must also be determined.
• A top-level value’s group has one completion point, after its values are typed and linked and its generalization is decided. All value-type demands written in its own module are collected before inference, including annotation reads and unused type definitions. An annotation read takes part in fixation like a name read; its quantified parts still use fresh scheme instances. Ordinary group checks finish first. All demands at this completion point read one unchanged snapshot and are checked in one batch before any permanent name is published. At this point their weak parts are fixed as follows. A demand in another module never fixes them.
• For a demanded non-general variable, collect all types that come to it, including through variable relationships. Put them together by union, replacing the non-general variables needed inside them by their fixed types. Pure cycles of variable relationships count once. A structural recursive type, an unfilled part, a generalized variable needed inside this replacement, or a part that cannot be made closed is a compile error. An explicit closed Never is allowed; the absence of any information does not invent Never. Literal types are never widened.
• Fixing adds both subtype constraints between the variable and the resulting closed type, keeping every previous constraint. Every needed variable is fixed together, and the usual occurs and place rules apply. If these equations cannot hold, it is a compile error. Pattern shape checks use the original argument variables, so skipping a distinct argument leaves it shared and unfixed. The pattern cannot supply a type to fill an unknown.
• A group that constrains an earlier non-general variable that was not fixed cannot fix its own non-general parts. A demanded part carrying such an earlier variable also cannot be fixed. This conservative rule makes the result independent of unrelated groups’ inference order.
• From then on, later uses must agree with each fixed part. A use that would widen it incompatibly is a type error with a note at the place that fixed it. Write a wider annotation at the source when needed. For example, reading r = task.ref(1) may fix its invariant argument to 1; write r : Ref(Int) = task.ref(1) to allow other Int values.
• In another module, or when a new definition read is performed by a later group, an alias pattern or other permanent value-derived definition must start from a wholly closed completed source type. A fixed component behind an open enclosing type is not sufficient, even when the open arguments are skipped. This read adds no constraints to the source. If the source remains open, the error says to use the closed name made by its source module and to export it when needed. Annotation instantiation and current-group local monotype sharing keep their rules above. Adding foreign fixation demands cannot change the source module’s completion result. Ordinary expression constraints and local monomorphic sharing remain shared as elsewhere in this section; this rule does not fix the display of every uncompleted weak part.
• A permanent name denotes the completed closed part. It does not change when later bindings are checked. A same-module top-level pattern is handled at its source’s completion, regardless of where the item is written. Names with several sources assemble already closed per-source results, not saved partial source types. Definitions are completed before their dependents. Importing or using the closed name later does not read its source value again.
• The whole annotation after value types and names are read must obey §4.4’s rules of places. A value-type spelling does not hide variable members from that check.

4.8 Typing rulesCopy Anchor Link

Γ ⊢ e : A <- N says: with the names in Γ, the expression e has the type A and needs the services N (§9.2), errors included as Fail(E) (§9.3). Γ gives every name a type scheme ∀a1 … an. T. A program is correct when every binding has a type by these rules. Every rule may use any N; the parts of one rule use the same N, unless the rule says otherwise. Every value that an expression can have at run time is in its known type (below); selection (rule 5a), narrowing (rule 12) and keys (rule 13) depend on this.

1. Subtypes. If e : A <- N, A <: A', and N fits in N' (§4.5 rule 4), then e : A' <- N'.

2. Literals have the types of §6.3.

3. Names. If Γ(x) = ∀a1 … an. T, then x : T with each ai changed to any type.

4. Functions. Let the parameter group be the data pattern q, and the service pattern x1 : T1, …, xk : Tk (§6.8). q is fitted to a data type P (below). If Γ with the names of q and xi : Ti gives body : A <- M, the function has the type { P } <- M' -> A, where M' is the merge (§9.2) of M, every Ti, and Assert when q may fail for P (§7.3). With ..env : N in the service pattern, M must fit in (..N, T1, …, Tk), and M' is (..N, T1, …, Tk). If the function writes -> R, check its body with expected type R and require A <: R; the function’s result type is then R. Without that part, its result type is A. A written <…> is scoped and checked by §4.7 before those body constraints are solved. Making the function needs nothing.

5. Calls. If f : {P} <- N -> A and the argument data d : D with D <: P, then f(d) : A <- N. 5a. Selection. When f is a name with a selection table (§6.12), its type at the call is the type of the selected branches, computed from the known types of the arguments before inference constrains the call. 5b. Provide. For e <- s, where e : A <- N and the provided data has keys K with types T_k (§9.2): for every k in K that N has, T_k <: N_k. The provide has the type A <- N', where N' is N without the keys K, merged with the need of working out s. A provided key that N does not have gives a warning. When N has a rigid row variable, a key that it may carry and that N does not state is a compile error.

6. Data and lists. If every item ei : Ti at key ki, the data has the data type with Ti at ki; a spread contributes the parts of the type of its base at their keys. If every ei : T and r : List(T), then [e1, …, en] : List(T) and [e1, …, en, ..r] : List(T).

7. Constructors are functions from their data type to their type, or values when the data is () (§6.7).

8. Operators are not functions. Each has the types of §6.9. a |> f(b) has the type of f(a, b).

9. Blocks. { s1 … sn e } has the type of e, with the names bound by s1 … sn (§6.10). The need of a block is the merge of the needs of its statements and of e.

10. Bindings. For p = e with e : A: p is fitted to A (below). If p may fail for A (§7.3), then Assert is in N.

11. Groups. This rule is for a shape group of a chain (§6.12) with more than one branch or with a guard. Let it be called with data of type B: in a match e |> C with e : A, the one-position data (A); in a call, the argument data type. The parameter patterns (each alternative of | counts) are looked at by place. The top place is the argument data. Below a pattern at a place, its parts are at places of their own: the part under each key of a data pattern, the part under each key of a constructor’s data, and the parts and the rest of a list. Places below different constructors are different places. At each place, let B be the type of the values there (the argument data at the top place, and else the part type of the pattern type above it), and let P be the union of the pattern types (below) of the patterns at that place that are not catch-alls. Patterns at one place with the same type constructor use the same new type variables, so Ok(v) and Error(e) at one place give Ok(b1) | Error(b2), and Some(v) and None give Some(b) | None. A type test x : T at a place also needs B <: T | r - T, with a new type variable r: it takes every value whose type constructor is that of a member of T, and that, for a member of Int or String, is in the value set of that member (§7.1), so those values must be in T. So v |> (x : Box(Int)) { … } | (y : Box(String)) { … } with v : Box(Int | String) is a compile error. A data or constructor pattern with .. counts as having a catch-all at the places of the keys that it leaves out. If some branch without a guard has a catch-all at that place or at a place above it, then B <: P | r - P, with a new type variable r: a value that no pattern takes may still come there. If not, then B <: P. So a group with only literal branches and no catch-all takes only those values: (0) { "zero" } | (1) { "one" } has the type (0 | 1) -> "one" | "zero". In a match e |> C whose subject already has a type with values that are in no literal of P, so that B <: P is not true only for that reason, as (n : Int) { n |> (0) { "zero" } | (1) { "one" } }, the error is the one of §7.4, with a value that no branch matches, and no other error is given for it. A chain that is not the right side of a match gets its values later, through the type of its parameter: from a call, or from the type it is given to, as in list.map(xs, (0) { "zero" } | (1) { "one" }) with xs : List(Int). Then there are two errors: a type error where the values come, and the error of §7.4 at the chain. A catch-all at a place gets the type of rule 12. Every guard has the type Bool, each branch body has its own type Ri, and the need of every guard and body is part of the need N of the chain. The group has the type { B } <- N -> R1 | … | Rn, and a match has the type R1 | … | Rn. Making the chain needs nothing, as for a function in rule 4. Coverage (§7.4) is checked with the types that inference finds.

    A group with one branch and no guard is not typed by this rule. It is the function of rule 4: its parameter group is fitted to the parameter type (below), it is not checked for coverage, and Assert is in its need when the pattern may fail. A match s |> (p) { e } with such a chain is typed as the binding p = s followed by e (rule 10), with the one difference that p is not generalized, as a parameter is not. So the subject s gets the expected type that a binding gives its value (below).

12. Narrowing. Let a catch-all be at some place in a parameter pattern of a group, and let B be the type of the values at that place. A type constructor T is taken at that place when every value that the branch’s pattern matches, with a value of T at that place, is matched by an earlier branch of the group without a guard. In the same way, a value v of an earlier Int or String literal pattern at that place, and a member of the type of an earlier type test at that place, is taken when every value that the pattern matches with it at that place is matched by an earlier branch without a guard. The catch-all gets the type B - H, where H is the union of the taken members: each taken type constructor with new type variables as its arguments, the literal type of each taken value, and each taken member of a type test. So in s |> ("a") { 0 } | (rest) { f(rest) } with s : String, rest gets String - "a". Guarded branches take nothing.

13. Keys. For v.k and v.f, v must have a known type or a structural hint (below), and every member of it must be data with that key, or a labelled type whose data has that key and whose constructor may be used here (§2.4). The inferred result is the union of those parts with the type arguments from the corresponding bound forms, or the constructor-pattern arguments already supplied by §7.5. The inferred type of v, using its branch-local view when there is one (§7.5), must fit the bound. If not, it is a compile error. The bound takes all Int and String values at covariant places, removes exclusions of only some of those values there, and takes fresh holes at noncovariant places. Use this bound also when a known function type constrains a call. Known key results are obtained separately from the original known facts, not by narrowing the inferred result to them. A known type may have fewer values than the inferred type: after x = "a" = s with s : String, x has the type String and the known type "a", and (x, 0).0 is correct.

14. Generalization. A binding whose value is a direct value is generalized (§4.7) after its value is typed. Other bindings and parameter groups are not.

A catch-all is a name, a discard, or a conjunction p1 = … = pk whose parts are all catch-alls.

To fit a pattern q to a type B, in a binding or in the parameter group of a group with one branch and no guard: if q is a catch-all, its names get B. If not, B <: Q, where Q is the pattern type of q, and the parts of q are fitted to the parts of Q given below. A constructor pattern C(…) with pattern type Q needs only B <: Q | r - Q, with a new type variable r: it may fail, and when the known type of the value is disjoint from Q the compiler warns that it can never match. Fitting never adds Assert by itself; rule 4 and rule 10 do. In any other group, rules 11 and 12 take the place of fitting.

Alternatives q1 | … | qn may occur in a parameter item of any shape group (§7.1). Their pattern domain is the union of the alternatives’ domains; successful matching may use any alternative. The binder requirements are those of §7.1. If one alternative is a catch-all, the names get B. If not, B <: Q1 | … | Qn, where Qi is the pattern type of qi, and alternatives with the same type constructor use the same new type variables. The parts of each qi are fitted to the parts of its Qi, and a name gets the union of its types in the alternatives (§7.2). In alternatives, x : T is a test, not a type annotation (§7.1), so T may not have a type variable as a member. The alternatives may fail for B when together they do not match every value of B (§7.3); then Assert is in the need of the function (rule 4).

The pattern type of a pattern that is not a catch-all, and its parts, are:

• A literal of Int or String, also - and an integer literal: in a group typed by rule 11, its literal type (§4.2); where it is fitted, Int or String, so that every value of that type may come there and the pattern may fail (§7.3). At a place whose type is shared with another place, or inside one, also Int or String: an item of a list pattern, because all the items of a list have one type, and a key of a constructor whose written data has a type parameter that occurs more than once in it (counting through names), as both parts of Twin(A) = (A, A), and the parts of the data of W(A) = ((A, A)). A literal type at one such place would be a type for all of them. So when that type is not written and does not come from the subject, a group that matches those places only with literals is not covered (§7.4): (xs) { xs |> ([]) { 0 } | (["a", ..]) { 1 } | (["b", ..]) { 2 } } gives xs the type List(String), and the error names a value such as [""]. With (xs : List("a" | "b")) written, the same chain is covered. A float literal: Float.
• C(…): C(b1, …, bm), the labelled type C with a new type variable for each type parameter. The part for each item is the part of its data type at that item’s key, with these variables.
• A data pattern: the data type of its shape, with a new type variable at each key. The part for each item is the variable at its key; a rest ..r gets the data type of the remaining keys of the unique known shape (§7.1).
• [p1, …, pn] and [p1, …, pn, ..r]: List(b), with a new type variable. The part for each pi is b, and r gets List(b).
• "lit" <> r, r <> "lit", and "a" <> r <> "b": String, and r gets String.
• A bit array pattern: BitArray. The parts get the types of their formats (§8.2). A literal value in a segment also has the type of its format, not its literal type.
• A conjunction p1 = … = pk: the intersection of the pattern types of its parts that are not catch-alls, and each name part gets that type.
• x : T: T, with new variables for holes and value types read as §4.7 says; x gets that type.

A value type in an annotation uses the inferred type of its source, not a narrower known type at the use. A completed scheme gives its known structural form, with _ for general variables. For a local source still being inferred, use its stored structural monotype with unresolved variables erased to _. A written type on the source name is part of that monotype. The known type of a matched value does not supply a type for a name inside its pattern. Do not infer a smaller shape from temporary lower bounds. Later literal tests or branch narrowing do not refine this shape. A local value type can read the type of a key result:

f = (d : (a = Int, b = String)) {
	a = d.a
	q : a = d.a
	q == 1
}
main = () { f((a = 1, b = "s")) }

Here a is a bound value, and q has the known type Int. For x = "a" = s with s : String, x’s inferred type is String even though its known type is "a"; an annotation naming x uses String.

The parts of data are covariant in the hidden-input and structural-hint operations below; invariant arguments inside them still count in both directions. An item written in a data literal gets the matching expected part, when guaranteed. The base of a spread gets no expected type.

A factual known type contains every runtime value possible at that expression in its reachable context, for every caller, provider, callback and use allowed by inference. _ imposes no restriction. Successful patterns can supply facts local to their branch even when the stored inferred type is wider. An initial value or an inference lower bound alone is not a fact about later hidden inputs. Selection, rule-12 factual narrowing and W0503 use only factual known types.

The known type K(e) of an expression is found from the parts of the expression, left to right, and from the expected type of its place (below). Where no case below gives it, e has no known type.

• A data literal has the data of the known types of its items, with _ for an item that has none; a spread contributes the known parts of its base.
• A literal, also - and an integer literal, also inside groups, has its type (§6.3), and a bit array has BitArray. A list has List of the union of the known types of its parts when they all have one, and List(_) when not. So [] has List(Never).
• An operator expression has the result type of §6.9; a |> f(…) is the call f(a, …).
• A match e |> C has the union of the known types of its branch bodies when they all have one.
• The names of a parameter group get known types as names in patterns (below), but the argument data has no known type. So x : T gives x the type T, and a parameter with no type has no known type. A name of a service pattern x : T has T.
• A built-in name, an imported name, and a member m.x of an imported module have their type scheme. So does the name of a generalized binding (§4.7), local or top-level, where it is used outside its own value and outside its group. A type variable in such a scheme that is not generalized is replaced by the matching part of the known type of the binding’s value, or by _. A constructor has its function type, or its type when it is a value.
• A function expression has the type made from: for its parameter data, the shape of its parameter group, with the type written at the top of each item (as in x : T), or else the type it gets from an expected type (below), or else _; and for the result, the written -> part, or else the known type of its body, or else _. A chain literal has, for each shape group, a known function type made in the same way, with the union of the known types of its branch bodies as the result when they all have one; a chain with several groups has the known multi-shape type { D1 | … | Dn } <- N -> R of §6.12. When the parameter of a group has a known type B, from a written type or from an expected type, every parameter pattern of the group is a pattern fitted to a value with the known type B, as in a match (below), and the narrowing of rule 12 is used in the same way. So with opts : List(Option(User)), list.map(opts, (Some(u)) { u.name } | (None) { "" }) is correct.
• A name used inside the value of its own binding, and a top-level name of the same group, get their known types only from what is written, because their values are not yet known there: from x : T at the top of the binding’s pattern when it is there, or else from what is written in the value, with _ for the rest. So a function that uses its own result in .f or .k needs a written -> part. Every other name bound by a pattern gets its known type as below.
• A known type may have _ in it, for a part that is not known. A part that is _ has no known type, but the rest of the type is still known. So the shape of a function is known even when its types are not.
• A call f(d), also when written with |>, has a known type when f has a known function type, and every type variable of its result gets a type when its parameter type is matched with the known type of the argument data (below). Then it has the result type with those types put in. A constructor with data is a call.
• To match a type P with a known type K: when P is a type variable, K is one of its types. When P is a named type, a data type, or a function type, and K has one member with the same type constructor, the parts are matched: the type arguments, the parts at each key, or the parameter and result types. When P is a union, each member of P that is not a type variable is matched with the member of K that has its type constructor, if there is one, and each type variable in P is matched with K less the other members of P (§4.4). A type variable in P that is matched with a _ in K, or with a type variable that is generalized in K, gets _, because that part may be any value. When P is an intersection, each of its members is matched with K. Before matching, a difference in K is replaced by its members (§4.4), and an intersection a & T by T. When a type variable gets more than one type, it gets their union. So matching (a | Nil) with (User | Nil) gives a the type User.
• Expected types. An expression may have an expected type from its place, as in TypeScript:

  • An item of the argument data of a call (also with |>) whose callee has a known function type has the type of the parameter data at that key. Its type variables are put in when matching the parameter type with the known types of the items before it fixes them. Function expressions that have a parameter with no written type, and names with a selection table of more than one branch, are left out of this matching, and come last: their expected types use all the other items. A function given as an argument may give values to the called function that the other arguments do not show: as its result, as the argument of a function it is given (a parameter of a parameter), or to a service of its need. A service in the called function’s own need gives it values that come from the caller’s provide. And a function that the called function gives back may get values from a later caller. Walk the type of the called function, also its own need: its parameter is given to it, its result is given by it, and every type variable in its own need is given to it, and the direction turns at each parameter of a function type and at each contravariant argument of a constructor; an argument of a constructor that is invariant or bivariant, and a need, count as both directions. A type variable at a place given to the called function, other than a place in the parameter reached from its top only through parts of data and covariant arguments of constructors (the argument shows the values there), is a hidden input. Its match is _ in the expected type of every item: the hidden values may have different type constructors from the other shown arguments. For the call’s known result, match the facts of all its arguments, including the results of callbacks after they have been checked. A hidden input not described by those arguments, in the callee’s need or supplied by a later caller of its result, still has match _. Unknown argument parts remain unknown in matching; proven hidden matches may be made whole as above. Thus list.map(users, (u) { u.name }) can have known result List(String) when the checked callback has known result String. Thus in list.fold(xs, 0, (n, x) { … }), n has no factual known type; the initial value does not determine every accumulator value. The same holds for values read from a service or an invariant cell and values supplied by a later caller.

    Separately, keep a structural hint from matching these variables as usual and making their matches whole: every Int and String member in a covariant part takes all its values, Never there becomes _, and noncovariant parts become _. Hints propagate by the same structural operations as known types, but never justify selection, rule-12 factual narrowing, or W0503. Rule 13 may use a hint to find a key’s layout and construct its inference bound; the receiver must fit that bound, and the inferred result comes from the bound. A projected hint is not a projected fact. This permits list.fold(xs, (n = 0), (acc, x) { (n = acc.n + x) }): using acc.n constrains every accumulator value to the record layout. It does not permit selecting a branch from the initial accumulator’s constructor alone.

  • The value of a binding whose pattern has x : T at its top has T. The body of a function with a written -> part has that type.

  • The last expression of a block has the expected type of the block, and every branch body of a match has the expected type of the match. A part of data or of a list has the matching part of the expected type, when that type has one member, data of that shape or a list.

  • When a function expression has an expected type with one member, a function type whose parameter type has a member of the function’s shape, every item of its parameter group with no type written at its top is fitted to the matching part of that member, as for names in patterns below. This only gives known types. So list.map(users, (u) { u.name }) is correct when users has a known type.

  • In a match s |> (p) { e } whose chain has one branch with no guard and no alternatives, when p has x : T at its top, s has the expected type T, as the value of a binding x : T = s does.

  • A name with a selection table used other than as a callee, at a place whose expected type has exactly one member, a function type with parameter part P, has the type of the branches selected for each member of P whose shape it has (§6.12). So in list.map([1, 2], show), the expected type of show is (Int) -> B, and the result is selected by it.

• v.f and v.k have the part type of rule 13, when it has no type variable that is not put in.
• A block has the known type of its last expression.
• In a match e |> C, every parameter pattern of the one-position group of C is a pattern fitted to a value with the known type of e (below), also when the group has one branch and no guard. So with opt : Option(User), opt |> (Some(u)) { u.name } is correct, as Some(u) = opt followed by u.name is.
• Names in patterns: when a pattern q is fitted to a value with a known type B: a catch-all gets B, less the members that rule 12 takes out. If q is not a catch-all, take the one member of B with the type constructor of Q; for a literal pattern with the value v, only that value, if the member has it: B & v, with v the literal type of the value (not B & Q, because where a pattern is fitted Q is the whole Int or String); if there is not exactly one, the names of q get no known type. The parts of q then have the known part types of that member, with its type arguments put in; the binder r of a string prefix, suffix, or combined pattern has the known type String, all its values, because the known type of the whole value says nothing about its remaining part. A name part of a conjunction gets that member. The name x of x : T gets T, whatever the value.

So (u) { u.name } needs a type, (u : User) { u.name }, but with opt : Option(User), opt |> (Some(u)) { u.name } | (None) { "" } is correct.