Auto-implicits in \where block stops working under function defined as a full pat mat

[Odomontois]

E.g. this code

\func DepPath {X : \Type} {x x' : X} {Y : X -> \Type} (p : x = x') (y : Y x) (y' : Y x'): \Type
  | idp, y, y' => y = y' \where {

  \func pe (p : x = x') (y : Y x) (y' : Y x'): Path (\lam i => Y (p @ i)) y y' = DepPath p y y' \elim p
    | idp => idp
}

reports erros in pe definition on multiple "cannot resolve reference" while this works

\func DepPath {X : \Type} {x x' : X} {Y : X -> \Type} (p : x = x') (y : Y x) (y' : Y x'): \Type \elim p
  | idp => y = y' \where {

  \func pe (p : x = x') (y : Y x) (y' : Y x'): Path (\lam i => Y (p @ i)) y y' = DepPath p y y' \elim p
    | idp => idp
}

[Odomontois]

As discussed, eliminated parameters could not be seen from the subdefinitions.