OpaqueType::not-a-function
Key: OpaqueType::not-a-function
Category: arity · Severity: error
Source: src/diag/hints.nix:890
the annotation on an opaque lambda must be a Pi type
Example
Hint::OpaqueType::not-a-function means the OpaqueType position uses a non-function where the checker needs a Pi-typed term. The example shows the failing form first, then one way to give the checker the missing structure.
# Bad: an opaque lambda annotation must be a Pi type.
opaqueLam nat body
# Better: annotate it with a function type.
opaqueLam (pi nat (_: nat)) body