HB.instance: failure building a class is not fatal

It may be due to a parameter being not rich enough for a mixin
we were able to found during synthesis.

Author: gares

HB/instance.elpi

@@ -169,7 +169,9 @@ 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.

_CoqProject.test-suite

@@ -96,6 +96,7 @@ tests/unit/struct.v
 tests/factory_when_notation.v
 
 tests/saturate_on.v
+tests/bug_435.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.