Correct way of extending the context of the typechecker
Hi ghc-devs, Recently we've been trying to merge the typeclass branch of Liquid Haskell into the develop branch (link to the PR: https://github.com/ucsd-progsys/liquidhaskell/pull/1778). Since we want GHC to typecheck the refinements, we had to add some predefined logic symbols such as ==> to the global environment of GHC. In our branch, we use execStmt to add those extra symbols to the interactive context. This is no longer possible after LH becomes available as a GHC plugin because the plugin lives in TcRn. It seems that the only way is to directly interact with the typechecker and explicitly add the extra symbols to the context. It is not obvious to me how that can be done without accidentally breaking the invariants of the compiler. I wonder if there are examples or certain files that I can look into to learn how to interact with the typechecker? Adding the extra symbols is probably not that difficult, but I'd also want to acquire some general knowledge of how the typechecker works to further the integration between LH and GHC so we can remove some of the hacks on our end. Thanks, -Yiyun
Yiyun
You might need to explain in a bit more detail.
The simplest thing may be this.
* Define, say, (==>) in some ordinary Haskell source module,
say Liquid.Haskell
* Look up "Liquid.Haskell.==>", to get its Name, via
GHC.Iface.Env.lookupOrig
* Then you can look up that Name, via GHC.Tc.Utils.Env.tcLookupGlobal
This should load the interface for Liquid.Haskell, if it isn't
already loaded.
Simon
| -----Original Message-----
| From: ghc-devs
participants (2)
-
Simon Peyton Jones -
Yiyun Liu