Positions

Shared diagnostic alphabet. Pure data.

A Position names the blame location in a structural descent through a Desc or through raw MLTT structure (Π / Σ / Ann / μ / App). The alphabet is description-centric: names such as DArgSort, DPlusL, and PiDom identify sub-positions by their meaning in the structure, not by the code path that happens to visit them.

Each Position carries four fields:

• tag : variant discriminator (used by hint-key lookup);
• segment : short rendered path label (e.g. "arg.S", "Π.dom");
• intent : semantic role description, rendered by the pretty printer as a "what was expected at this position" gloss alongside the segment;
• rule : optional descent-rule annotation; null on every constant. withRule produces a decorated variant and bindPR populates it at the emission site.

intent and rule are opaque to the hint resolver: keys are built from tag only, so decorating Positions does not affect lookup.

Two kinds of consumer:

• A kernel enrichment layer that wraps rule delegations, emitting a child error tagged with the Position of the sub-call that failed.
• A value-level validator (record / list / variant field walkers) that emits Field / Elem / Tag positions from its per- component blame traversal.

Both consumers produce Error trees whose children are keyed by Position, allowing errors from either source to compose into one tree.

AnnTerm

AnnTerm: canonical Position constant for the term being annotated.

Position

Canonical diagnostic Position constant. Segment: ann.term.

AnnType

AnnType: canonical Position constant for the type annotation supplied.

Position

Canonical diagnostic Position constant. Segment: ann.type.

AppArg

AppArg: canonical Position constant for the argument supplied to the application.

Position

Canonical diagnostic Position constant. Segment: app.arg.

AppHead

AppHead: canonical Position constant for the function applied.

Position

Canonical diagnostic Position constant. Segment: app.head.

Case

Case: parameterised position naming an eliminator's case handler by name — generated constructor names, "inl"/"inr", "base", "onRet"/"onArg"/"onRec"/"onPi"/"onPlus", "step".

Case : String -> Position

DArgBody

DArgBody: canonical Position constant for the description body produced by arg's family.

Position

Canonical diagnostic Position constant. Segment: arg.T.

DArgEq

DArgEq: canonical Position constant for the equality witness paired with arg's sort.

Position

Canonical diagnostic Position constant. Segment: arg.eq.

DArgLevel

DArgLevel: canonical Position constant for the universe level at which arg's sort lives.

Position

Canonical diagnostic Position constant. Segment: arg.k.

DArgSort

DArgSort: canonical Position constant for the sort inhabited by arg's argument.

Position

Canonical diagnostic Position constant. Segment: arg.S.

DConLayer

DConLayer: parameterised position naming the layer-th step in a peeled linear-recursive desc-con trampoline chain (0 = outermost, n = base); renders as con[<layer>]; quotient representative of homogeneous μ-unfolding paths so per-blame chain depth stays constant regardless of trampoline depth.

DConLayer : Int -> Position

DElimLevel

DElimLevel: canonical Position constant for the universe level at which the eliminator's motive lives.

Position

Canonical diagnostic Position constant. Segment: elim.k.

DPiBody

DPiBody: canonical Position constant for the description body produced by pi's family.

Position

Canonical diagnostic Position constant. Segment: pi.T.

DPiEq

DPiEq: canonical Position constant for the equality witness paired with pi's sort.

Position

Canonical diagnostic Position constant. Segment: pi.eq.

DPiFn

DPiFn: canonical Position constant for the index selector function of pi.

Position

Canonical diagnostic Position constant. Segment: pi.f.

DPiLevel

DPiLevel: canonical Position constant for the universe level at which pi's domain lives.

Position

Canonical diagnostic Position constant. Segment: pi.k.

DPiSort

DPiSort: canonical Position constant for the sort inhabited by pi's domain.

Position

Canonical diagnostic Position constant. Segment: pi.S.

DPlusL

DPlusL: canonical Position constant for the left summand of plus.

Position

Canonical diagnostic Position constant. Segment: plus.L.

DPlusR

DPlusR: canonical Position constant for the right summand of plus.

Position

Canonical diagnostic Position constant. Segment: plus.R.

DRecIndex

DRecIndex: canonical Position constant for the index value supplied to rec.

Position

Canonical diagnostic Position constant. Segment: rec.j.

DRecTail

DRecTail: canonical Position constant for the description tail spliced onto rec.

Position

Canonical diagnostic Position constant. Segment: rec.D.

DRetIndex

DRetIndex: canonical Position constant for the index value supplied to ret.

Position

Canonical diagnostic Position constant. Segment: ret.j.

Elem

Elem: parameterised position naming a list element by idx; renders as [<idx>] in blame paths and carries idx for downstream lookup by integer index.

Elem : Int -> Position

