RatCast ℚ instance

Stream: mathlib4

[Thomas Murrills]

It seems like the instance of RatCast ℚ starts out as Field.toRatCast in Data.Rat.Basic, then becomes LinearOrderedField.toRatCast in Data.Rat.Order. Might this cause a problem at some point? (I noticed it while trying to locate a place for an instance that relies on RatCast ℚ.)

Also just wondering, why do we not have a special instance for RatCast ℚ that's just the identity? Is there a general pattern to which things we give special instances to and which instances we inherit from algebraic structure?

[Mario Carneiro]

The Field instance for Rat supplies the ratCast function and sets it to the identity