diff --git a/include/Control/Monad.spec b/include/Control/Monad.spec
deleted file mode 100644
--- a/include/Control/Monad.spec
+++ /dev/null
@@ -1,3 +0,0 @@
-module spec Control.Monad where
-
-sequence :: GHC.Base.Monad m => xs:[m a] -> m {v:[a] | (len v) = (len xs)}
diff --git a/include/Data/Foldable.spec b/include/Data/Foldable.spec
new file mode 100644
--- /dev/null
+++ b/include/Data/Foldable.spec
@@ -0,0 +1,5 @@
+module spec Data.Foldable where
+
+import GHC.Base
+
+assume length :: Data.Foldable.Foldable f => xs:f a -> {v:Nat | v = len xs}
diff --git a/include/Data/List.spec b/include/Data/List.spec
--- a/include/Data/List.spec
+++ b/include/Data/List.spec
@@ -1,21 +1,11 @@
 module spec Data.List where
 
+import GHC.Base
 import GHC.List
 import GHC.Types
 
 assume groupBy :: (a -> a -> GHC.Types.Bool) -> [a] -> [{v:[a] | len(v) > 0}]
 
 assume transpose :: [[a]] -> [{v:[a] | (len v) > 0}]
-
-// assume GHC.List.concat :: x:[[a]] -> {v:[a] | (len v) = (sumLens x)}
-//
-// measure sumLens :: [[a]] -> GHC.Types.Int
-//     sumLens ([])   = 0
-//     sumLens (c:cs) = (len c) + (sumLens cs)
-//
-// invariant {v:[[a]] | (sumLens v) >= 0}
-// qualif SumLensEq(v:List List a, x:List List a): (sumLens v) = (sumLens x)
-// qualif SumLensEq(v:List List a, x:List a): (sumLens v) = (len x)
-// qualif SumLensLe(v:List List a, x:List List a): (sumLens v) <= (sumLens x)
 
 
diff --git a/include/GHC/Base.spec b/include/GHC/Base.spec
--- a/include/GHC/Base.spec
+++ b/include/GHC/Base.spec
@@ -9,7 +9,8 @@
 
 measure Prop   :: GHC.Types.Bool -> Prop
 
-measure len :: forall a. [a] -> GHC.Types.Int
+class measure len :: forall f a. f a -> GHC.Types.Int
+instance measure len :: forall a. [a] -> GHC.Types.Int
 len []     = 0
 len (y:ys) = 1 + len ys
 
diff --git a/include/Prelude.spec b/include/Prelude.spec
--- a/include/Prelude.spec
+++ b/include/Prelude.spec
@@ -7,6 +7,7 @@
 import GHC.Real
 import GHC.Word
 
+import Data.Foldable
 import Data.Maybe
 import GHC.Exts
 
diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal
--- a/liquidhaskell.cabal
+++ b/liquidhaskell.cabal
@@ -1,5 +1,5 @@
 Name:                liquidhaskell
-Version:             0.4.0.1
+Version:             0.4.1.0
 Copyright:           2010-15 Ranjit Jhala, University of California, San Diego.
 build-type:          Simple
 Synopsis:            Liquid Types for Haskell 
@@ -44,8 +44,13 @@
 
 --Flag devel
 --  Description: turn on stricter error reporting for development
---  Default:     True
+--  Default:     False
+--  Manual:      True
 
+Flag include
+  Description: use in-tree include directory
+  Default:     False
+
 Executable liquid
   default-language: Haskell98
   Build-Depends: base >= 4 && < 5
@@ -83,7 +88,7 @@
                , liquidhaskell
 
   Main-is: Liquid.hs
-  ghc-options: -W
+  ghc-options: -W -fno-warn-unused-imports -fno-warn-dodgy-imports -fno-warn-deprecated-flags -fno-warn-deprecations
 --  if flag(devel)
 --    ghc-options: -Werror
   Default-Extensions: PatternGuards
@@ -159,7 +164,7 @@
                 , bytestring
                 , fingertree
  
-   hs-source-dirs:  include, src
+   hs-source-dirs:  src, include
  
    Exposed-Modules: Language.Haskell.Liquid.Prelude,
                     Language.Haskell.Liquid.Foreign, 
@@ -221,6 +226,8 @@
                     Language.Haskell.Liquid.Bare.SymSort
                     Language.Haskell.Liquid.Bare.Spec
 
+   if impl(ghc < 7.10)
+     exposed-modules:
                     --NOTE: these need to be exposed so GHC generates .dyn_o files for them..
                     Language.Haskell.Liquid.Desugar.Desugar,
                     Language.Haskell.Liquid.Desugar.DsExpr,
@@ -237,10 +244,12 @@
                     Language.Haskell.Liquid.Desugar.DsBinds,
                     Language.Haskell.Liquid.Desugar.DsGRHSs,
                     Language.Haskell.Liquid.Desugar.HscMain
-   ghc-options: -W
+   ghc-options: -W -fno-warn-unused-imports -fno-warn-dodgy-imports -fno-warn-deprecated-flags -fno-warn-deprecations
 --   if flag(devel)
 --     ghc-options: -Werror
---   ghc-prof-options: -fprof-auto
+   if flag(include)
+     hs-source-dirs: devel
+   ghc-prof-options: -fprof-auto
    Default-Extensions: PatternGuards
 
 test-suite test
diff --git a/src/Language/Haskell/Liquid/ACSS.hs b/src/Language/Haskell/Liquid/ACSS.hs
--- a/src/Language/Haskell/Liquid/ACSS.hs
+++ b/src/Language/Haskell/Liquid/ACSS.hs
@@ -4,7 +4,7 @@
   , hsannot
   , AnnMap (..)
   , breakS
-  , srcModuleName 
+  , srcModuleName
   , Status (..)
   ) where
 
@@ -14,30 +14,30 @@
 import qualified Language.Haskell.HsColour.CSS as CSS
 
 import Data.Either (partitionEithers)
-import Data.Maybe  (fromMaybe) 
+import Data.Maybe  (fromMaybe)
 import qualified Data.HashMap.Strict as M
 import Data.List   (find, isPrefixOf, findIndex, elemIndices, intercalate)
 import Data.Char   (isSpace)
 import Text.Printf
 import Language.Haskell.Liquid.GhcMisc
 
-data AnnMap  = Ann { 
+data AnnMap  = Ann {
     types  :: M.HashMap Loc (String, String) -- ^ Loc -> (Var, Type)
   , errors :: [(Loc, Loc, String)]           -- ^ List of error intervals
-  , status :: !Status          
-  } 
-  
-data Status = Safe | Unsafe | Error | Crash 
+  , status :: !Status
+  }
+
+data Status = Safe | Unsafe | Error | Crash
               deriving (Eq, Ord, Show)
 
