DPiFn::not-a-function
Key: DPiFn::not-a-function
Category: arity · Severity: error
Source: src/diag/hints.nix:872
the index selector f of pi must be a function S -> I
Example
Hint::DPiFn::not-a-function means the DPiFn 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 index selector is not a function.
descPi nat expectedIndex (_: descRet expectedIndex)
# Better: provide a selector from the domain into the index type.
descPi nat (x: expectedIndex) (_: descRet expectedIndex)