::unhandled-lam
Key: ::unhandled-lam
Category: shape · Severity: error
Source: src/diag/hints.nix:939
this lambda has no inference rule — its domain and codomain types are not determined by its syntax. Annotate with ann (lam …) (pi A B) to drive checking, or place it where the surrounding rule already supplies an expected Pi type.
Example
Hint::unhandled-lam means a lambda is in inference mode without an expected Pi type. The example shows the failing form first, then one way to give the checker the missing structure.
# Bad: a lambda reaches inference without an expected Pi type.
infer emptyCtx (lam "x" nat (x: x))
# Better: annotate it so checking mode knows the Pi type.
infer emptyCtx (ann (lam "x" nat (x: x)) (pi nat (_: nat)))