`simp +ground` error with a cryptic message

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In the snippet below, simp +ground fails with "Unknown constant _inhabitedExprDummy".
If I remove +ground, remove the cast to Rat, or even keep the cast to Rat but remove the division by const, there is no error.

import Mathlib.Data.Rat.Cast.Order

structure MyStruct (n : Nat) where
  vec : Vector Nat n
  const : Nat

theorem th {n : Nat} (s : MyStruct n) (i : Fin n) (h : s.const = 1) :
    s.vec[i] = (s.vec[i] : Rat) / s.const := by
  simp [h]

example : True := by
  let s : MyStruct _ := {
    vec := #v[1, 2, 3, 4]
    const := 1,
  }
  have := th s 3 (by decide)
  unfold s at this
  simp +ground at this  -- Error: Unknown constant `_inhabitedExprDummy`
  trivial

Sorry for the silly example 😅.

Versions

Lean 4.28.0
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the minimal example in the issue with Lean 4.28.0, focusing on the simp +ground invocation and the _inhabitedExprDummy error. Trace the relevant simplifier or grounding entry point and add a regression test for this example; done means the test no longer reports the unknown constant.