afterCompilation attributes are not always applied in noncomputable section

[fpvandoorn]

In the following code, I try to apply simp to three declarations, but it doesn't get applied to baz. In fact, no attributes that run afterCompilation get executed for baz.

import Lean

noncomputable section
@[simp] def foo : Nat := 1
@[simp] noncomputable def bar : Nat := Classical.choice ⟨0⟩
@[simp] def baz : Nat := Classical.choice ⟨0⟩ -- `@[simp]` attribute doesn't get executed

open Lean Meta Elab Command

#eval liftCoreM <| do
  let x1 := simpExtension.getState (← getEnv) |>.toUnfold.contains <| `foo
  let x2 := simpExtension.getState (← getEnv) |>.toUnfold.contains <| `bar
  let x3 := simpExtension.getState (← getEnv) |>.toUnfold.contains <| `baz
  logInfo m!"{x1} {x2} {x3}" -- returns: "true true false". expected: "true true true"

Version

Lean (version 4.0.0-nightly-2023-01-29, commit 38a0d1e, Release)