7.2 Type Checking and Conversion: Ensuring Every Operation Meets Language Rules

In some languages, "hello" * 3 is legal and denotes string repetition; in others, it's a type error. Semantic analysis can't rely on a single "universal operator table"; it implements the specific type rules defined for a given language.

This lesson's objectives

• Distinguish type inference, type checking, and type synthesis;
• Establish constraints for operators, calls, and returns;
• Distinguish implicit conversion, explicit conversion, and representation conversion;
• Use error types to suppress cascading errors.

1. Type Environments and Judgments

Type rules are often written as judgments:

$$\mathrm{\Gamma }⊢e:T,$$

The expression $e$ has type $T$ in the environment $\mathrm{\Gamma }$.

For example, integer addition:

$$\frac{\mathrm{\Gamma }⊢e_1:Int\mathrm{\Gamma }⊢e_2:Int}{\mathrm{\Gamma }⊢e_1+e_2:Int}.$$

An environment usually maps resolved symbol identities to types. It may also include generic parameters, lifetimes, mutability, effects, and the current function's return type.

2. Synthesis and Checking Run in Two Directions

• Synthesis synth(expr) -> Type: Infer types from the expression itself;
• Check check(expr, expected): Given an expected type, verify that the expression satisfies it.

Literal 42 can be inferred as the default integer type, or checked directly as u8 at a location that expects u8, including range validation. Lambda parameters often require a context-provided expected function type if not explicitly annotated.

Bidirectional type checking balances "local inference" and "predictable errors," without requiring type inference at every node in a context-free way.

3. Binary Operators Need Resolution Rules

On left + right:

1. Synthesize or check both operand types;
2. Look up built-in rules or overloaded candidates;
3. Find the required conversion;
4. Choose the single best candidate;
5. Insert explicit coercion nodes in AST/HIR;
6. Return result type.

int + int       → int
float + float   → float
int + float → Whether it converts to float is specified by the language.
string + string → Whether concatenation occurs depends on the language.
pointer + int → Whether allowed and the stride semantics, is specified by the language

The comparison result doesn't have to be int; many languages return bool. Whether == accepts arbitrary values of the same type also depends on whether the type defines equality, floating-point NaN semantics, and user-defined overloads.

4. Implicit Conversions Need Direction and Ranking

A conversion graph may contain:

• widening: a narrower integer type to a wider one;
• numeric promotion: integer to floating point;
• subtype coercion: coercion from subtype to supertype;
• dereferencing, borrowing, or boxing;
• User-defined conversion.

Compare viable overloads using the language’s conversion ranks, applicability phases, and specificity rules. These need not reduce to one numeric score; if there is no unique best candidate, report ambiguity. The ordering must not depend on hash table iteration order, otherwise the same program might select different candidates across different runs.

Narrowing or sign-changing conversions may require explicit syntax, but potential precision loss does not always make a conversion explicit: some languages implicitly convert integers to floating point even when large integers are not exactly representable.

Numeric conversion also differs from reinterpreting a representation. Converting IEEE 754 binary32 1.0 to an integer gives 1; reinterpreting those same 32 bits as an unsigned integer through a language-supported operation gives 0x3f800000, or 1065353216. These are different operations.

5. Function calls establish a set of constraints

For f(a,b), check at least:

• Is the called object callable;
• Argument count and positional/named argument rules;
• Can each actual parameter be converted to the corresponding formal parameter type;
• Can generic parameters satisfy constraints;
• How does the return type enter the outer expectation;
• How variable-length and default parameters are expanded.

Overload resolution first gathers all candidate functions with the same name, then filters out the invalid ones, and finally selects the single best match. Failure diagnostics should explain why the closest candidates don't match, rather than simply stating "no function found." When there are many candidates, output should be limited and results should be sorted.

6. Control Flow Impact on Types and Initialization

let x;
if cond { x = 1; }
print(x);

Local node-type checks cannot establish that x is initialized before use. Definite-assignment facts must flow through control flow, either over an explicit CFG or recursively through a structured AST. Facts required on every reachable predecessor are typically intersected at a join.

Similarly:

• Do all paths return;
• Is type narrowing valid within the branch?
• Has nullability been checked?
• Is the variable still used after being moved?

These rules often work alongside a type system but may be implemented as independent data flow passes.

7. Error Type Prevents Cascading

unknown + 1 * true

If unknown has been reported as undeclared, declare it as type ErrorType. An operation propagates ErrorType without adding a derived addition mismatch. However, 1 * true is an independent error and still needs checking: do not skip the right subtree just because the left has ErrorType. This C integration fragment relies on host definitions for TypeId, AST nodes, operator resolution, and diagnostics:

TypeId check_binary(BinaryExpr *expr) {
    TypeId left = check_expr(expr->left);
    TypeId right = check_expr(expr->right);
    if (is_error(left) || is_error(right)) return TYPE_ERROR;

    OperatorResult result = resolve_operator(expr->op, left, right);
    if (!result.ok) {
        report_operator_mismatch(expr->span, expr->op, left, right);
        return TYPE_ERROR;
    }
    insert_coercions(expr, result);
    return result.type;
}

ErrorType should be avoided in code generation; if errors occur on the frontend, generation can be halted, but in IDE mode, a partial typed tree should be retained for feature degradation.

8. Type equivalence also needs to be defined

When are two types equal?

• Nominal type: equal only if identity is the same;
• Structural types: compare members, mutability, and other properties required by the language;
• Type alias: transparent or creating a new type;
• Generic instance: same parameters and same constructor;
• Recursive types: must avoid infinite expansion.

Printing type as strings for comparison is both slow and unreliable. Compilers typically intern types, use stable TypeId values, and provide normalized and equivalent type comparisons.

Common Misconceptions

• Type checking is simply comparing whether the types on the left and right sides are the same: conversions, overloads, subtypes, and expected types all play a role.
• Implicit conversion is just inserting one machine instruction: it starts as language semantics, where some conversions need no runtime instruction, while others might allocate memory.
• Local recursion can perform all static checks: Path-sensitive properties require control-flow fact propagation.
• Return any default type after a type error: it can cause cascading errors or incorrect code generation.

Practice

1. Define the complete type matrix of + for a small language and explain each implicit conversion.
2. Design two overloads so that a single argument can be implicitly converted to either, and establish an unambiguous ordering rule.
3. Construct a control flow graph for uninitialized variables and write the data flow state.
4. Implement ErrorType propagation testing to ensure the root cause is reported only once.

Summary

Type checking is an executable version of a language's rules: it establishes constraints in the environment, resolves overloads, inserts conversions, and handles control-flow facts. Correctness comes from explicit rules, not from treating some language's intuition as universal truth.

The next lesson reduces the already-bound and typed tree to IR, explicitly representing basic blocks, control flow, and data dependencies.

References

• Java Language Specification: widening primitive conversions