RFC: type errors involving auto implicits should warn about auto implicits

Context

Currently, by default, when an unbound variable is accidentally used, the error message produced is not helpful. The exact error message produced depends on the situation, but it often involves a metavariable indicating the (could not be inferred) type of the implicitly bound variable, as well as an actual message that is completely unrelated. Nothing in the message suggests that this could be a misspelled variable, or that there is a constant with the same name but not in the current scope.

I have noticed many beginners have tripped on this issue, including myself when I was learning Lean. Without the help of someone who specifically knows about this counterintuitive (yet logical) behavior of Lean, it can be pretty challenging to find the cause of the error, especially for someone who may not know yet the precise differences between modules, namespaces and scopes in Lean.

Just to cite one example of this, consider this SO question:

import Std.Data.HashMap

--
-- A definition of the kinds of types given in the TOML specification at
-- https://toml.io/en/v1.0.0#objectives.
--
inductive TOMLType where
    | boolean (b : Bool)
    | integer (n : Int)
    | float (n : Float)
    | string (s : String)
    | array (elems : Array TOMLType)
    | table (kvPairs : HashMap String (fun _ => TOMLType))
    -- TODO: add more types like DateTime here.

This produces the following error message:

function expected at
  HashMap
term has type
  ?m.21

I don't know whether the person who asked the question knew about the auto implicit option, but if they didn't (which is not unlikely, given that it's opt out), it would have been pretty much impossible for them to figure out what is wrong. Especially because they seem to think that loading the Std.Data.HashMap implies having the HashMap constant available in the current scope.

Proposal

Have the error message suggest that this might be due to a misspelled name, or referencing a name present in an other namespace. Consider what happens, for instance, in Rust:

• if this looks like a misspelled name, and a similar name is found in the current scope, it is suggested: "help: a local variable with a similar name exists: ..."
• if this looks like a constant that exists in an other namespace, it is suggested: "help: consider importing one of these traits instead: ..."
  Both of these hints are accompanied by LSP actions that execute the suggestion.
  This is a non-trivial task because, at least in my understanding, auto implicits can cause a wide variety of errors for which it is not always easy to determine that we should instead report that "the variable implicitly bound" is such a variable.

Orthogonally to this solution, one could also think of having auto implicits off by default. It is a bit of a mistery to me who would want to use such a feature, because my experience with it has been that by the time I had reached the expertise required not to be confused about what this feature does exactly, and what its gotchas are, I was already convinced that it was a bad software engineering practice to have it on, because although it makes me type less, it also makes me think more when I need to read code that relies on it, which in this case I don't think is a good tradeoff. This is of course only my opinion on the matter, and other people might think that the tradeoff is actually worth it, but:

• I don't think that's a question a beginner should ask themselves;
• the fact that Mathlib has it turned off, and everyone who I spoke about this too, makes me think my opinion on this is rather common.
  This is especially true as, IIRC, there is a weaker version of auto implicits that only does so with names that look like parametric types, which is I think the only time this option is meant to be used anyways.

This is easy to implement. It's a breaking change, but it's not that hard to port a pre-change project: just explicitly opt in for this feature, and everything will work as before the change.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

No files or tests are named. Start by reviewing Lean's existing auto-implicit behavior and the diagnostic paths that produce the reported type errors; done means relevant errors suggest misspelled names or names in another namespace without breaking the stated opt-in compatibility path.