Why Lean don't allow to call this instance method?

Stream: new members

[Luis Enrique Muñoz Martín]

The following code works as expected:

structure Foo

class Bar (α : Type) where
    bar (a : α) : String

instance : Bar Foo where
   bar a := "bar"

def callBar (f : Foo) : String := Bar.bar f  --Works!

Nevertheless, if I add an extra type to Bar class, I no longer can call callBar:

structure Foo

class Bar (α β : Type) where -- <- Add β here
    bar (a : α) : String

instance : Bar Foo Unit where  -- We implement for the case of Unit
   bar a := "bar"

def callBar (f : Foo) : String := Bar.bar f  --No longer works

Nevertheless, by my understanding the compiler should know that Foo implements Bar, and β is implemented using Unit, so it should find the correct instance and let me call bar (?)

[Kyle Miller]

The reason is that typeclass inference is not willing to decide to solve for class parameters from the others unless you mark them as outParam. If you mark it as outParam, then you are promising that the rest of the non-outParam class parameters determine this one.

[Kyle Miller]

class Bar (α : Type) (β : outParam Type) where
    bar (a : α) : String

instance : Bar Foo Unit where
   bar a := "bar"

[Luis Enrique Muñoz Martín]

Just to the point, thanks @Kyle Miller

[Shreyas Srinivas]

@Kyle Miller : Is there a discussion of outParams in any of the basic books? There are lots of these small features which could do with a tutorial but only experts and maintainers seem to know about them

[Luis Enrique Muñoz Martín]

I read about this in the Functional Programming in Lean book, but I was not able to recognize the situation later when I was in front of it: https://lean-lang.org/functional_programming_in_lean/type-classes/out-params.html?highlight=outParam#output-parameters

[Kyle Miller]

@Shreyas Srinivas Not what you're asking, but the reference manual has a mention: https://lean-lang.org/lean4/doc/typeclass.html?highlight=outparam#output-parameters