VSCode underlines wrong position

Stream: general

[Kenny Lau]

variables (α : Type) [has_mul α] (f : α → α → α) (n1 n2 n3 : α)
#check by have : f (n1 * n2) n3 = function.uncurry f (n1 * n2)

[Kenny Lau]

[Kenny Lau]

VSCode highlights the first (n1 * n2) as the error, when it is in fact the second (n1 * n2) that causes the type mismatch

[Kevin Buzzard]

+1 for #check by have

[Jasmin Blanchette]

I'm not sure it's a bug. Type inference/checking in languages like ML, Haskell, and Lean is done by collecting and solving some constraints. It doesn't work left-to-right, and it often fails to identify the root cause.

[Kenny Lau]

it's a bug because if you do this instead:

variables (α : Type) [has_mul α] (f : α → α → α) (n1 n2 n3 : α)
#check f (n1 * n2) n3 = function.uncurry f (n1 * n2)

[Kenny Lau]

then the error is on the second n1 * n2 as it should

[Jasmin Blanchette]

Maybe it's a bug, but your argument doesn't convince me. ;)

[Kenny Lau]

well why can it identify the root cause in term mode but not in tactic mode?

[Jasmin Blanchette]

I don't know the procedure, but for all I know it could be nondeterministic and report random results.

[Jasmin Blanchette]

(The E prover, for example, compares pointers and is therefore nondetermistic.)

[Kevin Buzzard]

Maybe different elaboration strategies are being used for some reason?

[Kevin Buzzard]

I believe I've seen proofs of the form := <term> which fail, and then succeed with := by exact <term>

[Mario Carneiro]

I get a different error (failed to synthesize type class instance for has_mul (α × α)), but the error reporting is similarly odd. In particular, it reports the first term only when you use the same expression in both places, e.g. if you use n1 * n3 on the left then it reports on the right as you would expect. My guess is that it is hash consing the expressions and associating the error location to that, meaning that when we report the error we've forgotten which n1 * n2 was responsible for the error

[Kevin Buzzard]

So then it should be really easy to confuse lean in this way and we probably would have spotted it years ago?

[Mario Carneiro]

Indeed. It could be interacting with another feature though, like the have tactic or some other aspect here making it more niche

[Gabriel Ebner]

Hash consing is disabled by default IIRC.

[Reid Barton]

Is this at all related to rw thinking that it should rewrite every occurrence of whatever expression it decides to rewrite (e.g., x * y)?

[Sebastian Ullrich]

No idea what Lean 3 is doing there, but Lean 4 says image.png

[Mario Carneiro]

I see CoeT is dependent now :P

[Sebastian Ullrich]

The only non-hacky way to have

instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool :=
{ coe := decide p }

[Mario Carneiro]

:+1:

[Eric Wieser]

What's the story behind the change to CamelCase? Is the scope of the change just type classes, or does it extend to lemmas and defs too?

[Mario Carneiro]

they thought that lean didn't look enough like java