lower case 'string'

Stream: lean4

[Chris Lovett]

I find my self typing lowercase string accidentally instead of String, it shows up as blue in VS Code with no red squiggly, but goto definition on it goes no where. Does anyone have any idea why lowercase string is not red squiggled by the LSP ?

[Arthur Paulino]

It's turning into an implicit argument via auto-implicit

[Arthur Paulino]

You can shut it down with set_option autoImplicit false

[Chris Lovett]

oh man, I see, I wonder if we should black list some extra confusing keywords like this from becoming auto-implicit Type variable names ...?

[Chris Lovett]

Or hard code that type name with an error message saying "Perhaps you meant to type String" :-)

[Wojciech Nawrocki]

I like the idea of a heuristic linter which, upon encountering a multi-letter auto-implicit which looks suspiciously close to an existing constant (by Levenshtein distance, say), shows a warning message. Unfortunately it will not work in cases where something that you forgot to import becomes auto-implicit. I often type HashMap Foo Bar and then get confusing universe errors because I forgot to open Std.

[Chris Bailey]

Chris Lovett said:

Or hard code that type name with an error message saying "Perhaps you meant to type String" :-)

rustc does something like this, but I think it just looks at the current list of declarations in the environment and applies a string metric instead of hardcoding:

fn main() {
    let x : String = String::new();
    let y : Strig = x;
}

produces

error[E0412]: cannot find type `Strig` in this scope
   --> src/main.rs:297:13
    |
297 |     let y : Strig = x;
    |             ^^^^^ help: a struct with a similar name exists: `String`
    |
   ::: /Users/user/.rustup/toolchains/stable-x86_64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/string.rs:366:1
    |
366 | pub struct String {
    | ----------------- similarly named struct `String` defined here

For more information about this error, try `rustc --explain E0412`.
error: could not compile `_` due to previous error

[James Gallicchio]

suggestion for the heuristic: if the term typechecks, do not produce a warning. the "there is a similar name in scope: ___" is only useful to me if the term is not type-checking for some odd reason

[James Gallicchio]

sometimes my names are just very similar :)

[Henrik Böving]

I don't think this is a good idea. If you are declaring an inductive type that is parameterized by something of type string it will usually typecheck regardless of whether you meant the auto implicit variable or the actual String. And if you have a function like

def foo (x : string) := ...

and start calling functions onto x that are for String only these function calls won't type check but they could also not typecheck for a variety of other reasons so it is not directly deducible that the x : string is the issue here.

[Henrik Böving]

In general it would also be a good readability lint and not just for bug finding I think, we do not want auto implicit names that are too close to real type names because then your code becomes basically impossible to read without an LSP session that highlights your variables properly and you paying attention to the highlighting which is something many people probably won't do until they have encountered this issue.

[Arthur Paulino]

I know that the vim plugin for Lean 4 doesn't highlight auto-implicit parameters like the VS Code extension does
cc @Rish Vaishnav

[Henrik Böving]

Wojciech Nawrocki said:

I like the idea of a heuristic linter which, upon encountering a multi-letter auto-implicit which looks suspiciously close to an existing constant (by Levenshtein distance, say), shows a warning message. Unfortunately it will not work in cases where something that you forgot to import becomes auto-implicit. I often type HashMap Foo Bar and then get confusing universe errors because I forgot to open Std.

Regarding the open Std and HashMap part, in doc-gen4 when we linkify markdown documentation and the user did not give a specific link what we also do is iterate over all the namespaces that are available in this file and check whether they contain a declaration with the name we are seeing which would in this case link HashMap to Std.HashMap. This does of course have potential for false positives but this is actually a benefit here. My suggestion to solve this would be: If the autoImplicit feature detects a name that is longer than a single character (since signle character is in my experience basically always something we want autoImplicit) and supposed to be made auto implicitIt should start iterating over the namespaces that are in scope similar to doc-gen, if it finds something with the same name there it should mark this as a warning and tell the user about the names from unopened namespaces they might be referring to. While this does have the same potential for false benefits as what we do in doc-gen this is in my opinion a benefit because it again improves readability and maintainability:

1. If I have some namespace imported that contains a type with this name but just haven't opened it yet i might do that in the future, then the code that relied on the name being free will most likely break, if it was linted before and the user listened this will not happen
2. Again if i want to read this without a full LSP session I probably don't want auto implicit names that match up with types from namespaces that are imported here already, it's just confusing to the reader because they themselves have to keep track of which namespace is open and which is not

and in the case that you actually have a good reason to keep a name auto implicit that would be marked as a lint this way we can still have an option that marks this name as being fine for the file or w/e.

[Mac]

I agree with Henrik. Furthermore, if the user really does wish to create a clash with their variable name, they can always make the variable explicit rather than implicit to get around the linter. :wink: