Instance priorities

Stream: mathlib4

[Michael Stoll]

In Mathlib, many manually set instance priorities are around 100 (90, 95, 100, 110 or so). However, while looking at Data.Complex.Module, I noticed lines like

/- Register as an instance (with low priority) the fact that a complex vector space is also a real
vector space. -/
instance (priority := 900) Module.complexToReal (E : Type*) [AddCommGroup E] [Module ℂ E] :
    Module ℝ E :=

Playing around, it turns out that 1000 is the default priority:

class Foo (T : Type) where
  foo : Nat

instance Nat.foo : Foo Nat := ⟨37⟩

instance (priority := 999) Nat.foo' : Foo Nat := ⟨43⟩
-- with priority 1000: get `Nat.foo'` below

#synth Foo Nat -- `Nat.foo`

(Incidentally, this answers my question

The correct thing to try is Algebra.toSMul, but increasing its priority to 1000 does not seem to have any effect (I wonder why)

from another thread. I should have taken 1001 :smile:)

This raises the question whether the priorities around 100 are actually intended to be quite a bit lower than the default.

[Timo Carlin-Burns]

In Mathlib, 100 is the priority that we write by default for "blanket instances", i.e. those instances whose conclusions are a typeclass applied to free variables. Then my assumption is that these numbers around 100 are chosen to tweak priorities among these blanket instances

[Michael Stoll]

Then the next question is whether this "blanket instance" default priority is indeed applied to all such blanket instances (and also where this is documented...).

[Eric Wieser]

The reason everything is 100 is because in lean 3, 100 was autogenerated by the extends keyword

[Eric Wieser]

So priority 100 was chosen anywhere we want "the same low priority as the default low priority"

[Eric Wieser]

There is a lean4 issue that tracks restoring this behavior

[Matthew Ballard]

I also ran through possible instance priority changes to the default for parent projections and nothing was a clear W.

[Timo Carlin-Burns]

Blanket instance priority is documented here https://github.com/leanprover-community/mathlib4/blob/72721e375679fd7c7e0647775c028bcb9b91dedf/Mathlib/Algebra/HierarchyDesign.lean#L222