# Meta 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 `Val`s 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 `Val`s 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: `ฮ” : { = { 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 `Val`s โ€” true iff `v._vTag == "VMeta"`. Kernel `Val`s 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 ``` ## Source - [`src/tc/elaborate/meta/constraints.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/meta/constraints.nix) - [`src/tc/elaborate/meta/context.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/meta/context.nix) - [`src/tc/elaborate/meta/eval.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/meta/eval.nix) - [`src/tc/elaborate/meta/meta.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/meta/meta.nix) - [`src/tc/elaborate/meta/unify.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/meta/unify.nix) - [`src/tc/elaborate/meta/zonk.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/elaborate/meta/zonk.nix)