hs-to-coq
hs-to-coq copied to clipboard
Skip types from a skipped module
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.