Meta — nix-effects

fx.tc.elaborate.meta: meta-aware overlay — VMeta, overlay check/infer, overlay eliminators, quote, elabConv, five scoped meta-effects (force/getMetas/assignMeta/emitConstraint/getConstraints), runElab handler.

`addAndSimplifyConstraint`

addAndSimplifyConstraint c state: simplify a constraint, allocate its id, append it to 𝒦, and update mentions.

addAndSimplifyConstraint : Constraint -> ElabState -> { id : Int; state : ElabState; }

`addConstraint`

addConstraint c state: allocate a constraint id, append to 𝒦, and register watcher mentions.

addConstraint : Constraint -> ElabState -> { id : Int; state : ElabState; }

`assignMeta`

assignMeta id tm: send-emitter extending Δ with id ↦ tm. Wakes any watchers registered in mentions[id] (per Abel-Pientka, section 7) when the assignment lands. Response shape: unit.

assignMeta : Int -> Tm -> Comp Unit

`coerce`

coerce: embed a kernel Val into ElabVal. Identity at the Nix level — the coproduct ElabVal = Val ⊎ VMeta is structural (kernel Vals are already valid ElabVal inhabitants because VMeta has a disjoint tag).

coerce : Val -> ElabVal

`descendImplicitPi`

Wrap a body in implicit lambdas peeling leading implicit binders from an expected type.

descendImplicitPi : Ctx -> Val -> (Ctx -> Val -> Comp Tm) -> Comp Tm

`dispatchMeta`

dispatchMeta: bridge dispatch for the 5 meta-effects — selects the appropriate step on ctx.op._opTag and threads ctx.state (Nix-side Δ/𝒦/mentions attrset). Throws on unknown tags so accidental effect-set drift fails at build time.

dispatchMeta : { op; outputVal; state } -> { action; newState; response?; }

`elabAllDF`

elabAllDF fuel level I D K X M i d: meta-aware allD. VMeta in the description position appends EAllD.

elabAllDF : Fuel -> Val -> Val -> ElabVal -> Val -> Val -> Val -> Val -> Val -> ElabVal

`elabAppF`

elabAppF fuel fn arg: meta-aware application helper. Rigid fn delegates to the kernel evaluator; VMeta appends EApp arg to its spine.

elabAppF : Fuel -> ElabVal -> ElabVal -> ElabVal

`elabBootJ`

elabBootJ type lhs motive base rhs eq: meta-aware J eliminator. VBootRefl reduces to base; VMeta appends EBootJ.

elabBootJ : Val -> Val -> Val -> Val -> Val -> ElabVal -> ElabVal

`elabBootSumElimF`

elabBootSumElimF fuel left right motive onLeft onRight scrut: meta-aware bootstrap sum eliminator. VMeta appends EBootSumElim.

elabBootSumElimF : Fuel -> Val -> Val -> Val -> Val -> Val -> ElabVal -> ElabVal

`elabCheck`

elabCheck ctx tm ty: elaborator checking wrapper. Rigid cases delegate to the rigid checker; meta-involving Sub-rule cases synthesize then call elabConv, emitting postponed constraints instead of rigid type errors.

elabCheck : Ctx -> ElabTm -> ElabVal -> ElabComp ElabTm

`elabCheckTm`

elabCheckTm ctx tm ty: run elabCheck under runElab and return the value branch.

elabCheckTm : Ctx -> ElabTm -> ElabVal -> ElabTm | Error

`elabConv`

elabConv d ty lhs rhs: meta-aware conversion for elaboration. Rigid comparisons delegate to kernel conversion; comparisons involving VMeta emit postponed conv constraints; Pi/Sigma types are compared structurally using overlay eliminators so metas retain their spines.

elabConv : Depth -> Val -> ElabVal -> ElabVal -> Comp Bool

`elabDescIndF`

