-
Notifications
You must be signed in to change notification settings - Fork 11
Description
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.