-data Annotation = A { 
+data Annotation = A {
     typ :: Maybe String         -- ^ type  string
-  , err :: Maybe String         -- ^ error string 
-  , lin :: Maybe (Int, Int)     -- ^ line number, total width of lines i.e. max (length (show lineNum)) 
+  , err :: Maybe String         -- ^ error string
+  , lin :: Maybe (Int, Int)     -- ^ line number, total width of lines i.e. max (length (show lineNum))
   } deriving (Show)
 
 
--- | Formats Haskell source code using HTML and mouse-over annotations 
+-- | Formats Haskell source code using HTML and mouse-over annotations
 hscolour :: Bool     -- ^ Whether to include anchors.
          -> Bool     -- ^ Whether input document is literate haskell or not
          -> String   -- ^ Haskell source code, Annotations as comments at end
@@ -47,9 +47,9 @@
 
 type CommentTransform = Maybe (String -> [(TokenType, String)])
 
--- | Formats Haskell source code using HTML and mouse-over annotations 
+-- | Formats Haskell source code using HTML and mouse-over annotations
 hsannot  :: Bool             -- ^ Whether to include anchors.
-         -> CommentTransform -- ^ Function to refine comment tokens 
+         -> CommentTransform -- ^ Function to refine comment tokens
          -> Bool             -- ^ Whether input document is literate haskell or not
          -> (String, AnnMap) -- ^ Haskell Source, Annotations
          -> String           -- ^ Coloured Haskell source code.
@@ -63,7 +63,7 @@
 litSpans lits = zip lits $ spans lits
   where spans = tokenSpans Nothing . map unL
 
-hsannot' baseLoc anchor tx = 
+hsannot' baseLoc anchor tx =
     CSS.pre
     . (if anchor then concatMap (renderAnchors renderAnnotToken)
                       . insertAnnotAnchors
@@ -72,26 +72,26 @@
 
 -- | annotTokenise is absurdly slow: O(#tokens x #errors)
 
-annotTokenise :: Maybe Loc -> CommentTransform -> (String, AnnMap) -> [(TokenType, String, Annotation)] 
-annotTokenise baseLoc tx (src, annm) = zipWith (\(x,y) z -> (x,y,z)) toks annots 
-  where 
-    toks       = tokeniseWithCommentTransform tx src 
-    spans      = tokenSpans baseLoc $ map snd toks 
+annotTokenise :: Maybe Loc -> CommentTransform -> (String, AnnMap) -> [(TokenType, String, Annotation)]
+annotTokenise baseLoc tx (src, annm) = zipWith (\(x,y) z -> (x,y,z)) toks annots
+  where
+    toks       = tokeniseWithCommentTransform tx src
+    spans      = tokenSpans baseLoc $ map snd toks
     annots     = fmap (spanAnnot linWidth annm) spans
     linWidth   = length $ show $ length $ lines src
 
-spanAnnot w (Ann ts es _) span = A t e b 
-  where 
+spanAnnot w (Ann ts es _) span = A t e b
+  where
     t = fmap snd (M.lookup span ts)
     e = fmap (\_ -> "ERROR") $ find (span `inRange`) [(x,y) | (x,y,_) <- es]
     b = spanLine w span
 
-spanLine w (L (l, c)) 
-  | c == 1    = Just (l, w) 
+spanLine w (L (l, c))
+  | c == 1    = Just (l, w)
   | otherwise = Nothing
 
-inRange (L (l0, c0)) (L (l, c), L (l', c')) 
-  = l <= l0 && c <= c0 && l0 <= l' && c0 < c' 
+inRange (L (l0, c0)) (L (l, c), L (l', c'))
+  = l <= l0 && c <= c0 && l0 <= l' && c0 < c'
 
 tokeniseWithCommentTransform :: Maybe (String -> [(TokenType, String)]) -> String -> [(TokenType, String)]
 tokeniseWithCommentTransform Nothing  = tokenise
@@ -100,10 +100,10 @@
         expand _ z            = [z]
 
 tokenSpans :: Maybe Loc -> [String] -> [Loc]
-tokenSpans = scanl plusLoc . fromMaybe (L (1, 1)) 
+tokenSpans = scanl plusLoc . fromMaybe (L (1, 1))
 
 plusLoc :: Loc -> String -> Loc
-plusLoc (L (l, c)) s 
+plusLoc (L (l, c)) s
   = case '\n' `elemIndices` s of
       [] -> L (l, (c + n))
       is -> L ((l + length is), (n - maximum is))
@@ -111,19 +111,19 @@
 
 renderAnnotToken :: (TokenType, String, Annotation) -> String
 renderAnnotToken (x, y, a)  = renderLinAnnot (lin a)
-                            $ renderErrAnnot (err a) 
-                            $ renderTypAnnot (typ a) 
+                            $ renderErrAnnot (err a)
+                            $ renderTypAnnot (typ a)
                             $ CSS.renderToken (x, y)
 
 
 
 renderTypAnnot (Just ann) s = printf "<a class=annot href=\"#\"><span class=annottext>%s</span>%s</a>" (escape ann) s
-renderTypAnnot Nothing    s = s     
+renderTypAnnot Nothing    s = s
 
-renderErrAnnot (Just _) s   = printf "<span class=hs-error>%s</span>" s 
+renderErrAnnot (Just _) s   = printf "<span class=hs-error>%s</span>" s
 renderErrAnnot Nothing  s   = s
 
-renderLinAnnot (Just d) s   = printf "<span class=hs-linenum>%s: </span>%s" (lineString d) s 
+renderLinAnnot (Just d) s   = printf "<span class=hs-linenum>%s: </span>%s" (lineString d) s
 renderLinAnnot Nothing  s   = s
 
 lineString (i, w) = (replicate (w - (length is)) ' ') ++ is
@@ -136,25 +136,25 @@
 
 
 insertAnnotAnchors :: [(TokenType, String, a)] -> [Either String (TokenType, String, a)]
-insertAnnotAnchors toks 
+insertAnnotAnchors toks
   = stitch (zip toks' toks) $ insertAnchors toks'
-  where toks' = [(x,y) | (x,y,_) <- toks] 
+  where toks' = [(x,y) | (x,y,_) <- toks]
 
 stitch ::  Eq b => [(b, c)] -> [Either a b] -> [Either a c]
 stitch xys ((Left a) : rest)
   = (Left a) : stitch xys rest
-stitch ((x,y):xys) ((Right x'):rest) 
-  | x == x' 
+stitch ((x,y):xys) ((Right x'):rest)
+  | x == x'
   = (Right y) : stitch xys rest
   | otherwise
   = error "stitch"
 stitch _ []
   = []
-stitch _ _ 
+stitch _ _
   = error "stitch: cannot happen"
 
-splitSrcAndAnns ::  String -> (String, AnnMap) 
-splitSrcAndAnns s = 
+splitSrcAndAnns ::  String -> (String, AnnMap)
+splitSrcAndAnns s =
   let ls = lines s in
   case findIndex (breakS ==) ls of
     Nothing -> (s, Ann M.empty [] Safe)
@@ -165,26 +165,26 @@
 
 srcModuleName :: String -> String
 srcModuleName = fromMaybe "Main" . tokenModule . tokenise
-  
-tokenModule toks 
-  = do i <- findIndex ((Keyword, "module") ==) toks 
+
+tokenModule toks
+  = do i <- findIndex ((Keyword, "module") ==) toks
        let (_, toks')  = splitAt (i+2) toks
        j <- findIndex ((Space ==) . fst) toks'
        let (toks'', _) = splitAt j toks'
        return $ concatMap snd toks''
 
-breakS = "MOUSEOVER ANNOTATIONS" 
+breakS = "MOUSEOVER ANNOTATIONS"
 
 annotParse :: String -> String -> AnnMap
 annotParse mname s = Ann (M.fromList ts) [(x,y,"") | (x,y) <- es] Safe
-  where 
+  where
     (ts, es)       = partitionEithers $ parseLines mname 0 $ lines s
 
 
-parseLines _ _ [] 
+parseLines _ _ []
   = []
 
-parseLines mname i ("":ls)      
+parseLines mname i ("":ls)
   = parseLines mname (i+1) ls
 
 parseLines mname i (_:_:l:c:"0":l':c':rest')
@@ -194,10 +194,10 @@
           line' = (read l') :: Int
           col'  = (read c') :: Int
 
-parseLines mname i (x:f:l:c:n:rest) 
+parseLines mname i (x:f:l:c:n:rest)
   | f /= mname
   = parseLines mname (i + 5 + num) rest'
-  | otherwise 
+  | otherwise
   = Left (L (line, col), (x, anns)) : parseLines mname (i + 5 + num) rest'
     where line  = (read l) :: Int
           col   = (read c) :: Int
@@ -205,14 +205,14 @@
           anns  = intercalate "\n" $ take num rest
           rest' = drop num rest
 
-parseLines _ i _              
+parseLines _ i _
   = error $ "Error Parsing Annot Input on Line: " ++ show i
 
 instance Show AnnMap where
   show (Ann ts es _ ) =  "\n\n" ++ (concatMap ppAnnotTyp $ M.toList ts)
                                 ++ (concatMap ppAnnotErr [(x,y) | (x,y,_) <- es])
-      
-ppAnnotTyp (L (l, c), (x, s))     = printf "%s\n%d\n%d\n%d\n%s\n\n\n" x l c (length $ lines s) s 
+
+ppAnnotTyp (L (l, c), (x, s))     = printf "%s\n%d\n%d\n%d\n%s\n\n\n" x l c (length $ lines s) s
 ppAnnotErr (L (l, c), L (l', c')) = printf " \n%d\n%d\n0\n%d\n%d\n\n\n\n" l c l' c'
 
 
@@ -230,8 +230,8 @@
 inlines s = lines' s id
   where
   lines' []             acc = [acc []]
-  lines' ('\^M':'\n':s) acc = acc ['\n'] : lines' s id	-- DOS
-  lines' ('\n':s)       acc = acc ['\n'] : lines' s id	-- Unix
+  lines' ('\^M':'\n':s) acc = acc ['\n'] : lines' s id  -- DOS
+  lines' ('\n':s)       acc = acc ['\n'] : lines' s id  -- Unix
   lines' (c:s)          acc = lines' s (acc . (c:))
 
 
@@ -246,7 +246,7 @@
 classify (x:xs)         = Lit x: classify xs
 
 
-allProg name  = go 
+allProg name  = go
   where
     end       = "\\end{" ++ name ++ "}"
     go []     = []  -- Should give an error message,
@@ -262,4 +262,3 @@
 joinL (Code c:Code c2:xs) = joinL (Code (c++c2):xs)
 joinL (Lit c :Lit c2 :xs) = joinL (Lit  (c++c2):xs)
 joinL (any:xs)            = any: joinL xs
-
diff --git a/src/Language/Haskell/Liquid/ANFTransform.hs b/src/Language/Haskell/Liquid/ANFTransform.hs
--- a/src/Language/Haskell/Liquid/ANFTransform.hs
+++ b/src/Language/Haskell/Liquid/ANFTransform.hs
@@ -22,7 +22,7 @@
 import           Outputable                       (trace)
 import           Var                              (varType, setVarType)
 import           TypeRep
-import           Type                             (mkForAllTys, substTy, mkForAllTys, mkTopTvSubst)
+import           Type                             (mkForAllTys, substTy, mkForAllTys, mkTopTvSubst, isTyVar)
 import           TyCon                            (tyConDataCons_maybe)
 import           DataCon                          (dataConInstArgTys)
 import           FamInstEnv                       (emptyFamInstEnv)
@@ -70,10 +70,10 @@
   = do xes' <- runDsM $ execStateT (normalizeBind γ (Rec xes)) (DsST expandFlag [])
        return $ map normalizeTyVars (st_binds xes')
 
-normalizeTyVars (NonRec x e) = NonRec (setVarType x t') e
+normalizeTyVars (NonRec x e) = NonRec (setVarType x t') $ normalizeForAllTys e
   where t'       = subst msg as as' bt
         msg      = "WARNING unable to renameVars on " ++ showPpr x
-        as'      = fst $ collectTyBinders e
+        as'      = fst $ splitForAllTys $ exprType e
         (as, bt) = splitForAllTys (varType x)
 normalizeTyVars (Rec xes)    = Rec xes'
   where nrec = normalizeTyVars <$> ((\(x, e) -> NonRec x e) <$> xes)
@@ -85,6 +85,15 @@
   | otherwise
   = trace msg $ mkForAllTys as bt
   where su = mkTopTvSubst $ zip as (mkTyVarTys as')
+
+-- | eta-expand CoreBinds with quantified types
+normalizeForAllTys :: CoreExpr -> CoreExpr
+normalizeForAllTys e = case e of
+  Lam b _ | isTyVar b
+    -> e
+  _ -> mkLams tvs (mkTyApps e (map mkTyVarTy tvs))
+  where
+  (tvs, _) = splitForAllTys (exprType e)
 
 
 newtype DsM a = DsM {runDsM :: DsMonad.DsM a}
diff --git a/src/Language/Haskell/Liquid/Annotate.hs b/src/Language/Haskell/Liquid/Annotate.hs
--- a/src/Language/Haskell/Liquid/Annotate.hs
+++ b/src/Language/Haskell/Liquid/Annotate.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE TupleSections              #-}
 {-# LANGUAGE NoMonomorphismRestriction  #-}
 {-# LANGUAGE OverloadedStrings          #-}
diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs
--- a/src/Language/Haskell/Liquid/Bare/DataType.hs
+++ b/src/Language/Haskell/Liquid/Bare/DataType.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE TupleSections #-}
 
 module Language.Haskell.Liquid.Bare.DataType (
diff --git a/src/Language/Haskell/Liquid/Bare/Env.hs b/src/Language/Haskell/Liquid/Bare/Env.hs
--- a/src/Language/Haskell/Liquid/Bare/Env.hs
+++ b/src/Language/Haskell/Liquid/Bare/Env.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE FlexibleContexts         #-}
+
 module Language.Haskell.Liquid.Bare.Env (
     BareM
   , Warn
diff --git a/src/Language/Haskell/Liquid/Bare/GhcSpec.hs b/src/Language/Haskell/Liquid/Bare/GhcSpec.hs
--- a/src/Language/Haskell/Liquid/Bare/GhcSpec.hs
+++ b/src/Language/Haskell/Liquid/Bare/GhcSpec.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE RecordWildCards           #-}
 {-# LANGUAGE ViewPatterns              #-}
diff --git a/src/Language/Haskell/Liquid/Bare/Lookup.hs b/src/Language/Haskell/Liquid/Bare/Lookup.hs
--- a/src/Language/Haskell/Liquid/Bare/Lookup.hs
+++ b/src/Language/Haskell/Liquid/Bare/Lookup.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE OverloadedStrings #-}
@@ -18,7 +19,7 @@
 import HscMain
 import Name
 import PrelInfo                                 (wiredInThings)
-import PrelNames                                (fromIntegerName, smallIntegerName)
+import PrelNames                                (fromIntegerName, smallIntegerName, integerTyConName)
 import RdrName (setRdrNameSpace)
 import SrcLoc (SrcSpan, GenLocated(L))
 import TcRnDriver (tcRnLookupRdrName) 
@@ -91,6 +92,7 @@
   where
     wiredIns = [ (symbol n, n) | thing <- wiredInThings, let n = getName thing ]
     special  = [ ("GHC.Integer.smallInteger", smallIntegerName)
+               , ("GHC.Integer.Type.Integer", integerTyConName)
                , ("GHC.Num.fromInteger"     , fromIntegerName ) ]
 
 symbolLookupEnv env mod s
@@ -141,10 +143,15 @@
   where
     sx                 = symbol s
 
-
-lookupGhcDataCon dc  = case isTupleDC $ val dc of
-                         Just n  -> return $ tupleCon BoxedTuple n
-                         Nothing -> lookupGhcDataCon' dc 
+lookupGhcDataCon dc
+ | Just n <- isTupleDC (val dc)
+ = return $ tupleCon BoxedTuple n
+ | val dc == "[]"
+ = return nilDataCon
+ | val dc == ":"
+ = return consDataCon
+ | otherwise
+ = lookupGhcDataCon' dc
 
 isTupleDC zs
   | "(," `isPrefixOfSym` zs
diff --git a/src/Language/Haskell/Liquid/Bare/Measure.hs b/src/Language/Haskell/Liquid/Bare/Measure.hs
--- a/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/src/Language/Haskell/Liquid/Bare/Measure.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TupleSections #-}
 
diff --git a/src/Language/Haskell/Liquid/Bare/Misc.hs b/src/Language/Haskell/Liquid/Bare/Misc.hs
--- a/src/Language/Haskell/Liquid/Bare/Misc.hs
+++ b/src/Language/Haskell/Liquid/Bare/Misc.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts         #-}
 module Language.Haskell.Liquid.Bare.Misc (
     makeSymbols
 
diff --git a/src/Language/Haskell/Liquid/Bare/OfType.hs b/src/Language/Haskell/Liquid/Bare/OfType.hs
--- a/src/Language/Haskell/Liquid/Bare/OfType.hs
+++ b/src/Language/Haskell/Liquid/Bare/OfType.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE TupleSections #-}
 
 module Language.Haskell.Liquid.Bare.OfType (
@@ -13,7 +14,7 @@
 
 import BasicTypes
 import Name
-import TyCon
+import TyCon hiding (synTyConRhs_maybe)
 import Type (expandTypeSynonyms)
 import TysWiredIn
 
@@ -32,7 +33,7 @@
 import Language.Fixpoint.Misc (errorstar)
 import Language.Fixpoint.Types (Expr(..), Reftable, Symbol, meet, mkSubst, subst, symbol)
 
-import Language.Haskell.Liquid.GhcMisc (realTcArity, sourcePosSrcSpan, tyConTyVarsDef)
+import Language.Haskell.Liquid.GhcMisc 
 import Language.Haskell.Liquid.Misc (secondM)
 import Language.Haskell.Liquid.RefType
 import Language.Haskell.Liquid.Types
@@ -219,7 +220,7 @@
 
 --------------------------------------------------------------------------------
 
-bareTCApp r (Loc l _ c) rs ts | Just (SynonymTyCon rhs) <- synTyConRhs_maybe c
+bareTCApp r (Loc l _ c) rs ts | Just rhs <- synTyConRhs_maybe c
   = do when (realTcArity c < length ts) (Ex.throw err)
        return $ tyApp (subsTyVars_meet su $ ofType rhs) (drop nts ts) rs r
     where
diff --git a/src/Language/Haskell/Liquid/Bare/RefToLogic.hs b/src/Language/Haskell/Liquid/Bare/RefToLogic.hs
--- a/src/Language/Haskell/Liquid/Bare/RefToLogic.hs
+++ b/src/Language/Haskell/Liquid/Bare/RefToLogic.hs
@@ -51,7 +51,7 @@
 instance Transformable Reft where
   tx s m (Reft (v, Refa p)) = if v == s
                               then errorstar "Transformable: this should not happen"
-			      else Reft(v, Refa $ tx s m p)
+                              else Reft(v, Refa $ tx s m p)
 
 -- OLD instance Transformable Refa where
 -- OLD   tx s m (RConc p)     = RConc $ tx s m p
@@ -100,7 +100,7 @@
   tx s m x = x{eqns = tx s m <$> (eqns x)}
 
 instance Transformable (Def t c) where
-	tx s m x = x{body = tx s m (body x)} 
+        tx s m x = x{body = tx s m (body x)}
 
 instance Transformable Body where
   tx s m (E e)   = E $ tx s m e
diff --git a/src/Language/Haskell/Liquid/Bare/Resolve.hs b/src/Language/Haskell/Liquid/Bare/Resolve.hs
--- a/src/Language/Haskell/Liquid/Bare/Resolve.hs
+++ b/src/Language/Haskell/Liquid/Bare/Resolve.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeSynonymInstances #-}
diff --git a/src/Language/Haskell/Liquid/Bare/Spec.hs b/src/Language/Haskell/Liquid/Bare/Spec.hs
--- a/src/Language/Haskell/Liquid/Bare/Spec.hs
+++ b/src/Language/Haskell/Liquid/Bare/Spec.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ParallelListComp #-}
 {-# LANGUAGE TupleSections #-}
diff --git a/src/Language/Haskell/Liquid/Bounds.hs b/src/Language/Haskell/Liquid/Bounds.hs
--- a/src/Language/Haskell/Liquid/Bounds.hs
+++ b/src/Language/Haskell/Liquid/Bounds.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TupleSections #-}
 
 module Language.Haskell.Liquid.Bounds (
@@ -11,7 +12,7 @@
     makeBound,
     envToSub
 
-	) where
+        ) where
 
 import Text.PrettyPrint.HughesPJ
 
@@ -47,27 +48,27 @@
 
 
 instance Hashable (Bound t e) where
-	hashWithSalt i = hashWithSalt i . bname
+        hashWithSalt i = hashWithSalt i . bname
 
 instance Eq (Bound t e) where
   b1 == b2 = (bname b1) == (bname b2)
 
 instance (PPrint e, PPrint t) => (Show (Bound t e)) where
-	show = showpp
+        show = showpp
 
 
 instance (PPrint e, PPrint t) => (PPrint (Bound t e)) where
-	pprint (Bound s vs ps xs e) =   text "bound" <+> pprint s <+>
-	                                text "forall" <+> pprint vs <+> text "." <+>
-	                                pprint (fst <$> ps) <+> text "=" <+>
-	                                pprint_bsyms (fst <$> xs) <+> pprint e
+        pprint (Bound s vs ps xs e) =   text "bound" <+> pprint s <+>
+                                        text "forall" <+> pprint vs <+> text "." <+>
+                                        pprint (fst <$> ps) <+> text "=" <+>
+                                        pprint_bsyms (fst <$> xs) <+> pprint e
 
 pprint_bsyms [] = text ""
 pprint_bsyms xs = text "\\" <+> pprint xs <+> text "->"
 
 instance Bifunctor Bound where
-	first  f (Bound s vs ps xs e) = Bound s (f <$> vs) (mapSnd f <$> ps) (mapSnd f <$> xs) e
-	second f (Bound s vs ps xs e) = Bound s vs ps xs (f e)
+        first  f (Bound s vs ps xs e) = Bound s (f <$> vs) (mapSnd f <$> ps) (mapSnd f <$> xs) e
+        second f (Bound s vs ps xs e) = Bound s vs ps xs (f e)
 
 
 makeBound :: (PPrint r, UReftable r)
@@ -101,9 +102,9 @@
     go ((x, t):xtss) = (val x, mkt t x):(go xtss)
 
     mkt t x = ofRSort t `strengthen` ofUReft (U (Reft (val x, mempty))
-    	                                        (Pr $ M.lookupDefault [] (val x) ps) mempty)
+                                                (Pr $ M.lookupDefault [] (val x) ps) mempty)
     tp t x  = ofRSort t `strengthen` ofUReft (U (Reft (val x, refa rs))
-    	                                        (Pr $ M.lookupDefault [] (val x) ps) mempty)
+                                                (Pr $ M.lookupDefault [] (val x) ps) mempty)
     tq t x  = ofRSort t `strengthen` makeRef penv x q
 
     (ps, rs) = partitionPs penv qs
diff --git a/src/Language/Haskell/Liquid/CmdLine.hs b/src/Language/Haskell/Liquid/CmdLine.hs
--- a/src/Language/Haskell/Liquid/CmdLine.hs
+++ b/src/Language/Haskell/Liquid/CmdLine.hs
@@ -49,6 +49,7 @@
 import Language.Fixpoint.Names             (dropModuleNames)
 import Language.Fixpoint.Types
 import Language.Haskell.Liquid.Annotate
+import Language.Haskell.Liquid.GhcMisc
 import Language.Haskell.Liquid.Misc
 import Language.Haskell.Liquid.PrettyPrint
 import Language.Haskell.Liquid.Types       hiding (config, name, typ)
@@ -221,7 +222,7 @@
        -- idirs' <- if null (idirs cfg) then single <$> getIncludeDir else return (idirs cfg)
        id0 <- getIncludeDir
        return  $ cfg { files = files' }
-                     { idirs = (dropFileName <$> files') ++ [id0] ++ idirs cfg }
+                     { idirs = (dropFileName <$> files') ++ [id0 </> gHC_VERSION, id0] ++ idirs cfg }
                               -- tests fail if you flip order of idirs'
 
 ---------------------------------------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/Constraint/Constraint.hs b/src/Language/Haskell/Liquid/Constraint/Constraint.hs
--- a/src/Language/Haskell/Liquid/Constraint/Constraint.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Constraint.hs
@@ -13,8 +13,8 @@
 import Language.Fixpoint.Types
 
 instance Monoid LConstraint where
-	mempty  = LC []
-	mappend (LC cs1) (LC cs2) = LC (cs1 ++ cs2)
+        mempty  = LC []
+        mappend (LC cs1) (LC cs2) = LC (cs1 ++ cs2)
 
 typeToConstraint t = LC [t]
 
@@ -36,9 +36,9 @@
 
 subConstraintToLogicOne xts (x', (x, t)) = PImp (pAnd rs) r
   where
-  	(rs , su) = foldl go ([], []) xts
-  	([r], _ ) = go ([], su) (x', (x, t))
-  	go (acc, su) (x', (x, t)) = let (Reft(v, Refa p)) = toReft (fromMaybe mempty (stripRTypeBase t))
+        (rs , su) = foldl go ([], []) xts
+        ([r], _ ) = go ([], su) (x', (x, t))
+        go (acc, su) (x', (x, t)) = let (Reft(v, Refa p)) = toReft (fromMaybe mempty (stripRTypeBase t))
                                         su'               = (x', EVar x):(v, EVar x) : su
                                     in
                                      (subst (mkSubst su') p : acc, su')
diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs
--- a/src/Language/Haskell/Liquid/Constraint/Generate.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE ScopedTypeVariables       #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE TypeSynonymInstances      #-}
+{-# LANGUAGE FlexibleContexts          #-}
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE TupleSections             #-}
 {-# LANGUAGE DeriveDataTypeable        #-}
@@ -23,10 +24,14 @@
   ) where
 
 import CoreUtils     (exprType)
-
+import MkCore
+import Coercion
+import DataCon
+import Pair
 import CoreSyn
 import SrcLoc
 import Type
+import TyCon
 import PrelNames
 import TypeRep
 import Class            (Class, className)
@@ -526,7 +531,7 @@
   = bsplitC γ t1 t2
 
 splitC (SubC _ t1 t2)
-  = errorstar $ "(Another Broken Test!!!) splitc unexpected: " ++ showpp t1 ++ "\n\n" ++ showpp t2
+  = errorstar $ "(Another Broken Test!!!) splitc unexpected:\n" ++ showpp t1 ++ "\n\n" ++ showpp t2
 
 splitC (SubR γ o r)
   = do fg     <- pruneRefs <$> get
@@ -728,7 +733,7 @@
 γ ?= x = fromMaybe err $ lookupREnv x (renv γ)
          where err = errorstar $ "EnvLookup: unknown "
                                ++ showpp x
-                               ++ " in renv "
+                               ++ " in renv\n"
                                ++ showpp (renv γ)
 
 normalize idx
@@ -1317,6 +1322,17 @@
 cconsE γ (Tick tt e) t
   = cconsE (γ `setLoc` tickSrcSpan tt) e t
 
+-- GHC 7.10 encodes type classes with a single method as newtypes and
+-- `cast`s between the method and class type instead of applying the
+-- class constructor. Just rewrite the core to what we're used to
+-- seeing..
+cconsE γ (Cast e co) t
+  | Pair _t1 t2 <- coercionKind co
+  , isClassPred t2
+  , (tc,ts) <- splitTyConApp t2
+  , [dc]   <- tyConDataCons tc
+  = cconsE γ (mkCoreConApps dc $ map Type ts ++ [e]) t
+
 cconsE γ e@(Cast e' _) t
   = do t' <- castTy γ (exprType e) e'
        addC (SubC γ t' t) ("cconsE Cast" ++ showPpr e)
@@ -1462,6 +1478,17 @@
        return t
     where l = tickSrcSpan tt
 
+-- GHC 7.10 encodes type classes with a single method as newtypes and
+-- `cast`s between the method and class type instead of applying the
+-- class constructor. Just rewrite the core to what we're used to
+-- seeing..
+consE γ (Cast e co)
+  | Pair _t1 t2 <- coercionKind co
+  , isClassPred t2
+  , (tc,ts) <- splitTyConApp t2
+  , [dc]   <- tyConDataCons tc
+  = consE γ (mkCoreConApps dc $ map Type ts ++ [e])
+
 consE γ e@(Cast e' _)
   = castTy γ (exprType e) e'
 
@@ -1469,16 +1496,22 @@
    = trueTy $ exprType e
 
 consE _ e@(Type t)
-  = errorstar $ "consE cannot handle type" ++ showPpr (e, t)
+  = errorstar $ "consE cannot handle type " ++ showPpr (e, t)
 
 castTy _ τ (Var x)
   = do t <- trueTy τ
        return $  t `strengthen` (uTop $ F.uexprReft $ F.expr x)
 
-castTy γ τ e
-  = do t <- trueTy (exprType e)
-       cconsE γ e t
-       trueTy τ
+castTy g t (Tick _ e)
+  = castTy g t e
+
+castTy _ _ e
+  = errorstar $ "castTy cannot handle expr " ++ showPpr e
+
+-- castTy γ τ e
+--   = do t <- trueTy (exprType e)
+--        cconsE γ e t
+--        trueTy τ
 
 singletonReft = uTop . F.symbolReft . F.symbol
 
diff --git a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs
--- a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs
+++ b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs
@@ -1,8 +1,8 @@
 module Language.Haskell.Liquid.Constraint.ToFixpoint (
 
-	cgInfoFInfo
+        cgInfoFInfo
 
-	) where
+        ) where
 
 import qualified Language.Fixpoint.Types        as F
 import Language.Haskell.Liquid.Constraint.Types
diff --git a/src/Language/Haskell/Liquid/Constraint/Types.hs b/src/Language/Haskell/Liquid/Constraint/Types.hs
--- a/src/Language/Haskell/Liquid/Constraint/Types.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Types.hs
@@ -255,6 +255,7 @@
 insertFEnv (FE benv env) ((x, t), i)
   = FE (F.insertsIBindEnv [i] benv) (F.insertSEnv x t env)
 
+insertsFEnv :: FEnv -> [((F.Symbol, F.Sort), F.BindId)] -> FEnv
 insertsFEnv = L.foldl' insertFEnv
 
 initFEnv init = FE F.emptyIBindEnv $ F.fromListSEnv (wiredSortedSyms ++ init)
diff --git a/src/Language/Haskell/Liquid/Desugar/DsExpr.lhs b/src/Language/Haskell/Liquid/Desugar/DsExpr.lhs
--- a/src/Language/Haskell/Liquid/Desugar/DsExpr.lhs
+++ b/src/Language/Haskell/Liquid/Desugar/DsExpr.lhs
@@ -8,8 +8,6 @@
 \begin{code}
 module Language.Haskell.Liquid.Desugar.DsExpr ( dsExpr, dsLExpr, dsLocalBinds, dsValBinds, dsLit ) where
 
-import Language.Haskell.Liquid.GhcMisc (srcSpanTick)
-
 import Language.Haskell.Liquid.Desugar.Match
 import Language.Haskell.Liquid.Desugar.MatchLit
 import Language.Haskell.Liquid.Desugar.DsBinds
@@ -54,6 +52,11 @@
 import FastString
 
 import Control.Monad
+
+srcSpanTick :: Module -> SrcSpan -> Tickish a
+srcSpanTick m loc
+  = ProfNote (AllCafsCC m loc) False True
+
 \end{code}
 
 
diff --git a/src/Language/Haskell/Liquid/Dictionaries.hs b/src/Language/Haskell/Liquid/Dictionaries.hs
--- a/src/Language/Haskell/Liquid/Dictionaries.hs
+++ b/src/Language/Haskell/Liquid/Dictionaries.hs
@@ -17,7 +17,7 @@
 
 import Language.Fixpoint.Names      (dropModuleNames)
 import Language.Fixpoint.Types
-import Language.Fixpoint.Misc 
+import Language.Fixpoint.Misc
 
 import Language.Haskell.Liquid.GhcMisc ()
 import Language.Haskell.Liquid.Types
@@ -34,8 +34,8 @@
 
 makeDictionaryName :: Located Symbol -> SpecType -> Symbol
 makeDictionaryName t (RApp c _ _ _) = symbol ("$f" ++ (symbolString $ val t) ++ c')
-  where 
-  	c' = symbolString (dropModuleNames $ symbol $ rtc_tc c)
+  where
+        c' = symbolString (dropModuleNames $ symbol $ rtc_tc c)
 
 makeDictionaryName _ _              = errorstar "makeDictionaryName: called with invalid type"
 
@@ -63,4 +63,3 @@
 dhasinfo (Just xts) x = M.lookup x' xts
   where
      x' = (dropModuleNames $ symbol $ show x)
-
diff --git a/src/Language/Haskell/Liquid/DiffCheck.hs b/src/Language/Haskell/Liquid/DiffCheck.hs
--- a/src/Language/Haskell/Liquid/DiffCheck.hs
+++ b/src/Language/Haskell/Liquid/DiffCheck.hs
@@ -3,8 +3,9 @@
 --   modified since it was last checked, as determined by a diff against
 --   a saved version of the file.
 
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings         #-}
+{-# LANGUAGE FlexibleContexts          #-}
+{-# LANGUAGE FlexibleInstances         #-}
 
 module Language.Haskell.Liquid.DiffCheck (
 
@@ -32,7 +33,7 @@
 import            Data.Maybe                    (listToMaybe, mapMaybe, fromMaybe)
 import            Data.Hashable
 import qualified  Data.IntervalMap.FingerTree as IM
-import            CoreSyn
+import            CoreSyn                       hiding (sourceName)
 import            Name
 import            SrcLoc hiding (Located)
 import            Var
@@ -456,4 +457,3 @@
 
 lineE :: Located a -> Int
 lineE = sourceLine . locE
-
diff --git a/src/Language/Haskell/Liquid/GhcInterface.hs b/src/Language/Haskell/Liquid/GhcInterface.hs
--- a/src/Language/Haskell/Liquid/GhcInterface.hs
+++ b/src/Language/Haskell/Liquid/GhcInterface.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE TypeSynonymInstances      #-}
 {-# LANGUAGE FlexibleInstances         #-}
@@ -14,17 +15,17 @@
 import InstEnv
 import Bag (bagToList)
 import ErrUtils
-import GHC hiding (Target)
+import GHC hiding (Target, desugarModule)
 import DriverPhases (Phase(..))
 import DriverPipeline (compileFile)
 import Text.PrettyPrint.HughesPJ
 import HscTypes hiding (Target)
 import CoreSyn
 
+import Class
 import Var
 import CoreMonad    (liftIO)
 import DataCon
-import Language.Haskell.Liquid.Desugar.HscMain (hscDesugarWithLoc)
 import qualified Control.Exception as Ex
 
 import GHC.Paths (libdir)
@@ -97,11 +98,11 @@
                             | tc <- mgi_tcs modguts
                             , dc <- tyConDataCons tc
                             ]
-      let impVs           = importVars  coreBinds
+      let impVs           = importVars  coreBinds ++ classCons (mgi_cls_inst modguts)
       let defVs           = definedVars coreBinds
       let useVs           = readVars    coreBinds
       let letVs           = letVars     coreBinds
-      let derVs           = derivedVars coreBinds $ mgi_is_dfun modguts
+      let derVs           = derivedVars coreBinds $ fmap (fmap is_dfun) $ mgi_cls_inst modguts
       logicmap           <- liftIO makeLogicMap
       (spec, imps, incs) <- moduleSpec cfg coreBinds (impVs ++ defVs) letVs name' modguts tgtSpec logicmap impSpecs'
       liftIO              $ whenLoud $ putStrLn $ "Module Imports: " ++ show imps
@@ -114,6 +115,10 @@
        lspec <- readFile lg
        return $ parseSymbolToLogic lg lspec
 
+classCons :: Maybe [ClsInst] -> [Id]
+classCons Nothing   = []
+classCons (Just cs) = concatMap (dataConImplicitIds . head . tyConDataCons . classTyCon . is_cls) cs
+
 derivedVars :: CoreProgram -> Maybe [DFunId] -> [Id]
 derivedVars cbs (Just fds) = concatMap (derivedVs cbs) fds
 derivedVars _    Nothing    = []
@@ -153,6 +158,9 @@
                   --     `gopt_set` Opt_Hpc
                       `gopt_set` Opt_ImplicitImportQualified
                       `gopt_set` Opt_PIC
+#if __GLASGOW_HASKELL__ >= 710
+                      `gopt_set` Opt_Debug
+#endif
        (df'',_,_) <- parseDynamicFlags df' (map noLoc $ ghcOptions cfg)
        setSessionDynFlags $ df'' -- {profAuto = ProfAutoAll}
 
@@ -187,12 +195,12 @@
      Just modSummary -> do
        -- mod_guts <- modSummaryModGuts modSummary
        mod_p    <- parseModule modSummary
-       mod_guts <- coreModule <$> (desugarModuleWithLoc =<< typecheckModule (ignoreInline mod_p))
-       let deriv = getDerivedDictionaries mod_guts
+       mod_guts <- coreModule <$> (desugarModule =<< typecheckModule (ignoreInline mod_p))
+       let deriv = getDerivedDictionaries mod_guts 
        return   $! (miModGuts (Just deriv) mod_guts)
      Nothing     -> exitWithPanic "Ghc Interface: Unable to get GhcModGuts"
 
-getDerivedDictionaries cm = is_dfun <$> (instEnvElts $ mg_inst_env cm)
+getDerivedDictionaries cm = instEnvElts $ mg_inst_env cm
 
 cleanFiles :: FilePath -> IO ()
 cleanFiles fn
@@ -209,15 +217,6 @@
 -- | Desugaring (Taken from GHC, modified to hold onto Loc in Ticks) -----------
 --------------------------------------------------------------------------------
 
-desugarModuleWithLoc :: TypecheckedModule -> Ghc DesugaredModule
-desugarModuleWithLoc tcm = do
-  let ms = pm_mod_summary $ tm_parsed_module tcm
-  -- let ms = modSummary tcm
-  let (tcg, _) = tm_internals_ tcm
-  hsc_env <- getSession
-  let hsc_env_tmp = hsc_env { hsc_dflags = ms_hspp_opts ms }
-  guts <- liftIO $ hscDesugarWithLoc hsc_env_tmp ms tcg
-  return $ DesugaredModule { dm_typechecked_module = tcm, dm_core_module = guts }
 
 --------------------------------------------------------------------------------
 -- | Extracting Qualifiers -----------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/GhcMisc.hs b/src/Language/Haskell/Liquid/GhcMisc.hs
--- a/src/Language/Haskell/Liquid/GhcMisc.hs
+++ b/src/Language/Haskell/Liquid/GhcMisc.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                       #-}
 {-# LANGUAGE OverloadedStrings         #-}
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE GADTs                     #-}
@@ -20,7 +21,7 @@
 
 import           Avail                        (availsToNameSet)
 import           BasicTypes                   (Arity)
-import           CoreSyn                      hiding (Expr)
+import           CoreSyn                      hiding (Expr, sourceName)
 import qualified CoreSyn as Core
 import           CostCentre
 import           GHC                          hiding (L)
@@ -28,6 +29,10 @@
 import           Kind                         (superKind)
 import           NameSet                      (NameSet)
 import           SrcLoc                       (mkRealSrcLoc, mkRealSrcSpan, srcSpanFileName_maybe)
+import           Bag
+import           ErrUtils
+import           CoreLint
+import           CoreMonad
 
 import           Language.Fixpoint.Names      (dropModuleNames)
 import           Text.Parsec.Pos              (sourceName, sourceLine, sourceColumn, SourcePos, newPos)
@@ -41,6 +46,7 @@
 import           HscTypes                     (HscEnv(..), FindResult(..))
 import           FastString
 import           TcRnDriver
+import           TcRnTypes
 
 import           RdrName
 import           Type                         (liftedTypeKind)
@@ -69,6 +75,14 @@
 
 import Language.Fixpoint.Names      (symSepName, isSuffixOfSym, singletonSym)
 
+
+#if __GLASGOW_HASKELL__ < 710
+import Language.Haskell.Liquid.Desugar.HscMain
+#else
+import qualified HscMain as GHC
+#endif
+
+
 -----------------------------------------------------------------------
 --------------- Datatype For Holding GHC ModGuts ----------------------
 -----------------------------------------------------------------------
@@ -82,10 +96,10 @@
   , mgi_tcs       :: ![TyCon]
   , mgi_fam_insts :: ![FamInst]
   , mgi_exports   :: !NameSet
-  , mgi_is_dfun   :: !(Maybe [DFunId])
+  , mgi_cls_inst  :: !(Maybe [ClsInst])
   }
 
-miModGuts dids mg = MI {
+miModGuts cls mg  = MI {
     mgi_binds     = mg_binds mg
   , mgi_module    = mg_module mg
   , mgi_deps      = mg_deps mg
@@ -94,7 +108,7 @@
   , mgi_tcs       = mg_tcs mg
   , mgi_fam_insts = mg_fam_insts mg
   , mgi_exports   = availsToNameSet $ mg_exports mg
-  , mgi_is_dfun   = dids
+  , mgi_cls_inst  = cls
   }
 
 -----------------------------------------------------------------------
@@ -107,7 +121,11 @@
 
 tickSrcSpan ::  Outputable a => Tickish a -> SrcSpan
 tickSrcSpan (ProfNote cc _ _) = cc_loc cc
+#if __GLASGOW_HASKELL__ >= 710
+tickSrcSpan (SourceNote ss _) = RealSrcSpan ss
+#endif
 tickSrcSpan _                 = noSrcSpan
+
 -----------------------------------------------------------------------
 --------------- Generic Helpers for Accessing GHC Innards -------------
 -----------------------------------------------------------------------
@@ -238,10 +256,13 @@
 pprDoc    = sDocDoc . ppr
 
 -- Overriding Outputable functions because they now require DynFlags!
-showPpr      = Out.showPpr unsafeGlobalDynFlags
-showSDoc     = Out.showSDoc unsafeGlobalDynFlags
-showSDocDump = Out.showSDocDump unsafeGlobalDynFlags
+showPpr       = showSDoc . ppr
 
+-- FIXME: somewhere we depend on this printing out all GHC entities with
+-- fully-qualified names...
+showSDoc sdoc = Out.renderWithStyle unsafeGlobalDynFlags sdoc (Out.mkUserStyle Out.alwaysQualify Out.AllTheWay)
+showSDocDump  = Out.showSDocDump unsafeGlobalDynFlags
+
 typeUniqueString = {- ("sort_" ++) . -} showSDocDump . ppr
 
 instance Fixpoint Var where
@@ -425,10 +446,60 @@
   symbol = symbol . fastStringText
 
 fastStringText = T.decodeUtf8 . fastStringToByteString
-symbolFastString = T.unsafeDupablePerformIO . mkFastStringByteString . T.encodeUtf8 . symbolText
 
-
 tyConTyVarsDef c | TC.isPrimTyCon c || isFunTyCon c = []
 tyConTyVarsDef c | TC.isPromotedTyCon   c = error ("TyVars on " ++ show c) -- tyConTyVarsDef $ TC.ty_con c
 tyConTyVarsDef c | TC.isPromotedDataCon c = error ("TyVars on " ++ show c) -- DC.dataConUnivTyVars $ TC.datacon c
-tyConTyVarsDef c = TC.tyConTyVars c
+tyConTyVarsDef c = TC.tyConTyVars c 
+
+
+
+----------------------------------------------------------------------
+-- GHC Compatibility Layer
+----------------------------------------------------------------------
+
+gHC_VERSION :: String
+gHC_VERSION = show __GLASGOW_HASKELL__
+
+desugarModule :: TypecheckedModule -> Ghc DesugaredModule
+
+symbolFastString :: Symbol -> FastString
+
+lintCoreBindings :: [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
+
+synTyConRhs_maybe :: TyCon -> Maybe Type
+
+#if __GLASGOW_HASKELL__ < 710
+
+desugarModule tcm = do
+  let ms = pm_mod_summary $ tm_parsed_module tcm 
+  -- let ms = modSummary tcm
+  let (tcg, _) = tm_internals_ tcm
+  hsc_env <- getSession
+  let hsc_env_tmp = hsc_env { hsc_dflags = ms_hspp_opts ms }
+  guts <- liftIO $ hscDesugarWithLoc hsc_env_tmp ms tcg
+  return $ DesugaredModule { dm_typechecked_module = tcm, dm_core_module = guts }
+
+
+symbolFastString = T.unsafeDupablePerformIO . mkFastStringByteString . T.encodeUtf8 . symbolText
+
+lintCoreBindings = CoreLint.lintCoreBindings
+
+synTyConRhs_maybe t
+  | Just (TC.SynonymTyCon rhs) <- TC.synTyConRhs_maybe t
+  = Just rhs
+synTyConRhs_maybe _                     = Nothing
+
+#else
+
+desugarModule = GHC.desugarModule
+
+symbolFastString = mkFastStringByteString . T.encodeUtf8 . symbolText
+
+type Prec = TyPrec
+
+lintCoreBindings = CoreLint.lintCoreBindings CoreDoNothing
+
+synTyConRhs_maybe = TC.synTyConRhs_maybe
+
+#endif
diff --git a/src/Language/Haskell/Liquid/GhcPlay.hs b/src/Language/Haskell/Liquid/GhcPlay.hs
--- a/src/Language/Haskell/Liquid/GhcPlay.hs
+++ b/src/Language/Haskell/Liquid/GhcPlay.hs
@@ -5,7 +5,7 @@
 
 module Language.Haskell.Liquid.GhcPlay where
 
-import GHC		
+import GHC
 import CoreSyn
 import Var
 import TypeRep
@@ -38,7 +38,7 @@
   subTy s (App e1 e2)  = App (subTy s e1) (subTy s e2)
   subTy s (Lam b e)    | isTyVar b = Lam v' (subTy s e)
    where v' = case M.lookup b s of
-               Just (TyVarTy v) -> v      
+               Just (TyVarTy v) -> v
                _                -> b
 
   subTy s (Lam b e)      = Lam (subTy s b) (subTy s e)
@@ -58,7 +58,7 @@
  subTy s (a, b, e) = (a, map (subTy s) b, subTy s e)
 
 instance Subable Var where
- sub s v   | M.member v s = subVar $ s M.! v 
+ sub s v   | M.member v s = subVar $ s M.! v
            | otherwise    = v
  subTy s v = setVarType v (subTy s (varType v))
 
diff --git a/src/Language/Haskell/Liquid/Literals.hs b/src/Language/Haskell/Liquid/Literals.hs
--- a/src/Language/Haskell/Liquid/Literals.hs
+++ b/src/Language/Haskell/Liquid/Literals.hs
@@ -1,6 +1,6 @@
 module Language.Haskell.Liquid.Literals (
-	literalFRefType, literalFReft, literalConst
-	) where 
+        literalFRefType, literalFReft, literalConst
+        ) where
 
 import TypeRep
 import Literal 
@@ -18,24 +18,23 @@
 ----------------------- Typing Literals -----------------------
 ---------------------------------------------------------------
 
-makeRTypeBase (TyVarTy α)    x       
-  = RVar (rTyVar α) x 
-makeRTypeBase (TyConApp c ts) x 
+makeRTypeBase (TyVarTy α)    x
+  = RVar (rTyVar α) x
+makeRTypeBase (TyConApp c ts) x
   = rApp c ((`makeRTypeBase` mempty) <$> ts) [] x
 makeRTypeBase _              _
   = error "RefType : makeRTypeBase"
 
-literalFRefType tce l 
-  = makeRTypeBase (literalType l) (literalFReft tce l) 
+literalFRefType tce l
+  = makeRTypeBase (literalType l) (literalFReft tce l)
 
 literalFReft tce = maybe mempty exprReft . snd . literalConst tce
 
 
 -- | `literalConst` returns `Nothing` for unhandled lits because
---    otherwise string-literals show up as global int-constants 
---    which blow up qualifier instantiation. 
+--    otherwise string-literals show up as global int-constants
+--    which blow up qualifier instantiation.
 
 literalConst tce l         = (sort, mkLit l)
-  where 
-    sort                   = typeSort tce $ literalType l 
-
+  where
+    sort                   = typeSort tce $ literalType l
diff --git a/src/Language/Haskell/Liquid/Misc.hs b/src/Language/Haskell/Liquid/Misc.hs
--- a/src/Language/Haskell/Liquid/Misc.hs
+++ b/src/Language/Haskell/Liquid/Misc.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                       #-}
 {-# LANGUAGE TupleSections             #-}
 
 module Language.Haskell.Liquid.Misc where
@@ -64,9 +65,15 @@
 zip4 (x1:xs1) (x2:xs2) (x3:xs3) (x4:xs4) = (x1, x2, x3, x4) : (zip4 xs1 xs2 xs3 xs4) 
 zip4 _ _ _ _                             = []
 
-getIncludeDir      = dropFileName <$> (getDataFileName $ "include" </> "Prelude.spec")
+#if __GLASGOW_HASKELL__ < 710
+ghc = "ghc-7.8"
+#else
+ghc = "ghc-7.10"
+#endif
+
+getIncludeDir      = dropFileName <$> getDataFileName ("include" </> "Prelude.spec")
 getCssPath         = getDataFileName $ "syntax" </> "liquid.css"
-getCoreToLogicPath = getDataFileName $ "include" </> "CoreToLogic.lg"
+getCoreToLogicPath = fmap (</> "CoreToLogic.lg") getIncludeDir
 
 
 maximumWithDefault zero [] = zero
diff --git a/src/Language/Haskell/Liquid/Parse.hs b/src/Language/Haskell/Liquid/Parse.hs
--- a/src/Language/Haskell/Liquid/Parse.hs
+++ b/src/Language/Haskell/Liquid/Parse.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE FlexibleContexts          #-}
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE UndecidableInstances      #-}
 {-# LANGUAGE TypeSynonymInstances      #-}
@@ -755,7 +756,7 @@
   where
     idP p  = many1 (satisfy (not . p))
     badc c = (c == ':') || (c == ',') || bad c
-    bad c  = isSpace c || c `elem` "(,)"
+    bad c  = isSpace c || c `elem` ("(,)" :: String)
     pwr s  = symbol $ "(" `mappend` s `mappend` ")"
 
 grabs p = try (liftM2 (:) p (grabs p))
@@ -821,7 +822,7 @@
  <|> pwr <$> parens (idP bad)
   where
      idP p  = symbol <$> many1 (satisfy (not . p))
-     bad c  = isSpace c || c `elem` "(,)"
+     bad c  = isSpace c || c `elem` ("(,)" :: String)
      pwr s  = "(" <> s <> ")"
 
 dataSizeP
diff --git a/src/Language/Haskell/Liquid/PredType.hs b/src/Language/Haskell/Liquid/PredType.hs
--- a/src/Language/Haskell/Liquid/PredType.hs
+++ b/src/Language/Haskell/Liquid/PredType.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveDataTypeable, FlexibleInstances, UndecidableInstances, TupleSections, OverloadedStrings #-}
+{-# LANGUAGE DeriveDataTypeable, FlexibleInstances, FlexibleContexts, UndecidableInstances, TupleSections, OverloadedStrings #-}
 module Language.Haskell.Liquid.PredType (
     PrType
   , TyConP (..), DataConP (..)
diff --git a/src/Language/Haskell/Liquid/PrettyPrint.hs b/src/Language/Haskell/Liquid/PrettyPrint.hs
--- a/src/Language/Haskell/Liquid/PrettyPrint.hs
+++ b/src/Language/Haskell/Liquid/PrettyPrint.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleContexts     #-} 
+{-# LANGUAGE FlexibleContexts     #-}
 {-# LANGUAGE FlexibleInstances    #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE OverloadedStrings    #-}
@@ -7,16 +7,16 @@
 -- | Module with all the printing and serialization routines
 
 module Language.Haskell.Liquid.PrettyPrint (
-  
+
   -- * Tidy level
   Tidy (..)
- 
+
   -- * Printing RType
-  , rtypeDoc 
+  , rtypeDoc
   , ppr_rtype
 
   -- * Printing an Orderable List
-  , pprManyOrdered 
+  , pprManyOrdered
 
   -- * Printing a List with many large items
   , pprintLongList
@@ -36,7 +36,7 @@
 import Language.Fixpoint.Misc
 import Language.Haskell.Liquid.Types hiding (sort)
 import Language.Fixpoint.Names (dropModuleNames, propConName, hpropConName)
-import TypeRep          hiding (maybeParen, pprArrowChain)  
+import TypeRep          hiding (maybeParen, pprArrowChain)
 import Text.Parsec.Error (ParseError, errorMessages, showErrorMessages)
 import Var              (Var)
 import TyCon            (TyCon)
@@ -56,7 +56,7 @@
   pprint = pprDoc
 
 instance PPrint Doc where
-  pprint x = x 
+  pprint x = x
 
 instance PPrint ErrMsg where
   pprint = text . show
@@ -64,7 +64,7 @@
 instance PPrint SourceError where
   pprint = text . show
 
-instance PPrint ParseError where 
+instance PPrint ParseError where
   pprint e = vcat $ tail $ map text ls
     where
       ls = lines $ showErrorMessages "or" "unknown parse error"
@@ -75,10 +75,10 @@
 --   pprint (LPE _ msgs) = text "Parse Error: " <> vcat (map pprint msgs)
 
 instance PPrint Var where
-  pprint = pprDoc 
+  pprint = pprDoc
 
 instance PPrint Name where
-  pprint = pprDoc 
+  pprint = pprDoc
 
 instance PPrint TyCon where
   pprint = pprDoc
@@ -109,30 +109,30 @@
 -- to figure out all the constraints.
 
 rtypeDoc k    = ppr_rtype (ppE k) TopPrec
-  where 
+  where
     ppE Lossy = ppEnvShort ppEnv
     ppE Full  = ppEnv
 
-ppTyConB bb 
+ppTyConB bb
   | ppShort bb = text . symbolString . dropModuleNames . symbol . render . ppTycon
   | otherwise  = ppTycon
 
-    
-ppr_rtype bb p t@(RAllT _ _)       
+
+ppr_rtype bb p t@(RAllT _ _)
   = ppr_forall bb p t
-ppr_rtype bb p t@(RAllP _ _)       
+ppr_rtype bb p t@(RAllP _ _)
   = ppr_forall bb p t
-ppr_rtype bb p t@(RAllS _ _)       
+ppr_rtype bb p t@(RAllS _ _)
   = ppr_forall bb p t
-ppr_rtype _ _ (RVar a r)         
+ppr_rtype _ _ (RVar a r)
   = ppTy r $ pprint a
 ppr_rtype bb p t@(RFun _ _ _ _)
   = maybeParen p FunPrec $ ppr_rty_fun bb empty t
 ppr_rtype bb p (RApp c [t] rs r)
-  | isList c 
+  | isList c
   = ppTy r $ brackets (ppr_rtype bb p t) <> ppReftPs bb rs
 ppr_rtype bb p (RApp c ts rs r)
-  | isTuple c 
+  | isTuple c
   = ppTy r $ parens (intersperse comma (ppr_rtype bb p <$> ts)) <> ppReftPs bb rs
 ppr_rtype bb p (RApp c ts rs r)
   | isEmpty rsDoc && isEmpty tsDoc
@@ -143,7 +143,7 @@
     rsDoc            = ppReftPs bb rs
     tsDoc            = hsep (ppr_rtype bb p <$> ts)
     ppT              = ppTyConB bb
-    
+
 ppr_rtype bb p t@(REx _ _ _)
   = ppExists bb p t
 ppr_rtype bb p t@(RAllE _ _ _)
@@ -154,7 +154,7 @@
   = ppTy r $ ppr_rtype bb p t <+> ppr_rtype bb p t'
 ppr_rtype bb p (RRTy e _ OCons t)         
   = sep [braces (ppr_rsubtype bb p e) <+> "=>", ppr_rtype bb p t]
-ppr_rtype bb p (RRTy e r o t)         
+ppr_rtype bb p (RRTy e r o t)
   = sep [ppp (pprint o <+> ppe <+> pprint r), ppr_rtype bb p t]
   where ppe = (hsep $ punctuate comma (pprint <$> e)) <+> colon <> colon
         ppp = \doc -> text "<<" <+> doc <+> text ">>"
@@ -189,7 +189,7 @@
 maybeParen :: Prec -> Prec -> Doc -> Doc
 maybeParen ctxt_prec inner_prec pretty
   | ctxt_prec < inner_prec = pretty
-  | otherwise		       = parens pretty
+  | otherwise                  = parens pretty
 
 
 -- ppExists :: (RefTypable p c tv (), RefTypable p c tv r) => Bool -> Prec -> RType p c tv r -> Doc
@@ -197,23 +197,23 @@
   = text "exists" <+> brackets (intersperse comma [ppr_dbind bb TopPrec x t | (x, t) <- zs]) <> dot <> ppr_rtype bb p t'
     where (zs,  t')               = split [] t
           split zs (REx x t t')   = split ((x,t):zs) t'
-          split zs t	            = (reverse zs, t)
+          split zs t                = (reverse zs, t)
 
 -- ppAllExpr :: (RefTypable p c tv (), RefTypable p c tv r) => Bool -> Prec -> RType p c tv r -> Doc
 ppAllExpr bb p t
   = text "forall" <+> brackets (intersperse comma [ppr_dbind bb TopPrec x t | (x, t) <- zs]) <> dot <> ppr_rtype bb p t'
     where (zs,  t')               = split [] t
           split zs (RAllE x t t') = split ((x,t):zs) t'
-          split zs t	            = (reverse zs, t)
+          split zs t                = (reverse zs, t)
 
-ppReftPs _ rs 
+ppReftPs _ rs
   | all isTauto rs   = empty
-  | not (ppPs ppEnv) = empty 
+  | not (ppPs ppEnv) = empty
   | otherwise        = angleBrackets $ hsep $ punctuate comma $ pprint <$> rs
 
 -- ppr_dbind :: (RefTypable p c tv (), RefTypable p c tv r) => Bool -> Prec -> Symbol -> RType p c tv r -> Doc
-ppr_dbind bb p x t 
-  | isNonSymbol x || (x == dummySymbol) 
+ppr_dbind bb p x t
+  | isNonSymbol x || (x == dummySymbol)
   = ppr_rtype bb p t
   | otherwise
   = pprint x <> colon <> ppr_rtype bb p t
@@ -234,19 +234,19 @@
   where
     trep                   = toRTypeRep t
     (cls, t')              = bkClass $ fromRTypeRep $ trep {ty_vars = [], ty_preds = [], ty_labels = []}
-  
+
     ppr_foralls False _ _  _= empty
     ppr_foralls _    [] [] [] = empty
     ppr_foralls True αs πs ss = text "forall" <+> dαs αs <+> dπs (ppPs bb) πs <+> dss (ppSs bb) ss <> dot
     ppr_clss []            = empty
     ppr_clss cs            = (parens $ hsep $ punctuate comma (uncurry (ppr_cls bb p) <$> cs)) <+> text "=>"
 
-    dαs αs                 = sep $ pprint <$> αs 
-    
-    dπs _ []               = empty 
-    dπs False _            = empty 
+    dαs αs                 = sep $ pprint <$> αs
+
+    dπs _ []               = empty
+    dπs False _            = empty
     dπs True πs            = angleBrackets $ intersperse comma $ ppr_pvar_def pprint <$> πs
-    dss _ []               = empty 
+    dss _ []               = empty
     dss _ ss               = angleBrackets $ intersperse comma $ pprint <$> ss
 
 
@@ -259,16 +259,16 @@
 
 ppr_pvar_def pprv (PV s t _ xts)
   = pprint s <+> dcolon <+> intersperse arrow dargs <+> ppr_pvar_kind pprv t
-    
-  where 
+
+  where
     dargs = [pprv t | (t,_,_) <- xts]
 
-ppr_pvar_kind pprv (PVProp t) = pprv t <+> arrow <+> ppr_name propConName  
-ppr_pvar_kind _    (PVHProp)  = ppr_name hpropConName 
-ppr_name                      = text . symbolString 
-    
+ppr_pvar_kind pprv (PVProp t) = pprv t <+> arrow <+> ppr_name propConName
+ppr_pvar_kind _    (PVHProp)  = ppr_name hpropConName
+ppr_name                      = text . symbolString
+
 instance PPrint RTyVar where
-  pprint (RTV α) 
+  pprint (RTV α)
    | ppTyVar ppEnv = ppr_tyvar α
    | otherwise     = ppr_tyvar_short α
 
@@ -304,18 +304,18 @@
   pprint (AnnRDf t) = text "AnnRDf" <+> pprint t
   pprint (AnnLoc l) = text "AnnLoc" <+> pprDoc l
 
-pprAnnInfoBinds (l, xvs) 
+pprAnnInfoBinds (l, xvs)
   = vcat $ map (pprAnnInfoBind . (l,)) xvs
 
-pprAnnInfoBind (RealSrcSpan k, xv) 
+pprAnnInfoBind (RealSrcSpan k, xv)
   = xd $$ pprDoc l $$ pprDoc c $$ pprint n $$ vd $$ text "\n\n\n"
-    where 
+    where
       l        = srcSpanStartLine k
       c        = srcSpanStartCol k
-      (xd, vd) = pprXOT xv 
+      (xd, vd) = pprXOT xv
       n        = length $ lines $ render vd
 
-pprAnnInfoBind (_, _) 
+pprAnnInfoBind (_, _)
   = empty
 
 pprXOT (x, v) = (xd, pprint v)
@@ -323,14 +323,14 @@
     xd = maybe (text "unknown") pprint x
 
 instance PPrint a => PPrint (AnnInfo a) where
-  pprint (AI m) = vcat $ map pprAnnInfoBinds $ M.toList m 
+  pprint (AI m) = vcat $ map pprAnnInfoBinds $ M.toList m
 
 instance (Ord k, PPrint k, PPrint v) => PPrint (M.HashMap k v) where
   pprint = ppTable
-    
+
 ppTable m = vcat $ pprxt <$> xts
-  where 
-    pprxt (x,t) = pprint x $$ nest n (colon <+> pprint t)  
+  where
+    pprxt (x,t) = pprint x $$ nest n (colon <+> pprint t)
     n          = 1 + maximumWithDefault 0 [ i | (x, _) <- xts, let i = keySize x, i <= thresh ]
     keySize     = length . render . pprint
     xts         = sortBy (compare `on` fst) $ M.toList m
diff --git a/src/Language/Haskell/Liquid/RefSplit.hs b/src/Language/Haskell/Liquid/RefSplit.hs
--- a/src/Language/Haskell/Liquid/RefSplit.hs
+++ b/src/Language/Haskell/Liquid/RefSplit.hs
@@ -3,9 +3,9 @@
 
 module Language.Haskell.Liquid.RefSplit (
 
-	splitXRelatedRefs
+        splitXRelatedRefs
 
-	) where
+        ) where
 
 import Control.Applicative
 import Data.List (partition)
@@ -14,110 +14,110 @@
 import Language.Haskell.Liquid.Types
 import Language.Haskell.Liquid.PrettyPrint ()
 
-import Language.Fixpoint.Types 
-import Language.Fixpoint.Misc 
+import Language.Fixpoint.Types
+import Language.Fixpoint.Misc
 
 splitXRelatedRefs :: Symbol -> SpecType -> (SpecType, SpecType)
 splitXRelatedRefs x t = splitRType x t
-   
 
 
+
 splitRType f (RVar a r) = (RVar a r1, RVar a r2)
   where
-  	(r1, r2) = splitRef f r
+        (r1, r2) = splitRef f r
 
-splitRType f (RFun x tx t r) = (RFun x tx1 t1 r1, RFun x tx2 t2 r2) 
+splitRType f (RFun x tx t r) = (RFun x tx1 t1 r1, RFun x tx2 t2 r2)
   where
-  	(tx1, tx2) = splitRType f tx
-  	(t1,  t2)  = splitRType f t
-  	(r1,  r2)  = splitRef   f r
+        (tx1, tx2) = splitRType f tx
+        (t1,  t2)  = splitRType f t
+        (r1,  r2)  = splitRef   f r
 
 splitRType f (RAllT v t) = (RAllT v t1, RAllT v t2)
   where
-  	(t1, t2) = splitRType f t 
+        (t1, t2) = splitRType f t
 
 splitRType f (RAllP p t) = (RAllP p t1, RAllP p t2)
   where
-  	(t1, t2) = splitRType f t
+        (t1, t2) = splitRType f t
 
 splitRType f (RAllS s t) = (RAllS s t1, RAllS s t2)
   where
-  	(t1, t2) = splitRType f t
+        (t1, t2) = splitRType f t
 
 
 splitRType f (RApp c ts rs r) = (RApp c ts1 rs1 r1, RApp c ts2 rs2 r2)
   where
-  	(ts1, ts2) = unzip (splitRType f <$> ts)
-  	(rs1, rs2) = unzip (splitUReft f <$> rs)
-  	(r1,  r2)  = splitRef f r 
+        (ts1, ts2) = unzip (splitRType f <$> ts)
+        (rs1, rs2) = unzip (splitUReft f <$> rs)
+        (r1,  r2)  = splitRef f r
 
 splitRType f (RAllE x tx t) = (RAllE x tx1 t1, RAllE x tx2 t2)
   where
-  	(tx1, tx2) = splitRType f tx
-  	(t1, t2)   = splitRType f t
+        (tx1, tx2) = splitRType f tx
+        (t1, t2)   = splitRType f t
 
 splitRType f (REx x tx t) = (REx x tx1 t1, REx x tx2 t2)
   where
-  	(tx1, tx2) = splitRType f tx
-  	(t1, t2)   = splitRType f t
+        (tx1, tx2) = splitRType f tx
+        (t1, t2)   = splitRType f t
 
 splitRType _ (RExprArg e) = (RExprArg e, RExprArg e)
 
 splitRType f (RAppTy tx t r) = (RAppTy tx1 t1 r1, RAppTy tx2 t2 r2)
   where
-  	(tx1, tx2) = splitRType f tx
-  	(t1,  t2)  = splitRType f t
-  	(r1,  r2)  = splitRef   f r
+        (tx1, tx2) = splitRType f tx
+        (t1,  t2)  = splitRType f t
+        (r1,  r2)  = splitRef   f r
 
 splitRType f (RRTy xs r o t) = (RRTy xs1 r1 o t1, RRTy xs2 r2 o t2)
   where
-  	(xs1, xs2) = unzip (go <$> xs)
-  	(r1, r2) = splitRef   f r 
-  	(t1, t2) = splitRType f t
+        (xs1, xs2) = unzip (go <$> xs)
+        (r1, r2) = splitRef   f r
+        (t1, t2) = splitRType f t
 
-  	go (x, t) = let (t1, t2) = splitRType f t in ((x,t1), (x, t2))
+        go (x, t) = let (t1, t2) = splitRType f t in ((x,t1), (x, t2))
 
 
 splitRType f (RHole r) = (RHole r1, RHole r2)
   where
-  	(r1, r2) = splitRef f r 
+        (r1, r2) = splitRef f r
 
 splitUReft :: Symbol -> RTProp c tv (UReft Reft) -> (RTProp c tv (UReft Reft), RTProp c tv (UReft Reft))
 splitUReft x (RPropP xs r) = (RPropP xs r1, RPropP xs r2)
-  where 
-  	(r1, r2) = splitRef x r
+  where
+        (r1, r2) = splitRef x r
 
 splitUReft x (RProp xs t) = (RProp xs t1, RProp xs t2)
-  where 
-  	(t1, t2) = splitRType x t
+  where
+        (t1, t2) = splitRType x t
 
 splitUReft _ (RHProp xs _) = (RHProp xs w1, RHProp xs w2)
-  where 
-  	(w1, w2) = error "TODO: RefSplit.splitUReft"
+  where
+        (w1, w2) = error "TODO: RefSplit.splitUReft"
 
 splitRef f (U r p s) = (U r1 p1 s, U r2 p2 s)
-	where
-		(r1, r2) = splitReft f r 
-		(p1, p2) = splitPred f p
+        where
+                (r1, r2) = splitReft f r
+                (p1, p2) = splitPred f p
 
 splitReft f (Reft (v, Refa xs)) = (Reft (v, Refa $ pAnd xs1), Reft (v, Refa $ pAnd xs2))
   where
     (xs1, xs2)       = partition (isFree f) (unPAnd xs)
 
-    unPAnd (PAnd ps) = concatMap unPAnd ps 
+    unPAnd (PAnd ps) = concatMap unPAnd ps
     unPAnd p         = [p]
 
 splitPred f (Pr ps) = (Pr ps1, Pr ps2)
   where
     (ps1, ps2) = partition g ps
-    g p = any (isFree f) (thd3 <$> pargs p) 	
+    g p = any (isFree f) (thd3 <$> pargs p)
 
 
 class IsFree a where
-	isFree :: Symbol -> a -> Bool
+        isFree :: Symbol -> a -> Bool
 
 instance (Subable x) => (IsFree x) where
-	isFree x p = x `elem` syms p
+        isFree x p = x `elem` syms p
 
 instance Show (UReft Reft) where
-	 show = render . pprint
+         show = render . pprint
diff --git a/src/Language/Haskell/Liquid/Simplify.hs b/src/Language/Haskell/Liquid/Simplify.hs
--- a/src/Language/Haskell/Liquid/Simplify.hs
+++ b/src/Language/Haskell/Liquid/Simplify.hs
@@ -40,4 +40,3 @@
 
 simplifyLen :: Int
 simplifyLen = 5
-
diff --git a/src/Language/Haskell/Liquid/Tidy.hs b/src/Language/Haskell/Liquid/Tidy.hs
--- a/src/Language/Haskell/Liquid/Tidy.hs
+++ b/src/Language/Haskell/Liquid/Tidy.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts  #-}
 {-# LANGUAGE OverloadedStrings #-}
 ---------------------------------------------------------------------
 -- | This module contains functions for cleaning up types before
diff --git a/src/Language/Haskell/Liquid/TransformRec.hs b/src/Language/Haskell/Liquid/TransformRec.hs
--- a/src/Language/Haskell/Liquid/TransformRec.hs
+++ b/src/Language/Haskell/Liquid/TransformRec.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveDataTypeable        #-}
+{-# LANGUAGE FlexibleContexts          #-}
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
@@ -13,15 +14,15 @@
 import           Coercion
 import           Control.Arrow       (second)
 import           Control.Monad.State
-import           CoreLint
 import           CoreSyn
+import           CoreUtils
 import qualified Data.HashMap.Strict as M
 import           ErrUtils
 import           Id                  (idOccInfo, setIdInfo)
 import           IdInfo
 import           MkCore              (mkCoreLams)
 import           SrcLoc
-import           Type                (mkForAllTys)
+import           Type                (mkForAllTys, splitForAllTys)
 import           TypeRep
 import           Unique              hiding (deriveUnique)
 import           Var
@@ -136,7 +137,7 @@
 isNonPolyRec (Let (Rec xes) _) = any nonPoly (snd <$> xes)
 isNonPolyRec _                 = False
 
-nonPoly = null . fst . collectTyBinders
+nonPoly = null . fst . splitForAllTys . exprType
 
 collectNonRecLets = go []
   where go bs (Let b@(NonRec _ _) e') = go (b:bs) e'
diff --git a/src/Language/Haskell/Liquid/Types.hs b/src/Language/Haskell/Liquid/Types.hs
--- a/src/Language/Haskell/Liquid/Types.hs
+++ b/src/Language/Haskell/Liquid/Types.hs
@@ -460,8 +460,12 @@
 ------ Strictness --------------------------------------------------
 --------------------------------------------------------------------
 
-instance NFData Var
-instance NFData SrcSpan
+instance NFData Var where
+  rnf x = seq x ()
+
+instance NFData SrcSpan where
+  rnf x = seq x ()
+
 --------------------------------------------------------------------
 ------------------ Predicates --------------------------------------
 --------------------------------------------------------------------
@@ -1566,10 +1570,11 @@
 
 data Cinfo    = Ci { ci_loc :: !SrcSpan
                    , ci_err :: !(Maybe Error)
-                   }
-                deriving (Eq, Ord)
+                   } 
+                deriving (Eq, Ord, Generic) 
 
-instance NFData Cinfo
+instance NFData Cinfo where
+  rnf x = seq x ()
 
 
 ------------------------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/Variance.hs b/src/Language/Haskell/Liquid/Variance.hs
--- a/src/Language/Haskell/Liquid/Variance.hs
+++ b/src/Language/Haskell/Liquid/Variance.hs
@@ -2,7 +2,7 @@
 
 module Language.Haskell.Liquid.Variance (
     Variance(..), VarianceInfo
-	) where
+        ) where
 
 import Data.Typeable
 import Data.Data
diff --git a/src/Language/Haskell/Liquid/Visitors.hs b/src/Language/Haskell/Liquid/Visitors.hs
--- a/src/Language/Haskell/Liquid/Visitors.hs
+++ b/src/Language/Haskell/Liquid/Visitors.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE TypeSynonymInstances      #-} 
 {-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE FlexibleContexts          #-}
 {-# LANGUAGE TupleSections             #-}
 {-# LANGUAGE DeriveDataTypeable        #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
diff --git a/tests/neg/StateConstraints0.hs b/tests/neg/StateConstraints0.hs
--- a/tests/neg/StateConstraints0.hs
+++ b/tests/neg/StateConstraints0.hs
@@ -1,5 +1,6 @@
 module Compose where
 
+import Prelude hiding (Monad(..))
 
 -- | TODO 
 -- | 
@@ -17,7 +18,10 @@
 {-@ runState :: forall <p :: s -> Prop, q :: s -> s -> Prop, r :: s -> a -> Prop>. ST <p, q, r> s a -> x:s<p> -> (a<r x>, s<q x>) @-}
 
 
-
+class Monad m where
+  return :: a -> m a
+  (>>=)  :: m a -> (a -> m b) -> m b
+  (>>)   :: m a -> m b -> m b
 
 instance Monad (ST s) where
   {-@ instance Monad ST s where
@@ -55,7 +59,6 @@
   return x     = ST $ \s -> (x, s)
   (ST g) >>= f = ST (\x -> case g x of {(y, s) -> (runState (f y)) s})    
   (ST g) >>  f = ST (\x -> case g x of {(y, s) -> (runState f) s})    
-  fail         = error
  
 
 
diff --git a/tests/pos/ListLen-LType.hs b/tests/pos/ListLen-LType.hs
--- a/tests/pos/ListLen-LType.hs
+++ b/tests/pos/ListLen-LType.hs
@@ -39,6 +39,7 @@
 -- check [] = [liquidAssertB True]
 -- check (xs:xss) = let n = length xs in map (\xs' -> liquidAssertB (length xs' == n)) xss
 
+chk :: List [a] -> Bool
 chk Nil = liquidAssertB True
 chk (Cons xs xss) =
   case xss of 
diff --git a/tests/pos/ListLen.hs b/tests/pos/ListLen.hs
--- a/tests/pos/ListLen.hs
+++ b/tests/pos/ListLen.hs
@@ -17,6 +17,7 @@
 -- check [] = [liquidAssertB True]
 -- check (xs:xss) = let n = length xs in map (\xs' -> liquidAssertB (length xs' == n)) xss
 
+chk :: [[a]] -> Bool
 chk [] = liquidAssertB True
 chk (xs:xss) =
   case xss of 
diff --git a/tests/pos/ListSort.hs b/tests/pos/ListSort.hs
--- a/tests/pos/ListSort.hs
+++ b/tests/pos/ListSort.hs
@@ -13,6 +13,7 @@
 insertSort (x:xs)     = insert x (insertSort xs) 
 
 {-@ insertSort' :: (Ord a) => xs:[a] -> OList a @-}
+insertSort'           :: (Ord a) => [a] -> [a]
 insertSort' xs        = foldr insert [] xs
 
 insert y []                   = [y]
diff --git a/tests/pos/StateConstraints0.hs b/tests/pos/StateConstraints0.hs
--- a/tests/pos/StateConstraints0.hs
+++ b/tests/pos/StateConstraints0.hs
@@ -1,5 +1,6 @@
 module Compose where
 
+import Prelude hiding (Monad(..))
 
 -- | TODO 
 -- | 
@@ -17,6 +18,10 @@
 {-@ runState :: forall <p :: s -> Prop, q :: s -> s -> Prop, r :: s -> a -> Prop>. ST <p, q, r> s a -> x:s<p> -> (a<r x>, s<q x>) @-}
 
 
+class Monad m where
+  return :: a -> m a
+  (>>=)  :: m a -> (a -> m b) -> m b
+  (>>)   :: m a -> m b -> m b
 
 
 instance Monad (ST s) where
@@ -54,7 +59,6 @@
   return x     = ST $ \s -> (x, s)
   (ST g) >>= f = ST (\x -> case g x of {(y, s) -> (runState (f y)) s})    
   (ST g) >>  f = ST (\x -> case g x of {(y, s) -> (runState f) s})    
-  fail         = error
 
 {-@ incr :: ST <{\x -> true}, {\x v -> v = x + 1}, {\x v -> v = x}>  Int Int @-}
 incr :: ST Int Int
@@ -62,7 +66,7 @@
 
 {-@ foo :: ST <{\x -> true}, {\x v -> true}, {\x v -> v = 0}>  Bool Int @-}
 foo :: ST Bool Int
-foo = do return 0
+foo = return 0
 
 {-@ incr2 :: ST <{\x -> true}, {\x v -> v = x + 2}, {\x v -> v = x + 1}>  Int Int @-}
 incr2 :: ST Int Int
@@ -71,9 +75,7 @@
 {-@ incr3 :: ST <{\x -> true}, {\x v -> v = x + 3}, {\x v -> v = x + 2}>  Int Int @-}
 incr3 :: ST Int Int
 incr3 
-  = do incr
-       incr
-       incr
+  = incr >> incr >> incr
 
 run :: (Int, Int)
 {-@ run :: ({v:Int |  v = 1}, {v:Int |  v = 2}) @-}
diff --git a/tests/pos/ToyMVar.hs b/tests/pos/ToyMVar.hs
--- a/tests/pos/ToyMVar.hs
+++ b/tests/pos/ToyMVar.hs
@@ -5,6 +5,7 @@
 module ToyMVar where
 
 import Prelude hiding (IO)
+import Control.Applicative
 import Data.Set 
 data RealWorld
 data MVar# s a 
@@ -53,3 +54,10 @@
 instance Monad IO where --  GHC-Base.lhs
   return = undefined
   _ >> _ = undefined
+
+instance Applicative IO where
+  pure  = undefined
+  (<*>) = undefined
+
+instance Functor IO where
+  fmap = undefined
diff --git a/tests/pos/propmeasure1.hs b/tests/pos/propmeasure1.hs
new file mode 100644
--- /dev/null
+++ b/tests/pos/propmeasure1.hs
@@ -0,0 +1,11 @@
+module PropMeasure where
+
+nil  = []
+
+
+
+
+
+
+
+
diff --git a/tests/pos/wrap1.hs b/tests/pos/wrap1.hs
--- a/tests/pos/wrap1.hs
+++ b/tests/pos/wrap1.hs
@@ -24,6 +24,7 @@
 nflibXs n x           = prop2 n (WrapType nxs x)
                         where nxs = replicate n x 
 
+prop2 :: Int -> WrapType [a] t -> Bool
 prop2 n (WrapType xs _) = liquidAssertB (n == length xs) 
 
 
diff --git a/tests/test.hs b/tests/test.hs
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP  #-}
 {-# LANGUAGE DeriveDataTypeable  #-}
 {-# LANGUAGE DoAndIfThenElse     #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -19,16 +20,19 @@
 import System.Process
 import Test.Tasty
 import Test.Tasty.HUnit
-import Test.Tasty.Ingredients.Rerun
 import Test.Tasty.Options
 import Test.Tasty.Runners
 import Text.Printf
 
+import Test.Tasty.Ingredients.Rerun
+
+testRunner = rerunningTests [ listingTests, consoleTestReporter ]
+
 main :: IO ()
 main = run =<< tests
   where
     run   = defaultMainWithIngredients [
-                rerunningTests   [ listingTests, consoleTestReporter ]
+                testRunner
               , includingOptions [ Option (Proxy :: Proxy NumThreads)
                                  , Option (Proxy :: Proxy LiquidOpts)
                                  , Option (Proxy :: Proxy SmtSolver) ]