remove all instances with variable domain

Stream: general

[Floris van Doorn]

We need to remove all has_coe instances with variable domain, like:

#print uniform_space.completion.has_coe
#print localization.has_coe
#print filter.filter_product.coe_filterprod

All these instances go from a variable to a specific type, e.g. has_coe α (uniform_space.completion α). The problem is, that together with

coe_trans [_inst_1 : has_coe a b] [_inst_2 : has_coe_t b c] : has_coe_t a c

these instances will just loop forever. If coe_trans applies, then all of these instances always apply for _inst_1 and then _inst_2 can again be inferred using coe_trans.

Consider the following, when importing all of mathlib:

set_option class.instance_max_depth 10
def foo : has_coe_t name nat := by apply_instance

This will timeout with instance max depth (it is expected to fail).

The actual problem I ran into was:

def foo : list name := [`x]

Since the notation [ ... ] is overloaded (see #1502), it then tries to find an instance (vector3 name 1) (list name), which fails. The total elaboration time took 49s(!) for me.

Here is another example:

constant A : Type
constant B : Type
constant C : Type
@[priority 999] instance : has_coe A B := sorry
@[priority 999] instance : has_coe B C := sorry
def foo : has_coe_t A C :=
by apply_instance -- fails

The priority 999 is just to mimic any instance that was declared before filter.filter_product.coe_filterprod. Since type-class inference reaches an infinite loop, it fails, while it it expected to succeed.

[Floris van Doorn]

Here is the full list of instances which will have to be removed:

uniform_space.completion.has_coe : Π (α : Type u_1) [_inst_1 : uniform_space α], has_coe α (uniform_space.completion α)
localization.has_coe : Π {α : Type u} [_inst_1 : comm_ring α] {S : set α} [_inst_2 : is_submonoid S], has_coe α (localization α S)
filter.filter_product.coe_filterprod : Π {α : Type u} {β : Type v} {φ : filter α}, has_coe β (filter.filterprod β φ)
computation.has_coe : Π {α : Type u}, has_coe α (computation α)
quotient_group.has_coe : Π {α : Type u_1} [_inst_1 : group α] {s : set α} [_inst_2 : is_subgroup s], has_coe α (quotient_group.quotient s)

[Rob Lewis]

Yikes. Good find. I hope these won't be too painful to remove.

[Floris van Doorn]

I'm not sure if we should make them localized instances, or remove them altogether.

[Rob Lewis]

If we make them localized instances then some theorems will be stated with the coercions, and could end up being inconvenient to use without the locale open. We probably don't want to force people to open locales with dangerous instances.

[Floris van Doorn]

That's fair.

[Patrick Massot]

@Daniel Selsam Did you see that thread? Will we be able to keep those instances in Lean 4?

[Patrick Massot]

Getting rid of those instances really sounds bad from a mathematical point of view.

[Mario Carneiro]

The standard practice for these is to make them has_coe_t

[Daniel Selsam]

@Patrick Massot Yes, in addition to diamonds, cycles will be handled correctly in Lean4. You don't even need the has_coe_t anymore:

https://github.com/dselsam/lean4/blob/tabled_typeclasses/tests/lean/run/typeclass_coerce.lean#L16-L17

These four tests take ~10ms in total:

https://github.com/dselsam/lean4/blob/tabled_typeclasses/tests/lean/run/typeclass_coerce.lean#L49-L77

[Patrick Massot]

Thanks. Maybe I should try to learn how install Lean 4. Is this documented anywhere?

[Daniel Selsam]

@Patrick Massot Same instructions as Lean3. Note: Lean4 is still a long way from being ready for use. The typeclass procedure hasn't even been merged yet.

[Floris van Doorn]

The standard practice for these is to make them has_coe_t

Oh yes, thanks for reminding us. That is the correct way to go.

@Patrick Massot: this will mean in practice is that the coercion α -> quotient_group.quotient s will still work, but you cannot go further (e.g. it will not go from α to a quotient of a quotient of α).

[Patrick Massot]

It sounds fine.

[Yaël Dillies]

Why is this library note in file#group_theory/coset?