Field

Field: parameterised position naming a record field by name; renders as .<name> in blame paths and carries name for downstream lookup by field-key.

Field : String -> Position

JEq

JEq: canonical Position constant for the equality witness consumed by J.

Position

Canonical diagnostic Position constant. Segment: J.eq.

JLhs

JLhs: canonical Position constant for the left endpoint of J.

Position

Canonical diagnostic Position constant. Segment: J.a.

JRhs

JRhs: canonical Position constant for the right endpoint of J.

Position

Canonical diagnostic Position constant. Segment: J.b.

JType

JType: canonical Position constant for the type carrying J's two endpoints.

Position

Canonical diagnostic Position constant. Segment: J.A.

LamBody

LamBody: canonical Position constant for the body of the lambda under its bound variable.

Position

Canonical diagnostic Position constant. Segment: lam.body.

LetBody

LetBody: canonical Position constant for the body of the let-binding.

Position

Canonical diagnostic Position constant. Segment: let.body.

LevelMaxLhs

LevelMaxLhs: canonical Position constant for the left operand of max.

Position

Canonical diagnostic Position constant. Segment: max.L.

LevelMaxRhs

LevelMaxRhs: canonical Position constant for the right operand of max.

Position

Canonical diagnostic Position constant. Segment: max.R.

LevelSucPred

LevelSucPred: canonical Position constant for the predecessor of suc.

Position

Canonical diagnostic Position constant. Segment: suc.pred.

Motive

Motive: canonical Position constant for the motive of the eliminator.

Position

Canonical diagnostic Position constant. Segment: motive.

MuDesc

MuDesc: canonical Position constant for the description argument of con.

Position

Canonical diagnostic Position constant. Segment: con.D.

MuIndex

MuIndex: canonical Position constant for the index value supplied to con.

Position

Canonical diagnostic Position constant. Segment: con.i.

MuPayload

MuPayload: canonical Position constant for the payload of con at its index.

Position

Canonical diagnostic Position constant. Segment: con.d.

MuUnroll

MuUnroll: canonical Position constant for an unrolling step of μ.

Position

Canonical diagnostic Position constant. Segment: μ.

OpaqueType

OpaqueType: canonical Position constant for the Π-type annotation of the opaque lambda.

Position

Canonical diagnostic Position constant. Segment: opaque.type.

PiCod

PiCod: canonical Position constant for the codomain family of Π.

Position

Canonical diagnostic Position constant. Segment: Π.cod.

PiDom

PiDom: canonical Position constant for the domain type of Π.

Position

Canonical diagnostic Position constant. Segment: Π.dom.

Scrut

Scrut: canonical Position constant for the scrutinee of the eliminator.

Position

Canonical diagnostic Position constant. Segment: scrut.

SigmaFst

SigmaFst: canonical Position constant for the first component type of Σ.

Position

Canonical diagnostic Position constant. Segment: Σ.fst.

SigmaSnd

SigmaSnd: canonical Position constant for the second component type of Σ.

Position

Canonical diagnostic Position constant. Segment: Σ.snd.

Sub

Sub: canonical Position constant for the subsumption bridge from CHECK to INFER.

Position

Canonical diagnostic Position constant. Segment: sub.

Tag

Tag: parameterised position naming a tagged-union arm by name; renders as #<name> in blame paths and carries name for downstream lookup by variant tag.

Tag : String -> Position

Tuple

Tuple: parameterised position naming a tuple component by static idx; renders identically to Elem ([<idx>]) but stays distinct so consumers tell n-ary tuple from list descent.

Tuple : Int -> Position

ULevel

ULevel: canonical Position constant for the level argument of U.

Position

Canonical diagnostic Position constant. Segment: U.k.

eq

eq: structural equality on Position values; relies on Nix's attrset-by-content comparison so equal positions compare equal regardless of construction path.

eq : Position -> Position -> Bool

isPosition

isPosition: predicate recognising the Position ADT — checks _tag == "Position"; complements the Layer/Error predicates from fx.diag.error.

isPosition : Any -> Bool

renderSegment

renderSegment: render a Position as its short human-readable segment ("arg.S", "plus.L", ".age"); single field read since the segment is carried on the Position itself.

renderSegment : Position -> String

withRule

withRule: decorate a Position with a descent-rule annotation, returning a structurally distinct Position whose rule field is set to the supplied string; leaves the original canonical constant intact for sharing.

withRule : String -> Position -> Position

Use at the kernel-rule call site to record which rule emitted the descent — paired with bindPR to wrap the inner computation under a Position that carries both the structural coordinate (tag/segment/intent) and the rule identity. The hint resolver ignores rule (keys come from tag only), so decorating Positions never changes lookup.