Coercion not working

Stream: lean4

[James Randolf]

Hi, I'm trying to define a coercion from ∃x : T, P x to {x : T // P x}. Is there something I'm doing wrong?

noncomputable instance {T : Type} {P : T → Prop} : Coe (∃x : T, P x) {x : T // P x} := ⟨Classical.indefiniteDescription _⟩
def a : ∃x : Nat, True := ⟨0, True.intro⟩
noncomputable def b : Nat := Subtype.val (Classical.indefiniteDescription _ a) -- works
noncomputable def c : Nat := Subtype.val a -- doesn't work (it should be applying the coercion here)

[Kyle Miller]

Coe by itself isn't allowed to solve for the implicit arguments in Subtype.val (not sure if it's one or both of them). Both of these work:

noncomputable def c : Nat := Subtype.val (a : {x : Nat // True})
noncomputable def c' : Nat := Subtype.val (p := fun (_ : Nat) => True) a

[Kyle Miller]

I checked that CoeHead and CoeOut don't work here either