Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Skip types from a skipped module #166

Open
lastland opened this issue Nov 3, 2020 · 0 comments
Open

Skip types from a skipped module #166

lastland opened this issue Nov 3, 2020 · 0 comments

Comments

@lastland
Copy link
Collaborator

lastland commented Nov 3, 2020

Issue by Lysxia
Saturday Oct 17, 2020 at 20:27 GMT
Originally opened as antalsz/hs-to-coq#166


Trying to translate base-4.14, some modules (like Data.Foldable) mention types from skipped modules (like GHC.Generics.UWord), which causes the translation to fail. In particular, in this case the type is mentioned in an instance so it can't be worked around by skipping the value instead. Actually you can skip an instance, since they are referred to by their Coq name!

A naive solution is to skip uses of types from skipped modules, but the actual situation is a little trickier because those types can also be renamed, in which case they shouldn't be skipped.

This is related to #35 which is about skipping uses of individual types. And #39 would be fixed by the presently proposed feature.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant