Building derive_handlers

Stream: metaprogramming / tactics

[Eric Wieser]

What's going wrong here? How can I get to the point where I can at least see my trace output?

@[derive_handler] meta def decidable_rel_derive_handler : derive_handler :=
instance_derive_handler ``decidable_rel $
do env ← tactic.get_env,
   tactic.fail format!"Not implemented"

set_option trace.app_builder true

@[derive decidable_rel]
inductive both_zero : ℕ → ℕ → Prop
| zero : both_zero 0 0

(fails with

[app_builder] failed to create an 'decidable_rel'-application, failed to solve unification constraint for #1 argument (?x_0 → ?x_0 → Prop =?= Prop)

which I don't know the origin of)

[Alex J. Best]

You need to go one level deeper, into docs#instance_derive_handler

open tactic
/-- Given a tactic `tac` that can solve an application of `cls` in the right context,
    `instance_derive_handler` uses it to build an instance declaration of `cls n`. -/
meta def instance_derive_handler' (cls : name) (tac : tactic unit) (univ_poly := tt)
  (modify_target : name → list expr → expr → tactic expr := λ _ _, pure) : derive_handler :=
λ p n,
if p.is_constant_of cls then
do decl ← get_decl n,
   cls_decl ← get_decl cls,
   env ← get_env,
   guard (env.is_inductive n) <|> fail format!"failed to derive '{cls}', '{n}' is not an inductive type",
   let ls := decl.univ_params.map $ λ n, if univ_poly then level.param n else level.zero,
   -- incrementally build up target expression `Π (hp : p) [cls hp] ..., cls (n.{ls} hp ...)`
   -- where `p ...` are the inductive parameter types of `n`
   let tgt : expr := expr.const n ls,
   ⟨params, _⟩ ← mk_local_pis (decl.type.instantiate_univ_params (decl.univ_params.zip ls)),
   trace ">>>>>",
   let tgt := tgt.mk_app params,
   trace "###########",
   tgt ← mk_app cls [tgt],
   trace "!!!!!!!!!!!",
   tgt ← modify_target n params tgt,
   tgt ← params.enum.mfoldr (λ ⟨i, param⟩ tgt,
   do -- add typeclass hypothesis for each inductive parameter
      tgt ← do {
        guard $ i < env.inductive_num_params n,
        param_cls ← mk_app cls [param],
        -- TODO(sullrich): omit some typeclass parameters based on usage of `param`?
        pure $ expr.pi `a binder_info.inst_implicit param_cls tgt
      } <|> pure tgt,
      pure $ tgt.bind_pi param
   ) tgt,
   (_, val) ← tactic.solve_aux tgt (intros >> tac),
   val ← instantiate_mvars val,
   let trusted := decl.is_trusted ∧ cls_decl.is_trusted,
   add_protected_decl
     (declaration.defn (n ++ cls)
             (if univ_poly then decl.univ_params else [])
             tgt val reducibility_hints.abbrev trusted),
   set_basic_attribute `instance (n ++ cls) tt,
   pure true
else pure false
@[derive_handler] meta def decidable_rel_derive_handler : derive_handler :=
instance_derive_handler' ``decidable_rel $
do env ← tactic.get_env,
   tactic.fail format!"Not implemented"

set_option trace.app_builder true

@[derive decidable_rel]
inductive both_zero : ℕ → ℕ → Prop
| zero : both_zero 0 0

[Alex J. Best]

The error is coming from the line between ##### and !!!!!!!!!!

[Alex J. Best]

Commenting out let tgt := tgt.mk_app params, gets me to your not implemented FWIW