# 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[]`; 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 `[]` 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 `.` 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 `#` 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` (`[]`) 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.