HB.instance not produced anymore

[affeldt-aist]

The following branch

https://github.com/affeldt-aist/analysis/tree/evt2_HB_bug_report_20240906b

records a potential issue with HB.

In normedtype.v, we have changed the definition of the
structure NormedModule so that instead of using GRing.Lmodule
it uses Tvs, which is a structure that includes GRing.Lmodule.

We were expecting that compilation would not fail but a bit later
in the file the command

#[export, non_forgetful_inheritance]
HB.instance Definition _ := NormedModule.copy R R^o.

normedtype.v:849 fails with the following message

Error:
Definition illtyped: In environment
R : realType
The term "Phant R^o" has type "phant (GRing.regular (Real.sort R))"
while it is expected to have type "phant (@NormedModule.sort ?t0 ?t1)".

--

The problem can be circumvented by uncommenting l.811--l.827.
The problem seems to be that the command

HB.instance Definition _ :=
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R R^o (@normrM _).

was not producing an instance anymore and that might reveal
an HB insufficiency to identify instances of mixins.

@mkerjean @CohenCyril