diff --git a/djinn-ghc.cabal b/djinn-ghc.cabal
--- a/djinn-ghc.cabal
+++ b/djinn-ghc.cabal
@@ -1,5 +1,5 @@
 name:           djinn-ghc
-version:        0.0.1
+version:        0.0.2
 synopsis:       Generate Haskell code from a type. Bridge from Djinn to GHC API.
 description:    Djinn uses an theorem prover for intuitionistic propositional logic
                 to generate a Haskell expression when given a type.
@@ -15,8 +15,10 @@
 library
   exposed-modules:  Djinn.GHC
   build-depends:    base >= 4 && < 5,
-                    mtl < 2.2,
+                    mtl,
                     ghc,
                     containers,
-                    djinn-lib == 0.0.1
+                    transformers,
+                    djinn-lib >= 0.0.1.1,
+                    async
   hs-source-dirs:   src
diff --git a/src/Djinn/GHC.hs b/src/Djinn/GHC.hs
--- a/src/Djinn/GHC.hs
+++ b/src/Djinn/GHC.hs
@@ -1,12 +1,16 @@
-{-# LANGUAGE PatternGuards #-}
-module Djinn.GHC (djinn) where
+{-# LANGUAGE PatternGuards, BangPatterns #-}
+module Djinn.GHC (Environment, MaxSolutions(..), djinn) where
 
+import Control.Concurrent
+import Control.Concurrent.Async
 import Control.Monad (forM)
+import Data.Maybe (isJust)
 import Data.Set (Set, insert, union, unions, empty, toList)
 
 import qualified Djinn.HTypes as D
 import qualified Djinn.LJT as D
 
+import MonadUtils
 import qualified DataCon as G
 import qualified GHC as G
 import qualified Name as G
@@ -19,10 +23,12 @@
 
 getConTs :: G.Type -> Set G.Name
 getConTs t | Just (_, i)  <- G.splitForAllTy_maybe t = getConTs i
+getConTs t | Just (t1,t2) <- G.splitFunTy_maybe t    = getConTs t1 `union` getConTs t2
 getConTs t | Just (c, ts) <- G.splitTyConApp_maybe t = 
   let args = unions $ map getConTs ts
    in if G.isTupleTyCon c then args else insert (G.getName c) args
 getConTs t | Just (t1,t2) <- G.splitAppTy_maybe t    = getConTs t1 `union` getConTs t2
+getConTs t | Just _       <- G.getTyVar_maybe t      = empty
 getConTs _                                           = empty
 
 hType :: G.Type -> D.HType
@@ -39,12 +45,12 @@
 hType t | Just var <- G.getTyVar_maybe t          = D.HTVar (toHSymbol var)
 hType _                                           = error "Unimplemented"
 
-environment :: G.GhcMonad m => G.Type -> m HEnvironment
-environment = fmap concat . mapM environment1 . toList . getConTs
+environment :: G.GhcMonad m => Maybe G.ModuleInfo -> G.Type -> m HEnvironment
+environment minfo = fmap concat . mapM (environment1 minfo) . toList . getConTs
 
-environment1 :: G.GhcMonad m => G.Name -> m HEnvironment
-environment1 name = do
-  thing <- G.lookupGlobalName name
+environment1 :: G.GhcMonad m => Maybe G.ModuleInfo -> G.Name -> m HEnvironment
+environment1 minfo name = do
+  thing <- lookupNameEverywhere minfo name
   case thing of
     Just (G.ATyCon tycon) | G.isAlgTyCon tycon -> do
       let tyconName = toHSymbol $ G.tyConName tycon
@@ -53,7 +59,7 @@
       dtypes <- forM datacons $ \dcon -> do
         let dconN = toHSymbol $ G.dataConName dcon
             (_,_,dconT,_) = G.dataConSig dcon
-        dconE <- mapM environment dconT
+        dconE <- mapM (environment minfo) dconT
         return ((dconN, map hType dconT), dconE)
       let dtypesT = map fst dtypes
           dtypesE = concatMap snd dtypes
@@ -65,20 +71,51 @@
           varsH = map toHSymbol vars
           htype = hType defn
       -- Recursively obtain it for the environment of the type
-      defnEnv <- environment defn
+      defnEnv <- environment minfo defn
       return $ (tyconName, (varsH, htype, NoExtraInfo)) : defnEnv
     _ -> return []
 
+lookupNameEverywhere :: G.GhcMonad m => Maybe G.ModuleInfo -> G.Name -> m (Maybe G.TyThing)
+lookupNameEverywhere (Just minfo) name = do
+  thing <- G.modInfoLookupName minfo name
+  if isJust thing then return thing else G.lookupGlobalName name
+lookupNameEverywhere Nothing    name = G.lookupGlobalName name
+
 toHSymbol :: G.NamedThing a => a -> D.HSymbol
 toHSymbol = G.getOccString
 
+toLJTSymbol :: G.NamedThing a => a -> D.Symbol
+toLJTSymbol = D.Symbol . G.getOccString
+
+-- |Bindings which are in scope at a specific point.
+type Environment = [(G.Name, G.Type)]
+
+-- |Obtain a maximum number of solutions.
+newtype MaxSolutions = Max Int
+
 -- |Obtain the list of expressions which could fill
 -- something with the given type.
 -- The first flag specifies whether to return one
 -- or more solutions to the problem.
-djinn :: G.GhcMonad m => Bool -> G.Type -> m [String]
-djinn multi ty = do
-  env <- environment ty
-  let form = D.hTypeToFormula env (hType ty)
-      prfs = D.prove multi [] form
-  return $ map show prfs
+djinn :: G.GhcMonad m => Bool -> Maybe G.ModuleInfo -> Environment -> G.Type -> MaxSolutions -> Int -> m [String]
+djinn multi minfo env ty (Max mx) microsec = do
+  tyEnv <- environment minfo ty
+  let form = D.hTypeToFormula tyEnv (hType ty)
+      envF = map (\(n,t) -> (toLJTSymbol n, D.hTypeToFormula tyEnv (hType t))) env
+      prfs = D.prove multi envF form
+      trms = map (D.hPrExpr . D.termToHExpr) prfs
+  liftIO $ cropList trms microsec mx
+
+cropList :: [a] -> Int -> Int -> IO [a]
+cropList _   _  0 = return []
+cropList lst ms n = withAsync (let !l = lst in return l) $ \a -> do
+                      threadDelay ms
+                      res <- poll a
+                      case res of
+                        Just r -> case r of
+                          Right (x:xs) -> do ys <- cropList xs ms (n-1)
+                                             return $ x : ys
+                          _            -> return []
+                        Nothing -> do cancel a
+                                      return []
+