Unify declare saturate

HB/instance.elpi

@@ -66,14 +66,18 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
 
   private.check-non-forgetful-inheritance TheType Factory,
 
-  private.declare-instance Factory TheType TheFactory Clauses CSL,
+  private.declare-instance Factory TheType TheFactory Clauses CSL1,
 
   % handle parameters via a section -- end
   if (TyWP = arity _) true (
     if-verbose (coq.say {header} "closing instance section"),
     log.coq.env.end-section-name SectionName
   ),
-
+coq.say "HERE",
+  (Clauses => saturate-instances2 {term->cs-pattern TheType} CSL2),
+
+  std.append CSL1 CSL2 CSL,
+
   % we accumulate clauses now that the section is over
   acc-clauses current Clauses
 ].
@@ -117,9 +121,10 @@ declare-all-on-type-constructor TK [class Class Struct MLwP|Rest] [pr Name CS|L]
 
   %TODO: compute the arity of the Class subject and saturate up to that point
   %      there may even be more than one possibility
-  saturate-type-constructor TK T,
+  std.spy(coq.env.typeof Class ClassTy),
+  std.spy (saturate-type-constructor TK T),
 
-  infer-class T Class Struct MLwP S Name _STy Clauses,
+  std.spy (infer-class T Class Struct MLwP S Name _STy Clauses),
 
   !,
 
@@ -164,13 +169,19 @@ infer-class T  Class Struct MLwP S Name STy Clauses:- std.do![
   private.optimize-class-body THD {std.length Params} KCApp KCAppNames Clauses,
   coq.mk-app (global KS) {std.append Params [T, KCAppNames]} S,
   if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}),
-  std.assert-ok! (coq.typecheck S STy) "infer-class: S illtyped",
+
+  coq.typecheck S STy ok, % failure may be due to a parameter not rich enough see #435
+
 ].
 
 pred decl-const-in-struct i:string, i:term, i:term, i:constant.
 decl-const-in-struct Name S STy CS:- std.do![
 
-  log.coq.env.add-const-noimplicits Name S STy @transparent! CS, % Bug coq/coq#11155, could be a Let
+  if (ground_term S) (S1 = S, STy1 = STy)
+    (abstract-holes.main S S1,
+     std.assert-ok! (coq.typecheck S1 STy1) "HB: structure instance illtyped after generalizing over holes"),
+
+  log.coq.env.add-const-noimplicits Name S1 STy1 @transparent! CS, % Bug coq/coq#11155, could be a Let
   with-locality (log.coq.CS.declare-instance CS), % Bug coq/coq#11155, should be local
   acc-clause current (local-canonical CS),
   if-verbose (coq.say {header} "structure instance" Name "declared"),
@@ -261,6 +272,26 @@ saturate-instances Filter :- std.do! [
     declare-all-on-type-constructor t Classes _),
 ].
 
+pred saturate-instances2 i:cs-pattern o:list (pair id constant).
+saturate-instances2 Filter CSL :- std.spy-do! [
+
+  findall-has-mixin-instance Filter ClausesHas,
+
+  std.map ClausesHas has-mixin-instance_key KL,
+  undup-cs-patterns KL UKL,
+  std.map UKL cs-pattern->term TL,
+
+  findall-classes AllClasses,
+
+  std.map ClausesHas has-mixin-instance->mixin-src Clauses,
+
+  Clauses => std.map2 TL UKL (t\k\r\sigma Classes\
+    std.filter AllClasses (no-instance-for k) Classes,
+    std.spy(declare-all-on-type-constructor t Classes r)) CSLL,
+
+  std.flatten CSLL CSL,
+].
+
 pred no-instance-for i:cs-pattern, i:class.
 no-instance-for K (class _ S _) :-
   get-structure-sort-projection S (global Proj),
@@ -382,10 +413,10 @@ declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- std.do! [
       list-w-params_list {factory-provides Factory} ML,
       add-all-mixins T Factory ML tt Clauses MCSL,
       std.map-filter Clauses (mixin-src->has-mixin-instance ) ClausesHas,
-      ClausesHas => declare-all T {findall-classes-for ML} CCSL, % declare-all-on-type-constructor doesn't work here
+      % ClausesHas => declare-all T {findall-classes-for ML} CCSL, % declare-all-on-type-constructor doesn't work here
     ]
   ],
-  std.append MCSL CCSL CSL
+  std.append MCSL [] CSL
 ].
 
 % If you don't mention the factory in a builder, then Coq won't make

_CoqProject.test-suite

@@ -96,6 +96,8 @@ tests/unit/struct.v
 tests/factory_when_notation.v
 
 tests/saturate_on.v
+tests/bug_435.v
+tests/bug_447.v
 
 -R tests HB.tests
 -R examples HB.examples

tests/bug_435.v

@@ -0,0 +1,27 @@
+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}.
+#[verbose] HB.instance Definition _ (X : Type) := A2.Build X unit true.
+(*HB.saturate unit.*)
+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.

tests/bug_447.v

@@ -0,0 +1,22 @@
+From HB Require Import structures.
+
+Variant testTy := A | B.
+HB.mixin Record Stack1 T := { prop1 : unit }.
+HB.structure Definition JustStack1 := { T of Stack1 T }.
+HB.mixin Record Stack1Param R T := { prop2 : unit }.
+HB.structure Definition JustStack1Param R := { T of Stack1Param R T }.
+
+HB.mixin Record Stack2 T := { prop3 : unit }.
+HB.structure Definition JustStack2 := { T of Stack2 T }.
+HB.mixin Record Mixed T of Stack1 T & Stack2 T := { prop4 : unit }.
+HB.structure Definition JustMixed := { T of Mixed T & Stack1 T & Stack2 T}.
+HB.structure Definition JustMixedParam R := 
+  { T of Mixed T & Stack1 T & Stack1Param R T & Stack2 T}.
+
+HB.instance Definition _ := @Stack1.Build testTy tt.
+HB.instance Definition _ := @Stack2.Build testTy tt.
+
+HB.instance Definition _ {R} := @Stack1Param.Build R testTy tt.
+HB.instance Definition _ := @Mixed.Build testTy tt.
+
+Check testTy : JustMixedParam.type _.