_internal

fx.tc.check._internal: cross-part checker helpers reachable from sibling parts via the self-fixpoint; not part of the stable consumer surface.

checkDescAtAnyLevel

checkDescAtAnyLevel: description checking at any universe level — accepts both primitive VDesc results and encoded VMu descriptions (the VDesc ↔ μ_⊤(descDesc I L) correspondence) and threads the universe level back to the caller for downstream encoding decisions.

checkDescAtAnyLevel : Ctx -> Tm -> Val -> Computation { term; level }

Trusted-annotation fast path: when dTm is a T.mkAnnTrusted with a complete _descRef, build a canonical description term directly (skipping the unfolding scan) and reuse the carried level. Otherwise fall through to inference and dispatch on the inferred type's tag:

• VDesc: the level is already on the type; conv-check that the index type matches iTyVal and forward.
• VMu: the description is encoded — scan a bounded list of candidate universe levels (the prelude exercises L = 0..3) and ask conv whether V.vDesc lev iTyVal unifies with the inferred type. Conv fires the symmetric VDesc ↔ VMu unfolding internally (same mechanism as conv.nix:344-355).
• Anything else: emit a typeError — not a description.

Used by desc-con checking (check.nix) for _descConCert validation, by infer.nix for desc-ind motive and branch checking, and by type.nix:mu to thread the description level into the μ type's universe level.

checkMotive

checkMotive: eliminator-motive validation — walks the lambda layers of a motive against an expected domain chain D_1 → … → D_n → U(k) and returns the elaborated motive term together with the universe level k of its codomain.

checkMotive : Ctx -> Tm -> Chain -> Comp { term; level }

The domain chain is a { head : Val; tail : Val → Chain } | null sequence so each layer's domain may depend on the previously-bound value (required by desc-ind, whose motive is (i : I) → μ D i → U(k)). 1-argument call sites use the singleton helper to build a one-element chain.

• Lambda motive: extend the context with the current layer's domain, recurse into the body with chain.tail freshV, and wrap the result in T.mkLam. The level threads up unchanged through each lam wrapper so the innermost codomain's universe flows back to eliminators that care about it (e.g., desc-ind's allTy).
• Non-lambda motive: fall through to infer, then walk the inferred Π-chain in lock-step with the expected chain, conv-checking each domain and instantiating each codomain through a fresh variable. The innermost codomain must be a universe; its level is the motive's level.

Failure modes emit D.mkKernelError under the P.Motive position for the diagnostic renderer. Cross-ref: singleton for the unary-chain helper, infer for the synthesis fallback, checkTypeLevel for the innermost-universe leaf.

singleton

singleton: build a one-element motive chain — { head = dom; tail = _: null; } — the trivial telescope used by checkMotive call sites with a single domain and no nested binder dependency.

singleton : Val -> Chain

The motive chain consumed by checkMotive is a nested { head : Val; tail : Val → Chain } | null structure so each layer's domain may depend on prior binder values. Most eliminator sites (Sum, Eq, Squash) have only one motive argument and no inter-binder dependency; singleton dom packs that into the chain shape with a constant tail that ignores its argument and returns null — closing the chain after a single layer.