error location bug

Stream: lean4

[Bolton Bailey]

I encountered this error here, #mwe below. Is this a bug? As you can see, there is an error because the equality is comparing an arrow to a unit. The error message even says this is the problem. But the red squiggly underlines a completely different place from where the error is.

import Mathlib.Tactic.CategoryTheory.Coherence

section MonoidalCategory

open CategoryTheory
open scoped MonoidalCategory

universe v u

variable {C : Type u} [Category.{v} C] [MonoidalCategory C]

lemma otp
  (R : ∀ V₁ V₂ : C, V₁ ⊗ V₂ ⟶ V₂ ⊗ V₁)
  (xor : ∀ V₁ V₂ V₃ : C, V₁ ⊗ V₂ ⟶ V₃)
  (copy : ∀ V₁ V₂ V₃ : C, V₁ ⟶ V₂ ⊗ V₃)
  (copy_xor_comm : ∀ V₁ V₂ V₃ V₄ V₅ V₆ V₇ V₈ V₉ : C,
    -- The final arrow I want is V₁ ⊗ V₂ ⟶ V₃ ⊗ V₄
    ((((copy V₁ V₅ V₆) ⊗ (copy V₂ V₇ V₈)) : (V₁ ⊗ V₂ ⟶ (V₅ ⊗ V₆) ⊗ (V₇ ⊗ V₈))) -- error highlights this line
      ≫ (𝟙 _ ⊗≫ V₅ ◁ R V₆ V₇ ▷ V₈ ⊗≫ 𝟙 _)
      ≫ (((xor V₅ V₇ V₃) ⊗ (xor V₆ V₈ V₄)) : (V₅ ⊗ V₇) ⊗ (V₆ ⊗ V₈) ⟶ V₃ ⊗ V₄)
       : V₁ ⊗ V₂ ⟶ V₃ ⊗ V₄)
    =
    () -- but complains about this
  )
  (w : False)
  :
  False
  := by sorry

end MonoidalCategory

[Bolton Bailey]

I am noticing that if I delete some of the newlines the red squiggle gets longer. Is the issue that it is for some reason just impossible to make error highlighting span multiple lines?

[Sebastian Ullrich]

No, this is deliberate because otherwise many errors paint your entire declaration red, which people found confusing. We just don't usually have such "big" errors on the term level.

[Bolton Bailey]

Ok. I would suggest that, however confusing an error message that paints the entire term red may be, it might be even more confusing to put the error highlighting in a specific subterm which is not the locus of the problem.

In this case in particular it seems that it should not be hard to put the highlighting in the correct place. The error message itself directly copies out the part of the term which is the problem. Why can't we highlight just that subterm?

[Sebastian Ullrich]

I can't answer that off the top of my head, it works without notation

#check Eq true ()
#check true = ()

[Sebastian Ullrich]

Likely a binop% issue, it does work with simpler notation

#check Unit × ()

[Bolton Bailey]

Interesting that notation affects it, perhaps that is part of the problem.

I guess on further reflection, it makes more sense to me that the error message should highlight the whole equality when the types on either side don't match, because its not clear we should expect one side to be right over the other. So the concept that the error message reporting the () perhaps doesn't automatically mean that is what is wrong, and it doesn't mean we can just attach the highlighting there.

[Bolton Bailey]

Sebastian Ullrich said:

I can't answer that off the top of my head, it works without notation

#check Eq true ()
#check true = ()

No actually this has the same problem, look:

#check Eq true ()
#check true
= ()

when I split the line, the second half of the line isn't highlighted.

[Bolton Bailey]

Wait, perhaps I have misunderstood this in the context of my later comment. Is the idea supposed to be that the highlighting for the true = () is wrong and the Eq true () highlighting is right?

[Bolton Bailey]

I think there are perhaps two issues at play here. One is my issue with how errors in the type of an argument to the function are highlighted on the argument, which I think can be a little confusing if the problem is with the function and not the argument, but I understand the desire to keep the error where lean becomes aware of it.

The other is that the error highlighting is being changed by the presence of linebreaks, which I think is more objectively wrong behavior.

[Kyle Miller]

There are some bugs with how true = () shows the error. Working on a fix.

[Jon Eugster]

Bolton Bailey said:

No actually this has the same problem, look:

#check Eq true ()
#check true
= ()

I think the error diagnostics has the correct fullRange is this example (something like
{start : {line: 1, character: 7}, end: {line: 2, character: 4} but somehow VSCode (?) decides the correct thing to do here is to only highlight up to the first newline.

[Kyle Miller]

The error message wasn't being localized to the expression under consideration, which could be solved with some withRefs:

image.png

lean4#3442