From f2c5342aaa03979510f0963df4bb9b5411bf835e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 8 Sep 2017 18:22:34 +0200
Subject: [PATCH] feat(init/meta/derive): handle parameters, parameter
 instances, universes

---
 library/init/meta/derive.lean       | 21 +++++++++++++++++----
 tests/lean/derive.lean              |  4 ++--
 tests/lean/derive.lean.expected.out |  7 ++++---
 3 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/library/init/meta/derive.lean b/library/init/meta/derive.lean
index 6f78e8fc85..a1e8fde559 100644
--- a/library/init/meta/derive.lean
+++ b/library/init/meta/derive.lean
@@ -45,11 +45,24 @@ meta def instance_derive_handler (cls : name) (tac : tactic unit) : derive_handl
 λ p n,
 if p.is_constant_of cls then
 do decl ← get_decl n,
-   -- TODO: parameters, parameter instances, universes
-   ty ← mk_app cls [expr.const n []],
-   (_, val) ← tactic.solve_aux ty tac,
+   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 tgt : expr := expr.const n (decl.univ_params.map level.param),
+   ⟨params, _⟩ ← mk_local_pis decl.type,
+   let params := params.take (env.inductive_num_params n),
+   let tgt := tgt.mk_app params,
+   tgt ← mk_app cls [tgt],
+   tgt ← params.mfoldr (λ param tgt,
+   do param_cls ← mk_app cls [param],
+      -- TODO(sullrich): omit some typeclass parameters based on usage of `param`?
+      let tgt := expr.pi `a binder_info.inst_implicit param_cls tgt,
+      pure $ tgt.bind_pi param
+   ) tgt,
+   (_, val) ← tactic.solve_aux tgt (intros >> tac),
    val ← instantiate_mvars val,
-   add_decl (declaration.defn (n ++ cls) [] ty val reducibility_hints.abbrev tt),
+   let trusted := decl.is_trusted ∧ cls_decl.is_trusted,
+   add_decl (declaration.defn (n ++ cls) decl.univ_params tgt val reducibility_hints.abbrev trusted),
    set_basic_attribute `instance (n ++ cls) tt,
    pure true
 else pure false
diff --git a/tests/lean/derive.lean b/tests/lean/derive.lean
index e26b60da98..ff8c8dd59e 100644
--- a/tests/lean/derive.lean
+++ b/tests/lean/derive.lean
@@ -1,7 +1,7 @@
 @[derive [decidable_eq, inhabited, has_sizeof]]
-inductive foo
+inductive foo (α β : Type*)
 | bar : ℕ → foo
-| baz : foo
+| baz : foo → α → foo
 
 #check foo.decidable_eq
 #check foo.inhabited
diff --git a/tests/lean/derive.lean.expected.out b/tests/lean/derive.lean.expected.out
index fcccb03801..ffa23155a4 100644
--- a/tests/lean/derive.lean.expected.out
+++ b/tests/lean/derive.lean.expected.out
@@ -1,3 +1,4 @@
-foo.decidable_eq : decidable_eq foo
-foo.inhabited : inhabited foo
-foo.has_sizeof : has_sizeof foo
+foo.decidable_eq :
+  Π (α : Type u_1) [a : decidable_eq α] (β : Type u_2) [a : decidable_eq β], decidable_eq (foo α β)
+foo.inhabited : Π (α : Type u_1) [a : inhabited α] (β : Type u_2) [a : inhabited β], inhabited (foo α β)
+foo.has_sizeof : Π (α : Type u_1) [a : has_sizeof α] (β : Type u_2) [a : has_sizeof β], has_sizeof (foo α β)