Priority of `coe_sort_trans`

Stream: general

[Anne Baanen]

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]

Idem for docs#coe_fn_trans

[Floris van Doorn]

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]

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.