Quotient.induction can infer motive but fails on application

Stream: new members

[Dexin Zhang]

I encountered a strange "application type mismatch" error:

import Mathlib.Data.Quot

variable {α : Type u} {s : Setoid α} {p : Quotient s → Prop} {q : Quotient s → Prop}

-- OK
example : (∃ x, p x) → ∃ (x : α), p ⟦x⟧
  | ⟨x, h⟩ => Quotient.inductionOn x (fun x h => ⟨x, h⟩) h

-- application type mismatch
--   Quotient.inductionOn (motive := fun x => p x → q x → ∃ x, p ⟦x⟧ ∧ q ⟦x⟧) x (fun x h₁ h₂ => Exists.intro x ⟨h₁, h₂⟩) h₂
-- argument has type
--   q x
-- but function has type
--   p x → q x → ∃ x, p ⟦x⟧ ∧ q ⟦x⟧
example : (∃ (x : Quotient s), p x ∧ q x) → ∃ (x : α), p ⟦x⟧ ∧ q ⟦x⟧
  | ⟨x, h₁, h₂⟩ => Quotient.inductionOn x (fun x h₁ h₂ => ⟨x, h₁, h₂⟩) h₁ h₂

Looks like Quotient.inductionOn successfully infers the motive, but strangely "forget" the h₁ argument. Is that an internal bug?