Declaring dual `bPOrderType` and `tPOrderType` instances fails

[pi8027]

Here is a complete example:

From HB Require Import structures.

HB.mixin Record IsPOrdered T := { le : T -> T -> bool }.

HB.structure Definition POrder := { T of IsPOrdered T }.

HB.mixin Record HasBottom T of IsPOrdered T := { bottom : T }.

HB.structure Definition BPOrder := { T of HasBottom T & IsPOrdered T }.

HB.mixin Record HasTop T of IsPOrdered T := { top : T }.

HB.structure Definition TPOrder := { T of HasTop T & IsPOrdered T }.

Definition dual (T : Type) := T.

HB.instance Definition _ (T : POrder.type) :=
  IsPOrdered.Build (dual T) (fun x y => @le T y x).
HB.instance Definition _ (T : BPOrder.type) :=
  HasTop.Build (dual T) (@bottom T).
Fail HB.instance Definition _ (T : TPOrder.type) :=
  HasBottom.Build (dual T) (@top T).
(*
T is declared
HB_unnamed_factory_95 is defined

The command has indeed failed with message:
HB: structure-instance->mixin-srcs: ST = _ _ C: In environment
T : TPOrder.type
Unable to unify "T" with "{| TPOrder.sort := dual T; TPOrder.class := ?e0 |}".
*)

If I swap the last two declarations, the first one declaring a canonical tPOrderType instance fails dually. Any idea why it fails?

[pi8027]

It seems that I'm using HB from a random commit in #252 for some reason (which I don't remember)... I will try the latest one and master to see if it fixes the issue.

[pi8027]

I confirm it works with #252 and so let's close.

[pi8027]

Based on #252 and the hierarchy-builder+factory_sort_tac branch of MathComp, I still couldn't declare the canonical dual tPOrderType instance in the context where the canonical dual bPOrderType is declared. https://github.com/Coq-Polyhedra/mathcomp/blob/hb-semilattices/mathcomp/ssreflect/order.v#L2124

The second HB.instance declaration in the comment reports the following error:

Error:
declare-all: S illtyped: Illegal application: 
The term "TPOrder.Class" of type
 "forall (d : unit) (T : Type) (choice_HasChoice_mixin : HasChoice.axioms_ T)
    (eqtype_HasDecEq_mixin : Equality.mixin_of T)
    (Order_IsDualPOrdered_mixin : IsDualPOrdered.axioms_ d T
                                    eqtype_HasDecEq_mixin),
  HasTop.axioms_ d T choice_HasChoice_mixin eqtype_HasDecEq_mixin
    Order_IsDualPOrdered_mixin -> TPOrder.axioms_ d T"
cannot be applied to the terms
 "disp" : "unit"
 "T^d" : "Type"
 "HB_unnamed_mixin_846" : "HasChoice.axioms_ T^d"
 "HB_unnamed_mixin_847" : "Equality.mixin_of T^d"
 "HB_unnamed_mixin_848" : "IsDualPOrdered.axioms_ disp T^d (BPOrder.class T)"
 "HB_unnamed_factory_844"
   : "HasTop.axioms_ (dual_display disp) T^d (HB_unnamed_mixin_825 T)
        (HB_unnamed_mixin_826 T) (HB_unnamed_factory_823 T)"
The 6th term has type
 "HasTop.axioms_ (dual_display disp) T^d (HB_unnamed_mixin_825 T)
    (HB_unnamed_mixin_826 T) (HB_unnamed_factory_823 T)"
which should be coercible to
 "HasTop.axioms_ disp T^d HB_unnamed_mixin_846 HB_unnamed_mixin_847
    HB_unnamed_mixin_848".

[gares]

@pi8027 https://github.com/math-comp/hierarchy-builder/pull/242 should unblock you (even if your new order.v file has some perf issues)

[pi8027]

@gares Thanks! Unfortunately, it is still broken. https://github.com/Coq-Polyhedra/mathcomp/blob/618738046b250bce2c71101c3776e71cd3e0faed/mathcomp/ssreflect/order.v#L2144-L2148

