"omit" doesn't omit typeclass assumptions

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Once a typeclass variable has been declared, it's impossible to get rid of it. The omit keyword doesn't actually omit it from following declarations; it only cancels the effect of include so it isn't always included, but it is still "optionally" included.

This makes it very difficult to "refine" a typeclass variable from a general typeclass to a more specific one that extends it. Instead one ends up with multiple, unrelated instances of the base class on the same type, which can lead to craziness (of a sort that is extremely confusing for novices in particular).

Context

This is a de-mathlibized version of an issue that arose in a discussion about typeclass variables in mathlib on zulip here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Multiple.20overlapping.20typeclasses

Steps to Reproduce

MWE:

class AddComm (R : Type) extends Add R where
  add_comm : ∀ a b : R, a + b = b + a

variable (R : Type) [Add R]

omit [Add R] in
variable [AddComm R] in

example (a b : R) : a + b = b + a := by
  exact AddComm.add_comm a b -- fails, wrong "+"

Expected behavior:

It would be nice if the omit declaration actually omitted the Add R typeclass from the example, so the statement was elaborated with only the AddComm R instance in scope. (Alternatively, rather than changing omit we could have a new keyword omit! or forget.)

Actual behavior:

The elaborator has two instances of Add on R to choose from – the one from the explicitly declared Add R variable, and the one that's the base class of the AddComm R variable – and the one it chooses is the one we tried to omit. Hence we get a type mismatch error

type mismatch
  AddComm.add_comm a b
has type
  @HAdd.hAdd R R R (@instHAdd R AddComm.toAdd) a b = b + a : Prop
but is expected to have type
  @HAdd.hAdd R R R (@instHAdd R inst✝¹) a b = b + a : Prop

where inst✝¹ is the Add R instance.

Versions

Tested with live.lean-lang.org, version "4.12.0-nightly-2024-10-01"

Start by running the minimal AddComm example against the reported Lean nightly version and compare the expected and actual elaboration. Investigate the behavior of omit and the elaborator's handling of inherited typeclass instances; done means the example uses only the AddComm R instance, or the issue's proposed alternative is clearly resolved.