Very slow creation of a subtype instance.

[hivert]

In the following code, HB takes nearly 30s to find the unit ring instance. Some variation are faster. I got something even much slower (more that 2 min) on more complicated code. I can't figure out a clear pattern. So I put here a reasonably simple code where the time seems to be excessive.

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

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

Section DefType.
Variables (n : nat) (R : ringType).
Record sympoly : predArgType :=
  SymPoly {sympol :> {mpoly R[n]}; _ : sympol \is symmetric}.

HB.instance Definition _ := [isSub of sympoly for sympol].
HB.instance Definition _ := [Choice of sympoly by <:].
HB.instance Definition _ := [SubChoice_isSubLalgebra of sympoly by <:].
End DefType.

Section SymPolyComRingType.
Variables (n : nat) (R : comRingType).
HB.instance Definition _ := [SubRing_isSubComRing of (sympoly n R) by <:].
HB.instance Definition _ := [SubChoice_isSubAlgebra of (sympoly n R) by <:].
End SymPolyComRingType.

Section SymPolyIdomainType.
Variables (n : nat) (R : idomainType).
HB.instance Definition _ := [SubRing_isSubUnitRing of (sympoly n R) by <:].   (* stuck here for more than 25s *)
HB.instance Definition _ :=
  [SubComUnitRing_isSubIntegralDomain of (sympoly n R) by <:].
End SymPolyIdomainType.

Is was with

coq-hierarchy-builder     1.6.0
coq-mathcomp-ssreflect    2.1.0
coq-mathcomp-algebra      2.1.0
coq-mathcomp-multinomials 2.1.0

installed with OPAM on

The Coq Proof Assistant, version 8.18.0
compiled with OCaml 4.14.1