Relax auto-implicit restrictions

[Kha]

In the last dev meeting we decided that we can probably lift the restriction of auto-implicits to single-letter lower-case identifiers now that we have semantic highlighting, much like Isabelle does. I did voice the caveat though that because of limitations in the LSP clients, semantic hightlighting currently is updated only after the entire file has been elaborated.

This issue is to document the discussion, and see if there are any further concerns or other comments.

[Kha]

semantic hightlighting currently is updated only after the entire file has been elaborated.

To be more precise, lsp-mode on edit seems to request a highlighting update for the current view, and then for the remaining file (both without support for partial results). So it might not be too bad as long as your current viewport is not that expensive to elaborate. I don't know the behavior of other editors.

[gebner]

neovim doesn't have semantic highlights yet (probably next release). I haven't found auto-implicits to be confusing without the highlighting.

[leodemoura]

We can disable the feature using set_option relaxAutoImplicit false.
Let's see how confusing the new default is.