DPiSort::universe-mismatch
Key: DPiSort::universe-mismatch
Category: universe · Severity: error
Source: src/diag/hints.nix:848
the sort position of pi must live in U(0); descPi takes a small domain. Use u 0, or encode the dependency through an index instead of the Pi domain.
Example
Hint::DPiSort::universe-mismatch means the DPiSort 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: descPi's domain sort is too large.
descPi (u 1) f (_: descRet tt)
# Better: use a small domain sort.
descPi (u 0) f (_: descRet tt)