TC not resilient to small changes deep in a term

[Tragicus]

If we feed a term to the typeclass solver, which is not exactly of the expected form, then the latter fails. A funny example of this is when a variable appears several times in the term. Real-life examples include issues with primitive projections and their compatibility constants. I expect we would also have issues with convertible chains of coercions.

From elpi Require Import elpi tc.

Class C (T : Type) : Type := {}.
Axiom t : forall n m : nat, Type.

Instance tC (n : nat) : C (t n n) := Build_C (t n n).
Set Printing All.
Check _ : C (t 0 0).
(* tC O *)
Check _ : C (t 0 (id 0)).
(* ?c *)