Problem with universe polymorphism
SimonBoulier opened this issue · 10 comments
Thank you very much for the release! (installation with opam is very nice)
There seems to be a problem with universe polymorphism.
When I try to extract the dependency graph of the function foo:
Definition foo (A: Type) (B: A -> Type) (C: A -> Type) (c: {x : A & {_ : B x & C x}}) : {x : A & {_ : C x & B x}}.
Proof.
destruct c as [a [b c]].
exists a, c. exact b.
Defined.
It works. But if I precede the definition with Set Universe Polymorphism, it fails with Anomaly: Universe Var(1) undefined. Please report..
I'm afraid, it's lot of work to handle universe polymorphism...
Yes, I reproduced the problem on my machine. Currently, I have no clue about the correction. It may take a while.
The fork ybertot/coq-dpdgraph should contain a version that works better with universe polymorphic constants. @SimonBoulier can you check again?
Well, actually the modified version works less well for non-polymorphic constants. This needs still more work.
The version on ybertot/coq-dpdgraph is now satisfactory. @SimonBoulier Please try it again. I will make a new package for opam after enough testing has happened.
Now, the treatment of polymorphic constants suggests an new feature: polymorphic constants could be detected and displayed in yet another color.
I was just actually trying.
Indeed, it works for the small example.
But for my whole project it fails with:
Anomaly: File "searchdepend.ml4", line 45, characters 4-9: Pattern matching failed.
Please report.
I don't know how to provide you more informations...
Could you give me the whole development?
Yves
----- Mail original -----
De: "SimonBoulier" notifications@github.com
À: "Karmaki/coq-dpdgraph" coq-dpdgraph@noreply.github.com
Cc: "Yves Bertot" yves.bertot@inria.fr
Envoyé: Mercredi 16 Mars 2016 17:10:03
Objet: Re: [coq-dpdgraph] Problem with universe polymorphism (#2)I was just actually trying.
Indeed, it works for the small example.
But for my whole project it fails with:Anomaly: File "searchdepend.ml4", line 45, characters 4-9: Pattern matching
failed.Please report.
I don't know how to provide you more informations...
—
You are receiving this because you commented.
Reply to this email directly or view it on GitHub
The error message you gave me was enough to find a bug that is fixed in the version commited a few minutes ago. The reason must be that you also use "primitive projections". These projections did not exist in previous versions of Coq, and the case was not covered in the file. The version that was just committe should correct this problem.
Wonderful, it works !!!
Thank you very much.
On 03/17/2016 08:16 AM, SimonBoulier wrote:
Wonderful, it works !!!
Thank you very much.—
You are receiving this because you commented.
Reply to this email directly or view it on GitHub
#2 (comment)Ok, we may tag this version then and make it available through opam.
Alternatively, we may work on an improvement to highlight polymorphic
constants in a different color before making the tag. I will ask Coq
developers about the feasibility of this improvement.
With my best,
Yves