Correct way of extending the context of the typechecker

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

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

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Correct way of extending the context of the typechecker

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