DecidableEq on Multiplicative?

Stream: Is there code for X?

[Jireh Loreaux]

Can someone explain why the last one doesn't work?

import Mathlib.Data.ZMod.Defs

variables (M : Type*) [inst : DecidableEq M]

#synth DecidableEq (Multiplicative M) -- fun a b ↦ inst a b
#synth DecidableEq (ZMod 2) -- fun a b ↦ ZMod.decidableEq 2 a b
#synth DecidableEq (Multiplicative (ZMod 2)) -- failed to synthesize

Do we need these instances?

instance (M : Type*) [DecidableEq M] : DecidableEq (Multiplicative M) := inferInstance
instance (M : Type*) [DecidableEq M] : DecidableEq (Additive M) := inferInstance

[Eric Wieser]

That first one really shouldn't work

[Jireh Loreaux]

That's kind of what i figured, so we want these instances, right?

[Jireh Loreaux]

Should we raise an issue on the Lean 4 repo that the first one works at all?

[Jireh Loreaux]

#8072

[Kyle Miller]

minimized:

def myId (α : Type) : Type := α

-- Succeeds:
def foo (M : Type) [DecidableEq M] : DecidableEq (myId M) := inferInstance
-- Fails:
def foo' : DecidableEq (myId Nat) := inferInstance

[Kyle Miller]

It seems like the first only works because there's a local instance

[Kyle Miller]

Reading the code a bit, my understanding is that the way instance synthesis works here is that it collects all global instances that match in a syntactic way, as it collects all local instances filtered by just typeclass name. Then, it does a defeq check for everything in this list (that check is in tryResolve when you set set_option trace.Meta.synthInstance true). This means local instances don't care at all about syntax like global instances do.

[Jireh Loreaux]

When you say "local" you don't mean attribute [local instance] right? You mean local in the sense of provided within the declaration?

[Kyle Miller]

Yes, I mean "local" in the sense that it's a variable in the local context. These are called "local instances" inside the Lean codebase.

[Kyle Miller]

Hmm, the first one succeeds, but the second one fails:

def myId (α : Type) : Type := α

def foo1 [DecidableEq Nat] : DecidableEq (myId Nat) := inferInstance
def foo2 [Inhabited Nat] : Inhabited (myId Nat) := inferInstance

[Kyle Miller]

Does whether an argument is implicit or not change reducibility rules? In the first, myId Nat for typeclass inference purposes is technically an implicit argument to Eq

[Kyle Miller]

So maybe this problem is actually not a big deal since it'd only apply to abbreviations (like DecidableEq) that expand in such a way that an explicit argument becomes implicit?

[Eric Wieser]

This looks like a bug to me; I think it would be good to explore being stricter about it and seeing what breaks.

[Jireh Loreaux]

Yes, that definitely seems like a bug.