not-lower instance priority in number field

Stream: mathlib4

[Kevin Buzzard]

I just wrote

variable (K L : Type*) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [FiniteDimensional K L] -- can be deduced

thinking "we'd never have that finite-dimensionality instance, it looks really scary". I then thought "may as well check" and indeed we do have docs#NumberField.instFiniteDimensional . And the code is

-- See note [lower instance priority]
attribute [instance] NumberField.to_charZero NumberField.to_finiteDimensional

protected theorem isAlgebraic [NumberField K] : Algebra.IsAlgebraic ℚ K :=
  Algebra.IsAlgebraic.of_finite _ _

instance [NumberField K] [NumberField L] [Algebra K L] : FiniteDimensional K L :=
  Module.Finite.of_restrictScalars_finite ℚ K L

so clearly some people thought something was scary at some point with this note, but nothing has a lower instance priority at all ?!

[Eric Wieser]

It's possible this was lost in the port