Inference Proof Sketch

The checker is not a formal proof assistant, but its structure follows the standard progress path for a typed language: every accepted expression receives a type, and every emitted call has a statically established arity and value representation. The proof obligation is limited by OJaml's uniform WebAssembly ABI: values travel through i32 parameters and results, with compiler-side int/float specialization where polymorphic functions need different concrete representations at different call sites.

\operatorname{unify}(\tau_1,\tau_2) \Rightarrow \operatorname{prune}(\tau_1)=\operatorname{prune}(\tau_2)

Unification preservation. After a successful unify, both sides resolve to a shared representative type.

Soundness here means the compiler never emits direct WebAssembly for a program with unresolved names, inconsistent branches, impossible call arity, or collection access whose key/value relationship is statically contradictory. Runtime helpers also trap invalid collection access such as out-of-bounds array reads, empty-list head/tail, and missing map keys. This is still not a full safety proof for every pointer operation: garbage collection and recoverable language-level exceptions are outside the current core.

\Gamma \vdash m : (K,V)\;map \land \Gamma \vdash k : K \Rightarrow \Gamma \vdash \operatorname{Map.get}\;m\;k : V

Map key lemma. Map reads are type-preserving because Map.get unifies its key parameter with the map key type.

\Gamma \vdash s : T\;set \land \Gamma \vdash v : T \Rightarrow \Gamma \vdash \operatorname{Set.has}\;s\;v : bool

Set membership lemma. Set membership is type-preserving because Set.has unifies the queried value with the set element type.

The reconstruction hinge is preservation under unification: once two types are unified, all later pruned references see the same representative. Local hover information stays accurate because a binding span and every later use point at type graph nodes that resolve through the same pruning path.

\operatorname{fresh}(\forall \alpha.\tau) = \tau[\alpha \mapsto \beta_{new}]

No cross-call pollution. Fresh variables ensure one call to a polymorphic collection helper does not constrain another independent call.

Base cases assign primitive types to literals.
Inductive expression cases add local constraints and unify recursively checked subexpressions.
Function cases introduce fresh parameter variables and infer the body under the extended environment.
Match cases unify every pattern with the scrutinee and every arm body with a shared result.

Continue exploring