Typeclass search unfolds type aliases

Stream: general

[Eric Wieser]

Is this behavior deliberate?

import data.matrix.basic

class is_matrix {α : Sort*} (a : α)

variables {m n α : Type*}

instance inst (A : matrix m n α) : is_matrix A := ⟨⟩

example (x : m → m → α) : is_matrix x := by apply_instance  -- finds `inst` which is the wrong type

This comes up when trying to provide a reflected instance that is different for a type X and a synonym synonym X, as lean seems to just pick whichever one was declared last

[Gabriel Ebner]

That's because {α} is implicit in is_matrix, which means that the argument is unified with semireducible transparency. You get the same effect when searching for decidable (x = x).

[Eric Wieser]

So I guess we should probably change docs#reflected in core to take α as an explicit argument?

[Eric Wieser]

Does lean4 have any analog to reflected?

[Eric Wieser]

Eric Wieser said:

So I guess we should probably change docs#reflected in core to take α as an explicit argument?

Attempted in lean#734

[Eric Wieser]

Now passing CI. Thanks for the pointer, this does indeed fix the inference problem I had above.