Correct way of extending the context of the typechecker

[Yiyun Liu]

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