# Problem working with FMapWeakList and Parametrized Records

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.