Unused variable linter bug (?)

Stream: mathlib4

[Pim Otte]

The following gives an unused variable on G (and removing it gives errors for obvious reasons). My meta-programming skills are still a little lacking to de-mathlibify this mwe, but maybe someone else can? I have checked it on live.lean-lang.org with v4.11.0-rc3

import Mathlib.Combinatorics.SimpleGraph.Path

def oddVerts (G : SimpleGraph V) := {(c : SimpleGraph.ConnectedComponent G) | Nonempty c}

[Johan Commelin]

@Kyle Miller do you know what is going on?

[Kyle Miller]

I've seen this issue before -- in the macro expansion, you have match (c : SimpleGraph.ConnectedComponent G) with ..., and for some reason type ascriptions in match statement discriminants don't appear to elaborate correctly, or at least terminfo is missing (try hovering over the type in the type ascription; you don't get any hover information!)

A fix is to avoid using this particular notation and instead use the basic set separation notation:

def oddVerts (G : SimpleGraph V) := {c : SimpleGraph.ConnectedComponent G | Nonempty c}

We should probably extend basic set separation notation to accept parentheses here, since the parenthesis notation gives a surprising expansion anyway.

[Mario Carneiro]

I don't think it's match statement discriminants, but rather type ascriptions in match patterns

[Mario Carneiro]

example (F : Nat → Prop) (x : Nat) (y : F x) : Nat :=
  match (y : F x) with
            -- ^ this has hover info
  | (_y : F x) => 1
         -- ^ this doesn't

[Mario Carneiro]

the same issue appears in anything that desugars to match statements, including pattern matching in let and have

[Mario Carneiro]

this is lean4#3955