fix(library/data/tuple): modify definition to make sure we can compile it using new type class resolution procedure

The issue are universe level constraints that cannot be solved by the
new procedure.

library/data/tuple.lean

@@ -34,7 +34,7 @@ namespace tuple
   | (succ n) := inhabited.mk (inhabited.value h :: inhabited.value (is_inhabited n))
 
   protected definition has_decidable_eq [instance] [h : decidable_eq A] : ∀ (n : nat), decidable_eq (tuple A n) :=
-  _
+  λ n, subtype.has_decidable_eq
 
   definition head {n : nat} : tuple A (succ n) → A
   | (tag []     h) := by contradiction