Zulip Chat Archive

Stream: general

Topic: type class inference after colon


view this post on Zulip Kevin Buzzard (Mar 11 2018 at 18:34):

In example (α : Type) [comm_ring α] : ∀ x y z : α, x*(y+z)=x*y+x*z := mul_add, type class inference enables us to use mul_add. Is it possible to move the colon to the left of the alpha though? Not that I need to, it's just an idle question. If I try example : ∀ (α : Type) [comm_ring α], ∀ x y z : α, x*(y+z)=x*y+x*z := mul_add then Lean complains about not being able to find has_add alpha etc.

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 18:37):

A related question: is there ever a difference between [comm_ring alpha] and [H : comm_ring alpha] in terms of the type class inference system? Or between [comm_ring alpha] and [_inst_1 : comm_ring alpha]?

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 18:47):

And another type class subtlety. With

structure foo (α : Type) :=
(bar : α)
(baz : α → α)

#check @foo.bar
#check @foo.baz

both foo.bar and foo.baz are Π {α : Type},.... But if I change the structure to a class, foo.bar (but not foo.baz) magically changes to Π (α : Type)... (no longer implicit). It didn't have to be that way, right? That is presumably some design decision?

view this post on Zulip Mario Carneiro (Mar 11 2018 at 19:36):

The first issue is #1920. You have to write example : ∀ (α : Type) [comm_ring α], ∀ x y z : α, by exactI x*(y+z)=x*y+x*z if you want to use any typeclass args right of the colon

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 19:37):

Aah -- this is exactly the change that caused you so much trouble!

view this post on Zulip Mario Carneiro (Mar 11 2018 at 19:39):

The second issue is just the usual analysis of when to make arguments implicit. It's a design decision, of course, but it is reasonably predictable and well motivated


Last updated: May 16 2021 at 20:13 UTC