Commit 2022-07-21 13:52 8983bec7

fix(data/set_like): coe_sort_trans should have low priority (#15489) In core Lean, coe_sort_trans is given default priority, meaning it takes precedence over set_like.has_coe_to_sort. As a consequence, sometimes a weird instance path was chosen, such as submodule R M → Module R → Type* rather than the direct path submodule R M → Type*, and I believe this can lead to diamonds (including weird universe levels), and in any case to weird defeq checks (which are made extra expensive by occurring in the type). In fact, there are quite a few has_coe_to_sort instances that would be useless since they are preceded by a has_coe, e.g. lie_ideal. Lowering the priority of coe_sort_trans below that of set_like.has_coe_to_sort should ensure we use the preferred inheritance path. We did the same thing for coe_fn_trans in fun_like/basic.lean. The consequence is that certain places that (ab)used the weird coercion paths will need to be slightly redefined to use the new path, basically inserting unification hints manually. Those paths were slightly fragile anyway so I don't think that's an important loss compared to the advantages of clarifying.