diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,24 +1,30 @@
-(*
- * Copyright © 1990-2009 The Regents of the University of California. All rights reserved. 
- *
- * Permission is hereby granted, without written agreement and without 
- * license or royalty fees, to use, copy, modify, and distribute this 
- * software and its documentation for any purpose, provided that the 
- * above copyright notice and the following two paragraphs appear in 
- * all copies of this software. 
- * 
- * IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY 
- * FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES 
- * ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN 
- * IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY 
- * OF SUCH DAMAGE. 
- * 
- * THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, 
- * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY 
- * AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 
- * ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION 
- * TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
- *
- *)
+Copyright (c) 2013-2014, Ranjit Jhala
 
+All rights reserved.
 
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Ranjit Jhala nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Liquid.hs b/Liquid.hs
--- a/Liquid.hs
+++ b/Liquid.hs
@@ -25,9 +25,11 @@
 import           Language.Haskell.Liquid.Annotate (mkOutput)
 
 main :: IO b
-main = do cfg0    <- getOpts
-          res     <- mconcat <$> mapM (checkOne cfg0) (files cfg0)
-          exitWith $ resultExit $ o_result res
+main = do cfg0     <- getOpts
+          res      <- mconcat <$> mapM (checkOne cfg0) (files cfg0)
+          let ecode = resultExit $  {- traceShow "RESULT" $ -} o_result res
+          -- putStrLn  $ "ExitCode: " ++ show ecode
+          exitWith ecode
 
 checkOne :: Config -> FilePath -> IO (Output Doc)
 checkOne cfg0 t = getGhcInfo cfg0 t >>= either errOut (liquidOne t)
@@ -81,11 +83,11 @@
 solveCs cfg target cgi info dc 
   = do (r, sol) <- solve fx target (hqFiles info) (cgInfoFInfo cgi)
        let names = checkedNames dc
-       let warns = logWarn cgi
+       let warns = logErrors cgi
        let annm  = annotMap cgi
        let res   = ferr sol r
        let out0  = mkOutput cfg res sol annm
-       return    $ out0 { o_vars = names } { o_warns  = warns} { o_result = res }
+       return    $ out0 { o_vars = names } { o_errors  = warns} { o_result = res }
     where 
        fx        = def { FC.solver = smtsolver cfg, FC.real = real cfg }
        ferr s r  = fmap (tidyError s) $ result $ sinfo <$> r
diff --git a/include/Data/Set.spec b/include/Data/Set.spec
--- a/include/Data/Set.spec
+++ b/include/Data/Set.spec
@@ -13,13 +13,17 @@
 measure Set_cap  :: (Data.Set.Set a) -> (Data.Set.Set a) -> (Data.Set.Set a)
 
 -- | difference
-measure Set_dif  :: (Data.Set.Set a) -> (Data.Set.Set a) -> (Data.Set.Set a)
+measure Set_dif   :: (Data.Set.Set a) -> (Data.Set.Set a) -> (Data.Set.Set a)
 
 -- | singleton
-measure Set_sng  :: a -> (Data.Set.Set a)
+measure Set_sng   :: a -> (Data.Set.Set a)
 
 -- | emptiness test
-measure Set_emp  :: (Data.Set.Set a) -> Prop
+measure Set_emp   :: (Data.Set.Set a) -> Prop
+
+-- | empty set 
+measure Set_empty :: forall a. GHC.Types.Int -> (Data.Set.Set a)
+
 
 -- | membership test
 measure Set_mem  :: a -> (Data.Set.Set a) -> Prop
diff --git a/include/Data/Vector.spec b/include/Data/Vector.spec
--- a/include/Data/Vector.spec
+++ b/include/Data/Vector.spec
@@ -3,12 +3,13 @@
 import GHC.Base
 
 measure vlen    :: forall a. (Data.Vector.Vector a) -> Int
--- measure vlen    :: forall a. a -> Int
 
-invariant       {v: Data.Vector.Vector a | (vlen v) >= 0 } 
+invariant       {v: Data.Vector.Vector a | 0 <= vlen v } 
 
-assume !        :: forall a. x:(Data.Vector.Vector a) -> vec:{v: Int | ((0 <= v) && (v < (vlen x))) } -> a 
+assume !         :: forall a. x:(Data.Vector.Vector a) -> vec:{v:Nat | v < vlen x } -> a 
 
-assume fromList :: forall a. x:[a] -> {v: Data.Vector.Vector a  | (vlen v) = (len x) }
+assume fromList  :: forall a. x:[a] -> {v: Data.Vector.Vector a  | vlen v = len x }
 
-assume length   :: forall a. x:(Data.Vector.Vector a) -> {v: Int | (v = (vlen x) && v >= 0) }
+assume length    :: forall a. x:(Data.Vector.Vector a) -> {v : Nat | v = vlen x }
+
+assume replicate :: n:Nat -> a -> {v:Data.Vector.Vector a | vlen v = n} 
diff --git a/include/GHC/Real.spec b/include/GHC/Real.spec
--- a/include/GHC/Real.spec
+++ b/include/GHC/Real.spec
@@ -3,19 +3,18 @@
 
 GHC.Real.fromIntegral    :: (GHC.Real.Integral a, GHC.Num.Num b) => x:a -> {v:b|v=x}
 
-
 class (GHC.Real.Real a, GHC.Enum.Enum a) => GHC.Real.Integral a where
-  GHC.Real.quot :: a -> a -> a
-  GHC.Real.rem :: a -> a -> a
-  GHC.Real.mod :: x:a -> y:a -> {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))}
-  GHC.Real.div :: x:a -> y:a -> {v:a | ((v = (x / y))
+  GHC.Real.quot :: a -> {v:a | v /= 0} -> a
+  GHC.Real.rem :: a -> {v:a | v /= 0} -> a
+  GHC.Real.mod :: x:a -> y:{v:a | v /= 0} -> {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))}
+  GHC.Real.div :: x:a -> y:{v:a | v /= 0} -> {v:a | ((v = (x / y))
                                      && (((x>=0) && (y>=0)) => (v>=0))
                                      && (((x>=0) && (y>=1)) => (v<=x))) }
