How to combine type classes?

Stream: new members

[Marcus Rossel]

What is the general mechanism for using definitions/theorems which expect a given type to have instances for multiple type classes with a shared ancestor? This problem must come up in mathlib's algebraic hierarchy all the time, so I bet there's a good solution.

Say I have the following type classes:

class A (α : Type) where
  nat : α → Nat

class B₁ (α) extends A α where
  lt₉ : ∀ a, nat a < 9

class B₂ (α) extends A α where
  gt₁ : ∀ a, nat a > 1

class B₃ (α) extends A α where
  gt₅ : ∀ a, nat a < 5

class C (α) extends B₁ α, B₂ α, B₃ α

Now if I have a type with instances for B₁ and B₂ I should be able to combine their properties. The naive approach doesn't work:

open A B₁ B₂

example [B₁ α] [B₂ α] (a : α) : (nat a < 9) ∧ (nat a > 1) :=
  ⟨lt₉ a, gt₁ a⟩
/-
application type mismatch
  And.intro (lt₉ a)
argument
  lt₉ a
has type
  @nat α B₁.toA a < 9 : Prop
but is expected to have type
  @nat α B₂.toA a < 9 : Prop
-/

I understand that I could fix this by explicitly telling Lean which instances to use for each application of nat, but of course the problem is that I would like the instances of B₁ α and B₂ α to have the same underlying instance of A α.
From what I've seen, the solution for this is to explicitly create a class which combines the two classes:

class B₁₂ (α) extends B₁ α, B₂ α

theorem range₁₉ [B₁₂ α] (a : α) : (nat a < 9) ∧ (nat a > 1) :=
  ⟨lt₉ a, gt₁ a⟩ -- works

It seems like this would lead to a combinatorial explosion once you have many type classes that you want to combine in various ways, but I can live with that. What I can't figure out though is how to handle the following:

example [C α] (a : α) : (nat a < 9) ∧ (nat a > 1) :=
  range₁₉ -- failed to synthesize instance B₁₂ ?m.684

It makes sense that since C is based on B₁, B₂ and B₃ instead of B₁₂ and B₃, Lean can't find an instance for B₁₂. Now I could change the definition of C to use B₁₂ instead of B₁ and B₂, but then what do I do if I have a theorem over B₂₃?

[Yaël Dillies]

You're missing an instance C α → B₁₂ α.

[Yaël Dillies]

It seems that your confusion stems from the fact that you think that the only typeclasses used for TC search are the ones coming from extends clauses. This is (fortunately!) wrong. You can register extra instances after the fact using the instance keyword.

[Marcus Rossel]

@Yaël Dillies Thanks!

[Adam Topaz]

Just in case it's helpful for you, an alternative approach would be to use mixins, as follows:

class A (α : Type) where
  nat : α → Nat

open A

class B₁ (α) [A α] where
  lt₉ : ∀ a : α, nat a < 9

class B₂ (α) [A α] where
  gt₁ : ∀ a : α, nat a > 1

class B₃ (α) [A α] where
  gt₅ : ∀ a : α, nat a < 5

open B₁ B₂ B₃

theorem range₁₉ [A α] [B₁ α] [B₂ α] (a : α) : (nat a < 9) ∧ (nat a > 1) :=
  ⟨lt₉ a, gt₁ a⟩ -- works