# Zulip Chat Archive

## Stream: general

### Topic: Priority of `coe_sort_trans`

#### Anne Baanen (Aug 02 2021 at 14:55):

It seems to me the priority of docs#coe_sort_trans should be lower than all other docs#has_coe_to_sort instances, in particular lower than docs#set_like.has_coe_to_sort.

I discovered this issue when I got a timeout in the following code:

```
import ring_theory.fractional_ideal
example {R S m : Type*} [comm_semiring R] [integral_domain S] [algebra R S] {I : ideal S} :
basis m R I := sorry -- timeout at `I`, recursively tries coercing `I` to a fractional ideal in the ideal quotient of adjoining a root to the polynomials over ... of S
```

My proposed fix:

```
import ring_theory.fractional_ideal
local attribute [instance, priority 1] coe_sort_trans
local attribute [instance, priority 2] set_like.has_coe_to_sort
example {R S m : Type*} [comm_semiring R] [integral_domain S] [algebra R S] {I : ideal S} :
basis m R I := sorry -- nearly instant
end
```

#### Anne Baanen (Aug 02 2021 at 15:01):

Idem for docs#coe_fn_trans

#### Floris van Doorn (Aug 02 2021 at 20:51):

I'm worried that lowering these priorities is just a patch.

If we have a type-class problem that is supposed to fail (which we often have), then the combination of these instances will still loop.

docs#fractional_ideal.coe_to_fractional_ideal looks like a pretty dangerous instance, since neither `S`

nor `P`

can be inferred from the LHS.

It doesn't quite fall in the description of https://leanprover-community.github.io/mathlib_docs/notes.html#use%20has_coe_t, but maybe this loop is solved if we make `fractional_ideal.coe_to_fractional_ideal`

an `has_coe_t`

?

I'm not against lowering the priorities you mentioned, I think that we should *also* remove this loop.

#### Anne Baanen (Aug 03 2021 at 10:19):

Looks like turning it into a `coe_t`

speeds stuff up quite a bit, regardless of whether we get into a loop, so here's #8529.

Last updated: Aug 03 2023 at 10:10 UTC