Spurious noncomputable tag

Stream: lean4

[Frédéric Dupuis]

Here's a strange bug I've encountered while reviewing mathlib4#1453:

import Mathlib.Init.Set
import Mathlib.Init.ZeroOne

def Language (α) := Set (List α)

instance : Membership (List α) (Language α) := Set.instMembershipSet
instance : EmptyCollection  (Language α) := Set.instEmptyCollectionSet

/-
failed to compile definition, consider marking it as 'noncomputable' because it depends on
'EmptyCollection.emptyCollection', and it does not have executable code
-/
--instance : Zero (Language α) := ⟨(∅ : Language α)⟩

/- Works -/
def foo : Language α := ∅
instance inst1 : Zero (Language α) := ⟨foo⟩

/- Also works -/
instance inst2 : Zero (Language α) :=
  let foo : Language α := ∅
  ⟨foo⟩

[Eric Wieser]

I'm a bit surprised we're porting this already, given it's on no critical paths at all. It's rather unfortunate that #17965 predates it by a month.

[Mario Carneiro]

non-critical files are often being used as training ground for new porters, so we get a fair number of them in addition to the main stuff

[Matthew Ballard]

I ran into this with !4#2619 . The following

def ConcreteCategory.hasCoeToSort (C : Type v) [Category C] [ConcreteCategory C] :
    CoeSort C (Type u) where
  coe := ConcreteCategory.Forget.obj

throws the failure to compile warning but

coe := fun X => ConcreteCategory.Forget.obj X

is fine. I'll try to minimize.

[Gabriel Ebner]

lean4#2096