Controlling `unfold_projs`

The unfold_projs tactic takes all class projection functions and tries to reduce them. For example, in the following,

example : default = 0 := by
  unfold_projs
  -- ⊢ Nat.zero = 0

recall that default is the projection Inhabited.default {α : Type} [self : Inhabited α] : α, and so the tactic sees @default ℕ instInhabitedNat and reduces this projection by unfolding instInhabitedNat.

The tactic is very simple. The implementation is less than 20 lines. It transform the entire expression by trying to apply the core function unfoldProjInst? to each subexpression.

However, this tactic unfolds projections indiscriminately. It would be nice to be able to control the unfolding.

Suggested features:

• unfold_projs +singlePass could do one level of unfolding. This could be implemented by having it use return .continue (← instantiateMVars node') instead of return .visit (← instantiateMVars node') when that flag is set.
• unfold_projs could take a list of names of projections to unfold. For example, unfold_projs [default] could have it unfold only instances of Inhabited.default. Maybe also unfold_projs [Inhabited] would unfold all projections associated to Inhabited. I imagine that to implement this, it would be best to copy the code of unfoldProjInst?, making a new version that takes a (p : ProjectionFunctionInfo -> Bool) predicate.
• One might consider a more complicated version where unfold_projs takes expressions. For example, unfold_projs [Inhabited Nat] might only unfold projections for the specified parameters. Or, e.g., unfold_projs [HAdd Nat, Add Nat], to make sure only Nat additions are unfolded. The modified unfoldProjInst? should just need to have a (p : ProjectionFunctionInfo -> MetaM Bool) predicate for this.

Start in Mathlib/Tactic/DefEqTransformations.lean at the unfold_projs implementation and inspect the core unfoldProjInst? function. Determine which of the proposed controls is in scope, then define completion as unfold_projs honoring that control without changing its existing behavior; no test file is mentioned in the issue.