feat: hint when an autobound variable's type fails to be a function (#11518)

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.
```