Cryptic error in `inverse_spec`

Stream: general

[Vasily Ilin]

I get a cryptic error about metavriables and types in the example below, from MIL 4.2. Why does inverse_spec not work with f x but works with y?

import Mathlib.Tactic
import Mathlib.Util.Delaborators
import Mathlib.Data.Set.Function

set_option warningAsError false

variable {α β : Type*} [Inhabited α]
noncomputable section

open Classical

def inverse (f : α → β) : β → α := fun y : β ↦
  if h : ∃ x, f x = y then Classical.choose h else default

theorem inverse_spec {f : α → β} (y : β) (h : ∃ x, f x = y) : f (inverse f y) = y := by
  rw [inverse, dif_pos h]
  exact Classical.choose_spec h

variable (f : α → β)
variable (x : α) (hx : ∃ x, f x = f x)
variable (y : β) (hy : ∃ x, f x = y)
#check hx
#check inverse_spec (f x) hx -- cryptic error
#check @inverse_spec f (f x) hx -- cryptic error
#check inverse_spec y hy -- works

[Ruben Van de Velde]

What's the error?

[Vasily Ilin]

I edited the example so it actually runs. Errors are

application type mismatch
  inverse_spec (f x) hx
argument
  hx
has type
  ∃ x, f x = f x : Prop
but is expected to have type
  ∃ x_1, ?m.3089 x_1 = f x : Prop

and

application type mismatch
  @inverse_spec f
argument
  f
has type
  α → β : Type (max u_1 u_2)
but is expected to have type
  Type ?u.3242 : Type (?u.3242 + 1)

[Kevin Buzzard]

If you have a variable x then what do you expect exists x, f x = f x to mean? At the very least this is bad style and it might be the cause of your problems: you have both a free and a bound variable with the same name.

[Vasily Ilin]

Ah, that was it for the first error. Thank you!

[Kevin Buzzard]

I was just looking at the error, where lean had helpfully changed one of them to x_1 but not the other one :-)

[Vasily Ilin]

I got stumped by ?m.3089 in place of f.

[Kevin Buzzard]

For the other one (sorry I'm not at lean right now) do you understand what @ does? @inverse_spec f won't typecheck.

[Kevin Buzzard]

Because f will map X to Y and @ means "you must give me X and Y before f"

[Kevin Buzzard]

It switches off implicit inputs

[Vasily Ilin]

Yes, this helps. The following works:

#check @inverse_spec α β _ f (f x) hx

This time I got stumped by Type ?u.3147 : Type (?u.3147 + 1). I am scared of these ?u.crazy_number errors.

[Kevin Buzzard]

Would you be less scared of it just said u? It's just a universe metavariable. Would you be less scared if it just set u to be 0 and the error said "is expected to have type Type : Type 1? That's the sort of errors my students see because I encourage them, at the beginning, not to use universes at all.

[Kevin Buzzard]

The error says "you gave me a function, I was expecting a set" (or a type, as lean calls them)

[Vasily Ilin]

I guess I would be less scared because it's fewer weird symbols on screen :). I will get used to it as some point, I'm sure

[Kevin Buzzard]

Was there some recent change to lean which would enable people to switch off the numbers? Then you'd get "expected to have type Type ?u"

[Vasily Ilin]

That would be a nice QoL improvement.

[Damiano Testa]

Maybe set_option pp.mvars true?