local notation can change explicitness of arguments

[fpvandoorn]

(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