elabDescIndF fuel D motive step i scrut: meta-aware descInd eliminator. VMeta appends EDescInd.

elabDescIndF : Fuel -> Val -> Val -> Val -> Val -> ElabVal -> ElabVal

`elabEverywhereDF`

elabEverywhereDF fuel level I D K X M ih i d: meta-aware everywhereD. VMeta in the description position appends EEverywhereD.

elabEverywhereDF : Fuel -> Val -> Val -> ElabVal -> Val -> Val -> Val -> Val -> Val -> Val -> ElabVal

`elabFst`

elabFst p: meta-aware first projection. Rigid pairs/neutrals delegate to the kernel evaluator; VMeta appends EFst.

elabFst : ElabVal -> ElabVal

`elabInfer`

elabInfer ctx tm: elaborator synthesis wrapper. Rigid terms delegate to the rigid checker; overlay meta terms carrying a type annotation synthesize that annotation without entering the rigid checker.

elabInfer : Ctx -> ElabTm -> ElabComp { term : ElabTm; type : ElabVal }

`elabInferApp`

elabInferApp ctx tm: App-mode synthesis. Infers fn type, peels leading implicit Pis via insertImplicits when the call site is explicit, then checks the argument against the resulting explicit domain.

elabInferApp : Ctx -> ElabTm -> Comp ({ term; type } | Error)

`elabInferTm`

elabInferTm ctx tm: run elabInfer under runElab and return the value branch.

elabInferTm : Ctx -> ElabTm -> { term; type } | Error

`elabInterpDF`

elabInterpDF fuel level I D X i: meta-aware interpD. VMeta in the description position appends EInterpD.

elabInterpDF : Fuel -> Val -> Val -> ElabVal -> Val -> Val -> ElabVal

`elabLiftElimF`

elabLiftElimF l m eq A x: meta-aware Lift eliminator. VMeta appends ELiftElim.

elabLiftElimF : Val -> Val -> Val -> Val -> ElabVal -> ElabVal

`elabSnd`

elabSnd p: meta-aware second projection. Rigid pairs/neutrals delegate to the kernel evaluator; VMeta appends ESnd.

elabSnd : ElabVal -> ElabVal

`elabSquashElimF`

elabSquashElimF fuel A B f x: meta-aware propositional-truncation eliminator. VMeta appends ESquashElim.

elabSquashElimF : Fuel -> Val -> Val -> Val -> ElabVal -> ElabVal

`emitConstraint`

