local notation can change explicitness of arguments

(reporting this so that it can be linked to, not really requesting that this should be fixed)

The following code shows some weird interaction between local notation involving variables and the explicitness of said variables in declarations:

variables {G : Type*} {L : G → G}

local prefix ` ◾ `:67 := L

variables (L)

local prefix ` † `:67 := L

lemma explicit (p : G) : L p = p :=
sorry -- works as intended

lemma implicit (p : G) : ◾p = p :=
sorry -- the variable `L` is an implicit argument to this lemma, but should be explicit

variables {L}

lemma explicit2 (p : G) : †p = p :=
sorry -- the variable `L` is an explicit argument to this lemma, but should be implicit

#check @explicit
#check @explicit2
#check @implicit

Start by reproducing the supplied Lean snippet and compare the argument explicitness reported by #check @explicit, @explicit2, and @implicit. Investigate the interaction between local notation and variable declarations; done would mean determining whether the behavior is an accepted limitation or defining a precise correction.