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