finset -> set coercion

Stream: general

[Kevin Buzzard]

It's really nice to get back into doing some Lean. As my confidence grows I now know more about what should work, and am hence more confident about asking questions when I see discrepencies. What is going on here?

import data.finset

example (x : ℕ) : ℤ := x -- no ↑ needed

example (α : Type) (s : finset α) : set α := ↑s -- ↑ needed

I usually don't need the ↑ when coercing. I think Chris once told me that this is something to do with has_coe_t or has_lift or perhaps another one of these other inscrutible typeclasses whose names I don't know. Is this actually a problem? If so, can it be fixed? Or is it there by design?

[Gabriel Ebner]

Let me quote init/coe.lean: https://github.com/leanprover-community/lean/blob/master/library/init/coe.lean

The elaborator tries to insert coercions automatically.
Only instances of has_coe type class are considered in the process.
Lean also provides a "lifting" operator: ↑a.
It uses all instances of has_lift type class.
Every has_coe instance is also a has_lift instance.
We recommend users only use has_coe for coercions that do not produce a lot
of ambiguity.
All coercions and lifts can be identified with the constant coe.
We use the has_coe_to_fun type class for encoding coercions from
a type to a function space.
We use the has_coe_to_sort type class for encoding coercions from
a type to a sort.

[Patrick Massot]

I guess Kevin's question is: why is this particular coercion a has_lift but not a has_coe.

[Patrick Massot]

This is probably worth at least a comment in finset.lean, probably in the module docstring.

[Kevin Buzzard]

My question is whether it is by accident or by design.

[Gabriel Ebner]

git tells me we should blame @Mario Carneiro for this design choice, who added this line almost exactly two years ago.

[Mario Carneiro]

I think we could just get rid of has_lift, it is used exceedingly rarely

[Mario Carneiro]

I don't have any good reasons to share about why finset A -> set A is a has_lift

[Reid Barton]

I wonder whether it would cause issues with has_mem

[Reid Barton]

I still think it's weird that has_mem is not instead handled by coercions, but when I tried to fix it things got more complicated than I expected.

[Scott Morrison]

You mean coercing anything that you want to talk about membership to a set?

[Scott Morrison]

Is this something we can do incrementally without ripping out has_mem?

[Adam Topaz]

By currying, any has_mem instance is equivalent to a map to sets. Is there any example where there is a coersion to set and a has_mem instance which are not equivalent in this way?