AppHead::not-a-function
Key: AppHead::not-a-function
Category: arity · Severity: error
Source: src/diag/hints.nix:882
the head of an application must have a function type (Pi)
Example
Hint::AppHead::not-a-function means the AppHead position uses a non-function where the checker needs a Pi-typed term. The example shows the failing form first, then one way to give the checker the missing structure.
# Bad: the application head is not a function.
app (natLit 0) (natLit 1)
# Better: apply a lambda or another Pi-typed term.
app (lam "x" nat (x: x)) (natLit 1)