!4#2084 wrong instances

Stream: mathlib4

[Jon Eugster]

Consider the following MWE:

import Mathlib.Data.Fintype.Option

set_option autoImplicit false

universe u

/- simplified from `Fintype.induction_empty_option`. -/
@[elab_as_elim]
theorem induction_empty_optionₓ {P : ∀ (α : Type u) [Fintype α], Prop}
    (H : ∀ α [Fintype α], P α)
    (α : Type u)
    [Fintype α] : P α := by
  exact H α

example -- fails (error on `example`)
    {P : ∀ (α : Type u) [Fintype α], Prop}
    (H : ∀ α [Fintype α], P α)
    (α : Type u)
    [h : Fintype α] : P α := by
      refine induction_empty_optionₓ ?_ α
      exact H --fails

Using refine/refine' here creates the following two errors:

application type mismatch
  P x✝¹
argument has type
  Fintype α
but function has type
  [inst : Fintype x✝¹] → Prop

and

type mismatch
  H
has type
  ∀ (α : Type u) [inst : Fintype α], P α : Prop
but is expected to have type
  ∀ (α : Type u) [inst : Fintype α], P α : Prop

In the first error it unfolds to (@P x✝¹ h : Prop) where h is of Type Fintype α even though it should insert an instance Fintype x✝¹, and similarly in the second error the second of the two P α unfolds as @ P α h, but with h : Fintype α✝.

Does anybody know why lean4 would insert instances here that are clearly the for the wrong types? Is that maybe a bug that's already known or fixed in an upcoming bump?

Or is the Lemma docs4#Finite.induction_empty_option badly shaped with all these ∀ α [Fintype α], _?
(This problem appears as the first error in !4#2084 l. 438)

[Eric Wieser]

It works fine if I add some @s:

example -- ok
    {P : ∀ (α : Type u) [Fintype α], Prop}
    (H : ∀ α [Fintype α], P α)
    (α : Type u)
    [h : Fintype α] : P α := by
      refine @induction_empty_optionₓ _ ?_ α _
      exact H --ok

[Eric Wieser]

Changing induction_empty_optionₓ to take the Fintype argument in () instead of [] also works

[Eric Wieser]

I think this might be a bug in elab_as_eliminator

[Eric Wieser]

With () brackets the induction tactic also works:

/- simplified from `Fintype.induction_empty_option`. -/
@[elab_as_elim]
theorem induction_empty_optionₓ {P : ∀ (α : Type u) [Fintype α], Prop}
    (H : ∀ α [Fintype α], P α)
    {α : Type u}
    (h : Fintype α) : P α := by
  exact H α

example
    {P : ∀ (α : Type u) [Fintype α], Prop}
    (H : ∀ α [Fintype α], P α)
    (α : Type u)
    [Fintype α] : P α := by
      induction ‹Fintype α› using induction_empty_optionₓ
      apply H

[Jon Eugster]

The second suggestion also works in the full PR, thx!

I still wonder if there is an explanation why the instance inference would create seemingly absurd terms like @P α (H : Fintype β)