Instance priority only has local effect

Stream: lean4

[Jovan Gerbscheid]

I always assumed that type class resolution finds the instance where the smallest priority of all used instances is maximal. However this is not true:

class A
class B
instance normal_instance : A where
instance alternative_instance [B] : A where
instance (priority := low) should_really_not_be_used_instance : B where

#synth A -- alternative_instance

Is this an oversight or intended behaviour?

[Matthew Ballard]

Priority is only local to that node. It doesn’t influence things further up the branch. I would say it’s a known consequence of the design.