Zulip Chat Archive

Stream: lean4

Topic: Finding reduced typeclass instances


Parth Shastri (Nov 15 2022 at 23:57):

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 (Nov 16 2022 at 00:04):

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 (Nov 16 2022 at 00:11):

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 (Nov 16 2022 at 10:41):

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 (Nov 16 2022 at 17:35):

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 (Nov 16 2022 at 17:35):

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


Last updated: Dec 20 2023 at 11:08 UTC