diff --git a/Liquid.hs b/Liquid.hs
--- a/Liquid.hs
+++ b/Liquid.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE TupleSections  #-}
 
+import           Data.Maybe
 import           Data.Monoid      (mconcat, mempty)
 import           System.Exit 
 import           Control.Applicative ((<$>))
@@ -87,7 +88,7 @@
        let out0  = mkOutput cfg res sol annm
        return    $ out0 { o_vars = names } { o_errors  = warns} { o_result = res }
     where 
-       fx        = def { FC.solver = smtsolver cfg, FC.real = real cfg }
+       fx        = def { FC.solver = fromJust (smtsolver cfg), FC.real = real cfg }
        ferr s r  = fmap (tidyError s) $ result $ sinfo <$> r
 
 
diff --git a/include/GHC/Base.spec b/include/GHC/Base.spec
--- a/include/GHC/Base.spec
+++ b/include/GHC/Base.spec
@@ -10,11 +10,11 @@
 measure Prop   :: GHC.Types.Bool -> Prop
 
 measure len :: forall a. [a] -> GHC.Types.Int
-len ([])     = 0
-len (y:ys)   = 1 + (len ys)
+len []     = 0
+len (y:ys) = 1 + len ys
 
 measure null :: forall a. [a] -> Prop
-null ([])   = true
+null []     = true
 null (x:xs) = false
 
 measure fst :: (a,b) -> a
@@ -31,7 +31,7 @@
 map       :: (a -> b) -> xs:[a] -> {v: [b] | len(v) = len(xs)}
 (++)      :: xs:[a] -> ys:[a] -> {v:[a] | (len v) = (len xs) + (len ys)}
 
-$         :: (a -> b) -> a -> b
+($)       :: (a -> b) -> a -> b
 id        :: x:a -> {v:a | v = x}
 
 
diff --git a/include/GHC/CString.spec b/include/GHC/CString.spec
new file mode 100644
--- /dev/null
+++ b/include/GHC/CString.spec
@@ -0,0 +1,7 @@
+module spec GHC.CString where
+
+import GHC.Prim 
+
+-- The equality is untyped, but there is an implicit logic cast
+GHC.CString.unpackCString# :: x:GHC.Prim.Addr# -> {v:String | v = x}
+
diff --git a/include/GHC/Num.spec b/include/GHC/Num.spec
--- a/include/GHC/Num.spec
+++ b/include/GHC/Num.spec
@@ -4,6 +4,6 @@
                     => x:GHC.Integer.Type.Integer
                     -> {v:a | v = x }
 
--- GHC.Num.negate :: (GHC.Num.Num a)
---                => x:a
---                -> {v:a | v = (0-x)}
+GHC.Num.negate :: (GHC.Num.Num a)
+               => x:a
+               -> {v:a | v = -x}
diff --git a/include/GHC/Types.spec b/include/GHC/Types.spec
--- a/include/GHC/Types.spec
+++ b/include/GHC/Types.spec
@@ -6,9 +6,9 @@
 GHC.Types.GT :: {v:GHC.Types.Ordering | v = (cmp v) }
 
 measure cmp :: GHC.Types.Ordering -> GHC.Types.Ordering
-cmp (GHC.Types.EQ) = { v | v = GHC.Types.EQ }
-cmp (GHC.Types.LT) = { v | v = GHC.Types.LT }
-cmp (GHC.Types.GT) = { v | v = GHC.Types.GT }
+cmp GHC.Types.EQ = { v | v = GHC.Types.EQ }
+cmp GHC.Types.LT = { v | v = GHC.Types.LT }
+cmp GHC.Types.GT = { v | v = GHC.Types.GT }
 
 
 GHC.Types.True  :: {v:GHC.Types.Bool | (Prop(v))}
diff --git a/include/Prelude.hquals b/include/Prelude.hquals
--- a/include/Prelude.hquals
+++ b/include/Prelude.hquals
@@ -24,4 +24,8 @@
 qualif Papp3(v:a,~X:b, ~Y:c, ~P:Pred a b c) : papp3(~P, v, ~X, ~Y)
 constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])
 
+// qualif Papp4(v:a,~X:b, ~Y:c, ~Z:d, ~P:Pred a b c d) : papp4(~P, v, ~X, ~Y, ~Z)
+constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])
+
+
 constant Prop : func(0, [GHC.Types.Bool; bool])
diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal
--- a/liquidhaskell.cabal
+++ b/liquidhaskell.cabal
@@ -1,5 +1,5 @@
 Name:                liquidhaskell
-Version:             0.3.0.0
+Version:             0.3.1.0
 Copyright:           2010-15 Ranjit Jhala, University of California, San Diego.
 build-type:          Simple
 Synopsis:            Liquid Types for Haskell 
