Fin DecidableEq diamond

Stream: mathlib4

[Yaël Dillies]

There's currently a diamond on DecidableEq (Fin n). One comes from Core (docs#instDecidableEqFin), the other one comes from LinearOrder (Fin n) (docs#instDecidableEq). What should we do?

import Mathlib.Data.Fin.Basic

example (n : ℕ) : instDecidableEqFin n = instDecidableEq := rfl -- fails

[Eric Rodriguez]

Isn't the decidable eq on linear orders free to set for this reason?

[Eric Rodriguez]

@loogle LinearOrder (Fin _)

[loogle]

:search: Fin.instLinearOrderFin

[Yaël Dillies]

Yeah sure, but both decidability instances do "the same thing" by reducing x = y for x y : Fin n to x.val = y.val. They just do it slightly differently.

[Eric Wieser]

I think the problem here is docs#LinearOrder.liftWithOrd

[Eric Wieser]

That should be taking DecidableEq as an argument, probably

[Eric Wieser]

Though changing the core implementation to be defeq by coincidence seems pretty reasonable too

[Eric Rodriguez]

I would agree that liftWithOrd should be fixed

[Eric Wieser]

I suspect the default implementation there is going to be the right one for everything except weird instances in core