Correct way of extending the context of the typechecker

[Simon Peyton Jones]

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-bounces at haskell.org> On Behalf Of Yiyun Liu
|  Sent: 19 November 2020 04:06
|  To: ghc-devs at haskell.org
|  Cc: niki.vazou <niki.vazou at imdea.org>; James Parker
|  <jp at 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 at 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