## Stream: maths

### Topic: subgroup set coercion

#### Patrick Massot (Sep 20 2019 at 12:46):

Here is a little type class failure experiment. In a Lean file, write:

import algebra.module

variables {A : Type*} [comm_ring A] (S : submodule ℤ A)

#check (↑S : set A)

#check (S : set A)


Both check succeed instantly. Now replace the first line by import ring_theory.algebra. The second check times out.

#### Patrick Massot (Sep 20 2019 at 12:47):

Next, create a dummy copy of ring_theory.algebra where the instance on https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/algebra.lean#L537 is only a local instance. Then both checks succeed, but the second one is very slow.

#### Patrick Massot (Sep 20 2019 at 12:48):

What should we do?

#### Mario Carneiro (Sep 20 2019 at 13:03):

what does the trace look like?

#### Patrick Massot (Sep 20 2019 at 13:04):

Do you mean the trace that works quickly, the one that works slowly or the one that fail?

#### Mario Carneiro (Sep 20 2019 at 13:05):

both, what is the difference?

#### Mario Carneiro (Sep 20 2019 at 13:06):

I am guessing that it has to do with has lift vs has coe

#### Patrick Massot (Sep 20 2019 at 13:09):

failure at https://pastebin.com/b9rgT8v7

#### Patrick Massot (Sep 20 2019 at 13:10):

fast success at https://pastebin.com/D804HUNU

#### Patrick Massot (Sep 20 2019 at 13:11):

Note how the lovely successful one still ends up in (message too long, truncated at 262144 characters)

After 3662 lines

#### Patrick Massot (Sep 20 2019 at 13:12):

And let me conjecture we have a little problem anyway.

#### Patrick Massot (Sep 20 2019 at 17:24):

So, any idea? Anyone?

#### Mario Carneiro (Sep 20 2019 at 18:14):

I think it's just a big instance problem

#### Mario Carneiro (Sep 20 2019 at 18:14):

and it has the usual exponential blowup stuff

#### Mario Carneiro (Sep 20 2019 at 18:16):

Note that the added import both significantly increases the number of available instances and also changes the type of the problem:
before:

has_coe_to_fun
(@submodule ℤ A
(@domain.to_ring ℤ
(@to_domain ℤ
(@linear_ordered_comm_ring.to_linear_ordered_ring ℤ
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ℤ
int.decidable_linear_ordered_comm_ring))))


after:

has_coe_to_fun
(@submodule ℤ A
(@domain.to_ring ℤ
(@to_domain ℤ
(@linear_ordered_comm_ring.to_linear_ordered_ring ℤ
(@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ℤ
int.decidable_linear_ordered_comm_ring))))
(@algebra.module ℤ A
(@nonzero_comm_ring.to_comm_ring ℤ (@euclidean_domain.to_nonzero_comm_ring ℤ int.euclidean_domain))
(@comm_ring.to_ring A _inst_1)
(@algebra_int A _inst_1)))


#### Mario Carneiro (Sep 20 2019 at 18:17):

I think it's probably not good that the proof of module ℤ A changes to this more complicated one after the import

#### Mario Carneiro (Sep 20 2019 at 18:18):

we really need to think about using instance priorities in a systematic and coherent way across the library

#### Patrick Massot (Sep 20 2019 at 18:18):

I don't even understand how we get a has_coe_to_fun search

#### Mario Carneiro (Sep 20 2019 at 18:19):

I think it's because set A is a function type

How weird

#### Mario Carneiro (Sep 20 2019 at 18:20):

I agree, I would have expected a has_coe

#### Johan Commelin (Sep 20 2019 at 18:32):

Should set be irreducible?

#### Johan Commelin (Sep 20 2019 at 18:32):

That would prevent a lot of defeqness that we currently depend on...

#### Johan Commelin (Sep 20 2019 at 18:32):

Doesn't sound good

#### Mario Carneiro (Sep 20 2019 at 18:42):

no, I think that's a bad idea

#### Mario Carneiro (Sep 20 2019 at 18:42):

it might work in principle but there isn't a strong argument for the distinction and we occasionally make use of the defeqness

#### Patrick Massot (Sep 20 2019 at 19:27):

At least this explains why using a (↑S : set A) works better than (S : set A)

Last updated: May 10 2021 at 08:14 UTC