OpaqueType::type-mismatch
Key: OpaqueType::type-mismatch
Category: type-mismatch · Severity: error
Source: src/diag/hints.nix:892
the opaque lambda's declared domain does not match the expected domain
Example
Hint::OpaqueType::type-mismatch means the OpaqueType 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 opaque lambda domain disagrees with the expected domain.
opaqueLam (pi bool (_: nat)) body
# Better: align the declared domain with the expected Pi domain.
opaqueLam (pi nat (_: nat)) body