`tagToEnum` and `$con2Tag` unsupported (aka. missing `Deriving` module)

[WhatisRT]

In a file that I'm generating with hs-to-coq, there appears the line Require Deriving.. I don't know why this line is generated (I suspect it is related to the DeriveGeneric or DeriveAnyClass extension), but I cannot find a file named Deriving.v in the hs-to-coq sources.

I can of course skip this with an edit, but I assume this is probably related to several type class instances that I also have to skip to get coq to accept the file. What's the proper solution here?

[sweirich]

Thanks for the report. Can you provide a minimal version of the Haskell source file that is causing this issue?

[nomeata]

Judging from your description, there must be some value or type that hs-to-coq believes lives in a (Haskell) module called Deriving. If you grep through the generated file you should find that value or type, as every name is being used qualified.

[WhatisRT]

The minimal example that generates the Deriving imports is:

module TestModule where

data Test = A | B | C deriving (Eq, Ord)

It is crucial that the type has 3 constructors, with only 2 there is no such import generated. Maybe the deriving keyword is somehow interpreted as an import somewhere?

[WhatisRT]

The same file also generates an Import GHC.Prim.Notations., which also does not exist, and the type class implementations don't work.

[nomeata]

Oh, I have a hunch where there Deriving comes from. hs-to-coq jumps through quite some hoops to make deriving stuff work, maybe something is wrong there.

For the GHC.Prim: Did you run make in base/ and made sure that Coq has that library in the search path (-R ..../base "")?

[WhatisRT]

In the code of the generated instances, there are several lines like let 'lop_azh__ := (_Deriving.$con2tag_6RQENwcLfx1EMY3OJHNIZn_ a) in Do you see these lines too? These cause an issue for me, so I skip every instance that contains such a line.

For the GHC.Prim: yes. I can Require GHC.Prim. fine, but it just doesn't contain a module named Notations.

[nomeata]

Oh, yes, con2tag. I remember. That’s unsupported :-(

If you don’t need these instances in your verification project, then skipping them is the easiest thing you can do.

About GHC.Prim: I guess somewhere in the file there is a qualified operator form the GHC.Prim module that we do not support yet. Can you find it? Which one is it?

[WhatisRT]

I don't think any of these instances are actually required, certainly not in what I'm doing right now.

There are a few lines that mention GHC.Prim in the generated code, I believe these are representative:

    if ((_GHC.Prim.tagToEnum#_ (lop_azh__ GHC.Prim.<# lop_bzh__)) : bool) : bool
    then Lt
    else if ((_GHC.Prim.tagToEnum#_ (lop_azh__ GHC.Prim.==#

I'd assume that the notations get imported because of <# and ==#, but these are not defined in GHC.Prim.

By the way, what is your preferred channel where I could ask questions about hs-to-coq? Is it the deepspec mailing list?

[nomeata]

So if you remove these instances, then both problems go away?

GitHub issues are fine for discussion. But feel free to invade StackOverflow if you have a question that is not a bug report :-)

[WhatisRT]

Yes, exactly.

Ok, thanks, I'll keep it in mind!