inferInstance

Stream: lean4

[Jeremy Avigad]

I am trying to infer decidable equality for a defined type by unfolding it. In Lean 3, we'd use unfold and apply_instance. In Lean 4, I can do this:

def Foo := Nat
instance : DecidableEq Foo := @inferInstance (DecidableEq Nat) _

This also works just fine:

instance : DecidableEq Foo := show DecidableEq Nat from inferInstance

Does anyone know if there is a better idiom to use?

[Jeremy Avigad]

This also works:

instance : DecidableEq Foo := by simp [Foo]; exact inferInstance

[Jannis Limperg]

inferInstanceAs is probably what you want.

[Sebastian Ullrich]

It would be nice to have a deriving handler for this

[Sebastian Ullrich]

Ah, well, the current API doesn't quite allow for that yet

[Jeremy Avigad]

Yes, I am also doing the same thing to transfer Repr instances. But two lines of boilerplate is no problem. I am really enjoying Lean 4.

[Mario Carneiro]

Sebastian Ullrich said:

It would be nice to have a deriving handler for this

Actually, this came up in synport. Lean 3 has a deriving handler for this, the "delta derive handler", but lean 4 expects deriving handlers to be associated to a particular typeclass, and I don't see a space for fallback handlers

[Mac]

In Haskell, this type of deriving strategy is called 'newtype deriving'. Even if the current deriving syntax doesn't support it. I imagine one could write a deriving instance C for A from B to which elaborates to something like instance : C A := inferInstanceAs (C B) (for the unary case). There may even be a away to smartly infer B.

[Mario Carneiro]

But that has to work for all C

[Mario Carneiro]

Also, the syntax expects a unary typeclass which isn't always the case

[Mac]

Yeah, my example was just a trivial special case. There would be more nuances to getting it to work properly generally.