notation fail

Stream: general

[Kevin Buzzard]

I am in a situation where this term compiles fine:

nonempty (𝒞.equiv (locally_ringed_valued_space.to_𝒞.restrict U) (𝒞.Spa A))

but if I put

notation A ` ≅ `:50 B := nonempty (𝒞.equiv A B)

and try

(locally_ringed_valued_space.to_𝒞.restrict U) ≅ (𝒞.Spa A)

I get the error

type mismatch at application
  (λ (x_1 : 𝒞 ↥U) (x_2 : 𝒞 ?m_1[x_1]), x_1 ≅ x_2)
    (𝒞.restrict U (𝒱.to_𝒞 locally_ringed_valued_space))
    (𝒞.Spa A)
term
  𝒞.Spa A
has type
  𝒞 ↥(Spa A) : Type (?+1)
but is expected to have type
  𝒞 ?m_1[𝒞.restrict U (𝒱.to_𝒞 locally_ringed_valued_space)] : Type (max ? (?+1))

Similarly if I switch the two terms around I get

type mismatch at application
  (λ (x_1 : 𝒞 ↥(Spa A)) (x_2 : 𝒞 ?m_1[x_1]), x_1 ≅ x_2) (𝒞.Spa A)
    (𝒞.restrict U (𝒱.to_𝒞 locally_ringed_valued_space))
term
  𝒞.restrict U (𝒱.to_𝒞 locally_ringed_valued_space)
has type
  𝒞 ↥U : Type (max u (?+1))
but is expected to have type
  𝒞 ?m_1[𝒞.Spa A] : Type (max ? (?+1))

Is this a limitation of notation somehow? I'd be surprised -- I'd be more likely to believe that I'm not using it correctly or I've made some other error. If notation is just syntactic sugar then as far as I can see the thing that's failing just directly translates into the thing that's succeeding.

[Kevin Buzzard]

Oh! I've got to the bottom of it and it's part of the story which I didn't mention. The \iso notation is overloaded, and for some reason Lean isn't trying as hard to unify because it is not sure which function I mean. If I change my notation to an un-overloaded one then it works.

[Kevin Buzzard]

I guess Lean is being more cautious in trying to unify because it doesn't want to end up spending a lot of time trying to typecheck something which doesn't typecheck, or something.