incorrect hover for match in do-block

Stream: lean4

[Jovan Gerbscheid]

In this code:

def foo (y : Option Nat) : Option String := do
  let _ ← match y with
    | some n => some n
    | none => none
  return s! "oops"

If I hover over match, with or either of the |, there is a subtle highlight on the match block (which has type Option Nat), but the hover information tells me that the type is Option String (which is the type of the whole do-block). So there is a mismatch between what expression it seems like I'm hovering over, and what expression I'm getting the type of.

Replacing the matchwith an if-let fixes the problem (in the less preferred way), because there the hover highlight encompasses the whole do-block.

[Aaron Liu]

If you #print foo, you'll see that the match block got cps'd, and the corresponding match in the definition does have type Option String. This is probably why the hover also thinks the match block has type Option String. If you hover over the identifier being bound, the hover correctly displays Nat as the type.

I don't know how to fix this.

[Kyle Miller]

@Aaron Liu Hovers are generated during the elaboration process (surface syntax is associated to TermInfo data). The hover for match should be generated before any of the further transforms before the do notation.

[Kyle Miller]

There's some conceptual connection between them, but there does not have to be a direct correspondence between expressions you see in hovers and what appears in #print.

[Kyle Miller]

Reading docs#Lean.Elab.Term.Do.ToCodeBlock.doLetArrowToCode, it looks like the return type of the match really is Option String because match is a valid do element, and the code is transformed (I think) to something like

def foo (y : Option Nat) : Option String := do
  match y with
  | some n =>
    let _ ← some n
    return s! "oops"
  | none =>
    let _ ← none
    return s! "oops"

So the cps-like transformation happens sort of at macro expansion time for do notation.

If you wrap the match in parentheses, like

def foo (y : Option Nat) : Option String := do
  let _ ← (match y with
    | some n => some n
    | none => none)
  return s! "oops"

that prevents the match from being recognized as a do element, and so it elaborates as a plain term. That causes it to have an Option Nat hover.

[Kyle Miller]

One fix could be to have doLetArowToCode mark the match as being synthetic syntax, which would prevent incorrect hover.