Eric I'd like to help but I don't understand the question. What do you mean by "resolve" all the types that are imported from module A? If you have a TyCon (for A.Foo) in your hand, it has a Name. That Name tells you where it comes from. Inside it you will find its DataCons which also come from A. And so on. Later you say "is there a simple way to ask GHC to resolve the name x in the context of module m". You could mean * Imagine that the unqualified name "x" appeared in module m. How do I look it up, in m's top-level lexical environment. but I don’t think that is what you mean. I'm confused. Could you be more concrete? Possibly this may help? https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/NameType I'm cc'ing ghc-devs. Simon | -----Original Message----- | From: Eric Seidel [mailto:eseidel@cs.ucsd.edu] | Sent: 23 July 2014 19:01 | To: Simon Peyton Jones | Subject: A couple of GHC-API questions | | Hi Simon, | | I have a couple of questions about how to use GHC’s API properly. | There’s nothing urgent here as we’re making due just fine in | LiquidHaskell, but I’m pretty sure we’re hacking around GHC when we | don’t need to :) | | As you probably know, we basically use GHC to get the Core binders of a | module, and to resolve a bunch of names. Translating to Core has never | been an issue for us as far as I know, but our name-resolution code is | very haphazard. The core of our problems with name-resolution comes | down to resolving the names in specifications that have been imported | from another module, e.g. | | module A where | data Foo | mkFoo :: {v:Int | v >= 0} -> Foo | ... | | module B where | import qualified A | ... | | When we verify module B we have to first resolve all of the types that | were imported from module A, *but* we can’t do that in the context of | module B due to the qualified import. So I’ve been using a slightly | modified version of GHC’s DynamicLoading.lookupRdrNameInModule to | handle the change of context, but this seems to require that we use the | HscInterpreted flag, which causes further problems for a few of our | benchmarks that make use of the C FFI.. This method also only works for | modules where we actually have the source code available, i.e. we have | to use a different method of looking up names to attach specifications | to functions from the base libraries. | | So I guess my question is this: is there a simple way to ask GHC to | resolve the name x in the context of module m, without invoking the | code generator or any other part of GHC’s functionality? I suppose a | more principled solution would be to somehow hook into the .hi files | that GHC generates, but I’m not sure if that’s possible. | | Again, the code we have right now works, it’s just very fragile and I’d | like to clean things up. | | Thanks! | | Eric