Typeclass instantiation and extension

Stream: new members

[Kevin Sullivan]

When I'm instantiating a typeclass A that extends typeclasses B and C, and when I've already instantiated B and C, to what extent can I count on Lean finding and using the B and C instances so that I don't have to provide values for their field values when specifying those of A?

[Kevin Buzzard]

I think you always have to put ..(show B, by apply_instance) in, even if the instance is in the type class cache.

[Kevin Sullivan]

Kevin Buzzard said:

I think you always have to put ..(show B, by apply_instance) in, even if the instance is in the type class cache.

Kevin B, thanks very much. Here's a piece of code that works without my saying anything about instances of superclasses (if I may use that terminology). Is it just by coincidence? If so, can you perhaps pencil in what I should have written?

class A (α : Type) := (n : nat)
class B (α : Type) := (m : nat)
class C (α : Type) extends A α, B α := (k : nat)

instance : A nat := ⟨ 1 ⟩
instance : B nat := ⟨ 2 ⟩
instance : C nat := ⟨ 3 ⟩  -- works but maybe just by good luck

#reduce c                  -- {to_A := {n := 1}, to_B := {m := 2}, k := 3}

It's clear that we can't always rely on Lean finding superclass instances. And in cases where we can't, it's often unclear which or even how many fields need to be filled in, and in what order. Perhaps the right rule is to always use "show _, by apply_instance?" Is there documentation somewhere as to how resolution of superclass instances works and/or what we need to do to make it work?

[Mario Carneiro]

If the constructor actually takes a typeclass argument, you don't have to provide it like that. It's mainly when you use old structures that you need it since the C.mk doesn't actually have A and B as arguments but rather their fields

[Kevin Sullivan]

Mario Carneiro said:

If the constructor actually takes a typeclass argument, you don't have to provide it like that. It's mainly when you use old structures that you need it since the C.mk doesn't actually have A and B as arguments but rather their fields

Thank you.

[Kevin Sullivan]

Kevin Sullivan said:

Kevin Buzzard said:

I think you always have to put ..(show B, by apply_instance) in, even if the instance is in the type class cache.

Kevin B, thanks very much. The reason I ask is that Lean's behavior is inconsistent. Here's a piece of code that works without my saying anything about instances of superclasses (if I may use that terminology). I had mistakenly assumed that this is how Lean would work, in general. But clearly it's not.

class A (α : Type) := (n : nat)
class B (α : Type) := (m : nat)
class C (α : Type) extends A α, B α := (k : nat)

instance : A nat := ⟨ 1 ⟩
instance : B nat := ⟨ 2 ⟩
instance : C nat := ⟨ 3 ⟩  -- works but maybe just by good luck

#reduce c                  -- {to_A := {n := 1}, to_B := {m := 2}, k := 3}

Ok, I see where my confusion was. First, my example above uses anonymous constructor notation, ⟨ ... ⟩. Typeclass inference appears to work to fill in the missing fields in the example I've given, but it doesn't appear to work in all cases. That's what had me misled: I'd drawn an inference from its working in simple cases to conclude that it works in general. I haven't yet quite figured out what's going on with that: when it works and when it doesn't. Second, it also appears that the ..p notation does not work at all with anonymous constructor notation. So, conclusion, it appears that combining standard { ... } structure instance definition notation with ..p, ..q, ..r notation (telling Lean to try to fill in missing field values from fields defined in p, q, r in that order) is what I need.

class A (α : Type) := (n : nat)
instance a : A nat := ⟨ 1 ⟩     -- anonymous constructor notation

class B (α : Type) := (m : nat)
instance b : B nat := ⟨ 2 ⟩     -- anonymous constructor notation

class C (α : Type) extends A α, B α := (c : nat)
instance c : C nat := { c := 3, ..a, ..b }  -- curly brace / field assignment notation