Merge pull request #484 from math-comp/fix-435

HB.instance: failure building a class is not fatal

Author: CohenCyril

HB/instance.elpi

@@ -169,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"),

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