Xavier Allamigeon (Jun 15 2021 at 15:00): Xavier Allamigeon (Jun 15 2021 at 15:00):Hi all, I don't understand why the following example (pointed type on top of eqType) doesn't work:
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
HB.mixin Record Foo T of HasDecEq T := {
witness : T
}.
HB.structure Definition PEqType := { T of Foo T & }.
Section Test.
Variable (T : eqType) (x : T).
HB.instance Definition _ := @Foo.Build T x.
End Test.
HB fails with the following error message:
Definition illtyped: In environment
T : eqType
x : T
The term "id_phant" has type "phantom eqType T -> phantom eqType T"
while it is expected to have type
"unify eqType eqType T {| Equality.sort := T; Equality.class := ?a0 |} nomsg".
What am I missing?
Enrico Tassi (Jun 15 2021 at 16:50):I think it's all right, it's your test which does not work well with the way things are set up in HB.
If you are using HB master, I think you should be able to do
HB.declare Context (T : Type) (_ : HasDecEq T).
Here the problem can be worked around by eta expanding by hand the record, untested:
HB.instance Definition _ := Foo.Build (Equality.Pack T (Equality.Class T (Equality.class T)) x.
But you are not supposed to do that. Another way to do it (that is what HB.declare does) is (untested):
Section Test.
Variable T : Type.
Variable p : Equality.axiom T.
HB.instance Definition _ := HasEqDec.Build T p.
Variable x : T.
HB.instance Definition _ := Foo.Build T x.
Thanks a lot @Enrico Tassi, I hadn't used this HB.declarepattern so far, it makes sense.
Last updated: May 28 2023 at 18:29 UTC