HB.instance: abstract over unresolved holes (fix #447)

Author: gares

HB/instance.elpi

@@ -177,7 +177,11 @@ infer-class T  Class Struct MLwP S Name STy Clauses:- std.do![
 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

@@ -97,6 +97,7 @@ 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_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 _.