Cardinals - Failed to find LCNF signature

Stream: mathlib4

[Snir Broshi]

import Mathlib.SetTheory.Cardinal.Order

/-- error: Failed to find LCNF signature for Cardinal.instConditionallyCompleteLinearOrderBot -/
#guard_msgs in
def foo : Cardinal :=
  sInf {0}

-- `noncomputable` fixes it
noncomputable def foo' : Cardinal :=
  sInf {0}

Posting here instead of #lean4 since I'm not sure if this is a bug, and how to minimize.
I also tried the new set_option backward.isDefEq.respectTransparency false but it doesn't help.

[Snir Broshi]

Another example: #Is there code for X? > Functoriality of MvPolynomial @ 💬

[James E Hanson]

Oddly enough this fixes it:

import Mathlib.SetTheory.Cardinal.Order

def foo : Cardinal :=
  0 + sInf {0}