"omit" doesn't omit typeclass assumptions

[loefflerd]

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"