noncomputable bug?

Stream: mathlib4

[Adam Topaz]

mwe:

import Mathlib

variable (α : Type) [Preorder α]

open CategoryTheory

def foo0 (X Y : α) (h : X ≤ Y) : X ⟶ Y := homOfLE h

-- Lean complains without `noncomputable`.
noncomputable def foo1 (X Y : α) (h : X ≤ Y) : X ⟶ Y := h.hom

example : foo0 = foo1 := rfl

This came up in !4#2795

Is this a bug?