Problems with notation overloading

Stream: general

[Tomas Skrivan]

I'm having problems with overloading a notation.

Everything works fine without overloading

notation x | y := pair[x][y]
variables {X Y Z : type} {x : X} {y : Y} {z : Z}
#check (x|y)
| pair[x][y] : Expr (X × Y)

However, adding an overload for the notation produces:

notation x | y := pair[x][y]
notation x | y := ⟦pair⟧[x][y]
variables {X Y Z : type} {x : X} {y : Y} {z : Z}
#check (x|y)
| (λ (x_1 : Expr X), pair[x_1].app) x y : Expr (X × Y)

Why do I get (λ (x_1 : Expr X), pair[x_1].app) x y : Expr (X × Y) instead of pair[x][y] ?

This actually causes a failure of overload resolution for (x|y)|x with an error:

error for λ (x_1 : _), [choice Expr.app' Expr.app] ([choice Expr.app' Expr.app] (quotient.mk pair) x_1)
type mismatch at application
  (λ (x_1 : quotient ?m_1.setoid), Expr.app' ⟦pair⟧[x_1]) ((λ (x_1 : Expr X), pair[x_1].app) x y)
term
  (λ (x_1 : Expr X), pair[x_1].app) x y
has type
  Expr (X × Y)
but is expected to have type
  quotient ?m_1.setoid

error for λ (x_1 : _), [choice Expr.app' Expr.app] ([choice Expr.app' Expr.app] pair x_1)
type mismatch at application
  (λ (x_1 : Expr (X × Y)), pair[x_1].app) ((λ (x_1 : Expr X), pair[x_1].app) x y) x
term
  x
has type
  ↥X
but is expected to have type
  Expr ?m_1[(λ (x_1 : Expr X), pair[x_1].app) x y]

[Reid Barton]

I wouldn't recommend overloading notation, except possibly in cases where it's really obvious to Lean which variant is needed.

[Tomas Skrivan]

Not sure what is 'really obvious' but in my case those overloads either act on a type or on its quotient.

[Reid Barton]

Well, for example, since I don't know what pair[x] means, I couldn't tell which variant is expected in your #check example, except from context

[Reid Barton]

We don't really use overloaded notation, instead we use type classes. If you want to "overload function application" then you can create an instance of has_coe_to_fun.

[Tomas Skrivan]

I will have look at has_coe_to_fun.

Anyway, #check pair[x] gives pair[x] : Expr (?M_1 ⟶ X × ?M_1), it pairs with x.

[Reid Barton]

Is this [ ] notation also overloaded?

[Tomas Skrivan]

Yes it is. I'm working with a type representing expressions

inductive Expr : type → Type
| sym (T : type) (name : string) : Expr T
| app {X Y : type} : Expr (X ⟶ Y) → Expr X → Expr Y

notation f [ x ] := Expr.app f x

[Tomas Skrivan]

And it is also defined on the quotient

def Expr.app' {X Y : type} := quotient.lift₂ (λ f  x, ⟦f[x]⟧)
notation f [ x ] := Expr.app' f x

[Reid Barton]

Yeah, so in this situation I would not trust Lean to pick the correct overload variants.

[Eric Wieser]

So lean actually does support overloading without the usual approach of typeclasses? Is this documented anywhere?

[Reid Barton]

I'm pretty sure Lean makes some nonzero effort to select the right notation based on the available type information--it definitely does this for disambiguating the same name in several different open namespaces, which is a feature used mainly without being aware of it.

[Eric Wieser]

So functions can be overloaded by declaring them in different namespaces then opening both?

[Reid Barton]

Yes, or more commonly when a function in an opened namespace has the same name as one in the root namespace

[Sebastian Ullrich]

Overloaded names and notations are simply tried in turn, after which the unique successful interpretation is taken if any