typeclass inference doesn't find instance?

Stream: new members

[Felix Weilacher]

I've occasionally run into a situation where I know an instance for some class exists (because apply_instance finds it) but the instance isn't found automatically in the way I expect. Here is a recent example I ran into:

import order.filter.countable_Inter
import order.filter.curry

instance countable_Inter_filter_curry {α β: Type*} {f : filter α} {g : filter β}
  [countable_Inter_filter f] [countable_Inter_filter g] : countable_Inter_filter (f.curry g) :=
begin
  constructor,
  intros S Sct hS,
  dsimp[filter.curry],
  simp_rw[eventually_countable_ball Sct],
  exact hS,
end

example {α β: Type*} {f : filter α} {g : filter β}
  [countable_Inter_filter f] [countable_Inter_filter g]
  {S : set (set (α × β))} (Sct : S.countable) (hS : ∀ s ∈ S, s ∈ f.curry g) :
  ⋂₀ S ∈ f.curry g :=
begin
  --exact (countable_sInter_mem Sct).mpr hS, this works, but i'd like to be able to use rw
  rw countable_sInter_mem Sct, {exact hS},
  apply_instance, --why wasn't this found in the rewrite?
end

The theorem countable_sInter_mem invoked in the example requires knowing that some filter is a countable_Inter_filter. When I rw with the theorem, it creates a goal to show the filter is a countable_Inter_filter instead of using the instance I just registered. If apply_instance closes the goal, why isn't the instance found during the rw?

[Mario Carneiro]

it's an order of operations issue. What happens is that first the term countable_sInter_mem Sct is elaborated, and without any context one of the typeclasses can't be determined yet. This becomes a subgoal. Then the term with metavariables is used to search for matching subexpressions in the goal, which often solves the subgoals before they appear, but in this case not. At this point we have lost track of which of the subgoals are intended to be solved by typeclass inference so we can't just go back and clean up the remaining goals with apply_instance without potentially calling it on things that shouldn't be solved that way

[Alex J. Best]

You could do

  rw countable_sInter_mem,
  exact hS,
  exact Sct,

in this situation instead if you prefer, which sort of sidesteps the issue mario explains

[Felix Weilacher]

Thanks for the explanation! I think I follow you and I think I understand why Alex's suggestion works. I find it pretty unintuitive that providing less information (by leaving out Sct) causes the inference to succeed, though.