A couple of GHC-API questions

[Simon Peyton Jones]

| I think part of the confusion is coming from the fact that we don’t
| process each module individually, resolve all of the types, and
| serialize them to disk somewhere. Rather, when we check a module, we
| parse in ALL of the specifications it could possibly refer to (using
| the transitive closure of the module imports) and try to resolve all of
| them before moving to the actual constraint generation and solving
| step.

Yes that makes more sense.

But it's not a good fit with GHC's way of working. You want to take some random module M, parse it afresh to find its LIQUID bits, and then resolve what those things mean.  But that *necessarily* means that you must reconstruct the top-level lexical environment, which is formed from the import and top-level declarations. Constructing this environment -- the GlobalRdrEnv -- is not a simple matter. Much of RnNames does precisely that.

Alas, we do not serialise this environment into M's interface file M.hi.  We could do so, and doing so would be somewhat useful for GHCi, but it's absolutely not needed in the usual way of things.

So I suppose what you could do is to reconstruct it afresh using GHC's existing code to do so.  If you call RnNames.rnImports on the import declarations of your module, you'll get back a GlobalRdrEnv in which you can look up the RdrNames that occur in the LIQUID declarations.

Actually that'll deal only with the imported things.  You also want the locally defined top-level things.  To do that you could use things like getLocalNonValBinders (see the call in RnSource.rnSrcDecls), but it might be easier to take the TypeEnv computed from the module's interface file, and turn that back into a bunch of global binders.

But it's not so easy. What about

	module M( f ) where

	{-# LIQUID f :: { x | ...g... } -> Int
	f = blah

	g = blah

Here g is only mentioned form f's LIQUID spec. So g will have disappeared altogether from M's interface file, discarded as dead code.


The natural alternative would be to serialise the LIQUID things into M.hi. That would entail parsing and renaming them in GHC, and extending the interface file format to handle it.  I think it would be simpler.  But it would be a bit more invasive of GHC.


There is some support for serialising random stuff into interface files, called "annotations".  You write 
	{-# ANN f <Haskell expression> #-}
and GHC will record in the interface file that f is associated with expression.  See http://www.haskell.org/ghc/docs/latest/html/users_guide/extending-ghc.html#annotation-pragmas


Maybe there's a neater way to do this, that neither involves changing GHC nor all the faff above.  If so I'd be happy to change GHC to accommodate the neater way.  I'd like GHC to accommodate extensions like LH much more easily.

Simon


| -----Original Message-----
| From: Eric Seidel [mailto:gridaphobe at gmail.com]
| Sent: 25 July 2014 02:24
| To: Simon Peyton Jones
| Cc: ghc-devs at haskell.org
| Subject: RE: A couple of GHC-API questions
| 
| I think I see where the confusion is now. In your example,
| hscTcRnLookupRdrName should work perfectly. I’m thinking of a different
| scenario, where we are trying to use the specification of a function
| that has been imported from another module. Suppose we have
| 
| module List where
| 
| data List = Nil | Cons Int List
| {-# LIQUID measure length :: List -> Int #-}
| 
| replicate :: Int -> Int -> List
| {-# LIQUID replicate :: x:Int -> n:Int -> {v:List | length v = n } #-}
| 
| head :: List -> Int
| {-# LIQUID head :: {v:List | length v > 0} -> Int #-}
| 
| 
| module Main where
| import qualified List as L
| 
| main = print . L.head $ L.replicate 5 10
| 
| ---
| 
| LiquidHaskell should be able to prove that the call to L.head in
| Main.main is safe. In order to do so we have to first figure out what
| types were given to L.head and L.replicate.
| 
| When we first parse in the specifications from List, we get types that
| refer to the String
| 
|     "List"
| 
| which is parsed into the RdrName
| 
|     Unqual (OccName tcName "List")
| 
| hscTcRnLookupRdrName will *rightly complain* that this RdrName is not
| in scope because we’re currently in the context of Main; we have to
| instead look for it in the top-level environment of the List module.
| 
| I think part of the confusion is coming from the fact that we don’t
| process each module individually, resolve all of the types, and
| serialize them to disk somewhere. Rather, when we check a module, we
| parse in ALL of the specifications it could possibly refer to (using
| the transitive closure of the module imports) and try to resolve all of
| them before moving to the actual constraint generation and solving
| step.
| 
| Does that make more sense?
| 
| Eric
| 
| On July 24, 2014 at 15:54:27, Simon Peyton Jones
| (simonpj at microsoft.com) wrote:
| > | This is what I mean by “resolving” the types. For single-module
| > | programs this is trivial, we can do something like
| > |
| > | resolve x = do rn <- hscParseIdentifier x hscTcRnLookupRdrName rn
| > |
| > | For multi-module programs it becomes trickier because we also have
| > | to resolve the types that we’ve imported from other modules.
| >
| > No, that is no harder **provided those types are in scope**. So
| > suppose you have
| >
| > module M where
| > import A( Foo )
| > f :: Int -> Int
| > {-# LIQUID f :: { x | ..blah..Foo..blah } -> Int #-}
| >
| > Here I am supposing that the Liquid Haskell specification is in a
| > pragma of M, and mentions an imported data type Foo.
| >
| > To resolve the string "Foo" to the Name A.Foo (or Bar.Foo, or
| > whatever), hscTcRnLookupRdrName will work just fine.
| >
| > If you import Foo qualified, then of course you'll have to use a
| > qualified name in the source
| >
| > module M where
| > import qualified A( Foo )
| > f :: Int -> Int
| > {-# LIQUID f :: { x | ..blah..A.Foo..blah } -> Int #-}
| >
| > If you *don't* import Foo at all, then it's utterly non-obvious where
| > to look for it, so I don't suppose you are doing that.
| >
| > In short, why doesn’t hscTcRnLookupRdrName do the job?
|