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.
Here is an example:
leads to
@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.