Navigation

DArgBody::not-a-desc

Key: DArgBody::not-a-desc

Category: description · Severity: error

Source: src/diag/hints.nix:846

the body of arg must produce a description (Desc I), not an ordinary value. Build one with descRet, descArg, descRec, descPi, or descPlus.

Example

Hint::DArgBody::not-a-desc means the DArgBody 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 body returns an ordinary term.
descArg nat (_: natLit 0)

# Better: the body returns a description.
descArg nat (_: descRet tt)

← All diagnostic hints