feat(tactic/core): derive handler for simple instances

src/tactic/core.lean

@@ -1144,7 +1144,29 @@ do e ← get_env,
   since it is expensive to execute `get_mathlib_dir` many times. -/
 meta def is_in_mathlib (n : name) : tactic bool :=
 do ml ← get_mathlib_dir, e ← get_env, return $ e.is_prefix_of_file ml n
+/--
+Tries to derive unary instances by unfolding the newly introduced type.
 
+For example,
+```
+@[derive ring] def new_int : Type := ℤ
+```
+adds an instance `ring new_int`, defined to be the instance of `ring ℤ` found by `apply_instance`.
 
+Multiple instances can be added with `@[derive [ring, module ℝ]]`.
+-/
+@[derive_handler] meta def delta_instance : derive_handler :=
+λ cls tp,
+(do tp' ← mk_const tp,
+   tgt ← to_expr ``(%%cls %%tp'),
+   (_, v) ← solve_aux tgt (delta_target [tp] >> apply_instance >> done),
+   v ← instantiate_mvars v,
+   nm ← get_unused_name $ tp ++
+     match tgt with
+     | expr.app (expr.const nm _) _ := nm
+     | _ := "inst"
+     end,
+   add_decl $ mk_definition nm [] tgt v,
+   set_basic_attribute `instance nm tt,
+   return tt) <|> return ff
 end tactic
-open tactic

test/delta_instance.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2019 Robert Y. Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Y. Lewis
+-/
+
+import tactic.core
+
+@[derive ring] def T := ℤ
+
+class binclass (T1 T2 : Type)
+
+instance : binclass ℤ ℤ := ⟨_, _⟩
+
+@[derive [ring, binclass ℤ]] def U := ℤ
+
+@[derive λ α, binclass α ℤ] def V := ℤ