Why is type assertion needed here

Stream: general

[Bolton Bailey]

Sorry if this is a beginner question. The following throws a error "invalid field notation", and complains on the fourth line that ps has type ?m_1. But if I mouse over ps on the third line, it correctly says ps : ℕ × ℕ.

lemma bertrand_interval (n_low n_high : ℕ) (plist : list ℕ)
  (primeplist : ∀ p ∈ plist, prime p)
  (covering : ∀ ps ∈ list.zip plist (list.tail plist),
        (ps).2 ≤ 2 * ps.1) :
  (∀ n, plist.head ≤ n → n ≤ plist.reverse.head → ∃ p, nat.prime p ∧ n < p ∧ p ≤ 2 * n)

If I add a type ascription, it's fine:

lemma bertrand_interval (n_low n_high : ℕ) (plist : list ℕ)
  (primeplist : ∀ p ∈ plist, prime p)
  (covering : ∀ ps ∈ list.zip plist (list.tail plist),
        (ps : ℕ × ℕ).2 ≤ 2 * ps.1) :
  (∀ n, plist.head ≤ n → n ≤ plist.reverse.head → ∃ p, nat.prime p ∧ n < p ∧ p ≤ 2 * n)

Why is this type ascription necessary?

[Bolton Bailey]

I guess I understand that there might in theory be multiple types that can implement has_mem of a list of ℕ × ℕ, even if in practice only ℕ × ℕ does. But then how does the mouseover know the type!?

[Kevin Buzzard]

Yes that's exactly it -- has_mem only knows that ps has type ?m_1 : Type and the unifier isn't going to tell it any more information.

[Bolton Bailey]

But then the mouseover thing is almost magical. How can it possibly know the type ℕ × ℕ when that's possibly not even the correct type?

[Bolton Bailey]

Is it indeed possible to implement two has_mem instances with the same second type argument? Does that happen anywhere in mathlib?

[Mario Carneiro]

It is possible to do (in the sense that lean won't stop you), but it's about as good an idea as defining a second instance of semiring nat

[Mario Carneiro]

What's happening is that field notation has to be resolved relatively early in the elaboration process, such that it essentially can't see any text that comes after the field projection, but the error doesn't actually stop elaboration, and the hover reports type information coming from later in the term