how to make deriving handler

Stream: general

[Asei Inoue]

I want to understand how to make deriving handler, so I want to create a very simple toy example.

How to resolve this error?

import Lean

open Lean Elab Command

universe u

class ToUnit (α : Type u) where
  toUnit : α → Unit

instance : ToUnit Nat where
  toUnit := fun _ => ()

#guard ToUnit.toUnit 42 = ()

def deriveToUnitInstance (declNames : Array Name) : CommandElabM Bool := do
  for declName in declNames do
    let term := quote (k := `term) <| declName
    let cmd ← `(command| instance : ToUnit $term := ⟨fun _ => ()⟩)
    elabCommand cmd
  return true

/-
Application type mismatch: The argument
  `Foo
has type
  Name
of sort `Type` but is expected to have type
  Type ?u.1135
of sort `Type (?u.1135 + 1)` in the application
  ToUnit `Foo
-/
run_cmd
  deriveToUnitInstance #[`Foo]

initialize
  registerDerivingHandler ``ToUnit deriveToUnitInstance

[Robin Arnez]

Replace quote (k := `term) with mkCIdent

[Asei Inoue]

@Robin Arnez Thank you!!!!!!

[Robin Arnez]

quote x is meant to create a term that evaluates to x

[Robin Arnez]

mkCIdent nm instead creates an identifier term that resolves to the global declaration nm

[Robin Arnez]

mkIdent nm just creates an identifier which will go through namespace resolution