Navigation

DArgSort::universe-mismatch

Key: DArgSort::universe-mismatch

Category: universe · Severity: error

Source: src/diag/hints.nix:844

the sort position of arg must live in U(0); descriptions only carry small types. Pass u 0, or factor the dependency through descRec / descPi if a larger type is genuinely needed.

Example

Hint::DArgSort::universe-mismatch means the DArgSort position uses a universe level that is too large for that slot. The example shows the failing form first, then one way to give the checker the missing structure.

# Bad: description argument sorts must stay in U0.
descArg (u 1) (_: descRet tt)

# Better: keep the argument sort small.
descArg (u 0) (_: descRet tt)

← All diagnostic hints