More unified judgment type and All_local_env

[yannl35133]

No description provided.

[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.