::unhandled-boot-inl
Key: ::unhandled-boot-inl
Category: shape · Severity: error
Source: src/diag/hints.nix:945
the left injection inl x has no inference rule — the sum type's right summand is not determined by the syntax of x alone. Annotate with ann (inl x) (sum A B) to fix the expected sum, or place it where checking already provides one.
Example
Hint::unhandled-boot-inl means inl 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: inl does not determine the right summand by itself.
infer emptyCtx (inl (natLit 1))
# Better: annotate the intended sum type.
infer emptyCtx (ann (inl (natLit 1)) (sum nat bool))