Custom instance deriving handlers

Stream: lean4

[Matej Penciak]

This is something of a followup to this very old thread:

I have some experience with metaprogramming and wanted to take a crack and writing an extension to the instance deriving mechanism, but I'm quickly realizing I'm out of my depth here. I know for a fact I'm doing things wrong because I'm always running into the default handlers have not been implemented yet, ... error no matter how simple of an example I try.

I first started by copying the template from the deriving BEq file, and tried to strip it down to the easiest possible cases, but I'm finding debugging tricky, so I'm not sure where to even begin fixing my problems. Eventually I just copy and pasted the whole BEq deriving file and tried to modify it for NBEq (not BEq) and I was still getting the same error, which made me think I'm fundamentally misunderstanding things...

I've included a minimal (non)working example below if that might help in figuring out what I'm doing wrong

import Lean.Elab.Deriving.Basic
import Lean.Elab.Deriving.Util

universe u

class Foo (α : Sort u) where
  foo : String

section making_handler

namespace Lean.Elab.Deriving.Foo
open Lean.Parser.Term
open Meta

open Command

private def mkFooFuns (ctx : Context) (name : Name) : TermElabM Syntax := do
  let auxFunName := ctx.auxFunNames[0]
  `(private def $(mkIdent auxFunName):ident : String := "Bar")

def mkFooInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
  let ctx ← mkContext "foo" declName
  let cmds := #[← mkFooFuns ctx declName] ++ (← mkInstanceCmds ctx `Foo #[declName])
  return cmds

def mkFooHandler (declNames : Array Name) : CommandElabM Bool := do
  let cmds ← liftTermElabM none <| mkFooInstanceCmds declNames[0]
  cmds.forM elabCommand
  return true

initialize
  registerBuiltinDerivingHandler `Foo mkFooHandler

end Lean.Elab.Deriving.Foo
end making_handler

section testing_handler

inductive test where
  | con1 : test
  | con2 : test
deriving Foo -- default handlers have not been implemented yet, class: 'Foo' types: [test]

end testing_handler

[Matej Penciak]

(I should also mention that I tried having the instance handler in a separate module and importing it, but that doesn't work either)