`[porderMixin of ... by <:]` fails for some aliases such as `seqprod` and `seqlexi`

[pi8027]

Example:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Record tupleprod_of n (T : Type) :=
  Tupleprod { tpval : seqprod T; _ : size tpval == n }.

Canonical tupleprod_subType n (T : Type) :=
  [subType for @tpval n T].

Definition tupleprod_eqMixin n (T : eqType) :=
  [eqMixin of tupleprod_of n T by <:].

Canonical tupleprod_eqType n (T : eqType) :=
  EqType (tupleprod_of n T) (tupleprod_eqMixin n T).

Definition tupleprod_choiceMixin n (T : choiceType) :=
  [choiceMixin of tupleprod_of n T by <:].

Canonical tupleprod_choiceType n (T : choiceType) :=
  ChoiceType (tupleprod_of n T) (tupleprod_choiceMixin n T).

Definition tupleprod_countMixin n (T : countType) :=
  [countMixin of tupleprod_of n T by <:].

Canonical tupleprod_countType n (T : countType) :=
  CountType (tupleprod_of n T) (tupleprod_countMixin n T).

Canonical tupleprod_subCountType n (T : countType) :=
  [subCountType of tupleprod_of n T].

Fail Definition tupleprod_porderMixin d n (T : porderType d) :=
  [porderMixin of tupleprod_of n T by <:].
(*
The command has indeed failed with message:
In environment
d : unit
n : nat_eqType
T : porderType d
The term "Order.SubOrder.sub_POrderMixin ?sT" has type "lePOrderMixin (sub_choiceType ?sT)"
while it is expected to have type "lePOrderMixin [eqType of tupleprod_of n T]".
*)

It works if DefaultSeqProdOrder is imported.

[proux01]

@pi8027 this seems to work in the hierarchy-builder branch so maybe not worth trying to fix that in master

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

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Record tupleprod_of n (T : Type) :=
  Tupleprod { tpval : seqprod T; _ : size tpval == n }.

HB.instance Definition _ n T :=
  [isSub for @tpval n T].

(* work also if uncommented                                                                                                                                    
HB.instance Definition _ n (T : eqType) :=                                                                                                                     
  [Equality of tupleprod_of n T by <:].                                                                                                                        
*)

HB.instance Definition _ n (T : choiceType) :=
  [Choice of tupleprod_of n T by <:].

(* work also if uncommented                                                                                                                                    
HB.instance Definition _ n (T : countType) :=                                                                                                                  
  [Countable of tupleprod_of n T by <:].                                                                                                                       
*)

HB.instance Definition _ d n (T : porderType d) :=
  [SubChoice_isSubPOrder of tupleprod_of n T by <: with d].

Print Canonical Projections tupleprod_of.
(*                                                                                                                                                             
tupleprod_of <- SubChoice.sort ( test_tupleprod_of__canonical__choice_SubChoice )                                                                              
tupleprod_of <- Order.SubPOrder.sort ( test_tupleprod_of__canonical__Order_SubPOrder )                                                                         
tupleprod_of <- Sub.sort ( test_tupleprod_of__canonical__eqtype_Sub )                                                                                          
tupleprod_of <- Choice.sort ( test_tupleprod_of__canonical__choice_Choice )                                                                                    
tupleprod_of <- Order.POrder.sort ( test_tupleprod_of__canonical__Order_POrder )                                                                               
tupleprod_of <- Equality.sort ( test_tupleprod_of__canonical__eqtype_Equality )                                                                                
tupleprod_of <- SubEquality.sort ( test_tupleprod_of__canonical__eqtype_SubEquality )                                                                          
*)