fix(init/meta/derive): handle indexed families

library/init/meta/derive.lean

@@ -56,14 +56,17 @@ do decl ← get_decl n,
    -- 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)),
-   let params := params.take (env.inductive_num_params n),
    let tgt := tgt.mk_app params,
    tgt ← mk_app cls [tgt],
    tgt ← modify_target n params 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,
+   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),

tests/lean/derive.lean

@@ -1,8 +1,18 @@
-@[derive [decidable_eq, inhabited, has_sizeof]]
+@[derive [decidable_eq, inhabited, has_reflect, has_sizeof]]
 inductive foo (α β : Type*)
 | bar : ℕ → foo
 | baz : foo → α → foo
 
 #check foo.decidable_eq
 #check foo.inhabited
+#check foo.has_reflect
 #check foo.has_sizeof
+
+-- indexed families
+
+@[derive decidable_eq]
+inductive {u} foo' (α β : Type u) (n : nat) : nat → Type u
+| bar : ℕ → foo' 0
+| baz (n : nat) : foo' n → α → foo' (nat.succ n)
+
+#check foo'.decidable_eq

tests/lean/derive.lean.expected.out

@@ -1,4 +1,10 @@
 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_reflect :
+  Π (α : Type) [a : has_reflect α] (β : Type) [a : has_reflect β] [a : reflected α] [a : reflected β],
+    has_reflect (foo α β)
 foo.has_sizeof : Π (α : Type u_1) [a : has_sizeof α] (β : Type u_2) [a : has_sizeof β], has_sizeof (foo α β)
+foo'.decidable_eq :
+  Π (α : Type u_1) [a : decidable_eq α] (β : Type u_1) [a : decidable_eq β] (n a : ℕ),
+    decidable_eq (foo' α β n a)