emitConstraint c: send-emitter appending c to the constraint queue 𝒦. Distinct from typeError (a type-error is proof of unsolvability; a postponed constraint is a monotone wait per Optimist's Lemma, GMM section 6.2 Lemma 4). Response shape: the allocated constraint id.

emitConstraint : Constraint -> Comp Int

`emptyState`

emptyState: initial runElab state — Δ, 𝒦, watcher index, ordered meta ids, and monotone fresh counters.

emptyState : ElabState

`evalElab`

evalElab state env tm: zonk tm against state.delta then delegate to kernel eval. Unsolved metas yield a stuck VMeta value.

evalElab : ElabState -> Env -> Tm -> Val

`extendMeta`

extendMeta id type state: add a Hole entry to Δ and advance the fresh-id counter past it.

extendMeta : Int -> MetaType -> ElabState -> ElabState

`force`

force v: send-emitter requesting Δ-aware reduction of v. Kernel Vals pass through unchanged; VMeta { id; spine; type } is reduced via delta[id] · spine when id is solved in Δ, else returned unchanged. Response shape: ElabVal.

force : ElabVal -> Comp ElabVal

`forceMeta`

forceMeta v state: if v is solved in Δ, replay its captured spine over the solution.

forceMeta : VMeta -> ElabState -> ElabVal

`freshMeta`

freshMeta type: allocate a new metavariable hole in Δ of the given type. Response shape: VMeta.

freshMeta : MetaType -> Comp VMeta

`freshMetaInState`

freshMetaInState type state: allocate a new VMeta and append a matching Hole entry to Δ.

freshMetaInState : MetaType -> ElabState -> { meta : VMeta; state : ElabState; }

`getConstraints`

getConstraints: send-emitter reading the current constraint queue 𝒦. Response shape: 𝒦 : [Constraint].

getConstraints : Comp [Constraint]

`getMetas`

getMetas: send-emitter reading the current meta-context Δ. Response shape: Δ : { <metaId> = { tm; type } | null }.

getMetas : Comp Delta

`handle_Meta`

handle_Meta: kernel HOAS shell λ_op. λ_s. tt for the meta-effects bridge. Paired with runElab's dispatchMeta, which carries the actual per-op interpretation Nix-side.

`handle_MetaTy`

handle_MetaTy: Π(_op:metaEff). Π(_s:Unit). Unit. Unit codomain reflects that outputVal carries no info for meta-effects — Δ updates and responses flow Nix-side via dispatchMeta.

`insertImplicits`

Peel leading implicit Pi binders of a function's inferred type by fresh-meta insertion. Returns Comp { term; type } with the explicit head.

insertImplicits : Ctx -> Tm -> Val -> Comp { term : Tm; type : Val }

`isHole`

isHole m: true when a metavariable-context entry is unsolved.

isHole : MetaEntry -> Bool

`isImplicitPi`

Predicate: value is a VPi with implicit plicity sidecar.

isImplicitPi : Val -> Bool

`isSolved`

isSolved m: true when a metavariable-context entry carries a solution.

isSolved : MetaEntry -> Bool

`isVMeta`

isVMeta: predicate distinguishing the overlay VMeta from kernel Vals — true iff v._vTag == "VMeta". Kernel Vals use tag (not _vTag) for ADT discrimination, so the predicate is decidable on the disjoint union.

isVMeta : ElabVal -> Bool

`isVMetaTy`

Predicate: value is a VMeta (overlay representation).

isVMetaTy : Val -> Bool

`levelsVal`

levelsVal v: collect neutral variable levels referenced by an elaborator value.

levelsVal : ElabVal -> [Level]

`lookupMeta`

lookupMeta state id: read a Δ entry by metavariable id, returning null when absent.

lookupMeta : ElabState -> Int -> MetaEntry | Null

`markConstraint`

markConstraint cid status extra state: update one constraint status and merge extra diagnostic fields.

markConstraint : Int -> String -> AttrSet -> ElabState -> ElabState

`mentionsOf`

mentionsOf vals: collect unique metavariable ids referenced by a list of elaborator values.

mentionsOf : [ElabVal] -> [Int]

`metaEff`

metaEff: kernel-typed effect signature for the elaborator's 5 meta-effects — 5-element H.variant over tags force / getMetas / assignMeta / emitConstraint / getConstraints. Payload types are uniformly H.unit; semantic payload data rides in the Nix-host sentinel attached to the op argument.

metaEff : Hoas U

`metaIdsVal`

metaIdsVal v: collect metavariable ids referenced by an elaborator value and its spine payloads.

metaIdsVal : ElabVal -> [Int]

`metaResp`

metaResp: response-type function for metaEff — kernel-typed λ_op : metaEff. H.unit. All five meta-effects return Nix-host opaque values; the kernel-level response is uniformly unit.

metaResp : Hoas (metaEff -> U)

`mkConstraint`

mkConstraint c: normalize a constraint record with default position, mentions, and status fields.

mkConstraint : AttrSet -> Constraint

`mkHole`

mkHole id type: construct an unsolved metavariable-context entry.

mkHole : Int -> MetaType -> MetaEntry

`mkMeta`

mkMeta: overlay term head for quoted metavariables. This is not a kernel Tm constructor; it lives only in fx.tc.elaborate's meta-aware term overlay.

mkMeta : Int -> [ElabTm] -> ElabTm

`mkSolved`

mkSolved id tm type: construct a solved metavariable-context entry.

mkSolved : Int -> ElabVal -> MetaType -> MetaEntry

`mkVMeta`

mkVMeta: construct an overlay metavariable value — { _vTag = "VMeta"; id; spine; type = { ctx; ty } }. id is the globally-unique meta identifier allocated by runElab; spine is the local-variable spine captured at construction (Abel-Pientka, section 2 σ); type carries the meta's allocation-site typing context plus its expected type (paper's A[Φ] annotation).

