# Zulip Chat Archive

## Stream: general

### Topic: Problems with notation overloading

#### Tomas Skrivan (Oct 01 2020 at 22:17):

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 (Oct 01 2020 at 22:32):

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

#### Tomas Skrivan (Oct 01 2020 at 22:41):

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

#### Reid Barton (Oct 01 2020 at 22:43):

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 (Oct 01 2020 at 22:46):

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 (Oct 01 2020 at 22:53):

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 (Oct 01 2020 at 22:55):

Is this `[ ]`

notation also overloaded?

#### Tomas Skrivan (Oct 01 2020 at 22:57):

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 (Oct 01 2020 at 22:59):

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 (Oct 01 2020 at 23:16):

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

#### Eric Wieser (Oct 01 2020 at 23:18):

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

#### Reid Barton (Oct 01 2020 at 23:32):

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 (Oct 01 2020 at 23:37):

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

#### Reid Barton (Oct 01 2020 at 23:41):

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

#### Sebastian Ullrich (Oct 02 2020 at 08:32):

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

Last updated: May 08 2021 at 19:11 UTC