Module Sarek_scheme

Type Schemes

type scheme = {
  1. quantified : int list;
    (*

    IDs of generalized (forall-bound) type variables

    *)
  2. body : Sarek_types.typ;
    (*

    The type body with those variables

    *)
}

A type scheme represents a polymorphic type with quantified type variables. For example, the identity function has scheme: forall a. a -> a

val mono : Sarek_types.typ -> scheme

Create a monomorphic scheme (no quantified variables)

Free Type Variables

val free_tvars : Sarek_types.typ -> int list

Collect all free (unbound) type variable IDs in a type

val unique : int list -> int list

Remove duplicates from a list

Generalization

val copy_for_scheme : int -> Sarek_types.typ -> Sarek_types.typ * int list

Deep copy a type, creating fresh type variables with NEW ids for those that will be quantified. This ensures the scheme's body is completely independent of unification on the original or instantiated types.

CONSTRAINT PROPAGATION. Sarek_types keeps two registries keyed by tvar ID — "this tvar came from a bare float literal" and "this tvar stood where a numeric type was required, so it may never become float16". Minting a fresh id silently DROPS both, which turns generalization into a hole in the type system: the body of let[@sarek.module] twice (x : 'a) : 'a = x +. x records the original x as numeric-required, but its generalized copy did not, so a call site could unify the fresh variable with a float16 element and get half arithmetic past the guard.

Confirmed by construction: that exact helper applied to a float16 vector load produced NO Sarek diagnostic, while the identical shape at float32 compiled cleanly — i.e. the two differed only in the guard that should have fired and did not. Both registries are therefore carried onto every fresh variable here and in instantiate.

val generalize : int -> Sarek_types.typ -> scheme

Generalize a type at a given level. Type variables at levels greater than the given level are quantified.

  • parameter level

    The current binding level (from the environment)

  • parameter t

    The type to generalize

  • returns

    A type scheme with free variables at higher levels quantified

Instantiation

val instantiate : scheme -> Sarek_types.typ

Instantiate a type scheme by replacing quantified variables with fresh ones.

Each fresh variable inherits the quantified variable's ID-keyed constraints (see copy_for_scheme); this is the second half of the propagation, and the one a CALL SITE depends on. Skipping it would let twice a_f16.(tid) unify the instance with float16 even though the helper's body required a numeric type.

  • parameter s

    The type scheme to instantiate

  • returns

    A fresh type with all quantified variables replaced

Pretty Printing

val pp_scheme : Stdlib.Format.formatter -> scheme -> unit
val scheme_to_string : scheme -> string

Scheme Utilities

val is_mono : scheme -> bool

Check if a scheme is monomorphic (no quantified variables)

val is_poly : scheme -> bool

Check if a scheme is polymorphic (has quantified variables)

val function_arity : scheme -> int option

Get the arity of a function scheme

val schemes_equivalent : scheme -> scheme -> bool

Check if two schemes are equivalent (up to alpha-renaming)