isFinite.Build with an explicit list creates a warning about a canonical projection to cons

[RemiDiG]

Example:

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

Inductive T : Type := x.

Definition eqT (a b : T) : bool := true.
Lemma eqTP (a b : T) : reflect (a = b) (eqT a b).
Proof. case a. case b. by apply ReflectT. Qed.
HB.instance Definition _ := hasDecEq.Build T eqTP.

Definition T_to_unit (a : T) : unit := tt.
Definition unit_to_T (a : unit) : T := x.
Lemma TunitK : cancel T_to_unit unit_to_T.
Proof. by case. Qed.
HB.instance Definition _ : isCountable T := CanIsCountable TunitK.

Lemma enumPT : Finite.axiom [:: x].
Proof. by case. Qed.
HB.instance Definition _ := isFinite.Build T enumPT.
(*
HB_unnamed_factory_9 is defined
Ignoring canonical projection to cons by isFinite.enum_subdef in
HB_unnamed_factory_9: redundant with HB_unnamed_factory_20
[redundant-canonical-projection,typechecker]
Top_T__canonical__fintype_Finite is defined
*)