Correct way of extending the context of the typechecker
Simon Peyton Jones
simonpj at microsoft.com
Fri Nov 20 09:02:59 UTC 2020
You might need to explain in a bit more detail.
The simplest thing may be this.
* Define, say, (==>) in some ordinary Haskell source module,
* Look up "Liquid.Haskell.==>", to get its Name, via
* 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
| -----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:
| . 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.
| ghc-devs mailing list
| ghc-devs at haskell.org
More information about the ghc-devs