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 <ghc-devs-boun...@haskell.org> On Behalf Of Yiyun Liu | Sent: 19 November 2020 04:06 | To: ghc-devs@haskell.org | Cc: niki.vazou <niki.va...@imdea.org>; James Parker | <j...@jamesparker.me> | Subject: 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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | ub.com%2Fucsd- | progsys%2Fliquidhaskell%2Fpull%2F1778&data=04%7C01%7Csimonpj%40mic | rosoft.com%7C8ffb59d6e2534efa91d108d88c408d6c%7C72f988bf86f141af91ab2d | 7cd011db47%7C1%7C1%7C637413556756006684%7CUnknown%7CTWFpbGZsb3d8eyJWIj | oiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&am | p;sdata=pl2EqO3TwGC6Br1dQJa5Ej3WDQzN1vngy7HG9A7d9dc%3D&reserved=0) | . 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 | | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail. | haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- | devs&data=04%7C01%7Csimonpj%40microsoft.com%7C8ffb59d6e2534efa91d1 | 08d88c408d6c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637413556756 | 006684%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJ | BTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=heNWVmVkbhTgW1n9kdoKgXL0K | JICoORJOK97uJlEyH0%3D&reserved=0 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs