getting notation to work

Stream: general

[Johan Commelin]

I'm trying to use notation to hide a "parameter": an explicit variable that is constant in the entire file.
But it isn't working. Here is a MWE.

import algebra.big_operators -- should be sufficient

def foo (n : ℕ) (X : Type) [has_pow X ℕ] : X → X := λ x, x^n

variables (p : ℕ) (X : Type) [has_pow X ℕ]

localized "notation `bar` := foo p" in xyzzy

open_locale xyzzy

example : bar X = bar X :=
begin
  -- goal state shows `foo p X` instead of `bar X`
end

[Johan Commelin]

Is there a way to make this work nonetheless?

[Yury G. Kudryashov]

Does local notation work?

[Johan Commelin]

Same problem:

def foo (n : ℕ) (X : Type) [has_pow X ℕ] : X → X := λ x, x^n

variables (p : ℕ) (X : Type) [has_pow X ℕ]

local notation `bar` := foo p

example : bar X = bar X :=
begin
  -- goal state shows `foo p X` instead of `bar X`
end