From dbe10334273da03d26ddd3d47c4d1fef19461edf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 12 Sep 2017 15:16:47 -0700
Subject: [PATCH] fix(library/init/meta/mk_has_sizeof_instance): indexed
 families

see #1818
---
 library/init/meta/mk_has_sizeof_instance.lean |  5 ++++-
 tests/lean/run/has_sizeof_indices.lean        | 15 +++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/has_sizeof_indices.lean

diff --git a/library/init/meta/mk_has_sizeof_instance.lean b/library/init/meta/mk_has_sizeof_instance.lean
index 7ff9a7b6d6..157dbbab2c 100644
--- a/library/init/meta/mk_has_sizeof_instance.lean
+++ b/library/init/meta/mk_has_sizeof_instance.lean
@@ -64,10 +64,13 @@ do I_name ← get_has_sizeof_type_name,
    env ← get_env,
    v_name : name ← return `_v,
    F_name : name ← return `_F,
+   let num_indices := inductive_num_indices env I_name,
+   let idx_names := list.map (λ (p : name × nat), mk_num_name p.fst p.snd)
+                             (list.zip (list.repeat `idx num_indices) (list.iota num_indices)),
    -- Use brec_on if type is recursive.
    -- We store the functional in the variable F.
    if is_recursive env I_name
-   then intro `_v >>= (λ x, induction x [v_name, F_name] (some $ I_name <.> "brec_on") >> return ())
+   then intro `_v >>= (λ x, induction x (idx_names ++ [v_name, F_name]) (some $ I_name <.> "brec_on") >> return ())
    else intro v_name >> return (),
    arg_names : list (list name) ← mk_constructors_arg_names I_name `_p,
    get_local v_name >>= λ v, cases v (join arg_names),
diff --git a/tests/lean/run/has_sizeof_indices.lean b/tests/lean/run/has_sizeof_indices.lean
new file mode 100644
index 0000000000..dd73833b03
--- /dev/null
+++ b/tests/lean/run/has_sizeof_indices.lean
@@ -0,0 +1,15 @@
+universes u
+
+inductive foo : nat → Type
+| baz (n : nat) : foo n → foo (nat.succ n)
+
+lemma foo.size (α β : Type u) (n a : ℕ) : has_sizeof (foo a) :=
+by tactic.mk_has_sizeof_instance
+
+inductive bla : nat → bool → Type
+| mk : bla 0 ff
+| baz (n : nat) : bla n ff → bla (nat.succ n) tt
+| boo (n : nat) : bla n tt → bla (nat.succ n) ff
+
+lemma bla.size (α β : Type u) (a : ℕ) (t : bool)  : has_sizeof (bla a t) :=
+by tactic.mk_has_sizeof_instance