-  GHC.Real.quotRem :: x:a -> y:a -> ({v:a | ((v = (x / y))
+  GHC.Real.quotRem :: x:a -> y:{v:a | v /= 0} -> ({v:a | ((v = (x / y))
                                           && (((x>=0) && (y>=0)) => (v>=0))
                                           && (((x>=0) && (y>=1)) => (v<=x)))}
                                     ,{v:a | ((v >= 0) && (v < y))})
-  GHC.Real.divMod :: a -> a -> (a, a)
+  GHC.Real.divMod :: a -> {v:a | v /= 0} -> (a, a)
   GHC.Real.toInteger :: x:a -> {v:GHC.Integer.Type.Integer | v = x}
 
 -- fixpoint can't handle (x mod y), only (x mod c) so we need to be more clever here
diff --git a/include/Language/Haskell/Liquid/List.hs b/include/Language/Haskell/Liquid/List.hs
--- a/include/Language/Haskell/Liquid/List.hs
+++ b/include/Language/Haskell/Liquid/List.hs
@@ -2,7 +2,6 @@
 
 import Data.List hiding (transpose)
 
-{-# ANN transpose "forall a. n:Int -> xs:[{v:[a]|len(v) = n}] -> {v:[[a]] | len(v) = n}" #-}
 transpose                  :: Int -> [[a]] -> [[a]]
 transpose n []             = []
 transpose n ([]   : xss)   = transpose n xss
diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal
--- a/liquidhaskell.cabal
+++ b/liquidhaskell.cabal
@@ -1,11 +1,11 @@
 Name:                liquidhaskell
-Version:             0.2.0.0
-Copyright:           2010-13 Ranjit Jhala, University of California, San Diego.
+Version:             0.2.1.0
+Copyright:           2010-15 Ranjit Jhala, University of California, San Diego.
 build-type:          Simple
 Synopsis:            Liquid Types for Haskell 
 Description:         Liquid Types for Haskell.
 Homepage:            http://goto.ucsd.edu/liquidhaskell
-License:             GPL
+License:             BSD3
 License-file:        LICENSE
 Author:              Ranjit Jhala, Niki Vazou, Eric Seidel
 Maintainer:          Ranjit Jhala <jhala@cs.ucsd.edu>
@@ -32,6 +32,8 @@
           , include/Language/Haskell/Liquid/*.pred
           , include/System/*.spec
           , syntax/liquid.css
+          , syntax/*.el
+          , syntax/*.vim
 
 Source-Repository head
   Type:        git
@@ -65,7 +67,7 @@
                , syb
                , text
                , vector
-               , liquid-fixpoint >= 0.2
+               , liquid-fixpoint >= 0.2.1.0
                , hashable
                , unordered-containers
                , aeson
@@ -139,12 +141,11 @@
                 , process
                 , syb
                 , text
-                , unix
                 , intern
                 , vector
                 , hashable
                 , unordered-containers
-                , liquid-fixpoint >= 0.2
+                , liquid-fixpoint >= 0.2.1.0
                 , aeson
                 , bytestring
                 , fingertree
@@ -172,6 +173,7 @@
                     Language.Haskell.Liquid.CmdLine, 
                     Language.Haskell.Liquid.GhcMisc, 
                     Language.Haskell.Liquid.Misc, 
+                    Language.Haskell.Liquid.CoreToLogic,
                     Language.Haskell.Liquid.Qualifier, 
                     Language.Haskell.Liquid.TransformRec, 
                     Language.Haskell.Liquid.Tidy, 
@@ -211,9 +213,8 @@
                      filepath,
                      process,
                      tagged,
-                     unix,
                      liquidhaskell,
-                     optparse-applicative < 0.10,
-                     tasty >= 0.8,
-                     tasty-hunit >= 0.8,
+                     optparse-applicative == 0.11.*,
+                     tasty >= 0.10,
+                     tasty-hunit >= 0.9,
                      tasty-rerun >= 1.1
diff --git a/src/Language/Haskell/Liquid/Annotate.hs b/src/Language/Haskell/Liquid/Annotate.hs
--- a/src/Language/Haskell/Liquid/Annotate.hs
+++ b/src/Language/Haskell/Liquid/Annotate.hs
@@ -64,7 +64,7 @@
 --------------------------------------------------------------------------------------------
 mkOutput cfg res sol anna 
   = O { o_vars   = Nothing
-      , o_warns  = []
+      , o_errors = []
       , o_types  = toDoc <$> annTy 
       , o_templs = toDoc <$> annTmpl
       , o_bots   = mkBots    annTy 
@@ -85,7 +85,7 @@
        generateHtml srcF tyHtmlF typAnnMap 
        writeFile         vimF  $ vimAnnot cfg annTyp 
        B.writeFile       jsonF $ encode typAnnMap
-       forM_ bots (printf "WARNING: Found false in %s\n" . showPpr)
+       when showWarns $ forM_ bots (printf "WARNING: Found false in %s\n" . showPpr)
     where
        tplAnnMap  = mkAnnMap cfg result annTpl
        typAnnMap  = mkAnnMap cfg result annTyp
@@ -98,6 +98,7 @@
        annF       = extFileName Annot srcF
        jsonF      = extFileName Json  srcF  
        vimF       = extFileName Vim   srcF
+       showWarns  = not $ nowarnings cfg
 
 mkBots (AI m) = [ src | (src, (Just _, t) : _) <- sortBy (compare `on` fst) $ M.toList m
                       , isFalse (rTypeReft t) ]
diff --git a/src/Language/Haskell/Liquid/Bare.hs b/src/Language/Haskell/Liquid/Bare.hs
--- a/src/Language/Haskell/Liquid/Bare.hs
+++ b/src/Language/Haskell/Liquid/Bare.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE ParallelListComp           #-}
 {-# LANGUAGE OverloadedStrings          #-}
 {-# LANGUAGE ViewPatterns               #-}
+{-# LANGUAGE LambdaCase                 #-}
 
 -- | This module contains the functions that convert /from/ descriptions of 
 -- symbols, names and types (over freshly parsed /bare/ Strings),
@@ -31,7 +32,7 @@
 import PrelNames
 import PrelInfo                 (wiredInThings)
 import Type                     (expandTypeSynonyms, splitFunTy_maybe)
-import DataCon                  (dataConWorkId, dataConStupidTheta)
+import DataCon                  (dataConWorkId, dataConStupidTheta, dataConName)
 import TyCon                    (SynTyConRhs(SynonymTyCon))
 import HscMain
 import TysWiredIn
@@ -42,7 +43,8 @@
 import Data.Char                (isLower, isUpper)
 import Text.Printf
 -- import Data.Maybe               (listToMaybe, fromMaybe, mapMaybe, catMaybes, isNothing, fromJust)
-import Control.Monad.State      (get, gets, modify, State, evalState, evalStateT, execState, StateT)
+import Control.DeepSeq          (force)
+import Control.Monad.State      (get, gets, modify, put, State, evalState, evalStateT, execState, execStateT, StateT)
 import Data.Traversable         (forM)
 import Control.Applicative      ((<$>), (<*>), (<|>))
 import Control.Monad.Reader     hiding (forM)
@@ -63,9 +65,10 @@
 import Language.Haskell.Liquid.GhcMisc          hiding (L)
 import Language.Haskell.Liquid.Misc
 import Language.Haskell.Liquid.Types
-import Language.Haskell.Liquid.RefType
+import Language.Haskell.Liquid.RefType          hiding (freeTyVars)
 import Language.Haskell.Liquid.Errors
 import Language.Haskell.Liquid.PredType hiding (unify)
+import Language.Haskell.Liquid.CoreToLogic
 import qualified Language.Haskell.Liquid.Measure as Ms
 
 
@@ -88,7 +91,7 @@
   
   = throwOr (throwOr return . checkGhcSpec specs . postProcess cbs) =<< execBare act initEnv
   where
-    act      = makeGhcSpec' cfg vars defVars exports specs
+    act      = makeGhcSpec' cfg cbs vars defVars exports specs
     throwOr  = either Ex.throw
     initEnv  = BE name mempty mempty mempty env
     
@@ -100,16 +103,16 @@
 
 
 ------------------------------------------------------------------------------------------------
-makeGhcSpec' :: Config -> [Var] -> [Var] -> NameSet -> [(ModName, Ms.BareSpec)] -> BareM GhcSpec
+makeGhcSpec' :: Config -> [CoreBind] -> [Var] -> [Var] -> NameSet -> [(ModName, Ms.BareSpec)] -> BareM GhcSpec
 ------------------------------------------------------------------------------------------------
-makeGhcSpec' cfg vars defVars exports specs
+makeGhcSpec' cfg cbs vars defVars exports specs
   = do name                                    <- gets modName
        _                                       <- makeRTEnv specs
-       (tycons, datacons, dcSelectors, tyi)    <- makeGhcSpecCHOP1 specs
+       (tycons, datacons, dcSs, tyi, embs)     <- makeGhcSpecCHOP1 specs
        modify                                   $ \be -> be { tcEnv = tyi }
        (cls, mts)                              <- second mconcat . unzip . mconcat <$> mapM (makeClasses cfg vars) specs
-       (invs, ialias, embs, sigs, asms)        <- makeGhcSpecCHOP2 cfg vars defVars specs name cls mts 
-       (measures, cms', ms', cs', xs')         <- makeGhcSpecCHOP3 cfg vars specs dcSelectors datacons cls embs
+       (invs, ialias, sigs, asms)              <- makeGhcSpecCHOP2 cfg vars defVars specs name cls mts embs
+       (measures, cms', ms', cs', xs')         <- makeGhcSpecCHOP3 cfg cbs vars specs dcSs datacons cls embs
        syms                                    <- makeSymbols (vars ++ map fst cs') xs' (sigs ++ asms ++ cs') ms' (invs ++ (snd <$> ialias))
        let su  = mkSubst [ (x, mkVarExpr v) | (x, v) <- syms]
        return (emptySpec cfg)
@@ -122,6 +125,7 @@
 emptySpec     :: Config -> GhcSpec
 emptySpec cfg = SP [] [] [] [] [] [] [] [] [] mempty [] [] [] [] mempty mempty cfg mempty [] mempty 
 
+
 makeGhcSpec0 cfg defVars exports name sp
   = do targetVars <- makeTargetVars name defVars $ binders cfg
        return      $ sp { config = cfg         
@@ -129,13 +133,18 @@
                         , tgtVars = targetVars }
 
 makeGhcSpec1 vars embs tyi exports name sigs asms cs' ms' cms' su sp
-  = return $ sp { tySigs     = makePluggedSigs name embs tyi exports $ tx sigs  
-                , asmSigs    = renameTyVars <$> tx asms
-                , ctors      = tx   cs'
-                , meas       = tx $ ms' ++ varMeasures vars ++ cms' }
+  = do tySigs <- makePluggedSigs name embs tyi exports $ tx sigs
+       asmSigs <- makePluggedAsmSigs embs tyi $ tx asms
+       ctors <- makePluggedAsmSigs embs tyi $ tx cs'
+       return $ sp { tySigs     = tySigs
+                   , asmSigs    = asmSigs
+                   , ctors      = ctors
+                   , meas       = tx' $ tx $ ms' ++ varMeasures vars ++ cms' }
     where
       tx   = fmap . mapSnd . subst $ su
+      tx'  = fmap (mapSnd $ fmap uRType)
 
+
 makeGhcSpec2 invs ialias measures su sp
   = return $ sp { invariants = subst su invs 
                 , ialiases   = subst su ialias 
@@ -154,39 +163,43 @@
        texprs' <- mconcat <$> mapM (makeTExpr defVars) specs
        lazies  <- mkThing makeLazy
        lvars'  <- mkThing makeLVar
+       hmeas   <- mkThing makeHMeas
        quals   <- mconcat <$> mapM makeQualifiers specs
        return   $ sp { qualifiers = subst su quals
                      , decr       = decr'
                      , texprs     = texprs'
                      , lvars      = lvars'
-                     , lazy       = lazies }        
+                     , lazy       = lazies 
+                     , tySigs     = strengthenHaskellMeasures hmeas ++ tySigs sp}        
     where
        mkThing mk = S.fromList . mconcat <$> sequence [ mk defVars (m, s) | (m, s) <- specs, m == name ]
 
 makeGhcSpecCHOP1 specs
   = do (tcs, dcs)      <- mconcat <$> mapM makeConTypes specs
        let tycons       = tcs        ++ wiredTyCons 
-       let datacons     = mapSnd val <$> (concat dcs ++ wiredDataCons)
-       let dcSelectors  = concat $ map makeMeasureSelectors (concat dcs)
        let tyi          = makeTyConInfo tycons
-       return           $ (tycons, datacons, dcSelectors, tyi) 
+       embs            <- mconcat <$> mapM makeTyConEmbeds specs
+       datacons        <- makePluggedDataCons embs tyi (concat dcs ++ wiredDataCons)
+       let dcSelectors  = concat $ map makeMeasureSelectors datacons
+       return           $ (tycons, second val <$> datacons, dcSelectors, tyi, embs) 
 
-makeGhcSpecCHOP2 cfg vars defVars specs name cls mts
+makeGhcSpecCHOP2 cfg vars defVars specs name cls mts embs
   = do sigs'   <- mconcat <$> mapM (makeAssertSpec name cfg vars defVars) specs
        asms'   <- mconcat <$> mapM (makeAssumeSpec name cfg vars defVars) specs
        invs    <- mconcat <$> mapM makeInvariants specs
        ialias  <- mconcat <$> mapM makeIAliases   specs
-       embs    <- mconcat <$> mapM makeTyConEmbeds specs
        let dms  = makeDefaultMethods vars mts
        tyi     <- gets tcEnv
        let sigs = [ (x, txRefSort tyi embs . txExpToBind <$> t) | (m, x, t) <- sigs' ++ mts ++ dms ]
        let asms = [ (x, txRefSort tyi embs . txExpToBind <$> t) | (m, x, t) <- asms' ]
-       return     (invs, ialias, embs, sigs, asms)
+       return     (invs, ialias, sigs, asms)
 
-makeGhcSpecCHOP3 cfg vars specs dcSelectors datacons cls embs
+makeGhcSpecCHOP3 cfg cbs vars specs dcSelectors datacons cls embs
   = do measures'       <- mconcat <$> mapM makeMeasureSpec specs
-       tyi             <- gets tcEnv 
-       let measures     = measures' `mappend` Ms.mkMSpec' dcSelectors
+       tyi             <- gets tcEnv
+       name            <- gets modName 
+       hmeans          <- mapM (makeHaskellMeasures cbs name) specs
+       let measures     = mconcat (measures':Ms.mkMSpec' dcSelectors:hmeans)
        let (cs, ms)     = makeMeasureSpec' measures
        let cms          = makeClassMeasureSpec measures
        let cms'         = [ (x, Loc l $ cSort t) | (Loc l x, t) <- cms ]
@@ -195,6 +208,41 @@
        let xs'          = val . fst <$> ms
        return (measures, cms', ms', cs', xs')
        
+makeHaskellMeasures :: [CoreBind] -> ModName -> (ModName, Ms.BareSpec) -> BareM (Ms.MSpec SpecType DataCon)
+makeHaskellMeasures cbs name' (name, spec) | name /= name' = return mempty
+makeHaskellMeasures cbs _     (name, spec) = Ms.mkMSpec' <$> mapM (makeMeasureDefinition cbs) (S.toList $ Ms.hmeas spec)
+
+makeMeasureDefinition :: [CoreBind] -> LocSymbol -> BareM (Measure SpecType DataCon)
+makeMeasureDefinition cbs x 
+  = case (filter ((val x `elem`) . (map (dropModuleNames . simplesymbol)) . binders) cbs) of
+    (NonRec v def:_)   -> (Ms.mkM x (ofType $ varType v)) <$> coreToDef' x v def
+    (Rec [(v, def)]:_) -> (Ms.mkM x (ofType $ varType v)) <$> coreToDef' x v def
+    _                  -> mkError "Cannot extract measure from haskell function"
+  where
+    binders (NonRec x _) = [x]
+    binders (Rec xes)    = fst <$> xes  
+
+    coreToDef' x v def = case (runToLogic $ coreToDef x v def) of 
+                           Left x         -> return  x
+                           Right (LE str) -> mkError str
+
+    mkError str = throwError $ ErrHMeas (sourcePosSrcSpan $ loc x) (val x) (text str)                       
+
+simplesymbol = symbol . getName
+
+
+strengthenHaskellMeasures :: S.HashSet Var -> [(Var, Located SpecType)]
+strengthenHaskellMeasures hmeas = (\v -> (v, dummyLoc $ strengthenResult v)) <$> (S.toList hmeas)
+
+strengthenResult :: Var -> SpecType
+strengthenResult v
+  = fromRTypeRep $ rep{ty_res = ty_res rep `strengthen` r}
+  where rep = toRTypeRep t
+        r   = U (exprReft (EApp f [EVar x])) mempty mempty
+        x   = safeHead "strengthenResult" $ ty_binds rep
+        f   = dummyLoc $ dropModuleNames $ simplesymbol v
+        t   = (ofType $ varType v) :: SpecType
+
 makeMeasureSelectors :: (DataCon, Located DataConP) -> [Measure SpecType DataCon]
 makeMeasureSelectors (dc, (Loc loc (DataConP _ vs _ _ _ xts r))) = go <$> zip (reverse xts) [1..]
   where
@@ -203,15 +251,30 @@
     dty t         = foldr RAllT  (RFun dummySymbol r (fmap mempty t) mempty) vs
     n             = length xts
 
-
 makePluggedSigs name embs tcEnv exports sigs
-  = [ (x, plugHoles embs tcEnv x r τ t)
-    | (x, t) <- sigs
-    , let τ   = expandTypeSynonyms $ varType x
-    , let r   = maybeTrue x name exports
-    ]
+  = forM sigs $ \(x,t) -> do
+      let τ = expandTypeSynonyms $ varType x
+      let r = maybeTrue x name exports
+      (x,) <$> plugHoles embs tcEnv x r τ t
 
+makePluggedAsmSigs embs tcEnv sigs
+  = forM sigs $ \(x,t) -> do
+      let τ = expandTypeSynonyms $ varType x
+      let r = killHoles
+      (x,) <$> plugHoles embs tcEnv x r τ t
 
+makePluggedDataCons embs tcEnv dcs
+  = forM dcs $ \(dc, Loc l dcp) -> do
+       let (das, _, dts, dt) = dataConSig dc
+       let su = zip (freeTyVars dcp) (map rTyVar das)
+       tyArgs <- zipWithM (\t1 (x,t2) -> 
+                   (x,) . val <$> plugHoles embs tcEnv (dataConName dc) killHoles t1 (Loc l t2)) 
+                 dts (reverse $ tyArgs dcp)
+       tyRes <- val <$> plugHoles embs tcEnv (dataConName dc) killHoles dt (Loc l (tyRes dcp))
+       return (dc, Loc l dcp { freeTyVars = map rTyVar das
+                             , freePred = map (subts (zip (freeTyVars dcp) (map (rVar :: TyVar -> RSort) das))) (freePred dcp)
+                             , tyArgs = reverse tyArgs
+                             , tyRes = tyRes})
 
 makeMeasureSelector x s dc n i = M {name = x, sort = s, eqns = [eqn]}
   where eqn   = Def x dc (mkx <$> [1 .. n]) (E (EVar $ mkx i)) 
@@ -221,11 +284,14 @@
 makeRTEnv specs
   = do forM_ rts $ \(mod, rta) -> setRTAlias (rtName rta) $ Left (mod, rta)
        forM_ pts $ \(mod, pta) -> setRPAlias (rtName pta) $ Left (mod, pta)
+       forM_ ets $ \(mod, eta) -> setREAlias (rtName eta) $ Left (mod, eta)
+       makeREAliases ets
        makeRPAliases pts
        makeRTAliases rts
     where
        rts = (concat [(m,) <$> Ms.aliases  s | (m, s) <- specs])
        pts = (concat [(m,) <$> Ms.paliases s | (m, s) <- specs])
+       ets = (concat [(m,) <$> Ms.ealiases s | (m, s) <- specs])
        
 makeRTAliases xts = mapM_ expBody xts
   where
@@ -242,6 +308,14 @@
                           body <- withVArgs l (rtVArgs xt) $ expandRPAliasE l $ rtBody xt
                           setRPAlias (rtName xt) $ Right $ xt { rtBody = body }
 
+makeREAliases xts     = mapM_ expBody xts
+  where 
+    expBody (mod, xt) = inModule mod $ do
+                          let l = rtPos xt
+                          env  <- gets $ exprAliases . rtEnv
+                          body <- withVArgs l (rtVArgs xt) $ expandREAliasE l $ rtBody xt
+                          setREAlias (rtName xt) $ Right $ xt { rtBody = body }
+
 -- | Using the Alias Environment to Expand Definitions
 expandRTAliasMeasure m
   = do eqns <- sequence $ expandRTAliasDef <$> (eqns m)
@@ -266,21 +340,33 @@
 expandRTAlias   :: SourcePos -> BareType -> BareM SpecType
 expandRTAlias l bt = expType =<< expReft bt
   where 
-    expReft      = mapReftM (txPredReft expPred)
+    expReft      = mapReftM (txPredReft expPred expExpr)
     expType      = expandAlias  l []
     expPred      = expandPAlias l []
+    expExpr      = expandEAlias l []
 
-txPredReft :: (Pred -> BareM Pred) -> RReft -> BareM RReft
-txPredReft f (U r p l) = (\r -> U r p l) <$> txPredReft' f r
+mapPredM f = go
+  where
+    go (PAnd ps)       = PAnd <$> mapM go ps
+    go (POr ps)        = POr  <$> mapM go ps
+    go (PNot p)        = PNot <$> go p
+    go (PImp p q)      = PImp <$> go p <*> go q
+    go (PIff p q)      = PIff <$> go p <*> go q
+    go (PBexp e)       = PBexp <$> f e
+    go (PAtom b e1 e2) = PAtom b <$> f e1 <*> f e2
+    go (PAll xs p)     = PAll xs <$> go p
+    go p               = return p
+    
+
+txPredReft :: (Pred -> BareM Pred) -> (Expr -> BareM Expr) -> RReft -> BareM RReft
+txPredReft f fe (U r p l) = (\r -> U r p l) <$> txPredReft' f r
   where 
     txPredReft' f (Reft (v, ras)) = Reft . (v,) <$> mapM (txPredRefa f) ras
-    txPredRefa  f (RConc p)       = RConc <$> f p
+    txPredRefa  f (RConc p)       = fmap RConc $ (f <=< mapPredM fe) p
     txPredRefa  _ z               = return z
 
 -- | Using the Alias Environment to Expand Definitions
 
-expandRPAliasE l = expandPAlias l []
-
 expandAlias :: SourcePos -> [Symbol] -> BareType -> BareM SpecType
 expandAlias l = go
   where
@@ -296,7 +382,6 @@
     go s (RAllT a t)      = RAllT (symbolRTyVar a) <$> go s t
     go s (RAllP a t)      = RAllP <$> ofBPVar a <*> go s t
     go s (RAllS l t)      = RAllS l <$> go s t
-    go s (RCls c ts)      = RCls <$> lookupGhcClass c <*> mapM (go s) ts
     go _ (ROth s)         = return $ ROth s
     go _ (RExprArg e)     = return $ RExprArg e
     go _ (RHole r)        = RHole <$> resolve l r
@@ -335,25 +420,32 @@
 
 expandRTApp :: SourcePos -> [Symbol] -> RTAlias RTyVar SpecType  -> [BareType] -> RReft -> BareM SpecType
 expandRTApp l s rta args r
-  | length args == (length αs) + (length εs)
+  | length args == length αs + length εs
   = do args'  <- mapM (expandAlias l s) args
        let ts  = take (length αs) args'
            αts = zipWith (\α t -> (α, toRSort t, t)) αs ts
        return $ subst su . (`strengthen` r) . subsTyVars_meet αts $ rtBody rta
   | otherwise
-  = errortext $ (text msg)
+  = Ex.throw err
   where
     su        = mkSubst $ zip (symbol <$> εs) es
     αs        = rtTArgs rta 
     εs        = rtVArgs rta
---    msg       = rtName rta ++ " " ++ join (map showpp args)
     es_       = drop (length αs) args
-    es        = map (exprArg msg) es_
-    msg = "Malformed type alias application at " ++ show l ++ "\n\t"
-               ++ show (rtName rta) 
-               ++ " defined at " ++ show (rtPos rta)
-               ++ "\n\texpects " ++ show (length αs + length εs)
-               ++ " arguments but it is given " ++ show (length args)
+    es        = map (exprArg $ show err) es_
+    msg       = show err
+    err       :: Error
+    err       = ErrAliasApp (sourcePosSrcSpan l) (length args) (pprint $ rtName rta) (sourcePosSrcSpan $ rtPos rta) (length αs + length εs) 
+
+    -- JUNK msg = "Malformed type alias application at " ++ show l ++ "\n\t"
+    -- JUNK            ++ show (rtName rta) 
+    -- JUNK            ++ " defined at " ++ show (rtPos rta)
+    -- JUNK            ++ "\n\texpects " ++ show ()
+    -- JUNK            ++ " arguments but it is given " ++ show (length args)
+
+    -- JUNK Ex.throw $ errOther $ text 
+    -- JUNK                           $ "Cyclic Reftype Alias Definition: " ++ show (c:s)
+      
 -- | exprArg converts a tyVar to an exprVar because parser cannot tell 
 -- HORRIBLE HACK To allow treating upperCase X as value variables X
 -- e.g. type Matrix a Row Col = List (List a Row) Col
@@ -371,6 +463,8 @@
 exprArg msg z 
   = errorstar $ printf "Unexpected expression parameter: %s in %s" (show z) msg 
 
+expandRPAliasE l = expandPAlias l []
+
 expandPAlias :: SourcePos -> [Symbol] -> Pred -> BareM Pred
 expandPAlias l = go
   where 
@@ -383,9 +477,9 @@
               body <- inModule mod $ withVArgs l' (rtVArgs rp) $ expandPAlias l' (f':s) $ rtBody rp
               let rp' = rp { rtBody = body }
               setRPAlias f' $ Right $ rp'
-              expandRPApp l (f':s) rp' <$> resolve l es
+              expandEApp l (f':s) rp' <$> resolve l es
             Just (Right rp) ->
-              withVArgs l (rtVArgs rp) (expandRPApp l (f':s) rp <$> resolve l es)
+              withVArgs l (rtVArgs rp) (expandEApp l (f':s) rp <$> resolve l es)
             Nothing -> fmap PBexp (EApp <$> resolve l f <*> resolve l es)
     go s (PAnd ps)                = PAnd <$> (mapM (go s) ps)
     go s (POr  ps)                = POr  <$> (mapM (go s) ps)
@@ -395,16 +489,40 @@
     go s (PAll xts p)             = PAll xts <$> (go s p)
     go _ p                        = resolve l p
 
-expandRPApp l s rp es
-  = let su  = mkSubst $ safeZipWithError msg (rtVArgs rp) es
+expandREAliasE l = expandEAlias l []
+
+expandEAlias :: SourcePos -> [Symbol] -> Expr -> BareM Expr
+expandEAlias l = go
+  where 
+    --NOTE: don't do any name-resolution here, expandPAlias runs afterwards and
+    --      will handle it
+    go s e@(EApp f@(Loc l' f') es)
+      | f' `elem` s                = errorstar $ "Cyclic Predicate Alias Definition: " ++ show (f':s)
+      | otherwise = do
+          env <- gets (exprAliases.rtEnv)
+          case M.lookup f' env of
+            Just (Left (mod,re)) -> do
+              body <- inModule mod $ withVArgs l' (rtVArgs re) $ expandEAlias l' (f':s) $ rtBody re
+              let re' = re { rtBody = body }
+              setREAlias f' $ Right $ re'
+              expandEApp l (f':s) re' <$> mapM (go (f':s)) es
+            Just (Right re) ->
+              withVArgs l (rtVArgs re) (expandEApp l (f':s) re <$> mapM (go (f':s)) es)
+            Nothing -> EApp f <$> mapM (go s) es
+    go s (EBin op e1 e2)          = EBin op <$> go s e1 <*> go s e2
+    go s (EIte p  e1 e2)          = EIte p  <$> go s e1 <*> go s e2
+    go s (ECst e st)              = (`ECst` st) <$> go s e
+    go _ e                        = return e
+
+expandEApp l s re es
+  = let su  = mkSubst $ safeZipWithError msg (rtVArgs re) es
         msg = "Malformed alias application at " ++ show l ++ "\n\t"
-               ++ show (rtName rp) 
-               ++ " defined at " ++ show (rtPos rp)
-               ++ "\n\texpects " ++ show (length $ rtVArgs rp)
+               ++ show (rtName re) 
+               ++ " defined at " ++ show (rtPos re)
+               ++ "\n\texpects " ++ show (length $ rtVArgs re)
                ++ " arguments but it is given " ++ show (length es)
 --        msg = "expandRPApp: " ++ show (EApp (dummyLoc $ symbol $ rtName rp) es)
-    in subst su $ rtBody rp
-
+    in subst su $ rtBody re
 
 makeQualifiers (mod,spec) = inModule mod mkQuals
   where
@@ -423,17 +541,18 @@
                  let (dc:_) = tyConDataCons tc
                  let αs  = map symbolRTyVar as
                  let as' = [rVar $ symbolTyVar a | a <- as ]
-                 let ms' = [ (s, rFun "" (RCls c (flip RVar mempty <$> as)) t) | (s, t) <- ms]
+                 let ms' = [ (s, rFun "" (RApp c (flip RVar mempty <$> as) [] mempty) t) | (s, t) <- ms]
                  vts <- makeSpec cfg vs ms'
                  let sts = [(val s, unClass $ val t) | (s, _)    <- ms
                                                      | (_, _, t) <- vts]
-                 let t   = RCls (fromJust $ tyConClass_maybe tc) as'
+                 let t   = rCls tc as'
                  let dcp = DataConP l αs [] [] ss' (reverse sts) t
                  return ((dc,dcp),vts)
 
 makeHints vs (_, spec) = varSymbols id "Hint" vs $ Ms.decr spec
 makeLVar  vs (_, spec) = fmap fst <$> (varSymbols id "LazyVar" vs $ [(v, ()) | v <- Ms.lvars spec])
 makeLazy  vs (_, spec) = fmap fst <$> (varSymbols id "Lazy" vs $ [(v, ()) | v <- S.toList $ Ms.lazy spec])
+makeHMeas vs (_, spec) = fmap fst <$> (varSymbols id "HMeas" vs $ [(v, loc v) | v <- S.toList $ Ms.hmeas spec])
 makeTExpr vs (_, spec) = varSymbols id "TermExpr" vs $ Ms.termexprs spec
 
 varSymbols :: ([Var] -> [Var]) -> Symbol ->  [Var] -> [(LocSymbol, a)] -> BareM [(Var, a)]
@@ -528,26 +647,16 @@
 -- Renaming Type Variables in Haskell Signatures ------------------------------
 -------------------------------------------------------------------------------
 
--- This throws an exception if there is a mismatch
--- renameTyVars :: (Var, SpecType) -> (Var, SpecType)
-renameTyVars (x, lt@(Loc l t)) = (x, Loc l $ mkUnivs (rTyVar <$> αs) [] [] t')
-  where
-    t'                     = subts su $ mkUnivs [] ps ls tbody
-    su                     = [(y, rTyVar x) | (x, y) <- tyvsmap]
-    tyvsmap                = vmap $ execState (mapTyVars τbody tbody) initvmap 
-    initvmap               = initMapSt err
-    (αs, τbody)            = splitForAllTys $ expandTypeSynonyms $ varType x
-    (as, ps, ls, tbody)    = bkUniv t
-    err                    = errTypeMismatch x lt
-
-
 data MapTyVarST = MTVST { vmap   :: [(Var, RTyVar)]
                         , errmsg :: Error 
                         }
 
 initMapSt = MTVST []
 
-mapTyVars :: (PPrint r, Reftable r) => Type -> RRType r -> State MapTyVarST ()
+runMapTyVars :: StateT MapTyVarST (Either Error) () -> MapTyVarST -> Either Error MapTyVarST
+runMapTyVars x s = execStateT x s
+
+mapTyVars :: (PPrint r, Reftable r) => Type -> RRType r -> StateT MapTyVarST (Either Error) ()
 mapTyVars τ (RAllT a t)   
   = mapTyVars τ t
 mapTyVars (ForAllTy α τ) t 
@@ -557,13 +666,13 @@
 mapTyVars (TyConApp _ τs) (RApp _ ts _ _) 
    = zipWithM_ mapTyVars τs ts
 mapTyVars (TyVarTy α) (RVar a _)      
-   = modify $ \s -> mapTyRVar α a s
+   = do s  <- get
+        s' <- mapTyRVar α a s
+        put s'
 mapTyVars τ (RAllP _ t)   
   = mapTyVars τ t 
 mapTyVars τ (RAllS _ t)   
   = mapTyVars τ t 
-mapTyVars τ (RCls _ ts)     
-  = return ()
 mapTyVars τ (RAllE _ _ t)   
   = mapTyVars τ t 
 mapTyVars τ (REx _ _ t)
@@ -576,13 +685,13 @@
 mapTyVars τ (RHole _)
   = return ()
 mapTyVars τ t
-  = Ex.throw =<< errmsg <$> get
+  = throwError =<< errmsg <$> get
 
 mapTyRVar α a s@(MTVST αas err)
   = case lookup α αas of
-      Just a' | a == a'   -> s
-              | otherwise -> Ex.throw err
-      Nothing             -> MTVST ((α,a):αas) err
+      Just a' | a == a'   -> return s
+              | otherwise -> throwError err
+      Nothing             -> return $ MTVST ((α,a):αas) err
 
 mkVarExpr v 
   | isFunVar v = EApp (varFunSymbol v) []
@@ -617,7 +726,7 @@
 -----------------------------------------------------------------------------------
 -- | Error-Reader-IO For Bare Transformation --------------------------------------
 -----------------------------------------------------------------------------------
-
+-- FIXME: don't use WriterT [], very slow
 type BareM a = WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) a
 
 type Warn    = String
@@ -641,7 +750,7 @@
 
 withVArgs l vs act = do
   old <- gets rtEnv
-  mapM (mkExprAlias l . symbol . showpp) vs
+  mapM_ (mkExprAlias l . symbol . showpp) vs
   res <- act
   modify $ \be -> be { rtEnv = old }
   return res
@@ -657,11 +766,14 @@
 setRPAlias s a =
   modify $ \b -> b { rtEnv = mapRP (M.insert s a) $ rtEnv b }
 
+setREAlias s a =
+  modify $ \b -> b { rtEnv = mapRE (M.insert s a) $ rtEnv b }
+
 ------------------------------------------------------------------
 execBare :: BareM a -> BareEnv -> IO (Either Error a)
 ------------------------------------------------------------------
 execBare act benv = 
-   do z <- evalStateT (runErrorT (runWriterT act)) benv
+   do z <- evalStateT (runErrorT (runWriterT act)) benv `Ex.catch` (return . Left)
       case z of
         Left s        -> return $ Left s
         Right (x, ws) -> do forM_ ws $ putStrLn . ("WARNING: " ++) 
@@ -775,38 +887,39 @@
   where
     tx = (v,) . Loc l . generalize
 
-plugHoles tce tyi x f t (Loc l st) = Loc l $ mkArrow αs ps' (ls1 ++ ls2) cs' $ go rt' st'''
+plugHoles tce tyi x f t (Loc l st) 
+  = do tyvsmap <- case runMapTyVars (mapTyVars (toType rt') st'') initvmap of
+                    Left e -> throwError e
+                    Right s -> return $ vmap s
+       let su    = [(y, rTyVar x) | (x, y) <- tyvsmap]
+           st''' = subts su st''
+           ps'   = fmap (subts su') <$> ps
+           su'   = [(y, RVar (rTyVar x) ()) | (x, y) <- tyvsmap] :: [(RTyVar, RSort)]
+       Loc l . mkArrow αs ps' (ls1 ++ ls2) cs' <$> go rt' st'''
   where
     (αs, _, ls1, rt)  = bkUniv (ofType t :: SpecType)
     (cs, rt')         = bkClass rt
 
     (_, ps, ls2, st') = bkUniv st
     (_, st'')         = bkClass st'
-    cs'               = [(dummySymbol, RCls c t) | (c,t) <- cs]
-
-    tyvsmap           = vmap $ execState (mapTyVars (toType rt') st'') initvmap
+    cs'               = [(dummySymbol, RApp c t [] mempty) | (c,t) <- cs]
     initvmap          = initMapSt $ ErrMismatch (sourcePosSrcSpan l) (pprint x) t st
-    su                = [(y, rTyVar x) | (x, y) <- tyvsmap]
-    st'''             = subts su st''
-    ps'               = fmap (subts su') <$> ps
-    su'               = [(y, RVar (rTyVar x) ()) | (x, y) <- tyvsmap] :: [(RTyVar, RSort)]
 
-    go t                (RHole r)          = (addHoles t') { rt_reft = f r }
+    go :: SpecType -> SpecType -> BareM SpecType
+    go t                (RHole r)          = return $ (addHoles t') { rt_reft = f r }
       where
         t'       = everywhere (mkT $ addRefs tce tyi) t
         addHoles = fmap (const $ f $ uReft ("v", [hole]))
-    go (RVar _ _)       v@(RVar _ _)       = v
-    go (RFun _ i o _)   (RFun x i' o' r)   = RFun x (go i i') (go o o') r
-    go (RAllT _ t)      (RAllT a t')       = RAllT a $ 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 (RAppTy t1 t2 _) (RAppTy t1' t2' r) = RAppTy (go t1 t1') (go t2 t2') r
-    go (RApp _ t _ _)   (RApp c t' p r)    = RApp c (zipWith go t t') p r
-    go (RCls _ t)       (RCls c t')        = RCls c $ zipWith go t t'
-    go t                st                 = Ex.throw err
+    go (RVar _ _)       v@(RVar _ _)       = return v
+    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 t                (RAllE b a t')     = RAllE b a <$> go t t'
+    go t                (REx b x t')       = REx b x <$> 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 msg
-       msg = printf "plugHoles: unhandled case!\nt  = %s\nst = %s\n" (showpp t) (showpp st)
+       err = errOther $ text $ printf "plugHoles: unhandled case!\nt  = %s\nst = %s\n" (showpp t) (showpp st)
 
 addRefs :: TCEmb TyCon
      -> M.HashMap TyCon RTyCon
@@ -1167,8 +1280,6 @@
 ofBareType (RApp tc ts rs r) 
   = do tyi <- tcEnv <$> get
        liftM3 (bareTCApp tyi r) (lookupGhcTyCon tc) (mapM ofRef rs) (mapM ofBareType ts)
-ofBareType (RCls c ts)
-  = liftM2 RCls (lookupGhcClass c) (mapM ofBareType ts)
 ofBareType (ROth s)
   = return $ ROth s
 ofBareType (RHole r)
@@ -1276,7 +1387,11 @@
   = addps m pos r ++ getPsSig m pos t1 ++ getPsSig m pos t2
 getPsSig m pos (RFun _ t1 t2 r) 
   = addps m pos r ++ getPsSig m pos t2 ++ getPsSig m (not pos) t1
-
+getPsSig m pos (RHole r)
+  = addps m pos r 
+getPsSig m pos z 
+  = error $ "getPsSig" ++ show z
+    
 
 getPsSigPs m pos (RPropP _ r) = addps m pos r
 getPsSigPs m pos (RProp  _ t) = getPsSig m pos t
@@ -1345,7 +1460,7 @@
 checkGhcSpec specs sp =  applyNonNull (Right sp) Left errors
   where 
     errors           =  mapMaybe (checkBind "constructor" emb tcEnv env) (dcons      sp)
-                     ++ mapMaybe (checkBind "measure"     emb tcEnv env) (measSpec   sp)
+                     ++ mapMaybe (checkBind "measure"     emb tcEnv env) (meas       sp)
                      ++ mapMaybe (checkInv  emb tcEnv env)               (invariants sp)
                      ++ (checkIAl  emb tcEnv env) (ialiases   sp)
                      ++ checkMeasures emb env ms
@@ -1356,20 +1471,24 @@
                      ++ checkRTAliases "Type Alias" env            tAliases
                      ++ checkRTAliases "Pred Alias" env            pAliases 
                   -- ++ checkDuplicateRTAlias "Predicate Alias"    pAliases  
-                  --   ++ checkRTAliasSyms      "Predicate Alias"    (concat [Ms.paliases sp | (_, sp) <- specs])
+                  -- ++ checkRTAliasSyms      "Predicate Alias"    (concat [Ms.paliases sp | (_, sp) <- specs])
 
 
     tAliases         =  concat [Ms.aliases sp  | (_, sp) <- specs]
     pAliases         =  concat [Ms.paliases sp | (_, sp) <- specs]
-    dcons spec       =  [ (v, Loc l dc)        | (v, dc) <- dataConSpec (dconsP spec), let l = getSourcePos v ] 
+    dcons spec       =  [(v, Loc l t) | (v,t)   <- dataConSpec (dconsP spec) 
+                                      | (_,dcp) <- dconsP spec
+                                      , let l = dc_loc dcp
+                                      ]
     emb              =  tcEmbeds sp
     env              =  ghcSpecEnv sp
     tcEnv            =  tyconEnv sp
     ms               =  measures sp
-    measSpec sp      =  [(x, uRType <$> t) | (x, t) <- meas sp] 
     sigs             =  tySigs sp ++ asmSigs sp
 
 
+-- RJ: This is not nice. More than 3 elements should be a record.
+    
 type ReplaceM = ReaderT ( M.HashMap Symbol Symbol
                         , SEnv SortedReft
                         , TCEmb TyCon
@@ -1562,7 +1681,7 @@
 
 checkRType emb env t         = efoldReft cb (rTypeSortedReft emb) f insertPEnv env Nothing t 
   where 
-    cb c ts                  = classBinds (RCls c ts)
+    cb c ts                  = classBinds (rRCls c ts)
     f env me r err           = err <|> checkReft env emb me r
     insertPEnv p γ           = insertsSEnv γ (mapSnd (rTypeSortedReft emb) <$> pbinds p) 
     pbinds p                 = (pname p, pvarRType p :: RSort) 
@@ -1662,8 +1781,6 @@
   = do ts' <- mapM expToBindT ts
        rs' <- mapM expToBindReft rs
        expToBindRef r >>= addExists . RApp c ts' rs'
-expToBindT (RCls c ts)
-  = liftM (RCls c) (mapM expToBindT ts)
 expToBindT (RAppTy t1 t2 r)
   = do t1' <- expToBindT t1
        t2' <- expToBindT t2
@@ -1726,7 +1843,8 @@
     inTarget    = moduleName (nameModule name) == getModName target
     name        = getName x
     notExported = not $ getName x `elemNameSet` exports
-    killHoles r@(U (Reft (v,rs)) _ _) = r { ur_reft = Reft (v, filter (not . isHole) rs) }
+
+killHoles r@(U (Reft (v,rs)) _ _) = r { ur_reft = Reft (v, filter (not . isHole) rs) }
 
 -------------------------------------------------------------------------------------
 -- | Tasteful Error Messages --------------------------------------------------------
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
@@ -1,101 +1,111 @@
-{-# LANGUAGE TupleSections      #-}
-{-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE TupleSections             #-}
 {-# LANGUAGE TypeSynonymInstances      #-}
-{-# LANGUAGE FlexibleInstances         #-}
 {-# OPTIONS_GHC -fno-cse #-}
 
--- | This module contains all the code needed to output the result which 
---   is either: `SAFE` or `WARNING` with some reasonable error message when 
---   something goes wrong. All forms of errors/exceptions should go through 
---   here. The idea should be to report the error, the source position that 
+-- | This module contains all the code needed to output the result which
+--   is either: `SAFE` or `WARNING` with some reasonable error message when
+--   something goes wrong. All forms of errors/exceptions should go through
+--   here. The idea should be to report the error, the source position that
 --   causes it, generate a suitable .json file and then exit.
 
 
 module Language.Haskell.Liquid.CmdLine (
-   -- * Get Command Line Configuration 
+   -- * Get Command Line Configuration
      getOpts, mkOpts
 
    -- * Update Configuration With Pragma
    , withPragmas
-   
+
    -- * Exit Function
    , exitWithResult
 
    -- * Diff check mode
-   , diffcheck 
+   , diffcheck
 ) where
 
-import Control.DeepSeq
-import Control.Monad
-import Control.Applicative                      ((<$>))
+import           Control.Applicative                 ((<$>))
+import           Control.DeepSeq
+import           Control.Monad
 
-import           Data.List                                (foldl', nub)
+import qualified Data.HashMap.Strict                 as M
+import           Data.List                           (foldl', nub)
 import           Data.Maybe
 import           Data.Monoid
-import qualified Data.HashMap.Strict as M
-import qualified Data.Text as T
-import qualified Data.Text.IO as TIO
+import qualified Data.Text                           as T
+import qualified Data.Text.IO                        as TIO
 
-import           System.Directory                         (getCurrentDirectory)
-import           System.FilePath                          (dropFileName)
-import           System.Environment                       (lookupEnv, withArgs)
-import           System.Console.CmdArgs  hiding           (Loud)                
-import           System.Console.CmdArgs.Verbosity         (whenLoud)            
+import           System.Console.CmdArgs              hiding (Loud)
+import           System.Console.CmdArgs.Verbosity    (whenLoud)
+import           System.Directory                    (doesDirectoryExist, canonicalizePath, getCurrentDirectory)
+import           System.Environment                  (lookupEnv, withArgs)
+import           System.FilePath                     (dropFileName, isAbsolute,
+                                                      takeDirectory, (</>))
 
-import Language.Fixpoint.Misc
-import Language.Fixpoint.Files
-import Language.Fixpoint.Names                  (dropModuleNames)
-import Language.Fixpoint.Types hiding           (config)
-import Language.Fixpoint.Config hiding          (config, Config, real)
-import Language.Haskell.Liquid.Annotate
-import Language.Haskell.Liquid.Misc
-import Language.Haskell.Liquid.PrettyPrint
-import Language.Haskell.Liquid.Types hiding     (config, typ, name)
+import           Language.Fixpoint.Config            hiding (Config, config,
+                                                      real)
+import           Language.Fixpoint.Files
+import           Language.Fixpoint.Misc
+import           Language.Fixpoint.Names             (dropModuleNames)
+import           Language.Fixpoint.Types             hiding (config)
+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 Name
-import SrcLoc                                   (SrcSpan)
-import Text.PrettyPrint.HughesPJ    
-import Text.Parsec.Pos                          (newPos)
+import           Name
+import           SrcLoc                              (SrcSpan)
+import           Text.Parsec.Pos                     (newPos)
+import           Text.PrettyPrint.HughesPJ
 
 
 ---------------------------------------------------------------------------------
 -- Parsing Command Line----------------------------------------------------------
 ---------------------------------------------------------------------------------
 
-config = cmdArgsMode $ Config { 
-   files    
-    = def &= typ "TARGET" 
-          &= args 
-          &= typFile 
- 
- , idirs 
-    = def &= typDir 
-          &= help "Paths to Spec Include Directory " 
- 
- , fullcheck 
-     = def 
-           &= help "Full Checking: check all binders (DEFAULT)" 
-  
- , diffcheck 
-    = def 
-          &= help "Incremental Checking: only check changed binders" 
+config = cmdArgsMode $ Config {
+   files
+    = def &= typ "TARGET"
+          &= args
+          &= typFile
 
+ , idirs
+    = def &= typDir
+          &= help "Paths to Spec Include Directory "
+
+ , fullcheck
+     = def
+           &= help "Full Checking: check all binders (DEFAULT)"
+
+ , diffcheck
+    = def
+          &= help "Incremental Checking: only check changed binders"
+
  , real
-    = def 
-          &= help "Supports real number arithmetic" 
+    = def
+          &= help "Supports real number arithmetic"
 
  , binders
     = def &= help "Check a specific set of binders"
 
- , noPrune 
+ , noPrune
     = def &= help "Disable prunning unsorted Predicates"
           &= name "no-prune-unsorted"
 
- , notermination 
+ , notermination
     = def &= help "Disable Termination Check"
           &= name "no-termination-check"
 
+ , nowarnings
+    = def &= help "Don't display warnings, only show errors"
+          &= name "no-warnings"
+
+ , trustinternals
+    = def &= help "Trust all ghc auto generated code"
+          &= name "trust-interals"
+
  , nocaseexpand
     = def &= help "Disable Termination Check"
           &= name "no-case-expand"
@@ -106,25 +116,25 @@
     = def &= help "Disable Trueing Top Level Types"
           &= name "no-true-types"
 
- , totality 
+ , totality
     = def &= help "Check totality"
 
- , smtsolver 
-    = def &= help "Name of SMT-Solver" 
+ , smtsolver
+    = def &= help "Name of SMT-Solver"
 
- , noCheckUnknown 
+ , noCheckUnknown
     = def &= explicit
           &= name "no-check-unknown"
           &= help "Don't complain about specifications for unexported and unused values "
 
- , maxParams 
+ , maxParams
     = 2   &= help "Restrict qualifier mining to those taking at most `m' parameters (2 by default)"
 
  , shortNames
     = def &= name "short-names"
           &= help "Print shortened names, i.e. drop all module qualifiers."
- 
- , shortErrors 
+
+ , shortErrors
     = def &= name "short-errors"
           &= help "Don't show long error messages, just line numbers."
 
@@ -137,46 +147,63 @@
     = def &= name "c-files"
           &= typ "OPTION"
           &= help "Tell GHC to compile and link against these files"
- 
- -- , verbose  
+
+ -- , verbose
  --    = def &= help "Generate Verbose Output"
  --          &= name "verbose-output"
 
  } &= verbosity
-   &= program "liquid" 
-   &= help    "Refinement Types for Haskell" 
-   &= summary copyright 
+   &= program "liquid"
+   &= help    "Refinement Types for Haskell"
+   &= summary copyright
    &= details [ "LiquidHaskell is a Refinement Type based verifier for Haskell"
               , ""
               , "To check a Haskell file foo.hs, type:"
               , "  liquid foo.hs "
               ]
 
-getOpts :: IO Config 
-getOpts = do cfg0    <- envCfg 
-             cfg1    <- mkOpts =<< cmdArgsRun config 
+getOpts :: IO Config
+getOpts = do cfg0    <- envCfg
+             cfg1    <- mkOpts =<< cmdArgsRun config
              pwd     <- getCurrentDirectory
              cfg     <- canonicalizePaths (fixCfg $ mconcat [cfg0, cfg1]) pwd
              whenNormal $ putStrLn copyright
              return cfg
 
-fixCfg cfg = cfg { diffcheck = diffcheck cfg && not (fullcheck cfg) } 
+-- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have
+--   to worry about relative paths.
+canonicalizePaths :: Config -> FilePath -> IO Config
+canonicalizePaths cfg tgt
+  = do -- st  <- getFileStatus tgt
+       tgt   <- canonicalizePath tgt
+       isdir <- doesDirectoryExist tgt
+       let canonicalize f
+             | isAbsolute f = return f
+             | isdir        = canonicalizePath (tgt </> f)
+             --   | isDirectory st = canonicalizePath (tgt </> f)
+             | otherwise      = canonicalizePath (takeDirectory tgt </> f)
+       is <- mapM canonicalize $ idirs cfg
+       cs <- mapM canonicalize $ cFiles cfg
+       return $ cfg { idirs = is, cFiles = cs }
 
+
+fixCfg cfg = cfg { diffcheck = diffcheck cfg && not (fullcheck cfg) }
+
 envCfg = do so <- lookupEnv "LIQUIDHASKELL_OPTS"
             case so of
               Nothing -> return mempty
               Just s  -> parsePragma $ envLoc s
-         where 
+         where
             envLoc  = Loc (newPos "ENVIRONMENT" 0 0)
 
-copyright = "LiquidHaskell © Copyright 2009-14 Regents of the University of California. All Rights Reserved.\n"
+copyright = "LiquidHaskell Copyright 2009-14 Regents of the University of California. All Rights Reserved.\n"
 
 mkOpts :: Config -> IO Config
-mkOpts cfg  
-  = do files' <- sortNub . concat <$> mapM getHsTargets (files cfg) 
+mkOpts cfg
+  = do let files' = sortNub $ files cfg
        -- idirs' <- if null (idirs cfg) then single <$> getIncludeDir else return (idirs cfg)
-       id0 <- getIncludeDir 
-       return  $ cfg { files = files' } 
+       id0 <- getIncludeDir
+       return  $ cfg { files = files' }
                      { idirs = (dropFileName <$> files') ++ [id0] ++ idirs cfg }
                               -- tests fail if you flip order of idirs'
 
@@ -200,35 +227,37 @@
 -- | Monoid instances for updating options
 ---------------------------------------------------------------------------------------
 
-  
+
 instance Monoid Config where
-  mempty        = Config def def def def def def def def def def def def def 2 def def def def def
-  mappend c1 c2 = Config { files          = sortNub $ files c1   ++     files          c2  
-                         , idirs          = sortNub $ idirs c1   ++     idirs          c2 
-                         , fullcheck      = fullcheck c1         ||     fullcheck      c2  
-                         , real           = real      c1         ||     real           c2  
-                         , diffcheck      = diffcheck c1         ||     diffcheck      c2  
-                         , binders        = sortNub $ binders c1 ++     binders        c2  
-                         , noCheckUnknown = noCheckUnknown c1    ||     noCheckUnknown c2  
-                         , notermination  = notermination  c1    ||     notermination  c2  
-                         , nocaseexpand   = nocaseexpand   c1    ||     nocaseexpand   c2  
-                         , strata         = strata         c1    ||     strata         c2  
-                         , notruetypes    = notruetypes    c1    ||     notruetypes    c2  
-                         , totality       = totality       c1    ||     totality       c2  
-                         , noPrune        = noPrune        c1    ||     noPrune        c2  
-                         , maxParams      = maxParams      c1   `max`   maxParams      c2 
-                         , smtsolver      = smtsolver c1      `mappend` smtsolver      c2 
-                         , shortNames     = shortNames c1        ||     shortNames     c2 
-                         , shortErrors    = shortErrors c1       ||     shortErrors    c2 
+  mempty        = Config def def def def def def def def def def def def def def def 2 def def def def def
+  mappend c1 c2 = Config { files          = sortNub $ files c1   ++     files          c2
+                         , idirs          = sortNub $ idirs c1   ++     idirs          c2
+                         , fullcheck      = fullcheck c1         ||     fullcheck      c2
+                         , real           = real      c1         ||     real           c2
+                         , diffcheck      = diffcheck c1         ||     diffcheck      c2
+                         , binders        = sortNub $ binders c1 ++     binders        c2
+                         , noCheckUnknown = noCheckUnknown c1    ||     noCheckUnknown c2
+                         , notermination  = notermination  c1    ||     notermination  c2
+                         , nowarnings     = nowarnings     c1    ||     nowarnings     c2
+                         , trustinternals = trustinternals c1    ||     trustinternals c2
+                         , nocaseexpand   = nocaseexpand   c1    ||     nocaseexpand   c2
+                         , strata         = strata         c1    ||     strata         c2
+                         , notruetypes    = notruetypes    c1    ||     notruetypes    c2
+                         , totality       = totality       c1    ||     totality       c2
+                         , noPrune        = noPrune        c1    ||     noPrune        c2
+                         , maxParams      = maxParams      c1   `max`   maxParams      c2
+                         , smtsolver      = smtsolver c1      `mappend` smtsolver      c2
+                         , shortNames     = shortNames c1        ||     shortNames     c2
+                         , shortErrors    = shortErrors c1       ||     shortErrors    c2
                          , ghcOptions     = ghcOptions c1        ++     ghcOptions     c2
                          , cFiles         = cFiles c1            ++     cFiles         c2
                          }
 
 instance Monoid SMTSolver where
   mempty        = def
-  mappend s1 s2 
-    | s1 == s2  = s1 
-    | s2 == def = s1 
+  mappend s1 s2
+    | s1 == s2  = s1
+    | s2 == def = s1
     | otherwise = s2
 
 
@@ -237,34 +266,32 @@
 ------------------------------------------------------------------------
 
 ------------------------------------------------------------------------
-exitWithResult :: Config -> FilePath -> Output Doc -> IO (Output Doc) 
+exitWithResult :: Config -> FilePath -> Output Doc -> IO (Output Doc)
 ------------------------------------------------------------------------
 exitWithResult cfg target out
-  = do let r  = o_result out 
-       let rs = showFix r
-       {-# SCC "annotate" #-} annotate cfg target out
+  = do {-# SCC "annotate" #-} annotate cfg target out
        donePhase Loud "annotate"
        writeCheckVars $ o_vars  out
-       writeWarns     $ o_warns out
        writeResult cfg (colorResult r) r
-       writeFile   (extFileName Result target) rs
-       return $ out { o_result = if null (o_warns out) then r else Unsafe [] }
+       writeFile   (extFileName Result target) (showFix r)
+       return $ out { o_result = r }
+    where
+       r         = o_result out `addErrors` o_errors out
 
-writeWarns []            = return () 
-writeWarns ws            = colorPhaseLn Angry "Warnings:" "" >> putStrLn (unlines $ nub ws)
 
-writeCheckVars Nothing   = return ()
-writeCheckVars (Just []) = colorPhaseLn Loud "Checked Binders: None" ""
-writeCheckVars (Just ns) = colorPhaseLn Loud "Checked Binders:" "" >> forM_ ns (putStrLn . symbolString . dropModuleNames . symbol)
 
-writeResult cfg c        = mapM_ (writeDoc c) . zip [0..] . resDocs tidy 
-  where 
-    tidy                 = if shortErrors cfg then Lossy else Full
-    writeDoc c (i, d)    = writeBlock c i $ lines $ render d
-    writeBlock c _ []    = return ()
-    writeBlock c 0 ss    = forM_ ss (colorPhaseLn c "")
-    writeBlock c _ ss    = forM_ ("\n" : ss) putStrLn
+writeCheckVars Nothing     = return ()
+writeCheckVars (Just [])   = colorPhaseLn Loud "Checked Binders: None" ""
+writeCheckVars (Just ns)   = colorPhaseLn Loud "Checked Binders:" "" >> forM_ ns (putStrLn . symbolString . dropModuleNames . symbol)
 
+writeResult cfg c          = mapM_ (writeDoc c) . zip [0..] . resDocs tidy
+  where
+    tidy                   = if shortErrors cfg then Lossy else Full
+    writeDoc c (i, d)      = writeBlock c i $ lines $ render d
+    writeBlock c _ []      = return ()
+    writeBlock c 0 ss      = forM_ ss (colorPhaseLn c "")
+    writeBlock _  _ ss     = forM_ ("\n" : ss) putStrLn
+
 resDocs _ Safe             = [text "SAFE"]
 resDocs k (Crash xs s)     = text ("CRASH: " ++ s) : pprManyOrdered k "" xs
 resDocs k (Unsafe xs)      = text "UNSAFE" : pprManyOrdered k "" (nub xs)
@@ -273,6 +300,10 @@
 reportUrl              = text "Please submit a bug report at: https://github.com/ucsd-progsys/liquidhaskell"
 
 
+addErrors r []             = r
+addErrors Safe errs        = Unsafe errs
+addErrors (Unsafe xs) errs = Unsafe (xs ++ errs)
+addErrors r  _             = r
 instance Fixpoint (FixResult Error) where
   toFix = vcat . resDocs Full
 
diff --git a/src/Language/Haskell/Liquid/Constraint.hs b/src/Language/Haskell/Liquid/Constraint.hs
--- a/src/Language/Haskell/Liquid/Constraint.hs
+++ b/src/Language/Haskell/Liquid/Constraint.hs
@@ -97,7 +97,11 @@
 consAct info
   = do γ     <- initEnv info
        sflag <- scheck <$> get
-       foldM_ (consCBTop (derVars info)) γ (cbs info)
+       tflag <- trustghc <$> get
+       let trustBinding x = if tflag 
+                             then (x `elem` (derVars info) || isInternal x) 
+                             else False 
+       foldM_ (consCBTop trustBinding) γ (cbs info)
        hcs <- hsCs  <$> get 
        hws <- hsWfs <$> get
        scss <- sCs <$> get
@@ -184,7 +188,7 @@
 
 measEnv sp xts cbs lts asms hs
   = CGE { loc   = noSrcSpan
-        , renv  = fromListREnv $ second (uRType . val) <$> meas sp
+        , renv  = fromListREnv $ second val <$> meas sp
         , syenv = F.fromListSEnv $ freeSyms sp
         , fenv  = initFEnv $ lts ++ (second (rTypeSort tce . val) <$> meas sp)
         , recs  = S.empty 
@@ -350,9 +354,6 @@
 splitW (WfC γ t@(RVar _ _))
   = bsplitW γ t 
 
-splitW (WfC _ (RCls _ _))
-  = return []
-
 splitW (WfC γ t@(RApp _ ts rs _))
   =  do ws    <- bsplitW γ t 
         γ'    <- γ `extendEnvWithVV` t 
@@ -360,6 +361,18 @@
         ws''  <- concat <$> mapM (rsplitW γ) rs
         return $ ws ++ ws' ++ ws''
 
+splitW (WfC γ (RAllE x tx t))
+  = do  ws  <- splitW (WfC γ tx) 
+        γ'  <- (γ, "splitW") += (x, tx)
+        ws' <- splitW (WfC γ' t)
+        return $ ws ++ ws'
+
+splitW (WfC γ (REx x tx t))
+  = do  ws  <- splitW (WfC γ tx) 
+        γ'  <- (γ, "splitW") += (x, tx)
+        ws' <- splitW (WfC γ' t)
+        return $ ws ++ ws'
+
 splitW (WfC _ t) 
   = errorstar $ "splitW cannot handle: " ++ showpp t
 
@@ -440,6 +453,10 @@
   = splitS $ SubC γ t1 t2' 
   where t2' = subsTyVar_meet' (α2, RVar α1 mempty) t2
 
+splitS (SubC γ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isClass c1 && c1 == c2 
+  = return []
+
+
 splitS (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _))
   = do (t1',t2') <- unifyVV t1 t2
        cs    <- bsplitS t1' t2'
@@ -457,9 +474,6 @@
   | a1 == a2
   = bsplitS t1 t2
 
-splitS (SubC _ (RCls c1 _) (RCls c2 _)) | c1 == c2
-  = return []
-
 splitS c@(SubC _ t1 t2) 
   = errorstar $ "(Another Broken Test!!!) splitS unexpected: " ++ showpp t1 ++ "\n\n" ++ showpp t2
 
@@ -559,6 +573,10 @@
   = splitC $ SubC γ t1 t2' 
   where t2' = subsTyVar_meet' (α2, RVar α1 mempty) t2
 
+
+splitC (SubC γ t1@(RApp c1 _ _ _) t2@(RApp c2 _ _ _)) | isClass c1 && c1 == c2
+  = return []
+
 splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _))
   = do (t1',t2') <- unifyVV t1 t2
        cs    <- bsplitC γ t1' t2'
@@ -576,9 +594,6 @@
   | a1 == a2
   = bsplitC γ t1 t2
 
-splitC (SubC _ (RCls c1 _) (RCls c2 _)) | c1 == c2
-  = return []
-
 splitC c@(SubC _ t1 t2) 
   = errorstar $ "(Another Broken Test!!!) splitc unexpected: " ++ showpp t1 ++ "\n\n" ++ showpp t2
 
@@ -619,8 +634,7 @@
   | s1 <:= s2 = return ()
   | otherwise = addWarning wrn
   where [s1, s2]   = getStrata <$> [t1, t2]
-        wrn        =  "Stratum Error : " ++ show s1 ++ " > " ++ show s2 ++ 
-                      "\tat " ++ show (pprint $ loc γ)
+        wrn        =  ErrOther (loc γ) (text $ "Stratum Error : " ++ show s1 ++ " > " ++ show s2) 
 
 bsplitC' γ t1 t2 pflag
   | F.isFunctionSortedReft r1' && F.isNonTrivialSortedReft r2'
@@ -682,8 +696,9 @@
                      , lits       :: ![(F.Symbol, F.Sort)]        -- ^ ? FIX THIS 
                      , tcheck     :: !Bool                        -- ^ Check Termination (?) 
                      , scheck     :: !Bool                        -- ^ Check Strata (?)
+                     , trustghc   :: !Bool                        -- ^ Trust ghc auto generated bindings
                      , pruneRefs  :: !Bool                        -- ^ prune unsorted refinements
-                     , logWarn    :: ![String]                    -- ^ ? FIX THIS
+                     , logErrors  :: ![TError SpecType]           -- ^ Errors during coontraint generation
                      , kvProf     :: !KVProf                      -- ^ Profiling distribution of KVars 
                      , recCount   :: !Int                         -- ^ number of recursive functions seen (for benchmarks)
                      } -- deriving (Data, Typeable)
@@ -733,8 +748,9 @@
   , specLazy   = lazy spc
   , tcheck     = not $ notermination cfg
   , scheck     = strata cfg
+  , trustghc   = trustinternals cfg
   , pruneRefs  = not $ noPrune cfg
-  , logWarn    = []
+  , logErrors  = []
   , kvProf     = emptyKVProf
   , recCount   = 0
   } 
@@ -772,8 +788,8 @@
        let γ' = γ { renv = insertREnv x t (renv γ) }  
        pflag <- pruneRefs <$> get
        is    <- if isBase t 
-                  then liftM single $ addBind x $ rTypeSortedReft' pflag γ' t 
-                  else addClassBind t 
+                  then liftM2 (++) (liftM single $ addBind x $ rTypeSortedReft' pflag γ' t) (addClassBind t)
+                  else return [] -- addClassBind t 
        return $ γ' { fenv = insertsFEnv (fenv γ) is }
 
 (++=) :: CGEnv -> (String, F.Symbol, SpecType) -> CG CGEnv
@@ -882,8 +898,8 @@
 addW   :: WfC -> CG ()  
 addW !w = modify $ \s -> s { hsWfs = w : (hsWfs s) }
 
-addWarning   :: String -> CG ()  
-addWarning w = modify $ \s -> s { logWarn = w : (logWarn s) }
+addWarning   :: TError SpecType -> CG ()  
+addWarning w = modify $ \s -> s { logErrors = w : (logErrors s) }
 
 -- | Used for annotation binders (i.e. at binder sites)
 
@@ -1004,7 +1020,8 @@
 
 makeDecrIndex :: (Var, SpecType)-> CG [Int]
 makeDecrIndex (x, t) 
-  = do hint <- checkHint' . L.lookup x . specDecr <$> get
+  = do spDecr <- specDecr <$> get
+       hint   <- checkHint' (L.lookup x $ spDecr)
        case dindex of
          Nothing -> addWarning msg >> return []
          Just i  -> return $ fromMaybe [i] hint
@@ -1012,7 +1029,7 @@
        ts         = ty_args $ toRTypeRep t
        checkHint' = checkHint x ts isDecreasing
        dindex     = L.findIndex isDecreasing ts
-       msg        = printf "%s: No decreasing parameter" $ showPpr (getSrcSpan x) 
+       msg        = ErrTermin [x] (getSrcSpan x) (text "No decreasing parameter") 
 
 recType ((_, []), (_, [], t))
   = t
@@ -1029,13 +1046,13 @@
                   loc (showPpr x) (showPpr vs)
 
 checkIndex (x, vs, t, index)
-  = do mapM_ (safeLogIndex msg' vs)  index
+  = do mapM_ (safeLogIndex msg' vs) index
        mapM  (safeLogIndex msg  ts) index
     where
-       loc   = showPpr (getSrcSpan x)
+       loc   = getSrcSpan x
        ts    = ty_args $ toRTypeRep t
-       msg'  = printf "%s: No decreasing argument on %s with %s" loc (showPpr x) (showPpr vs)
-       msg   = printf "%s: No decreasing parameter" loc
+       msg'  = ErrTermin [x] loc (text $ "No decreasing argument on " ++ (showPpr x) ++ " with " ++ (showPpr vs))
+       msg   = ErrTermin [x] loc (text "No decreasing parameter")
 
 makeRecType t vs dxs is
   = fromRTypeRep $ trep {ty_binds = xs', ty_args = ts'}
@@ -1050,26 +1067,26 @@
   | otherwise      = return $ Just $ ls !! n
 
 checkHint _ _ _ Nothing 
-  = Nothing
+  = return Nothing
 
 checkHint x ts f (Just ns) | L.sort ns /= ns
-  = errorstar $ printf "%s: The hints should be increasing" loc
-  where loc = showPpr $ getSrcSpan x
+  = addWarning (ErrTermin [x] loc (text "The hints should be increasing")) >> return Nothing
+  where loc = getSrcSpan x
 
 checkHint x ts f (Just ns) 
-  = Just $ catMaybes (checkValidHint x ts f <$> ns)
+  = (mapM (checkValidHint x ts f) ns) >>= (return . Just . catMaybes)
 
 checkValidHint x ts f n
-  | n < 0 || n >= length ts = errorstar err
-  | f (ts L.!! n)           = Just n
-  | otherwise               = errorstar err
-  where err = printf "%s: Invalid Hint %d for %s" loc (n+1) (showPpr x)
-        loc = showPpr $ getSrcSpan x
+  | n < 0 || n >= length ts = addWarning err >> return Nothing
+  | f (ts L.!! n)           = return $ Just n
+  | otherwise               = addWarning err >> return Nothing
+  where err = ErrTermin [x] loc (text $ "Invalid Hint " ++ show (n+1) ++ " for " ++ (showPpr x) ++  "\nin\n" ++ show (ts))
+        loc = getSrcSpan x
 
 -------------------------------------------------------------------
 -------------------- Generation: Corebind -------------------------
 -------------------------------------------------------------------
-consCBTop :: [Var] -> CGEnv -> CoreBind -> CG CGEnv 
+consCBTop :: (Var -> Bool) -> CGEnv -> CoreBind -> CG CGEnv 
 consCBLet :: CGEnv -> CoreBind -> CG CGEnv 
 -------------------------------------------------------------------
 
@@ -1083,14 +1100,13 @@
        modify $ \s -> s{tcheck = oldtcheck}
        return γ'
 
-consCBTop dVs γ cb | isDerived
+consCBTop trustBinding γ cb | all trustBinding xs
   = do ts <- mapM trueTy (varType <$> xs)
        foldM (\γ xt -> (γ, "derived") += xt) γ (zip xs' ts)
-  where isDerived = all (`elem` dVs) xs
-        xs        = bindersOf cb
-        xs'       = F.symbol <$> xs
+  where xs             = bindersOf cb
+        xs'            = F.symbol <$> xs
 
-consCBTop _  γ cb
+consCBTop _ γ cb
   = do oldtcheck <- tcheck <$> get
        strict    <- specLazy <$> get
        let tflag  = oldtcheck
@@ -1115,12 +1131,12 @@
        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 refreshArgs $ (fromAsserted . thd3 <$> xets)
        let vs    = zipWith collectArgs ts' es
-       is       <- checkSameLens <$> mapM makeDecrIndex (zip xs ts')
+       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)
-       checkEqTypes . L.transpose <$> mapM checkIndex (zip4 xs vs ts is)
+       (L.transpose <$> mapM checkIndex (zip4 xs vs ts is)) >>= checkEqTypes
        let rts   = (recType <$>) <$> xeets
        let xts   = zip xs (Asserted <$> ts)
        γ'       <- foldM extender γ xts
@@ -1131,17 +1147,18 @@
   where
        dmapM f  = sequence . (mapM f <$>)
        (xs, es) = unzip xes
-       collectArgs   = collectArguments . length . ty_binds . toRTypeRep
-       checkEqTypes  = map (checkAll err1 toRSort . catMaybes)
-       checkSameLens = checkAll err2 length
-       err1          = printf "%s: The decreasing parameters should be of same type" loc
-       err2          = printf "%s: All Recursive functions should have the same number of decreasing parameters" loc
-       loc           = showPpr $ getSrcSpan (head xs)
+       collectArgs    = collectArguments . length . ty_binds . toRTypeRep
+       checkEqTypes :: [[Maybe SpecType]] -> CG [[SpecType]]
+       checkEqTypes x = mapM (checkAll err1 toRSort) (catMaybes <$> x)
+       checkSameLens  = checkAll err2 length
+       err1           = ErrTermin xs loc $ text "The decreasing parameters should be of same type"
+       err2           = ErrTermin xs loc $ text "All Recursive functions should have the same number of decreasing parameters"
+       loc            = getSrcSpan (head xs)
 
-       checkAll _   _ []            = []
+       checkAll _   _ []            = return []
        checkAll err f (x:xs) 
-         | all (==(f x)) (f <$> xs) = (x:xs)
-         | otherwise                = errorstar err
+         | all (==(f x)) (f <$> xs) = return (x:xs)
+         | otherwise                = addWarning err >> return [] 
 
 consCBWithExprs γ (Rec xes) 
   = do xets'     <- forM xes $ \(x, e) -> liftM (x, e,) (varTemplate γ (x, Just e))
@@ -1519,7 +1536,6 @@
 
 refreshVV (RAllT a t) = liftM (RAllT a) (refreshVV t)
 refreshVV (RAllP p t) = liftM (RAllP p) (refreshVV t)
-refreshVV (RCls c ts) = liftM (RCls c) (mapM refreshVV ts)
 
 refreshVV (REx x t1 t2)
   = do [t1', t2'] <- mapM refreshVV [t1, t2]
@@ -1621,7 +1637,6 @@
   show = showPpr
 
 checkTyCon _ t@(RApp _ _ _ _) = t
-checkTyCon _ t@(RCls cl ts)   = classToRApp t
 checkTyCon x t                = checkErr x t --errorstar $ showPpr x ++ "type: " ++ showPpr t
 
 -- checkRPred _ t@(RAll _ _)     = t
diff --git a/src/Language/Haskell/Liquid/CoreToLogic.hs b/src/Language/Haskell/Liquid/CoreToLogic.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/Liquid/CoreToLogic.hs
@@ -0,0 +1,171 @@
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FlexibleContexts       #-} 
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE OverloadedStrings      #-}
+{-# LANGUAGE TupleSections          #-}
+
+module Language.Haskell.Liquid.CoreToLogic ( coreToDef , mkLit, runToLogic, LError(..) ) where
+
+import GHC hiding (Located)
+import Var
+
+import qualified CoreSyn as C
+import Literal
+import IdInfo
+
+import Control.Applicative 
+
+import Language.Fixpoint.Misc
+import Language.Fixpoint.Names (dropModuleNames, isPrefixOfSym)
+import Language.Fixpoint.Types hiding (Def, R, simplify)
+import qualified Language.Fixpoint.Types as F
+import qualified Language.Fixpoint.Types as F
+import Language.Haskell.Liquid.GhcMisc hiding (isDictionary)
+import Language.Haskell.Liquid.Types    hiding (GhcInfo(..), GhcSpec (..))
+
+
+import qualified Data.HashMap.Strict as M
+
+import Data.Monoid
+import Data.Functor
+import Data.Either
+
+newtype LogicM a = LM (Either a LError)
+
+
+data LError = LE String
+
+instance Monad LogicM where
+	return = LM . Left
+	(LM (Left x))  >>= f = f x
+	(LM (Right x)) >>= f = LM (Right x)
+
+instance Functor LogicM where
+	fmap f (LM (Left x))  = LM $ Left $ f x
+	fmap f (LM (Right x)) = LM $ Right x
+
+instance Applicative LogicM where
+	pure = LM . Left
+
+	(LM (Left f))  <*> (LM (Left x))  = LM $ Left (f x)
+	(LM (Right f)) <*> (LM (Left x))  = LM $ Right f
+	(LM (Left f))  <*> (LM (Right x)) = LM $ Right x
+	(LM (Right f)) <*> (LM (Right x)) = LM $ Right x
+
+throw :: String -> LogicM a
+throw = LM . Right . LE
+
+runToLogic (LM x) = x
+
+coreToDef :: LocSymbol -> Var -> C.CoreExpr ->  LogicM [Def DataCon]
+coreToDef x v e = go $ simplify e
+  where
+    go (C.Lam a e)  = go e
+    go (C.Tick _ e) = go e
+    go (C.Case _ _ _ alts) = mapM goalt alts
+    go e'                 = throw "Measure Functions should have a case at top level"
+
+    goalt ((C.DataAlt d), xs, e) = ((Def x d (symbol <$> xs)) . E) <$> coreToLogic e
+    goalt alt = throw $ "Bad alternative" ++ showPpr alt
+
+
+coreToLogic :: C.CoreExpr -> LogicM Expr
+coreToLogic (C.Let b e)  = subst1 <$> coreToLogic e <*>  makesub b
+coreToLogic (C.Tick _ e) = coreToLogic e
+coreToLogic (C.App (C.Var v) e) | ignoreVar v = coreToLogic e
+coreToLogic (C.Lit l)            
+  = case mkLit l of 
+     Nothing -> throw $ "Bad Literal in measure definition" ++ showPpr l
+     Just i -> return i
+coreToLogic (C.Var x)           = return $ EVar $ symbol x
+coreToLogic e@(C.App _ _)       = toLogicApp e 
+coreToLogic e                   = throw ("Cannot transform to Logic" ++ showPpr e)
+
+toLogicApp :: C.CoreExpr -> LogicM Expr
+toLogicApp e   
+  =  do let (f, es) = splitArgs e
+        args       <- reverse <$> (mapM coreToLogic es)
+        (`makeApp` args) <$> tosymbol f
+
+makeApp f [e1, e2] | Just op <- M.lookup (val f) bops
+  = EBin op e1 e2
+
+makeApp f args 
+  = EApp f args
+
+bops :: M.HashMap Symbol Bop
+bops = M.fromList [ (symbol ("+" :: String), Plus)
+                  , (symbol ("-" :: String), Minus)
+                  , (symbol ("*" :: String), Times)
+                  , (symbol ("/" :: String), Div)
+                  , (symbol ("%" :: String), Mod)
+                  ] 
+
+splitArgs (C.App (C.Var i) e) | ignoreVar i       = splitArgs e
+splitArgs (C.App f (C.Var v)) | isDictionary v    = splitArgs f
+splitArgs (C.App f e) = (f', e:es) where (f', es) = splitArgs f
+splitArgs f           = (f, [])
+
+tosymbol (C.Var x) = return $ dummyLoc $ simpleSymbolVar x
+tosymbol  e        = throw ("Bad Measure Definition:\n" ++ showPpr e ++ "\t cannot be applied")
+
+makesub (C.NonRec x e) =  (symbol x,) <$> coreToLogic e
+makesub  _             = throw "Cannot make Logical Substitution of Recursive Definitions"
+
+mkLit :: Literal -> Maybe Expr
+mkLit (MachInt    n)   = mkI n
+mkLit (MachInt64  n)   = mkI n
+mkLit (MachWord   n)   = mkI n
+mkLit (MachWord64 n)   = mkI n
+mkLit (MachFloat  n)   = mkR n
+mkLit (MachDouble n)   = mkR n
+mkLit (LitInteger n _) = mkI n
+mkLit _                = Nothing -- ELit sym sort
+mkI                    = Just . ECon . I  
+mkR                    = Just . ECon . F.R . fromRational
+
+ignoreVar i = simpleSymbolVar i `elem` ["I#"]
+
+
+simpleSymbolVar  = dropModuleNames . symbol . showPpr . getName
+
+isDictionary v   = isPrefixOfSym (symbol ("$" :: String)) (simpleSymbolVar v)
+
+isDead = isDeadOcc . occInfo . idInfo
+
+class Simplify a where
+  simplify :: a -> a 
+
+instance Simplify C.CoreExpr where
+  simplify e@(C.Var x) 
+    = e
+  simplify e@(C.Lit _) 
+    = e
+  simplify (C.App e (C.Type _))                        
+    = simplify e
+  simplify (C.App e (C.Var dict))  | isDictionary dict 
+    = simplify e
+  simplify (C.App (C.Lam x e) _)   | isDead x          
+    = simplify e
+  simplify (C.App e1 e2) 
+    = C.App (simplify e1) (simplify e2)
+  simplify (C.Lam x e) | isTyVar x 
+    = simplify e
+  simplify (C.Lam x e) 
+    = C.Lam x (simplify e)
+  simplify (C.Let xes e) 
+    = C.Let (simplify xes) (simplify e)
+  simplify (C.Case e x t alts) 
+    = C.Case (simplify e) x t (simplify <$> alts)
+  simplify (C.Cast e c)    
+    = simplify e
+  simplify (C.Tick _ e) 
+    = simplify e
+
+instance Simplify C.CoreBind where
+  simplify (C.NonRec x e) = C.NonRec x (simplify e)
+  simplify (C.Rec xes)    = C.Rec (mapSnd simplify <$> xes )
+
+instance Simplify C.CoreAlt where
+  simplify (c, xs, e) = (c, xs, simplify e) 
+
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
@@ -192,6 +192,10 @@
   = dSp <+> text "Bad Measure Specification"
     $+$ (nest 4 $ text "measure " <+> pprint t $+$ pprint s)
 
+ppError' _ dSp (ErrHMeas _ t s)
+  = dSp <+> text "Cannot promote Haskell function" <+> pprint t <+> text "to logic"
+    $+$ (nest 4 $ pprint s)
+
 ppError' _ dSp (ErrDupSpecs _ v ls)
   = dSp <+> text "Multiple Specifications for" <+> pprint v <> colon
     $+$ (nest 4 $ vcat $ pprint <$> ls)
@@ -214,8 +218,17 @@
     $+$ text "Haskell:" <+> pprint τ
     $+$ text "Liquid :" <+> pprint t
 
+ppError' _ dSp (ErrAliasApp _ n name dl dn)
+  = dSp <+> text "Malformed Type Alias Application"
+    $+$ text "Type alias:" <+> pprint name
+    $+$ text "Defined at:" <+> pprint dl
+    $+$ text "Expects"     <+> pprint dn <+> text "arguments, but is given" <+> pprint n  
+
 ppError' _ dSp (ErrSaved _ s)
   = dSp <+> s
+
+ppError' _ dSp (ErrTermin xs _ s)
+  = dSp <+> text "Termination Error on" <+> (hsep $ intersperse comma $ map pprint xs) $+$ s
 
 ppError' _ _ (ErrOther _ s)
   = text "Panic!" <+> nest 4 (pprint s)
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
@@ -67,6 +67,9 @@
 trueRefType (RFun _ t t' _)
   = rFun <$> fresh <*> true t <*> true t'
 
+trueRefType (RApp c ts _  _) | isClass c
+  = rRCls c <$> mapM true ts
+
 trueRefType (RApp c ts rs r)
   = RApp c <$> mapM true ts <*> mapM trueRef rs <*> true r
 
@@ -95,6 +98,9 @@
 refreshRefType (RFun b t t' _)
   | b == dummySymbol = rFun <$> fresh <*> refresh t <*> refresh t'
   | otherwise        = rFun     b     <$> refresh t <*> refresh t'
+
+refreshRefType (RApp rc ts _ _) | isClass rc
+  = return $ rRCls rc ts 
 
 refreshRefType (RApp rc ts rs r)
   = RApp rc <$> mapM refresh ts <*> mapM refreshRef rs <*> refresh r
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
@@ -138,12 +138,12 @@
         deps :: [Id]
         deps = concatMap dep $ (unfoldingInfo . idInfo <$> concatMap bindersOf cbf)
 
-        dep (DFunUnfolding _ _ e) = concatMap grapDep  e
-        dep _                     = []
+        dep (DFunUnfolding _ _ e)         = concatMap grapDep  e
+        dep (CoreUnfolding {uf_tmpl = e}) = grapDep  e
+        dep f                             = []
 
         grapDep :: CoreExpr -> [Id]
-        grapDep (Var x)     = [x]
-        grapDep _           = []
+        grapDep e           = freeVars S.empty e
 
 updateDynFlags cfg
   = do df <- getSessionDynFlags
@@ -203,7 +203,7 @@
      Nothing     -> exitWithPanic "Ghc Interface: Unable to get GhcModGuts"
 
 
-getDerivedDictionaries cm mod = filter ((`elem` pdFuns) . shortPpr) dFuns 
+getDerivedDictionaries cm mod = dFuns -- filter ((`elem` pdFuns) . shortPpr) dFuns 
   where hsmod    = unLoc $ pm_parsed_source mod
         decls    = unLoc <$> hsmodDecls hsmod
         tyClD    = [d  | TyClD  d <- decls]
@@ -395,7 +395,11 @@
 specIncludes ext paths reqs 
   = do let libFile  = extFileNameR ext $ symbolString preludeName
        let incFiles = catMaybes $ reqFile ext <$> reqs 
-       liftIO $ forM (libFile : incFiles) (`findFileInDirs` paths)
+       liftIO $ forM (libFile : incFiles) $ \f -> do
+         mfile <- getFileInDirs f paths
+         case mfile of
+           Just file -> return file
+           Nothing -> errorstar $ "cannot find " ++ f ++ " in " ++ show paths
 
 reqFile ext s 
   | isExtFile ext s 
diff --git a/src/Language/Haskell/Liquid/GhcMisc.hs b/src/Language/Haskell/Liquid/GhcMisc.hs
--- a/src/Language/Haskell/Liquid/GhcMisc.hs
+++ b/src/Language/Haskell/Liquid/GhcMisc.hs
@@ -13,6 +13,9 @@
 
 module Language.Haskell.Liquid.GhcMisc where
 
+import PrelNames (fractionalClassKeys)
+import Class     (classKey)
+
 import           Debug.Trace
 
 import           Avail                        (availsToNameSet)
@@ -25,6 +28,7 @@
 import           NameSet                      (NameSet)
 import           SrcLoc                       (mkRealSrcLoc, mkRealSrcSpan, srcSpanFile, srcSpanFileName_maybe, srcSpanStartLine, srcSpanStartCol)
 
+import           Language.Fixpoint.Names      (dropModuleNames)
 import           Language.Fixpoint.Misc       (errorstar, stripParens)
 import           Text.Parsec.Pos              (sourceName, sourceLine, sourceColumn, SourcePos, newPos)
 import           Language.Fixpoint.Types      hiding (SESearch(..))
@@ -162,6 +166,8 @@
 unTickExpr (Tick _ e)         = unTickExpr e
 unTickExpr x                  = x
 
+isFractionalClass clas = classKey clas `elem` fractionalClassKeys
+
 -----------------------------------------------------------------------
 ------------------ Generic Helpers for DataConstructors ---------------
 -----------------------------------------------------------------------
@@ -304,6 +310,7 @@
   where
     go tvs (Lam b e) | isTyVar b = go tvs     e
     go tvs (Lam b e) | isId    b = go (b:tvs) e
+    go tvs (Tick _ e)            = go tvs e
     go tvs e                     = (reverse tvs, e)
 
 ignoreLetBinds e@(Let (NonRec x xe) e') 
@@ -311,8 +318,8 @@
 ignoreLetBinds e 
   = e
 
-isDictionary x = L.isPrefixOf "$d" (showPpr x)
-isInternal   x = L.isPrefixOf "$" (showPpr x)
+isDictionary x = L.isPrefixOf "$d" (symbolString $ dropModuleNames $ symbol x)
+isInternal   x = L.isPrefixOf "$"  (symbolString $ dropModuleNames $ symbol x)
 
 
 instance Hashable Var where
diff --git a/src/Language/Haskell/Liquid/Measure.hs b/src/Language/Haskell/Liquid/Measure.hs
--- a/src/Language/Haskell/Liquid/Measure.hs
+++ b/src/Language/Haskell/Liquid/Measure.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FlexibleContexts       #-} 
 {-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE OverloadedStrings      #-}
 
 module Language.Haskell.Liquid.Measure (  
     Spec (..)
@@ -19,8 +20,11 @@
 import Text.PrettyPrint.HughesPJ hiding (first)
 import Text.Printf (printf)
 import DataCon
+
+import qualified Data.List as L 
 import qualified Data.HashMap.Strict as M 
 import qualified Data.HashSet        as S 
+import qualified Data.Text as T
 import Data.Monoid hiding ((<>))
 import Data.List (foldl1', union, nub)
 import Data.Either (partitionEithers)
@@ -50,11 +54,13 @@
   , includes   :: ![FilePath]                   -- ^ Included qualifier files
   , aliases    :: ![RTAlias Symbol BareType]    -- ^ RefType aliases
   , paliases   :: ![RTAlias Symbol Pred]        -- ^ Refinement/Predicate aliases
+  , ealiases   :: ![RTAlias Symbol Expr]        -- ^ Expression aliases
   , embeds     :: !(TCEmb (LocSymbol))          -- ^ GHC-Tycon-to-fixpoint Tycon map
   , qualifiers :: ![Qualifier]                  -- ^ Qualifiers in source/spec files
   , decr       :: ![(LocSymbol, [Int])]         -- ^ Information on decreasing arguments
   , lvars      :: ![(LocSymbol)]                -- ^ Variables that should be checked in the environment they are used
   , lazy       :: !(S.HashSet LocSymbol)        -- ^ Ignore Termination Check in these Functions
+  , hmeas      :: !(S.HashSet LocSymbol)        -- ^ Binders to turn into measures using haskell definitions
   , pragmas    :: ![Located String]             -- ^ Command-line configurations passed in through source
   , cmeasures  :: ![Measure ty ()]              -- ^ Measures attached to a type-class
   , imeasures  :: ![Measure ty bndr]            -- ^ Mappings from (measure,type) -> measure
@@ -123,6 +129,10 @@
     ms'    = checkDuplicateMeasure ms
     -- ms'    = checkFail "Duplicate Measure Definition" (distinct . fmap name) ms
 
+
+
+
+
 checkDuplicateMeasure ms 
   = case M.toList dups of 
       []         -> ms
@@ -149,11 +159,13 @@
            , includes   = sortNub $ includes s1   ++ includes s2
            , aliases    =           aliases s1    ++ aliases s2
            , paliases   =           paliases s1   ++ paliases s2
+           , ealiases   =           ealiases s1   ++ ealiases s2
            , embeds     = M.union   (embeds s1)     (embeds s2)
            , qualifiers =           qualifiers s1 ++ qualifiers s2
            , decr       =           decr s1       ++ decr s2
            , lvars      =           lvars s1      ++ lvars s2
            , lazy       = S.union   (lazy s1)        (lazy s2)
+           , hmeas      = S.union   (hmeas s1)       (hmeas s2)
            , pragmas    =           pragmas s1    ++ pragmas s2
            , cmeasures  =           cmeasures s1  ++ cmeasures s2
            , imeasures  =           imeasures s1  ++ imeasures s2
@@ -173,11 +185,13 @@
            , includes   = [] 
            , aliases    = [] 
            , paliases   = [] 
+           , ealiases   = [] 
            , embeds     = M.empty
            , qualifiers = []
            , decr       = []
            , lvars      = []
            , lazy       = S.empty
+           , hmeas      = S.empty
            , pragmas    = []
            , cmeasures  = []
            , imeasures  = []
@@ -270,7 +284,7 @@
 mapTy :: (tya -> tyb) -> Measure tya c -> Measure tyb c
 mapTy f (M n ty eqs) = M n (f ty) eqs
 
-dataConTypes :: MSpec RefType DataCon -> ([(Var, RefType)], [(LocSymbol, RefType)])
+dataConTypes :: MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)])
 dataConTypes  s = (ctorTys, measTys)
   where 
     measTys     = [(name m, sort m) | m <- M.elems (measMap s) ++ imeas s]
@@ -280,7 +294,7 @@
     defsTy      = foldl1' meet . fmap defRefType 
     defsVar     = ctor . safeHead "defsVar" 
 
-defRefType :: Def DataCon -> RefType
+defRefType :: Def DataCon -> RRType Reft
 defRefType (Def f dc xs body) = mkArrow as [] [] xts t'
   where 
     as  = RTV <$> dataConUnivTyVars dc
diff --git a/src/Language/Haskell/Liquid/Misc.hs b/src/Language/Haskell/Liquid/Misc.hs
--- a/src/Language/Haskell/Liquid/Misc.hs
+++ b/src/Language/Haskell/Liquid/Misc.hs
@@ -48,10 +48,18 @@
 zip4 (x1:xs1) (x2:xs2) (x3:xs3) (x4:xs4) = (x1, x2, x3, x4) : (zip4 xs1 xs2 xs3 xs4) 
 zip4 _ _ _ _                             = []
 
-getIncludeDir = dropFileName <$> getDataFileName "include/Prelude.spec"
-getCssPath    = getDataFileName "syntax/liquid.css"
-getHqBotPath  = getDataFileName "include/Bot.hquals"
+getIncludeDir = dropFileName <$> (getDataFileName $ "include" </> "Prelude.spec")
+getCssPath    = getDataFileName $ "syntax" </> "liquid.css"
+getHqBotPath  = getDataFileName $ "include" </> "Bot.hquals"
 
+
+maximumWithDefault zero [] = zero
+maximumWithDefault _    xs = maximum xs
+
+{-@ type ListN a N = {v:[a] | len v = N} @-}
+{-@ type ListL a L = ListN a (len L) @-}
+
+{-@ safeZipWithError :: _ -> xs:[a] -> ListL b xs -> ListL (a,b) xs / [xs] @-}
 safeZipWithError msg (x:xs) (y:ys) = (x,y) : safeZipWithError msg xs ys
 safeZipWithError _   []     []     = []
 safeZipWithError msg _      _      = errorstar msg
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
@@ -100,12 +100,12 @@
 ---------------------------------------------------------------------------
 parseErrorError     :: SourceName -> ParseError -> Error
 ---------------------------------------------------------------------------
-parseErrorError f e = ErrParse sp msg lpe
+parseErrorError f e = ErrParse sp msg e
   where 
     pos             = errorPos e
     sp              = sourcePosSrcSpan pos 
     msg             = text $ "Error Parsing Specification from: " ++ f
-    lpe             = LPE pos (eMsgs e)
+    -- lpe             = LPE pos (eMsgs e)
     eMsgs           = fmap messageString . errorMessages 
 
 ---------------------------------------------------------------------------
@@ -326,15 +326,13 @@
 
 
 
-getClasses (RApp tc ts _ _) 
+getClasses t@(RApp tc ts _ _) 
   | isTuple tc
-  = getClass `fmap` ts 
+  = ts
+  | otherwise 
+  = [t]
 getClasses t 
-  = [getClass t]
-getClass (RApp c ts _ _)
-  = RCls c ts
-getClass t
-  = errorstar $ "Cannot convert " ++ (show t) ++ " to Class"
+  = [t]
 
 dummyP ::  Monad m => m (Reft -> b) -> m b
 dummyP fm 
@@ -446,11 +444,13 @@
   | IAlias  (Located ty, Located ty)
   | Alias   (RTAlias Symbol BareType)
   | PAlias  (RTAlias Symbol Pred)
+  | EAlias  (RTAlias Symbol Expr)
   | Embed   (LocSymbol, FTycon)
   | Qualif  Qualifier
   | Decr    (LocSymbol, [Int])
   | LVars   LocSymbol
   | Lazy    LocSymbol
+  | HMeas   LocSymbol
   | Pragma  (Located String)
   | CMeas   (Measure ty ())
   | IMeas   (Measure ty ctor)
@@ -470,11 +470,13 @@
   show (IAlias _) = "IAlias" 
   show (Alias  _) = "Alias"  
   show (PAlias _) = "PAlias" 
+  show (EAlias _) = "EAlias" 
   show (Embed  _) = "Embed"  
   show (Qualif _) = "Qualif" 
   show (Decr   _) = "Decr"   
   show (LVars  _) = "LVars"  
   show (Lazy   _) = "Lazy"   
+  show (HMeas  _) = "HMeas"   
   show (Pragma _) = "Pragma" 
   show (CMeas  _) = "CMeas"  
   show (IMeas  _) = "IMeas"  
@@ -498,11 +500,13 @@
   , Measure.includes   = [q | Incl   q <- xs]
   , Measure.aliases    = [a | Alias  a <- xs]
   , Measure.paliases   = [p | PAlias p <- xs]
+  , Measure.ealiases   = [e | EAlias e <- xs]
   , Measure.embeds     = M.fromList [e | Embed e <- xs]
   , Measure.qualifiers = [q | Qualif q <- xs]
   , Measure.decr       = [d | Decr d   <- xs]
   , Measure.lvars      = [d | LVars d  <- xs]
-  , Measure.lazy       = S.fromList [s | Lazy s <- xs]
+  , Measure.lazy       = S.fromList [s | Lazy s  <- xs]
+  , Measure.hmeas      = S.fromList [s | HMeas s <- xs]
   , Measure.pragmas    = [s | Pragma s <- xs]
   , Measure.cmeasures  = [m | CMeas  m <- xs]
   , Measure.imeasures  = [m | IMeas  m <- xs]
@@ -515,7 +519,8 @@
   = try (reserved "assume"    >> liftM Assm   tyBindP   )
     <|> (reserved "assert"    >> liftM Asrt   tyBindP   )
     <|> (reserved "Local"     >> liftM LAsrt  tyBindP   )
-    <|> (reserved "measure"   >> liftM Meas   measureP  ) 
+    <|> try (reserved "measure"   >> liftM Meas   measureP  ) 
+    <|> (reserved "measure"   >> liftM HMeas  hmeasureP ) 
     <|> try (reserved "class" >> reserved "measure" >> liftM CMeas cMeasureP)
     <|> (reserved "instance"  >> reserved "measure" >> liftM IMeas iMeasureP)
     <|> (reserved "class"     >> liftM Class  classP    )
@@ -526,6 +531,7 @@
     <|> (reserved "using"     >> liftM IAlias invaliasP )
     <|> (reserved "type"      >> liftM Alias  aliasP    )
     <|> (reserved "predicate" >> liftM PAlias paliasP   )
+    <|> (reserved "expression">> liftM EAlias ealiasP   )
     <|> (reserved "embed"     >> liftM Embed  embedP    )
     <|> (reserved "qualif"    >> liftM Qualif qualifierP)
     <|> (reserved "Decrease"  >> liftM Decr   decreaseP )
@@ -544,6 +550,9 @@
 lazyVarP :: Parser LocSymbol
 lazyVarP = locParserP binderP
 
+hmeasureP :: Parser LocSymbol
+hmeasureP = locParserP binderP
+
 decreaseP :: Parser (LocSymbol, [Int])
 decreaseP = mapSnd f <$> liftM2 (,) (locParserP binderP) (spaces >> (many integer))
   where f = ((\n -> fromInteger n - 1) <$>)
@@ -588,6 +597,7 @@
 
 aliasP  = rtAliasP id     bareTypeP
 paliasP = rtAliasP symbol predP
+ealiasP = rtAliasP symbol exprP
 
 rtAliasP :: (Symbol -> tv) -> Parser ty -> Parser (RTAlias tv ty) 
 rtAliasP f bodyP
@@ -631,9 +641,10 @@
     mb Nothing   = []
     mb (Just xs) = xs
     superP = maybeP (parens ( liftM (toRCls <$>)  (bareTypeP `sepBy1` comma)) <* reserved "=>")
-    toRCls (RApp c ts rs r) = RCls c ts
-    toRCls t@(RCls _ _)     = t
-    toRCls t                = errorstar $ "Parse.toRCls called with" ++ show t
+    toRCls x = x
+--     toRCls (RApp c ts rs r) = RCls c ts
+--     toRCls t@(RCls _ _)     = t
+--     toRCls t                = errorstar $ "Parse.toRCls called with" ++ show t
 
 rawBodyP 
   = braces $ do
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
@@ -109,9 +109,6 @@
   = rFun dummySymbol (dataConTy m t1) (dataConTy m t2)
 dataConTy m (ForAllTy α t)          
   = RAllT (rTyVar α) (dataConTy m t)
-dataConTy _ t
-  | Just t' <- ofPredTree (classifyPredType t)
-  = t'
 dataConTy m (TyConApp c ts)        
   = rApp c (dataConTy m <$> ts) [] mempty
 dataConTy _ _
@@ -163,9 +160,6 @@
        t2' <- unifyS rt2 pt2
        return $ RAppTy t1' t2' (bUnify r p)
 
-unifyS t@(RCls _ _) (RCls _ _)
-  = return t
-
 unifyS (RVar v a) (RVar _ p)
   = do modify $ \s -> s `S.union` (S.fromList $ pvars p)
        return $ RVar v $ bUnify a p
@@ -318,7 +312,6 @@
   where (r', πs)                = splitRPvar π r
 
 substPred msg su (RRTy e r o t) = RRTy (mapSnd (substPred msg su) <$> e) r o (substPred msg su t)
-substPred msg su (RCls c ts)    = RCls c (substPred msg su <$> ts)
 substPred msg su (RAllE x t t') = RAllE x (substPred msg su t) (substPred msg su t')
 substPred msg su (REx x t t')   = REx   x (substPred msg su t) (substPred msg su t')
 substPred _   _  t              = t
@@ -370,8 +363,6 @@
   = not (p == p') && isPredInType p t 
 isPredInType p (RApp _ ts _ r) 
   = isPredInURef p r || any (isPredInType p) ts
-isPredInType p (RCls _ ts) 
-  = any (isPredInType p) ts
 isPredInType p (RAllE _ t1 t2) 
   = isPredInType p t1 || isPredInType p t2 
 isPredInType p (RAppTy t1 t2 r) 
@@ -394,8 +385,6 @@
   | otherwise = freeArgsPs p t 
 freeArgsPs p (RApp _ ts _ r) 
   = nub $ freeArgsPsRef p r ++ concatMap (freeArgsPs p) ts
-freeArgsPs p (RCls _ ts) 
-  = nub $ concatMap (freeArgsPs p) ts
 freeArgsPs p (RAllE _ t1 t2) 
   = nub $ freeArgsPs p t1 ++ freeArgsPs p t2 
 freeArgsPs p (RAppTy t1 t2 r) 
diff --git a/src/Language/Haskell/Liquid/PrettyPrint.hs b/src/Language/Haskell/Liquid/PrettyPrint.hs
--- a/src/Language/Haskell/Liquid/PrettyPrint.hs
+++ b/src/Language/Haskell/Liquid/PrettyPrint.hs
@@ -38,7 +38,7 @@
 import Language.Fixpoint.Names (dropModuleNames, propConName, hpropConName)
 import TypeRep          hiding (maybeParen, pprArrowChain)  
 import Text.Parsec.Pos              (SourcePos, newPos, sourceName, sourceLine, sourceColumn) 
-import Text.Parsec.Error (ParseError)
+import Text.Parsec.Error (ParseError, errorMessages, showErrorMessages)
 import Var              (Var)
 import Control.Applicative ((<*>), (<$>))
 import Data.Maybe   (fromMaybe)
@@ -50,7 +50,6 @@
 import Data.Interned
 import qualified Data.HashMap.Strict as M
 
-
 instance PPrint SrcSpan where
   pprint = pprDoc
 
@@ -63,11 +62,15 @@
 instance PPrint SourceError where
   pprint = text . show
 
--- instance PPrint ParseError where 
---   pprint = text . show 
+instance PPrint ParseError where 
+  pprint e = vcat $ tail $ map text ls
+    where
+      ls = lines $ showErrorMessages "or" "unknown parse error"
+                                     "expecting" "unexpected" "end of input"
+                                     (errorMessages e)
 
-instance PPrint LParseError where
-  pprint (LPE _ msgs) = text "Parse Error: " <> vcat (map pprint msgs)
+-- instance PPrint LParseError where
+--   pprint (LPE _ msgs) = text "Parse Error: " <> vcat (map pprint msgs)
 
 instance PPrint Var where
   pprint = pprDoc 
@@ -105,6 +108,7 @@
     ppE Lossy = ppEnvShort ppEnv
     ppE Full  = ppEnv
 
+
 ppr_rtype bb p t@(RAllT _ _)       
   = ppr_forall bb p t
 ppr_rtype bb p t@(RAllP _ _)       
@@ -135,8 +139,6 @@
         | otherwise  = ppTycon
 
 
-ppr_rtype bb p (RCls c ts)
-  = ppr_cls bb p c ts
 ppr_rtype bb p t@(REx _ _ _)
   = ppExists bb p t
 ppr_rtype bb p t@(RAllE _ _ _)
@@ -161,7 +163,6 @@
 ppSpine (RFun _ i o _)   = ppSpine i <+> text "->" <+> ppSpine o
 ppSpine (RAppTy t t' _)  = text "RAppTy" <+> parens (ppSpine t) <+> parens (ppSpine t')
 ppSpine (RHole r)        = text "RHole"
-ppSpine (RCls c ts)      = text "RCls" <+> parens (ppCls c ts)
 ppSpine (RApp c ts rs _) = text "RApp" <+> parens (pprint c)
 ppSpine (RVar v _)       = text "RVar"
 ppSpine (RExprArg _)     = text "RExprArg"
@@ -315,10 +316,7 @@
 ppTable m = vcat $ pprxt <$> xts
   where 
     pprxt (x,t) = pprint x $$ nest n (colon <+> pprint t)  
-    n          = 1 + maximum [ i | (x, _) <- xts, let i = keySize x, i <= thresh ]
+    n          = 1 + maximumWithDefault 0 [ i | (x, _) <- xts, let i = keySize x, i <= thresh ]
     keySize     = length . render . pprint
     xts         = sortBy (compare `on` fst) $ M.toList m
     thresh      = 6
-
-
-
diff --git a/src/Language/Haskell/Liquid/RefType.hs b/src/Language/Haskell/Liquid/RefType.hs
--- a/src/Language/Haskell/Liquid/RefType.hs
+++ b/src/Language/Haskell/Liquid/RefType.hs
@@ -34,7 +34,7 @@
   , freeTyVars, tyClasses, tyConName
 
   -- TODO: categorize these!
-  , ofType, ofPredTree, toType
+  , ofType, toType
   , rTyVar, rVar, rApp, rEx 
   , addTyConInfo
   -- , expandRApp
@@ -63,11 +63,11 @@
 import Literal
 import GHC              hiding (Located)
 import DataCon
-import PrelInfo         (isNumericClass)
 import qualified TyCon  as TC
 import TypeRep          hiding (maybeParen, pprArrowChain)  
 import Type             (mkClassPred, splitFunTys, expandTypeSynonyms, isPredTy, substTyWith, classifyPredType, PredTree(..), isClassPred)
-import TysWiredIn       (listTyCon, intDataCon, trueDataCon, falseDataCon)
+import TysWiredIn       (listTyCon, intDataCon, trueDataCon, falseDataCon, 
+                         intTyCon, charTyCon)
 
 import qualified        Data.Text as T
 import Data.Interned
@@ -94,6 +94,8 @@
 import Language.Haskell.Liquid.Types hiding (R, DataConP (..), sort)
 import Language.Haskell.Liquid.World
 
+import Language.Haskell.Liquid.CoreToLogic (mkLit)
+
 import Language.Haskell.Liquid.Misc
 import Language.Fixpoint.Misc
 import Language.Haskell.Liquid.GhcMisc (pprDoc, sDocDoc, typeUniqueString, tracePpr, tvId, getDataConVarUnique, showSDoc, showPpr, showSDocDump)
@@ -210,31 +212,7 @@
   bot         = errorstar "bot on RType"
 
 
--------------------------------------------------------------------------------
--- | TyConable Instances -------------------------------------------------------
--------------------------------------------------------------------------------
 
--- MOVE TO TYPES
-instance TyConable RTyCon where
-  isFun   = isFunTyCon . rtc_tc
-  isList  = (listTyCon ==) . rtc_tc
-  isTuple = TC.isTupleTyCon   . rtc_tc 
-  ppTycon = toFix 
-
--- MOVE TO TYPES
-instance TyConable Symbol where
-  isFun   s = funConName == s
-  isList  s = listConName == s
-  isTuple s = tupConName == s
-  ppTycon = text . symbolString
-
-instance TyConable LocSymbol where
-  isFun   = isFun . val
-  isList  = isList . val
-  isTuple = isTuple . val
-  ppTycon = ppTycon . val
-
-
 -------------------------------------------------------------------------------
 -- | RefTypable Instances -----------------------------------------------------
 -------------------------------------------------------------------------------
@@ -248,7 +226,7 @@
   toFix = text . showPpr
 
 -- MOVE TO TYPES
-instance (Eq p, PPrint p, TyConable c, Reftable r, PPrint r) => RefTypable p c Symbol r where
+instance (Eq p, PPrint p, TyConable c, Reftable r, PPrint r, PPrint c) => RefTypable p c Symbol r where
   ppCls   = ppClassSymbol
   ppRType = ppr_rtype ppEnv
 
@@ -293,9 +271,7 @@
   = eqRSort m t1 t1' && eqRSort m t2 t2'
 eqRSort m (RAppTy t1 t2 _) (RAppTy t1' t2' _) 
   = eqRSort m t1 t1' && eqRSort m t2 t2'
-eqRSort m (RApp c ts _ _) (RApp c' ts' _ _)
-  = c == c' && length ts == length ts' && and (zipWith (eqRSort m) ts ts')
-eqRSort m (RCls c ts) (RCls c' ts')
+eqRSort m t1@(RApp c ts _ _) t2@(RApp c' ts' _ _)
   = c == c' && length ts == length ts' && and (zipWith (eqRSort m) ts ts')
 eqRSort m (RVar a _) (RVar a' _)
   = a == M.lookupDefault a' a' m 
@@ -331,9 +307,6 @@
 instance Ord RTyCon where
   compare x y = compare (rtc_tc x) (rtc_tc y)
 
-instance Eq RTyCon where
-  x == y = rtc_tc x == rtc_tc y
-
 instance Hashable RTyCon where
   hashWithSalt i = hashWithSalt i . rtc_tc  
 
@@ -373,8 +346,6 @@
  = (t, ps)
 nlzP ps (RAllS _ t)
  = (t, ps)
-nlzP ps t@(RCls _ _)
- = (t, ps)
 nlzP ps (RAllP p t)
  = (t', [p] ++ ps ++ ps')
   where (t', ps') = nlzP [] t
@@ -556,7 +527,6 @@
 freeTyVars (RAllT α t)     = freeTyVars t L.\\ [α]
 freeTyVars (RFun _ t t' _) = freeTyVars t `L.union` freeTyVars t' 
 freeTyVars (RApp _ ts _ _) = L.nub $ concatMap freeTyVars ts
-freeTyVars (RCls _ ts)     = []
 freeTyVars (RVar α _)      = [α] 
 freeTyVars (RAllE _ _ t)   = freeTyVars t
 freeTyVars (REx _ _ t)     = freeTyVars t
@@ -573,21 +543,17 @@
 tyClasses (REx _ _ t)     = tyClasses t
 tyClasses (RFun _ t t' _) = tyClasses t ++ tyClasses t'
 tyClasses (RAppTy t t' _) = tyClasses t ++ tyClasses t'
-tyClasses (RApp _ ts _ _) = concatMap tyClasses ts 
-tyClasses (RCls c ts)     = (c, ts) : concatMap tyClasses ts 
+tyClasses (RApp c ts _ _) 
+  | Just cl <- tyConClass_maybe $ rtc_tc c 
+  = [(cl, ts)] 
+  | otherwise       
+  = []
 tyClasses (RVar α _)      = [] 
 tyClasses (RRTy _ _ _ t)  = tyClasses t
 tyClasses (RHole r)       = []
 tyClasses t               = errorstar ("RefType.tyClasses cannot handle" ++ show t)
 
 
-
---getTyClasses = everything (++) ([] `mkQ` f)
---  where f ((RCls c ts) :: SpecType) = [(c, ts)]
---        f _                        = []
-
-
-
 ----------------------------------------------------------------
 ---------------------- Strictness ------------------------------
 ----------------------------------------------------------------
@@ -603,7 +569,6 @@
   rnf (RAllS s t)      = rnf s `seq` rnf t
   rnf (RFun x t t' r)  = rnf x `seq` rnf t `seq` rnf t' `seq` rnf r
   rnf (RApp _ ts rs r) = rnf ts `seq` rnf rs `seq` rnf r
-  rnf (RCls c ts)      = c `seq` rnf ts
   rnf (RAllE x t t')   = rnf x `seq` rnf t `seq` rnf t'
   rnf (REx x t t')     = rnf x `seq` rnf t `seq` rnf t'
   rnf (ROth s)         = rnf s
@@ -634,15 +599,6 @@
 instance PPrint (RTProp p c tv r) => Show (RTProp p c tv r) where
   show = showpp
 
-instance Fixpoint RTyCon where
-  toFix (RTyCon c _ _) = text $ showPpr c -- <+> text "\n<<" <+> hsep (map toFix ts) <+> text ">>\n"
-
-instance PPrint RTyCon where
-  pprint = toFix
-
-instance Show RTyCon where
-  show = showpp  
-
 instance PPrint REnv where
   pprint (REnv m)  = pprint m
  
@@ -678,8 +634,6 @@
 subsFree m s z@(α, τ, _) (RApp c ts rs r)     
   = RApp (subt z' c) (subsFree m s z <$> ts) (subsFreeRef m s z <$> rs) r  
     where z' = (α, τ) -- UNIFY: why instantiating INSIDE parameters?
-subsFree m s z (RCls c ts)     
-  = RCls c (subsFree m s z <$> ts)
 subsFree meet s (α', _, t') t@(RVar α r) 
   | α == α' && not (α `S.member` s) 
   = if meet then t' `strengthen` r else t' 
@@ -795,9 +749,6 @@
   = rFun dummySymbol (ofType_ τ) (ofType_ τ') 
 ofType_ (ForAllTy α τ)  
   = RAllT (rTyVar α) $ ofType_ τ  
-ofType_ τ
-  | Just t <- ofPredTree (classifyPredType τ)
-  = t
 ofType_ (TyConApp c τs)
   | Just (αs, τ) <- TC.synTyConDefn_maybe c
   = ofType_ $ substTyWith αs τs τ
@@ -805,13 +756,13 @@
   = rApp c (ofType_ <$> τs) [] mempty 
 ofType_ (AppTy t1 t2)
   = RAppTy (ofType_ t1) (ofType t2) mempty             
--- ofType_ τ               
---   = errorstar ("ofType cannot handle: " ++ showPpr τ)
-
-ofPredTree (ClassPred c τs)
-  = Just $ RCls c (ofType_ <$> τs)
-ofPredTree _
-  = Nothing
+ofType_ (LitTy x)
+  = fromTyLit x
+  where
+    fromTyLit (NumTyLit n) = rApp intTyCon [] [] mempty
+    fromTyLit (StrTyLit s) = rApp listTyCon [rApp charTyCon [] [] mempty] [] mempty
+ofType_ τ               
+  = errorstar ("ofType cannot handle: " ++ showPpr τ)
 
 ----------------------------------------------------------------
 ------------------- Converting to Fixpoint ---------------------
@@ -882,8 +833,6 @@
   = TyVarTy α
 toType (RApp (RTyCon {rtc_tc = c}) ts _ _)   
   = TyConApp c (toType <$> ts)
-toType (RCls c ts)   
-  = mkClassPred c (toType <$> ts)
 toType (RAllE _ _ t)
   = toType t
 toType (REx _ _ t)
@@ -926,16 +875,6 @@
 literalConst tce l         = (sort, mkLit l)
   where 
     sort                   = typeSort tce $ literalType l 
-    mkLit (MachInt    n)   = mkI n
-    mkLit (MachInt64  n)   = mkI n
-    mkLit (MachWord   n)   = mkI n
-    mkLit (MachWord64 n)   = mkI n
-    mkLit (MachFloat  n)   = mkR n
-    mkLit (MachDouble n)   = mkR n
-    mkLit (LitInteger n _) = mkI n
-    mkLit _                = Nothing -- ELit sym sort
-    mkI                    = Just . ECon . I  
-    mkR                    = Just . ECon . R . fromRational
 
 ---------------------------------------------------------------
 ---------------- Annotations and Solutions --------------------
@@ -1061,9 +1000,13 @@
 -- | Binders generated by class predicates, typically for constraining tyvars (e.g. FNum)
 -----------------------------------------------------------------------------------------
 
-classBinds (RCls c ts) 
-  | isNumericClass c = [(rTyVarSymbol a, trueSortedReft FNum) | (RVar a _) <- ts]
-classBinds _         = [] 
+classBinds t@(RApp c ts _ _) 
+   | isFracCls c
+   = [(rTyVarSymbol a, trueSortedReft FReal) | (RVar a _) <- ts]
+   | isNumCls c
+   = [(rTyVarSymbol a, trueSortedReft FNum) | (RVar a _) <- ts]
+classBinds t         
+  = [] 
 
 rTyVarSymbol (RTV α) = typeUniqueSymbol $ TyVarTy α
 
diff --git a/src/Language/Haskell/Liquid/Tidy.hs b/src/Language/Haskell/Liquid/Tidy.hs
--- a/src/Language/Haskell/Liquid/Tidy.hs
+++ b/src/Language/Haskell/Liquid/Tidy.hs
@@ -119,7 +119,6 @@
 tyVars (RFun _ t t' _) = tyVars t ++ tyVars t' 
 tyVars (RAppTy t t' _) = tyVars t ++ tyVars t' 
 tyVars (RApp _ ts _ _) = concatMap tyVars ts
-tyVars (RCls _ ts)     = concatMap tyVars ts 
 tyVars (RVar α _)      = [α] 
 tyVars (RAllE _ _ t)   = tyVars t
 tyVars (REx _ _ t)     = tyVars t
@@ -139,7 +138,6 @@
 funBinds (RAllS _ t)      = funBinds t
 funBinds (RFun b t1 t2 _) = b : funBinds t1 ++ funBinds t2
 funBinds (RApp _ ts _ _)  = concatMap funBinds ts
-funBinds (RCls _ ts)      = concatMap funBinds ts 
 funBinds (RAllE b t1 t2)  = b : funBinds t1 ++ funBinds t2
 funBinds (REx b t1 t2)    = b : funBinds t1 ++ funBinds t2
 funBinds (RVar _ _)       = [] 
diff --git a/src/Language/Haskell/Liquid/TransformRec.hs b/src/Language/Haskell/Liquid/TransformRec.hs
--- a/src/Language/Haskell/Liquid/TransformRec.hs
+++ b/src/Language/Haskell/Liquid/TransformRec.hs
@@ -25,20 +25,51 @@
 import           TypeRep
 import           Unique              hiding (deriveUnique)
 import           Var
+import           Name (isSystemName)
 import           Language.Haskell.Liquid.GhcMisc
 import           Language.Haskell.Liquid.Misc (mapSndM)
+import           Language.Fixpoint.Misc       (mapSnd)
 
 import           Data.List                (foldl', isInfixOf)
 import           Control.Applicative      ((<$>))
 
+import qualified Data.List as L
+
 transformRecExpr :: CoreProgram -> CoreProgram
 transformRecExpr cbs
   | isEmptyBag $ filterBag isTypeError e
   =  {-trace "new cbs"-} pg 
   | otherwise 
-  = error (showPpr pg ++ "Type-check" ++ showSDoc (pprMessageBag e))
-  where pg     = evalState (transPg cbs) initEnv
+  = error ("INITIAL\n" ++ showPpr pg0 ++ "\nTRANSFORMED\n" ++ showPpr pg ++ "Type-check" ++ showSDoc (pprMessageBag e))
+  where pg0    = evalState (transPg cbs) initEnv
         (_, e) = lintCoreBindings [] pg
+        pg     = inlineFailCases pg0
+
+
+inlineFailCases :: CoreProgram -> CoreProgram
+inlineFailCases = (go [] <$>)
+  where 
+    go su (Rec xes)    = Rec (mapSnd (go' su) <$> xes)
+    go su (NonRec x e) = NonRec x (go' su e)
+
+    go' su (App (Var x) _)       | isFailId x, Just e <- getFailExpr x su = e  
+    go' su (Let (NonRec x ex) e) | isFailId x   = go' (addFailExpr x (go' su ex) su) e
+
+    go' su (App e1 e2)      = App (go' su e1) (go' su e2)
+    go' su (Lam x e)        = Lam x (go' su e)
+    go' su (Let xs e)       = Let (go su xs) (go' su e)
+    go' su (Case e x t alt) = Case (go' su e) x t (goalt su <$> alt) 
+    go' su (Cast e c)       = Cast (go' su e) c
+    go' su (Tick t e)       = Tick t (go' su e)
+    go' su e                = e
+
+    goalt su (c, xs, e)     = (c, xs, go' su e)
+
+    isFailId x  = isLocalId x && (isSystemName $ varName x) && L.isPrefixOf "fail" (show x)
+    getFailExpr = L.lookup
+
+    addFailExpr x (Lam _ e) su = (x, e):su 
+    addFailExpr x e         _  = error "internal error" -- this cannot happen
 
 isTypeError s | isInfixOf "Non term variable" (showSDoc s) = False
 isTypeError _ = True
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
@@ -17,7 +17,7 @@
 module Language.Haskell.Liquid.Types (
 
   -- * Options
-    Config (..), canonicalizePaths
+    Config (..)
   
   -- * Ghc Information
   , GhcInfo (..)
@@ -40,6 +40,7 @@
   , TyConInfo(..)
   , rTyConPVs 
   , rTyConPropVs
+  , isClassRTyCon
  
   -- * Refinement Types 
   , RType (..), Ref(..), RTProp (..)
@@ -73,7 +74,7 @@
   , BSort, BPVar
 
   -- * Instantiated RType
-  , BareType, RefType, PrType
+  , BareType, PrType
   , SpecType, SpecProp 
   , RSort
   , UsedPVar, RPVar, RReft
@@ -83,7 +84,7 @@
   , RTypeRep(..), fromRTypeRep, toRTypeRep
   , mkArrow, bkArrowDeep, bkArrow, safeBkArrow 
   , mkUnivs, bkUniv, bkClass
-  , rFun
+  , rFun, rCls, rRCls
 
   -- * Manipulating `Predicates`
   , pvars, pappSym, pToRef, pApp
@@ -139,8 +140,7 @@
   -- * Refinement Type Aliases
   , RTEnv (..)
   , RTBareOrSpec
-  , mapRT
-  , mapRP
+  , mapRT, mapRP, mapRE
 
   -- * Final Result
   , Result (..)
@@ -149,7 +149,7 @@
   , Error
   , TError (..)
   , EMsg (..)
-  , LParseError (..)
+  -- , LParseError (..)
   , ErrorResult
   , errSpan
   , errOther
@@ -173,7 +173,6 @@
   , updKVProf     -- extend profile
 
   -- * Misc 
-  , classToRApp
   , mapRTAVars
   , insertsSEnv
 
@@ -188,7 +187,7 @@
 
 import FastString                               (fsLit)
 import SrcLoc                                   (noSrcSpan, mkGeneralSrcSpan, SrcSpan)
-import TyCon
+import TyCon 
 import DataCon
 import Name                                     (getName)
 import NameSet
@@ -203,6 +202,10 @@
 import GHC.Generics
 import Language.Haskell.Liquid.GhcMisc 
 
+import PrelInfo         (isNumericClass)
+
+
+import TysWiredIn                               (listTyCon)
 import Control.Arrow                            (second)
 import Control.Monad                            (liftM, liftM2, liftM3)
 import qualified Control.Monad.Error as Ex
@@ -229,12 +232,12 @@
 import Language.Fixpoint.Misc
 import Language.Fixpoint.Types      hiding (Predicate, Def, R)
 -- import qualified Language.Fixpoint.Types as F
-import Language.Fixpoint.Names      (symSepName, isSuffixOfSym, singletonSym)
+import Language.Fixpoint.Names      (symSepName, isSuffixOfSym, singletonSym, funConName, listConName, tupConName)
 import CoreSyn (CoreBind)
 
-import System.Directory (canonicalizePath)
+import Language.Haskell.Liquid.GhcMisc (isFractionalClass)
+
 import System.FilePath ((</>), isAbsolute, takeDirectory)
-import System.Posix.Files (getFileStatus, isDirectory)
 
 import Data.Default
 -----------------------------------------------------------------------------
@@ -251,6 +254,8 @@
   , binders        :: [String]   -- ^ set of binders to check
   , noCheckUnknown :: Bool       -- ^ whether to complain about specifications for unexported and unused values
   , notermination  :: Bool       -- ^ disable termination check
+  , nowarnings     :: Bool       -- ^ disable warnings output (only show errors)
+  , trustinternals :: Bool       -- ^ type all internal variables with true
   , nocaseexpand   :: Bool       -- ^ disable case expand
   , strata         :: Bool       -- ^ enable strata analysis
   , notruetypes    :: Bool       -- ^ disable truing top level types
@@ -264,21 +269,7 @@
   , cFiles         :: [String]   -- ^ .c files to compile and link against (for GHC)
   } deriving (Data, Typeable, Show, Eq)
 
--- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have
---   to worry about relative paths.
-canonicalizePaths :: Config -> FilePath -> IO Config
-canonicalizePaths cfg tgt
-  = do st  <- getFileStatus tgt
-       tgt <- canonicalizePath tgt
-       let canonicalize f
-             | isAbsolute f   = return f
-             | isDirectory st = canonicalizePath (tgt </> f)
-             | otherwise      = canonicalizePath (takeDirectory tgt </> f)
-       is <- mapM canonicalize $ idirs cfg
-       cs <- mapM canonicalize $ cFiles cfg
-       return $ cfg { idirs = is, cFiles = cs }
 
-
 -----------------------------------------------------------------------------
 -- | Printer ----------------------------------------------------------------
 -----------------------------------------------------------------------------
@@ -346,7 +337,7 @@
   , asmSigs    :: ![(Var, Located SpecType)]     -- ^ Assumed Reftypes
   , ctors      :: ![(Var, Located SpecType)]     -- ^ Data Constructor Measure Sigs
                                                  -- eg.  (:) :: a -> xs:[a] -> {v: Int | v = 1 + len(xs) }
-  , meas       :: ![(Symbol, Located RefType)]   -- ^ Measure Types  
+  , meas       :: ![(Symbol, Located SpecType)]  -- ^ Measure Types  
                                                  -- eg.  len :: [a] -> Int
   , invariants :: ![Located SpecType]            -- ^ Data Type Invariants
 
@@ -386,8 +377,8 @@
                          , freeTyVars :: ![RTyVar]
                          , freePred   :: ![PVar RSort]
                          , freeLabels :: ![Symbol]
-                         , tyConsts   :: ![SpecType]
-                         , tyArgs     :: ![(Symbol, SpecType)]
+                         , tyConsts   :: ![SpecType] -- ^ FIXME: WHAT IS THIS??
+                         , tyArgs     :: ![(Symbol, SpecType)] -- ^ These are backwards, why??
                          , tyRes      :: !SpecType
                          } deriving (Data, Typeable)
 
@@ -511,6 +502,8 @@
 
 -- | Accessors for @RTyCon@
 
+
+isClassRTyCon = isClassTyCon . rtc_tc
 rTyConInfo   = rtc_info 
 rTyConTc     = rtc_tc
 rTyConPVs    = rtc_pvars
@@ -599,11 +592,6 @@
     , rt_reft   :: !r
     }
 
-  | RCls  { 
-      rt_class  :: !p
-    , rt_args   :: ![RType p c tv r]
-    }
-
   | RAllE { 
       rt_bind   :: !Symbol
     , rt_allarg :: !(RType p c tv r)
@@ -711,7 +699,6 @@
 type PrType     = RRType    Predicate
 type BareType   = BRType    RReft
 type SpecType   = RRType    RReft 
-type RefType    = RRType    Reft
 type SpecProp   = RRProp    RReft
 type RRProp r   = Ref       RSort r (RRType r)
 
@@ -736,7 +723,15 @@
   isList   :: c -> Bool
   isTuple  :: c -> Bool
   ppTycon  :: c -> Doc
+  isClass  :: c -> Bool
 
+  isNumCls  :: c -> Bool
+  isFracCls :: c -> Bool
+
+  isClass   = const False
+  isNumCls  = const False
+  isFracCls = const False
+
 class ( TyConable c
       , Eq p, Eq c, Eq tv
       , Hashable tv
@@ -747,6 +742,50 @@
     ppCls    :: p -> [RType p c tv r] -> Doc
     ppRType  :: Prec -> RType p c tv r -> Doc 
 
+
+
+-------------------------------------------------------------------------------
+-- | TyConable Instances -------------------------------------------------------
+-------------------------------------------------------------------------------
+
+-- MOVE TO TYPES
+instance TyConable RTyCon where
+  isFun      = isFunTyCon . rtc_tc
+  isList     = (listTyCon ==) . rtc_tc
+  isTuple    = TyCon.isTupleTyCon   . rtc_tc 
+  isClass    = isClassRTyCon
+  ppTycon    = toFix 
+
+  isNumCls c  = maybe False isNumericClass    (tyConClass_maybe $ rtc_tc c)
+  isFracCls c = maybe False isFractionalClass (tyConClass_maybe $ rtc_tc c)
+
+-- MOVE TO TYPES
+instance TyConable Symbol where
+  isFun   s = funConName == s
+  isList  s = listConName == s
+  isTuple s = tupConName == s
+  ppTycon = text . symbolString
+
+instance TyConable LocSymbol where
+  isFun   = isFun . val
+  isList  = isList . val
+  isTuple = isTuple . val
+  ppTycon = ppTycon . val
+
+
+instance Eq RTyCon where
+  x == y = rtc_tc x == rtc_tc y
+
+instance Fixpoint RTyCon where
+  toFix (RTyCon c _ _) = text $ showPpr c -- <+> text "\n<<" <+> hsep (map toFix ts) <+> text ">>\n"
+
+
+instance PPrint RTyCon where
+  pprint = toFix
+
+instance Show RTyCon where
+  show = showpp  
+
 --------------------------------------------------------------------------
 -- | Values Related to Specifications ------------------------------------
 --------------------------------------------------------------------------
@@ -852,10 +891,15 @@
 bkUniv (RAllS s t)      = let (αs, πs, ss, t') = bkUniv t in  (αs, πs, s:ss, t') 
 bkUniv t                = ([], [], [], t)
 
-bkClass (RFun _ (RCls c t) t' _) = let (cs, t'') = bkClass t' in ((c, t):cs, t'')
-bkClass t                        = ([], t)
+bkClass (RFun _ (RApp c t _ _) t' _)  
+  | isClass c 
+  = let (cs, t'') = bkClass t' in ((c, t):cs, t'')
+bkClass t                                              
+  = ([], t)
 
 rFun b t t' = RFun b t t' mempty
+rCls c ts   = RApp (RTyCon c [] defaultTyConInfo) ts [] mempty
+rRCls rc ts = RApp rc ts [] mempty
 
 addTermCond = addObligation OTerm
 
@@ -1008,7 +1052,6 @@
 emapReft f γ (RAllS p t)         = RAllS p (emapReft f γ t)
 emapReft f γ (RFun x t t' r)     = RFun  x (emapReft f γ t) (emapReft f (x:γ) t') (f γ r)
 emapReft f γ (RApp c ts rs r)    = RApp  c (emapReft f γ <$> ts) (emapRef f γ <$> rs) (f γ r)
-emapReft f γ (RCls c ts)         = RCls  c (emapReft f γ <$> ts) 
 emapReft f γ (RAllE z t t')      = RAllE z (emapReft f γ t) (emapReft f γ t')
 emapReft f γ (REx z t t')        = REx   z (emapReft f γ t) (emapReft f γ t')
 emapReft _ _ (RExprArg e)        = RExprArg e
@@ -1048,7 +1091,6 @@
 mapReftM f (RAllS s t)        = liftM   (RAllS s)   (mapReftM f t)
 mapReftM f (RFun x t t' r)    = liftM3  (RFun x)    (mapReftM f t)          (mapReftM f t')       (f r)
 mapReftM f (RApp c ts rs r)   = liftM3  (RApp  c)   (mapM (mapReftM f) ts)  (mapM (mapRefM f) rs) (f r)
-mapReftM f (RCls c ts)        = liftM   (RCls  c)   (mapM (mapReftM f) ts) 
 mapReftM f (RAllE z t t')     = liftM2  (RAllE z)   (mapReftM f t)          (mapReftM f t')
 mapReftM f (REx z t t')       = liftM2  (REx z)     (mapReftM f t)          (mapReftM f t')
 mapReftM _ (RExprArg e)       = return  $ RExprArg e 
@@ -1071,11 +1113,11 @@
     go γ z (RAllT _ t)                  = go γ z t
     go γ z (RAllP p t)                  = go (fp p γ) z t
     go γ z (RAllS s t)                  = go γ z t
-    go γ z me@(RFun _ (RCls c ts) t' r) = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t') 
+    go γ z me@(RFun _ (RApp c ts _ _) t' r) 
+       | isClass c                      = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t')       
     go γ z me@(RFun x t t' r)           = f γ (Just me) r (go (insertSEnv x (g t) γ) (go γ z t) t')
     go γ z me@(RApp _ ts rs r)          = f γ (Just me) r (ho' γ (go' (insertSEnv (rTypeValueVar me) (g me) γ) z ts) rs)
     
-    go γ z (RCls c ts)                  = go' γ z ts
     go γ z (RAllE x t t')               = go (insertSEnv x (g t) γ) (go γ z t) t' 
     go γ z (REx x t t')                 = go (insertSEnv x (g t) γ) (go γ z t) t' 
     go _ z (ROth _)                     = z 
@@ -1085,7 +1127,7 @@
     go γ z me@(RHole r)                 = f γ (Just me) r z
 
     -- folding over Ref 
-    ho  γ z (RPropP ss r)                = f (insertsSEnv γ (mapSnd (g . ofRSort) <$> ss)) Nothing r z
+    ho  γ z (RPropP ss r)               = f (insertsSEnv γ (mapSnd (g . ofRSort) <$> ss)) Nothing r z
     ho  γ z (RProp ss t)                = go (insertsSEnv γ ((mapSnd (g . ofRSort)) <$> ss)) z t
    
     -- folding over [RType]
@@ -1101,7 +1143,6 @@
 mapBot f (RFun x t t' r)   = RFun x (mapBot f t) (mapBot f t') r
 mapBot f (RAppTy t t' r)   = RAppTy (mapBot f t) (mapBot f t') r
 mapBot f (RApp c ts rs r)  = f $ RApp c (mapBot f <$> ts) (mapBotRef f <$> rs) r
-mapBot f (RCls c ts)       = RCls c (mapBot f <$> ts)
 mapBot f (REx b t1 t2)     = REx b  (mapBot f t1) (mapBot f t2)
 mapBot f (RAllE b t1 t2)   = RAllE b  (mapBot f t1) (mapBot f t2)
 mapBot f t'                = f t' 
@@ -1113,7 +1154,6 @@
 mapBind f (RAllS s t)      = RAllS s (mapBind f t)
 mapBind f (RFun b t1 t2 r) = RFun (f b)  (mapBind f t1) (mapBind f t2) r
 mapBind f (RApp c ts rs r) = RApp c (mapBind f <$> ts) (mapBindRef f <$> rs) r
-mapBind f (RCls c ts)      = RCls c (mapBind f <$> ts)
 mapBind f (RAllE b t1 t2)  = RAllE  (f b) (mapBind f t1) (mapBind f t2)
 mapBind f (REx b t1 t2)    = REx    (f b) (mapBind f t1) (mapBind f t2)
 mapBind _ (RVar α r)       = RVar α r
@@ -1142,7 +1182,6 @@
 stripQuantifiers (RFun x t t' r)  = RFun x (stripQuantifiers t) (stripQuantifiers t') r
 stripQuantifiers (RAppTy t t' r)  = RAppTy (stripQuantifiers t) (stripQuantifiers t') r
 stripQuantifiers (RApp c ts rs r) = RApp c (stripQuantifiers <$> ts) (stripQuantifiersRef <$> rs) r
-stripQuantifiers (RCls c ts)      = RCls c (stripQuantifiers <$> ts)
 stripQuantifiers t                = t
 stripQuantifiersRef (RProp s t)   = RProp s $ stripQuantifiers t
 stripQuantifiersRef r             = r
@@ -1327,22 +1366,21 @@
 
 -- | INVARIANT : all Error constructors should have a pos field
 data TError t = 
-    ErrSubType  { pos  :: !SrcSpan
-                , msg  :: !Doc 
-                , ctx  :: !(M.HashMap Symbol t) 
-                , tact :: !t
-                , texp :: !t
-                } -- ^ liquid type error
-
-   | ErrAssType { pos :: !SrcSpan
-                , obl :: !Oblig
-                , msg :: !Doc
-                , ref :: !RReft
-                } -- ^ liquid type error
+    ErrSubType { pos  :: !SrcSpan
+               , msg  :: !Doc 
+               , ctx  :: !(M.HashMap Symbol t) 
+               , tact :: !t
+               , texp :: !t
+               } -- ^ liquid type error
+  | ErrAssType { pos :: !SrcSpan
+               , obl :: !Oblig
+               , msg :: !Doc
+               , ref :: !RReft
+               } -- ^ liquid type error
 
   | ErrParse    { pos :: !SrcSpan
                 , msg :: !Doc
-                , err :: !LParseError
+                , err :: !ParseError
                 } -- ^ specification parse error
 
   | ErrTySpec   { pos :: !SrcSpan
@@ -1383,6 +1421,11 @@
                 , msg :: !Doc
                 } -- ^ Measure sort error
 
+  | ErrHMeas    { pos :: !SrcSpan
+                , ms  :: !Symbol
+                , msg :: !Doc
+                } -- ^ Haskell bad Measure error
+
   | ErrUnbound  { pos :: !SrcSpan
                 , var :: !Doc
                 } -- ^ Unbound symbol in specification 
@@ -1397,17 +1440,30 @@
                 , texp :: !t
                 } -- ^ Mismatch between Liquid and Haskell types
 
+  | ErrAliasApp { pos   :: !SrcSpan
+                , nargs :: !Int
+                , dname :: !Doc
+                , dpos  :: !SrcSpan
+                , dargs :: !Int
+                }
+
   | ErrSaved    { pos :: !SrcSpan 
                 , msg :: !Doc
-                } -- ^ Unexpected PANIC 
- 
+                } -- ^ Previously saved error, that carries over after DiffCheck
+
+  
+  | ErrTermin   { bind :: ![Var]
+                , pos  :: !SrcSpan
+                , msg  :: !Doc
+                } -- ^ Termination Error 
+
   | ErrOther    { pos :: !SrcSpan
                 , msg :: !Doc
                 } -- ^ Unexpected PANIC 
   deriving (Typeable, Functor)
 
-data LParseError = LPE !SourcePos [String] 
-                   deriving (Data, Typeable, Generic)
+-- data LParseError = LPE !SourcePos [String] 
+--                    deriving (Data, Typeable, Generic)
 
 
 instance Eq Error where
@@ -1492,16 +1548,22 @@
 type RTPredAlias  = Either (ModName, RTAlias Symbol Pred)
                            (RTAlias Symbol Pred)
 
+type RTExprAlias  = Either (ModName, RTAlias Symbol Expr)
+                           (RTAlias Symbol Expr)
+
 data RTEnv   = RTE { typeAliases :: M.HashMap Symbol RTBareOrSpec
                    , predAliases :: M.HashMap Symbol RTPredAlias
+                   , exprAliases :: M.HashMap Symbol RTExprAlias
                    }
 
 instance Monoid RTEnv where
-  (RTE ta1 pa1) `mappend` (RTE ta2 pa2) = RTE (ta1 `M.union` ta2) (pa1 `M.union` pa2)
-  mempty = RTE M.empty M.empty
+  (RTE ta1 pa1 ea1) `mappend` (RTE ta2 pa2 ea2)
+    = RTE (ta1 `M.union` ta2) (pa1 `M.union` pa2) (ea1 `M.union` ea2)
+  mempty = RTE M.empty M.empty M.empty
 
 mapRT f e = e { typeAliases = f $ typeAliases e }
 mapRP f e = e { predAliases = f $ predAliases e }
+mapRE f e = e { exprAliases = f $ exprAliases e }
 
 cinfoError (Ci _ (Just e)) = e
 cinfoError (Ci l _)        = errOther $ text $ "Cinfo:" ++ showPpr l
@@ -1569,6 +1631,7 @@
   subst su (R s e) = R s $ subst su e
 
 
+
 data RClass ty
   = RClass { rcName    :: LocSymbol
            , rcSupers  :: [ty]
@@ -1579,7 +1642,6 @@
 instance Functor RClass where
   fmap f (RClass n ss tvs ms) = RClass n (fmap f ss) tvs (fmap (second f) ms)
 
-
 ------------------------------------------------------------------------
 -- | Annotations -------------------------------------------------------
 ------------------------------------------------------------------------
@@ -1613,7 +1675,7 @@
 ------------------------------------------------------------------------
 
 data Output a = O { o_vars   :: Maybe [String]
-                  , o_warns  :: [String]
+                  , o_errors :: ! [Error]
                   , o_types  :: !(AnnInfo a)
                   , o_templs :: !(AnnInfo a)
                   , o_bots   :: ![SrcSpan] 
@@ -1625,7 +1687,7 @@
 instance Monoid (Output a) where 
   mempty        = emptyOutput  
   mappend o1 o2 = O { o_vars   = sortNub <$> mappend (o_vars   o1) (o_vars   o2)
-                    , o_warns  = sortNub  $  mappend (o_warns  o1) (o_warns  o2)
+                    , o_errors = sortNub  $  mappend (o_errors o1) (o_errors o2)
                     , o_types  =             mappend (o_types  o1) (o_types  o2) 
                     , o_templs =             mappend (o_templs o1) (o_templs o2) 
                     , o_bots   = sortNub  $  mappend (o_bots o1)   (o_bots   o2)
@@ -1678,9 +1740,9 @@
 
 hasHole (toReft -> (Reft (_, rs))) = any isHole rs
 
-classToRApp :: SpecType -> SpecType
-classToRApp (RCls cl ts) 
-  = RApp (RTyCon (classTyCon cl) def def) ts mempty mempty
+-- classToRApp :: SpecType -> SpecType
+-- classToRApp (RCls cl ts) 
+--   = RApp (RTyCon (classTyCon cl) def def) ts mempty mempty
 
 instance Symbolic DataCon where
   symbol = symbol . dataConWorkId
diff --git a/syntax/flycheck-liquid.el b/syntax/flycheck-liquid.el
new file mode 100644
--- /dev/null
+++ b/syntax/flycheck-liquid.el
@@ -0,0 +1,86 @@
+;;; 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
new file mode 100644
--- /dev/null
+++ b/syntax/haskell.vim
@@ -0,0 +1,379 @@
+" 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
new file mode 100644
--- /dev/null
+++ b/syntax/liquid-tip.el
@@ -0,0 +1,281 @@
+;;; 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 'json)
+(require 'pos-tip nil t)
+(require 'thingatpt)
+(require 'button-lock nil t)
+
+;; (require 'json-mode)
+;; (require 'ring)
+;; (require 'etags)
+;; (require 'flymake)
+;; (require 'eldoc)
+;; (require 'log4e)
+;; (require 'yaxception)
+
+;; ------------------------------------------------------------------------
+;; 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)
+        (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)
+	 ;; DEBUG (button-lock-set-button "yoga" 'liquid-tip-show)
+	 ;; DEBUG (button-lock-set-button "mydiv" 'liquid-tip-show)
+	 ))
+
+;;;###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)))
+
+;; DEBUG (defface my-tooltip
+;; DEBUG   '((t
+;; DEBUG      :background "gray85"
+;; DEBUG      :foreground "black"
+;; DEBUG      :inherit variable-pitch))
+;; DEBUG   "Face for my tooltip.")
+;; DEBUG 
+;; DEBUG (defface my-tooltip-highlight
+;; DEBUG   '((t
+;; DEBUG      :background "blue"
+;; DEBUG      :foreground "white"
+;; DEBUG      :inherit my-tooltip))
+;; DEBUG   "Face for my tooltip highlighted.")
+;; DEBUG 
+;; DEBUG (let ((str (propertize "foo\nbar\nbaz" 'face 'my-tooltip)))
+;; DEBUG   (put-text-property 6 11 'face 'my-tooltip-highlight str)
+;; DEBUG   (pos-tip-show-no-propertize str 'my-tooltip))
+
+(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
new file mode 100644
--- /dev/null
+++ b/syntax/liquid.vim
@@ -0,0 +1,47 @@
+"============================================================================
+"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
@@ -1,13 +1,20 @@
+{-# LANGUAGE DeriveDataTypeable  #-}
+{-# LANGUAGE DoAndIfThenElse     #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 module Main where
 
 import Control.Applicative
 import Control.Monad
+import Data.Char
 import Data.Proxy
+import Data.Tagged
+import Data.Typeable
+import Options.Applicative
 import System.Directory
 import System.Exit
 import System.FilePath
 import System.IO
-import qualified System.Posix as Posix
+-- import qualified System.Posix as Posix
 import System.Process
 import Test.Tasty
 import Test.Tasty.HUnit
@@ -16,44 +23,29 @@
 import Test.Tasty.Runners
 import Text.Printf
 
--- main
---   = do pos         <- dirTests "tests/pos"   [] ExitSuccess
---        neg         <- dirTests "tests/neg"   [] (ExitFailure 1)
---        crash       <- dirTests "tests/crash" [] (ExitFailure 2)
---        -- benchmarks
---        text        <- dirTests "benchmarks/text-0.11.2.3"             textIgnored  ExitSuccess
---        bs          <- dirTests "benchmarks/bytestring-0.9.2.1"        []           ExitSuccess
---        esop        <- dirTests "benchmarks/esop2013-submission"       ["Base0.hs"] ExitSuccess
---        vector_algs <- dirTests "benchmarks/vector-algorithms-0.5.4.2" []           ExitSuccess
---        hscolour    <- dirTests "benchmarks/hscolour-1.20.0.0"         []           ExitSuccess
---        -- TestTrees
---        let unit = testGroup "Unit"
---                     [ testGroup "pos" pos
---                     , testGroup "neg" neg
---                     , testGroup "crash" crash
---                     ]
---        let bench = testGroup "Benchmarks"
---                      [ testGroup "text" text
---                      , testGroup "bytestring" bs
---                      , testGroup "esop" esop
---                      , testGroup "vector-algorithms" vector_algs
---                      , testGroup "hscolour" hscolour
---                      ]
---        defaultMainWithIngredients
---          [ rerunningTests [ listingTests, consoleTestReporter ]
---          , includingOptions [ Option (Proxy :: Proxy NumThreads) ]
---          ] $ testGroup "Tests" [ unit, bench ]
-
 main :: IO ()
 main = run =<< tests 
   where
     run   = defaultMainWithIngredients [ 
                 rerunningTests   [ listingTests, consoleTestReporter ]
-              , includingOptions [ Option (Proxy :: Proxy NumThreads) ]
+              , includingOptions [ Option (Proxy :: Proxy NumThreads)
+                                 , Option (Proxy :: Proxy SmtSolver) ]
               ]
     
     tests = group "Tests" [ unitTests, benchTests ]
 
+data SmtSolver = Z3 | CVC4 deriving (Show, Read, Eq, Ord, Typeable)
+instance IsOption SmtSolver where
+  defaultValue = Z3
+  parseValue = safeRead . map toUpper
+  optionName = return "smtsolver"
+  optionHelp = return "Use this SMT solver"
+  optionCLParser =
+    option (fmap (read . map toUpper) str)
+      (  long (untag (optionName :: Tagged SmtSolver String))
+      <> help (untag (optionHelp :: Tagged SmtSolver String))
+      )
+
 unitTests  
   = group "Unit" [ 
       testGroup "pos"         <$> dirTests "tests/pos"                            []           ExitSuccess
@@ -82,28 +74,35 @@
 isTest   :: FilePath -> Bool
 isTest f = takeExtension f == ".hs" -- `elem` [".hs", ".lhs"]
 
-
-
 ---------------------------------------------------------------------------
 mkTest :: ExitCode -> FilePath -> FilePath -> TestTree
 ---------------------------------------------------------------------------
 mkTest code dir file
-  = testCase file $ do
-      createDirectoryIfMissing True $ takeDirectory log
-      liquid <- canonicalizePath "dist/build/liquid/liquid"
-      withFile log WriteMode $ \h -> do
-        let cmd     = testCmd liquid dir file
-        (_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}
-        c          <- waitForProcess ph
-        assertEqual "Wrong exit code" code c
+  = askOption $ \(smt :: SmtSolver) -> testCase file $ do
+      if test `elem` knownToFail smt
+      then do
+        printf "%s is known to fail with %s: SKIPPING" test (show smt)
+        assertEqual "" True True
+      else do
+        createDirectoryIfMissing True $ takeDirectory log
+        liquid <- canonicalizePath "dist/build/liquid/liquid"
+        withFile log WriteMode $ \h -> do
+          let cmd     = testCmd liquid dir file smt
+          (_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}
+          c          <- waitForProcess ph
+          assertEqual "Wrong exit code" code c
   where
+    test = dir </> file
     log = let (d,f) = splitFileName file in dir </> d </> ".liquid" </> f <.> "log"
 
+knownToFail CVC4 = [ "tests/pos/RealProps.hs", "tests/pos/RealProps1.hs", "tests/pos/initarray.hs" ]
+knownToFail Z3   = []
 
 ---------------------------------------------------------------------------
-testCmd :: FilePath -> FilePath -> FilePath -> String
+testCmd :: FilePath -> FilePath -> FilePath -> SmtSolver -> String
 ---------------------------------------------------------------------------
-testCmd liquid dir file = printf "cd %s && %s --verbose %s" dir liquid file
+testCmd liquid dir file smt 
+  = printf "cd %s && %s --verbose --smtsolver %s %s" dir liquid (show smt) file
 
 
 textIgnored = [ "Data/Text/Axioms.hs"
@@ -152,7 +151,7 @@
 walkDirectory :: FilePath -> IO [FilePath]
 ----------------------------------------------------------------------------------------
 walkDirectory root
-  = do (ds,fs) <- partitionM isDirectory . candidates =<< getDirectoryContents root
+  = do (ds,fs) <- partitionM doesDirectoryExist . candidates =<< getDirectoryContents root
        (fs++) <$> concatMapM walkDirectory ds
   where
     candidates fs = [root </> f | f <- fs, not (isExtSeparator (head f))]
@@ -165,8 +164,8 @@
                          if b then go (x:ls) rs xs
                               else go ls (x:rs) xs
 
-isDirectory :: FilePath -> IO Bool
-isDirectory = fmap Posix.isDirectory . Posix.getFileStatus
+-- isDirectory :: FilePath -> IO Bool
+-- isDirectory = fmap Posix.isDirectory . Posix.getFileStatus
 
 concatMapM :: Applicative m => (a -> m [b]) -> [a] -> m [b]
 concatMapM f []     = pure []