out_params and products

Stream: general

[Sebastien Gouezel]

I have just stumbled on a situation where I am not happy with typeclass inference. Maybe I am misusing it. I have been able to minimize the example, so maybe @Daniel Selsam you will be interested in this. Some motivation. Assume that some types can have a model type, whatever that means, and that this model type when it exists is unique. Then I want to register it as an outparam, to avoid writing it explicitly in all the formulas. This works pretty well most of the time, but not when I have products where it fails to find the relevant instance. MWE:

variables {α : Type} {β : Type} {γ : Type} {δ : Type}

class model (α : Type)

instance model_prod [model α] [model β] : model (α × β) := by constructor

class has_model (α : out_param $ Type) [out_param $ model α] (γ : Type) :=
(my_fun : γ → α)

instance has_model_prod [model α] [model β] [has_model α γ] [has_model β δ] :
  has_model (α × β) (γ × δ) :=
{ my_fun := λp, (has_model.my_fun p.1, has_model.my_fun p.2) }

def come_on_lean [model α] [model β] [has_model α γ] [has_model β δ] : has_model (α × β) (γ × δ) :=
  by apply_instance

def foo [model α] [has_model α γ] (x : γ) : γ := x

lemma doesnt_work [model α] [has_model α γ] [model β] [has_model β δ] (p : γ × δ) : foo p = p := rfl

In come_on_lean (which is exactly the same statement as the instance just before), apply_instance fails to find the relevant instance. And the instance search starts with @has_model ?x_0 ?x_1 (γ × δ), which looks crazy to me because I have said right away that the model type should be α × β, so why start the search with ?x_0? Then doesnt_work also fails, not surprisingly, because Lean fails to find the same model space instance on the product.

Is there a proper way to formulate my instances (while keeping the out_param)?

[Mario Carneiro]

I'm not surprised that the search starts with @has_model ?x_0 ?x_1 (γ × δ); you said the first two args are out_params so it doesn't use them in the search

[Mario Carneiro]

this works:

instance has_model_prod {_ : model α} {_ : model β}
  [has_model α γ] [has_model β δ] : has_model (α × β) (γ × δ) :=
{ my_fun := λp, (has_model.my_fun p.1, has_model.my_fun p.2) }

def works [model α] [model β] [has_model α γ] [has_model β δ] : has_model (α × β) (γ × δ) :=
  by apply_instance

[Sebastien Gouezel]

Thanks a lot, this is black magic to me! And it also works in my more complicated real use case, by replacing randomly some typeclass arguments in several of my definitions by implicit arguments. A little bit like with the recent changes to implicit arguments in coercions, I don't really understand what is going on. Is there a rule of thumb like the following: If we have lemma foo [first_class A B] [second_class A B] ... and second_class in its definition has a typeclass argument [first_class A B], then one could (and should?) change the definition of foo to lemma foo {_ : first_class A B} [second_class A B]?

[Mario Carneiro]

What happens is that in your instance, with [model α] [model β] [has_model α γ] [has_model β δ], it will search for all four of these instances, from left to right. Since the target is @has_model ?x_0 ?x_1 (γ × δ) which unifies with the instance conclusion, you end up searching for model ?m_2 where ?x_0 := (?m_2 × ?m_3)`, which is not good

[Mario Carneiro]

By setting the model α arguments to implicit, we are saying to not attempt to typeclass search for them, and instead search only for has_model α γ (which gives us model α by unification), and since this has an out_param on α this works

[Mario Carneiro]

Whether to use [first_class A B] [second_class A B] or {_ : first_class A B} [second_class A B] depends on whether the typeclass search @second_class A ? B is supposed to be able to succeed

[Mario Carneiro]

If there is an out_param on that argument, then this search will work, otherwise it's probably not a good idea