Spurious warning Projection value has no head constant

[hivert]

Here is an example:

Variable R : ringType.
Variable n : nat.

Implicit Types (p q r s : {poly R}).

Record truncfps := MkTfps { tfps : {poly R}; _ : size tfps <= n.+1 }.

HB.instance Definition _ : isSub _ _ truncfps := [isSub for tfps].

leads to

HB_unnamed_factory_1 is defined
Warning: Projection value has no head constant:
fun (K : truncfps -> Type)
  (K_S : forall (x : {poly R}) (Px : (fun x0 : {poly R} => size x0 <= n.+1) x),
         K (MkTfps Px)) (u : truncfps) =>
match u as u0 return (K u0) with
| @MkTfps x Px => K_S x Px
end in canonical instance HB_unnamed_factory_1 of isSub.Sub_rect, ignoring it.
[projection-no-head-constant,records,default]
tfps_truncfps__canonical__eqtype_SubType is defined

@cyrilcohen on zulip said: the canonical projections on non "keys" should be ignored. We should add a declaration of the form "canonical=false" when we declare mixin instances in hb.

[pi8027]

We usually write -arg -w -arg -projection-no-head-constant in _CoqProject to suppress this warning.