DPlusR::not-a-desc
Key: DPlusR::not-a-desc
Category: description · Severity: error
Source: src/diag/hints.nix:878
the right summand of plus must be a description at the same index type as the left summand
Example
Hint::DPlusR::not-a-desc means the DPlusR 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 right summand is not a description.
descPlus leftDesc (natLit 0)
# Better: both summands are descriptions.
descPlus leftDesc (descRet tt)