filter CS db in a more precise way (fix#120)

_CoqProject

@@ -50,6 +50,6 @@ Coq2020_material/CoqWS_expansion/withoutHB.v
 tests/type_of_exported_ops.v
 tests/duplicate_structure.v
 tests/instance_params_no_type.v
+tests/test_CS_db_filtering.v
 
 -R . HB
-

hb.elpi

@@ -594,15 +594,17 @@ get-canonical-mixins-of T S MSL :- std.do! [
   structure-nparams S NParams,
   coq.mk-n-holes NParams Holes,
   coq.mk-app Sort {std.append Holes [ST]} SortHolesST,
-  std.assert-ok! (coq.unify-eq T SortHolesST) "HB: get-canonical-mixins-of: T = sort ST",
-  % Hum, this unification problem is not super trivial. TODO replace by something simpler
-  get-constructor S KS,
-  coq.mk-app (global KS) {std.append Holes [T, C]} KSHolesC,
-  std.assert-ok! (coq.unify-eq ST KSHolesC) "HB: get-canonical-mixins-of: ST = _ _ C",
-  C = app Stuff,
-  std.drop {calc (NParams + 2)} Stuff MIL,
-  std.map MIL (mixin-srcs T) MSLL,
-  std.flatten MSLL MSL
+  if (coq.unify-eq T SortHolesST ok) (
+    % Hum, this unification problem is not super trivial. TODO replace by something simpler
+    get-constructor S KS,
+    coq.mk-app (global KS) {std.append Holes [T, C]} KSHolesC,
+    std.assert-ok! (coq.unify-eq ST KSHolesC) "HB: get-canonical-mixins-of: ST = _ _ C",
+    C = app Stuff,
+    std.drop {calc (NParams + 2)} Stuff MIL,
+    std.map MIL (mixin-srcs T) MSLL,
+    std.flatten MSLL MSL
+  )
+    (MSL = [])
 ].
 
 pred under-canonical-mixins-of.do! i:term, i:list prop.

tests/test_CS_db_filtering.v

@@ -0,0 +1,33 @@
+From HB Require Import structures.
+
+HB.mixin Record base_m T := { A : T }.
+HB.structure Definition base := { T of base_m T }.
+
+HB.mixin Record child1_m T := { C1 : T }.
+HB.structure Definition child1 := { T of base T & child1_m T }.
+
+HB.mixin Record child2_m T := { C2 : T }.
+HB.structure Definition child2 := { T of base T & child2_m T }.
+
+Axiom ix : Type.
+Definition vec T := ix -> T.
+
+Section b.
+Variable T : base.type.
+HB.instance Definition v_base_m : base_m (vec T) :=
+  base_m.Build _ (fun _ => A).
+End b.
+
+Section c1.
+Variable T : child1.type.
+HB.instance Definition v_child1_m : child1_m (vec T) :=
+    child1_m.Build _ (fun _ => C1).
+End c1.
+
+Section c2.
+Variable T : child2.type.
+
+  HB.instance Definition v_child2_m : child2_m (vec T) :=
+  child2_m.Build _ (fun _ => C2).
+
+End c2.