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 ([email protected]) 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?
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
