Coq infrastructure

Turning type class failure into subgoals

Coq's type class inference shelves dependent subgoals and doesn't fail if they remain unsolved by unification. An instance argument of the form Phantom A x thus results in a new (shelved) subgoal A. Since the ssreflect apply tactic does not shelve these subgoals, we can use this to run partial typeclass inference.

Example: Typeclasses eauto := debug. Class pointed (A : Type) := point : A. Instance shelve_pointed {A : Type} (x : A) `{phantom A x} : pointed A | 1000 := x. Goal forall P : Prop, P -> P. move=> P h. apply: point. change P with (pointed P) in h. apply: point. Qed.

Manually invoking unification / canonical structure inference

This is verbatim from "Canonical structures for the working Coq user" by Assia Mahboubi and Enrico Tassi. In ssreflect, unify is called phant_id, but it doesn't have the extra error message.