Unexplained ^^^ on check

Stream: new members

[Lars Ericson]

For this code in Lean 4:

structure Even where
  twice :: x : Nat

class Plus (α : Type) where
  plus : α → α → α

def Nat.plus : Nat → Nat → Nat
  | 0, k => k
  | n+1, k => (n.plus k) + 1

def Even.plus : Even → Even → Even
  | Even.twice a, Even.twice b => Even.twice (a + b)

instance : Plus Even where
  plus := Even.plus

instance : Add Even where
  add := Even.plus

def Even.toNat : Even → Nat
  | Even.twice x => x * 2

instance : ToString Even where
  toString x := toString (x.toNat)

instance : OfNat Even Nat.zero where
  ofNat := Even.twice Nat.zero

instance [OfNat Even x] : OfNat Even (Nat.succ (Nat.succ x)) where
  ofNat := (Even.twice 1) + ((@OfNat.ofNat Even) x)

#check (@OfNat.ofNat Even)

#check (0:Even)
#check (1:Even) -- expected to fail
#check (2:Even)
#check (3:Even) -- expected to fail
#check (4:Even)

The #checks which are not marked "expected to file" work fine. However, they are underlined with ^^^. "View problem" gives no text. What is happening? I did a lake exe cache get and lake build so I think I have the latest Mathlib 4. Attached is a screenshot showing the problem. At one point I got the tooltip to tell me that there was some problem with the definition of #check but I wasn't able to get that message back subsequently.
Screenshot-from-2023-07-16-10-10-35.png

[Yaël Dillies]

They do fail. Look at the infoview. It says failed to synthesize instance.

[Lars Ericson]

@Yaël Dillies that is for lines 35 and 37 which are the ones marked "expected to file". Here is a shorter version:

structure Even where
  twice :: x : Nat

instance : OfNat Even Nat.zero where
  ofNat := Even.twice Nat.zero

#check (@OfNat.ofNat Even)

You can see that in the attached screenshot, the #check is underlined, and it says "1 of 1 problem", however with no error message or diagnostic explainining that it thinks is a problem, and in the InfoView, we see a type on line 7 and no indication of a problem.
Screenshot-from-2023-07-16-10-59-21.png

[Kyle Miller]

In your first screenshot, if you put your cursor where the red underlines are (on 1 and 3) then you'll see the errors are there. Errors aren't reported on the #check token itself, but where the error actually is.

[Kyle Miller]

Notice in "all messages" it says you have an error at 35:8, which means line 35 column 8

[Lars Ericson]

@Kyle Miller please see the screenshot for the shorter reproducing example, line 7. No errors are indicated in the infoview. The #check is underlined with blue ^^^. Clicking "Show Problem" indicates a problem with the #check, with no diagnosis. Here is the text to reproduce the example:

structure Even where
  twice :: x : Nat

instance : OfNat Even Nat.zero where
  ofNat := Even.twice Nat.zero

#check (@OfNat.ofNat Even)

Screenshot-from-2023-07-16-11-27-08.png

My question is just why I am seeing blue ^^^^s under the #check when nothing is wrong.

[Yaël Dillies]

Blue underline means there's an info attached to it in the infoview (here the OfNat.ofNat : (x : ℕ) → [self : OfNat Even x] → Even)

[Lars Ericson]

@Yaël Dillies in the blue case it would be less confusing if "View problem. No quick fixes available" was not displayed.

[Yaël Dillies]

Agreed. Not sure what manages the right click context though.