under-canonical-mixins should filter the CS db better

[gares]

See: https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Builder.20devs.20.26.20users/topic/instance.20family.20bug.3F

Test case:

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.

  (* CS lookup for `vec` says yes... but the instance is for a paramter T of different type, kaboom *)
  HB.instance Definition v_child2_m : child2_m (vec T) :=
  child2_m.Build _ (fun _ => C2).

End c2.

[gares]

Proposed fix:

diff --git a/hb.elpi b/hb.elpi
index 9bb314b..3daff91 100644
--- a/hb.elpi
+++ b/hb.elpi
@@ -595,15 +595,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.

[gares]

The old code just filers looking at the head constant, but this is not sufficient to rule out spurious instances.
Here we tolerate that the sort ? = T unif problem fails, which is the more expensive but correct test IMO.