Error:
declare-all: S illtyped: Illegal application: 
The term "FinTPOrder.Class" of type
 "forall (d : unit) (T : Type),
  IsCountable.axioms_ T ->
  forall (choice_HasChoice_mixin : HasChoice.axioms_ T)
    (eqtype_HasDecEq_mixin : Equality.mixin_of T),
  IsFinite.axioms_ T eqtype_HasDecEq_mixin ->
  forall
    Order_IsDualPOrdered_mixin : IsDualPOrdered.axioms_ d T
                                   eqtype_HasDecEq_mixin,
  HasTop.axioms_ d T choice_HasChoice_mixin eqtype_HasDecEq_mixin
    Order_IsDualPOrdered_mixin -> FinTPOrder.axioms_ d T"
cannot be applied to the terms
 "dual_display disp" : "unit"
 "T^d" : "Type"
 "HB_unnamed_mixin_1121 T" : "IsCountable.axioms_ T^d"
 "HB_unnamed_mixin_1115 T" : "HasChoice.axioms_ T^d"
 "HB_unnamed_mixin_1110 T" : "Equality.mixin_of T^d"
 "HB_unnamed_mixin_1128 T" : "IsFinite.axioms_ T^d (HB_unnamed_factory_1123 T)"
 "HB_unnamed_factory_1129 T"
   : "IsDualPOrdered.axioms_ (dual_display disp) T^d (HB_unnamed_mixin_1110 T)"
 "HB_unnamed_mixin_1154"
   : "HasTop.axioms_ disp T (FinTPOrder.class T) (FinTPOrder.class T)
        (FinTPOrder.class T)"
The 8th term has type
 "HasTop.axioms_ disp T (FinTPOrder.class T) (FinTPOrder.class T)
    (FinTPOrder.class T)"
which should be coercible to
 "HasTop.axioms_ (dual_display disp) T^d (HB_unnamed_mixin_1115 T)
    (HB_unnamed_mixin_1110 T) (HB_unnamed_factory_1129 T)".

[pi8027]

It seems that you closed this issue by mistake. So I reopen it.

[gares]

I must have messed up, sorry

[gares]

BTW, I did push a minimized version of your bug, which is likely not good enough. Do you think you can fix (actually break) it? https://github.com/math-comp/hierarchy-builder/blob/master/tests/test_synthesis_params.v

[pi8027]

@gares I think we need one more extension of porderType such as finPOrderType to reproduce the current bug. Let me try.

[gares]

OK, thanks for trying. The problem is that, for some bug/reason,on the same type T^d there are two competing mixins, one with parameter d and one (dual_display d).

I think the root of the problem is the procedure which looks CS up, and which I tried to rewrite a few times already. It does so by calling the unifier on (sort ?S = T^d) and then (Pack ?T ?C = ?S) and finally (Axioms ?M1 .. ?MN = ?C). The problem is that the first problem also succeeds by unfolding ^d, and we pick the list of structures (hence the sort here) by looking all all the structures one has on ^d, and up in the file you have a preorder on dual already, but one where the parameter is not (dual_display d). So I think it find the wrong instance on T (instead of T^d as asked), and we try that before/after the good one, which is shadowed.

I think I can make this procedure less stupid, but I'd really like a smaller example.

[gares]

Your observation that changing the order of the declarations makes it work is correct, I think because of this "shadowing and competing mixins" is very sensible on the order of structures for which there is an instance in the Coq DB :-(

[pi8027]

See #263.

[pi8027]

Apparently, I still have this issue: https://github.com/pi8027/math-comp/blob/60beb559993a4147d5c71c1210015401997e87e1/mathcomp/ssreflect/order.v#L2004-L2061

I will minimize it when I have time.

[pi8027]

#263 is still valid as a minimization.

[pi8027]

Currently, we use HB.saturate as a workaround for this issue. It works, but it's slow.