ch:gradual-typing: ch:gradual-typing

Problem, result, and invariant. Implement the finite source elaborator and ground-cast evaluator used by the chapter’s blame examples. The result is the five-case report in appendix E. The invariant is that every accepted source application produces typed target casts with two distinct application-derived labels.

Representation. Use nominal datatypes for gradual types, source and target terms, source positions, blame faces, frames, states, and observations. A refocused machine with function, argument, and cast frames represents the printed evaluation contexts without rebuilding whole target terms after each step.

First complete version. Write inferElaborate as a syntax walk that performs function matching and consistency tests, then inserts both casts of I-App. Implement capture-avoiding beta substitution. In machineStep, add beta, identity, grounding, expansion, projection, mismatch, and one-frame blame propagation before adding higher-order wrappers.

Remaining cases. For wrapper application, complement the label on the domain cast and retain the provider label on the result cast. Run the successful and failing ground projections, both higher-order blame directions, and the precise/less-precise pair only from closed source terms elaborated by the implementation. Treat fuel exhaustion as rejection, not as divergence evidence.

A failing version. Preserve the provider face rather than complementing it in an arrow domain. The program remains type-correct, but the positive higher-order case blames the protected provider. Swapping unequal-tag rejection for payload exposure and reusing the function label for the argument are independent controls.

Acceptance test. Run the four gates in appendix E. Require five exact PASS lines, the frozen summary, and [] from audit. Reproduce the domain-polarity, ground-tag, and label-allocation mutations; each must fail the output oracle and match the recorded transcript.

Mathematical boundary. The corpus checks a finite source-to-target insertion tree and refocused machine traces. It proves neither preservation, progress, blame safety, simulation, either gradual guarantee, nor the separate dependent- interoperability theorem.