What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites?

Question

There is an obvious, dirty and probably wrong approach that allows one to prove function extensionality in a straight-forward manner: provide an equality primitive with a context-aware rewrite. For example, if you had the following context:

P (λx. 1 + f x)
---------------
f : Bool -> Nat
e : (x : Bool) -> f x == 1

You could rewrite the goal to P (λx. 1 + 1) as follows:

...
rewrite X in P (λx. 1 + X) with e x
...

This "rewrite" primitive would work exactly as usual, with the only exception being we allow e to access the x bound in P (λx. 1 + X); which makes logical sense, after all, why should it not? This syntax would elaborate to the full rewrite primitive, whose type could be, kind-of, written as:

rewrite :
  (K : Type) ->
  (A : Type) ->
  (a : K -> A) ->
  (b : K -> A) ->
  (e : K -> Equal A a b) ->
  (P : A -> Type) ->
  (p : P a{k:K}) ->
  P b{k:K}

Here, Equal is just propositional equality, K is the type of a variable that is in context where x occurs in P, and {k:K} means that, after substitution, this expression will "capture" the k:K bound, and be applied to it. Explaining with words is hard, but the "magic" is that rewrite would, in an ugly and hard-coded way, inspect P to assert that there is a k:K variable where its bound variable occurs, and it would apply e to that bound variable. That's basically it.

rewrite _ _ _ _ e (λ x -> ... (λ k -> ... x ...) ...) p
                                 /\ k is in context where x occurs

The actual type of rewrite would depend on the amount of λ-binders surrounding x in the body of P. If it had no λ, then its type would be the same as the usual rewrite ((A : Type) -> (a b : A) -> (e : Equal A a b) -> (P : A -> Type) -> P a -> P b).

With such primitive, fun-ext would be trivial, because we would be able to rewrite g y in (λx. f x) == (λk. g k) applying h to the k variable bound inside the λk.

fun-ext :
  (A : Type) ->
  (B : A -> Type) ->
  (f : (x : A) -> B x) -> 
  (g : (x : A) -> B x) -> 
  (h : (x : A) -> f x == g x) ->
  f == g

fun-ext =

  // goal: f == g

  eta-expand f
  eta-expand g

  // goal: (λx. f x) == (λk. g k)

  rewrite K in (λx. f x) == (λk. K) with h k
  //                                       /\ we use the `k` bound in `λk. K` 
  //                                       /\ to make `h k : f k == g k` here,
  //                                       /\ which justifies rewriting `g k`                                           
  //                                       /\ by `f k` in the goal. this
  //                                       /\ is the only difference w.r.t.
  //                                       /\ the usual `rewrite`, which
  //                                       /\ won't let `h` access that `k`

  // goal: (λx. f x) == (λk. f k)

  refl

As a last attempt to explain: the naive intuition is that, in order to prove fun-ext, we need to apply h to some variable k : A, but there is no such variable in context. But, in the location where we need to rewrite - i.e., (λx. f x) == (λk. <HERE>), inside the goal - we do have a k in context. Normally, we can't apply h to that "inner" k in the goal. But if we hard-coded rewrite to allow its equality witness, e, to depend on variables in context in the location where the rewrite takes place (<HERE>), then we could apply h to that k, and fun-ext would be trivial. It kinda makes logical sense that the equality witness e should be allowed to depend on these variables; after all, e exists to justify the rewrite, and these variables are in scope where the rewrite takes place.

My question is: what is wrong with this approach? I assume this isn't done because it is ugly and kind of hacky, but so are the current cubical type theories, specially when it comes to transp and faces. Regardless, I'm curious: is there anything inherently wrong/broken/inconsistent in implementing funext that way?