Ambiguous ⋂₀ notation (ZFC) and binrel elaborators

Stream: mathlib4

[Eric Wieser]

In the following example, ⋂₀ seems to sometimes get confused about whether it's the docs#Set.sInter or docs#Class.sInter operator.

What's particularly weird is that this seems to only be a problem when inside =; it elaborates just fine with Eq or directly:

-- imported to create ambiguity; all the examples below want the `Set` version
import Mathlib.SetTheory.ZFC.Basic

-- works as a top-level term
def foo : (Set ℕ → Prop) → Set ℕ :=
  fun P => ⋂₀ setOf P

-- does not work in a equality
def IsFoo (foo : (Set ℕ → Prop) → Set ℕ) : Prop :=
  foo = fun P => ⋂₀ setOf P

-- unless we avoid using notation!
def IsFoo2 (foo : (Set ℕ → Prop) → Set ℕ) : Prop :=
  Eq foo (fun P => ⋂₀ setOf P)

[Eric Wieser]

Should Class.sInter be scoped to avoid this issue for users of import Mathlib who don't care about ZFC?

[Eric Wieser]

Or is there some way to fix this so that the ambiguity never arises?

[Violeta Hernández]

Eric Wieser said:

Should Class.sInter be scoped to avoid this issue for users of import Mathlib who don't care about ZFC?

This is a problem even for users who care about ZFC, since it also clashes with docs#ZFSet.sInter