Instance caching not always working

[sgouezel]

Following example based on mathlib (I have not been able to minimise):

import topology.algebra.infinite_sum

set_option trace.class_instances true

lemma blah (α : Type*) [topological_space α] (f : ℝ → α) : continuous f :=
begin
  apply continuous.mul,
end

The line apply continuous.mul fails, as it should, but the instance search gives a lot of caching failure for linear_ordered_ring α, and no cached failure at all. simp [continuous.mul] has the same problem.

[gebner]

Thanks for minimizing this.

I wouldn't be surprised if the culprit was type_context_old::mk_nested_instance:

// HACK(gabriel): do not reuse type-class cache for nested resolution problems
// For one example that easily breaks, see the default field values in `init/control/lawful.lean`
// TODO(gabriel): allow local caching