Module Sarek_typer

Type Unification with Error Reporting

val unify_or_error : Sarek_types.typ -> Sarek_types.typ -> Sarek_ast.loc -> (unit, Sarek_error.error list) Stdlib.result

Unify two types and convert unification errors to typed errors with location

Reserved-Prefix Policy

User-written identifiers may not begin with the sarek_ prefix, which the code generator reserves for its own emitted device-code names (param length aliases, the sarek_smod / sarek_copysign helpers, and any future generated helper). Enforcing this once at elaboration time closes the user/generated collision class structurally; the collision-safe name computation in the backends (PR #255 / #256) is kept as defense-in-depth.

This is the single validation function; every user-binder introduction path in the typer calls it (or check_reserved_prefix_all for lists). It must only fire on user-written binders — never on names the generator itself synthesizes (those are produced downstream, in lowering / codegen).

val check_reserved_prefix : string -> Sarek_ast.loc -> unit Sarek_error.result

Reject a single user-written binder whose name is reserved.

val check_reserved_prefix_all : string list -> Sarek_ast.loc -> unit Sarek_error.result

Reject any reserved name in a list of user-written binders sharing loc (e.g. all record fields or variant constructors of one declaration).

Type Validators

Result-returning validators for type checking with error messages.

These functions validate types and return detailed error messages on failure. For simple boolean checks without errors, use predicates from Sarek_types:

val check_numeric : ?what:string -> Sarek_types.typ -> Sarek_ast.loc -> (unit, Sarek_error.error list) Stdlib.result

Check that a type is numeric (int32, int64, float32, float64).

  • parameter t

    The type to check

  • parameter loc

    Source location for error reporting

  • returns

    Ok () if numeric, Error with type mismatch otherwise

See also: Sarek_types.is_numeric for bool predicate version.

val reject_float16 : what:string -> Sarek_types.typ -> Sarek_ast.loc -> (unit, Sarek_error.error list) Stdlib.result

Reject a float16 operand for an operator that is not numeric-checked (the equality and boolean/bitwise families). f16 is storage-only, so no operator may see it — Eq/Ne skipped check_numeric entirely, which is how a.(i) = b.(i) on a float16 vector compiled and emitted a[tid] == b[tid] on __half (#57 slice 1 review, MF4a).

val reject_aggregate_equality : what:string -> Sarek_types.typ -> Sarek_ast.loc -> (unit, Sarek_error.error list) Stdlib.result

backlog-194. Reject an AGGREGATE operand of = / <>. The comment that used to sit at the Eq | Ne arm said equality "is legal on bool, records and variants"; it was legal only in the sense that nothing stopped it. Measured on this tree, all three aggregate shapes reached codegen and every one produced source no device compiler accepts:

  • (a, (b, c)) = (a, (b, c)) — a non-primitive tuple, which lowered to Ir.ETuple and emitted a bare brace list {x, y} == {x, y} ("expected ';' after expression" from clang -x cl);
  • (a, b) = (a, b) — a primitive tuple, which lowers to the synthesized _tup_* record and emitted (_tup_float32_float32){...} == (...){...} ("invalid operands to binary expression");
  • r1 = r2 on a @@sarek.type record, which emitted a == b ("invalid operands to binary expression").

Only the C-family emitters print ==; the native backend emits OCaml = (Sarek_native_gen.ml:213), which is structural and answers correctly. So the construct was not uniformly broken — it was silently non-portable, the worse shape. Refused here rather than at the emitters, so the diagnostic names the operator and the type at the source location.

NARROWNESS, stated: an operand still unresolved (TVar) is NOT refused here — this runs at infer_binop time and nothing re-examines the operator after unification binds it. The backstop for that is the TEBinop (Eq | Ne, …) arm in Sarek_lower_ir, which runs after monomorphisation and covers every member of the set, record and variant included; test_poly_aggregate_eq pins it on a record reached through a polymorphic helper.

The set is Sarek_types.is_uncomparable_operand_typ and is NOT hand-rolled here: the backstop calls the same predicate, because two copies of one constructor list is how the two gates would come to disagree. It is deliberately narrower than "aggregate": a vector or local-array operand is a pointer on the device, src = dst emits (src == dst), and clang -x cl accepts it — refusing that would be a removal with no evidence behind it.

val check_integer : Sarek_types.typ -> Sarek_ast.loc -> (unit, Sarek_error.error list) Stdlib.result

Check that a type is integer (int32, int64, int).

  • parameter t

    The type to check

  • parameter loc

    Source location for error reporting

  • returns

    Ok () if integer, Error with type mismatch otherwise

See also: Sarek_types.is_integer for bool predicate version.

val check_boolean : Sarek_types.typ -> Sarek_ast.loc -> (unit, Sarek_error.error list) Stdlib.result

Check that a type is boolean.

  • parameter t

    The type to check

  • parameter loc

    Source location for error reporting

  • returns

    Ok () if boolean, Error with type mismatch otherwise

See also: Sarek_types.is_boolean for bool predicate version.

module TvarCtx : sig ... end

Type variable context for tracking named type variables like 'a, 'b

type tvar_ctx = {
  1. tvars : Sarek_types.typ TvarCtx.t Stdlib.ref;
  2. level : int;
    (*

    Level at which to create new type variables

    *)
}
val fresh_tvar_ctx : ?level:int -> unit -> tvar_ctx

Create a fresh type variable context at a given level

val type_of_type_expr_ctx : Sarek_env.t -> tvar_ctx -> Sarek_ast.type_expr -> Sarek_types.typ

Convert a parsed type expression using the current typing environment and a type variable context for polymorphic type variables

val type_of_type_expr_env : Sarek_env.t -> Sarek_ast.type_expr -> Sarek_types.typ

Convert a parsed type expression using the current typing environment. Creates fresh type variables for each TEVar - use type_of_type_expr_ctx when type variable names need to be preserved across multiple types.

val binop_name : Sarek_ast.binop -> string

Human-readable operator name for diagnostics. Defined in Sarek_error (backlog-194) because the lowering's aggregate-equality backstop renders the same operator into the same sentence; a second match over binop there was two independent renderings of one name, and nothing compared them.

Infer type of a binary operation

val infer_unop : Sarek_ast.unop -> Sarek_types.typ -> Sarek_ast.loc -> (Sarek_types.typ, Sarek_error.error list) Stdlib.result

Infer type of a unary operation

Type Inference Helpers

These helpers partition the main infer function by expression category.

Infer type of literal expressions (unit, bool, int, float constants).

Infer type of binary and unary operations (arithmetic, logical, bitwise).

Infer type of memory access operations (vectors, arrays, record fields). Handles field resolution for both known and external record types.

Infer type of control flow expressions (if, for, while, sequence). Ensures loop bounds are int32 and conditions are boolean.

val infer_data_structure : infer: (Sarek_env.t -> Sarek_ast.expr -> (Sarek_typed_ast.texpr * Sarek_env.t, Sarek_error.error list) Stdlib.result) -> infer_record_fields: (Sarek_env.t -> (string * Sarek_ast.expr) list -> ((string * Sarek_typed_ast.texpr) list * Sarek_env.t, Sarek_error.error list) Stdlib.result) -> infer_list: (Sarek_env.t -> Sarek_ast.expr list -> (Sarek_typed_ast.texpr list * Sarek_env.t, Sarek_error.error list) Stdlib.result) -> Sarek_env.t -> Sarek_ast.loc -> Sarek_ast.expr_desc -> (Sarek_typed_ast.texpr * Sarek_env.t) Sarek_error.result

Infer type of data structures (records, variants, tuples, arrays). Uses mutual recursion helpers for complex nested structures.

Infer type of special expressions (global refs, native blocks, pragmas, type annotations, open). These handle meta-level constructs and environment manipulation.

Infer type of let bindings (assign, let, let mut, let rec). Handles mutability constraints and recursive binding generalization.

Main type inference function

val infer_list : Sarek_env.t -> Sarek_ast.expr list -> (Sarek_typed_ast.texpr list * Sarek_env.t, Sarek_error.error list) Stdlib.result
val unify_args : Sarek_types.typ list -> Sarek_typed_ast.texpr list -> Sarek_ast.loc -> (unit, Sarek_error.error list) Stdlib.result
val infer_record_fields : Sarek_env.t -> (string * Sarek_ast.expr) list -> ((string * Sarek_typed_ast.texpr) list * Sarek_env.t, Sarek_error.error list) Stdlib.result
val infer_patterns : Sarek_env.t -> Sarek_types.typ list -> Sarek_ast.pattern list -> (Sarek_typed_ast.tpattern list * Sarek_env.t, Sarek_error.error list) Stdlib.result
val is_intrinsic_fun : Sarek_env.StringMap.key -> Sarek_env.t -> bool

Check if a name is an intrinsic function in the environment

Type a complete kernel