Towards a direct (non plugin-based) API

[gergoerdi]

For users that need to do custom steps on the way to a full TypecheckedModule, it'd make sense to provide an API that directly consumes the TypecheckedModule.

[facundominguez]

The title of the PR intrigues me, but the changes in the last commit look ok.

[facundominguez]

Regarding the unoptimiseDynFlags setting, I think it is possible that we can get rid of it.

When I remove it, many failures seem to be related to the fact that tcg_exports does not contain all identifiers that are in scope anymore. For instance, LH complains that bar is not in scope in the following test

module LocalSpec() where

import Language.Haskell.Liquid.Prelude (choose)

prop = if x > 0 then bar x else x
  where x = choose 0
    {-@ bar :: Nat -> Nat @-}
        bar :: Int -> Int
        bar x = x

{-@ bar :: a -> {v:Int | v = 9} @-}
bar :: a -> Int
bar _ = 9

but if I open the export list, then verification passes again

-module LocalSpec() where
+module LocalSpec where

Fixing this might require building LH environment from names in scope rather than tcg_exports (perhaps tcg_rdr_env).

Update: Looking up for TyThings for everything in tcg_rdr_env seems too slow. We might need to rearrange things to only lookup TyThings that are actually needed. This connects a bit to #2169.

[gergoerdi]

The title of the PR intrigues me, but the changes in the last commit look ok.

Basically, I'm thinking of a "bring-your-own-TypecheckedModule" API for users that are not GHC itself, but rather programs using the GHC API and using any kind of out-of-band inter-phase communication.

For example, in that setting, "the" parsed module as seen by a plugin (LH or otherwise) might not actually be the right module if the API client needs to do some postprocessing on it.

[gergoerdi]

Regarding the unoptimiseDynFlags setting, I think it is possible that we can get rid of it.

Indeed, the only part of unoptimiseDynFlags that should matter anymore is setting the backend to interpreterBackend. Relying on tcg_exports to find out what is in a module is the wrong approach anyway, so I hope you'll be able to remove that. Meanwhile I'll remove all other DynFlags fiddling in an update to #2389.

[gergoerdi]

Fixing this might require building LH environment from names in scope rather than tcg_exports (perhaps tcg_rdr_env).

Update: Looking up for TyThings for everything in tcg_rdr_env seems too slow. We might need to rearrange things to only lookup TyThings that are actually needed. This connects a bit to #2169.

Could you point me to where exactly this is? Do you mean availVars / availTyCons as computed in mkPipelineData?

Whether you should use tcg_exports or not depends on why you need these Ids and TyCons. If you need them to check them, then it should be completely divorced from questions of exporting -- imagine if GHC only typechecked definitions that are exported...! You should only care about tcg_exports (or, actually, mg_exports since we should move as much as we can to only consuming the ModGuts, in anticipation of a glorious future where we can plug into GHC's desugared output directly instead of starting from a TcGblEnv and doing it ourselves) if you need to make decisions based on whether a given thing is exported or not.

Also, if you need all this so you can match user-written occurrences in LH specs to the GHC side, you shouldn't need to build anything from the mg_rdr_env :: GlobalRdrEnv, because that is already the thing you can use to look up names in!

[facundominguez]

Could you point me to where exactly this is? Do you mean availVars / availTyCons as computed in mkPipelineData?

That's the place.