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