Description
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.