# ::unhandled-boot-refl


**Key:** `::unhandled-boot-refl`

**Category:** shape · **Severity:** error

**Source:** [`src/diag/hints.nix:949`](https://github.com/kleisli-io/nix-effects/blob/main/src/diag/hints.nix#L949)

`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.

```nix
# 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))

```


---

[← All diagnostic hints](/nix-effects/diag-hints)