Type universes and mutual definitions not working together

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

The following code

inductive ArityZero
inductive Expr (sig: Type u)

def IsStrongCause (expr: Expr sig) := expr = expr

mutual
def bar (a: IsStrongCause expr): True := trivial

def foo (expr: Expr ArityZero) :=
  let isc: IsStrongCause expr := rfl
  bar isc
end

procuces the following error

application type mismatch
  bar isc
argument
  isc
has type
  IsStrongCause expr : Prop
but is expected to have type
  IsStrongCause ?m.141 : Prop

Using @bar ArityZero expr isc instead gives

application type mismatch
  @bar ArityZero
argument
  ArityZero
has type
  Type : Type 1
but is expected to have type
  Type u_1 : Type (u_1 + 1)

The issue does not manifest if either:

• the type of sig is changed from Type u to Type
• the type of ArityZero is changed from Type to Type u, or
• the definitions are made not mutual (which is OK since they aren't recursive)

Expected behavior: The code produces no errors, as in the case of the above changes.

Versions

Lean: 4.12.0-nightly-2024-10-01
OS/Platform: live.lean-lang.org

Impact

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

Start by running the self-contained reproducer from the issue against the specified Lean nightly version, then compare it with the listed non-mutual and universe-annotation variants. Done means the original mutual definitions using Type universes elaborate without errors; no repository file or test is named.