Stream: Hierarchy Builder devs & users

Topic: Strange error with eqType

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Enrico Tassi (Jun 15 2021 at 16:55):

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.

view this post on Zulip Enrico Tassi (Jun 15 2021 at 17:00):

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.

view this post on Zulip Xavier Allamigeon (Jun 18 2021 at 06:42):

Thanks a lot @Enrico Tassi, I hadn't used this HB.declarepattern so far, it makes sense.

Last updated: Jan 29 2023 at 15:02 UTC