A couple of GHC-API questions

[Eric Seidel]

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?