Failing to use a declared implicit variable

Stream: new members

[Stuart Presnell]

I'm sure this is a simple thing I'm overlooking, but can someone explain why Lean is giving a don't know how to synthesize placeholder error at the theorem statement here, complaining that it needs a term of type A → B? Why isn't it using the implicit variable l : A → B declared above? (I thought I might need to explicitly include it to force Lean to notice it, but that hasn't fixed the problem).

import order.boolean_algebra

variables {A B : Type} [boolean_algebra A] [boolean_algebra B]
variables {l : A → B}

include l

def R (a:A) (b:B) : Prop := l a ≤ b

theorem R_upward_closed_right (a:A) (b0 b1 : B) : (b0 ≤ b1) → (R a b0) → (R a b1)
  := sorry

omit l

[Yaël Dillies]

When you use R, l is treated as an implicit argument. Problem is, it doesn't appear in the definition of R, so Lean can't figure out what to put there!

[Yaël Dillies]

The definition of R doesn't "remember" that the particular variable it was defined with is l. You can achieve your expected result using parameter, but we advise against it.

[Yaël Dillies]

Best thing here is to simply make l explicit.

[Stuart Presnell]

Ok, thanks very much