Replacing Typeclass Instances with Other Equivalent Ones?

Stream: Is there code for X?

[Qiyuan Zhao]

I want to write a metaprogram that replaces all Decidable instances in a term that are generated by Classical.propDecidable with those that are computable by inferring instances. This metaprogram should also return a proof showing the equivalence between the before/after terms (this should be feasible since any two Decidable instances are propositionally equal).

For example, assume this metaprogram can be used as a term elaborator replace%, then ideally Lean should not complain that b cannot be compiled.

variable (p : Nat → Prop)

open Classical in
noncomputable def a (n : Nat) : Bool := if p n then true else false

variable [DecidablePred p]

def b (n : Nat) : Bool := replace% (a n)

Is there any existing code doing typeclass instance replacement like this? Thanks in advance!