More unified judgment type and All_local_env

[yannl35133]

@JasonGross This PR changes many low-level elements and seems to break quite seriously the quotation part, which I don't know how to repair. I may have to remove it from the CI if I want it to still check all other components. Can I have your opinion on how to find a solution ? (This PR is the first step towards supporting SProp in MetaCoq)

[JasonGross]

I expect the quotation part should not be too hard to repair; the bulk of the code is just mirror of the rest of the development where there's a definition for every record, inductive, and type-valued-definition-containing-a-match. Assuming there are no new types that hold either informative functions (things like "here's a map from names to universes, represented as a function") nor hold Types nor live in Prop while being undecidable, I expect adaptation to be pretty straightforward. I don't have much time to spend on this, but I'm happy to assist with fixing. Could you point me at what breaks / what breaks that you don't know how to fix?

[yannl35133]

I'm stuck there here, I can't quote quote_All_local_env_over_sorting, presumably because I can't quote quote_lift_sorting, this one I just don't know how to.

[JasonGross]

My guess is that quote_lift_sorting just needs some extra arguments that say that not only can you quote elements of check and sorting but also check and sorting can themselves be quoted, i.e., try

- #[export] Instance quote_lift_sorting {check sorting j} {quote_check : forall tm, j_term j = Some tm -> ground_quotable (check tm (j_typ j))} {quote_sorting : forall u, ground_quotable (sorting (j_typ j) u)} : ground_quotable (@lift_sorting check sorting j) := ltac:(cbv [lift_sorting]; exact _).
+ #[export] Instance quote_lift_sorting {check sorting j} {qcheck : quotation_of check} {qsorting : quotation_of sorting} {quote_check : forall tm, j_term j = Some tm -> ground_quotable (check tm (j_typ j))} {quote_sorting : forall u, ground_quotable (sorting (j_typ j) u)} : ground_quotable (@lift_sorting check sorting j) := ltac:(cbv [lift_sorting]; exact _).

