DPiBody::not-a-desc
Key: DPiBody::not-a-desc
Category: description · Severity: error
Source: src/diag/hints.nix:850
the body of pi must produce a description for each input, not a plain term. Return a Desc I via descRet, descArg, descRec, descPi, or descPlus.
Example
Hint::DPiBody::not-a-desc means the DPiBody position uses an ordinary term where the checker needs a Desc. The example shows the failing form first, then one way to give the checker the missing structure.
# Bad: the dependent body returns a term.
descPi nat f (_: natLit 0)
# Better: the dependent body returns a Desc.
descPi nat f (_: descRet tt)