Zulip Chat Archive

Stream: general

Topic: remove all instances with variable domain

Floris van Doorn (Oct 01 2019 at 18:31):

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 (Oct 01 2019 at 18:36):

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 (Oct 01 2019 at 19:10):

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

Floris van Doorn (Oct 01 2019 at 19:14):

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

Rob Lewis (Oct 01 2019 at 19:22):

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 (Oct 01 2019 at 19:25):

That's fair.

Patrick Massot (Oct 01 2019 at 19:41):

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

Patrick Massot (Oct 01 2019 at 19:41):

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

Mario Carneiro (Oct 01 2019 at 20:12):

The standard practice for these is to make them has_coe_t

Daniel Selsam (Oct 01 2019 at 21:53):

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


These four tests take ~10ms in total:


Patrick Massot (Oct 01 2019 at 22:16):

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

Daniel Selsam (Oct 01 2019 at 22:27):

@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 (Oct 01 2019 at 22:57):

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 (Oct 02 2019 at 19:55):

It sounds fine.

Yaël Dillies (Dec 14 2022 at 16:09):

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

Last updated: Aug 03 2023 at 10:10 UTC