Confusion with `outParam`

Stream: new members

[Nick Attkiss]

Hi all! In Section 7.2 the Mathematics in Lean tutorial introduces the outParam function to help fix typeclass resolution problems for monoid morphisms. In this setup, we start by representing objects that are "at least monoid morphisms":

class MonoidHomClass₁ (F : Type) (M N : Type) [Monoid M] [Monoid N] where
  toFun : F → M → N
  map_one : ∀ f : F, toFun f 1 = 1
  map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

We then try to register the following CoeFun instance, which would raise an error if we actually used the instance keyword:

def badInst [Monoid M] [Monoid N] [MonoidHomClass₁ F M N] : CoeFun F (fun _ ↦ M → N) where
  coe := MonoidHomClass₁.toFun

To fix this, we change our definition of the MonoidHomClass₁ class by tagging M and N with outParam:

class MonoidHomClass₂ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] where
  toFun : F → M → N
  map_one : ∀ f : F, toFun f 1 = 1
  map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

Now the CoeFun instance can be successfully registered:

instance [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] : CoeFun F (fun _ ↦ M → N) where
  coe := MonoidHomClass₂.toFun

I don't see how adding outParam solves the error, or even what the error is exactly. As I understand it, the problem with the first implementation is that when Lean sees f x with f : F not a function type, it will try to use the CoeFun instance but get stuck because it doesn't know the order to infer F, M, and N. Marking M and N with outParam will tell Lean to infer F first, as it should.

But then why is the change made to the MonoidHomClass class, when the problem is with the CoeFun instance? And why does Lean raise an error when we define the bad CoeFun instance, instead of when we try to use the bad CoeFun instance?

I would really benefit from a step-by-step analysis of what Lean is trying to do at each line, in both the bad first implementation and the corrected second implementation; that way I can see exactly where the problem lies and how the change with outParam solves it. I've played around with set_option trace.Meta.synthInstance true to try to do this myself, but there's a lot of distracting irrelevant information.

Thanks for the help!

[Daniel Weber]

The problem is caused because docs#CoeFun has the function type as an outParam. This means that, when seeing f x for f : F Lean would search for some CoeFun F _ instance, but it can't apply badInst because synthesizing MonoidHomClass₁ requires knowing M and N, but it doesn't know them yet. It is able to figure this out when registering the instance and give an error.
When changing M, N in MonoidHomClass₂ to outParam it can now use the instance because it can search for some MonoidHomClass₂ F _ _, and once that resolves it knows M, N

[Nick Attkiss]

It's making a little more sense, but I'm still confused about what order everything happens in. An example could be useful. Sticking with the fixed implementation MonoidHomClass₂, let's define a structure for monoid morphisms and register it as an instance of MonoidHomClass₂:

structure MonoidHom₁ (G H : Type) [Monoid G] [Monoid H]  where
  toFun : G → H
  map_one : toFun 1 = 1
  map_mul : ∀ g g', toFun (g * g') = toFun g * toFun g'

instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₂ (MonoidHom₁ M N) M N where
  toFun := MonoidHom₁.toFun
  map_one := fun f ↦ f.map_one
  map_mul := fun f ↦ f.map_mul

Now say we run the following check:

variable (G H : Type) [Monoid G] [Monoid H] (f : MonoidHom₁ G H) (x : G)

#check f x

The last line forces Lean to find a CoeFun instance. How does this play out from start to end? I.e., when do we pass from CoeFun to MonoidHomClass₂, how does Lean infer the variables and in what order, etc? Can we do a step-by-step analysis of the algorithm? I tried set_option trace.Meta.synthInstance true again but this time there's not enough information for me to make sense of it.