mkVMeta : Int -> [Val] -> { ctx : Ctx; ty : Val } -> ElabVal

`nf`

nf env tm: kernel eval followed by meta-aware quote.

nf : Env -> Tm -> ElabTm

`occurs`

occurs id v: true when v references metavariable id.

occurs : Int -> ElabVal -> Bool

`patternSpine`

patternSpine spine: true for application spines whose arguments are distinct bound variables.

patternSpine : Spine -> Bool

`plicityAwait`

Emit a postponed plicity-await constraint awaiting the named meta; re-awakens when the meta solves.

plicityAwait : Ctx -> Int -> Val -> Val -> Comp Int

`processActiveConstraints`

processActiveConstraints state: rerun local simplification for active constraints and preserve non-active constraints.

processActiveConstraints : ElabState -> ElabState

`quote`

quote d v: meta-aware read-back. Rigid values delegate to fx.tc.quote; VMeta quotes to mkMeta id [] with its elimination spine replayed as ordinary term eliminators.

quote : Depth -> ElabVal -> ElabTm

`quoteElim`

quoteElim d head frame: replay one kernel spine frame against an overlay term head, recursively using meta-aware quote for frame payloads.

quoteElim : Depth -> ElabTm -> SpineEntry -> ElabTm

`quoteSp`

quoteSp d head spine: fold quoteElim over a stored elimination spine.

quoteSp : Depth -> ElabTm -> [SpineEntry] -> ElabTm

`reawakenMentions`

reawakenMentions ids state: mark postponed constraints watching solved metavariables active.

reawakenMentions : [Int] -> ElabState -> ElabState

`registerMentions`

registerMentions mentions cid index: add a constraint id to every mentioned metavariable watcher list.

registerMentions : [Int] -> Int -> MentionsIndex -> MentionsIndex

`runElab`

runElab A program: discharge an elaborator computation through the descInterp trampoline. Threads emptyState Nix-side via the bridge's state channel; handle_Meta (kernel shell) plus dispatchMeta (Nix-side interpreter) discharge the 5 meta-effects.

runElab : Hoas U -> Hoas (μ freeFxApp metaEff metaResp A) -> { value; state : ElabState; }

`sigmaFlatten`

sigmaFlatten id state: replace an unsolved Sigma-typed meta with a pair of freshly allocated component metas.

sigmaFlatten : Int -> ElabState -> ElabState

`simplifyConstraint`

simplifyConstraint c state: locally simplify one constraint by rigid conversion, direct meta solving, occurs-check failure, or postponement.

simplifyConstraint : Constraint -> ElabState -> { state : ElabState; constraint : Constraint; }

`solveMeta`

solveMeta id tm state: replace a Δ entry with a Solved entry and reawaken constraints watching that id.

solveMeta : Int -> ElabVal -> ElabState -> ElabState

`updateConstraint`

updateConstraint cid f state: update one constraint in 𝒦 by id.

updateConstraint : Int -> (Constraint -> Constraint) -> ElabState -> ElabState

`zonkTm`

zonkTm depth state tm: substitute solved metas in tm. Returns { error = { unsolved-meta; id; ctx; } } if any Hole is in state.delta; else { value = tm' } with thunked sub-fields (stack-safe, forcing deferred to consumer access).

zonkTm : Depth -> ElabState -> Tm -> Result Tm