Elaboration of parameters in HB.structure and HB.builders

[gares]

We now run type inference but we first turn all id_phant into _. The problem is that if you don't do that the term does not type check, e.g. the factory requires are not postulated (yet). Similarly in structures, before we were ignoring (no type inference for the parameters) parameters and then we were postulating all requires.

IMO this PR makes things a bit more predictable (and similar to the usual way Coq works), but this is a sharp weapon since inference goes left to right, so you should put the most demanding factory (on parameters) first (in a structure declaration).

There is also another subtle problem with indexed that stays there in some terms and type inference can put it in the type of a parameter breaking things (see the commit in the test suite).

Fix #134
Fix #133

[gares]

diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 16c4c58..0cd3e00 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -4569,18 +4569,16 @@ Qed.
 
 End ClosedFieldTheory.
 
-Implicit Type V : zmodType.
-
 HB.mixin
-Record is_subZmodule V (S : {pred V}) (U : indexed Type) of SUB V S U & Zmodule U := {
+Record is_subZmodule (V : zmodType) (S : {pred V}) (U : indexed Type) of SUB V S U & Zmodule U := {
   valB : additive (val : U -> V);
 }.
 
 #[mathcomp]
-HB.structure Definition subZmodule V S := { U of subChoice V S U & Zmodule U & is_subZmodule V S U }.
+HB.structure Definition subZmodule V S := { U of is_subZmodule V S U  & subChoice V S U & Zmodule U }.
 
 Section additive.
-Context V (S : {pred V}) (U : subZmodule.type S).
+Context (V : zmodType) (S : {pred V}) (U : subZmodule.type S).
 Notation val := (val : U -> V).
 Canonical val_additive := Additive (valB : additive val).
 Lemma valD : {morph val : x y / x + y}. Proof. exact: raddfD. Qed.
@@ -4588,15 +4586,12 @@ Lemma val0 : val 0 = 0. Proof. exact: raddf0. Qed.
 Lemma valN : {morph val : x / - x}. Proof. exact: raddfN. Qed.
 End additive.
 
-HB.factory Record pred_subZmodule V (S : {pred V})
+HB.factory Record pred_subZmodule (V : zmodType) (S : {pred V})
     (subS : zmodPred S)
     (kS : keyed_pred subS)
     (U : indexed Type) of subChoice V S U := {}.
 
-HB.builders Context (V : zmodType) (S : {pred V})
-  (subS : zmodPred S)
-  (kS : keyed_pred subS)
-  (U : indexed Type) of pred_subZmodule V S subS kS U.
+HB.builders Context V S subS kS U of pred_subZmodule V S subS kS U.
 
 Let kS_S v : v \in kS -> v \in S. Proof. by rewrite keyed_predE. Qed.
 Let S_kS v : v \in S -> v \in kS. Proof. by rewrite keyed_predE. Qed.
@@ -4625,12 +4620,12 @@ HB.instance Definition _ := is_subZmodule.Build V S U raddf_val.
 HB.end.
 
 HB.mixin
-Record is_subRing (R : ringType) (S : {pred R}) (U : indexed Type) of subZmodule R S U & Ring U := {
+Record is_subRing (R : ringType) S (U : indexed Type) of subZmodule R S U & Ring U := {
   valM : multiplicative (val : U -> R);
 }.
 
 HB.structure
-Definition subRing R S := { U of subZmodule R S U & Ring U & is_subRing R S U}.
+Definition subRing R S := { U of is_subRing R S U & subZmodule R S U & Ring U }.
 
 Section multiplicative.
 Context (R : ringType) (S : {pred R}) (U : subRing.type S).
@@ -4643,9 +4638,7 @@ HB.factory Record pred_subRing (R : ringType) (S : {pred R})
   (ringS : subringPred S) (kS : keyed_pred ringS)
   (U : indexed Type) of subZmodule R S U := {}.
 
-HB.builders Context (R : ringType) (S : {pred R})
-(ringS : subringPred S) (kS : keyed_pred ringS)
-(U : indexed Type) of pred_subRing R S ringS kS U.
+HB.builders Context R S ringS kS U of pred_subRing R S ringS kS U.
 
 Let kS_S v : v \in kS -> v \in S. Proof. by rewrite keyed_predE. Qed.
 Let S_kS v : v \in S -> v \in kS. Proof. by rewrite keyed_predE. Qed.
@@ -4680,10 +4673,9 @@ HB.mixin Record is_subLmodule  (R : ringType) (V : lmodType R) (S : {pred V})
  valZ : scalable (val : W -> V);
 }.
 
-(* BUG: coercions *)
 HB.structure
-Definition subLmodule (R : ringType) (V : lmodType (Ring.sort R)) (S : {pred (Lmodule.sort V)}) :=
-  { W of subZmodule V S W & is_Lmodule_of_Zmodule R W & is_subLmodule R V S W}.
+Definition subLmodule R V S :=
+  { W of is_subLmodule R V S W & subZmodule V S W & is_Lmodule_of_Zmodule R W}.
 

[CohenCyril]

Amazing!

[CohenCyril]

Really nice!