diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index a58daf3824..4d7147576f 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -599,6 +599,7 @@ template<typename F> optional<expr> type_checker::reduce_bin_nat_op(F const & f,
 
 optional<expr> type_checker::reduce_pow(expr const & e) {
     expr arg1 = whnf(app_arg(app_fn(e)));
+    if (!is_nat_lit_ext(arg1)) return none_expr();
     expr arg2 = whnf(app_arg(e));
     if (!is_nat_lit_ext(arg2)) return none_expr();
     nat v1 = get_nat_val(arg1);
diff --git a/tests/lean/run/pow_exploit.lean b/tests/lean/run/pow_exploit.lean
new file mode 100644
index 0000000000..de5d38c261
--- /dev/null
+++ b/tests/lean/run/pow_exploit.lean
@@ -0,0 +1,43 @@
+import Lean
+
+/-!
+This was once an exploit of a bug in the Lean kernel relying on the Lean kernel
+falsely interpreting an expression as a Nat literal.
+-/
+
+def g.{u} : PUnit.{u} → Nat := fun _ => open Classical in if Type = Type then 0 else 0
+
+-- Just writing `Nat.pow (Nat.pow 10 8) 502` would also work; `Nat.pow (Nat.pow 10 8) 503` wouldn't
+def T : Nat → Prop := fun x => if x = 0 then False else True
+
+-- The kernel reduces this to a number between 10^8032 and 10^8048
+def POW! := Nat.pow (g.{0} ⟨⟩) 1
+
+elab "#inject_bad_proof" : command => do
+  let decl : Lean.Declaration := .defnDecl {
+      name := `mythm,
+      hints := .regular 0,
+      safety := .safe,
+      type := (.app (.const `T []) (.const `POW! [])),
+      levelParams := [],
+      value := (.const `True.intro [])
+    }
+  Lean.Elab.Command.liftCoreM (Lean.addDecl decl)
+
+/--
+error: (kernel) declaration type mismatch, 'mythm' has type
+  True
+but it is expected to have type
+  T POW!
+-/
+#guard_msgs in
+#inject_bad_proof
+
+theorem g_eq_zero : g.{u} n = 0 := by
+  unfold g
+  split <;> rfl
+
+theorem show_false : False := by
+  change T (Nat.pow 0 1)
+  rw [← g_eq_zero]
+  exact mythm