Denumerable Rat vs Encodable Rat

Stream: mathlib4

[Alex Meiburg]

There's both a Denumerable Rat instance https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Rat/Denumerable.lean and an Encodable Rat instance https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Rat/Encodable.lean

They are functionally basically identical, except that you can also derive an Encodable instance from a Denumerable instance; and in fact the proof of Denumerable re-builds an (almost exactly same) Encodable instance in it. Is there any reason these two shouldn't just be merged into the one Denumerable instance, possibly with a short-circuit for the Encodable?

[Yaël Dillies]

I remember looking at this two years ago and deciding it was too hard to fix, but I don't remember what the problem was anymore :thinking: Maybe an import issue?