Diagnostic Hints
Stable diagnostic Hint keys for checker and validation failures, with focused pages for each emitted key.
Diagnostic hints are stable labels for recurring checker and validation
failures. When an error includes a Hint::<key> token, the matching
page explains what the key means and where to start debugging.
Use this section when the raw error is too local and you need the larger shape of the failure: which kind of invariant was violated, what the checker was trying to establish, and what sort of change is usually relevant.
Each hint page also points back to the source location that emits the hint.
DArgSort::universe-mismatch
DArgSort::universe-mismatch — the sort position of `arg` must live in U(0); descriptions only carry small types.
DPiSort::universe-mismatch
DPiSort::universe-mismatch — the sort position of `pi` must live in U(0); `descPi` takes a small domain.
LevelMaxLhs::type-mismatch
LevelMaxLhs::type-mismatch — the left operand of `max` must be a Level.
LevelMaxRhs::type-mismatch
LevelMaxRhs::type-mismatch — the right operand of `max` must be a Level.
LevelSucPred::type-mismatch
LevelSucPred::type-mismatch — the predecessor of `suc` must be a Level.
ULevel::type-mismatch
ULevel::type-mismatch — the level argument of `U` must be a Level.
AnnType::not-a-type
AnnType::not-a-type — the annotation position must be a type (live in some U(k)), not a term.
JType::not-a-type
JType::not-a-type — the type parameter of `J` must be a type (live in some U(k)), not a term.
Motive.PiDom::not-a-type
Motive.PiDom::not-a-type — the motive's domain must be a type (live in some U(k)).
Motive::not-a-type
Motive::not-a-type — an eliminator's motive must return a type (live in some U(k)).
PiCod::not-a-type
PiCod::not-a-type — the codomain family of Π must return a type for each argument, not an ordinary value.
PiDom::not-a-type
PiDom::not-a-type — the domain of Π must be a type (live in some U(k)), not a term or value.
DArgBody::not-a-desc
DArgBody::not-a-desc — the body of `arg` must produce a description (Desc I), not an ordinary value.
DPiBody::not-a-desc
DPiBody::not-a-desc — the body of `pi` must produce a description for each input, not a plain term.
DPlusL::not-a-desc
DPlusL::not-a-desc — the left summand of `plus` must be a description (Desc I).
DPlusR::not-a-desc
DPlusR::not-a-desc — the right summand of `plus` must be a description at the same index type as the left summand.
DRecTail::not-a-desc
DRecTail::not-a-desc — the tail position of `rec` must itself be a description, not an ordinary term.
MuDesc::not-a-desc
MuDesc::not-a-desc — the description argument of μ must be a Desc I term, not an ordinary value.
AppHead::not-a-function
AppHead::not-a-function — the head of an application must have a function type (Pi).
DPiFn::not-a-function
DPiFn::not-a-function — the index selector `f` of `pi` must be a function `S -> I`.
Motive::not-a-function
Motive::not-a-function — the motive must be a function from the scrutinee's type into a type, not a bare type or value.
OpaqueType::not-a-function
OpaqueType::not-a-function — the annotation on an opaque lambda must be a Pi type.
DPiFn::type-mismatch
DPiFn::type-mismatch — the index selector's domain must match the declared sort `S`.
DRecIndex::type-mismatch
DRecIndex::type-mismatch — the index position of `rec` must match the Desc's declared index type.
DRetIndex::type-mismatch
DRetIndex::type-mismatch — the index position of `ret` must match the Desc's declared index type.
MuIndex::type-mismatch
MuIndex::type-mismatch — the index passed to `con` must have the description's index type.
MuPayload::type-mismatch
MuPayload::type-mismatch — the payload of `con` must inhabit the description's interpretation at the given index.
Elem::inhabitation-failed
Elem::inhabitation-failed — the element does not inhabit the list's element type.
Field::inhabitation-failed
Field::inhabitation-failed — the field's value does not inhabit the declared field type.
SigmaFst::inhabitation-failed
SigmaFst::inhabitation-failed — the first component does not inhabit the declared `fst` type.
SigmaSnd::inhabitation-failed
SigmaSnd::inhabitation-failed — the second component does not inhabit the dependent `snd` type.
Tag::inhabitation-failed
Tag::inhabitation-failed — the variant's payload does not inhabit the branch type.
Elem::refinement-failed
Elem::refinement-failed — the element violates the element type's refinement predicate.
Field::refinement-failed
Field::refinement-failed — the field's value violates the field type's refinement predicate.
SigmaFst::refinement-failed
SigmaFst::refinement-failed — the first component violates the `fst` type's refinement predicate.
SigmaSnd::refinement-failed
SigmaSnd::refinement-failed — the second component violates the `snd` type's refinement predicate.
Tag::refinement-failed
Tag::refinement-failed — the variant's payload violates the branch type's refinement predicate.
Case::type-mismatch
Case::type-mismatch — this case-body's inferred type does not match the type the eliminator's motive requires.
Scrut::type-mismatch
Scrut::type-mismatch — the scrutinee's type must match the eliminator's expected shape.
AnnTerm::type-mismatch
AnnTerm::type-mismatch — the annotated term does not match its declared type.
AppArg::type-mismatch
AppArg::type-mismatch — the argument does not match the function's domain.
JType::type-mismatch
JType::type-mismatch — the type parameter of `J` must match the type of its two endpoints.
OpaqueType::type-mismatch
OpaqueType::type-mismatch — the opaque lambda's declared domain does not match the expected domain.
::unhandled-boot-inl
::unhandled-boot-inl — the left injection `inl x` has no inference rule — the sum type's right summand is not determined by the syntax of `x` alone.
::unhandled-boot-inr
::unhandled-boot-inr — the right injection `inr y` has no inference rule — the sum type's left summand is not determined by the syntax of `y` alone.
::unhandled-boot-refl
::unhandled-boot-refl — `refl` has no inference rule — the type of the equated endpoint is not determined by its syntax.
::unhandled-lam
::unhandled-lam — this lambda has no inference rule — its domain and codomain types are not determined by its syntax.
::unhandled-other
::unhandled-other — this intro form has no inference rule — its type is not determined by its syntax alone.
::unhandled-pair
::unhandled-pair — this pair has no inference rule — its component types are not determined by its syntax.
::unhandled-tt
::unhandled-tt — the unit value `tt` has no inference rule — there is exactly one type it can inhabit.