ab606ba754
This PR provides an additional hint when the type of an autobound implicit is required to have function type or equality type — this fails, and the existing error message does not address the fact that the source of the error is an unknown identifier that was automatically bound. ## Example ``` import Lean example : MetaM String := pure "" ``` Current error message: ``` Function expected at MetaM but this term has type ?m Note: Expected a function because this term is being applied to the argument String ``` Additional error message provided by this PR: ``` Hint: The identifier `MetaM` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement. ``` |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||