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

The same multiplication operator may represent numeric multiplication, string repetition, or be invalid depending on the language; the semantic checker must adhere to the rules of the current language.

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 Environment and Pattern Matching

Type rules are often written as judgments:

$$ \Gamma\vdash e:T, $$

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

For example, integer addition:

$$ \frac{\Gamma\vdash e_1:Int\qquad\Gamma\vdash e_2:Int} {\Gamma\vdash e_1+e_2:Int}. $$

An environment isn't just a mapping from names to types, it may also include generic parameters, lifetimes, mutability, effects, and the current function's return type.

2. Integration and Verification Are Two Different Directions

• Comprehensive 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.

Type checking works in balance between "local inference" and "predictable errors," without requiring type inference at every node in a context-free way.

3. Binary operators require parsing rules

On left + right:

1. Get or check left-right type;
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-overridden behavior.

Implicit conversions must have direction and cost

A converted image may contain:

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

If two overloads are available, they should be ordered by conversion cost and specificity. The ordering must not depend on hash table iteration order, otherwise the same program might select different candidates across different runs.

Narrowing conversions that might lose precision or alter the sign usually require explicit specification. Even when grammatically allowed, compilers can provide configurable warnings.

5. Function calls establish a set of constraints

Call f(a,b) to at least verify:

• Is the called object callable;
• Rules for positional and named parameters;
• 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);

Proving initialization of x on all paths cannot be achieved with mere AST-local recursion; definite assignment analysis on a control flow graph is required.

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. When an operation encounters ErrorType, it returns ErrorType instead of reporting derived errors such as "cannot add to int".

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;
• Structure type: The composition structure only needs to be the same;
• 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 happen at runtime without instructions, while others might allocate memory.
• Local recursion can perform all static checks: Path-sensitive properties require CFG data flow.
• Return any default type after a type error: it can cause cascading errors or incorrect error 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 transformations, 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 finalized tree to IR, explicitly representing basic blocks, control flow, and data dependencies.