Skip to content

Skip types from a skipped module #166

@lastland

Description

@lastland

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions