fix: guard against Nat.reducePow panicking

In the Carleson project a non-fatal PANIC occurring in the application
of certain applications of `Nat.reducePow` was discovered
(https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/PANIC.20at.20Lean.2EExpr.2EappArg!.20application.20expected/near/457037665).
We fix this regression from leanprover#4637.

Fixes leanprover#4947.

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -55,6 +55,7 @@ builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Nat)) := reduceBin ``HDiv.hDi
 builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMod 6 (· % ·)
 
 builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := fun e => do
+  unless e.isAppOfArity ``HPow.hPow 6 do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
   unless (← checkExponent m) do return .continue

tests/lean/4947.lean

@@ -0,0 +1,17 @@
+/-! # Test that safe exponentiation does not cause a panic -/
+
+universe u
+
+class G (A : outParam Nat) where Z : Type u
+
+export G (Z)
+
+/-! Define an abbrev which `reducePow` can work on -/
+
+abbrev f (a : Nat) : Nat := 2 ^ a
+
+variable [G (f 0)]
+
+/-! This should not cause a panic -/
+
+example {s : Z} : s = s := by simp only [Nat.reducePow]