Stream: Coq devs & plugin devs

Topic: NonStuckFailure


view this post on Zulip Janno (Nov 08 2023 at 14:20):

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?

view this post on Zulip Gaëtan Gilbert (Nov 08 2023 at 15:08):

there's a best_effort:true in resolve_all_evars so maybe it gets called that way somehow

view this post on Zulip Janno (Nov 08 2023 at 15:20):

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.

view this post on Zulip Gaëtan Gilbert (Nov 08 2023 at 15:21):

I think this is the path called by https://github.com/coq/coq/issues/6583 (apply calls tc resolution on unrelated goals)

view this post on Zulip Janno (Nov 09 2023 at 11:37):

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.

view this post on Zulip Janno (Nov 09 2023 at 11:45):

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