Cryptic error message in new lean toolchain?

Stream: lean4

[Grant Yang]

Hi all, I've run into an error message on 4.29.0-rc1 that's much more cryptic than it had been on 4.28.0.

If I use something noncomputable in a def that's not marked noncomputable, on 4.28.0 i would get a reasonable error like Error: depends on declaration 'IsAdjoinRoot.ofAdjoinRootEquiv', which has no executable code; consider marking definition as 'noncomputable'

However, on 4.29.0-rc1 the same code errors out with Failed to find LCNF signature for IsAdjoinRoot.ofAdjoinRootEquiv, which was very confusing to me and I thought it was a compiler bug. The code and the errors can be seen here, switching between mathlib latest and stable: https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOJgCmAdnAAoToCexEIwS6eAbklA1uoXAN4BKcAMoBfOAG0AwnRB9gxAOZw+AXXFSQMuYsGqxAQXTzCWKEiVDlOAMSFW6OABlCSYgDpmhKAGdgEYoJh2BRwAE0IAMzhgLz0QgCsIOT4ICBgAfQhwg3kAUQBHAFdgZjgACkiALiUxAA1lAEocOGay7irSvlrVQA/KOABJMMZXLzAXXnDherhAYSJABIIxFSEpqr6Y+MTiZNShOEimuAqAXn61hKSUmFdM2LPNi/yiksIcIA

Is this a regression, or is this just something normal that happens on release candidate toolchains?

[Jovan Gerbscheid]

It's easier if you share the code like this, it comes with a link to Lean web:

import Mathlib

open Polynomial

variable {R S} [CommRing R] [CommRing S] [Algebra R S]
#eval Lean.versionString
def isAdjoinRoot_ofAlgEquiv (f : R[X])
    (e : (R[X] ⧸ Ideal.span {f}) ≃ₐ[R] S) : IsAdjoinRoot S f
  := IsAdjoinRoot.ofAdjoinRootEquiv e

[Jovan Gerbscheid]

From what I understand there has been some work/changes on how to figure out if something is non-computable, so I guess the changing error messages are a side effect. The new error message is indeed a lot more obscure!

[Sebastian Ullrich]

Thanks for the reports, this should be fixed by #12625 but I'll need to wait for Mathlib to be compiled against it to verify

[Snir Broshi]

Oh this is also #mathlib4 > Cardinals - Failed to find LCNF signature @ 💬 and #Is there code for X? > Functoriality of MvPolynomial @ 💬, thanks

[Eric Wieser]

(lean4#12625)