Typeclass synthesis fails with an `abbrev` involved

Stream: lean4

[Alex Keizer]

Does someone have an idea of what is going on with the following MWE?
If I define FooWithUnit as an abbrev, and have an instance for Class (FooWithUnit FooNat), but typeclass synthesis for exactly that expression fails.
On the other hand, if I change FooWithUnit to be a def, everything works

structure Foo where
  (α β : Type)

class Class (w : Foo) where

abbrev FooNat : Foo := ⟨Nat, Nat⟩

/-- A function `Foo → Foo` that changes `Foo.β`, but takes `Foo.α` from the argument -/
abbrev FooWithUnit (w : Foo) : Foo where
  α := w.α
  β := Unit

instance inst (w : Foo) : Class (FooWithUnit w) := ⟨⟩

#check (inst FooNat : Class (FooWithUnit FooNat)) -- this typechecks
#synth Class (FooWithUnit FooNat)                 -- yet, we get `failed to synthesize`

-- Making `FooWithUnit` a `def` instead of an `abbrev` somehow fixes the issue
def FooWithUnit' (w : Foo) : Foo where
  α := w.α
  β := Unit

instance inst' (w : Foo) : Class (FooWithUnit' w) := ⟨⟩

#check (inst' FooNat : Class (FooWithUnit' FooNat))
#synth Class (FooWithUnit' FooNat) -- this now works

[Eric Wieser]

I think abbrev is working as intended; the behavior is the same if you inline everything:

structure Foo where
  (α β : Type)

class Class (w : Foo) where

instance inst (w : Foo) : Class ({ α := w.α, β := Unit }) := ⟨⟩

#check inst ⟨Nat, Nat⟩
#synth Class ({ α := (⟨Nat, Nat⟩ : Foo).α, β := Unit }) --fails

[Alex Keizer]

Ah, right. thanks for the info! I understand why it's happening now, but it's certainly surprising when having an instance for exactly the thing being synthesized doesn't work

[Matthew Ballard]

Can you share the underlying issue? I assume it is the discrimination tree indexing because synthesis isn't crashing and there are no instances found when tracing.

[Alex Keizer]

What I assume is happening, is that when an instance is defined, the type is reduced with reducible transparancy, and the result of that is used in the discrimination tree. In my example, this would be Class { α := Wrapper.α w, β := Unit }. Since w is a variable at this point, no more reduction is possible. In particular, I assume the discrimnation tree indexes the presence of the Wrapper.α projection.
However, at the point of synthesis, the value of w is known, namely, I'm trying to synthesize Class (FooWithUnit FooNat). I assume this, too, gets reduced, and since FooNat is an abbrev as well, reducing this fully gives Class { α := Nat, β := Unit }, and I assume that this is what is actually being synthesized. Notice the lack of Wrapper.α in the reduced form, which I'd guess is what causes the synthesis to fail.

Notice my liberal use of "assume". I don't actually know how typeclass synthesis is implemented, this is just my mental model that would support this behaviour.

[Matthew Ballard]

Sounds reasonable.

[Matthew Ballard]

Making Foo a class also makes the #synth work (because projections from classes are not reducible whereas those from structures are)

[Matthew Ballard]

In this example, the keys for FooWithUnit FooNat are #[Foo.mk, Nat, PUnit] and the keys for inst are #[Class, Foo.mk, Foo.0, *, PUnit]

The keys for FooWithUnit' FooNat are #[FooWithUnit', Foo.mk, Nat, Nat] and for inst' are #[Class, FooWithUnit', *]

[Matthew Ballard]

You can do

instance inst (w : Foo) : Class no_index (FooWithUnit w) := ⟨⟩

to turn the keys into #[Class, *] and match with anything asking for a Class

[Matthew Ballard]

Is the matching for the keys just equal arrays up to skipping .stars?

[Alex Keizer]

Matthew Ballard said:

Is the matching for the keys just equal arrays up to skipping .stars?

Is this question for me? I'm not sure.

Anyways, thanks for the in-depth investigation! I somehow keep forgetting about no_index and how it can fix issues related to discrimination trees

[Matthew Ballard]

That was in general but I found a post by Mario which gave me the summary