hs-to-coq icon indicating copy to clipboard operation
hs-to-coq copied to clipboard

Skip types from a skipped module

Open Lysxia opened this issue 4 years ago • 0 comments

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.

Lysxia avatar Oct 17 '20 20:10 Lysxia