This PR changes the "declaration uses 'sorry'" warning to use backticks
instead of single quotes, consistent with Lean's conventions for
formatting code identifiers in diagnostic messages.
This PR causes Lean to search through `@[suggest_for]` annotations on
certain errors that look like unknown identifiers that got incorrectly
autobound. This will correctly identify that a declaration of type
`Maybe String` should be `Option String` instead.
## Example
```
example : Except String Unit := return .ok ()
```
```
Function expected at
Result
but this term has type
?m.1
Note: Expected a function because this term is being applied to the argument
String
Hint: The identifier `Result` 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.
Perhaps you meant `Except` in place of `Result`?
```
The last line is added by this PR.
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.
```
