Instance incorrectly marked as `noncomputable`

Stream: lean4

[Violeta Hernández]

Just came across this behavior I'm pretty sure is some sort of bug

class Data (α : Type _) (n : α) where
  data : Nat

def Foo : Type := Int
noncomputable instance : NatCast Foo where
  natCast _ := Classical.choice ⟨(0 : Int)⟩

noncomputable def bar (n : Nat) : Foo := n

-- Needs to be noncomputable!
noncomputable instance (n : Nat) : Data Foo n where
  data := n

-- Generates code just fine?
instance (n : Nat) : Data Foo (bar n) where
  data := n

[Violeta Hernández]

What's going on here? How can I make the first instance computable without resorting to the weird hack from the second instance?

[Violeta Hernández]

Interestingly, this works

class Data (α : Type _) (n : α) where
  data : Nat

def Foo : Type := Int
noncomputable instance : Zero Foo where
  zero := Classical.choice ⟨(0 : Int)⟩

-- Generates code just fine?
instance : Data Foo 0 where
  data := 37

[Violeta Hernández]

So somehow it seems like the dependent nature of the instance that doesn't work is causing something to trip up.

[Violeta Hernández]

I opened an issue about this:
https://github.com/leanprover/lean4/issues/7281

[Eric Wieser]

Somehow the builtin Nat.cast is the problem?

class Data (α : Type _) (n : α) where
  data : Nat

class MyNatCast (α : Type _) where
  natCast : Nat → α

instance {R : Type u_1} [MyNatCast R] : CoeHTCT Nat R where
  coe := MyNatCast.natCast

def Foo : Type := Int

noncomputable instance : MyNatCast Foo where
  natCast _ := Classical.choice ⟨(0 : Int)⟩

-- works fine
instance (n : Nat) : Data Foo n where
  data := n

[Eric Wieser]

The fix is adding @[inline] to src#Nat.cast

[Eric Wieser]

lean4#7283

[Violeta Hernández]

Thanks! Your GitHub description seems to completely explain the issue

[Violeta Hernández]

Is there any way I can get this working in my own codebase while the PR goes through? attribute [inline] Nat.cast doesn't work since the definition is from another module.