I am seeing Debug: Goal 1 has no more solutions, returning exception: NonStuckFailure
in my typeclasses eauto debug output. AFAICT there is only a single code path that raises this exception and it is guarded by info.search_best_effort.
. My debug log is the result of a call to Class_tactics.Search.eauto_tac
with ~best_effort:false
so I think I shouldn't ever see the NonStuckFailure
exception. Is that correct?
there's a best_effort:true
in resolve_all_evars so maybe it gets called that way somehow
I think that one is only used in solve_all_instances
. Although I see that that in turn is used here:
let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
?(fail=true) env evd =
if not (has_typeclasses filter evd) then evd
else solve_all_instances env evd filter unique fail
and resolve_typeclasses
is used in several places. But I don't know that any of those would be called from eauto_tac
.
I think this is the path called by https://github.com/coq/coq/issues/6583 (apply calls tc resolution on unrelated goals)
It took us quite a while to get to the bottom of this. We are creating evars for arguments of a lemma and accidentally made them typeclass candidates even when they were dependent variables. Then, when we apply the lemma, the nondependent assumptions (correctly marked TC candidates) are resolved via TC search and a hint extern calling eassumption
ends up triggering on the first TC goal. eassumption
succeeds and instantiates the dependent evar but for some reason the call to try_resolve_typeclasses
in w_unify_core_0
now takes over from the initial typeclass search and starts solving remaining assumptions of the lemma. Unfortunately, this happens with best_effort:true
. Our lemma had the shape forall n, solvable n -> not_solvable -> super_expensive_subgoal -> conclusion
with solvable n
being solved by eassumption
. Despite not_solvable
having no solution, the inner TC search now ends up running the search for super_expensive_subgoal
.
I wonder if we shouldn't stop turning things into typeclass candidates altogether. I honestly don't quite understand when it comes into play. We usually turn all remaining evars into new goals manually and call typeclasses eauto
on them. Does that tactic even care about the typeclass_candidate
flag?
Last updated: Oct 13 2024 at 01:02 UTC