multiple solutions for typeclass search

Stream: general

[Oliver Nash]

I'm wondering how evil, if at all, the following pattern is:

class foo := (x : ℕ)

def bar [foo] : ℕ := foo.x

def baz (f : foo) := bar

instance foo_inst : foo := ⟨37⟩

lemma bar_val : bar = 37 := rfl

lemma baz_val (f : foo) : baz f = f.x := rfl

The point is that baz_val is true only because typeclass search first looks for the nearby argument f before it heads off to look for registered instances. So is the correctness of this lemma due only to an implementation detail of typeclass search, or is this a feature which it is valid to exploit?