::unhandled-boot-refl
Key: ::unhandled-boot-refl
Category: shape · Severity: error
Source: src/diag/hints.nix:949
refl has no inference rule — the type of the equated endpoint is not determined by its syntax. Annotate with ann refl (eq A x x), or use refl where the surrounding rule already supplies an expected equality type.
Example
Hint::unhandled-boot-refl means refl is in inference mode without an expected equality type. The example shows the failing form first, then one way to give the checker the missing structure.
# Bad: refl does not determine the equality type by itself.
infer emptyCtx refl
# Better: annotate the equality being proven.
infer emptyCtx (ann refl (eq nat zero zero))