PiCod::not-a-type
Key: PiCod::not-a-type
Category: sort · Severity: error
Source: src/diag/hints.nix:860
the codomain family of Π must return a type for each argument, not an ordinary value. Provide a function whose body inhabits some U k.
Example
Hint::PiCod::not-a-type means the PiCod position uses a term or value where the checker needs a type. The example shows the failing form first, then one way to give the checker the missing structure.
# Bad: the codomain family returns a term.
pi nat (_: natLit 0)
# Better: the codomain family returns a type.
pi nat (_: nat)