@@ -33,13 +33,15 @@
           , include/Language/Haskell/Liquid/*.pred
           , include/System/*.spec
           , syntax/liquid.css
-          , syntax/*.el
-          , syntax/*.vim
 
 Source-Repository head
   Type:        git
   Location:    https://github.com/ucsd-progsys/liquidhaskell/
 
+--Flag devel
+--  Description: turn on stricter error reporting for development
+--  Default:     False
+
 Executable liquid
   default-language: Haskell98
   Build-Depends: base >= 4 && < 5
@@ -78,6 +80,8 @@
 
   Main-is: Liquid.hs
   ghc-options: -W
+  -- if flag(devel)
+  --   ghc-options: -Werror
   Default-Extensions: PatternGuards
 
 -- Executable liquid-count-binders
@@ -146,7 +150,7 @@
                 , vector
                 , hashable
                 , unordered-containers
-                , liquid-fixpoint >= 0.2.2.0
+                , liquid-fixpoint >= 0.2.3.0
                 , aeson
                 , bytestring
                 , fingertree
@@ -185,9 +189,11 @@
                     Language.Haskell.Liquid.TransformRec, 
                     Language.Haskell.Liquid.Tidy, 
                     Language.Haskell.Liquid.Types,
+                    Language.Haskell.Liquid.Simplify,
                     Language.Haskell.Liquid.Literals,
                     Language.Haskell.Liquid.Strata,
                     Language.Haskell.Liquid.Fresh,
+                    Language.Haskell.Liquid.Visitors,
                     Language.Haskell.Liquid.WiredIn,
                     Paths_liquidhaskell,
 
@@ -226,6 +232,8 @@
                     Language.Haskell.Liquid.Desugar.DsGRHSs,
                     Language.Haskell.Liquid.Desugar.HscMain
    ghc-options: -W
+   -- if flag(devel)
+   --   ghc-options: -Werror
    ghc-prof-options: -fprof-auto
    Default-Extensions: PatternGuards
 
diff --git a/src/Language/Haskell/Liquid/Bare/Check.hs b/src/Language/Haskell/Liquid/Bare/Check.hs
--- a/src/Language/Haskell/Liquid/Bare/Check.hs
+++ b/src/Language/Haskell/Liquid/Bare/Check.hs
@@ -28,7 +28,7 @@
 import qualified Data.HashMap.Strict as M
 import qualified Data.HashSet        as S
 
-import Language.Fixpoint.Misc (applyNonNull, group, mapSnd, snd3)
+import Language.Fixpoint.Misc (applyNonNull, group, mapSnd, snd3, errorstar, safeHead)
 import Language.Fixpoint.Names (isPrefixOfSym, stripParensSym)
 import Language.Fixpoint.Sort (checkSorted, checkSortedReftFull, checkSortFull)
 import Language.Fixpoint.Types hiding (R)
@@ -203,10 +203,10 @@
 ------------------------------------------------------------------------------------------------
 -- | @checkRType@ determines if a type is malformed in a given environment ---------------------
 ------------------------------------------------------------------------------------------------
-checkRType :: (PPrint r, Reftable r) => TCEmb TyCon -> SEnv SortedReft -> RRType r -> Maybe Doc 
+checkRType :: (PPrint r, Reftable r) => TCEmb TyCon -> SEnv SortedReft -> RRType (UReft r) -> Maybe Doc 
 ------------------------------------------------------------------------------------------------
 
-checkRType emb env t         = efoldReft cb (rTypeSortedReft emb) f insertPEnv env Nothing t 
+checkRType emb env t         = checkAbstractRefs t <|> efoldReft cb (rTypeSortedReft emb) f insertPEnv env Nothing t 
   where 
     cb c ts                  = classBinds (rRCls c ts)
     f env me r err           = err <|> checkReft env emb me r
@@ -214,8 +214,64 @@
     pbinds p                 = (pname p, pvarRType p :: RSort) 
                               : [(x, t) | (t, x, _) <- pargs p]
 
+checkAbstractRefs t = go t
+  where
+    penv = mkPEnv t
 
-checkReft                    :: (PPrint r, Reftable r) => SEnv SortedReft -> TCEmb TyCon -> Maybe (RRType r) -> r -> Maybe Doc 
+    go (RAllT _ t)        = go t
+    go (RAllP _ t)        = go t
+    go (RAllS _ t)        = go t
+    go t@(RApp c ts rs r) = check (toRSort t :: RSort) r <|>  efold go ts <|> go' c rs
+    go t@(RFun _ t1 t2 r) = check (toRSort t :: RSort) r <|> go t1 <|> go t2
+    go t@(RVar _ r)       = check (toRSort t :: RSort) r
+    go (RAllE _ t1 t2)    = go t1 <|> go t2
+    go (REx _ t1 t2)      = go t1 <|> go t2
+    go t@(RAppTy t1 t2 r) = check (toRSort t :: RSort) r <|> go t1 <|> go t2
+    go (RRTy xts _ _ t)   = efold go (snd <$> xts) <|> go t
+    go (RExprArg _)       = Nothing
+    go (RHole _)          = Nothing
+
+    go' c rs = foldl (\acc (x, y) -> acc <|> checkOne' x y) Nothing (zip rs (rTyConPVs c))
+
+    checkOne' (RProp xs t) p 
+      | pvType p /= toRSort t 
+      = Just $ text "Unexpected Sort in" <+> pprint p
+      | or [s1 /= s2 | ((_, s1), (s2, _, _)) <- zip xs (pargs p)]  
+      = Just $ text "Wrong Arguments in" <+> pprint p
+      | length xs /= length (pargs p) 
+      = Just $ text "Wrong Number of Arguments in" <+> pprint p
+      | otherwise  
+      = go t
+    checkOne' (RPropP xs _) p 
+      | or [s1 /= s2 | ((_, s1), (s2, _, _)) <- zip xs (pargs p)]  
+      = Just $ text "Wrong Arguments in" <+> pprint p
+      | length xs /= length (pargs p) 
+      = Just $ text "Wrong Number of Arguments in" <+> pprint p
+      | otherwise  
+      = Nothing 
+    checkOne' _ _ = errorstar "This cannot happen"  
+
+    efold f = foldl (\acc x -> acc <|> f x) Nothing 
+
+    check s (U _ (Pr ps) _) = foldl (\acc pp -> acc <|> checkOne s pp) Nothing ps
+
+    checkOne s p | pvType' p /= s                          
+                 = Just $ text "Incorrect Sort"        <+> pprint p
+                 | or [x == y | (_, x, EVar y) <- pargs p] 
+                 = Just $ text "Missing arguments on " <+> pprint p
+                 | otherwise                               
+                 = Nothing 
+
+    mkPEnv (RAllT _ t) = mkPEnv t
+    mkPEnv (RAllP p t) = p:mkPEnv t 
+    mkPEnv _           = []
+
+    pvType' p = safeHead (showpp p ++ " not in env of " ++ showpp t) [pvType q | q <- penv, pname p == pname q]
+
+
+
+
+checkReft                    :: (PPrint r, Reftable r) => SEnv SortedReft -> TCEmb TyCon -> Maybe (RRType (UReft r)) -> (UReft r) -> Maybe Doc 
 checkReft _   _   Nothing _  = Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.  
 checkReft env emb (Just t) _ = (dr $+$) <$> checkSortedReftFull env' r 
   where 
diff --git a/src/Language/Haskell/Liquid/Bare/Existential.hs b/src/Language/Haskell/Liquid/Bare/Existential.hs
--- a/src/Language/Haskell/Liquid/Bare/Existential.hs
+++ b/src/Language/Haskell/Liquid/Bare/Existential.hs
@@ -52,7 +52,14 @@
   = do t1' <- expToBindT t1
        t2' <- expToBindT t2
        expToBindRef r >>= addExists . RAppTy t1' t2'
-expToBindT t 
+expToBindT (RRTy xts r o t)
+  = do xts' <- zip xs <$> mapM expToBindT ts
+       r'   <- expToBindRef r
+       t'   <- expToBindT t
+       return $ RRTy xts' r' o t'
+  where
+     (xs, ts) = unzip xts 
+expToBindT t
   = return t
 
 expToBindReft              :: SpecProp -> State ExSt SpecProp
diff --git a/src/Language/Haskell/Liquid/Bare/Expand.hs b/src/Language/Haskell/Liquid/Bare/Expand.hs
--- a/src/Language/Haskell/Liquid/Bare/Expand.hs
+++ b/src/Language/Haskell/Liquid/Bare/Expand.hs
@@ -104,6 +104,8 @@
          Nothing ->
            EApp f <$> mapM expandExpr es
 
+expandExpr (ENeg e)
+  = ENeg <$> expandExpr e
 expandExpr (EBin op e1 e2)
   = EBin op <$> expandExpr e1 <*> expandExpr e2
 expandExpr (EIte p e1 e2)
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
@@ -13,6 +13,7 @@
 import NameSet
 import TyCon
 import Var
+import TysWiredIn 
 
 import Control.Applicative ((<$>))
 import Control.Monad.Reader
@@ -26,9 +27,9 @@
 import qualified Data.HashMap.Strict as M
 import qualified Data.HashSet        as S
 
-import Language.Fixpoint.Misc (mapSnd, thd3)
+import Language.Fixpoint.Misc
 import Language.Fixpoint.Names (takeWhileSym)
-import Language.Fixpoint.Types (Expr, SEnv, SortedReft, Symbol, TCEmb, fromListSEnv, insertSEnv, mkSubst, subst, substa, symbol)
+import Language.Fixpoint.Types (Expr(..), SEnv, SortedReft, Symbol, TCEmb, fromListSEnv, insertSEnv, mkSubst, subst, substa, symbol)
 
 import Language.Haskell.Liquid.Dictionaries
 import Language.Haskell.Liquid.GhcMisc (getSourcePos, sourcePosSrcSpan)
@@ -36,6 +37,8 @@
 import Language.Haskell.Liquid.RefType
 import Language.Haskell.Liquid.Types
 import Language.Haskell.Liquid.WiredIn
+import Language.Haskell.Liquid.Visitors
+import Language.Haskell.Liquid.CoreToLogic
 
 import qualified Language.Haskell.Liquid.Measure as Ms
 
@@ -61,8 +64,8 @@
 makeGhcSpec cfg name cbs vars defVars exports env lmap specs
   
   = do sp <- throwLeft =<< execBare act initEnv
-       let env = ghcSpecEnv sp
-       throwLeft $ checkGhcSpec specs env $ postProcess cbs env sp
+       let renv = ghcSpecEnv sp cbs 
+       throwLeft $ checkGhcSpec specs renv $ postProcess cbs renv sp
   where
     act       = makeGhcSpec' cfg cbs vars defVars exports specs
     throwLeft = either Ex.throw return
@@ -78,16 +81,21 @@
     asmSigs' = mapSnd (addTyConInfo tcEmbeds tyconEnv <$>) <$> asmSigs
     dicts'   = dmapty (addTyConInfo tcEmbeds tyconEnv) dicts
 
-ghcSpecEnv sp        = fromListSEnv binds
+ghcSpecEnv sp cbs    = fromListSEnv binds
   where 
     emb              = tcEmbeds sp
     binds            =  [(x,        rSort t) | (x, Loc _ t) <- meas sp]
                      ++ [(symbol v, rSort t) | (v, Loc _ t) <- ctors sp]
                      ++ [(x,        vSort v) | (x, v) <- freeSyms sp, isConLikeId v]
+                     ++ [(val x   , rSort stringrSort) | Just (ELit x s) <- mkLit <$> lconsts, isString s]
     rSort            = rTypeSortedReft emb 
     vSort            = rSort . varRSort 
     varRSort         :: Var -> RSort
     varRSort         = ofType . varType
+    lconsts          = literals cbs
+    stringrSort      :: RSort 
+    stringrSort      = ofType stringTy
+    isString s       = rTypeSort emb stringrSort == s
 
 ------------------------------------------------------------------------------------------------
 makeGhcSpec' :: Config -> [CoreBind] -> [Var] -> [Var] -> NameSet -> [(ModName, Ms.BareSpec)] -> BareM GhcSpec
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
@@ -20,7 +20,7 @@
 import DataCon
 import Id
 import Name
-import Type
+import Type hiding (isFunTy)
 import Var
 
 import Control.Applicative ((<$>), (<*>))
@@ -126,9 +126,11 @@
 strengthenHaskellMeasures hmeas = (\v -> (val v, fmap strengthenResult v)) <$> (S.toList hmeas)
 
 makeMeasureSelectors :: (DataCon, Located DataConP) -> [Measure SpecType DataCon]
-makeMeasureSelectors (dc, (Loc loc (DataConP _ vs _ _ _ xts r))) = go <$> zip (reverse xts) [1..]
+makeMeasureSelectors (dc, (Loc loc (DataConP _ vs _ _ _ xts r))) = catMaybes (go <$> zip (reverse xts) [1..])
   where
-    go ((x,t), i) = makeMeasureSelector (Loc loc x) (dty t) dc n i
+    go ((x,t), i)
+      | isFunTy t = Nothing
+      | True      = Just $ makeMeasureSelector (Loc loc x) (dty t) dc n i
         
     dty t         = foldr RAllT  (RFun dummySymbol r (fmap mempty t) mempty) vs
     n             = length xts
diff --git a/src/Language/Haskell/Liquid/Bare/Plugged.hs b/src/Language/Haskell/Liquid/Bare/Plugged.hs
--- a/src/Language/Haskell/Liquid/Bare/Plugged.hs
+++ b/src/Language/Haskell/Liquid/Bare/Plugged.hs
@@ -21,8 +21,6 @@
 import Data.Generics.Aliases (mkT)
 import Data.Generics.Schemes (everywhere)
 import Data.Monoid
-import Text.PrettyPrint.HughesPJ
-import Text.Printf
 
 import qualified Data.HashMap.Strict as M
 
@@ -88,14 +86,17 @@
     go (RFun _ i o _)   (RFun x i' o' r)   = RFun x <$> go i i' <*> go o o' <*> return r
     go (RAllT _ t)      (RAllT a t')       = RAllT a <$> go t t'
     go (RAllT a t)      t'                 = RAllT a <$> go t t'
+    go t                (RAllP p t')       = RAllP p <$> go t t'
+    go t                (RAllS s t')       = RAllS s <$> go t t'
     go t                (RAllE b a t')     = RAllE b a <$> go t t'
     go t                (REx b x t')       = REx b x <$> go t t'
     go t                (RRTy e r o t')    = RRTy e r o <$> go t t'
     go (RAppTy t1 t2 _) (RAppTy t1' t2' r) = RAppTy <$> go t1 t1' <*> go t2 t2' <*> return r
     go (RApp _ t _ _)   (RApp c t' p r)    = RApp c <$> (zipWithM go t t') <*> return p <*> return r
-    go t                st                 = throwError err
-     where
-       err = errOther $ text $ printf "plugHoles: unhandled case!\nt  = %s\nst = %s\n" (showpp t) (showpp st)
+    -- If we reach the default case, there's probably an error, but we defer
+    -- throwing it as checkGhcSpec does a much better job of reporting the
+    -- problem to the user.
+    go _                st                 = return st
 
     pushCls cs (RRTy e r o t) = RRTy e r o (pushCls cs t)
     pushCls cs t              = foldr (uncurry rFun) t cs 
diff --git a/src/Language/Haskell/Liquid/Bare/RTEnv.hs b/src/Language/Haskell/Liquid/Bare/RTEnv.hs
--- a/src/Language/Haskell/Liquid/Bare/RTEnv.hs
+++ b/src/Language/Haskell/Liquid/Bare/RTEnv.hs
@@ -222,6 +222,8 @@
         go (EApp (Loc _ f) es)
           = go_alias f ++ concatMap go es
 
+        go (ENeg e)
+          = go e
         go (EBin _ e1 e2)
           = go e1 ++ go e2
         go (EIte _ e1 e2)
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
@@ -87,6 +87,7 @@
 	tx _ _ (ESym c)       = ESym c
 	tx _ _ (ECon c)       = ECon c
 	tx _ _ (ELit l s')    = ELit l s'
+	tx s m (ENeg e)       = ENeg (tx s m e)
 	tx s m (EBin o e1 e2) = EBin o (tx s m e1) (tx s m e2)
 	tx s m (EIte p e1 e2) = EIte (tx s m p) (tx s m e1) (tx s m e2)
 	tx s m (ECst e s')    = ECst (tx s m e) s'
@@ -136,4 +137,4 @@
 txPApp (s, m) f es = PBexp $ txEApp (s, m) f es
 
 cmpSymbol s1 {- symbol in Core -} s2 {- logical Symbol-}
-  = (dropModuleNames s1) == s2  
+  = (dropModuleNames s1) == s2
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
@@ -47,6 +47,7 @@
 instance Resolvable Expr where
   resolve l (EVar s)       = EVar   <$> resolve l s
   resolve l (EApp s es)    = EApp   <$> resolve l s  <*> resolve l es
+  resolve l (ENeg e)       = ENeg   <$> resolve l e
   resolve l (EBin o e1 e2) = EBin o <$> resolve l e1 <*> resolve l e2
   resolve l (EIte p e1 e2) = EIte   <$> resolve l p  <*> resolve l e1 <*> resolve l e2
   resolve l (ECst x s)     = ECst   <$> resolve l x  <*> resolve l s
diff --git a/src/Language/Haskell/Liquid/CTags.hs b/src/Language/Haskell/Liquid/CTags.hs
--- a/src/Language/Haskell/Liquid/CTags.hs
+++ b/src/Language/Haskell/Liquid/CTags.hs
@@ -28,7 +28,7 @@
 
 import Language.Fixpoint.Misc         (mapSnd)
 import Language.Fixpoint.Types     (Tag)
-import Language.Haskell.Liquid.GhcInterface (freeVars)
+import Language.Haskell.Liquid.Visitors (freeVars)
 
 -- | The @TagKey@ is the top-level binder, and @Tag@ is a singleton Int list
 
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
@@ -26,30 +26,35 @@
    , diffcheck
 ) where
 
-import           Control.Applicative                 ((<$>))
-import           Control.Monad
+import Control.Applicative                 ((<$>))
+import Control.Monad
+import Data.Maybe
+import System.Directory
+import System.Exit
+import System.Environment
 
-import           Data.List                           (nub)
-import           Data.Monoid
+import System.Console.CmdArgs.Explicit
+import System.Console.CmdArgs.Implicit     hiding (Loud)
+import System.Console.CmdArgs.Text
 
-import           System.Console.CmdArgs              hiding (Loud)
-import           System.Directory                    (doesDirectoryExist, canonicalizePath, getCurrentDirectory)
-import           System.Environment                  (lookupEnv, withArgs)
+import Data.List                           (nub)
+import Data.Monoid
+
 import           System.FilePath                     (dropFileName, isAbsolute,
                                                       takeDirectory, (</>))
 
-import           Language.Fixpoint.Config            hiding (Config, real)
-import           Language.Fixpoint.Files
-import           Language.Fixpoint.Misc
-import           Language.Fixpoint.Names             (dropModuleNames)
-import           Language.Fixpoint.Types             
-import           Language.Haskell.Liquid.Annotate
-import           Language.Haskell.Liquid.Misc
-import           Language.Haskell.Liquid.PrettyPrint
-import           Language.Haskell.Liquid.Types       hiding (config, name, typ)
+import Language.Fixpoint.Config            hiding (Config, real)
+import Language.Fixpoint.Files
+import Language.Fixpoint.Misc
+import Language.Fixpoint.Names             (dropModuleNames)
+import Language.Fixpoint.Types
+import Language.Haskell.Liquid.Annotate
+import Language.Haskell.Liquid.Misc
+import Language.Haskell.Liquid.PrettyPrint
+import Language.Haskell.Liquid.Types       hiding (config, name, typ)
 
-import           Text.Parsec.Pos                     (newPos)
-import           Text.PrettyPrint.HughesPJ
+import Text.Parsec.Pos                     (newPos)
+import Text.PrettyPrint.HughesPJ           hiding (Mode)
 
 
 ---------------------------------------------------------------------------------
@@ -155,12 +160,33 @@
 
 getOpts :: IO Config
 getOpts = do cfg0    <- envCfg
-             cfg1    <- mkOpts =<< cmdArgsRun config
+             cfg1    <- mkOpts =<< cmdArgsRun' config
              pwd     <- getCurrentDirectory
              cfg     <- canonicalizePaths (fixCfg $ mconcat [cfg0, cfg1]) pwd
              whenNormal $ putStrLn copyright
-             return cfg
+             case smtsolver cfg of
+               Just _  -> return cfg
+               Nothing -> do smts <- mapM find [Z3, Cvc4, Mathsat]
+                             case catMaybes smts of
+                               (s:_) -> return (cfg {smtsolver = Just s})
+                               _     -> do putStrLn "ERROR: LiquidHaskell requires z3, cvc4, or mathsat to be installed."
+                                           exitWith $ ExitFailure 2
 
+cmdArgsRun' :: Mode (CmdArgs a) -> IO a
+cmdArgsRun' mode
+  = do parseResult <- process mode <$> getArgs
+       case parseResult of
+         Left err ->
+           putStrLn (help err) >> exitFailure
+         Right args ->
+           cmdArgsApply args
+  where
+    help err
+      = showText defaultWrap $ helpText [err] HelpFormatDefault mode
+
+find :: SMTSolver -> IO (Maybe SMTSolver)
+find smt = maybe Nothing (const $ Just smt) <$> findExecutable (show smt)
+
 -- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have
 --   to worry about relative paths.
 canonicalizePaths :: Config -> FilePath -> IO Config
@@ -284,7 +310,7 @@
     writeBlock _  _ ss     = forM_ ("\n" : ss) putStrLn
 
 resDocs _ Safe             = [text "SAFE"]
-resDocs k (Crash xs s)     = text ("CRASH: " ++ s) : pprManyOrdered k "" xs
+resDocs k (Crash xs s)     = text ("ERROR: " ++ s) : pprManyOrdered k "" xs
 resDocs k (Unsafe xs)      = text "UNSAFE" : pprManyOrdered k "" (nub xs)
 resDocs _ (UnknownError d) = [text $ "PANIC: Unexpected Error: " ++ d, reportUrl]
 
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
@@ -10,8 +10,7 @@
 import Language.Haskell.Liquid.Types
 import Language.Haskell.Liquid.Constraint.Types
 
-import Language.Fixpoint.Types           
-
+import Language.Fixpoint.Types
 
 instance Monoid LConstraint where
 	mempty  = LC []
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
@@ -1,3 +1,5 @@
+{-# LANGUAGE DeriveFoldable            #-}
+{-# LANGUAGE DeriveTraversable         #-}
 {-# LANGUAGE StandaloneDeriving        #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
@@ -46,6 +48,8 @@
 import qualified Data.Text           as T
 import Data.Bifunctor
 import Data.List (foldl')
+import qualified Data.Foldable    as F
+import qualified Data.Traversable as T
 
 import Text.Printf
 
@@ -60,8 +64,8 @@
 import Language.Haskell.Liquid.Variance
 import Language.Haskell.Liquid.Types            hiding (binds, Loc, loc, freeTyVars, Def)
 import Language.Haskell.Liquid.Strata
-import Language.Haskell.Liquid.GhcInterface
 import Language.Haskell.Liquid.RefType
+import Language.Haskell.Liquid.Visitors
 import Language.Haskell.Liquid.PredType         hiding (freeTyVars)          
 import Language.Haskell.Liquid.GhcMisc          ( isInternal, collectArguments, tickSrcSpan
                                                 , hasBaseTypeVar, showPpr)
@@ -554,7 +558,7 @@
        pflag <- pruneRefs <$> get
        γ' <- γ ++= ("bsplitC", v, t1) 
        let r = (mempty :: UReft F.Reft){ur_reft = F.Reft (F.dummySymbol,  [F.RConc $ constraintToLogic γ' (lcs γ')])}
-       let t1' = t1 `strengthen` r
+       let t1' = addRTyConInv (invs γ')  t1 `strengthen` r
        return $ bsplitC' γ' t1' t2 pflag
   where
     F.Reft(v, _) = ur_reft (fromMaybe mempty (stripRTypeBase t1))
@@ -656,6 +660,11 @@
 
 {- see tests/pos/polyfun for why you need everything in fixenv -} 
 addCGEnv :: (SpecType -> SpecType) -> CGEnv -> (String, F.Symbol, SpecType) -> CG CGEnv
+addCGEnv tx γ (msg, x, RAllE y tyy tyx)
+  = do y' <- fresh 
+       γ' <- addCGEnv tx γ (msg, y', tyy)
+       addCGEnv tx γ' (msg, x, tyx `F.subst1` (y, F.EVar y'))
+
 addCGEnv tx γ (_, x, t') 
   = do idx   <- fresh
        let t  = tx $ normalize {-x-} idx t'  
@@ -893,13 +902,25 @@
 ----------------------- TERMINATION TYPE --------------------------------------
 -------------------------------------------------------------------------------
 
-makeDecrIndex :: (Var, SpecType)-> CG [Int]
-makeDecrIndex (x, t) 
+makeDecrIndex :: (Var, Template SpecType)-> CG [Int]
+makeDecrIndex (x, Assumed t)
+  = do dindex <- makeDecrIndexTy x t
+       case dindex of
+         Left _  -> return []
+         Right i -> return i
+makeDecrIndex (x, Asserted t)
+  = do dindex <- makeDecrIndexTy x t
+       case dindex of
+         Left msg -> addWarning msg >> return []
+         Right i  -> return i
+makeDecrIndex _ = return []
+
+makeDecrIndexTy x t
   = do spDecr <- specDecr <$> get
        hint   <- checkHint' (L.lookup x $ spDecr)
        case dindex of
-         Nothing -> addWarning msg >> return []
-         Just i  -> return $ fromMaybe [i] hint
+         Nothing -> return $ Left msg -- addWarning msg >> return []
+         Just i  -> return $ Right $ fromMaybe [i] hint
     where
        ts         = ty_args $ toRTypeRep t
        checkHint' = checkHint x ts isDecreasing
@@ -921,7 +942,7 @@
        mapM  (safeLogIndex msg  ts) index
     where
        loc   = getSrcSpan x
-       ts    = ty_args $ toRTypeRep t
+       ts    = ty_args $ toRTypeRep $ unTemplate t
        msg'  = ErrTermin [x] loc (text $ "No decreasing argument on " ++ (showPpr x) ++ " with " ++ (showPpr vs))
        msg   = ErrTermin [x] loc (text "No decreasing parameter")
 
@@ -1002,22 +1023,22 @@
        let cmakeFinType = if sflag then makeFinType else id
        let cmakeFinTy   = if sflag then makeFinTy   else snd
        let xets = mapThd3 (fmap cmakeFinType) <$> xets''
-       ts'      <- mapM refreshArgs $ (fromAsserted . thd3 <$> xets)
+       ts'      <- mapM (T.mapM refreshArgs) $ (thd3 <$> xets)
        let vs    = zipWith collectArgs ts' es
        is       <- mapM makeDecrIndex (zip xs ts') >>= checkSameLens
        let ts = cmakeFinTy  <$> zip is ts'
-       let xeets = (\vis -> [(vis, x) | x <- zip3 xs is ts]) <$> (zip vs is)
+       let xeets = (\vis -> [(vis, x) | x <- zip3 xs is $ map unTemplate ts]) <$> (zip vs is)
        (L.transpose <$> mapM checkIndex (zip4 xs vs ts is)) >>= checkEqTypes
        let rts   = (recType <$>) <$> xeets
-       let xts   = zip xs (Asserted <$> ts)
+       let xts   = zip xs ts
        γ'       <- foldM extender γ xts
        let γs    = [γ' `withTRec` (zip xs rts') | rts' <- rts]
-       let xets' = zip3 xs es (Asserted <$> ts)
+       let xets' = zip3 xs es ts
        mapM_ (uncurry $ consBind True) (zip γs xets')
        return γ'
   where
        (xs, es) = unzip xes
-       collectArgs    = collectArguments . length . ty_binds . toRTypeRep
+       collectArgs    = collectArguments . length . ty_binds . toRTypeRep . unTemplate
        checkEqTypes :: [[Maybe SpecType]] -> CG [[SpecType]]
        checkEqTypes x = mapM (checkAll err1 toRSort) (catMaybes <$> x)
        checkSameLens  = checkAll err2 length
@@ -1050,8 +1071,11 @@
                    | otherwise              = Nothing
         err      = "Constant: consCBWithExprs"
 
-makeFinTy (ns, t) = fromRTypeRep $ trep {ty_args = args'}
-  where trep = toRTypeRep t
+makeFinTy (ns, t) = fmap go t
+  where
+    go t = fromRTypeRep $ trep {ty_args = args'}
+      where
+        trep = toRTypeRep t
         args' = mapNs ns makeFinType $ ty_args trep
 
 
@@ -1181,18 +1205,18 @@
 
 addBinders γ0 x' cbs   = foldM (++=) (γ0 -= x') [("addBinders", x, t) | (x, t) <- cbs]
 
-data Template a = Asserted a | Assumed a | Unknown deriving (Functor)
+data Template a = Asserted a | Assumed a | Unknown deriving (Functor, F.Foldable, T.Traversable)
 
 deriving instance (Show a) => (Show (Template a))
 
+unTemplate (Asserted t) = t
+unTemplate (Assumed t) = t
+unTemplate _ = errorstar "Constraint.Generate.unTemplate called on `Unknown`"
 
 addPostTemplate γ (Asserted t) = Asserted <$> addPost γ t
 addPostTemplate γ (Assumed  t) = Assumed  <$> addPost γ t
 addPostTemplate _ Unknown      = return Unknown 
 
-fromAsserted (Asserted t) = t
-fromAsserted _            = errorstar "Constraint.Generate.fromAsserted called on invalid inputs"
-
 safeFromAsserted _ (Asserted t) = t
 safeFromAsserted msg _ = errorstar $ "safeFromAsserted:" ++ msg 
 
@@ -1407,8 +1431,8 @@
 consE _ e@(Coercion _)
    = trueTy $ exprType e
 
-consE _ e	    
-  = errorstar $ "consE cannot handle " ++ showPpr e 
+consE _ e@(Type t)     
+  = errorstar $ "consE cannot handle type" ++ showPpr (e, t) 
 
 castTy _ τ (Var x)
   = do t <- trueTy τ 
@@ -1446,8 +1470,11 @@
        return t
 
 checkUnbound γ e x t 
-  | x `notElem` (F.syms t) = t
-  | otherwise              = errorstar $ "consE: cannot handle App " ++ showPpr e ++ " at " ++ showPpr (loc γ)
+  | x `notElem` (F.syms t) 
+  = t
+  | otherwise              
+  = errorstar $ "checkUnbound: " ++ show x ++ " is elem of syms of " ++ show t
+                 ++ "\nIn\t"  ++ showPpr e ++ " at " ++ showPpr (loc γ)
 
 dropExists γ (REx x tx t) = liftM (, t) $ (γ, "dropExists") += (x, tx)
 dropExists γ t            = return (γ, t)
diff --git a/src/Language/Haskell/Liquid/CoreToLogic.hs b/src/Language/Haskell/Liquid/CoreToLogic.hs
--- a/src/Language/Haskell/Liquid/CoreToLogic.hs
+++ b/src/Language/Haskell/Liquid/CoreToLogic.hs
@@ -22,13 +22,13 @@
 import Literal
 import IdInfo
 
-
-import TysWiredIn
+import qualified Data.ByteString as B
+import TysWiredIn 
 
 import Control.Applicative 
 
 import Language.Fixpoint.Misc
-import Language.Fixpoint.Names (dropModuleNames, isPrefixOfSym)
+import Language.Fixpoint.Names (dropModuleNames, isPrefixOfSym, propConName)
 import Language.Fixpoint.Types hiding (Def, R, simplify)
 import qualified Language.Fixpoint.Types as F
 import Language.Haskell.Liquid.GhcMisc
@@ -79,11 +79,12 @@
   where rep = toRTypeRep t
         res = ty_res rep
         xs  = intSymbol (symbol ("x" :: String)) <$> [1..]
-        r'  = U (exprReft (EApp f (EVar <$> vxs)))         mempty mempty
-        r   = U (propReft (PBexp $ EApp f (EVar <$> vxs))) mempty mempty
-        vxs = fst $  unzip $ dropWhile isClassBind $ zip xs (ty_args rep)
+        r'  = U (exprReft (EApp f (mkA <$> vxs)))         mempty mempty
+        r   = U (propReft (PBexp $ EApp f (mkA <$> vxs))) mempty mempty
+        vxs = dropWhile isClassBind $ zip xs (ty_args rep)
         f   = dummyLoc $ dropModuleNames $ simplesymbol v
         t   = (ofType $ varType v) :: SpecType
+        mkA = \(x, t) -> if isBool t then EApp (dummyLoc propConName) [(EVar x)] else EVar x
 
 
 simplesymbol = symbol . getName
@@ -151,9 +152,9 @@
     go acc (C.Lam x e)  = go (symbol x : acc) e
     go acc (C.Tick _ e) = go acc e
     go acc e            | eqType rty boolTy 
-                        = (reverse acc,) . Left  . traceShow "coreToPred"  <$> coreToPred e  
+                        = (reverse acc,) . Left  <$> coreToPred e  
                         | otherwise       
-                        = (reverse acc,) . Right . traceShow "coreToLogic" <$> coreToLogic e
+                        = (reverse acc,) . Right <$> coreToLogic e
 
     inline_preds = inline (eqType boolTy . varType)
 
@@ -242,6 +243,9 @@
         (\x -> makeApp def lmap x args) <$> tosymbol' f
 
 makeApp :: Expr -> LogicMap -> Located Symbol-> [Expr] -> Expr
+makeApp _ _ f [e] | val f == symbol ("GHC.Num.negate" :: String)
+  = ENeg e
+
 makeApp _ _ f [e1, e2] | Just op <- M.lookup (val f) bops
   = EBin op e1 e2
 
@@ -299,9 +303,20 @@
 mkLit (MachFloat  n)   = mkR n
 mkLit (MachDouble n)   = mkR n
 mkLit (LitInteger n _) = mkI n
+mkLit (MachStr s)      = mkS s 
 mkLit _                = Nothing -- ELit sym sort
+
 mkI                    = Just . ECon . I  
 mkR                    = Just . ECon . F.R . fromRational
+mkS s                  = Just (ELit  (dummyLoc $ symbol s) stringSort)
+
+
+stringSort = rTypeSort M.empty (ofType stringTy :: RSort)
+-- stringSort = rTypeSort M.empty (ofType stringTy :: RSort)
+
+
+instance Symbolic B.ByteString where
+  symbol x = symbol $ init $ tail $ show x
 
 ignoreVar i = simpleSymbolVar i `elem` ["I#"]
 
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
@@ -42,8 +42,9 @@
 import            Language.Fixpoint.Types         (FixResult (..))
 import            Language.Fixpoint.Files
 import            Language.Haskell.Liquid.Types   (AnnInfo (..), Error, TError (..), Output (..))
-import            Language.Haskell.Liquid.GhcInterface
 import            Language.Haskell.Liquid.GhcMisc
+import            Language.Haskell.Liquid.Visitors
+import            Language.Haskell.Liquid.Errors   ()
 import            Text.Parsec.Pos                  (sourceName, sourceLine, sourceColumn, SourcePos, newPos)
 import            Text.PrettyPrint.HughesPJ        (text, render, Doc)
 
diff --git a/src/Language/Haskell/Liquid/Errors.hs b/src/Language/Haskell/Liquid/Errors.hs
--- a/src/Language/Haskell/Liquid/Errors.hs
+++ b/src/Language/Haskell/Liquid/Errors.hs
@@ -9,11 +9,13 @@
 
 
 import           Control.Applicative                 ((<$>), (<*>))
+import           Control.Arrow                       (second)
 import           Control.Exception                   (Exception (..))
 import           Data.Aeson
-import           Data.Hashable
+import           Data.Generics                       (everywhere, mkT)
 import qualified Data.HashMap.Strict                 as M
 import qualified Data.HashSet                        as S
+import           Data.Hashable
 import           Data.List                           (intersperse)
 import           Data.Maybe                          (fromMaybe, maybeToList)
 import           Data.Monoid                         hiding ((<>))
@@ -21,12 +23,13 @@
 import           Language.Fixpoint.Types             hiding (shiftVV)
 import           Language.Haskell.Liquid.PrettyPrint
 import           Language.Haskell.Liquid.RefType
+import           Language.Haskell.Liquid.Simplify
 import           Language.Haskell.Liquid.Tidy
 import           Language.Haskell.Liquid.Types
 import           SrcLoc                              (SrcSpan)
 import           Text.PrettyPrint.HughesPJ
-import           Control.Arrow                       (second)
 
+
 type Ctx = M.HashMap Symbol SpecType
 
 ------------------------------------------------------------------------
@@ -64,10 +67,11 @@
     (t', ro)  = stripRType t                
 
 stripRType    :: SpecType -> (SpecType, Maybe RReft)
-stripRType t  = (t', ro)
+stripRType st = (t', ro)
   where
     t'        = fmap (const (uTop mempty)) t
     ro        = stripRTypeBase  t 
+    t         = simplifyBounds st 
 
 tidyREnv      :: [Symbol] -> M.HashMap Symbol SpecType -> [(Symbol, SpecType)]
 tidyREnv xs m = [(x, t) | x <- xs', t <- maybeToList (M.lookup x m), ok t]
@@ -119,8 +123,10 @@
   | otherwise   = dt <+> dr 
     where
       dt        = rtypeDoc Lossy t'
-      dr        = maybe empty ((text "|" <+>) . pprint) ro 
+      dr        = maybe empty ((text "|" <+>) . pprint . everywhere (mkT noCasts)) ro 
       (t', ro)  = stripRType t
+      noCasts (ECst x _) = x
+      noCasts e          = e
 
 -- full = isNontrivialVV $ rTypeValueVar t = 
 
diff --git a/src/Language/Haskell/Liquid/Fresh.hs b/src/Language/Haskell/Liquid/Fresh.hs
--- a/src/Language/Haskell/Liquid/Fresh.hs
+++ b/src/Language/Haskell/Liquid/Fresh.hs
@@ -50,13 +50,13 @@
   refresh [] = fresh
   refresh s  = return s
 
-instance (Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) where
+instance (Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => Freshable m (RRType r) where
   fresh   = errorstar "fresh RefType"
   refresh = refreshRefType
   true    = trueRefType
 
 -----------------------------------------------------------------------------------------------
-trueRefType :: (Freshable m Integer, Freshable m r, Reftable r) => RRType r -> m (RRType r)
+trueRefType :: (Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => RRType r -> m (RRType r)
 -----------------------------------------------------------------------------------------------
 trueRefType (RAllT α t)
   = RAllT α <$> true t
@@ -79,7 +79,13 @@
 trueRefType (RVar a r)
   = RVar a <$> true r
 
-trueRefType t
+trueRefType (RAllE y ty tx)
+  = do y'  <- fresh 
+       ty' <- true ty
+       tx' <- true tx
+       return $ RAllE y' ty' (tx' `subst1` (y, EVar y')) 
+
+trueRefType t 
   = return t
 
 trueRef (RProp s t) = RProp s <$> trueRefType t
@@ -87,7 +93,7 @@
 
 
 -----------------------------------------------------------------------------------------------
-refreshRefType :: (Freshable m Integer, Freshable m r, Reftable r) => RRType r -> m (RRType r)
+refreshRefType :: (Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => RRType r -> m (RRType r)
 -----------------------------------------------------------------------------------------------
 refreshRefType (RAllT α t)
   = RAllT α <$> refresh t
@@ -110,6 +116,12 @@
 
 refreshRefType (RAppTy t t' r)
   = RAppTy <$> refresh t <*> refresh t' <*> refresh r
+
+refreshRefType (RAllE y ty tx)
+  = do y'  <- fresh 
+       ty' <- refresh ty
+       tx' <- refresh tx
+       return $ RAllE y' ty' (tx' `subst1` (y, EVar y')) 
 
 refreshRefType t
   = return t
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
@@ -10,8 +10,6 @@
   -- * extract all information needed for verification
     getGhcInfo
 
-  -- * visitors 
-  , CBVisitable (..) 
   ) where
 import IdInfo
 import InstEnv
@@ -22,7 +20,6 @@
 import DriverPipeline (compileFile)
 import Text.PrettyPrint.HughesPJ
 import HscTypes hiding (Target)
-import Literal
 import CoreSyn
 
 import Var
@@ -36,10 +33,9 @@
 
 import DynFlags
 import Control.Monad (filterM, foldM, when, forM, forM_, liftM)
-import Control.DeepSeq
 import Control.Applicative  hiding (empty)
 import Data.Monoid hiding ((<>))
-import Data.List (foldl', find, (\\), delete, nub)
+import Data.List (find, nub)
 import Data.Maybe (catMaybes, maybeToList)
 import qualified Data.HashSet        as S
   
@@ -55,6 +51,8 @@
 import Language.Haskell.Liquid.Misc
 import Language.Haskell.Liquid.PrettyPrint
 
+import Language.Haskell.Liquid.Visitors
+
 import Language.Haskell.Liquid.CmdLine (withPragmas)
 import Language.Haskell.Liquid.Parse
 
@@ -96,6 +94,10 @@
       modguts            <- getGhcModGuts1 target
       hscEnv             <- getSession
       coreBinds          <- liftIO $ anormalize (not $ nocaseexpand cfg) hscEnv modguts
+      let datacons        = [ dataConWorkId dc
+                            | tc <- mgi_tcs modguts
+                            , dc <- tyConDataCons tc
+                            ]
       let impVs           = importVars  coreBinds 
       let defVs           = definedVars coreBinds 
       let useVs           = readVars    coreBinds
@@ -105,7 +107,7 @@
       (spec, imps, incs) <- moduleSpec cfg coreBinds (impVs ++ defVs) letVs name' modguts tgtSpec logicmap impSpecs'
       liftIO              $ whenLoud $ putStrLn $ "Module Imports: " ++ show imps
       hqualFiles         <- moduleHquals modguts paths target imps incs
-      return              $ GI hscEnv coreBinds derVs impVs letVs useVs hqualFiles imps incs spec 
+      return              $ GI hscEnv coreBinds derVs impVs (letVs ++ datacons) useVs hqualFiles imps incs spec 
 
 
 makeLogicMap 
@@ -335,126 +337,8 @@
   = Nothing
 
 
-------------------------------------------------------------------------------
--------------------------------- A CoreBind Visitor --------------------------
-------------------------------------------------------------------------------
 
--- TODO: syb-shrinkage
 
-class CBVisitable a where
-  freeVars :: S.HashSet Var -> a -> [Var]
-  readVars :: a -> [Var] 
-  letVars  :: a -> [Var] 
-  literals :: a -> [Literal]
-
-instance CBVisitable [CoreBind] where
-  freeVars env cbs = (sortNub xs) \\ ys 
-    where xs = concatMap (freeVars env) cbs 
-          ys = concatMap bindings cbs
-  
-  readVars = concatMap readVars
-  letVars  = concatMap letVars 
-  literals = concatMap literals
-
-instance CBVisitable CoreBind where
-  freeVars env (NonRec x e) = freeVars (extendEnv env [x]) e 
-  freeVars env (Rec xes)    = concatMap (freeVars env') es 
-                              where (xs,es) = unzip xes 
-                                    env'    = extendEnv env xs 
-
-  readVars (NonRec _ e)     = readVars e
-  readVars (Rec xes)        = concat [x `delete` nubReadVars e |(x, e) <- xes]
-    where nubReadVars = sortNub . readVars
-
-  letVars (NonRec x e)      = x : letVars e
-  letVars (Rec xes)         = xs ++ concatMap letVars es
-    where 
-      (xs, es)              = unzip xes
-
-  literals (NonRec _ e)      = literals e
-  literals (Rec xes)         = concatMap literals $ map snd xes
-
-instance CBVisitable (Expr Var) where
-  freeVars = exprFreeVars
-  readVars = exprReadVars
-  letVars  = exprLetVars
-  literals = exprLiterals
-
-exprFreeVars = go 
-  where 
-    go env (Var x)         = if x `S.member` env then [] else [x]  
-    go env (App e a)       = (go env e) ++ (go env a)
-    go env (Lam x e)       = go (extendEnv env [x]) e
-    go env (Let b e)       = (freeVars env b) ++ (go (extendEnv env (bindings b)) e)
-    go env (Tick _ e)      = go env e
-    go env (Cast e _)      = go env e
-    go env (Case e x _ cs) = (go env e) ++ (concatMap (freeVars (extendEnv env [x])) cs) 
-    go _   _               = []
-
-exprReadVars = go
-  where
-    go (Var x)             = [x]
-    go (App e a)           = concatMap go [e, a] 
-    go (Lam _ e)           = go e
-    go (Let b e)           = readVars b ++ go e 
-    go (Tick _ e)          = go e
-    go (Cast e _)          = go e
-    go (Case e _ _ cs)     = (go e) ++ (concatMap readVars cs) 
-    go _                   = []
-
-exprLetVars = go
-  where
-    go (Var _)             = []
-    go (App e a)           = concatMap go [e, a] 
-    go (Lam x e)           = x : go e
-    go (Let b e)           = letVars b ++ go e 
-    go (Tick _ e)          = go e
-    go (Cast e _)          = go e
-    go (Case e x _ cs)     = x : go e ++ concatMap letVars cs
-    go _                   = []
-
-exprLiterals = go
-  where
-    go (Lit l)             = [l]
-    go (App e a)           = concatMap go [e, a] 
-    go (Let b e)           = literals b ++ go e 
-    go (Lam _ e)           = go e
-    go (Tick _ e)          = go e
-    go (Cast e _)          = go e
-    go (Case e _ _ cs)     = (go e) ++ (concatMap literals cs) 
-    go _                   = []
-
-
-instance CBVisitable (Alt Var) where
-  freeVars env (a, xs, e) = freeVars env a ++ freeVars (extendEnv env xs) e
-  readVars (_,_, e)       = readVars e
-  letVars  (_,xs,e)       = xs ++ letVars e
-  literals (c,_, e)       = literals c ++ literals e
-
-
-instance CBVisitable AltCon where
-  freeVars _ (DataAlt dc) = dataConImplicitIds dc
-  freeVars _ _            = []
-  readVars _              = []
-  letVars  _              = []
-  literals (LitAlt l)     = [l]
-  literals _              = []
-
-
-
-extendEnv = foldl' (flip S.insert)
-
-bindings (NonRec x _) 
-  = [x]
-bindings (Rec  xes  ) 
-  = map fst xes
-
---------------------------------------------------------------------
------- Strictness --------------------------------------------------
---------------------------------------------------------------------
-
-instance NFData Var
-instance NFData SrcSpan
 
 instance PPrint GhcSpec where
   pprint spec =  (text "******* Target Variables ********************")
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
@@ -184,6 +184,13 @@
 holeRefP    = reserved "_" >> spaces >> return (RHole . uTop)
 refasHoleP  = refasP <|> (reserved "_" >> return [hole])
 
+-- FIXME: the use of `blanks = oneOf " \t"` here is a terrible and fragile hack
+-- to avoid parsing:
+--
+--   foo :: a -> b
+--   bar :: a
+--
+-- as `foo :: a -> b bar`..
 bbaseP :: Parser (Reft -> BareType)
 bbaseP 
   =  holeRefP
@@ -645,7 +652,7 @@
   = do pos  <- getPosition
        name <- upperIdP
        spaces
-       args <- sepBy aliasIdP spaces
+       args <- sepBy aliasIdP blanks
        whiteSpace >> reservedOp "=" >> whiteSpace
        body <- bodyP 
        let (tArgs, vArgs) = partition (isLower . headSym) args
@@ -740,16 +747,16 @@
 
 measurePatP :: Parser (LocSymbol, [LocSymbol])
 measurePatP 
-  =  try tupPatP 
- <|> try (parens conPatP)
- <|> try (parens consPatP)
- <|>     (parens nilPatP)
+  =  parens (try conPatP <|> try consPatP <|> nilPatP <|> tupPatP)
+ <|> nullaryConPatP
 
-tupPatP  = mkTupPat  <$> (parens       $  sepBy locLowerIdP comma)
+tupPatP  = mkTupPat  <$> sepBy1 locLowerIdP comma
 conPatP  = (,)       <$> locParserP dataConNameP <*> sepBy locLowerIdP whiteSpace
 consPatP = mkConsPat <$> locLowerIdP  <*> colon <*> locLowerIdP
-nilPatP  = mkNilPat  <$> brackets whiteSpace 
+nilPatP  = mkNilPat  <$> brackets whiteSpace
 
+nullaryConPatP = nilPatP <|> ((,[]) <$> locParserP dataConNameP)
+
 mkTupPat zs     = (tupDataCon (length zs), zs)
 mkNilPat _      = (dummyLoc "[]", []    )
 mkConsPat x _ y = (dummyLoc ":" , [x, y])
@@ -762,8 +769,18 @@
 
 dataConFieldsP 
   =   (braces $ sepBy predTypeDDP comma)
-  <|> (sepBy (parens predTypeDDP) spaces)
+  <|> (sepBy dataConFieldP spaces)
 
+dataConFieldP
+  = parens ( try predTypeDDP
+             <|> do v <- dummyBindP
+                    t <- bareTypeP
+                    return (v,t)
+           )
+    <|> do v <- dummyBindP
+           t <- bareTypeP
+           return (v,t)
+
 predTypeDDP 
   = liftM2 (,) bbindP bareTypeP
 
@@ -827,7 +844,7 @@
          Nothing -> return []
 
 -- specWrap  = between     (string "{-@" >> spaces) (spaces >> string "@-}")
-specWraps = betweenMany (string "{-@" >> spaces) (spaces >> string "@-}")
+specWraps = betweenMany (string "{-@" >> whiteSpace) (whiteSpace >> string "@-}")
 
 ---------------------------------------------------------------
 -- | Bundling Parsers into a Typeclass ------------------------
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
@@ -281,9 +281,10 @@
   = r2 `meet` r1
   | all (\(_, x, EVar y) -> x /= y) (pargs π)
   = r2 `meet` (subst su r1)
-  | otherwise
+  | otherwise 
   = errorstar $ "PredType.meetListWithPSub partial application to " ++ showpp π
-  where su  = mkSubst [(x, y) | (x, (_, _, y)) <- zip (fst <$> ss) (pargs π)]
+  where 
+    su  = mkSubst [(x, y) | (x, (_, _, y)) <- zip (fst <$> ss) (pargs π)]
 
 meetListWithPSubRef ss (RProp s1 r1) (RProp s2 r2) π
   | all (\(_, x, EVar y) -> x == y) (pargs π)
diff --git a/src/Language/Haskell/Liquid/Qualifier.hs b/src/Language/Haskell/Liquid/Qualifier.hs
--- a/src/Language/Haskell/Liquid/Qualifier.hs
+++ b/src/Language/Haskell/Liquid/Qualifier.hs
@@ -22,14 +22,13 @@
 specificationQualifiers :: Int -> GhcInfo -> [Qualifier]
 -----------------------------------------------------------------------------------
 specificationQualifiers k info
-  = [ q | (x, t) <- (tySigs $ spec info) ++ (asmSigs $ spec info)
+  = [ q | (x, t) <- (tySigs $ spec info) ++ (asmSigs $ spec info) ++ (ctors $ spec info)
         -- FIXME: this mines extra, useful qualifiers but causes a significant increase in running time
         -- , ((isClassOp x || isDataCon x) && x `S.member` (S.fromList $ impVars info ++ defVars info)) || x `S.member` (S.fromList $ defVars info)
         , x `S.member` (S.fromList $ defVars info)
         , q <- refTypeQuals (getSourcePos x) (tcEmbeds $ spec info) (val t)
         , length (q_params q) <= k + 1
     ]
-
 
 -- GRAVEYARD: scraping quals from imports kills the system with too much crap
 -- specificationQualifiers info = {- filter okQual -} qs 
diff --git a/src/Language/Haskell/Liquid/Simplify.hs b/src/Language/Haskell/Liquid/Simplify.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/Liquid/Simplify.hs
@@ -0,0 +1,32 @@
+module Language.Haskell.Liquid.Simplify (simplifyBounds) where
+
+import Language.Haskell.Liquid.Types
+
+import Language.Fixpoint.Types
+
+import Control.Applicative                 ((<$>))
+
+simplifyLen = 5
+
+simplifyBounds :: SpecType -> SpecType
+simplifyBounds = fmap go 
+  where
+  	go x = x{ur_reft = go' $ ur_reft x}
+
+  	go' (Reft (v, rs)) = Reft(v, filter (not . isBoundLike) rs)
+
+  	isBoundLike (RConc pred) = isBoundLikePred pred
+  	isBoundLike (RKvar _ _)  = False
+
+  	isBoundLikePred (PAnd ps)
+  	  = moreThan simplifyLen (isImp <$> ps)
+  	isBoundLikePred _ = False
+
+  	isImp (PImp _ _) = True
+  	isImp _          = False
+
+  	moreThan 0 _          = True
+  	moreThan _ []         = False
+  	moreThan i (True:xs)  = moreThan (i-1) xs
+  	moreThan i (False:xs) = moreThan i xs
+
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
@@ -231,6 +231,7 @@
 import Language.Fixpoint.Misc
 import Language.Fixpoint.Types      hiding (Predicate, Def, R)
 import Language.Fixpoint.Names      (funConName, listConName, tupConName)
+import qualified Language.Fixpoint.PrettyPrint as F
 import CoreSyn (CoreBind)
 
 import Language.Haskell.Liquid.Variance
@@ -238,7 +239,6 @@
 
 
 import Data.Default
-
 -----------------------------------------------------------------------------
 -- | Command Line Config Options --------------------------------------------
 -----------------------------------------------------------------------------
@@ -261,7 +261,7 @@
   , totality       :: Bool       -- ^ check totality in definitions
   , noPrune        :: Bool       -- ^ disable prunning unsorted Refinements
   , maxParams      :: Int        -- ^ the maximum number of parameters to accept when mining qualifiers
-  , smtsolver      :: SMTSolver  -- ^ name of smtsolver to use [default: z3-API]
+  , smtsolver      :: Maybe SMTSolver  -- ^ name of smtsolver to use [default: try z3, cvc4, mathsat in order]
   , shortNames     :: Bool       -- ^ drop module qualifers from pretty-printed names.
   , shortErrors    :: Bool       -- ^ don't show subtyping errors and contexts. 
   , ghcOptions     :: [String]   -- ^ command-line options to pass to GHC
@@ -302,7 +302,7 @@
 
 ppEnv           = ppEnvPrintPreds
 _ppEnvCurrent    = PP False False False False
-ppEnvPrintPreds = PP True False False False
+ppEnvPrintPreds = PP False False False False
 ppEnvShort pp   = pp { ppShort = True }
 
 
@@ -449,7 +449,14 @@
   hashWithSalt i (PV n _ _ _) = hashWithSalt i n
 
 
+
 --------------------------------------------------------------------
+------ Strictness --------------------------------------------------
+--------------------------------------------------------------------
+
+instance NFData Var
+instance NFData SrcSpan
+--------------------------------------------------------------------
 ------------------ Predicates --------------------------------------
 --------------------------------------------------------------------
 
@@ -991,20 +998,17 @@
 instance (PPrint r, Reftable r) => Reftable (UReft r) where
   isTauto            = isTauto_ureft 
   ppTy               = ppTy_ureft
-  toReft (U r ps _)  = toReft r `meet` toReft ps
+  toReft (U r ps _)  = toReft r `meet` toReft ps 
   params (U r _ _)   = params r
   bot (U r _ s)      = U (bot r) (Pr []) (bot s)
   top (U r p s)      = U (top r) (top p) (top s)
 
   ofReft = error "TODO: UReft.ofReft"
 
-isTauto_ureft u      = isTauto (ur_reft u) && isTauto (ur_pred u) && (isTauto $ ur_strata u)
-
-isTauto_ureft' u     = isTauto (ur_reft u) && isTauto (ur_pred u)
+isTauto_ureft u      = isTauto (ur_reft u) && isTauto (ur_pred u) -- && (isTauto $ ur_strata u)
 
 ppTy_ureft u@(U r p s) d 
   | isTauto_ureft  u  = d
-  | isTauto_ureft' u  = d <> ppr_str s
   | otherwise         = ppr_reft r (ppTy p d) s
 
 ppr_reft r d s       = braces (toFix v <+> colon <+> d <> ppr_str s <+> text "|" <+> pprint r')
@@ -1050,6 +1054,7 @@
   isTauto (Pr ps)      = null ps
 
   bot (Pr _)           = errorstar "No BOT instance for Predicate"
+  -- NV: This does not print abstract refinements....
   -- HACK: Hiding to not render types in WEB DEMO. NEED TO FIX.
   ppTy r d | isTauto r        = d 
            | not (ppPs ppEnv) = d
@@ -1117,6 +1122,7 @@
 isBase (RFun _ t1 t2 _) = isBase t1 && isBase t2
 isBase (RAppTy t1 t2 _) = isBase t1 && isBase t2
 isBase (RRTy _ _ _ t)   = isBase t
+isBase (RAllE _ _ t)    = isBase t
 isBase _                = False
 
 isFunTy (RAllE _ _ t)    = isFunTy t
@@ -1308,66 +1314,34 @@
   pprint = pprint . val 
 
 instance PPrint Int where
-  pprint = toFix
+  pprint = F.pprint
 
 instance PPrint Integer where
-  pprint = toFix
+  pprint = F.pprint
 
 instance PPrint Constant where
-  pprint = toFix
+  pprint = F.pprint
 
 instance PPrint Brel where
-  pprint Eq = text "=="
-  pprint Ne = text "/="
-  pprint r  = toFix r
+  pprint = F.pprint
 
 instance PPrint Bop where
-  pprint  = toFix 
+  pprint = F.pprint
 
 instance PPrint Sort where
-  pprint = toFix  
+  pprint = F.pprint
 
 instance PPrint Symbol where
   pprint = pprint . symbolText
 
 instance PPrint Expr where
-  pprint (EApp f es)     = {- parens $ -} intersperse empty $ (pprint f) : (pprint <$> es) 
-  pprint (ECon c)        = pprint c 
-  pprint (EVar s)        = pprint s
-  pprint (ELit s _)      = pprint s
-  pprint (EBin o e1 e2)  = {- parens $ -} pprint e1 <+> pprint o <+> pprint e2
-  pprint (EIte p e1 e2)  = {- parens $ -} text "if" <+> parens (pprint p) <+> text "then" <+> pprint e1 <+> text "else" <+> pprint e2 
-  pprint (ECst e so)     = parens $ pprint e <+> text " : " <+> pprint so 
-  pprint (EBot)          = text "_|_"
-  pprint (ESym s)        = pprint s
+  pprint = F.pprint
 
 instance PPrint SymConst where
-  pprint (SL s)          = text $ T.unpack s
+  pprint = F.pprint
 
 instance PPrint Pred where
-  pprint PTop            = text "???"
-  pprint PTrue           = trueD 
-  pprint PFalse          = falseD
-  pprint (PBexp e)       = {- parens $ -} pprint e
-  pprint (PNot p)        = {- parens $ -} text "not" <+> parens (pprint p)
-  pprint (PImp p1 p2)    = {- parens $ -} pprint p1 <+> text "=>"  <+> pprint p2
-  pprint (PIff p1 p2)    = {- parens $ -} (pprint p1) <+> text "<=>" <+> (pprint p2)
-  pprint (PAnd ps)       = {- parens $ -} pprintBin trueD  andD ps
-  pprint (POr  ps)       = {- parens $ -} pprintBin falseD orD  ps 
-  pprint (PAtom r e1 e2) = {- parens $ -} pprint e1 <+> pprint r <+> pprint e2
-  pprint (PAll xts p)    = text "forall" <+> toFix xts <+> text "." <+> pprint p
-
-trueD  = text "true"
-falseD = text "false"
-andD   = text " &&"
-orD    = text " ||"
-
-pprintBin b _ []     = b
-pprintBin _ o xs     = intersperse o $ pprint <$> xs 
-
--- pprintBin b o []     = b
--- pprintBin b o [x]    = pprint x
--- pprintBin b o (x:xs) = pprint x <+> o <+> pprintBin b o xs 
+  pprint = F.pprint
 
 instance PPrint a => PPrint (PVar a) where
   pprint (PV s _ _ xts)   = pprint s <+> hsep (pprint <$> dargs xts)
@@ -1382,15 +1356,11 @@
   pprint (RConc p)     = pprint p
   pprint k             = toFix k
  
-instance PPrint Reft where 
-  pprint r@(Reft (_,ras)) 
-    | isTauto r        = text "true"
-    | otherwise        = {- intersperse comma -} pprintBin trueD andD $ flattenRefas ras
+instance PPrint Reft where
+  pprint = F.pprint
 
 instance PPrint SortedReft where
-  pprint (RR so (Reft (v, ras))) 
-    = braces 
-    $ (pprint v) <+> (text ":") <+> (toFix so) <+> (text "|") <+> pprint ras
+  pprint = F.pprint
 
 ------------------------------------------------------------------------
 -- | Error Data Type ---------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/Visitors.hs b/src/Language/Haskell/Liquid/Visitors.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/Liquid/Visitors.hs
@@ -0,0 +1,142 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE TypeSynonymInstances      #-} 
+{-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE TupleSections             #-}
+{-# LANGUAGE DeriveDataTypeable        #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
+
+
+module Language.Haskell.Liquid.Visitors (
+  
+  -- * visitors 
+  CBVisitable (..) 
+
+  ) where
+
+
+import DataCon
+import Literal
+import CoreSyn
+
+import Var
+
+import Data.List (foldl', (\\), delete)
+
+import qualified Data.HashSet        as S
+import Language.Fixpoint.Misc
+import Language.Haskell.Liquid.GhcMisc ()
+
+
+------------------------------------------------------------------------------
+-------------------------------- A CoreBind Visitor --------------------------
+------------------------------------------------------------------------------
+
+-- TODO: syb-shrinkage
+
+class CBVisitable a where
+  freeVars :: S.HashSet Var -> a -> [Var]
+  readVars :: a -> [Var] 
+  letVars  :: a -> [Var] 
+  literals :: a -> [Literal]
+
+instance CBVisitable [CoreBind] where
+  freeVars env cbs = (sortNub xs) \\ ys 
+    where xs = concatMap (freeVars env) cbs 
+          ys = concatMap bindings cbs
+  
+  readVars = concatMap readVars
+  letVars  = concatMap letVars 
+  literals = concatMap literals
+
+instance CBVisitable CoreBind where
+  freeVars env (NonRec x e) = freeVars (extendEnv env [x]) e 
+  freeVars env (Rec xes)    = concatMap (freeVars env') es 
+                              where (xs,es) = unzip xes 
+                                    env'    = extendEnv env xs 
+
+  readVars (NonRec _ e)     = readVars e
+  readVars (Rec xes)        = concat [x `delete` nubReadVars e |(x, e) <- xes]
+    where nubReadVars = sortNub . readVars
+
+  letVars (NonRec x e)      = x : letVars e
+  letVars (Rec xes)         = xs ++ concatMap letVars es
+    where 
+      (xs, es)              = unzip xes
+
+  literals (NonRec _ e)      = literals e
+  literals (Rec xes)         = concatMap literals $ map snd xes
+
+instance CBVisitable (Expr Var) where
+  freeVars = exprFreeVars
+  readVars = exprReadVars
+  letVars  = exprLetVars
+  literals = exprLiterals
+
+exprFreeVars = go 
+  where 
+    go env (Var x)         = if x `S.member` env then [] else [x]  
+    go env (App e a)       = (go env e) ++ (go env a)
+    go env (Lam x e)       = go (extendEnv env [x]) e
+    go env (Let b e)       = (freeVars env b) ++ (go (extendEnv env (bindings b)) e)
+    go env (Tick _ e)      = go env e
+    go env (Cast e _)      = go env e
+    go env (Case e x _ cs) = (go env e) ++ (concatMap (freeVars (extendEnv env [x])) cs) 
+    go _   _               = []
+
+exprReadVars = go
+  where
+    go (Var x)             = [x]
+    go (App e a)           = concatMap go [e, a] 
+    go (Lam _ e)           = go e
+    go (Let b e)           = readVars b ++ go e 
+    go (Tick _ e)          = go e
+    go (Cast e _)          = go e
+    go (Case e _ _ cs)     = (go e) ++ (concatMap readVars cs) 
+    go _                   = []
+
+exprLetVars = go
+  where
+    go (Var _)             = []
+    go (App e a)           = concatMap go [e, a] 
+    go (Lam x e)           = x : go e
+    go (Let b e)           = letVars b ++ go e 
+    go (Tick _ e)          = go e
+    go (Cast e _)          = go e
+    go (Case e x _ cs)     = x : go e ++ concatMap letVars cs
+    go _                   = []
+
+exprLiterals = go
+  where
+    go (Lit l)             = [l]
+    go (App e a)           = concatMap go [e, a] 
+    go (Let b e)           = literals b ++ go e 
+    go (Lam _ e)           = go e
+    go (Tick _ e)          = go e
+    go (Cast e _)          = go e
+    go (Case e _ _ cs)     = (go e) ++ (concatMap literals cs) 
+    go _                   = []
+
+
+instance CBVisitable (Alt Var) where
+  freeVars env (a, xs, e) = freeVars env a ++ freeVars (extendEnv env xs) e
+  readVars (_,_, e)       = readVars e
+  letVars  (_,xs,e)       = xs ++ letVars e
+  literals (c,_, e)       = literals c ++ literals e
+
+
+instance CBVisitable AltCon where
+  freeVars _ (DataAlt dc) = dataConImplicitIds dc
+  freeVars _ _            = []
+  readVars _              = []
+  letVars  _              = []
+  literals (LitAlt l)     = [l]
+  literals _              = []
+
+
+
+extendEnv = foldl' (flip S.insert)
+
+bindings (NonRec x _) 
+  = [x]
+bindings (Rec  xes  ) 
+  = map fst xes
diff --git a/syntax/flycheck-liquid.el b/syntax/flycheck-liquid.el
deleted file mode 100644
--- a/syntax/flycheck-liquid.el
+++ /dev/null
@@ -1,86 +0,0 @@
-;;; flycheck-liquid.el --- A flycheck checker for Haskell using liquid (i.e. liquidhaskell)
-
-;; Modified from flycheck-hdevtools.el by Steve Purcell
-
-;; Author: Ranjit Jhala <jhala@cs.ucsd.edu>
-;; URL: https://github.com/ucsd-progsys/liquidhaskell/flycheck-liquid.el
-;; Keywords: convenience languages tools
-;; Package-Requires: ((flycheck "0.15"))
-;; Version: 20140801.00
-;; X-Original-Version: DEV
-
-;; This file is not part of GNU Emacs.
-
-;; This program is free software; you can redistribute it and/or modify
-;; it under the terms of the GNU General Public License as published by
-;; the Free Software Foundation, either version 3 of the License, or
-;; (at your option) any later version.
-
-;; This program is distributed in the hope that it will be useful,
-;; but WITHOUT ANY WARRANTY; without even the implied warranty of
-;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-;; GNU General Public License for more details.
-
-;; You should have received a copy of the GNU General Public License
-;; along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-;;; Commentary:
-
-;; Adds a Flycheck syntax checker for Haskell based on liquid-haskell.
-
-;;;; Setup
-
-;; (eval-after-load 'flycheck '(require 'flycheck-liquid))
-
-;;; Code:
-
-(require 'flycheck)
-
-(defvar flycheck-liquid-diffcheck nil
-  "Whether to run liquid in incremental-checking mode.")
-
-(flycheck-define-checker haskell-liquid
-  "A Haskell refinement type checker using liquidhaskell.
-
-See URL `https://github.com/ucsd-progsys/liquidhaskell'."
-  :command
-  ("liquid" (option-flag "--diffcheck" flycheck-liquid-diffcheck) source-inplace)
-  ;; ("~/bin/Checker.hs" source-inplace)
-  :error-patterns
-  (
-   (error line-start " " (file-name) ":" line ":" column ":"
-          (message
-	   (one-or-more " ") (one-or-more not-newline)
-	   (zero-or-more "\n"
-			 (one-or-more " ")
-			 (zero-or-more not-newline)))
-          line-end)
-
-   (error line-start " " (file-name) ":" line ":" column "-" (one-or-more digit) ":"
-	  (message
-	   (one-or-more " ") (one-or-more not-newline)
-	   (zero-or-more "\n"
-			 (one-or-more " ")
-			 (zero-or-more not-newline)))
-          line-end)
-
-   (error line-start " " (file-name) ":(" line "," column ")-(" (one-or-more digit) "," (one-or-more digit) "):"
-	  (message
-	   (one-or-more " ") (one-or-more not-newline)
-	   (zero-or-more "\n"
-			 (one-or-more " ")
-			 (zero-or-more not-newline)))
-          line-end)
-   )
-  :error-filter
-  (lambda (errors)
-    (-> errors
-      flycheck-dedent-error-messages
-      flycheck-sanitize-errors))
-  :modes (haskell-mode literate-haskell-mode)
-  :next-checkers ((warnings-only . haskell-hlint)))
-
-(add-to-list 'flycheck-checkers 'haskell-liquid)
-
-(provide 'flycheck-liquid)
-;;; flycheck-liquid.el ends here
diff --git a/syntax/haskell.vim b/syntax/haskell.vim
deleted file mode 100644
--- a/syntax/haskell.vim
+++ /dev/null
@@ -1,379 +0,0 @@
-" Vim syntax file
-"
-" Modification of vims Haskell syntax file:
-"   - match types using regular expression
-"   - highlight toplevel functions
-"   - use "syntax keyword" instead of "syntax match" where appropriate
-"   - functions and types in import and module declarations are matched
-"   - removed hs_highlight_more_types (just not needed anymore)
-"   - enable spell checking in comments and strings only
-"   - FFI highlighting
-"   - QuasiQuotation
-"   - top level Template Haskell slices
-"   - PackageImport
-"
-" TODO: find out which vim versions are still supported
-"
-" From Original file:
-" ===================
-"
-" Language:		    Haskell
-" Maintainer:		Haskell Cafe mailinglist <haskell-cafe@haskell.org>
-" Last Change:		2010 Feb 21
-" Original Author:	John Williams <jrw@pobox.com>
-"
-" Thanks to Ryan Crumley for suggestions and John Meacham for
-" pointing out bugs. Also thanks to Ian Lynagh and Donald Bruce Stewart
-" for providing the inspiration for the inclusion of the handling
-" of C preprocessor directives, and for pointing out a bug in the
-" end-of-line comment handling.
-"
-" Options-assign a value to these variables to turn the option on:
-"
-" hs_highlight_delimiters - Highlight delimiter characters--users
-"			    with a light-colored background will
-"			    probably want to turn this on.
-" hs_highlight_boolean - Treat True and False as keywords.
-" hs_highlight_types - Treat names of primitive types as keywords.
-" hs_highlight_debug - Highlight names of debugging functions.
-" hs_allow_hash_operator - Don't highlight seemingly incorrect C
-"			   preprocessor directives but assume them to be
-"			   operators
-" 
-" 
-
-if version < 600
-  syn clear
-elseif exists("b:current_syntax")
-  finish
-endif
-
-"syntax sync fromstart "mmhhhh.... is this really ok to do so?
-syntax sync linebreaks=15 minlines=50 maxlines=500
-
-syn match  hsSpecialChar	contained "\\\([0-9]\+\|o[0-7]\+\|x[0-9a-fA-F]\+\|[\"\\'&\\abfnrtv]\|^[A-Z^_\[\\\]]\)"
-syn match  hsSpecialChar	contained "\\\(NUL\|SOH\|STX\|ETX\|EOT\|ENQ\|ACK\|BEL\|BS\|HT\|LF\|VT\|FF\|CR\|SO\|SI\|DLE\|DC1\|DC2\|DC3\|DC4\|NAK\|SYN\|ETB\|CAN\|EM\|SUB\|ESC\|FS\|GS\|RS\|US\|SP\|DEL\)"
-syn match  hsSpecialCharError	contained "\\&\|'''\+"
-sy region  hsString		start=+"+  skip=+\\\\\|\\"+  end=+"+  contains=hsSpecialChar,@Spell
-sy match   hsCharacter		"[^a-zA-Z0-9_']'\([^\\]\|\\[^']\+\|\\'\)'"lc=1 contains=hsSpecialChar,hsSpecialCharError
-sy match   hsCharacter		"^'\([^\\]\|\\[^']\+\|\\'\)'" contains=hsSpecialChar,hsSpecialCharError
-
-" (Qualified) identifiers (no default highlighting)
-syn match ConId "\(\<[A-Z][a-zA-Z0-9_']*\.\)\=\<[A-Z][a-zA-Z0-9_']*\>"
-syn match VarId "\(\<[A-Z][a-zA-Z0-9_']*\.\)\=\<[a-z][a-zA-Z0-9_']*\>"
-
-" Infix operators--most punctuation characters and any (qualified) identifier
-" enclosed in `backquotes`. An operator starting with : is a constructor,
-" others are variables (e.g. functions).
-syn match hsVarSym "\(\<[A-Z][a-zA-Z0-9_']*\.\)\=[-!#$%&\*\+/<=>\?@\\^|~.][-!#$%&\*\+/<=>\?@\\^|~:.]*"
-syn match hsConSym "\(\<[A-Z][a-zA-Z0-9_']*\.\)\=:[-!#$%&\*\+./<=>\?@\\^|~:]*"
-syn match hsVarSym "`\(\<[A-Z][a-zA-Z0-9_']*\.\)\=[a-z][a-zA-Z0-9_']*`"
-syn match hsConSym "`\(\<[A-Z][a-zA-Z0-9_']*\.\)\=[A-Z][a-zA-Z0-9_']*`"
-
-" Toplevel Template Haskell support
-"sy match hsTHTopLevel "^[a-z]\(\(.\&[^=]\)\|\(\n[^a-zA-Z0-9]\)\)*"
-sy match hsTHIDTopLevel "^[a-z]\S*" 
-sy match hsTHTopLevel "^\$(\?" nextgroup=hsTHTopLevelName 
-sy match hsTHTopLevelName "[a-z]\S*" contained
-
-" Reserved symbols--cannot be overloaded.
-syn match hsDelimiter  "(\|)\|\[\|\]\|,\|;\|_\|{\|}"
-
-sy region hsInnerParen start="(" end=")" contained contains=hsInnerParen,hsConSym,hsType,hsVarSym
-sy region hs_InfixOpFunctionName start="^(" end=")\s*[^:`]\(\W\&\S\&[^'\"`()[\]{}@]\)\+"re=s
-    \ contained keepend contains=hsInnerParen,hs_HlInfixOp
-
-sy match hs_hlFunctionName "[a-z_]\(\S\&[^,\(\)\[\]]\)*" contained 
-sy match hs_FunctionName "^[a-z_]\(\S\&[^,\(\)\[\]]\)*" contained contains=hs_hlFunctionName
-sy match hs_HighliteInfixFunctionName "`[a-z_][^`]*`" contained
-sy match hs_InfixFunctionName "^\S[^=]*`[a-z_][^`]*`"me=e-1 contained contains=hs_HighliteInfixFunctionName,hsType,hsConSym,hsVarSym,hsString,hsCharacter
-sy match hs_HlInfixOp "\(\W\&\S\&[^`(){}'[\]]\)\+" contained contains=hsString
-sy match hs_InfixOpFunctionName "^\(\(\w\|[[\]{}]\)\+\|\(\".*\"\)\|\('.*'\)\)\s*[^:]=*\(\W\&\S\&[^='\"`()[\]{}@]\)\+"
-    \ contained contains=hs_HlInfixOp,hsCharacter
-
-sy match hs_OpFunctionName        "(\(\W\&[^(),\"]\)\+)" contained
-"sy region hs_Function start="^["'a-z_([{]" end="=\(\s\|\n\|\w\|[([]\)" keepend extend
-sy region hs_Function start="^["'a-zA-Z_([{]\(\(.\&[^=]\)\|\(\n\s\)\)*=" end="\(\s\|\n\|\w\|[([]\)" 
-        \ contains=hs_OpFunctionName,hs_InfixOpFunctionName,hs_InfixFunctionName,hs_FunctionName,hsType,hsConSym,hsVarSym,hsString,hsCharacter
-
-sy match hs_TypeOp "::"
-sy match hs_DeclareFunction "^[a-z_(]\S*\(\s\|\n\)*::" contains=hs_FunctionName,hs_OpFunctionName,hs_TypeOp
-
-" hi hs_TypeOp guibg=red
-
-" hi hs_InfixOpFunctionName guibg=yellow
-" hi hs_Function guibg=green
-" hi hs_InfixFunctionName guibg=red
-" hi hs_DeclareFunction guibg=red
-
-sy keyword hsStructure data family class where instance default deriving
-sy keyword hsTypedef type newtype
-
-sy keyword hsInfix infix infixl infixr
-sy keyword hsStatement  do case of let in
-sy keyword hsConditional if then else
-
-"if exists("hs_highlight_types")
-  " Primitive types from the standard prelude and libraries.
-  sy match hsType "\<[A-Z]\(\S\&[^,.]\)*\>"
-  sy match hsType "()"
-"endif
-
-" Not real keywords, but close.
-if exists("hs_highlight_boolean")
-  " Boolean constants from the standard prelude.
-  syn keyword hsBoolean True False
-endif
-
-syn region	hsPackageString	start=+L\="+ skip=+\\\\\|\\"\|\\$+ excludenl end=+"+ end='$' contains=cSpecial contained
-sy match   hsModuleName  excludenl "\([A-Z]\w*\.\?\)*" contained 
-
-sy match hsImport "\<import\>\s\+\(qualified\s\+\)\?\(\<\(\w\|\.\)*\>\)" 
-    \ contains=hsModuleName,hsImportLabel
-    \ nextgroup=hsImportParams,hsImportIllegal skipwhite
-sy keyword hsImportLabel import qualified contained
-
-sy match hsImportIllegal "\w\+" contained
-
-sy keyword hsAsLabel as contained
-sy keyword hsHidingLabel hiding contained
-
-sy match hsImportParams "as\s\+\(\w\+\)" contained
-    \ contains=hsModuleName,hsAsLabel
-    \ nextgroup=hsImportParams,hsImportIllegal skipwhite
-sy match hsImportParams "hiding" contained
-    \ contains=hsHidingLabel
-    \ nextgroup=hsImportParams,hsImportIllegal skipwhite 
-sy region hsImportParams start="(" end=")" contained
-    \ contains=hsBlockComment,hsLineComment, hsType,hsDelimTypeExport,hs_hlFunctionName,hs_OpFunctionName
-    \ nextgroup=hsImportIllegal skipwhite
-
-" hi hsImport guibg=red
-"hi hsImportParams guibg=bg
-"hi hsImportIllegal guibg=bg
-"hi hsModuleName guibg=bg
-
-"sy match hsImport		"\<import\>\(.\|[^(]\)*\((.*)\)\?" 
-"         \ contains=hsPackageString,hsImportLabel,hsImportMod,hsModuleName,hsImportList
-"sy keyword hsImportLabel import contained
-"sy keyword hsImportMod		as qualified hiding contained
-"sy region hsImportListInner start="(" end=")" contained keepend extend contains=hs_OpFunctionName
-"sy region  hsImportList matchgroup=hsImportListParens start="("rs=s+1 end=")"re=e-1
-"        \ contained 
-"        \ keepend extend
-"        \ contains=hsType,hsLineComment,hsBlockComment,hs_hlFunctionName,hsImportListInner
-
-
-
-" new module highlighting
-syn region hsDelimTypeExport start="\<[A-Z]\(\S\&[^,.]\)*\>(" end=")" contained
-   \ contains=hsType
-
-sy keyword hsExportModuleLabel module contained
-sy match hsExportModule "\<module\>\(\s\|\t\|\n\)*\([A-Z]\w*\.\?\)*" contained contains=hsExportModuleLabel,hsModuleName
-
-sy keyword hsModuleStartLabel module contained
-sy keyword hsModuleWhereLabel where contained
-
-syn match hsModuleStart "^module\(\s\|\n\)*\(\<\(\w\|\.\)*\>\)\(\s\|\n\)*" 
-  \ contains=hsModuleStartLabel,hsModuleName
-  \ nextgroup=hsModuleCommentA,hsModuleExports,hsModuleWhereLabel
-
-syn region hsModuleCommentA start="{-" end="-}"
-  \ contains=hsModuleCommentA,hsCommentTodo,@Spell contained
-  \ nextgroup=hsModuleCommentA,hsModuleExports,hsModuleWhereLabel skipwhite skipnl
-
-syn match hsModuleCommentA "--.*\n"
-  \ contains=hsCommentTodo,@Spell contained
-  \ nextgroup=hsModuleCommentA,hsModuleExports,hsModuleWhereLabel skipwhite skipnl
-
-syn region hsModuleExports start="(" end=")" contained
-   \ nextgroup=hsModuleCommentB,hsModuleWhereLabel skipwhite skipnl
-   \ contains=hsBlockComment,hsLineComment,hsType,hsDelimTypeExport,hs_hlFunctionName,hs_OpFunctionName,hsExportModule
-
-syn match hsModuleCommentB "--.*\n"
-  \ contains=hsCommentTodo,@Spell contained
-  \ nextgroup=hsModuleCommentB,hsModuleWhereLabel skipwhite skipnl
-
-syn region hsModuleCommentB start="{-" end="-}"
-   \ contains=hsModuleCommentB,hsCommentTodo,@Spell contained
-   \ nextgroup=hsModuleCommentB,hsModuleWhereLabel skipwhite skipnl
-" end module highlighting
-
-" FFI support
-sy keyword hsFFIForeign foreign contained
-"sy keyword hsFFIImportExport import export contained
-sy keyword hsFFIImportExport export contained
-sy keyword hsFFICallConvention ccall stdcall contained
-sy keyword hsFFISafety safe unsafe contained
-sy region  hsFFIString		start=+"+  skip=+\\\\\|\\"+  end=+"+  contained contains=hsSpecialChar
-sy match hsFFI excludenl "\<foreign\>\(.\&[^\"]\)*\"\(.\)*\"\(\s\|\n\)*\(.\)*::"
-  \ keepend
-  \ contains=hsFFIForeign,hsFFIImportExport,hsFFICallConvention,hsFFISafety,hsFFIString,hs_OpFunctionName,hs_hlFunctionName
-
-
-sy match   hsNumber		"\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>"
-sy match   hsFloat		"\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>"
-
-" Comments
-sy keyword hsCommentTodo    TODO FIXME XXX TBD contained
-sy match   hsLineComment      "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=hsCommentTodo,@Spell
-sy region  hsBlockComment     start="{-"  end="-}" contains=hsBlockComment,hsCommentTodo,@Spell
-sy region  hsPragma	       start="{-#" end="#-}"
-
-" Liquid Types
-sy region  hsLiquidAnnot   start="{-@\s*" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC
-sy region  hsLiquidAnnot   start="{-@\s*\<invariant\>" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC
-sy region  hsLiquidAnnot   start="{-@\s*\<predicate\>" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC
-sy region  hsLiquidAnnot   start="{-@\s*\<assert\>" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC
-sy region  hsLiquidAnnot   start="{-@\s*\<type\>" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC
-sy region  hsLiquidAnnot   start="{-@\s*\<data\>" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC
-sy keyword hsLiquidKeyword  assume assert invariant predicate type data contained
-sy region  hsLiquidReftA   start="{\(\s\|\w\)" end=":" contained
-sy region  hsLiquidReftB   start="|" end="}" contained
-sy match   hsLiquidReftC   "\w*:" contained
-
-" QuasiQuotation
-sy region hsQQ start="\[\$" end="|\]"me=e-2 keepend contains=hsQQVarID,hsQQContent nextgroup=hsQQEnd
-sy region hsQQNew start="\[\(.\&[^|]\&\S\)*|" end="|\]"me=e-2 keepend contains=hsQQVarIDNew,hsQQContent nextgroup=hsQQEnd
-sy match hsQQContent ".*" contained
-sy match hsQQEnd "|\]" contained
-sy match hsQQVarID "\[\$\(.\&[^|]\)*|" contained
-sy match hsQQVarIDNew "\[\(.\&[^|]\)*|" contained
-
-if exists("hs_highlight_debug")
-  " Debugging functions from the standard prelude.
-  syn keyword hsDebug undefined error trace
-endif
-
-
-" C Preprocessor directives. Shamelessly ripped from c.vim and trimmed
-" First, see whether to flag directive-like lines or not
-if (!exists("hs_allow_hash_operator"))
-    syn match	cError		display "^\s*\(%:\|#\).*$"
-endif
-" Accept %: for # (C99)
-syn region	cPreCondit	start="^\s*\(%:\|#\)\s*\(if\|ifdef\|ifndef\|elif\)\>" skip="\\$" end="$" end="//"me=s-1 contains=cComment,cCppString,cCommentError
-syn match	cPreCondit	display "^\s*\(%:\|#\)\s*\(else\|endif\)\>"
-syn region	cCppOut		start="^\s*\(%:\|#\)\s*if\s\+0\+\>" end=".\@=\|$" contains=cCppOut2
-syn region	cCppOut2	contained start="0" end="^\s*\(%:\|#\)\s*\(endif\>\|else\>\|elif\>\)" contains=cCppSkip
-syn region	cCppSkip	contained start="^\s*\(%:\|#\)\s*\(if\>\|ifdef\>\|ifndef\>\)" skip="\\$" end="^\s*\(%:\|#\)\s*endif\>" contains=cCppSkip
-syn region	cIncluded	display contained start=+"+ skip=+\\\\\|\\"+ end=+"+
-syn match	cIncluded	display contained "<[^>]*>"
-syn match	cInclude	display "^\s*\(%:\|#\)\s*include\>\s*["<]" contains=cIncluded
-syn cluster	cPreProcGroup	contains=cPreCondit,cIncluded,cInclude,cDefine,cCppOut,cCppOut2,cCppSkip,cCommentStartError
-syn region	cDefine		matchgroup=cPreCondit start="^\s*\(%:\|#\)\s*\(define\|undef\)\>" skip="\\$" end="$"
-syn region	cPreProc	matchgroup=cPreCondit start="^\s*\(%:\|#\)\s*\(pragma\>\|line\>\|warning\>\|warn\>\|error\>\)" skip="\\$" end="$" keepend
-
-syn region	cComment	matchgroup=cCommentStart start="/\*" end="\*/" contains=cCommentStartError,cSpaceError contained
-syntax match	cCommentError	display "\*/" contained
-syntax match	cCommentStartError display "/\*"me=e-1 contained
-syn region	cCppString	start=+L\="+ skip=+\\\\\|\\"\|\\$+ excludenl end=+"+ end='$' contains=cSpecial contained
-
-
-if version >= 508 || !exists("did_hs_syntax_inits")
-  if version < 508
-    let did_hs_syntax_inits = 1
-    command -nargs=+ HiLink hi link <args>
-  else
-    command -nargs=+ HiLink hi def link <args>
-  endif
-
-  HiLink hs_hlFunctionName    Function
-  HiLink hs_HighliteInfixFunctionName Function
-  HiLink hs_HlInfixOp       Function
-  HiLink hs_OpFunctionName  Function
-  HiLink hsTypedef          Typedef
-  HiLink hsVarSym           hsOperator
-  HiLink hsConSym           hsOperator
-  if exists("hs_highlight_delimiters")
-    " Some people find this highlighting distracting.
-	HiLink hsDelimiter        Delimiter
-  endif
-
-  HiLink hsModuleStartLabel Structure
-  HiLink hsExportModuleLabel Keyword
-  HiLink hsModuleWhereLabel Structure
-  HiLink hsModuleName       Normal
-  
-  HiLink hsImportIllegal    Error
-  HiLink hsAsLabel          hsImportLabel
-  HiLink hsHidingLabel      hsImportLabel
-  HiLink hsImportLabel      Include
-  HiLink hsImportMod        Include
-  HiLink hsPackageString    hsString
-
-  HiLink hsOperator         Operator
-
-  HiLink hsInfix            Keyword
-  HiLink hsStructure        Structure
-  HiLink hsStatement        Statement
-  HiLink hsConditional      Conditional
-
-  HiLink hsSpecialCharError Error
-  HiLink hsSpecialChar      SpecialChar
-  HiLink hsString           String
-  HiLink hsFFIString        String
-  HiLink hsCharacter        Character
-  HiLink hsNumber           Number
-  HiLink hsFloat            Float
-
-  HiLink hsLiterateComment		  hsComment
-  HiLink hsBlockComment     hsComment
-  HiLink hsLineComment      hsComment
-  HiLink hsModuleCommentA   hsComment
-  HiLink hsModuleCommentB   hsComment
-  HiLink hsComment          Comment
-  HiLink hsCommentTodo      Todo
-  HiLink hsPragma           SpecialComment
-  HiLink hsBoolean			Boolean
-
-  " Liquid Types
-  HiLink hsLiquidAnnot      SpecialComment  "String
-  HiLink hsLiquidKeyword    Operator        "Float
-  HiLink hsLiquidReftA      Include
-  HiLink hsLiquidReftB      Include
-  HiLink hsLiquidReftC      Include
-  
-  if exists("hs_highlight_types")
-      HiLink hsDelimTypeExport  hsType
-      HiLink hsType             Type
-  endif
-
-  HiLink hsDebug            Debug
-
-  HiLink hs_TypeOp          hsOperator
-
-  HiLink cCppString         hsString
-  HiLink cCommentStart      hsComment
-  HiLink cCommentError      hsError
-  HiLink cCommentStartError hsError
-  HiLink cInclude           Include
-  HiLink cPreProc           PreProc
-  HiLink cDefine            Macro
-  HiLink cIncluded          hsString
-  HiLink cError             Error
-  HiLink cPreCondit         PreCondit
-  HiLink cComment           Comment
-  HiLink cCppSkip           cCppOut
-  HiLink cCppOut2           cCppOut
-  HiLink cCppOut            Comment
-
-  HiLink hsFFIForeign       Keyword
-  HiLink hsFFIImportExport  Structure
-  HiLink hsFFICallConvention Keyword
-  HiLink hsFFISafety         Keyword
-
-  HiLink hsTHIDTopLevel   Macro
-  HiLink hsTHTopLevelName Macro
-
-  HiLink hsQQVarID Keyword
-  HiLink hsQQVarIDNew Keyword
-  HiLink hsQQEnd   Keyword
-  HiLink hsQQContent String
-
-  delcommand HiLink
-endif
-
-let b:current_syntax = "haskell"
-
diff --git a/syntax/liquid-tip.el b/syntax/liquid-tip.el
deleted file mode 100644
--- a/syntax/liquid-tip.el
+++ /dev/null
@@ -1,270 +0,0 @@
-;;; liquid-tip.el --- show inferred liquid-types
-
-;; Copyright (C) 2014 by Ranjit Jhala 
-
-;; Author: Ranjit Jhala <jhala@cs.ucsd.edu>
-;; Version: 0.0.1
-;; Package-Requires: ((flycheck "0.13") (dash "1.2") (emacs "24.1") (pos-tip "0.5.0"))
-;;; License:
-;; This program is free software: you can redistribute it and/or modify
-;; it under the terms of the GNU General Public License as published by
-;; the Free Software Foundation, either version 3 of the License, or
-;; (at your option) any later version.
-;;
-;; This program is distributed in the hope that it will be useful,
-;; but WITHOUT ANY WARRANTY; without even the implied warranty of
-;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-;; GNU General Public License for more details.
-;;
-;; You should have received a copy of the GNU General Public License
-;; along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-;;; Commentary:
-;; see https://github.com/ucsd-progsys/liquidhaskell#emacs
-
-;;; Code:
-(eval-when-compile (require 'cl))
-(require 'auto-complete)
-(require 'json)
-(require 'pos-tip nil t)
-(require 'thingatpt)
-(require 'button-lock)
-(require 'hdevtools)
-
-;; ------------------------------------------------------------------------
-;; A structure to represent positions 
-;; ------------------------------------------------------------------------
-
-(cl-defstruct position file row col)
-
-;; ------------------------------------------------------------------------
-;; Utilities for reading json/files
-;; ------------------------------------------------------------------------
-
-(defun get-string-from-file (filePath)
-  "Return filePath's file content."
-  (with-temp-buffer
-    (insert-file-contents filePath)
-    (buffer-string)))
-
-(defun get-json-from-file (filePath)
-  "Return json object from filePath's content"
-  (if (file-exists-p filePath)
-      (let* ((json-key-type 'string)
-	     (str (get-string-from-file filePath)))
-	(json-read-from-string str))
-      nil))
-
-;; ------------------------------------------------------------------------
-;; get/set annot information 
-;; ------------------------------------------------------------------------
-
-(defun gethash-nil (key table) 
-  (if table 
-      (gethash key table nil)
-      nil))
-
-(defun liquid-annot-filepath-prefix (mode)
-  "Return prefix of annotation file using mode"
-  (if (equal mode 'flycheck)
-      "flycheck_"
-      nil))
-
-;; (liquid-annot 'flycheck "/path/to/file.hs") 
-;;    ==> "/path/to/.liquid/flycheck_file.hs.json"
-;;
-;; (liquid-annot nil       "/path/to/file.hs") 
-;;    ==> "/path/to/.liquid/file.hs.json"
-
-(defun liquid-annot-filepath (mode file)
-  "Return name of annotation file"
-  (let* ((dir    (file-name-directory file))
-	 (name   (file-name-nondirectory file))
-	 (prefix (liquid-annot-filepath-prefix mode)))
-    (concat dir ".liquid/" prefix name ".json")))
-
-(defvar liquid-annot-table (make-hash-table :test 'equal))
-
-;; API
-(defun liquid-annot-set (file mode)
-  "Load information for file into liquid-annot-table"
-  (let* ((file-path        (liquid-annot-filepath mode file))
-	 (json-object-type 'hash-table)
-	 (file-info        (get-json-from-file file-path)))
-    (if file-info (puthash file file-info liquid-annot-table))))
-
-;; API
-(defun liquid-annot-get (file row col)
-  "Get annotation for identifier at row, col in file"
-  (let* ((table (gethash-nil file liquid-annot-table))
-	 (r     (format "%d" row))
-	 (c     (format "%d" col))
-	 (tys   (gethash-nil "types" table))
-	 (ro    (gethash-nil r tys)))
-    (gethash-nil "ann" (gethash-nil c ro))))
-
-;; ------------------------------------------------------------------------
-;; Display Annot in Tooltip 
-;; ------------------------------------------------------------------------
-
-;; For simple, ascii popups, use:
-;;    (setq liquid-tip-mode 'ascii) 
-;;
-;; For emacs', balloon based popups, use:
-;;    (setq liquid-tip-mode 'balloon)
-
-(defvar liquid-tip-mode 'balloon)
-
-(defun pad-line (str)
-  (concat " " str " "))
-
-(defun popup-tip-pad (text)
-  (let* ((lines     (split-string text "\n"))
-         (pad-lines (mapcar 'pad-line lines))
-	 (pad-text  (concat "\n" (mapconcat 'identity pad-lines "\n") "\n")))
-    (popup-tip pad-text)))
-
-(defun liquid-tip-popup-balloon (text)
-  "Display text in a balloon popup"
-  (if (and (functionp 'ac-quick-help-use-pos-tip-p)
-           (ac-quick-help-use-pos-tip-p))
-      (pos-tip-show text 'popup-tip-face nil nil 300 popup-tip-max-width)
-    (popup-tip-pad text)))
-
-(defun liquid-tip-popup-ascii (text)
- "Display text in ascii popup"
-  (popup-tip-pad text))
-
-(defun liquid-tip-popup (text)
-  (if (equal liquid-tip-mode 'ascii)
-      (liquid-tip-popup-ascii   text)
-      (liquid-tip-popup-balloon text)))
-
-;; -- Compute range ---------------------------------------------------------
-
-(defvar liquid-id-regexp 
-  (rx (one-or-more (not (in " \n\t()[]{}")))))
-
-(defun liquid-splitters () 
-  '( ?\s  ?\t ?\n ?\( ?\) ?\[ ?\] ))
-
-(defun liquid-is-split (c)
-  "Is the character `c` a splitter?"
-  (member c (liquid-splitters)))
-
-(defun liquid-id-start-pos (low p)
-  "Find the largest position less than `p` that is a splitter"
-  (let* ((ch (char-before p)))
-     (if (or (<= p low) (liquid-is-split ch)) 
-	 p 
-         (liquid-id-start-pos low (- p 1)))))
-
-
-(defun column-number-at-pos (pos)
-  "Find the column of position pos"
-  (+ (- pos (line-beginning-position)) 1))
-
-(defun start-column-number-at-pos (pos)
-  "Find the starting column of identifier at pos"
-     (let* ((low   (line-beginning-position))
-	    (start (liquid-id-start-pos low pos)))
-       (column-number-at-pos start)))
-
-(defsubst liquid-get-position ()
-  (save-excursion
-    (widen)
-    (make-position
-     :file (expand-file-name (buffer-file-name))
-     :row  (line-number-at-pos)
-     :col  (start-column-number-at-pos (point)))))
-
-(defun position-string (pos)
-  "position -> string"
-  (format "(%s, %s) in [%s]" 
-	  (position-row pos) 
-	  (position-col pos)
-	  (position-file pos)))
-
-;; DEBUG (defun liquid-annot-at-pos-0 (pos)
-;; DEBUG   "Info to display: just the file/line/constant string"
-;; DEBUG   (let* ((info  (format "hello!")))
-;; DEBUG     (format "the information at %s is %s" 
-;; DEBUG 	    (position-string pos)
-;; DEBUG 	    info)))
-
-;; DEBUG (defun liquid-annot-at-pos-1 (pos)
-;; DEBUG   "Info to display: the identifier at the position or NONE" 
-;; DEBUG   (let* ((ident (liquid-ident-at-pos pos)))
-;; DEBUG     (format "the identifier at %s is %s" 
-;; DEBUG 	    (position-string pos) 
-;; DEBUG 	    ident)))
-
-(defun liquid-ident-at-pos (pos)
-  "Return the identifier at a given position"
-  (thing-at-point 'word))
-
-(defun liquid-annot-at-pos-2 (pos)
-  "Info to display: type annotation for the identifier at the position or NONE" 
-  (let* ((file (position-file pos))
-	 (row  (position-row  pos))
-	 (col  (position-col  pos)))
-    (liquid-annot-get file row col)))
-
-(defun liquid-annot-at-pos (pos)
-  "Determine info to display"
-  (liquid-annot-at-pos-2 pos))
-
-;;;###autoload
-(defun liquid-tip-show ()
-  "Popup help about anything at point."
-  (interactive)
-  (let* ((pos    (liquid-get-position))
-         (ident  (liquid-ident-at-pos pos))
-         (sorry  (format "No information for %s" ident))
-         (annot  (liquid-annot-at-pos pos)))
-    (if annot 
-        (liquid-tip-popup annot)
-      (hdevtools/show-type-info)
-      ;; (liquid-tip-popup sorry)
-      )))
-
-
-;;;###autoload
-(defun liquid-tip-init (&optional mode)
-  "Initialize liquid-tip by making all identifiers buttons"
-  (interactive)
-  (progn (if mode (setq liquid-tip-mode mode))
-	 (button-lock-mode 1)
-	 (button-lock-set-button liquid-id-regexp 'liquid-tip-show :mouse-face nil :face nil :face-policy nil :mouse-binding 'double-mouse-1)
-	 ))
-
-;;;###autoload
-(defun liquid-tip-update (mode)
-  "Update liquid-annot-table by reloading annot file for buffer"
-  (interactive)
-  (let* ((pos  (liquid-get-position))
-	 (file (position-file pos)))
-    (liquid-annot-set file mode)))
-
-
-;; For simple, ascii popups, use:
-;;    (liquid-tip-init 'ascii) 
-;; For emacs', balloon based popups, use:
-;;    (liquid-tip-init 'balloon)
-;; or just
-;;    (liquid-tip-init 'balloon)
-
-;; Reload annotations after check
-(add-hook 'flycheck-after-syntax-check-hook
-	  (lambda () (liquid-tip-update 'flycheck)))
-
-
-
-(provide 'liquid-tip)
-
-;; Local Variables:
-;; coding: utf-8
-;; mode: emacs-lisp
-;; End:
-
-;;; liquid-tip.el ends here
diff --git a/syntax/liquid.vim b/syntax/liquid.vim
deleted file mode 100644
--- a/syntax/liquid.vim
+++ /dev/null
@@ -1,47 +0,0 @@
-"============================================================================
-"File:        liquid.vim
-"Description: LiquidHaskell checking plugin for syntastic.vim
-"Maintainer:  Ranjit Jhala <jhala at cs dot ucsd dot edu>
-"License:     BSD
-"============================================================================
-
-if exists('g:loaded_syntastic_haskell_liquid_checker')
-    finish
-endif
-let g:loaded_syntastic_haskell_liquid_checker = 1
-
-
-let s:save_cpo = &cpo
-set cpo&vim
-
-function! SyntaxCheckers_haskell_liquid_GetLocList() dict
-    let makeprg = self.makeprgBuild({
-        \ 'fname'    : syntastic#util#shexpand('%:p')})
-
-    let errorformat =
-        \ '%E%f:%l:%v: Error: %m,' .
-        \ '%E%f:%l:%c-%*[0-9]: Error: %m,' .
-        \ '%W%f:%l:%v: Warning: %m,' .
-        \ '%C%m'
-
-    let retVals = SyntasticMake({
-        \ 'makeprg': makeprg,
-        \ 'errorformat': errorformat,
-        \ 'defaults': {'vcol': 1},
-        \ 'postprocess': ['compressWhitespace'] })
-
-    if exists("g:loaded_vim_annotations")
-      call annotations#LoadAnnsDefault()
-    endif
-
-    return retVals
-endfunction
-
-call g:SyntasticRegistry.CreateAndRegisterChecker({
-    \ 'filetype': 'haskell',
-    \ 'name': 'liquid'})
-
-let &cpo = s:save_cpo
-unlet s:save_cpo
-
-" vim: set et sts=4 sw=4:
diff --git a/tests/test.hs b/tests/test.hs
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -51,9 +51,8 @@
       testGroup "pos"         <$> dirTests "tests/pos"                            []           ExitSuccess
     , testGroup "neg"         <$> dirTests "tests/neg"                            []           (ExitFailure 1)
     , testGroup "crash"       <$> dirTests "tests/crash"                          []           (ExitFailure 2) 
-    , testGroup "parserpos"   <$> dirTests "tests/parser/pos"                    []           ExitSuccess
-    , testGroup "errorcrash"  <$> dirTests "tests/error_messages/crash"           []           (ExitFailure 2)
-    , testGroup "errorpos"    <$> dirTests "tests/parser/pos"                     []           ExitSuccess
+    , testGroup "parser/pos"  <$> dirTests "tests/parser/pos"                     []           ExitSuccess
+    , testGroup "error/crash" <$> dirTests "tests/error_messages/crash"           []           (ExitFailure 2)
    ]
 
 benchTests
@@ -63,7 +62,8 @@
     , testGroup "esop"        <$> dirTests "benchmarks/esop2013-submission"       ["Base0.hs"] ExitSuccess
     , testGroup "vect-algs"   <$> dirTests "benchmarks/vector-algorithms-0.5.4.2" []           ExitSuccess
     , testGroup "hscolour"    <$> dirTests "benchmarks/hscolour-1.20.0.0"         []           ExitSuccess
-
+    , testGroup "icfp_pos"    <$> dirTests "benchmarks/icfp15/pos"                []           ExitSuccess
+    , testGroup "icfp_neg"    <$> dirTests "benchmarks/icfp15/neg"                ["RIO.hs", "DataBase.hs", "DataBase.Domain.hs"]           (ExitFailure 1)
     ]
 
 ---------------------------------------------------------------------------