MIRR Type System Reference

Status: Active MEGA-1 Extended: Refinement types, linear types, effect types, clock domains, phantom tags — all wired into the pipeline via typecheck_extended(). Opt-in with PipelineConfig::extended_typecheck. Module: src/typeck/mod.rs Campaigns: TYPE-001 through TYPE-005, FOUNDATION-001, MEGA-1, MEGA-1b Error codes: E601–E625

The MIRR type checker runs after semantic validation and before simplification. It enforces signedness consistency across all expressions: guard conditions, reflex assignments, and property formulas.

Signal Types

MIRR has three categories of signal types:

Declared in MIRR source:

module example {
    signal sensor: in u16;
    signal offset: in i16;
    signal alarm:  out bool;
    signal error_code: out u8;
}

Type Rules

T1: Assignment Compatibility

An assignment target = expr requires the expression type to be compatible with the target signal type. Compatible means:

• Exact match — always accepted
• Bool <-> Unsigned(1) — bidirectional promotion
• Unsigned(N) -> Unsigned(M) where N <= M — safe zero-extension
• Signed(N) -> Signed(M) where N <= M — safe sign-extension
• Signed <-> Unsigned — always rejected (E602)

T2: Arithmetic Operators (+, -, *)

• Both operands must be numeric (not Bool — E603)
• Both operands must be the same category (both signed or both unsigned — E608)
• Result width = max(left_width, right_width), preserving signedness

T3: Shift Operators (<<, >>)

• Both operands must be numeric (not Bool — E603)
• Both must be same category (signed/unsigned — E608)
• Result width = left operand width, preserving signedness

T4: Logical Operators (&&, ||)

• Both operands must be Bool (E604)
• Result type: Bool

T5: XOR Operator (^)

• Both operands must match types (E607)
• Bool <-> Unsigned(1) allowed
• Result type: left operand type

T6: Ordering Comparisons (<, <=, >, >=)

• Cannot compare Bool values (E605)
• Cannot compare signed vs unsigned (E605)
• Result type: Bool

T7: Equality Comparisons (==, !=)

• Both operands must be same category: both Bool, both Unsigned, or both Signed (E606)
• Result type: Bool

T8: Logical Not (!)

• Works on Bool, Unsigned, and Signed
• Result type: same as operand

T9: Arithmetic Negation (-expr)

• Unsigned(N) -> Signed(N+1) — two's complement requires one extra bit
• Signed(N) -> Signed(N) — preserves width
• Bool -> error (E609) — use ! for logical negation

T10: Previous-tick (prev(signal, delay))

• Preserves the declared type of the signal
• Delay is a compile-time constant (not type-checked)

T11: Guard Conditions

• Guard conditions must evaluate to Bool (E601)

T12: Literal Inference

• Boolean literals (true, false) -> Bool
• Integer literals -> Unsigned(min_bits) where min_bits is the minimum bit width needed to represent the value

The Cross-Category Rule

The fundamental invariant: signed and unsigned types never mix in the same expression. This eliminates an entire class of bugs common in C/C++ where implicit signed-to-unsigned conversion causes unexpected behavior.

// REJECTED — E608: cannot mix signed and unsigned
signal a: in u16;
signal b: in i16;
reflex always_on {
    // error_val = a + b;  // E608
}

// CORRECT — explicit same-category usage
signal a: in i16;
signal b: in i16;
reflex always_on {
    result = a + b;  // OK: both signed
}

TypeMap Output

The type checker returns a TypeMap (HashMap<*const Expr, SignalType>) that maps every visited expression node (by pointer identity) to its inferred type. Downstream passes (width inference, R-SPU emission) can query this map to determine signedness without re-walking expression trees.

use mirr::{run_pipeline, PipelineConfig};

let config = PipelineConfig {
    typecheck: true,
    // ... other fields
};
let result = run_pipeline(source, config)?;
let type_map = &result.type_map;  // Option<TypeMap>

The TypeMap is now wired into the compilation pipeline and will be consumed by width inference in a future update (proposal 025, Section F). An extended type map (ExtendedTypeMap) is defined in src/typeck/extended.rs for MEGA-1 programs.

Error Codes

Pipeline Integration

Type checking is optional and controlled by PipelineConfig::typecheck:

let config = PipelineConfig {
    typecheck: true,   // Enable type checking (default: true)
    // ...
};

When enabled, the type checker runs between semantic validation (Step 4) and simplification (Step 6) in the pipeline. If disabled, downstream passes still function correctly but without signedness enforcement.

MEGA-1 Type Annotations (Phase 7c -- Complete)

Status: Complete (all sections of proposals 025 + 027 delivered). Extended type checker wired into pipeline. Module: src/typeck/extended.rs (2138 lines) Error codes: E610--E625

MIRR's type system is being extended with compile-time annotations that encode hardware constraints directly in the type language. All annotations are opt-in -- existing programs remain valid. Annotations generate zero additional hardware; they are checked at compile time only.

Type Annotation Syntax

Signal declarations now support optional qualifier and constraint syntax:

signal sensor: in linear u16 where 0..1023 @clk_fast #Sensor;

Grammar:

<kind> [linear] [stateful|pure] <base_type> [where <refinement>] [@<clock>] [#<Tag>]

Linearity

linear signals must be consumed exactly once per clock cycle. This prevents the hardware anti-pattern of multiple drivers on a single net.

Effect Qualification

• stateful -- signal carries state across clock cycles (implies register)
• pure -- signal is purely combinational (no register inference)

Refinement Types

where clauses constrain signal value ranges at compile time:

• where 0..1023 -- inclusive range
• where value < 1024 -- predicate form

Clock Domain Qualifiers

@domain annotations tag signals with their clock domain. Cross-domain assignments without explicit synchronizers produce E618.

Phantom Tags

#Tag annotations add zero-cost provenance tracking. Mismatched phantom tags in assignments produce E620.

Extended Error Codes (E610--E625)

See Also

• Error Codes — Full error code catalogue (E6xx section)
• Tutorial — Lesson 8: Reading compiler output
• R-SPU ISA Spec — How types map to R-SPU registers
• Roadmap — TYPE campaigns overview