omitting a type-class argument doesn't always work

Stream: lean4

[Floris van Doorn]

I believe Core Lean has improved the possibility of omitting section variables a lot, but a PhD student in Bonn - @Sven Manthe - noticed one place where the current behavior isn't ideal yet.

Consider the following code:

import Mathlib.Algebra.Group.Basic

variable {G : Type*} [Group G] (x : G)

-- stuff about groups

variable [CommGroup G]

omit [Group G] in
lemma foo : x * x = x * x := by rfl -- error

This errors, because Lean uses the [Group G] instance to interpret what * means, and then complains that it cannot omit that variable. Ideally, the [Group G] was never available to begin with, and type-class inference would just find the [CommGroup G] instance instead.
(Note: this is a pattern we might not want in Mathlib, that's a separate discussion)

[Floris van Doorn]

Here is an artificial, Mathlib-free MWE:

section
variable {G : Type _} [Inhabited G]

theorem foo : Classical.choice (α := G) (by infer_instance) = -- works fine
    Classical.choice (α := G) (by infer_instance) := by rfl

end

variable {G : Type _} [Nonempty G] [Inhabited G]

omit [Nonempty G] in
theorem bar : Classical.choice (α := G) (by infer_instance) =
    Classical.choice (α := G) (by infer_instance) := by rfl
-- Result: error. Expected: behaves like theorem `foo`.

[Floris van Doorn]

Is a RFC welcome for this, or is this a known limitation of the current system?

[Sebastian Ullrich]

I'm not completely sure if there is a previous bug report about this, but if you can't find one, feel free to open one

[Floris van Doorn]

I thought I had searched, but apparently not careful enough. This is lean#5595

[Kenny Lau]

that sounds like an elaboration order issue?