search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
97 stars 21 forks source link

A brief report on trying to port the Iris hierarchy to HB #72

Open Janno opened 4 years ago

Janno commented 4 years ago

Hey everyone,

I was very happy to see the hierarchy builder being announced and I wanted to see what would happen if I used it to define the hierarchy in Iris. This was really just for fun since I do not expect the result to be usable given Iris's reliance on type classes. I also wanted to learn from the resulting definitions since I still don't really understand how one is supposed to set up canonical structures.

But my experiment ended before I got to actually trying out the result. I pushed the experiment to https://gitlab.mpi-sws.org/janno/iris-coq/-/tree/janno/try-HB (the branch name is janno/try-HB). The only file that changed is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v. It contains both old an new definitions, which are confined to lines 150-178. The original file without my new stuff is here: https://gitlab.mpi-sws.org/iris/iris/-/blob/962637df10a879ac4b1b9d523854d6fa4c9e8fb4/theories/bi/interface.v

Of particular interest is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L242 where I cannot get HB to accept the definition of an SBI (an extension of the BI definition in https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L156). The error HB reports is this (when using the right printing settings):

The term "@Some" of type "∀ A : Type, A → option A"
cannot be applied to the terms
 "?e5" : "Type"
 "("is not canonically a", bi.type)" : "(string * Type)%type"

I suppose the underlying error is a mistake on my side but I don't know what it would be.

To get to this point I also had to work around an unexpected shortcoming regarding implicit type class arguments. As you can see in the definition of the BI structure, I had to manually spell out all type class instances since HB would not accept the terms otherwise. (This is veeeeery annoying since it also means that notation such as that for equiv needs to be unfolded.)

Finally, there's something that I wouldn't count as a bug but more of a feature request: in the original Iris hierarchy, the bi_mixin Section (at the top of the file) creates local notation for the operators that make the axioms look very natural. I couldn't find a way to replicate this setup. Maybe HB.mixin could accept where clauses for (local) syntax?

Building the branch My opam switch reports the following packages:

coq-elpi                1.3.1                     Elpi extension language for Coq
coq-hierarchy-builder   0.9.0                     Hierarchy Builder
coq-stdpp               dev.2019-12-06.0.1ef53c55 pinned to version dev.2019-12-06.0.1ef53c55 at git+https://gitlab.mpi-sws.org/iris/stdpp.git

If you want to avoid pinning coq-stdpp to the git hash (the suffix of that weird dev version) you can 

opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

and then opam should be able to find that exact version.

Running make inside a clone of my iris-coq branch should eventually compile interfaces.v and report the errors.

gares commented 4 years ago

Thanks for posting, we will look at it.

gares commented 4 years ago

@CohenCyril The full error, with #[verbose] is:

HB: start module and section Sbi_of_Bi
HB: postulate type PROP
HB: postulate mixin_Bi_of_TYPE on PROP
HB: declare canonical instance PROP_is_a_bi
HB: declare record axioms_
HB: declare notation axioms
HB: declare notation Axioms
elpi: mk-phant-abbrev: T illtyped : 
Illegal application: 
The term "@Some" of type "∀ A : Type, A → option A"
cannot be applied to the terms
 "?e5" : "Type"
 "("is not canonically a", bi.type)" : "(string * Type)%type"
The 2nd term has type "(string * Type)%type" which should be coercible to
 "?e5".
gares commented 4 years ago

Here the term T

(fun (_elpi_ctx_entry_0_ : ?e) (s : bi.type)
   (_ : @unify ?e1 ?e3 _elpi_ctx_entry_0_ (bi.sort s)
          (@Some ?e5
             (@pair ?e7 ?e9
                (String ... EmptyString))))))))))))))))))))
                bi.type))) (c : bi.axioms _elpi_ctx_entry_0_)
   (_ : @unify ?e11 ?e13 s (bi.Pack _elpi_ctx_entry_0_ c) (@None ?e15))
   (m : Bi_of_TYPE.axioms_ _elpi_ctx_entry_0_)
   (_ : @unify ?e17 ?e19 c (bi.Class _elpi_ctx_entry_0_ m) (@None ?e21))
   (sbi_later : forall _ : _elpi_ctx_entry_0_, _elpi_ctx_entry_0_)
   (sbi_internal_eq : forall (T : ofeT) (_ : ofe_car T) (_ : ofe_car T),
                      _elpi_ctx_entry_0_)
   (sbi_mixin_later_intro : forall P : _elpi_ctx_entry_0_,
                            @bi_entails (PROP_is_a_bi _elpi_ctx_entry_0_ m) P
                              (sbi_later P)) =>
 Axioms_ _elpi_ctx_entry_0_ m sbi_later sbi_internal_eq sbi_mixin_later_intro)
gares commented 4 years ago

Looks like a universe issue, the real error message is that @Some ?e (pair "eeee" bi.type) is wrong because the implicit type ?e for Some is not a unifiable with (string * Type) and I suspect it is the type of bi.type that make it fail.

gares commented 4 years ago

I now remark that it is on coq-elpi 1.3. Version 1.4 fixed a couple of universe related bugs. We should try to reproduce the bug in HB master + coq-elpi 1.4