Implicit lambdas in inverse function

Stream: lean4

[Matthew Ballard]

I have

structure LeftInverse (f : α → β) where
  to_fun : β → α
  invl : to_fun ∘ f = id

structure RightInverse (g : β → α) where
  to_fun : α → β
  invr : f ∘ to_fun = id

structure Inverse (f : α → β) where
  to_fun : β → α
  invl : to_fun ∘ f = id
  invr: f ∘ to_fun = id

def inv_to_left_inv (f : α → β) (g : Inverse f) : LeftInverse f := ⟨g.to_fun,g.invl⟩
def inv_to_right_inv (f : α → β) (g : Inverse f) : RightInverse f := ⟨g.to_fun,g.invr⟩

The g.invr is triggering an implicit lambda

type mismatch
  g.invr
has type
  f ∘ g.to_fun = id : Prop
but is expected to have type
  f✝ ∘ g.to_fun = id : Prop
the following variables have been introduced by the implicit lambda feature
  f✝ : ?m.3973 → ?m.3972
you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.

but despite the error message I am not sure what to do to disable it here.

[Adam Topaz]

you have a typo in RightInverse: g should be f

[Matthew Ballard]

Doh! Thanks.

[Matthew Ballard]

Not telling Lean what f is would do it.

[Adam Topaz]

I wish there was some option that would disable some of the new automatic stuff in Lean4 like this. In Lean3, the definition of RightInverse would give an error saying that Lean doesn't know what f is. Similarly if you make a typo in the name of some type, it can lead to issues that are hard to debug.

[Kevin Buzzard]

I am getting into the habit of switching off the "if it's a random string of characters, let's just guess that you mean a new variable" thing

[Adam Topaz]

How do you switch it off?

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/dumb.20questions/near/294944238 Patrick does the same too.

[Adam Topaz]

Oh excellent! set_option autoImplicit false!

[Matthew Ballard]

I am glad something productive came from my typo :)

[Kevin Buzzard]

I have also trained myself to spot that light blue is a variable and dark blue isn't, so e.g. if you write nil instead of list.nil then you can see it's a different colour. But that wouldn't have helped Matt.

[Adam Topaz]

IIRC in the earlier days of Lean4, this was only activated for greek letters implicitly inserting types. Am I misremembering? Is there a slightly more relaxed option that only does this autoImplicit for greek letters?

[Matthew Ballard]

Kevin Buzzard said:

I have also trained myself to spot that light blue is a variable and dark blue isn't, so e.g. if you write nil instead of list.nil then you can see it's a different colour. But that wouldn't have helped Matt.

For multiple reasons

[Sebastian Ullrich]

Kevin Buzzard said:

I have also trained myself to spot that light blue is a variable and dark blue isn't, so e.g. if you write nil instead of list.nil then you can see it's a different colour. But that wouldn't have helped Matt.

Yes, this is a quite interesting case. IIRC, Isabelle uses a different color for implicitly introduced variables, with a quite noticeable background shading in fact. Perhaps we should too.

[Matthew Ballard]

I would say that, if the error message suggested that it was possible that I misnamed a variable, it would (most likely) have been fixed immediately without the puzzlement.

[Sebastian Ullrich]

That the mistake happened in a different declaration does make it a bit complicated. It sure would be better in general if users noticed the mistake right there.