Incompatibility between rewriter and uncompute

[jdevuyst]

The following code

plusCommutativeRewrite' : (l, r : Nat) -> Fin (l + r) -> Fin (r + l)
plusCommutativeRewrite' = %runElab (do rewriter {ty=`(Nat)} natPlusRefl)

fails with the error

No such variable goal

because natPlusRefl includes a call to uncompute:

natPlusRefl : Elab ()
natPlusRefl = do
  intros
  compute
  uncompute $ unSucc {binop=`(plus)} {neutral=`(Z)} {succ=`(S)}
  CommutativeMonoid.refl {ty=`(Nat)} {tc=`(PlusNatCommMonoidV)} {binop=`(plus)} {neutral=`(Z)}

Specifically, the issue is that a Pruviloj.Core.equiv call by uncompute creates a hole named "goal", which then later vanishes.

I attempted to create an alternative implementation of equiv, that would call replace and then ran into this issue: idris-lang/Idris-dev#3934. I wonder if the same issue may cause "goal" to disappear. 🤔