Does this work? (You shouldn't need qj : quotation_of j because I expect there should be an instance of ground_quotable judgment already available at this point; if not, then that should be added / exposed in the appropriate place.)

[JasonGross]

(Sorry, I wrote this all yesterday and then forgot to click "comment")

Btw, if you stick

#[local] Instance:debug_opt := true.

before the failing #[export] Instance quote_lift_sorting ..., you'll see the printout starts with

(Ast.tVar "check"%bs)
(Ast.tVar "check"%bs)
(quotation_of check)

which indicates that it's having trouble finding quotation_of check. Adding {qcheck : quotation_of check} to the argument list makes the printout start with

(Ast.tVar "sorting"%bs)
(Ast.tVar "sorting"%bs)
(quotation_of sorting)

and then adding {qsorting : quotation_of sorting} makes the instance go through.

Debugging the proof below the same way gives an output that starts with

(Ast.tVar "Hc"%bs)
(Ast.tVar "Hc"%bs)
(quotation_of Hc)

If I do

Set Typeclasses Debug Verbosity 2.
try pose proof (_ : quotation_of Hc).

I see

this log

``` Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2211 : (quotation_of Hc) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2211 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for (quotation_of Hc) without backtracking Debug: 1.1: (*external*) (is_var t; destruct t) on (quotation_of Hc) failed with: pattern-matching failed Debug: 1.1: (*external*) (progress repeat autounfold with quotation in *) on (quotation_of Hc), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2234 : (quotation_of Hc) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2234 status: initial Debug: considering goal 1 of status initial Debug: 1.1-1 : (quotation_of Hc) Debug: calling eauto recursively at depth 2 on 1 subgoals Debug: 1.1-1: looking for (quotation_of Hc) without backtracking Debug: 1.1-1.1: (*external*) (is_var t; destruct t) on (quotation_of Hc) failed with: pattern-matching failed Debug: 1.1-1.1: (*external*) (progress repeat autounfold with quotation in *) on (quotation_of Hc) failed with: Failed to progress. Debug: 1.1-1.1: (*external*) (progress intros) on (quotation_of Hc) failed with: Failed to progress. Debug: 1.1-1.1: (*external*) (destruct t) on (quotation_of Hc) failed with: pattern-matching failed Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2282 : debug_opt Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2282 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for debug_opt without backtracking Debug: 1.1: exact debug_opt_instance_0 on debug_opt, 0 subgoal(s) Debug: 1.1: after exact debug_opt_instance_0 finished, 0 goals are shelved and unsolved ( ) Debug: Goal 1 has a success, continuing resolution Debug: Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run. Stuck: Failed: Initial: Debug: Result goals after fixpoint: 0 goals: Debug: after eauto_tac_stuck: 0 goals: Debug: The tactic trace is: simple refine debug_opt_instance_0;shelve_goals Debug: Finished resolution with a complete solution. Old typeclass evars not concerned by this resolution = Shelf = Debug: New typeclass evars are: Debug: 1.1-1.1: (*external*) (replace_quotation_of_goal ltac:(())) on (quotation_of Hc) failed with: In nested Ltac calls to "replace_quotation_of_goal" and "run_template_program (constr) (tactic)", last call failed. Avoiding loops Debug: 1.1-1.1: simple apply @quote_ground on (quotation_of Hc), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2283 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2283 status: initial Debug: considering goal 1 of status initial Debug: 1.1-1.1-1 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: calling eauto recursively at depth 3 on 1 subgoals Debug: 1.1-1.1-1: looking for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) without backtracking Debug: 1.1-1.1-1.1: simple apply quote_cproperty on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Cannot unify (MCOption.option_default (fun tm : term => checking Γ tm (j_typ (TermTyp b t))) (j_term (TermTyp b t)) unit) and (checking Γ b (j_typ (TermTyp b t))) Debug: 1.1-1.1-1.1: (*external*) (is_var t; destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.1-1.1-1.1: (*external*) (progress repeat autounfold with quotation in *) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Failed to progress. Debug: 1.1-1.1-1.1: (*external*) (progress intros) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Failed to progress. Debug: 1.1-1.1-1.1: (*external*) (destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.1-1.1-1: no match for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))), 5 possibilities Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.1-1.1: simple apply @quote_ground failed with: Proof-search failed. Debug: 1.1-1.2: simple apply @BasicAst.quotation_of_mfixpoint failed with: Cannot unify (quotation_of ?M20949) and (quotation_of Hc) Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2308 : debug_opt Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2308 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for debug_opt without backtracking Debug: 1.1: exact debug_opt_instance_0 on debug_opt, 0 subgoal(s) Debug: 1.1: after exact debug_opt_instance_0 finished, 0 goals are shelved and unsolved ( ) Debug: Goal 1 has a success, continuing resolution Debug: Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run. Stuck: Failed: Initial: Debug: Result goals after fixpoint: 0 goals: Debug: after eauto_tac_stuck: 0 goals: Debug: The tactic trace is: simple refine debug_opt_instance_0;shelve_goals Debug: Finished resolution with a complete solution. Old typeclass evars not concerned by this resolution = Shelf = Debug: New typeclass evars are: (Ast.tVar "Hc"%bs) Debug: 1.1-1.2: (*external*) (make_quotation_of_goal ltac:(())) failed with: In nested Ltac calls to "make_quotation_of_goal" and "run_template_program (constr) (tactic)", last call failed. bound argument is not ground Debug: 1.1-1.2: simple apply @qquotation on (quotation_of Hc), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2309 : (inductive_quotation_of Hc) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2309 status: initial Debug: considering goal 1 of status initial Debug: 1.1-1.2-1 : (inductive_quotation_of Hc) Debug: calling eauto recursively at depth 3 on 1 subgoals Debug: 1.1-1.2-1: looking for (inductive_quotation_of Hc) without backtracking Debug: 1.1-1.2-1.1: (*external*) (progress intros) on (inductive_quotation_of Hc) failed with: Failed to progress. Debug: 1.1-1.2-1.1: (*external*) simple notypeclasses refine (default_inductive_quotation_of _ _) on (inductive_quotation_of Hc), 2 subgoal(s) Debug: Launching resolution fixpoint on 2 goals: ?X2311 : (quotation_of Hc) ?X2313 : (cls_is_true match ?qt with | Ast.tInd _ _ => true | _ => false end) Debug: Calling fixpoint on : 2 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2311 status: initial Goal 2 evar: ?X2313 status: initial Debug: considering goal 1 of status initial Debug: 1.1-1.2-1.1-1 : (quotation_of Hc) Debug: calling eauto recursively at depth 4 on 1 subgoals Debug: 1.1-1.2-1.1-1: looking for (quotation_of Hc) with backtracking Debug: 1.1-1.2-1.1-1.1: (*external*) (is_var t; destruct t) on (quotation_of Hc) failed with: pattern-matching failed Debug: 1.1-1.2-1.1-1.1: (*external*) (progress repeat autounfold with quotation in *) on (quotation_of Hc) failed with: Failed to progress. Debug: 1.1-1.2-1.1-1.1: (*external*) (progress intros) on (quotation_of Hc) failed with: Failed to progress. Debug: 1.1-1.2-1.1-1.1: (*external*) (destruct t) on (quotation_of Hc) failed with: pattern-matching failed Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2338 : debug_opt Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2338 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for debug_opt without backtracking Debug: 1.1: exact debug_opt_instance_0 on debug_opt, 0 subgoal(s) Debug: 1.1: after exact debug_opt_instance_0 finished, 0 goals are shelved and unsolved ( ) Debug: Goal 1 has a success, continuing resolution Debug: Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run. Stuck: Failed: Initial: Debug: Result goals after fixpoint: 0 goals: Debug: after eauto_tac_stuck: 0 goals: Debug: The tactic trace is: simple refine debug_opt_instance_0;shelve_goals Debug: Finished resolution with a complete solution. Old typeclass evars not concerned by this resolution = Shelf = Debug: New typeclass evars are: Debug: 1.1-1.2-1.1-1.1: (*external*) (replace_quotation_of_goal ltac:(())) on (quotation_of Hc) failed with: In nested Ltac calls to "replace_quotation_of_goal" and "run_template_program (constr) (tactic)", last call failed. Avoiding loops Debug: 1.1-1.2-1.1-1.1: simple apply @quote_ground on (quotation_of Hc), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2339 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2339 status: initial Debug: considering goal 1 of status initial Debug: 1.1-1.2-1.1-1.1-1 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: calling eauto recursively at depth 5 on 1 subgoals Debug: 1.1-1.2-1.1-1.1-1: looking for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) with backtracking Debug: 1.1-1.2-1.1-1.1-1.1: simple apply quote_cproperty on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Cannot unify (MCOption.option_default (fun tm : term => checking Γ tm (j_typ (TermTyp b t))) (j_term (TermTyp b t)) unit) and (checking Γ b (j_typ (TermTyp b t))) Debug: 1.1-1.2-1.1-1.1-1.1: (*external*) (is_var t; destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.1-1.2-1.1-1.1-1.1: (*external*) (progress repeat autounfold with quotation in *) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Failed to progress. Debug: 1.1-1.2-1.1-1.1-1.1: (*external*) (progress intros) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Failed to progress. Debug: 1.1-1.2-1.1-1.1-1.1: (*external*) (destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.1-1.2-1.1-1.1-1: no match for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))), 5 possibilities Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.1-1.2-1.1-1.1: simple apply @quote_ground failed with: Proof-search failed. Debug: 1.1-1.2-1.1-1.2: simple apply @BasicAst.quotation_of_mfixpoint failed with: Cannot unify (quotation_of ?M20949) and (quotation_of Hc) Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2364 : debug_opt Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2364 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for debug_opt without backtracking Debug: 1.1: exact debug_opt_instance_0 on debug_opt, 0 subgoal(s) Debug: 1.1: after exact debug_opt_instance_0 finished, 0 goals are shelved and unsolved ( ) Debug: Goal 1 has a success, continuing resolution Debug: Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run. Stuck: Failed: Initial: Debug: Result goals after fixpoint: 0 goals: Debug: after eauto_tac_stuck: 0 goals: Debug: The tactic trace is: simple refine debug_opt_instance_0;shelve_goals Debug: Finished resolution with a complete solution. Old typeclass evars not concerned by this resolution = Shelf = Debug: New typeclass evars are: (Ast.tVar "Hc"%bs) Debug: 1.1-1.2-1.1-1.2: (*external*) (make_quotation_of_goal ltac:(())) failed with: In nested Ltac calls to "make_quotation_of_goal" and "run_template_program (constr) (tactic)", last call failed. bound argument is not ground Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.1-1.2-1.1: (*external*) simple notypeclasses refine (default_inductive_quotation_of _ _) failed with: Proof-search failed. Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.1-1.2: simple apply @qquotation failed with: Proof-search failed. Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.1: (*external*) (progress repeat autounfold with quotation in *) failed with: Proof-search failed. Debug: 1.2: (*external*) (progress intros) failed with: Failed to progress. Debug: 1.2: (*external*) (destruct t) failed with: pattern-matching failed Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2366 : debug_opt Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2366 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for debug_opt without backtracking Debug: 1.1: exact debug_opt_instance_0 on debug_opt, 0 subgoal(s) Debug: 1.1: after exact debug_opt_instance_0 finished, 0 goals are shelved and unsolved ( ) Debug: Goal 1 has a success, continuing resolution Debug: Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run. Stuck: Failed: Initial: Debug: Result goals after fixpoint: 0 goals: Debug: after eauto_tac_stuck: 0 goals: Debug: The tactic trace is: simple refine debug_opt_instance_0;shelve_goals Debug: Finished resolution with a complete solution. Old typeclass evars not concerned by this resolution = Shelf = Debug: New typeclass evars are: Debug: 1.2: (*external*) (replace_quotation_of_goal ltac:(())) failed with: In nested Ltac calls to "replace_quotation_of_goal" and "run_template_program (constr) (tactic)", last call failed. Avoiding loops Debug: 1.2: simple apply @quote_ground on (quotation_of Hc), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2367 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2367 status: initial Debug: considering goal 1 of status initial Debug: 1.2-1 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: calling eauto recursively at depth 2 on 1 subgoals Debug: 1.2-1: looking for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) without backtracking Debug: 1.2-1.1: simple apply quote_cproperty on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Cannot unify (MCOption.option_default (fun tm : term => checking Γ tm (j_typ (TermTyp b t))) (j_term (TermTyp b t)) unit) and (checking Γ b (j_typ (TermTyp b t))) Debug: 1.2-1.1: (*external*) (is_var t; destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.2-1.1: (*external*) (progress repeat autounfold with quotation in *) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2390 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2390 status: initial Debug: considering goal 1 of status initial Debug: 1.2-1.1-1 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: calling eauto recursively at depth 3 on 1 subgoals Debug: 1.2-1.1-1: looking for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) without backtracking Debug: 1.2-1.1-1.1: simple apply quote_cproperty on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Cannot unify (MCOption.option_default (fun tm : term => checking Γ tm (j_typ (TermTyp b t))) (j_term (TermTyp b t)) unit) and (checking Γ b (j_typ (TermTyp b t))) Debug: 1.2-1.1-1.1: (*external*) (is_var t; destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.2-1.1-1.1: (*external*) (progress repeat autounfold with quotation in *) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Failed to progress. Debug: 1.2-1.1-1.1: (*external*) (progress intros) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Failed to progress. Debug: 1.2-1.1-1.1: (*external*) (destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.2-1.1-1: no match for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))), 5 possibilities Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.2-1.1: (*external*) (progress repeat autounfold with quotation in *) failed with: Proof-search failed. Debug: 1.2-1.2: (*external*) (progress intros) failed with: Failed to progress. Debug: 1.2-1.2: (*external*) (destruct t) failed with: pattern-matching failed Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.2: simple apply @quote_ground failed with: Proof-search failed. Debug: 1.3: simple apply @BasicAst.quotation_of_mfixpoint failed with: Cannot unify (quotation_of ?M20949) and (quotation_of Hc) Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2438 : debug_opt Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2438 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for debug_opt without backtracking Debug: 1.1: exact debug_opt_instance_0 on debug_opt, 0 subgoal(s) Debug: 1.1: after exact debug_opt_instance_0 finished, 0 goals are shelved and unsolved ( ) Debug: Goal 1 has a success, continuing resolution Debug: Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run. Stuck: Failed: Initial: Debug: Result goals after fixpoint: 0 goals: Debug: after eauto_tac_stuck: 0 goals: Debug: The tactic trace is: simple refine debug_opt_instance_0;shelve_goals Debug: Finished resolution with a complete solution. Old typeclass evars not concerned by this resolution = Shelf = Debug: New typeclass evars are: (Ast.tVar "Hc"%bs) Debug: 1.3: (*external*) (make_quotation_of_goal ltac:(())) failed with: In nested Ltac calls to "make_quotation_of_goal" and "run_template_program (constr) (tactic)", last call failed. bound argument is not ground Debug: 1.3: simple apply @qquotation on (quotation_of Hc), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2439 : (inductive_quotation_of Hc) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2439 status: initial Debug: considering goal 1 of status initial Debug: 1.3-1 : (inductive_quotation_of Hc) Debug: calling eauto recursively at depth 2 on 1 subgoals Debug: 1.3-1: looking for (inductive_quotation_of Hc) without backtracking Debug: 1.3-1.1: (*external*) (progress intros) on (inductive_quotation_of Hc) failed with: Failed to progress. Debug: 1.3-1.1: (*external*) simple notypeclasses refine (default_inductive_quotation_of _ _) on (inductive_quotation_of Hc), 2 subgoal(s) Debug: Launching resolution fixpoint on 2 goals: ?X2441 : (quotation_of Hc) ?X2443 : (cls_is_true match ?qt with | Ast.tInd _ _ => true | _ => false end) Debug: Calling fixpoint on : 2 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2441 status: initial Goal 2 evar: ?X2443 status: initial Debug: considering goal 1 of status initial Debug: 1.3-1.1-1 : (quotation_of Hc) Debug: calling eauto recursively at depth 3 on 1 subgoals Debug: 1.3-1.1-1: looking for (quotation_of Hc) with backtracking Debug: 1.3-1.1-1.1: (*external*) (is_var t; destruct t) on (quotation_of Hc) failed with: pattern-matching failed Debug: 1.3-1.1-1.1: (*external*) (progress repeat autounfold with quotation in *) on (quotation_of Hc), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2466 : (quotation_of Hc) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2466 status: initial Debug: considering goal 1 of status initial Debug: 1.3-1.1-1.1-1 : (quotation_of Hc) Debug: calling eauto recursively at depth 4 on 1 subgoals Debug: 1.3-1.1-1.1-1: looking for (quotation_of Hc) with backtracking Debug: 1.3-1.1-1.1-1.1: (*external*) (is_var t; destruct t) on (quotation_of Hc) failed with: pattern-matching failed Debug: 1.3-1.1-1.1-1.1: (*external*) (progress repeat autounfold with quotation in *) on (quotation_of Hc) failed with: Failed to progress. Debug: 1.3-1.1-1.1-1.1: (*external*) (progress intros) on (quotation_of Hc) failed with: Failed to progress. Debug: 1.3-1.1-1.1-1.1: (*external*) (destruct t) on (quotation_of Hc) failed with: pattern-matching failed Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2514 : debug_opt Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2514 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for debug_opt without backtracking Debug: 1.1: exact debug_opt_instance_0 on debug_opt, 0 subgoal(s) Debug: 1.1: after exact debug_opt_instance_0 finished, 0 goals are shelved and unsolved ( ) Debug: Goal 1 has a success, continuing resolution Debug: Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run. Stuck: Failed: Initial: Debug: Result goals after fixpoint: 0 goals: Debug: after eauto_tac_stuck: 0 goals: Debug: The tactic trace is: simple refine debug_opt_instance_0;shelve_goals Debug: Finished resolution with a complete solution. Old typeclass evars not concerned by this resolution = Shelf = Debug: New typeclass evars are: Debug: 1.3-1.1-1.1-1.1: (*external*) (replace_quotation_of_goal ltac:(())) on (quotation_of Hc) failed with: In nested Ltac calls to "replace_quotation_of_goal" and "run_template_program (constr) (tactic)", last call failed. Avoiding loops Debug: 1.3-1.1-1.1-1.1: simple apply @quote_ground on (quotation_of Hc), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2515 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2515 status: initial Debug: considering goal 1 of status initial Debug: 1.3-1.1-1.1-1.1-1 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: calling eauto recursively at depth 5 on 1 subgoals Debug: 1.3-1.1-1.1-1.1-1: looking for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) with backtracking Debug: 1.3-1.1-1.1-1.1-1.1: simple apply quote_cproperty on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Cannot unify (MCOption.option_default (fun tm : term => checking Γ tm (j_typ (TermTyp b t))) (j_term (TermTyp b t)) unit) and (checking Γ b (j_typ (TermTyp b t))) Debug: 1.3-1.1-1.1-1.1-1.1: (*external*) (is_var t; destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.3-1.1-1.1-1.1-1.1: (*external*) (progress repeat autounfold with quotation in *) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Failed to progress. Debug: 1.3-1.1-1.1-1.1-1.1: (*external*) (progress intros) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Failed to progress. Debug: 1.3-1.1-1.1-1.1-1.1: (*external*) (destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.3-1.1-1.1-1.1-1: no match for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))), 5 possibilities Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.3-1.1-1.1-1.1: simple apply @quote_ground failed with: Proof-search failed. Debug: 1.3-1.1-1.1-1.2: simple apply @BasicAst.quotation_of_mfixpoint failed with: Cannot unify (quotation_of ?M20949) and (quotation_of Hc) Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2540 : debug_opt Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2540 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for debug_opt without backtracking Debug: 1.1: exact debug_opt_instance_0 on debug_opt, 0 subgoal(s) Debug: 1.1: after exact debug_opt_instance_0 finished, 0 goals are shelved and unsolved ( ) Debug: Goal 1 has a success, continuing resolution Debug: Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run. Stuck: Failed: Initial: Debug: Result goals after fixpoint: 0 goals: Debug: after eauto_tac_stuck: 0 goals: Debug: The tactic trace is: simple refine debug_opt_instance_0;shelve_goals Debug: Finished resolution with a complete solution. Old typeclass evars not concerned by this resolution = Shelf = Debug: New typeclass evars are: (Ast.tVar "Hc"%bs) Debug: 1.3-1.1-1.1-1.2: (*external*) (make_quotation_of_goal ltac:(())) failed with: In nested Ltac calls to "make_quotation_of_goal" and "run_template_program (constr) (tactic)", last call failed. bound argument is not ground Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.3-1.1-1.1: (*external*) (progress repeat autounfold with quotation in *) failed with: Proof-search failed. Debug: 1.3-1.1-1.2: (*external*) (progress intros) failed with: Failed to progress. Debug: 1.3-1.1-1.2: (*external*) (destruct t) failed with: pattern-matching failed Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2542 : debug_opt Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2542 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for debug_opt without backtracking Debug: 1.1: exact debug_opt_instance_0 on debug_opt, 0 subgoal(s) Debug: 1.1: after exact debug_opt_instance_0 finished, 0 goals are shelved and unsolved ( ) Debug: Goal 1 has a success, continuing resolution Debug: Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run. Stuck: Failed: Initial: Debug: Result goals after fixpoint: 0 goals: Debug: after eauto_tac_stuck: 0 goals: Debug: The tactic trace is: simple refine debug_opt_instance_0;shelve_goals Debug: Finished resolution with a complete solution. Old typeclass evars not concerned by this resolution = Shelf = Debug: New typeclass evars are: Debug: 1.3-1.1-1.2: (*external*) (replace_quotation_of_goal ltac:(())) failed with: In nested Ltac calls to "replace_quotation_of_goal" and "run_template_program (constr) (tactic)", last call failed. Avoiding loops Debug: 1.3-1.1-1.2: simple apply @quote_ground on (quotation_of Hc), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2543 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2543 status: initial Debug: considering goal 1 of status initial Debug: 1.3-1.1-1.2-1 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: calling eauto recursively at depth 4 on 1 subgoals Debug: 1.3-1.1-1.2-1: looking for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) with backtracking Debug: 1.3-1.1-1.2-1.1: simple apply quote_cproperty on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Cannot unify (MCOption.option_default (fun tm : term => checking Γ tm (j_typ (TermTyp b t))) (j_term (TermTyp b t)) unit) and (checking Γ b (j_typ (TermTyp b t))) Debug: 1.3-1.1-1.2-1.1: (*external*) (is_var t; destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.3-1.1-1.2-1.1: (*external*) (progress repeat autounfold with quotation in *) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))), 1 subgoal(s) Debug: Launching resolution fixpoint on 1 goals: ?X2566 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2566 status: initial Debug: considering goal 1 of status initial Debug: 1.3-1.1-1.2-1.1-1 : (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) Debug: calling eauto recursively at depth 5 on 1 subgoals Debug: 1.3-1.1-1.2-1.1-1: looking for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) with backtracking Debug: 1.3-1.1-1.2-1.1-1.1: simple apply quote_cproperty on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Cannot unify (MCOption.option_default (fun tm : term => checking Γ tm (j_typ (TermTyp b t))) (j_term (TermTyp b t)) unit) and (checking Γ b (j_typ (TermTyp b t))) Debug: 1.3-1.1-1.2-1.1-1.1: (*external*) (is_var t; destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.3-1.1-1.2-1.1-1.1: (*external*) (progress repeat autounfold with quotation in *) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Failed to progress. Debug: 1.3-1.1-1.2-1.1-1.1: (*external*) (progress intros) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Failed to progress. Debug: 1.3-1.1-1.2-1.1-1.1: (*external*) (destruct t) on (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: pattern-matching failed Debug: 1.3-1.1-1.2-1.1-1: no match for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))), 5 possibilities Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.3-1.1-1.2-1.1: (*external*) (progress repeat autounfold with quotation in *) failed with: Proof-search failed. Debug: 1.3-1.1-1.2-1.2: (*external*) (progress intros) failed with: Failed to progress. Debug: 1.3-1.1-1.2-1.2: (*external*) (destruct t) failed with: pattern-matching failed Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.3-1.1-1.2: simple apply @quote_ground failed with: Proof-search failed. Debug: 1.3-1.1-1.3: simple apply @BasicAst.quotation_of_mfixpoint failed with: Cannot unify (quotation_of ?M20949) and (quotation_of Hc) Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded Debug: Launching resolution fixpoint on 1 goals: ?X2614 : debug_opt Debug: Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run. Stuck: Failed: Initial: Goal 1 evar: ?X2614 status: initial Debug: considering goal 1 of status initial Debug: 1: looking for debug_opt without backtracking Debug: 1.1: exact debug_opt_instance_0 on debug_opt, 0 subgoal(s) Debug: 1.1: after exact debug_opt_instance_0 finished, 0 goals are shelved and unsolved ( ) Debug: Goal 1 has a success, continuing resolution Debug: Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run. Stuck: Failed: Initial: Debug: Result goals after fixpoint: 0 goals: Debug: after eauto_tac_stuck: 0 goals: Debug: The tactic trace is: simple refine debug_opt_instance_0;shelve_goals Debug: Finished resolution with a complete solution. Old typeclass evars not concerned by this resolution = Shelf = Debug: New typeclass evars are: (Ast.tVar "Hc"%bs) Debug: 1.3-1.1-1.3: (*external*) (make_quotation_of_goal ltac:(())) failed with: In nested Ltac calls to "make_quotation_of_goal" and "run_template_program (constr) (tactic)", last call failed. bound argument is not ground Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.3-1.1: (*external*) simple notypeclasses refine (default_inductive_quotation_of _ _) failed with: Proof-search failed. Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint Debug: 1.3: simple apply @qquotation failed with: Proof-search failed. Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint ```

The important lines are

Debug: 1.1-1.1-1: looking for (ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) without backtracking
Debug: 1.1-1.1-1.1: simple apply quote_cproperty on
(ground_quotable (cproperty Γ all b (j_typ (TermTyp b t)) (fst tu))) failed with: Cannot unify
(MCOption.option_default (fun tm : term => checking Γ tm (j_typ (TermTyp b t))) (j_term (TermTyp b t)) unit) and
(checking Γ b (j_typ (TermTyp b t)))

If we Set Debug "tactic-unification". as well, between the above lines there's a unification trace ending in

Debug:
[tactic-unification] Starting unification: MCOption.option_default (fun tm : term => checking Γ tm (j_typ (TermTyp b t)))
                                             (j_term (TermTyp b t)) unit ~= checking Γ b (j_typ (TermTyp b t))
Debug: [tactic-unification] Leaving unification with failure

So we can add cbn [MCOption.option_default j_term] in * after induction 1, and indeed this allows the proof to go through with induction 1; cbn [MCOption.option_default j_term] in *; exact _. If it turns out that there are many proofs that need this sort of modification, we could try adding MCOption.option_default and j_term to the list of Hint Unfold and Typeclasses Transparent, but I'd rather keep those lists as small as possible for typeclass resolution performance.