Sarek_typesPrimitive types supported in GPU kernels (core language only). Numeric types like float32, float64, int64 are library-defined.
type registered_type = | IntOCaml int - alias for int32 on GPU
*)| Int6464-bit integer
*)| Float16IEEE binary16 half float. A storage type: f16 is deliberately NOT in is_numeric / is_float / float_literal_can_link, so f16 values cannot be added, compared, passed to math intrinsics, or written as bare literals.
The two conversions are the CORE PRIMITIVES float32_of_float16 and float16_of_float32 (registered in Sarek_core_primitives.all, category "conv_f16"). There is NO Float16 stdlib module and there cannot be one in slice 1: a %sarek_intrinsic stdlib type registration needs a ctype, and Ctypes has no half type. An earlier version of this comment named Float16.of_float32 / Float16.to_float32; those do not exist.
Rejection of f16 at an operator is enforced by Sarek_typer (check_numeric's TReg Float16 arm plus reject_float16 for the equality/boolean/bitwise families) and, for an operand type still unresolved at that point, by the "never float16" tvar registry below. Together that is what makes "store as binary16, compute in f32" a type-system guarantee rather than a convention.
| Float3232-bit float
*)| Float6464-bit float (double)
*)| Char8-bit character
*)| Custom of stringUser-registered types via @@sarek.type
Registered type name - for library-defined types like float32, float64, int64. These are not built-in but are registered by libraries via @@sarek.type.
type typ = | TPrim of prim_typePrimitive types (core language)
*)| TReg of registered_typeRegistered types (library-defined: float32, float64, int64, etc.)
*)| TVar of tvar Stdlib.refUnification variable
*)| TVec of typVector type (GPU array parameter)
*)| TArr of typ * memspaceLocal array with memory space
*)| TFun of typ list * typFunction type
*)| TRecord of string * (string * typ) listRecord type: name, fields
*)| TVariant of string * (string * typ option) listVariant type: name, constructors
*)| TTuple of typ listTuple type
*)Types
and tvar = | Unbound of int * intid, level for generalization
*)| Link of typResolved to this type
*)val fresh_tvar : ?level:int -> unit -> typCreate a fresh unbound type variable at given level
A bare float literal (e.g. 1.0) is typed as a fresh unification variable instead of being hard-typed float32, so it can unify with its context (e.g. a float64 binding). Two invariants make this safe:
float32/float64) — it must never unify with an integer or other concrete type (enforced in unify via float_literal_can_link);float32 (see default_float_literals), so float32 stays the GPGPU default.The registry is process-global but scoped per kernel: it is cleared at the start of each infer_kernel and whenever the tvar counter is reset.
IDs are monotonic within a kernel so no stale collision is possible — and that holds only because every tvar id comes from fresh_tvar_id. It was briefly untrue: one site in Sarek_typer drew a tvar id from the TERM variable counter (backlog-183), which made this id space non-injective and therefore made a lookup in this very registry able to hit a tvar that never came from a float literal — rejecting a legal program. The single-allocator premise this sentence rests on is now enforced mechanically by scripts/check-tvar-id-allocator.sh, because a premise stated only here is exactly what failed.
IDs of tvars that originate from bare float literals.
val float_literal_tvars : typ list Stdlib.refThe float-literal tvars in creation order, used for defaulting.
"must never be float16" tvar registry
f16 is a storage-only type. Sarek_typer.check_numeric and friends can only reject it when the operand type is already resolved; their TVar _ -> Ok () arm let an unresolved operand through, and nothing re-checked it once unification later bound it (#57 slice 1 review, MF4b). Registering the tvar here turns "numeric was required at this operator" into a standing constraint that unify enforces, so a late binding to float16 fails instead of silently producing __half arithmetic.
Deliberately NOT reusing the float-literal registry: that one also forbids integers, and Add is legal on int32. This registry forbids exactly float16. Same per-kernel lifetime as the float-literal registry — clear_float_literals clears it too, so every existing reset point already covers it.
val register_float_literal : typ -> unitRecord a fresh float-literal tvar so it can be guarded and later defaulted. (See the L17b registry section above.)
val register_numeric_required : typ -> unitRecord that a tvar stood where a numeric type was required, so it can never later link to float16. See the registry section above.
val occurs : int -> typ -> boolCheck if a type variable occurs in a type (for occurs check)
type unify_error = | Cannot_unify of typ * typ| Occurs_check of int * typ| Float16_where_numeric_requiredA tvar that stood where a numeric type was required was about to be bound to float16. Distinguished from Cannot_unify so the typer can report the actionable f16 message instead of leaking the variable ("Cannot unify types: 't30 and float16").
Unification error
val float_literal_can_link : typ -> boolA float-literal tvar may only link to a floating-point type or to another type variable (which will itself carry the constraint). Linking it to any other concrete type (int32, int64, bool, records, ...) is a type error — a bare float literal is never an integer.
val is_float16_repr : typ -> boolIs t (after repr) the f16 storage type?
val unify : typ -> typ -> (unit, unify_error) Stdlib.resultUnify two types
val pp_prim : Stdlib.Format.formatter -> prim_type -> unitPretty printing
val pp_registered : Stdlib.Format.formatter -> registered_type -> unitval pp_memspace : Stdlib.Format.formatter -> memspace -> unitval pp_typ : Stdlib.Format.formatter -> typ -> unitval typ_to_string : typ -> stringHelper functions to construct common types.
val t_unit : typPrimitive type constructors
val t_bool : typval t_int32 : typval t_float32 : typRegistered numeric types (library-defined).
These are not built-in primitives but use TReg for type-checking. They must be registered via @@sarek.type attributes.
val t_float64 : typval t_float16 : typHalf float. Intentionally absent from is_numeric / is_float and from float_literal_can_link: see Float16.
val t_int64 : typval t_int : typval t_char : typDefault every still-unconstrained float-literal tvar to float32. Called once after kernel inference: literal-origin tvars that context never resolved (e.g. an unconstrained let z = 1.0) become float32, preserving the GPGPU default. Already-resolved literals (unified to float64 by context, or to float32) are left untouched. Non-literal tvars are never in the registry, so the polymorphic-kernel-parameter guard in Sarek_lower_ir.elttype_of_typ keeps firing for them.
Boolean-returning functions to check type properties.
For Result-returning validators with error messages, see Sarek_typer:
check_numeric: Validates numeric types with location-aware errorscheck_integer: Validates integer types with location-aware errorscheck_boolean: Validates boolean types with location-aware errorsval is_numeric : typ -> boolCheck if type is numeric (includes both core int32 and registered float/int types).
val is_integer : typ -> boolCheck if type is integer (core int32 or registered int64)
val is_float : typ -> boolCheck if type is floating point (registered types)
val is_boolean : typ -> boolCheck if type is boolean
val is_uncomparable_operand_typ : typ -> boolbacklog-194. Is t a type whose values cannot be compared with = / <> in a kernel?
Per member, each measured on this tree rather than reasoned about:
TTuple — a primitive tuple lowers to the synthesized _tup_* record and emitted (_tup_float32_float32){...} == (...){...}; a non-primitive one emitted a bare brace list. clang -x cl rejects both ("invalid operands to binary expression", "expected ';' after expression").TRecord, TVariant — emitted a == b on a struct; same rejection.TFun — let f x = ... in let g x = ... in if f = g compiled, and emitted if ((f == g)) naming two identifiers that appear NOWHERE in the emitted source: the helpers are inlined, not declared. clang -x cl fails with "use of undeclared identifier 'f'". Unlike the three above there is no backend on which this means anything, so refusing it removes nothing.TVec and TArr are deliberately NOT here, and that boundary is measured in BOTH directions. if src = dst on two vector parameters emits (src == dst), which clang -x cl accepts (exit 0) and glslangValidator -V accepts (exit 0) — refusing it would remove something that works. It is not portable, though: the same kernel through the WGSL emitter compares two array<f32> storage bindings and naga rejects it ("Incompatible operands: Equal(Array ..., _)"). That is a real defect; it predates backlog-194, it is a WGSL-emitter question rather than a frontend one — four backends emit legal code for this construct — and it is recorded in kb/sarek/ppx/lowering.md rather than silently folded in here. Widening this set to TVec would refuse four working backends to fix one.
This is the single definition. Both refusal sites call it — the typer's Sarek_typer.reject_aggregate_equality at inference time and the post-monomorphisation backstop in Sarek_lower_ir — because two hand-rolled copies of one constructor list is exactly how the two gates would come to disagree about what they refuse.
val is_tvar : typ -> boolCheck if type is an unbound type variable
Functions to convert between different type representations.
val type_of_type_expr : Sarek_ast.type_expr -> typConvert AST type expression to type (with fresh type variables). Core types (unit, bool, int32) are handled directly. Other types (float32, float64, int64, etc.) are looked up in the type registry.
val memspace_of_ast : Sarek_ast.memspace -> memspaceConvert memspace from AST to types