Current issues of the plugin

[LeventErkok]

The plugin, while it can be useful as is, doesn't really scale in practice. Main problems:

1. Definitions in other modules are not visible
2. It gets utterly confused even with simple uses of polymorphism. Dictionaries in core are hard to track and process correctly. Note that the issue here isn't that we want to support polymorphism: We're completely happy with monomorphic code, but the core we get from GHC has dictionary applications still lying around, which makes the analyzer really complicated. A monomorphising GHC core pass would be most welcome at this point. (And would potentially be useful to other plugins, not just sbv.)
3. It's extremely slow, even when the user is willing to code in a style that avoids the first two problems above. Symbolically simulating the core is tricky due to lots of traversals.

If the plugin is going to see more usage, these problems need to be addressed. Hopefully by someone who is well versed in GHC-core.