Navigation

AnnTerm::type-mismatch

Key: AnnTerm::type-mismatch

Category: type-mismatch · Severity: error

Source: src/diag/hints.nix:880

the annotated term does not match its declared type

Example

Hint::AnnTerm::type-mismatch means the AnnTerm position supplies a term whose type does not match the expected type. The example shows the failing form first, then one way to give the checker the missing structure.

# Bad: the annotated term does not inhabit the annotation.
ann true_ nat

# Better: the term matches the annotation.
ann (natLit 1) nat

← All diagnostic hints