Surprising change in type inference

Stream: lean4

[Simon Hudon]

I'm upgrading to the latest nightly of Lean 4 I'm seeing the following change to some of my code:

structure FoldImpl (α β : Type u) where
  γ : Type u
  x₀ : γ
  f : γ → α → γ
  out : γ → β

inductive R : FoldImpl α β → FoldImpl α β → Prop
| intro {γ γ' x₀ y₀ f g out out'} :
  R ⟨γ, x₀, f, out⟩ ⟨γ', y₀, g, out'⟩

#check @R.intro
-- @R.intro : ∀ {x : {γ γ' : Type u_1} → {x₀ : γ} → {y₀ : γ'} → Type u_1}
--   {x_1 : {γ γ' : Type u_1} → {x₀ : γ} → {y₀ : γ'} → {f : γ → x → γ} → {g : γ' → x → γ'} → Type u_1} {γ γ' : Type u_1}
--   {x₀ : γ} {y₀ : γ'} {f : γ → x → γ} {g : γ' → x → γ'} {out : γ → x_1} {out' : γ' → x_1},
--   R { γ := γ, x₀ := x₀, f := f, out := out } { γ := γ', x₀ := y₀, f := g, out := out' }

before the update, here is what that #check would print out:

#check @R.intro
-- @R.intro : ∀ {α β γ γ' : Type u_1} {x₀ : γ} {y₀ : γ'} {f : γ → α → γ} {g : γ' → α → γ'} {out : γ → β} {out' : γ' → β},
--   R { γ := γ, x₀ := x₀, f := f, out := out } { γ := γ', x₀ := y₀, f := g, out := out' }

In order to get the same result, I have to declare R as:

inductive R : FoldImpl α β → FoldImpl α β → Prop
| intro {γ γ' x₀ y₀ f g out out'} :
  @R α β ⟨γ, x₀, f, out⟩ ⟨γ', y₀, g, out'⟩

Is this change expected? If so, why is it desirable?

[Leonardo de Moura]

No, the change is not expected. I will create an issue for it.

[Leonardo de Moura]

Pushed a fix for this bug https://github.com/leanprover/lean4/commit/87e6581e6bdb3c5db0588b721a1cb10731914358

[Simon Hudon]

That was fast! Thanks a lot!