Here is a small instance of my problem:
Record ord : Type := mk_ord
{ tord: Type;
ole: tord -> tord -> Prop;
}.
Definition onat := mk_ord nat le.
Definition singl (O : ord) (e : tord O) : list (tord O) :=
cons e nil.
Lemma singl_len :
forall (O : ord) (e : tord O), length (singl O e) = 1.
Proof.
trivial.
Qed.
Example unif : length (singl onat 2) = 1.
Proof.
Set Printing All.
simpl (tord _). (* [tord nat] changes to [nat] *)
Fail rewrite singl_len.
Abort.
I guess that the rewriting fails while trying to unify tord ?O (in the lemma) with nat (in the goal).
But ?O will be set to onat anyway because of the singl onat 2 matched in the goal, so why does it fail to convert tord onat to nat here?
There is more than one solution for ?O, not only onat, that would make this rewrite valid, so there's a legitimate reason for it to fail.
(* ... *)
Definition onat2 := mk_ord nat gt. (* gt instead of le *)
Example unif : length (singl onat 2) = 1.
Proof. apply (singl_len onat2). Qed. (* onat and onat2 both work here *)
In general the unifier in rewrite is very syntactic, so it's best to not rely on it unfolding definitions to make proofs more predictable.
However in this case the problem is to solve the equation tord ?O = nat, which does not have a unique solution, as shown above, but we can declare a canonical solution for it, because morally we do want to associate the nat type with the onat record. This is done by using the Canonical keyword when defining the onat record.
Canonical onat := mk_ord nat le. (* solves tord ?O = nat with ?O := onat *)
(* ... *)
Example unif : length (singl onat 2) = 1.
Proof.
Set Printing All.
simpl (tord _). (* [tord nat] changes to [nat] *)
rewrite singl_len.
reflexivity.
Qed.