FTR: A scenario where HB.instance is too eager to infer

[affeldt-aist]

The following PR to MathComp-Analysis (math-comp/analysis#1256, this is actually wip)
seems to illustrate a potential improvement to HB. Concretely, we tried to generalize the structure of measurable
functions (from a realType codomain to any measurableType) and then equipping the constant function with both
the type of measurable functions and the type of simple functions (i.e., with codomain realType) caused HB to
complain that constant functions aren't all simple functions; we avoided the problem so far by restricting ourselves
to real-valued functions. We found a kludge that we are in the process of experimenting.

@t6s @hoheinzollern

[CohenCyril]

In order to witness the issue, one needs to remove the enclosing Module HBSimple..

[ybertot]

Here is the piece of code that is frowned upon (from theories/lebesgue_integral.v)

[CohenCyril]

I believe this is the same bug as #447, we should use "saturate" code i.e. reabstract parameters and compute the actual prerequisite by unification.

[CohenCyril]

Minimized:

From HB Require Import structures.

HB.mixin Record M T := { m : bool }.
HB.structure Definition S := {T of M T}.

HB.mixin Record A1 X T := { a1 : bool }.
HB.structure Definition B1 X := {T of A1 X T}.

HB.instance Definition _ (X : Type) := A1.Build X unit true.

HB.mixin Record A2 (X : Type) T := { a2 : bool }.
HB.structure Definition B2 (X : Type) := {T of A2 X T}.

(* This should work but fails. *)
Module should_work_but_fails.
HB.structure Definition B (X : S.type) := {T of A1 X T & A2 X T}.
Fail HB.instance Definition _ (X : Type) := A2.Build X unit true.
Fail Check unit : B.type _.
End should_work_but_fails.

Module workaround.
HB.instance Definition _ (X : Type) := A2.Build X unit true.
HB.structure Definition B (X : S.type) := {T of A1 X T & A2 X T}.
HB.saturate unit.
Check unit : B.type _.
End workaround.