Declaration becomes noncomputable with new compiler

Stream: lean4

[Christian Merten]

The following declaration throws an error on latest mathlib, but is accepted without noncomputable on mathlib stable:

import Mathlib.Algebra.Category.CommAlgCat.Basic
import Mathlib.CategoryTheory.MorphismProperty.Comma
import Mathlib.AlgebraicGeometry.GammaSpecAdjunction

open CategoryTheory

variable (Q : MorphismProperty CommRingCat) (R : CommRingCat.{u})

-- noncomputable
def CommRingCat.Under.inclusion :
    MorphismProperty.Under Q ⊤ R ⥤ Under R :=
  MorphismProperty.Under.forget Q ⊤ R

The error messages is very strange, because the declaration AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity does not feature anywhere in the definition:

failed to compile definition, compiler IR check failed at 'CommRingCat.Under.inclusion._redArg._closed_0'.
Error: depends on declaration 'CategoryTheory.Functor.id._at_.AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity.spec_0',
which has no executable code; consider marking definition as 'noncomputable'

The error vanishes if the (unused) Mathlib.AlgebraicGeometry.GammaSpecAdjunction import is removed.
(@Cameron Zwarich)

[Cameron Zwarich]

This is fixed by lean4#8691, which should be in an upcoming v4.22.0 rc3.

[Christian Merten]

Great, thanks!