Consider the following definition of a record R, parametrized over an arbitrary eqType:
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype.
From Coq Require Import DecidableType DecidableTypeEx FMapWeakList.
Record R {s : eqType} := mkR {
a : nat;
b : s
}.
Now, I want to use R as a UsualDecidableType to index weak maps. Following examples here, a create a module R_as_DT:
Module R_as_DT <: UsualDecidableType.
Parameter s : eqType.
Definition t := @R s.
Definition eq := @Logic.eq t.
Definition eq_refl := @Logic.eq_refl t.
Definition eq_sym := @Logic.eq_sym t.
Definition eq_trans := @Logic.eq_trans t.
Definition eq_dec : forall (x y : t), {eq x y} + {~ eq x y}.
intros x y.
destruct (x.(a) == y.(a)) eqn:Ha.
2 : {
right; unfold eq; destruct x,y; cbv; intro H; inversion H.
simpl in Ha; rewrite H1 in Ha; contradict Ha.
apply Bool.not_false_iff_true; apply /eqP; reflexivity.
}
destruct (x.(b) == y.(b)) eqn:Hb.
2 : {
right; unfold eq; destruct x,y; cbv; intro H; inversion H.
simpl in Hb; rewrite H2 in Hb; contradict Hb.
apply Bool.not_false_iff_true; apply /eqP; reflexivity.
}
destruct x,y; left; simpl in Ha,Hb;
move: Ha => /eqP Ha; move: Hb => /eqP Hb; subst.
reflexivity.
Defined.
End R_as_DT.
Then, I import the FMapWeakList module passing R_as_DT as parameter.
Module Import RMap := FMapWeakList.Make(R_as_DT).
Problem is that now, Coq does not understand that R is the same as key.
Definition R1 : R := mkR nat_eqType 0 0.
Fail Definition test := RMap.add R1 2.
Do I need to somehow specify explicitely that parameter s of module R_as_DT is instantiated with nat_eqType ? The problem does not happen if R does not contain a type parameter.
