invalid field notation, insufficient number of arguments

Stream: general

[Eric Wieser]

Extracted from another thread; what's going on with this error message?

import order.filter.basic

open filter

/-- Alias for dot notation -/
abbreviation filter_mem_dot_notation (P : Prop) : Prop := P

instance filter.has_mem' {α : Type*} : has_mem (set α) (filter α) :=
{mem := λ u f, filter_mem_dot_notation (u ∈ f.sets) }

-- replacing `hx` with `filter_mem_dot_notation (x ∈ f)` fixes the error
lemma filter_mem_dot_notation.up {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
sorry

variables {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y)
#check hx.up -- ok
#check hx.up h  -- invalid field notation, insufficient number of arguments for 'filter_mem_dot_notation.up'

[Kevin Buzzard]

#check filter_mem_dot_notation.up hx h works fine. More interestingly, #check hx.up h _ gives

invalid field notation, function 'filter_mem_dot_notation.up' does not have explicit argument with type (filter_mem_dot_notation ...)

so that's probably what the issue is -- Lean's dot notation is confused by this point (because it doesn't work with abbreviations very well?)