Weird `match` behaviour

Stream: general

[Martin Dvořák]

inductive Foo
  | bar
  | baz

example (x : Foo) (y : Fin 2)
    (h0 : 0 = (match x with | .bar => 0 | .baz => 1))
    (hy : y = (match x with | .bar => 0 | .baz => 1))
    : 0 = y := by
  sorry

Why does hy change, once I am inside the proof, to matching on x and h0 at the same time?
It looks like a bug.
Note that the constants don't have to be identical for it to appear.

[Eric Wieser]

inductive Foo
  | bar
  | baz

example (x : Foo) (y : Fin 2)
    (h0 : 0 = (match x with | .bar => 0 | .baz => 1))
    (hy : y = (match (generalizing := false) x with | .bar => 0 | .baz => 1))
    : 0 = y := by
  sorry

avoids it

[Martin Dvořák]

OK but why does match generalize something in the first place?

[Martin Dvořák]

Many seemingly random changes make the match generalizations disappear.

[Aaron Liu]

so you don't have to do it yourself (for example if you had ended up using h0 in the body of the second match)

[Martin Dvořák]

Are there no risks in Lean generalizing match expressions without the user noticing?

[Aaron Liu]

what kind of risks are you thinking of

[Aaron Liu]

it doesn't change the behavior of the match

[Martin Dvořák]

I mean, can something change from provable to unprovable under me hands, or even worse, from unprovable to provable?

[Aaron Liu]

I don't see how adding unused match discriminants could change anything significantly

[Aaron Liu]

I guess if you were intending on using the ungeneralized variable you could accidentally end up with something equal but not defeq to what you were intending

[Martin Dvořák]

OK but all unprovable things stay unprovable?

[Aaron Liu]

I'm sure skeletor could come up with an example involving complicated unification or custom elaborators for which generalizing and no generalizing gives actually different results, but I wouldn't worry about this in normal circumstances.

[Martin Dvořák]

I don't know who skeletor is. I'll just hope that match generalization isn't impactful. Thanks for all replies!