Typecheck

Pair with experimental.desc-interp.trampoline.run:

let tc = typecheck.atType_collecting fx.tc.kernel.failure.DiagError;
in run tc.eff tc.resp H.unit
     { inherit (tc) handler dispatch; }
     program initialState

A program is a bind chain of tc.report reason path carrier passed ops; reason is the closed five-token enum, path the internalized structural blame site (a Path = List Position over the value-side alphabet Field/Elem/Tag/Tuple), carrier the opaque host residue, passed the host-precomputed decision. Every op resumes with tt; the handler folds the decision into its state and never inspects the carrier.

ByReason

Per-reason counter tuple in constructor order (a five-Nat Σ-chain).

EffTypeCheck

EffTypeCheck : Π(R:U₀). U₀ — one constructor report(reason:Reason, path:Path, carrier:R, passed:Bool).

EffTypeCheckTy

Π-type of the op-identity family: Π(R:U₀). U₀.

Path

Path = List Position — the structural blame site carried by report, mirroring the producer's typeCheck path.

Position

Value-side descent position: Field name / Elem idx / Tag name / Tuple idx. The internalized core of fx.diag.positions for value-validation paths (name a strEq-comparable carrier, idx a Nat); rendered segment text stays host-side.

Reason

Closed five-token diagnostic enum (shapeMismatch/missingField/extraField/predicateFailed/deferredPi).

Resp

Response family: every report op resumes with Unit (the decision rides in the op, not the resume).

atType_collecting

atType_collecting R — monomorphises the collecting handler and ships { eff; resp; handler; dispatch; report; evalOp; handlerShortcut }. The shortcut rebuilds the resume residual directly (certified by typecheck-shortcut-laws.nix).

atType_firstN

atType_firstN R — monomorphised first-N bridge record.

atType_logging

atType_logging R — monomorphised logging bridge record.

atType_pretty

atType_pretty R — monomorphised pretty bridge record.

atType_strict

atType_strict R — monomorphises the strict handler and ships { eff; resp; handler; dispatch; report; evalOp; handlerShortcut } with a conditional-throw dispatch (resume on pass, throw on fail); the shortcut emits the Sum directly (Resume/Abort).

atType_summarize

atType_summarize R — monomorphised summarize bridge record.

atType_summarizeAssoc

atType_summarizeAssoc R — monomorphised summarize-assoc bridge record (assoc-list byReason).

bumpReason

bumpReason r b — increment the counter for reason r via the Reason eliminator (no string comparison).

handle_collecting

Collecting handler: a fail conses the residue, a pass keeps the list. Returns Σ (List R) Unit.

handle_firstN

First-N handler: an O(1) down-counter records failures until it reaches zero, then drops. Returns Σ (Σ (List R) Nat) Unit.

handle_logging

Logging handler: every decision is recorded as (passed, residue). Returns Σ (List (Σ Bool R)) Unit.

handle_pretty

Pretty handler: conses the host-rendered failure line (carried opaquely) on a fail. Same shape as collecting.

handle_strict

Strict handler: a pass resumes (left summand), a fail surrenders the residue (right summand). Returns Sum (Σ Unit Unit) (Σ R Unit); the right summand drives a throw.

handle_summarize

Summarize handler: groups failures by the reason enum, tracking (passed, failed) totals. Returns Σ (Σ ByReason (Σ Nat Nat)) Unit.

handle_summarizeAssoc

Summarize-assoc handler: groups failures into a List (Σ String Nat) byReason assoc list via insertOrIncrement (a listElim+strEq fold), tracking (passed, failed) totals. Returns Σ (Σ (List (Σ String Nat)) (Σ Nat Nat)) Unit. The production-faithful byReason attrset shape, alongside the O(1) closed-enum variant.

insertOrIncrement

insertOrIncrement key assoc — a listElim fold over a List (Σ String Nat) byReason assoc list: a strEq key match bumps the entry's count in place, otherwise a new (key, 1) is appended.

reasonName

reasonName r — render the reason enum to its production byReason key token (shape-mismatch/missing-field/extra-field/predicate-failed/deferred-pi) via the Reason eliminator.