lean 3 ignores ascription of function

Stream: mathlib4

[Jireh Loreaux]

I just encountered a weird error while porting that I thought was a mathport bug, but turned out to be something obscene in mathlib3/lean3:
If you look here, you will see this declaration:

@[simp, norm_cast]
lemma sup'_coe {ι : Type*} {s : finset ι} (H : s.nonempty) (f : ι → C(β, γ)) :
  ((s.sup' H f : C(β, γ)) : ι → β) = s.sup' H (λ a, (f a : β → γ)) :=
by { ext, simp [sup'_apply], }

which at first glance looks reasonable, until you notice that this is an equality between terms of type β → γ, and on the left-hand side the type ascription to ι → β. This is strange because, without any type ascription Lean complains, but you can even add the type ascription ℕ → ℤ to the left-hand side in place of ι → β and Lean is happy. What the hell is going on here?

I think maybe I understand, which is that Lean does unification, figures out that the right-hand side is a bare function, coerces the left-hand side to a function without paying attention the precise types and proceeds happily. But without any type ascription, the unification path goes down a different way and gets stuck. But this is hellishly weird, and if that's not a bug, I don't know what is. (I'm not saying we should necessarily bother to fix it.)

[Jireh Loreaux]

I'm put this in the mathlib4 stream just so people porting might see this in case it comes up again, but if someone wants to move it to a different stream that's fine.

[Kevin Buzzard]

Lean 3 a bit more minimised:

import topology.continuous_function.basic

variables {β : Type*} {γ : Type*}
  [topological_space β] [topological_space γ]

example (f : C(β, γ)) : ((f : C(β, γ)) : ℕ → ℤ) = f := sorry

[Kevin Buzzard]

I would just PR the fix to the mathlib3 file I guess?

[Jireh Loreaux]

It's not necessary, I've already ported the file.

[Jireh Loreaux]

Mainly I just wanted other people to be aware that this is a thing.

[Jireh Loreaux]

But actually your minimized example kind of wrecks my theory about what is going on.

[Alex J. Best]

I would guess this is a bug in C-land

[Alex J. Best]

Adding a type ascription maybe causes coe to fn to be inserted, but not with the type asked for?

[Alex J. Best]

Adding a type ascription maybe causes coe to fn to be inserted, but not with the type asked for?

[Jireh Loreaux]

Well, what's really weird is that _ → _ doesn't work.

[Floris van Doorn]

I believe that if you give the type ascription _ → _, Lean still respects the possibility that this is a dependent function (that the second _ depends on the first one). Maybe that is related.

[Floris van Doorn]

I opened it in Lean, and that seems to be the issue exactly.