Noncomputable Coe.coe ?

Stream: lean4

[Arthur Adjedj]

Hi, the following code gives a rather unexpected error:

instance [h : Coe α (Sort u)] : CoeSort α (Sort u) where
  coe := h.coe
/-failed to compile definition,
  consider marking it as 'noncomputable'
  because it depends on 'Coe.coe', and it
  does not have executable code-/

Even though this works fine:

instance [h : Coe α (Sort u)] : CoeSort α (Sort u) where
  coe x := h.coe x

I'm assuming this is a bug ?

[Gabriel Ebner]

Looks similar to https://github.com/leanprover/lean4/issues/2104

[Arthur Adjedj]

Indeed ! Should I add this MWE to the issue as well, or would it be best left as-is ?

[Scott Morrison]

I think it's good to add it.