We disabled beta, zeta, iota reduction in simp. However, there is a nasty interaction with the discrimination tree module.
Consider the following example:

example (h : a = b) : (fun x => a + x) 0 = b := by
  simp (config := { beta := false })
  -- h : a = b |- a = b    <<<< Goal here
  done

We requested beta reduction to be disabled, but simp performed indirectly using the discrimination tree module.
Note that the following example works as expected

example (h1 : a = b) (h2 : c = 0) : (fun x => a + x) c = b := by
  simp (config := { beta := false })
  -- h : a = b |- (fun x => a + x) c = b
  done

The issue is that the discrimination tree module retrieves rewriting rules modulo whnf with [reducible] setting. Then, when simp tries to retrieve rewriting rules for the term (fun x => a + x) 0, it finds Nat.add_zero : a + 0 = a. We need a flag in the discrimination tree modulo to control reduction when retrieving candidates. As an extra complication, we may still want to reduce [reducible] definitions, and beta-reduction here should be allowed.

The issue above may also cause performance issues.