Zulip Chat Archive

Stream: new members

Topic: typeclass inference doesn't find instance?

Felix Weilacher (Dec 06 2022 at 15:01):

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) :=
  intros S Sct hS,
  simp_rw[eventually_countable_ball Sct],
  exact hS,

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 :=
  --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?

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 (Dec 06 2022 at 15:05):

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 (Dec 06 2022 at 15:08):

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 (Dec 06 2022 at 15:30):

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.

Last updated: Dec 20 2023 at 11:08 UTC