Wrong Elaborator

Stream: general

[Adalynn]

axiom Left: Type
axiom Right: Type
instance: Coe Left Right := sorry
instance: HasSubset Right := sorry
variable (a: Left)
variable (B: Right)
#check a⊆B

Hey, I just noticed that the above MRE doesn't work since I'm getting an error that it can't convert B of type Right to type Left. Could this be because it has the wrong elaborator? Sorry if this isn't the right place to put it.

[Arthur Adjedj]

Putting an explicit coercion on a solves it:

axiom Left: Type
axiom Right: Type
instance: Coe Left Right := sorry
instance: HasSubset Right := sorry
variable (a: Left)
variable (B: Right)
#check ↑a ⊆ B --works

[Adalynn]

Oh yeah I know that, it just... feels as if the elaborator should be the same as =? For = it automatically coes.

[Kyle Miller]

You are correct that a⊆B has no special support. This one is tricky because generally it's for types like Set X or Finset X that are functorial, where you might want something that can compute a target functor to coerce everything to. Maybe a target carrier type too.

You could try your luck with the binrel% elaborator though. It does make your example work.

local macro_rules | `($x ⊆ $y) => `(binrel% HasSubset.Subset $x $y)

#check a ⊆ B
-- Coe.coe a ⊆ B : Prop

[Kyle Miller]

(Relately, mathlib has an fbinop% elaborator to support being able to create products of set-like objects with ×ˢ notation.)

[Adalynn]

Oh, that should work well! I had a workaround (literally just overloading the notation, admittedly not the best solution), but this feels more like the intended/correct way to do it that won't run into problems down the line. Thanks!

[Kyle Miller]

This isn't great though because binrel% is meant to be for arithmetic binary relations. It won't interact with intersections and unions for example, since these are not using the binop% elaborator.

[Adalynn]

Ah, yeah. I'll play it by ear: but I came from lean 3 and I just ditched preludes when I worked on my from-scratch ZFC file I work on when I'm bored. So heterogeneous intersections will probably have to be using overloading.