Instance cache not always preserved between simp invocations

[sgouezel]

Here is an example where instance search done by the first simp is done again by the second simp, without taking advantage of the cache.

set_option trace.class_instances true

lemma foo (α : Type*) (x y z t : α) (hx : x = x) (hy : y = y) : z = t :=
begin
  simp at hx,
  simp at hy,
  sorry
end

The instance trace for both simp calls is as follows (while I would expect the second to be shorter than the first):

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton (Type u_1) := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u_1) := @pi.subsingleton ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u_1) := decidable.subsingleton ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton (Type u_1) := subsingleton_prop ?x_5
failed is_def_eq
[class_instances] caching failure for subsingleton (Type u_1)
[class_instances] caching failure for subsingleton (Type u_1)
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton α := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @pi.subsingleton ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := decidable.subsingleton ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_prop ?x_5
failed is_def_eq
[class_instances] caching failure for subsingleton α
[class_instances] caching failure for subsingleton α
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : subsingleton α := punit.subsingleton
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := @pi.subsingleton ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := decidable.subsingleton ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : subsingleton α := subsingleton_prop ?x_5
failed is_def_eq
[class_instances] caching failure for subsingleton α
[class_instances] caching failure for subsingleton α