universe inconsistency about coq-ext-lib HOT 14 CLOSED

It looks like a universe problem. Generally those are kind of difficult to debug but they also rarely crop up when "simple" things are going on. I don't think that I can debug this without a more complete example. If there is a place where I can see the code, I can take a look.

from coq-ext-lib.

I am attaching self-contained example. Last line of R.v gives the error shown above.

Rtheta.txt
WriterMonadNoT.txt

Thanks!

from coq-ext-lib.

It looks like the issue is with the fact that the writerT is not universe polymorphic. I can fix that in ExtLib and build a new package.

from coq-ext-lib.

Thanks for looking into it and I am looking forward to the fix.

from coq-ext-lib.

This is fixed in ff0e272.

from coq-ext-lib.

Thanks! How soon do you think this fix will propagate to OPAM repository? I would rather avoid installing it manually.

from coq-ext-lib.

I will submit a pull request tonight.

from coq-ext-lib.

Pull request submitted. coq/opam#63

from coq-ext-lib.

After this patch WriterMonadNoT.v no longer compiles:

File "./WriterMonadNoT.v", line 18, characters 33-44:
Error:
In environment
s, t : Type
Monoid_s : Monoid s
x : writerT Monoid_s ident t
The term "runWriter x" has type "PPair.pprod t s"
while it is expected to have type "(?A * ?B)%type".
make: *** [WriterMonadNoT.vo] Error 1

from coq-ext-lib.

In order to (partially) break the dependence on pairs (which introduces some universe constraints), I needed to implement the writer monad using polymorphic pairs. They work essentially the same way as regular pairs except they are polymorphic and use primitive projections (and are therefore more efficient).

from coq-ext-lib.

I have changed in WriterMonadNoT in my example above 'fst' to 'pfst' and 'snd' to 'psnd' after which it compiled without the problem. However the original error still persists:

The term "Monoid_RthetaFlags" has type "Monoid.Monoid RthetaFlags"
while it is expected to have type "Monoid.Monoid ?s" (universe inconsistency).

Here is the line which triggers it:

Definition flags_m : Type -> Type := writer Monoid_RthetaFlags.

from coq-ext-lib.

Hmmm...it is working for me. Here are the two files that you sent me fixed so that they compile.

WriterMonadNoT.txt
Rtheta.txt

from coq-ext-lib.

Sorry, I did not realized I need now specify:

Set Universe Polymorphism.

It solved the problem. Thanks!

from coq-ext-lib.

Ah. I should have pointed that out. U had forgotten that that was the first
thing that I did.

On Tue, Apr 26, 2016, 3:17 PM Vadim Zaliva [email protected] wrote:

Sorry, I did not realized I need not specify:

Set Universe Polymorphism.

It solved the problem. Thanks!

—
You are receiving this because you modified the open/close state.

Reply to this email directly or view it on GitHub
#23 (comment)

• gregory malecha
  gmalecha.github.io

from coq-ext-lib.