Finding reduced typeclass instances

Stream: lean4

[Parth Shastri]

In the following example, typeclass resolution is able to synthesize the instance when the type directly matches the instance, but not when it only reduces to the instance type.

class Foo (n : Nat)
instance : Foo (no_index (nat_lit 2)) where
#synth Foo 2 -- works
#synth Foo [(), ()].length -- failed to synthesize

Is there any way to get this to work?

[Jannis Limperg]

Typeclass synthesis only unfolds reducible definitions (abbrev or @[reducible]). Additionally, the indexing data structures assume, iiuc, that only non-recursive definitions are reducible. These are pretty fundamental restrictions, so you probably won't be able to make your example work as-is.

[Parth Shastri]

I was trying to implement a coercion from lists to fintuples.

instance : CoeDep (List α) l (Fin (no_index l.length) → α) where
  coe := l.get

I guess I'll stick to using a macro.

I'm not sure if this is related or not, but I ran into another issue when defining a different coercion from lists to fintuples.

instance : Coe (List α) ((n : Nat) × (Fin n → α)) where
  coe l := ⟨l.length, l.get⟩

#check ([0] : (n : Nat) × (Fin n → Nat)) -- works
#check ([] : (n : Nat) × (Fin n → Nat)) -- type mismatch

[Jannis Limperg]

Yeah, I don't see immediately how you could get the desired coercion. Bit unfortunate. If we ever get the ability to run custom code during typeclass synthesis, this would become possible.

For your second issue, the problem seems to be that [] has type List ?α where ?α is undetermined. In this case, the elaborator apparently doesn't apply coercions. You can write (([] : List Nat) : (n : Nat) × (Fin n → Nat)) if you like type salad.

[Gabriel Ebner]

It's technically possible to make the function coercion work:

instance : CoeFun (List α) (Fin ·.length → α) where
  coe l := l.get

#check fun i : Fin 0 => [] i
#check ([] : Fin 0 → Nat)

[Gabriel Ebner]

But I would really strongly advise you not to add any of these as coercions.