::unhandled-boot-inr
Key: ::unhandled-boot-inr
Category: shape · Severity: error
Source: src/diag/hints.nix:947
the right injection inr y has no inference rule — the sum type's left summand is not determined by the syntax of y alone. Annotate with ann (inr y) (sum A B) to fix the expected sum, or place it where checking already provides one.
Example
Hint::unhandled-boot-inr means inr is in inference mode without an expected Sum type. The example shows the failing form first, then one way to give the checker the missing structure.
# Bad: inr does not determine the left summand by itself.
infer emptyCtx (inr true_)
# Better: annotate the intended sum type.
infer emptyCtx (ann (inr true_) (sum nat bool))