We use this method to report typeclass (and coercion) resolution problems that are "stuck". That is, there is nothing else to do, and we don't have enough information to synthesize them using TC resolution.
Try to process pending synthetic metavariables. If
mayPostpone == false,
 after executing this method.
It keeps executing
synthesizeSyntheticMVarsStep while progress is being made.
mayPostpone == false, then it applies default instances to
SyntheticMVarKind.typeClass (if available)
metavariables that are still unresolved, and then tries to resolve metavariables
mayPostpone == false. That is, we force them to produce error messages and/or commit to
a "best option". If, after that, we still haven't made progress, we report "stuck" errors.
Remark: we set
ignoreStuckTC := true when elaborating
simp arguments. Then,
pending TC problems become implicit parameters for the simp theorem.
k, and synthesize pending synthetic metavariables created while executing
k are solved.
mayPostpone == false, then all of them must be synthesized.
Remark: even if
mayPostpone == true, the method still uses
Collect unassigned metavariables at
e that have associated tactic blocks, and then execute them using
We use this method at the
match .. with elaborator when it cannot be postponed anymore, but it is still waiting
the result of a tactic block.