diff --git a/liquid-fixpoint b/liquid-fixpoint
index e7521c124d..08a09adfa8 160000
--- a/liquid-fixpoint
+++ b/liquid-fixpoint
@@ -1 +1 @@
-Subproject commit e7521c124d12f3d572ce76845aad66a0cb4da07e
+Subproject commit 08a09adfa8a47ae2018b2b18eeacb7ad2d322adf
diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal
index dc531712ad..53410f692e 100644
--- a/liquidhaskell.cabal
+++ b/liquidhaskell.cabal
@@ -91,6 +91,8 @@ library
                       Language.Haskell.Liquid.Bare.Resolve
                       Language.Haskell.Liquid.Bare.ToBare
                       Language.Haskell.Liquid.Bare.Types
+                      Language.Haskell.Liquid.Bare.Typeclass
+                      Language.Haskell.Liquid.Bare.Elaborate
                       Language.Haskell.Liquid.Constraint.Constraint
                       Language.Haskell.Liquid.Constraint.Env
                       Language.Haskell.Liquid.Constraint.Fresh
@@ -127,6 +129,7 @@ library
                       Language.Haskell.Liquid.Transforms.RefSplit
                       Language.Haskell.Liquid.Transforms.Rewrite
                       Language.Haskell.Liquid.Transforms.Simplify
+                      Language.Haskell.Liquid.Transforms.InlineAux
                       Language.Haskell.Liquid.Types
                       Language.Haskell.Liquid.Types.Bounds
                       Language.Haskell.Liquid.Types.Dictionaries
@@ -193,6 +196,8 @@ library
                     , transformers         >= 0.3
                     , unordered-containers >= 0.2
                     , vector               >= 0.10
+                    , recursion-schemes
+                    , free
   default-language:   Haskell98
   default-extensions: PatternGuards
   ghc-options:        -W -fwarn-missing-signatures
diff --git a/src/Language/Haskell/Liquid/Bare.hs b/src/Language/Haskell/Liquid/Bare.hs
index 4175ff4a1a..5f693c09c8 100644
--- a/src/Language/Haskell/Liquid/Bare.hs
+++ b/src/Language/Haskell/Liquid/Bare.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE FlexibleContexts          #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
 {-# LANGUAGE TupleSections             #-}
 {-# LANGUAGE RecordWildCards           #-}
 {-# LANGUAGE ViewPatterns              #-}
@@ -27,7 +28,7 @@ module Language.Haskell.Liquid.Bare (
 
 import           Prelude                                    hiding (error)
 import           Optics
-import           Control.Monad                              (unless)
+import           Control.Monad                              (unless, when, void, forM)
 import qualified Control.Exception                          as Ex
 import qualified Data.Binary                                as B
 import qualified Data.Maybe                                 as Mb
@@ -49,7 +50,8 @@ import           Language.Haskell.Liquid.WiredIn
 import qualified Language.Haskell.Liquid.Measure            as Ms
 import qualified Language.Haskell.Liquid.Bare.Types         as Bare 
 import qualified Language.Haskell.Liquid.Bare.Resolve       as Bare 
-import qualified Language.Haskell.Liquid.Bare.DataType      as Bare 
+import qualified Language.Haskell.Liquid.Bare.DataType      as Bare
+import           Language.Haskell.Liquid.Bare.Elaborate
 import qualified Language.Haskell.Liquid.Bare.Expand        as Bare 
 import qualified Language.Haskell.Liquid.Bare.Measure       as Bare 
 import qualified Language.Haskell.Liquid.Bare.Plugged       as Bare 
@@ -57,7 +59,8 @@ import qualified Language.Haskell.Liquid.Bare.Axiom         as Bare
 import qualified Language.Haskell.Liquid.Bare.ToBare        as Bare 
 import qualified Language.Haskell.Liquid.Bare.Class         as Bare 
 import qualified Language.Haskell.Liquid.Bare.Check         as Bare 
-import qualified Language.Haskell.Liquid.Bare.Laws          as Bare 
+import qualified Language.Haskell.Liquid.Bare.Laws          as Bare
+import qualified Language.Haskell.Liquid.Bare.Typeclass     as Bare 
 import qualified Language.Haskell.Liquid.Transforms.CoreToLogic as CoreToLogic 
 import           Control.Arrow                    (second)
 
@@ -110,12 +113,37 @@ makeTargetSpec :: Config
                -> TargetSrc
                -> BareSpec
                -> TargetDependencies
-               -> Either [Error] (TargetSpec, LiftedSpec)
-makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do
+               -> Ghc.Ghc (Either [Error] (TargetSpec, LiftedSpec))
+makeTargetSpec cfg lmap targetSrc bareSpec dependencies = 
   -- Check that our input 'BareSpec' doesn't contain duplicates.
-  validatedBareSpec <- Bare.checkBareSpec (giTargetMod targetSrc) (review bareSpecIso bareSpec)
-  ghcSpec           <- makeGhcSpec cfg (review targetSrcIso targetSrc) lmap (allSpecs validatedBareSpec)
-  pure $ view targetSpecGetter ghcSpec
+  case Bare.checkBareSpec (giTargetMod targetSrc) (review bareSpecIso bareSpec) of
+    Left errs -> pure $ Left errs
+    Right validatedBareSpec -> do
+      -- we should be able to setContext regardless of whether
+      -- we use the ghc api. However, ghc will complain
+      -- if the filename does not match the module name
+      when (typeclass cfg) $ do
+        Ghc.setContext [iimport |(modName, _) <- allSpecs validatedBareSpec,
+                        let iimport = if isTarget modName
+                                      then Ghc.IIModule (getModName modName)
+                                      else Ghc.IIDecl (Ghc.simpleImportDecl (getModName modName))]
+        void $ Ghc.execStmt
+          "let {infixr 1 ==>; True ==> False = False; _ ==> _ = True}"
+          Ghc.execOptions
+        void $ Ghc.execStmt
+          "let {infixr 1 <=>; True <=> False = False; _ <=> _ = True}"
+          Ghc.execOptions
+        void $ Ghc.execStmt
+          "let {infix 4 ==; (==) :: a -> a -> Bool; _ == _ = undefined}"
+          Ghc.execOptions
+        void $ Ghc.execStmt
+          "let {infix 4 /=; (/=) :: a -> a -> Bool; _ /= _ = undefined}"
+          Ghc.execOptions
+        void $ Ghc.execStmt
+          "let {infixl 7 /; (/) :: Num a => a -> a -> a; _ / _ = undefined}"
+          Ghc.execOptions        
+      ghcSpec <- makeGhcSpec cfg (review targetSrcIso targetSrc) lmap (allSpecs validatedBareSpec)
+      pure $ view targetSpecGetter <$> ghcSpec
   where
     toLegacyDep :: (StableModule, LiftedSpec) -> (ModName, Ms.BareSpec)
     toLegacyDep (sm, ls) = (ModName SrcImport (Ghc.moduleName . unStableModule $ sm), unsafeFromLiftedSpec ls)
@@ -135,20 +163,20 @@ makeGhcSpec :: Config
             -> GhcSrc 
             -> LogicMap 
             -> [(ModName, Ms.BareSpec)] 
-            -> Either [Error] GhcSpec
+            -> Ghc.Ghc (Either [Error] GhcSpec)
 -------------------------------------------------------------------------------------
 makeGhcSpec cfg src lmap mspecs0  = do
-  _validTargetSpec <- Bare.checkTargetSpec (map snd mspecs) 
+  sp     <- makeGhcSpec0 cfg src lmap mspecs
+  let renv             = ghcSpecEnv sp 
+      _validTargetSpec = Bare.checkTargetSpec (map snd mspecs) 
                                            (view targetSrcIso src)
                                            renv 
                                            cbs 
                                            (fst . view targetSpecGetter $ sp)
-  pure sp
+  pure (_validTargetSpec >> pure sp)
   where 
     mspecs =  [ (m, checkThrow $ Bare.checkBareSpec m sp) | (m, sp) <- mspecs0, isTarget m ] 
            ++ [ (m, sp) | (m, sp) <- mspecs0, not (isTarget m)]
-    sp     = makeGhcSpec0 cfg src lmap mspecs 
-    renv   = ghcSpecEnv sp 
     cbs    = _giCbs src
 
 checkThrow :: Ex.Exception e => Either e c -> c
@@ -177,50 +205,88 @@ ghcSpecEnv sp = fromListSEnv binds
 --   essentially, to get to the `BareRTEnv` as soon as possible, as thats what
 --   lets us use aliases inside data-constructor definitions.
 -------------------------------------------------------------------------------------
-makeGhcSpec0 :: Config -> GhcSrc ->  LogicMap -> [(ModName, Ms.BareSpec)] -> GhcSpec
+makeGhcSpec0 :: Config -> GhcSrc ->  LogicMap -> [(ModName, Ms.BareSpec)] -> Ghc.Ghc GhcSpec
 -------------------------------------------------------------------------------------
-makeGhcSpec0 cfg src lmap mspecs = SP 
-  { _gsConfig = cfg 
-  , _gsImps   = makeImports mspecs
-  , _gsSig    = addReflSigs refl sig 
-  , _gsRefl   = refl 
-  , _gsLaws   = laws 
-  , _gsData   = sData 
-  , _gsQual   = qual 
-  , _gsName   = makeSpecName env     tycEnv measEnv   name 
-  , _gsVars   = makeSpecVars cfg src mySpec env measEnv
-  , _gsTerm   = makeSpecTerm cfg     mySpec env       name    
-  , _gsLSpec  = makeLiftedSpec   src env refl sData sig qual myRTE lSpec1 {
-                   impSigs   = makeImports mspecs,
-                   expSigs   = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ],
-                   dataDecls = dataDecls mySpec2 
-                   } 
-  }
+makeGhcSpec0 cfg src lmap mspecsNoCls = do
+  tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) coreToLg simplifier
+  let tyi      = Bare.tcTyConMap   tycEnv 
+  let sigEnv   = makeSigEnv  embs tyi (_gsExports src) rtEnv 
+  let lSpec1   = lSpec0 <> makeLiftedSpec1 cfg src tycEnv lmap mySpec1 
+  let mySpec   = mySpec2 <> lSpec1 
+  let specs    = M.insert name mySpec iSpecs2
+  let measEnv  = makeMeasEnv      env tycEnv sigEnv       specs 
+  let sig      = makeSpecSig cfg name specs env sigEnv   tycEnv measEnv (_giCbs src)
+  let myRTE    = myRTEnv       src env sigEnv rtEnv  
+  elaboratedSig<- if allowTC then Bare.makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods
+                              >>= elaborateSig sig
+                             else pure sig
+  let qual     = makeSpecQual cfg env tycEnv measEnv rtEnv specs 
+  let sData    = makeSpecData  src env sigEnv measEnv elaboratedSig specs 
+  let refl     = makeSpecRefl  cfg src measEnv specs env name elaboratedSig tycEnv 
+  let laws     = makeSpecLaws env sigEnv (gsTySigs elaboratedSig ++ gsAsmSigs elaboratedSig) measEnv specs 
+  pure $ SP 
+    { _gsConfig = cfg 
+    , _gsImps   = makeImports mspecs
+    , _gsSig    = addReflSigs refl elaboratedSig
+    , _gsRefl   = refl 
+    , _gsLaws   = laws 
+    , _gsData   = sData 
+    , _gsQual   = qual 
+    , _gsName   = makeSpecName env     tycEnv measEnv   name 
+    , _gsVars   = makeSpecVars cfg src mySpec env measEnv
+    , _gsTerm   = makeSpecTerm cfg     mySpec env       name    
+    , _gsLSpec  = makeLiftedSpec   src env refl sData elaboratedSig qual myRTE lSpec1 {
+                     impSigs   = makeImports mspecs,
+                     expSigs   = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ],
+                     dataDecls = dataDecls mySpec2 
+                     } 
+    }
   where
-    -- build up spec components 
-    myRTE    = myRTEnv       src env sigEnv rtEnv  
-    qual     = makeSpecQual cfg env tycEnv measEnv rtEnv specs 
-    sData    = makeSpecData  src env sigEnv measEnv sig specs 
-    refl     = makeSpecRefl  cfg src measEnv specs env name sig tycEnv 
-    laws     = makeSpecLaws env sigEnv (gsTySigs sig ++ gsAsmSigs sig) measEnv specs 
-    sig      = makeSpecSig cfg name specs env sigEnv   tycEnv measEnv (_giCbs src)
-    measEnv  = makeMeasEnv      env tycEnv sigEnv       specs 
+    -- typeclass elaboration
+    allowTC    = typeclass cfg
+    simplifier :: Ghc.CoreExpr -> Ghc.Ghc Ghc.CoreExpr
+    simplifier = pure -- no simplification
+    coreToLg e =
+      case CoreToLogic.runToLogic
+             embs
+             lmap
+             dm
+             (\x -> todo Nothing ("coreToLogic not working " ++ x))
+             (CoreToLogic.coreToLogic allowTC e) of
+        Left msg -> panic Nothing (F.showpp msg)
+        Right e -> e    
+    elaborateSig si auxsig = do
+      tySigs <-
+        forM (gsTySigs si) $ \(x, t) ->
+          if Ghc.nameModule (Ghc.getName x) == Ghc.gHC_REAL then
+            pure (x, t)
+          else do t' <- traverse (elaborateSpecType coreToLg simplifier) t
+                  pure (x, t')
+      -- things like len breaks the code
+      -- asmsigs should be elaborated only if they are from the current module
+      -- asmSigs <- forM (gsAsmSigs si) $ \(x, t) -> do
+      --   t' <- traverse (elaborateSpecType (pure ()) coreToLg) t
+      --   pure (x, fst <$> t')
+      pure
+        si
+          { gsTySigs = F.notracepp ("asmSigs" ++ F.showpp (gsAsmSigs si)) tySigs ++ auxsig  }
+
     -- build up environments
-    specs    = M.insert name mySpec iSpecs2
-    mySpec   = mySpec2 <> lSpec1 
-    lSpec1   = lSpec0 <> makeLiftedSpec1 cfg src tycEnv lmap mySpec1 
-    sigEnv   = makeSigEnv  embs tyi (_gsExports src) rtEnv 
-    tyi      = Bare.tcTyConMap   tycEnv 
-    tycEnv   = makeTycEnv   cfg name env embs mySpec2 iSpecs2 
+    (tycEnv0, datacons)   = makeTycEnv0   cfg name env embs mySpec2 iSpecs2 
     mySpec2  = Bare.qualifyExpand env name rtEnv l [] mySpec1    where l = F.dummyPos "expand-mySpec2"
     iSpecs2  = Bare.qualifyExpand env name rtEnv l [] iSpecs0    where l = F.dummyPos "expand-iSpecs2"
     rtEnv    = Bare.makeRTEnv env name mySpec1 iSpecs0 lmap  
+    mspecs   = if allowTC then M.toList $ M.insert name mySpec0 iSpecs0 else mspecsNoCls
+    (mySpec0, instMethods)  = if allowTC
+                              then Bare.compileClasses src env (name, mySpec0NoCls) (M.toList iSpecs0)
+                              else (mySpec0NoCls, [])
     mySpec1  = mySpec0 <> lSpec0    
     lSpec0   = makeLiftedSpec0 cfg src embs lmap mySpec0 
     embs     = makeEmbeds          src env ((name, mySpec0) : M.toList iSpecs0)
+    dm       = Bare.tcDataConMap tycEnv0
     -- extract name and specs
-    env      = Bare.makeEnv cfg src lmap mspecs  
-    (mySpec0, iSpecs0) = splitSpecs name mspecs 
+    env      = Bare.makeEnv cfg src lmap mspecsNoCls
+    (mySpec0NoCls, iSpecs0) = splitSpecs name mspecsNoCls
     -- check barespecs 
     name     = F.notracepp ("ALL-SPECS" ++ zzz) $ _giTargetMod  src 
     zzz      = F.showpp (fst <$> mspecs)
@@ -263,8 +329,8 @@ makeTyConEmbeds env (name, spec)
 --------------------------------------------------------------------------------
 makeLiftedSpec1 :: Config -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec 
                 -> Ms.BareSpec
-makeLiftedSpec1 _ src tycEnv lmap mySpec = mempty
-  { Ms.measures  = Bare.makeHaskellMeasures src tycEnv lmap mySpec }
+makeLiftedSpec1 config src tycEnv lmap mySpec = mempty
+  { Ms.measures  = Bare.makeHaskellMeasures (typeclass config) src tycEnv lmap mySpec }
 
 --------------------------------------------------------------------------------
 -- | [NOTE]: LIFTING-STAGES 
@@ -281,7 +347,7 @@ makeLiftedSpec1 _ src tycEnv lmap mySpec = mempty
 makeLiftedSpec0 :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec 
                 -> Ms.BareSpec
 makeLiftedSpec0 cfg src embs lmap mySpec = mempty
-  { Ms.ealiases  = lmapEAlias . snd <$> Bare.makeHaskellInlines src embs lmap mySpec 
+  { Ms.ealiases  = lmapEAlias . snd <$> Bare.makeHaskellInlines (typeclass cfg) src embs lmap mySpec 
   , Ms.reflects  = Ms.reflects mySpec
   , Ms.dataDecls = Bare.makeHaskellDataDecls cfg name mySpec tcs  
   }
@@ -543,7 +609,7 @@ makeSpecSig cfg name specs env sigEnv tycEnv measEnv cbs = SpSig
   , gsAsmSigs  = F.notracepp "gsAsmSigs" asmSigs
   , gsRefSigs  = [] 
   , gsDicts    = dicts 
-  , gsMethods  = if noclasscheck cfg then [] else Bare.makeMethodTypes dicts (Bare.meClasses  measEnv) cbs 
+  , gsMethods  = if noclasscheck cfg then [] else Bare.makeMethodTypes (typeclass cfg) dicts (Bare.meClasses  measEnv) cbs 
   , gsInSigs   = mempty -- TODO-REBARE :: ![(Var, LocSpecType)]  
   , gsNewTypes = makeNewTypes env sigEnv allSpecs 
   , gsTexprs   = [ (v, t, es) | (v, t, Just es) <- mySigs ] 
@@ -578,12 +644,12 @@ makeMthSigs measEnv = [ (v, t) | (_, v, t) <- Bare.meMethods measEnv ]
 
 makeInlSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)] 
 makeInlSigs env rtEnv 
-  = makeLiftedSigs rtEnv CoreToLogic.inlineSpecType 
+  = makeLiftedSigs rtEnv (CoreToLogic.inlineSpecType (typeclass (getConfig env)))
   . makeFromSet "hinlines" Ms.inlines env 
 
 makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)] 
 makeMsrSigs env rtEnv 
-  = makeLiftedSigs rtEnv CoreToLogic.measureSpecType 
+  = makeLiftedSigs rtEnv (CoreToLogic.inlineSpecType (typeclass (getConfig env)))
   . makeFromSet "hmeas" Ms.hmeas env 
 
 makeLiftedSigs :: BareRTEnv -> (Ghc.Var -> SpecType) -> [Ghc.Var] -> [(Ghc.Var, LocSpecType)]
@@ -767,9 +833,9 @@ makeSpecData :: GhcSrc -> Bare.Env -> Bare.SigEnv -> Bare.MeasEnv -> GhcSpecSig
 ------------------------------------------------------------------------------------------
 makeSpecData src env sigEnv measEnv sig specs = SpData 
   { gsCtors      = -- F.notracepp "GS-CTORS" 
-                   [ (x, tt) 
+                   [ (x, if allowTC then t else tt) 
                        | (x, t) <- Bare.meDataCons measEnv
-                       , let tt  = Bare.plugHoles sigEnv name (Bare.LqTV x) t 
+                       , let tt  = Bare.plugHoles (typeclass $ getConfig env) sigEnv name (Bare.LqTV x) t 
                    ]
   , gsMeas       = [ (F.symbol x, uRType <$> t) | (x, t) <- measVars ] 
   , gsMeasures   = Bare.qualifyTopDummy env name <$> (ms1 ++ ms2)
@@ -778,12 +844,13 @@ makeSpecData src env sigEnv measEnv sig specs = SpData
   , gsUnsorted   = usI ++ (concatMap msUnSorted $ concatMap measures specs)
   }
   where
+    allowTC      = typeclass (getConfig env)
     measVars     = Bare.meSyms      measEnv -- ms'
                 ++ Bare.meClassSyms measEnv -- cms' 
                 ++ Bare.varMeasures env
     measuresSp   = Bare.meMeasureSpec measEnv  
     ms1          = M.elems (Ms.measMap measuresSp)
-    ms2          =          Ms.imeas   measuresSp
+    ms2          = Ms.imeas   measuresSp
     mySpec       = M.lookupDefault mempty name specs
     name         = _giTargetMod      src
     (minvs,usI)  = makeMeasureInvariants env name sig mySpec
@@ -879,15 +946,16 @@ makeSpecName env tycEnv measEnv name = SpNames
 
 
 -- REBARE: formerly, makeGhcCHOP1
+-- split into two to break circular dependency. we need dataconmap for core2logic
 -------------------------------------------------------------------------------------------
-makeTycEnv :: Config -> ModName -> Bare.Env -> TCEmb Ghc.TyCon -> Ms.BareSpec -> Bare.ModSpecs 
-           -> Bare.TycEnv 
+makeTycEnv0 :: Config -> ModName -> Bare.Env -> TCEmb Ghc.TyCon -> Ms.BareSpec -> Bare.ModSpecs 
+           -> (Bare.TycEnv, [Located DataConP] )
 -------------------------------------------------------------------------------------------
-makeTycEnv cfg myName env embs mySpec iSpecs = Bare.TycEnv 
+makeTycEnv0 cfg myName env embs mySpec iSpecs = (,datacons) $ Bare.TycEnv 
   { tcTyCons      = tycons                  
-  , tcDataCons    = val <$> datacons 
+  , tcDataCons    = mempty -- val <$> datacons 
   , tcSelMeasures = dcSelectors             
-  , tcSelVars     = recSelectors            
+  , tcSelVars     = mempty -- recSelectors            
   , tcTyConMap    = tyi                     
   , tcAdts        = adts                    
   , tcDataConMap  = dm
@@ -902,14 +970,34 @@ makeTycEnv cfg myName env embs mySpec iSpecs = Bare.TycEnv
     -- tycons        = F.tracepp "TYCONS" $ Misc.replaceWith tcpCon tcs wiredTyCons
     -- datacons      =  Bare.makePluggedDataCons embs tyi (Misc.replaceWith (dcpCon . val) (F.tracepp "DATACONS" $ concat dcs) wiredDataCons)
     tycons        = tcs ++ knownWiredTyCons env myName 
-    datacons      = Bare.makePluggedDataCon embs tyi <$> (concat dcs ++ knownWiredDataCons env myName)
+    datacons      = Bare.makePluggedDataCon (typeclass cfg) embs tyi <$> (concat dcs ++ knownWiredDataCons env myName)
     tds           = [(name, tcpCon tcp, dd) | (name, tcp, Just dd) <- tcDds]
     adts          = Bare.makeDataDecls cfg embs myName tds       datacons
     dm            = Bare.dataConMap adts
     dcSelectors   = concatMap (Bare.makeMeasureSelectors cfg dm) datacons
-    recSelectors  = Bare.makeRecordSelectorSigs env myName       datacons
     fiTcs         = _gsFiTcs (Bare.reSrc env)
-   
+
+
+makeTycEnv1 ::
+     ModName
+  -> Bare.Env
+  -> (Bare.TycEnv, [Located DataConP])
+  -> (Ghc.CoreExpr -> F.Expr)
+  -> (Ghc.CoreExpr -> Ghc.Ghc Ghc.CoreExpr)
+  -> Ghc.Ghc Bare.TycEnv
+makeTycEnv1 myName env (tycEnv, datacons) coreToLg simplifier = do
+  -- fst for selector generation, snd for dataconsig generation
+  lclassdcs <- forM classdcs $ traverse (Bare.elaborateClassDcp coreToLg simplifier)
+  let recSelectors = Bare.makeRecordSelectorSigs env myName (dcs ++ (fmap . fmap) snd lclassdcs)
+  pure $
+    tycEnv {Bare.tcSelVars = recSelectors, Bare.tcDataCons = F.val <$> ((fmap . fmap) fst lclassdcs ++ dcs )}
+  where
+    (classdcs, dcs) =
+      L.partition
+        (Ghc.isClassTyCon . Ghc.dataConTyCon . dcpCon . F.val)
+        datacons
+
+    
 knownWiredDataCons :: Bare.Env -> ModName -> [Located DataConP] 
 knownWiredDataCons env name = filter isKnown wiredDataCons 
   where 
@@ -936,12 +1024,12 @@ makeMeasEnv env tycEnv sigEnv specs = Bare.MeasEnv
   }
   where 
     measures      = mconcat (Ms.mkMSpec' dcSelectors : (Bare.makeMeasureSpec env sigEnv name <$> M.toList specs))
-    (cs, ms)      = Bare.makeMeasureSpec'     measures
+    (cs, ms)      = Bare.makeMeasureSpec' (typeclass $ getConfig env)   measures
     cms           = Bare.makeClassMeasureSpec measures
     cms'          = [ (x, Loc l l' $ cSort t)  | (Loc l l' x, t) <- cms ]
     ms'           = [ (F.val lx, F.atLoc lx t) | (lx, t) <- ms
                                                , Mb.isNothing (lookup (val lx) cms') ]
-    cs'           = [ (v, txRefs v t) | (v, t) <- Bare.meetDataConSpec embs cs (datacons ++ cls)]
+    cs'           = [ (v, txRefs v t) | (v, t) <- Bare.meetDataConSpec (typeclass (getConfig env)) embs cs (datacons ++ cls)]
     txRefs v t    = Bare.txRefSort tyi embs (const t <$> GM.locNamedThing v) 
     -- unpacking the environment
     tyi           = Bare.tcTyConMap    tycEnv 
diff --git a/src/Language/Haskell/Liquid/Bare/Axiom.hs b/src/Language/Haskell/Liquid/Bare/Axiom.hs
index 55875b3710..0e8cc81a74 100644
--- a/src/Language/Haskell/Liquid/Bare/Axiom.hs
+++ b/src/Language/Haskell/Liquid/Bare/Axiom.hs
@@ -54,8 +54,10 @@ getReflectDefs src sig spec = findVarDefType cbs sigs <$> xs
 
 findVarDefType :: [Ghc.CoreBind] -> [(Ghc.Var, LocSpecType)] -> LocSymbol
                -> (LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)
-findVarDefType cbs sigs x = case findVarDef (val x) cbs of
-  Just (v, e) -> if Ghc.isExportedId v
+findVarDefType cbs sigs x = case findVarDefMethod (val x) cbs of
+  -- YL: probably ok even without checking typeclass flag since user cannot
+  -- manually reflect internal names
+  Just (v, e) -> if Ghc.isExportedId v || isMethod (F.symbol x) || isDictionary (F.symbol x)
                    then (x, val <$> lookup v sigs, v, e)
                    else Ex.throw $ mkError x ("Lifted functions must be exported; please export " ++ show v)
   Nothing     -> Ex.throw $ mkError x "Cannot lift haskell function"
@@ -69,33 +71,35 @@ makeAxiom env tycEnv name lmap (x, mbT, v, def)
             = (v, t, e)
   where 
     t       = Bare.qualifyTop env name (F.loc t0) t0 
-    (t0, e) = makeAssumeType embs lmap dm x mbT v def
+    (t0, e) = makeAssumeType allowTC embs lmap dm x mbT v def
     embs    = Bare.tcEmbs       tycEnv 
-    dm      = Bare.tcDataConMap tycEnv 
+    dm      = Bare.tcDataConMap tycEnv
+    allowTC = typeclass (getConfig env)
 
 mkError :: LocSymbol -> String -> Error
 mkError x str = ErrHMeas (sourcePosSrcSpan $ loc x) (pprint $ val x) (PJ.text str)
 
 makeAssumeType
-  :: F.TCEmb Ghc.TyCon -> LogicMap -> DataConMap -> LocSymbol -> Maybe SpecType
+  :: Bool -- ^ typeclass enabled
+  -> F.TCEmb Ghc.TyCon -> LogicMap -> DataConMap -> LocSymbol -> Maybe SpecType
   -> Ghc.Var -> Ghc.CoreExpr
   -> (LocSpecType, F.Equation)
-makeAssumeType tce lmap dm x mbT v def
+makeAssumeType allowTC tce lmap dm x mbT v def
   = (x {val = aty at `strengthenRes` F.subst su ref},  F.mkEquation (val x) xts (F.subst su le) out)
   where
     t     = Mb.fromMaybe (ofType τ) mbT
     τ     = Ghc.varType v
-    at    = axiomType x t
+    at    = axiomType allowTC x t
     out   = rTypeSort tce $ ares at 
     xArgs = (F.EVar . fst) <$> aargs at
     _msg  = unwords [showpp x, showpp mbT]
-    le    = case runToLogicWithBoolBinds bbs tce lmap dm mkErr (coreToLogic  def') of
+    le    = case runToLogicWithBoolBinds bbs tce lmap dm mkErr (coreToLogic allowTC def') of
               Right e -> e
               Left  e -> panic Nothing (show e)
     ref        = F.Reft (F.vv_, F.PAtom F.Eq (F.EVar F.vv_) le)
     mkErr s    = ErrHMeas (sourcePosSrcSpan $ loc x) (pprint $ val x) (PJ.text s)
     bbs        = filter isBoolBind xs
-    (xs, def') = grabBody (Ghc.expandTypeSynonyms τ) $ normalize def
+    (xs, def') = grabBody allowTC (Ghc.expandTypeSynonyms τ) $ normalize allowTC def
     su         = F.mkSubst  $ zip (F.symbol     <$> xs) xArgs
                            ++ zip (simplesymbol <$> xs) xArgs
     xts        = [(F.symbol x, rTypeSortExp tce t) | (x, t) <- aargs at]
@@ -103,21 +107,24 @@ makeAssumeType tce lmap dm x mbT v def
 rTypeSortExp :: F.TCEmb Ghc.TyCon -> SpecType -> F.Sort
 rTypeSortExp tce = typeSort tce . Ghc.expandTypeSynonyms . toType
 
-grabBody :: Ghc.Type -> Ghc.CoreExpr -> ([Ghc.Var], Ghc.CoreExpr)
-grabBody (Ghc.ForAllTy _ t) e 
-  = grabBody t e 
-grabBody (Ghc.FunTy { Ghc.ft_arg = tx, Ghc.ft_res = t}) e | Ghc.isClassPred tx 
-  = grabBody t e 
-grabBody (Ghc.FunTy { Ghc.ft_res = t}) (Ghc.Lam x e) 
-  = (x:xs, e') where (xs, e') = grabBody t e
-grabBody t (Ghc.Tick _ e) 
-  = grabBody t e
-grabBody t@(Ghc.FunTy {}) e               
+grabBody :: Bool -- ^ typeclass enabled
+         -> Ghc.Type -> Ghc.CoreExpr -> ([Ghc.Var], Ghc.CoreExpr)
+grabBody allowTC (Ghc.ForAllTy _ t) e 
+  = grabBody allowTC t e 
+grabBody allowTC@False (Ghc.FunTy { Ghc.ft_arg = tx, Ghc.ft_res = t}) e | Ghc.isClassPred tx 
+  = grabBody allowTC t e 
+grabBody allowTC@True (Ghc.FunTy { Ghc.ft_arg = tx, Ghc.ft_res = t}) e | isEmbeddedDictType tx 
+  = grabBody allowTC t e 
+grabBody allowTC (Ghc.FunTy { Ghc.ft_res = t}) (Ghc.Lam x e) 
+  = (x:xs, e') where (xs, e') = grabBody allowTC t e
+grabBody allowTC t (Ghc.Tick _ e) 
+  = grabBody allowTC t e
+grabBody allowTC t@(Ghc.FunTy {}) e               
   = (txs++xs, e') 
    where (ts,tr)  = splitFun t 
-         (xs, e') = grabBody tr (foldl Ghc.App e (Ghc.Var <$> txs))
+         (xs, e') = grabBody allowTC tr (foldl Ghc.App e (Ghc.Var <$> txs))
          txs      = [ stringVar ("ls" ++ show i) t |  (t,i) <- zip ts [1..]]
-grabBody _ e              
+grabBody allowTC _ e              
   = ([], e)
 
 splitFun :: Ghc.Type -> ([Ghc.Type], Ghc.Type)
@@ -172,13 +179,13 @@ instance Subable Ghc.CoreAlt where
 data AxiomType = AT { aty :: SpecType, aargs :: [(F.Symbol, SpecType)], ares :: SpecType }
 
 -- | Specification for Haskell function
-axiomType :: LocSymbol -> SpecType -> AxiomType
-axiomType s t = AT to (reverse xts) res  
+axiomType :: Bool -> LocSymbol -> SpecType -> AxiomType
+axiomType allowTC s t = AT to (reverse xts) res  
   where
     (to, (_,xts, Just res)) = runState (go t) (1,[], Nothing)
     go (RAllT a t r) = RAllT a <$> go t <*> return r 
     go (RAllP p t) = RAllP p <$> go t 
-    go (RFun x tx t r) | isClassType tx = (\t' -> RFun x tx t' r) <$> go t
+    go (RFun x tx t r) | isErasable tx = (\t' -> RFun x tx t' r) <$> go t
     go (RFun x tx t r) = do 
       (i,bs,res) <- get 
       let x' = unDummy x i 
@@ -191,7 +198,7 @@ axiomType s t = AT to (reverse xts) res
       let t' = strengthen t (singletonApp s ys)
       put (i, bs, Just t')
       return t' 
-
+    isErasable = if allowTC then isEmbeddedClass else isClassType
 unDummy :: F.Symbol -> Int -> F.Symbol
 unDummy x i
   | x /= F.dummySymbol = x
diff --git a/src/Language/Haskell/Liquid/Bare/Check.hs b/src/Language/Haskell/Liquid/Bare/Check.hs
index 23267a80ad..ff6a21fc52 100644
--- a/src/Language/Haskell/Liquid/Bare/Check.hs
+++ b/src/Language/Haskell/Liquid/Bare/Check.hs
@@ -106,15 +106,15 @@ checkTargetSpec :: [Ms.BareSpec]
                 -> Either [Error] TargetSpec
 checkTargetSpec specs src env cbs sp = Misc.applyNonNull (Right sp) Left errors
   where
-    errors           =  mapMaybe (checkBind allowHO bsc "measure"      emb tcEnv env) (gsMeas       (gsData sp))
+    errors           =  mapMaybe (checkBind allowTC allowHO bsc "measure"      emb tcEnv env) (gsMeas       (gsData sp))
                      ++ condNull noPrune 
-                        (mapMaybe (checkBind allowHO bsc "constructor"  emb tcEnv env) (txCtors $ gsCtors      (gsData sp)))
-                     ++ mapMaybe (checkBind allowHO bsc "assume"       emb tcEnv env) (gsAsmSigs    (gsSig sp))
-                     ++ checkTySigs         allowHO bsc cbs            emb tcEnv env                (gsSig sp)
+                        (mapMaybe (checkBind allowTC allowHO bsc "constructor"  emb tcEnv env) (txCtors $ gsCtors      (gsData sp)))
+                     ++ mapMaybe (checkBind allowTC allowHO bsc "assume"       emb tcEnv env) (gsAsmSigs    (gsSig sp))
+                     ++ checkTySigs         allowTC allowHO bsc cbs            emb tcEnv env                (gsSig sp)
                      -- ++ mapMaybe (checkTerminationExpr             emb       env) (gsTexprs     (gsSig  sp)) 
-                     ++ mapMaybe (checkBind allowHO bsc "class method" emb tcEnv env) (clsSigs      (gsSig sp))
-                     ++ mapMaybe (checkInv allowHO bsc emb tcEnv env)                 (gsInvariants (gsData sp))
-                     ++ checkIAl allowHO bsc emb tcEnv env                            (gsIaliases   (gsData sp))
+                     ++ mapMaybe (checkBind allowTC allowHO bsc "class method" emb tcEnv env) (clsSigs      (gsSig sp))
+                     ++ mapMaybe (checkInv allowTC allowHO bsc emb tcEnv env)                 (gsInvariants (gsData sp))
+                     ++ checkIAl allowTC allowHO bsc emb tcEnv env                            (gsIaliases   (gsData sp))
                      ++ checkMeasures emb env ms
                      ++ checkClassMeasures                                        (gsMeasures (gsData sp))
                      ++ checkClassMethods (gsCls src) (gsCMethods (gsVars sp)) (gsTySigs     (gsSig sp))
@@ -143,6 +143,7 @@ checkTargetSpec specs src env cbs sp = Misc.applyNonNull (Right sp) Left errors
     ms               = gsMeasures (gsData sp)
     clsSigs sp       = [ (v, t) | (v, t) <- gsTySigs sp, isJust (isClassOpId_maybe v) ]
     sigs             = gsTySigs (gsSig sp) ++ gsAsmSigs (gsSig sp) ++ gsCtors (gsData sp)
+    allowTC          = typeclass (getConfig sp)
     allowHO          = higherOrderFlag sp
     bsc              = bscope (getConfig sp)
     noPrune          = not (pruneFlag sp)
@@ -162,17 +163,17 @@ checkPlugged xs = mkErr <$> filter (hasHoleTy . val . snd) xs
 
 
 --------------------------------------------------------------------------------
-checkTySigs :: Bool -> BScope -> [CoreBind] -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft 
+checkTySigs :: Bool -> Bool -> BScope -> [CoreBind] -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft 
             -> GhcSpecSig
             -> [Error]
 --------------------------------------------------------------------------------
-checkTySigs allowHO bsc cbs emb tcEnv env sig
+checkTySigs allowTC allowHO bsc cbs emb tcEnv env sig
                    = concatMap (check env) topTs
                    -- (mapMaybe   (checkT env) [ (x, t)     | (x, (t, _)) <- topTs])
                    -- ++ (mapMaybe   (checkE env) [ (x, t, es) | (x, (t, Just es)) <- topTs]) 
                    ++ coreVisitor checkVisitor env [] cbs 
   where 
-    check env      = checkSigTExpr allowHO bsc emb tcEnv env
+    check env      = checkSigTExpr allowTC allowHO bsc emb tcEnv env
     locTm          = M.fromList locTs
     (locTs, topTs) = Bare.partitionLocalBinds vtes 
     vtes           = [ (x, (t, es)) | (x, t) <- gsTySigs sig, let es = M.lookup x vExprs]
@@ -189,13 +190,13 @@ checkTySigs allowHO bsc cbs emb tcEnv env sig
                          Nothing -> [] 
                          Just t  -> check env (v, t) 
 
-checkSigTExpr :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft 
+checkSigTExpr :: Bool -> Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft 
               -> (Var, (LocSpecType, Maybe [Located F.Expr])) 
               -> [Error]
-checkSigTExpr allowHO bsc emb tcEnv env (x, (t, es)) 
+checkSigTExpr allowTC allowHO bsc emb tcEnv env (x, (t, es)) 
            = catMaybes [mbErr1, mbErr2] 
    where 
-    mbErr1 = checkBind allowHO bsc empty emb tcEnv env (x, t) 
+    mbErr1 = checkBind allowTC allowHO bsc empty emb tcEnv env (x, t) 
     mbErr2 = checkTerminationExpr emb env . (x, t,) =<< es 
 
 _checkQualifiers :: F.SEnv F.SortedReft -> [F.Qualifier] -> [Error]
@@ -263,24 +264,25 @@ _firstDuplicate = go . L.sort
                 | otherwise = go (x:xs)
     go _                    = Nothing
 
-checkInv :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (Maybe Var, LocSpecType) -> Maybe Error
-checkInv allowHO bsc emb tcEnv env (_, t) = checkTy allowHO bsc err emb tcEnv env t
+checkInv :: Bool -> Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (Maybe Var, LocSpecType) -> Maybe Error
+checkInv allowTC allowHO bsc emb tcEnv env (_, t) = checkTy allowTC allowHO bsc err emb tcEnv env t
   where
     err              = ErrInvt (GM.sourcePosSrcSpan $ loc t) (val t)
 
-checkIAl :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> [(LocSpecType, LocSpecType)] -> [Error]
-checkIAl allowHO bsc emb tcEnv env ials = catMaybes $ concatMap (checkIAlOne allowHO bsc emb tcEnv env) ials
+checkIAl :: Bool -> Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> [(LocSpecType, LocSpecType)] -> [Error]
+checkIAl allowTC allowHO bsc emb tcEnv env ials = catMaybes $ concatMap (checkIAlOne allowTC allowHO bsc emb tcEnv env) ials
 
 checkIAlOne :: Bool
+            -> Bool
             -> BScope
             -> F.TCEmb TyCon
             -> Bare.TyConMap
             -> F.SEnv F.SortedReft
             -> (LocSpecType, LocSpecType)
             -> [Maybe (TError SpecType)]
-checkIAlOne allowHO bsc emb tcEnv env (t1, t2) = checkEq : (tcheck <$> [t1, t2])
+checkIAlOne allowTC allowHO bsc emb tcEnv env (t1, t2) = checkEq : (tcheck <$> [t1, t2])
   where
-    tcheck t = checkTy allowHO bsc (err t) emb tcEnv env t
+    tcheck t = checkTy allowTC allowHO bsc (err t) emb tcEnv env t
     err    t = ErrIAl (GM.sourcePosSrcSpan $ loc t) (val t)
     t1'      :: RSort
     t1'      = toRSort $ val t1
@@ -297,8 +299,8 @@ checkRTAliases msg _ as = err1s
   where
     err1s               = checkDuplicateRTAlias msg as
 
-checkBind :: (PPrint v) => Bool -> BScope -> Doc -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (v, LocSpecType) -> Maybe Error
-checkBind allowHO bsc s emb tcEnv env (v, t) = checkTy allowHO bsc msg emb tcEnv env t
+checkBind :: (PPrint v) => Bool -> Bool -> BScope -> Doc -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (v, LocSpecType) -> Maybe Error
+checkBind allowTC allowHO bsc s emb tcEnv env (v, t) = checkTy allowTC allowHO bsc msg emb tcEnv env t
   where
     msg                      = ErrTySpec (GM.fSrcSpan t) (Just s) (pprint v) (val t)
 
@@ -324,8 +326,8 @@ checkTerminationExpr emb env (v, Loc l _ t, les)
     rSort   = rTypeSortedReft emb
     cmpZero e = F.PAtom F.Le (F.expr (0 :: Int)) (val e)
 
-checkTy :: Bool -> BScope -> (Doc -> Error) -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Error
-checkTy allowHO bsc mkE emb tcEnv env t = mkE <$> checkRType allowHO bsc emb env (Bare.txRefSort tcEnv emb t)
+checkTy :: Bool -> Bool -> BScope -> (Doc -> Error) -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Error
+checkTy allowTC allowHO bsc mkE emb tcEnv env t = mkE <$> checkRType allowTC allowHO bsc emb env (Bare.txRefSort tcEnv emb t)
   where
     _msg =  "CHECKTY: " ++ showpp (val t)
 
@@ -393,13 +395,14 @@ errTypeMismatch x t = ErrMismatch lqSp (pprint x) (text "Checked")  d1 d2 Nothin
 ------------------------------------------------------------------------------------------------
 -- | @checkRType@ determines if a type is malformed in a given environment ---------------------
 ------------------------------------------------------------------------------------------------
-checkRType :: Bool -> BScope -> F.TCEmb TyCon -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Doc
+checkRType :: Bool -> Bool -> BScope -> F.TCEmb TyCon -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Doc
 ------------------------------------------------------------------------------------------------
-checkRType allowHO bsc emb env lt
+checkRType allowTC allowHO bsc emb env lt
   =   checkAppTys t
   <|> checkAbstractRefs t
-  <|> efoldReft farg bsc cb (tyToBind emb) (rTypeSortedReft emb) f insertPEnv env Nothing t
+  <|> efoldReft isErasable farg bsc cb (tyToBind emb) (rTypeSortedReft emb) f insertPEnv env Nothing t
   where
+    isErasable         = if allowTC then isEmbeddedDict else isClass
     t                  = val lt
     cb c ts            = classBinds emb (rRCls c ts)
     farg _ t           = allowHO || isBase t  -- NOTE: this check should be the same as the one in addCGEnv
@@ -547,7 +550,7 @@ checkMBody γ emb _ sort (Def m c _ bs body) = checkMBody' emb sort γ' sp body
   where
     sp    = F.srcSpan m
     γ'    = L.foldl' (\γ (x, t) -> F.insertSEnv x t γ) γ xts
-    xts   = zip (fst <$> bs) $ rTypeSortedReft emb . subsTyVars_meet su <$> filter (not . isClassType) (ty_args trep)
+    xts   = zip (fst <$> bs) $ rTypeSortedReft emb . subsTyVars_meet su <$>  (ty_args trep)
     trep  = toRTypeRep ct
     su    = checkMBodyUnify (ty_res trep) (last txs)
     txs   = snd4 $ bkArrowDeep sort
diff --git a/src/Language/Haskell/Liquid/Bare/Class.hs b/src/Language/Haskell/Liquid/Bare/Class.hs
index 4138037373..194e8973c3 100644
--- a/src/Language/Haskell/Liquid/Bare/Class.hs
+++ b/src/Language/Haskell/Liquid/Bare/Class.hs
@@ -41,10 +41,10 @@ import qualified Control.Exception                 as Ex
 
 
 -------------------------------------------------------------------------------
-makeMethodTypes :: DEnv Ghc.Var LocSpecType -> [DataConP] -> [Ghc.CoreBind] -> [(Ghc.Var, MethodType LocSpecType)]
+makeMethodTypes :: Bool -> DEnv Ghc.Var LocSpecType -> [DataConP] -> [Ghc.CoreBind] -> [(Ghc.Var, MethodType LocSpecType)]
 -------------------------------------------------------------------------------
-makeMethodTypes (DEnv m) cls cbs 
-  = [(x, MT (addCC x . fromRISig <$> methodType d x m) (addCC x <$> classType (splitDictionary e) x)) | (d,e) <- ds, x <- grepMethods e]
+makeMethodTypes allowTC (DEnv m) cls cbs 
+  = [(x, MT (addCC allowTC x . fromRISig <$> methodType d x m) (addCC allowTC x <$> classType (splitDictionary e) x)) | (d,e) <- ds, x <- grepMethods e]
     where 
       grepMethods = filter GM.isMethod . freeVars mempty
       ds = filter (GM.isDictionary . fst) (concatMap unRec cbs)
@@ -67,8 +67,8 @@ makeMethodTypes (DEnv m) cls cbs
       subst [] t = t 
       subst ((a,ta):su) t = subsTyVar_meet' (a,ofType ta) (subst su t)
 
-addCC :: Ghc.Var -> LocSpecType -> LocSpecType
-addCC x zz@(Loc l l' st0) 
+addCC :: Bool -> Ghc.Var -> LocSpecType -> LocSpecType
+addCC allowTC x zz@(Loc l l' st0) 
   = Loc l l' 
   . addForall hst  
   . mkArrow [] ps' [] [] 
@@ -79,7 +79,7 @@ addCC x zz@(Loc l l' st0)
   where
     hst           = ofType (Ghc.expandTypeSynonyms t0) :: SpecType
     t0            = Ghc.varType x 
-    tyvsmap       = case Bare.runMapTyVars t0 st err of
+    tyvsmap       = case Bare.runMapTyVars allowTC t0 st err of
                           Left e  -> Ex.throw e 
                           Right s -> Bare.vmap s
     su            = [(y, rTyVar x)           | (x, y) <- tyvsmap]
@@ -273,4 +273,4 @@ lookupDefaultVar env name v = Mb.maybeToList
   where 
     dmSym                   = F.atLoc v (GM.qualifySymbol mSym dnSym)
     dnSym                   = F.mappendSym "$dm" nSym
-    (mSym, nSym)            = GM.splitModuleName (F.symbol v) 
\ No newline at end of file
+    (mSym, nSym)            = GM.splitModuleName (F.symbol v) 
diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs
index ad09e5a7ab..85ce0e6a7c 100644
--- a/src/Language/Haskell/Liquid/Bare/DataType.hs
+++ b/src/Language/Haskell/Liquid/Bare/DataType.hs
@@ -27,6 +27,7 @@ import           Prelude                                hiding (error)
 -- import           Language.Haskell.Liquid.GHC.TypeRep
 
 import qualified Control.Exception                      as Ex
+import           Control.Monad.Reader
 import qualified Data.List                              as L
 import qualified Data.HashMap.Strict                    as M
 import qualified Data.HashSet                           as S
@@ -347,22 +348,22 @@ muSort c n  = V.mapSort tx
 -}
 
 --------------------------------------------------------------------------------
-meetDataConSpec :: F.TCEmb Ghc.TyCon -> [(Ghc.Var, SpecType)] -> [DataConP] 
+meetDataConSpec :: Bool -> F.TCEmb Ghc.TyCon -> [(Ghc.Var, SpecType)] -> [DataConP] 
                 -> [(Ghc.Var, SpecType)]
 --------------------------------------------------------------------------------
-meetDataConSpec emb xts dcs  = M.toList $ snd <$> L.foldl' upd dcm0 xts
+meetDataConSpec allowTC emb xts dcs  = M.toList $ snd <$> L.foldl' upd dcm0 xts
   where
-    dcm0                     = M.fromList (dataConSpec' dcs)
+    dcm0                     = M.fromList (dataConSpec' allowTC dcs)
     upd dcm (x, t)           = M.insert x (Ghc.getSrcSpan x, tx') dcm
                                 where
                                   tx' = maybe t (meetX x t) (M.lookup x dcm)
     meetX x t (sp', t')      = F.notracepp (_msg x t t') $ meetVarTypes emb (pprint x) (Ghc.getSrcSpan x, t) (sp', t') 
     _msg x t t'              = "MEET-VAR-TYPES: " ++ showpp (x, t, t')
 
-dataConSpec' :: [DataConP] -> [(Ghc.Var, (Ghc.SrcSpan, SpecType))]
-dataConSpec' = concatMap tx 
+dataConSpec' :: Bool -> [DataConP] -> [(Ghc.Var, (Ghc.SrcSpan, SpecType))]
+dataConSpec' allowTC = concatMap tx 
   where
-    tx dcp   =  [ (x, res) | (x, t0) <- dataConPSpecType dcp
+    tx dcp   =  [ (x, res) | (x, t0) <- dataConPSpecType allowTC dcp
                           , let t    = RT.expandProductType x t0  
                           , let res  = (GM.fSrcSpan dcp, t)
                 ]
@@ -655,10 +656,42 @@ checkRecordSelectorSigs vts = [ (v, take1 v ts) | (v, ts) <- Misc.groupList vts
                                 (t:ts) -> Ex.throw (ErrDupSpecs (GM.fSrcSpan t) (pprint v) (GM.fSrcSpan <$> ts) :: Error)
                                 _      -> impossible Nothing "checkRecordSelectorSigs"
 
+
+strengthenClassSel :: Ghc.Var -> LocSpecType -> LocSpecType
+strengthenClassSel v lt = lt { val = t }
+ where
+  t = runReader (go (F.val lt)) (1, [])
+  s = GM.namedLocSymbol v
+  extend :: F.Symbol -> (Int, [F.Symbol]) -> (Int, [F.Symbol])
+  extend x (i, xs) = (i + 1, x : xs)
+  go :: SpecType -> Reader (Int, [F.Symbol]) SpecType
+  go (RAllT a t r) = RAllT a <$> go t <*> pure r
+  go (RAllP p t  ) = RAllP p <$> go t
+  go (RFun x tx t r) | isEmbeddedClass tx =
+    RFun <$> pure x <*> pure tx <*> go t <*> pure r
+  go (RFun x tx t r) = do
+    x' <- unDummy x <$> reader fst
+    r' <- singletonApp s <$> (L.reverse <$> reader snd)
+    RFun x' tx <$> local (extend x') (go t) <*> pure (F.meet r r')
+  go t = RT.strengthen t . singletonApp s . L.reverse <$> reader snd
+
+singletonApp :: F.Symbolic a => F.LocSymbol -> [a] -> UReft F.Reft
+singletonApp s ys = MkUReft r mempty
+  where r = F.exprReft (F.mkEApp s (F.eVar <$> ys))
+
+
+unDummy :: F.Symbol -> Int -> F.Symbol
+unDummy x i | x /= F.dummySymbol = x
+            | otherwise          = F.symbol ("_cls_lq" ++ show i)
+
 makeRecordSelectorSigs :: Bare.Env -> ModName -> [Located DataConP] -> [(Ghc.Var, LocSpecType)]
 makeRecordSelectorSigs env name = checkRecordSelectorSigs . concatMap makeOne
   where
   makeOne (Loc l l' dcp)
+    | Just cls <- maybe_cls
+    = let cfs = Ghc.classAllSelIds cls in
+        fmap ((,) <$> fst <*> uncurry strengthenClassSel)
+          [(v, Loc l l' t)| (v,t) <- zip cfs (reverse $ fmap snd args)]
     | null fls                    --    no field labels
     || any (isFunTy . snd) args && not (higherOrderFlag env)   -- OR function-valued fields
     || dcpIsGadt dcp              -- OR GADT style datcon
@@ -666,6 +699,7 @@ makeRecordSelectorSigs env name = checkRecordSelectorSigs . concatMap makeOne
     | otherwise 
     = [ (v, t) | (Just v, t) <- zip fs ts ] 
     where
+      maybe_cls = Ghc.tyConClass_maybe (Ghc.dataConTyCon dc)
       dc  = dcpCon dcp
       fls = Ghc.dataConFieldLabels dc
       fs  = Bare.lookupGhcNamedVar env name . Ghc.flSelector <$> fls 
diff --git a/src/Language/Haskell/Liquid/Bare/Elaborate.hs b/src/Language/Haskell/Liquid/Bare/Elaborate.hs
new file mode 100644
index 0000000000..8e84152346
--- /dev/null
+++ b/src/Language/Haskell/Liquid/Bare/Elaborate.hs
@@ -0,0 +1,797 @@
+{-# LANGUAGE ViewPatterns              #-}
+{-# LANGUAGE ExplicitForAll            #-}
+{-# LANGUAGE TypeFamilies              #-}
+{-# LANGUAGE DeriveFunctor             #-}
+{-# LANGUAGE TypeApplications          #-}
+{-# LANGUAGE LambdaCase                #-}
+-- | This module uses GHC API to elaborate the resolves expressions
+
+-- TODO: Genearlize to BareType and replace the existing resolution mechanisms
+
+module Language.Haskell.Liquid.Bare.Elaborate
+  ( fixExprToHsExpr
+  , elaborateSpecType
+  , buildSimplifier
+  )
+where
+
+import qualified Language.Fixpoint.Types       as F
+import           Control.Arrow
+import qualified Language.Haskell.Liquid.GHC.Misc
+                                               as GM
+import           Language.Haskell.Liquid.Types.Visitors
+import           Language.Haskell.Liquid.Types.Types
+import           Language.Haskell.Liquid.Types.RefType
+                                                ( ofType )
+import qualified Data.List                     as L
+import qualified Data.HashMap.Strict           as M
+import qualified Data.HashSet                  as S
+import           Control.Monad.Free
+import           Data.Functor.Foldable
+import           Data.Char                      ( isUpper )
+import           GHC
+import           GhcPlugins                     ( isDFunId
+                                                , gopt_set
+                                                )
+import           OccName
+import           FastString
+import           CoreSyn
+import           PrelNames
+import qualified Outputable                    as O
+import           TysWiredIn                     ( boolTyCon
+                                                , true_RDR
+                                                )
+import           ErrUtils
+import           RdrName
+import           BasicTypes
+import           Data.Default                   ( def )
+import qualified Data.Maybe                    as Mb
+import           CoreSubst               hiding ( substExpr )
+import           SimplCore
+import           CoreMonad
+import           CoreFVs                        ( exprFreeVarsList )
+import           VarEnv                         ( lookupVarEnv
+                                                , lookupInScope
+                                                )
+import           CoreUtils                      ( mkTick )
+import qualified CoreUtils                     as Utils
+import qualified Data.HashMap.Strict           as M
+
+
+-- TODO: make elaboration monadic so typeclass names are unified to something
+-- that is generated in advance. This can greatly simplify the implementation
+-- of elaboration
+
+
+lookupIdSubstAll :: O.SDoc -> M.HashMap Id CoreExpr -> Id -> CoreExpr
+lookupIdSubstAll doc env v | Just e <- M.lookup v env = e
+                           | otherwise                = Var v
+        -- Vital! See Note [Extending the Subst]
+  -- | otherwise = WARN( True, text "CoreSubst.lookupIdSubst" <+> doc <+> ppr v
+  --                           $$ ppr in_scope)
+
+substExprAll :: O.SDoc -> M.HashMap Id CoreExpr -> CoreExpr -> CoreExpr
+substExprAll doc subst orig_expr = subst_expr_all doc subst orig_expr
+
+
+subst_expr_all :: O.SDoc -> M.HashMap Id CoreExpr -> CoreExpr -> CoreExpr
+subst_expr_all doc subst expr = go expr
+ where
+  go (Var v) = lookupIdSubstAll (doc O.$$ O.text "subst_expr_all") subst v
+  go (Type     ty      ) = Type ty
+  go (Coercion co      ) = Coercion co
+  go (Lit      lit     ) = Lit lit
+  go (App  fun     arg ) = App (go fun) (go arg)
+  go (Tick tickish e   ) = Tick tickish (go e)
+  go (Cast e       co  ) = Cast (go e) co
+     -- Do not optimise even identity coercions
+     -- Reason: substitution applies to the LHS of RULES, and
+     --         if you "optimise" an identity coercion, you may
+     --         lose a binder. We optimise the LHS of rules at
+     --         construction time
+
+  go (Lam  bndr    body) = Lam bndr (subst_expr_all doc subst body)
+
+  go (Let  bind    body) = Let (mapBnd go bind) (subst_expr_all doc subst body)
+
+  go (Case scrut bndr ty alts) =
+    Case (go scrut) bndr ty (map (go_alt subst) alts)
+
+  go_alt subst (con, bndrs, rhs) = (con, bndrs, subst_expr_all doc subst rhs)
+
+
+mapBnd :: (Expr b -> Expr b) -> Bind b -> Bind b
+mapBnd f (NonRec b e) = NonRec b (f e)
+mapBnd f (Rec bs    ) = Rec (map (second f) bs)
+
+-- substLet :: CoreExpr -> CoreExpr
+-- substLet (Lam b body) = Lam b (substLet body)
+-- substLet (Let b body)
+--   | NonRec x e <- b = substLet
+--     (substExprAll O.empty (extendIdSubst emptySubst x e) body)
+--   | otherwise = Let b (substLet body)
+-- substLet e = e
+
+
+buildDictSubst :: CoreProgram -> M.HashMap Id CoreExpr
+buildDictSubst = cata f
+ where
+  f Nil = M.empty
+  f (Cons b s) | NonRec x e <- b, isDFunId x -- || isDictonaryId x
+                                             = M.insert x e s
+               | otherwise                   = s
+
+buildSimplifier :: CoreProgram -> CoreExpr -> Ghc CoreExpr
+buildSimplifier cbs e = pure e-- do
+ --  df <- getDynFlags
+ --  liftIO $ simplifyExpr (df `gopt_set` Opt_SuppressUnfoldings) e'
+ -- where
+ --  -- fvs = fmap (\x -> (x, getUnique x, isLocalId x))  (freeVars mempty e)
+ --  dictSubst = buildDictSubst cbs
+ --  e'        = substExprAll O.empty dictSubst e
+
+
+-- | Base functor of RType
+data RTypeF c tv r f
+  = RVarF {
+      rtf_var    :: !tv
+    , rtf_reft   :: !r
+    }
+
+  | RFunF  {
+      rtf_bind   :: !F.Symbol
+    , rtf_in     :: !f
+    , rtf_out    :: !f
+    , rtf_reft   :: !r
+    }
+
+  | RImpFF  {
+      rtf_bind   :: !F.Symbol
+    , rtf_in     :: !f
+    , rtf_out    :: !f
+    , rtf_reft   :: !r
+    }
+
+  | RAllTF {
+      rtf_tvbind :: !(RTVU c tv) -- RTVar tv (RType c tv ()))
+    , rtf_ty     :: !f
+    , rtf_ref    :: !r
+    }
+
+  -- | "forall x y <z :: Nat, w :: Int> . TYPE"
+  --               ^^^^^^^^^^^^^^^^^^^ (rtf_pvbind)
+  | RAllPF {
+      rtf_pvbind :: !(PVU c tv)  -- ar (RType c tv ()))
+    , rtf_ty     :: !f
+    }
+
+  -- | For example, in [a]<{\h -> v > h}>, we apply (via `RApp`)
+  --   * the `RProp`  denoted by `{\h -> v > h}` to
+  --   * the `RTyCon` denoted by `[]`.
+  | RAppF  {
+      rtf_tycon  :: !c
+    , rtf_args   :: ![f]
+    , rtf_pargs  :: ![RTPropF c tv f]
+    , rtf_reft   :: !r
+    }
+
+  | RAllEF {
+      rtf_bind   :: !F.Symbol
+    , rtf_allarg :: !f
+    , rtf_ty     :: !f
+    }
+
+  | RExF {
+      rtf_bind   :: !F.Symbol
+    , rtf_exarg  :: !f
+    , rtf_ty     :: !f
+    }
+
+  | RExprArgF (F.Located F.Expr)
+
+  | RAppTyF{
+      rtf_arg   :: !f
+    , rtf_res   :: !f
+    , rtf_reft  :: !r
+    }
+
+  | RRTyF  {
+      rtf_env   :: ![(F.Symbol, f)]
+    , rtf_ref   :: !r
+    , rtf_obl   :: !Oblig
+    , rtf_ty    :: !f
+    }
+
+  | RHoleF r
+  deriving (Functor)
+
+-- It's probably ok to treat (RType c tv ()) as a leaf..
+type RTPropF c tv f = Ref (RType c tv ()) f
+
+
+-- | SpecType with Holes.
+--   It provides us a context to construct the ghc queries.
+--   I don't think we can reuse RHole since it is not intended
+--   for this use case
+
+type SpecTypeF = RTypeF RTyCon RTyVar RReft
+type PartialSpecType = Free SpecTypeF ()
+
+type instance Base (RType c tv r) = RTypeF c tv r
+
+instance Recursive (RType c tv r) where
+  project (RVar var reft           ) = RVarF var reft
+  project (RFun  bind tin tout reft) = RFunF bind tin tout reft
+  project (RImpF bind tin tout reft) = RImpFF bind tin tout reft
+  project (RAllT tvbind ty ref     ) = RAllTF tvbind ty ref
+  project (RAllP pvbind ty         ) = RAllPF pvbind ty
+  project (RApp c args pargs reft  ) = RAppF c args pargs reft
+  project (RAllE bind allarg ty    ) = RAllEF bind allarg ty
+  project (REx   bind exarg  ty    ) = RExF bind exarg ty
+  project (RExprArg e              ) = RExprArgF e
+  project (RAppTy arg res reft     ) = RAppTyF arg res reft
+  project (RRTy env ref obl ty     ) = RRTyF env ref obl ty
+  project (RHole r                 ) = RHoleF r
+
+instance Corecursive (RType c tv r) where
+  embed (RVarF var reft           ) = RVar var reft
+  embed (RFunF  bind tin tout reft) = RFun bind tin tout reft
+  embed (RImpFF bind tin tout reft) = RImpF bind tin tout reft
+  embed (RAllTF tvbind ty ref     ) = RAllT tvbind ty ref
+  embed (RAllPF pvbind ty         ) = RAllP pvbind ty
+  embed (RAppF c args pargs reft  ) = RApp c args pargs reft
+  embed (RAllEF bind allarg ty    ) = RAllE bind allarg ty
+  embed (RExF   bind exarg  ty    ) = REx bind exarg ty
+  embed (RExprArgF e              ) = RExprArg e
+  embed (RAppTyF arg res reft     ) = RAppTy arg res reft
+  embed (RRTyF env ref obl ty     ) = RRTy env ref obl ty
+  embed (RHoleF r                 ) = RHole r
+
+
+-- specTypeToLHsType :: SpecType -> LHsType GhcPs
+-- specTypeToLHsType = typeToLHsType . toType
+
+-- -- Given types like x:a -> y:a -> _, this function returns x:a -> y:a -> Bool
+-- -- Free monad takes care of substitution
+
+-- A one-way function. Kind of like injecting something into Maybe
+specTypeToPartial :: forall a . SpecType -> SpecTypeF (Free SpecTypeF a)
+specTypeToPartial = hylo (fmap wrap) project
+
+-- probably should return spectype instead..
+plugType :: SpecType -> PartialSpecType -> SpecType
+plugType t = refix . f
+ where
+  f = hylo Fix $ \case
+    Pure _   -> specTypeToPartial t
+    Free res -> res
+
+-- build the expression we send to ghc for elaboration
+-- YL: tweak this function to see if ghc accepts explicit dictionary binders
+-- returning both expressions and binders since ghc adds unique id to the expressions
+
+-- | returns (lambda binders, forall binders)
+collectSpecTypeBinders :: SpecType -> ([F.Symbol], [F.Symbol])
+collectSpecTypeBinders = para $ \case
+  RFunF bind (tin, _) (_, (bs, abs)) _ | isClassType tin -> (bs, abs)
+                                       | otherwise       -> (bind : bs, abs)
+  RImpFF bind (tin, _) (_, (bs, abs)) _ | isClassType tin -> (bs, abs)
+                                        | otherwise       -> (bind : bs, abs)
+  RAllEF b _ (_, (bs, abs))  -> (b : bs, abs)
+  RAllTF (RTVar (RTV ab) _) (_, (bs, abs)) _ -> (bs, F.symbol ab : abs)
+  RExF b _ (_, (bs, abs))    -> (b : bs, abs)
+  RAppTyF _ (_, (bs, abs)) _ -> (bs, abs)
+  RRTyF _ _ _ (_, (bs, abs)) -> (bs, abs)
+  _                          -> ([], [])
+
+-- really should be fused with collectBinders. However, we need the binders
+-- to correctly convert fixpoint expressions to ghc expressions because of
+-- namespace related issues (whether the symbol denotes a varName or a datacon)
+buildHsExpr :: LHsExpr GhcPs -> SpecType -> LHsExpr GhcPs
+buildHsExpr res = para $ \case
+  RFunF bind (tin, _) (_, res) _
+    | isClassType tin -> res
+    | otherwise       -> mkHsLam [nlVarPat (varSymbolToRdrName bind)] res
+  RImpFF bind (tin, _) (_, res) _
+    | isClassType tin -> res
+    | otherwise       -> mkHsLam [nlVarPat (varSymbolToRdrName bind)] res
+  RAllEF  _ _        (_, res) -> res
+  RAllTF  _ (_, res) _        -> res
+  RExF    _ _        (_, res) -> res
+  RAppTyF _ (_, res) _        -> res
+  RRTyF _ _ _ (_, res)        -> res
+  _                           -> res
+
+
+
+canonicalizeDictBinder
+  :: F.Subable a => [F.Symbol] -> (a, [F.Symbol]) -> (a, [F.Symbol])
+canonicalizeDictBinder [] (e', bs') = (e', bs')
+canonicalizeDictBinder bs (e', [] ) = (e', bs)
+canonicalizeDictBinder bs (e', bs') = (renameDictBinder bs bs' e', bs)
+ where
+  renameDictBinder :: (F.Subable a) => [F.Symbol] -> [F.Symbol] -> a -> a
+  renameDictBinder []          _  = id
+  renameDictBinder _           [] = id
+  renameDictBinder canonicalDs ds = F.substa $ \x -> M.lookupDefault x x tbl
+    where tbl = F.notracepp "TBL" $ M.fromList (zip ds canonicalDs)
+
+elaborateSpecType
+  :: (CoreExpr -> F.Expr)
+  -> (CoreExpr -> Ghc CoreExpr)
+  -> SpecType
+  -> Ghc SpecType
+elaborateSpecType coreToLogic simplifier t = do
+  (t', xs) <- elaborateSpecType' (pure ()) coreToLogic simplifier t
+  case xs of
+    _ : _ -> panic
+      Nothing
+      "elaborateSpecType: invariant broken. substitution list for dictionary is not completely consumed"
+    _ -> pure t'
+
+elaborateSpecType'
+  :: PartialSpecType
+  -> (CoreExpr -> F.Expr) -- core to logic
+  -> (CoreExpr -> Ghc CoreExpr)
+  -> SpecType
+  -> Ghc (SpecType, [F.Symbol]) -- binders for dictionaries
+                   -- should have returned Maybe [F.Symbol]
+elaborateSpecType' partialTp coreToLogic simplify t =
+  case F.notracepp "elaborateSpecType'" t of
+    RVar (RTV tv) (MkUReft reft@(F.Reft (vv, _oldE)) p) -> do
+      elaborateReft
+        (reft, t)
+        (pure (t, []))
+        (\bs' ee -> pure (RVar (RTV tv) (MkUReft (F.Reft (vv, ee)) p), bs'))
+        -- YL : Fix
+    RFun bind tin tout ureft@(MkUReft reft@(F.Reft (vv, _oldE)) p) -> do
+      -- the reft is never actually used by the child
+      -- maybe i should enforce this information at the type level
+      let partialFunTp =
+            Free (RFunF bind (wrap $ specTypeToPartial tin) (pure ()) ureft) :: PartialSpecType
+          partialTp' = partialTp >> partialFunTp :: PartialSpecType
+      (eTin , bs ) <- elaborateSpecType' partialTp coreToLogic simplify tin
+      (eTout, bs') <- elaborateSpecType' partialTp' coreToLogic simplify tout
+      let buildRFunContTrivial
+            | isClassType tin, dictBinder : bs0' <- bs' = do
+              let (eToutRenamed, canonicalBinders) =
+                    canonicalizeDictBinder bs (eTout, bs0')
+              pure
+                ( F.notracepp "RFunTrivial0"
+                  $ RFun dictBinder eTin eToutRenamed ureft
+                , canonicalBinders
+                )
+            | otherwise = do
+              let (eToutRenamed, canonicalBinders) =
+                    canonicalizeDictBinder bs (eTout, bs')
+              pure
+                ( F.notracepp "RFunTrivial1" $ RFun bind eTin eToutRenamed ureft
+                , canonicalBinders
+                )
+          buildRFunCont bs'' ee
+            | isClassType tin, dictBinder : bs0' <- bs' = do
+              let (eToutRenamed, canonicalBinders) =
+                    canonicalizeDictBinder bs (eTout, bs0')
+                  (eeRenamed, canonicalBinders') =
+                    canonicalizeDictBinder canonicalBinders (ee, bs'')
+              pure
+                ( RFun dictBinder
+                       eTin
+                       eToutRenamed
+                       (MkUReft (F.Reft (vv, eeRenamed)) p)
+                , canonicalBinders'
+                )
+            | otherwise = do
+              let (eToutRenamed, canonicalBinders) =
+                    canonicalizeDictBinder bs (eTout, bs')
+                  (eeRenamed, canonicalBinders') =
+                    canonicalizeDictBinder canonicalBinders (ee, bs'')
+              pure
+                ( RFun bind
+                       eTin
+                       eToutRenamed
+                       (MkUReft (F.Reft (vv, eeRenamed)) p)
+                , canonicalBinders'
+                )
+      elaborateReft (reft, t) buildRFunContTrivial buildRFunCont
+
+        -- (\bs' ee | isClassType tin -> do
+        --    let eeRenamed = renameDictBinder canonicalBinders bs' ee
+        --    pure (RFun bind eTin eToutRenamed (MkUReft (F.Reft (vv, eeRenamed)) p), bs')
+        -- )
+    -- YL: implicit dictionary param doesn't seem possible..
+    RImpF bind tin tout ureft@(MkUReft reft@(F.Reft (vv, _oldE)) p) -> do
+      let partialFunTp =
+            Free (RImpFF bind (wrap $ specTypeToPartial tin) (pure ()) ureft) :: PartialSpecType
+          partialTp' = partialTp >> partialFunTp :: PartialSpecType
+      (eTin , bs ) <- elaborateSpecType' partialTp' coreToLogic simplify tin
+      (eTout, bs') <- elaborateSpecType' partialTp' coreToLogic simplify tout
+      let (eToutRenamed, canonicalBinders) =
+            canonicalizeDictBinder bs (eTout, bs')
+
+      -- eTin and eTout might have different dictionary names
+      -- need to do a substitution to make the reference to dictionaries consistent
+      -- if isClassType eTin
+      elaborateReft
+        (reft, t)
+        (pure (RImpF bind eTin eToutRenamed ureft, canonicalBinders))
+        (\bs'' ee -> do
+          let (eeRenamed, canonicalBinders') =
+                canonicalizeDictBinder canonicalBinders (ee, bs'')
+          pure
+            ( RImpF bind eTin eTout (MkUReft (F.Reft (vv, eeRenamed)) p)
+            , canonicalBinders'
+            )
+        )
+    -- support for RankNTypes/ref
+    RAllT (RTVar tv ty) tout ureft@(MkUReft ref@(F.Reft (vv, _oldE)) p) -> do
+      (eTout, bs) <- elaborateSpecType'
+        (partialTp >> Free (RAllTF (RTVar tv ty) (pure ()) ureft))
+        coreToLogic
+        simplify
+        tout
+      elaborateReft
+        (ref, RVar tv mempty)
+        (pure (RAllT (RTVar tv ty) eTout ureft, bs))
+        (\bs' ee ->
+          let (eeRenamed, canonicalBinders) =
+                canonicalizeDictBinder bs (ee, bs')
+          in  pure
+                ( RAllT (RTVar tv ty) eTout (MkUReft (F.Reft (vv, eeRenamed)) p)
+                , canonicalBinders
+                )
+        )
+      -- pure (RAllT (RTVar tv ty) eTout ref, bts')
+    -- todo: might as well print an error message?
+    RAllP pvbind tout -> do
+      (eTout, bts') <- elaborateSpecType'
+        (partialTp >> Free (RAllPF pvbind (pure ())))
+        coreToLogic
+        simplify
+        tout
+      pure (RAllP pvbind eTout, bts')
+    -- pargs not handled for now
+    -- RApp tycon args pargs reft
+    RApp tycon args pargs ureft@(MkUReft reft@(F.Reft (vv, _)) p)
+      | isClass tycon -> pure (t, [])
+      | otherwise -> do
+        args' <- mapM
+          (fmap fst . elaborateSpecType' partialTp coreToLogic simplify)
+          args
+        elaborateReft
+          (reft, t)
+          (pure (RApp tycon args' pargs ureft, []))
+          (\bs' ee ->
+            pure (RApp tycon args' pargs (MkUReft (F.Reft (vv, ee)) p), bs')
+          )
+    RAppTy arg res ureft@(MkUReft reft@(F.Reft (vv, _)) p) -> do
+      (eArg, bs ) <- elaborateSpecType' partialTp coreToLogic simplify arg
+      (eRes, bs') <- elaborateSpecType' partialTp coreToLogic simplify res
+      let (eResRenamed, canonicalBinders) =
+            canonicalizeDictBinder bs (eRes, bs')
+      elaborateReft
+        (reft, t)
+        (pure (RAppTy eArg eResRenamed ureft, canonicalBinders))
+        (\bs'' ee ->
+          let (eeRenamed, canonicalBinders') =
+                canonicalizeDictBinder canonicalBinders (ee, bs'')
+          in  pure
+                ( RAppTy eArg eResRenamed (MkUReft (F.Reft (vv, eeRenamed)) p)
+                , canonicalBinders'
+                )
+        )
+    -- todo: Existential support
+    RAllE bind allarg ty -> do
+      (eAllarg, bs ) <- elaborateSpecType' partialTp coreToLogic simplify allarg
+      (eTy    , bs') <- elaborateSpecType' partialTp coreToLogic simplify ty
+      let (eTyRenamed, canonicalBinders) = canonicalizeDictBinder bs (eTy, bs')
+      pure (RAllE bind eAllarg eTyRenamed, canonicalBinders)
+    REx bind allarg ty -> do
+      (eAllarg, bs ) <- elaborateSpecType' partialTp coreToLogic simplify allarg
+      (eTy    , bs') <- elaborateSpecType' partialTp coreToLogic simplify ty
+      let (eTyRenamed, canonicalBinders) = canonicalizeDictBinder bs (eTy, bs')
+      pure (REx bind eAllarg eTyRenamed, canonicalBinders)
+    -- YL: might need to filter RExprArg out and replace RHole with ghc wildcard
+    -- in the future
+    RExprArg _ -> impossible Nothing "RExprArg should not appear here"
+    RHole    _ -> impossible Nothing "RHole should not appear here"
+    RRTy _ _ _ _ ->
+      todo Nothing ("Not sure how to elaborate RRTy" ++ F.showpp t)
+ where
+  boolType = RApp (RTyCon boolTyCon [] def) [] [] mempty :: SpecType
+  elaborateReft
+    :: (F.PPrint a)
+    => (F.Reft, SpecType)
+    -> Ghc a
+    -> ([F.Symbol] -> F.Expr -> Ghc a)
+    -> Ghc a
+  elaborateReft (reft@(F.Reft (vv, e)), vvTy) trivial nonTrivialCont =
+    if isTrivial reft
+      then trivial
+      else do
+        let
+          querySpecType =
+            plugType (rFun vv vvTy boolType) partialTp :: SpecType
+
+          (origBinders, origTyBinders) = F.notracepp "collectSpecTypeBinders"
+            $ collectSpecTypeBinders querySpecType
+
+
+
+          hsExpr =
+            buildHsExpr (fixExprToHsExpr (S.fromList origBinders) e)
+                        querySpecType :: LHsExpr GhcPs
+          exprWithTySigs = noLoc $ ExprWithTySig
+            NoExtField
+            hsExpr
+            (mkLHsSigWcType (specTypeToLHsType querySpecType))
+        (msgs, mbExpr) <- GM.elaborateHsExprInst exprWithTySigs
+
+        -- grab the forall variables from the type of mbExpr
+
+        case mbExpr of
+          Nothing -> panic
+            Nothing
+            (  "Ghc is unable to elaborate the expression: "
+            ++ GM.showPpr exprWithTySigs
+            ++ "\n"
+            ++ -- GM.showPpr
+               (GM.showSDoc $ O.sep (pprErrMsgBagWithLoc (snd msgs)))
+            )
+          Just eeWithLamsCore -> do
+            eeWithLamsCore' <- simplify eeWithLamsCore
+            let
+              (_, tyBinders) =
+                collectSpecTypeBinders
+                  . ofType
+                  . Utils.exprType
+                  $ eeWithLamsCore'
+              substTy = zip tyBinders origTyBinders
+              eeWithLams =
+                coreToLogic (GM.notracePpr "eeWithLamsCore" eeWithLamsCore')
+              (bs', ee) = F.notracepp "grabLams" $ grabLams ([], eeWithLams)
+              (dictbs, nondictbs) =
+                L.partition (F.isPrefixOfSym (F.symbol "$d")) bs'
+          -- invariant: length nondictbs == length origBinders
+              subst = if length nondictbs == length origBinders
+                then F.notracepp "SUBST" $ zip (L.reverse nondictbs) origBinders
+                else panic
+                  Nothing
+                  "Oops, Ghc gave back more/less binders than I expected"
+            ret <- nonTrivialCont
+              dictbs
+              ( renameBinderCoerc (\x -> Mb.fromMaybe x (L.lookup x substTy))
+              . F.substa (\x -> Mb.fromMaybe x (L.lookup x subst))
+              $ F.notracepp
+                  (  "elaborated: subst "
+                  ++ F.showpp substTy
+                  ++ "  "
+                  ++ F.showpp
+                       (ofType $ Utils.exprType eeWithLamsCore' :: SpecType)
+                  )
+                  ee
+              )  -- (GM.dropModuleUnique <$> bs')
+            pure (F.notracepp "result" ret)
+                           -- (F.substa )
+  isTrivial :: F.Reft -> Bool
+  isTrivial (F.Reft (_, F.PTrue)) = True
+  isTrivial _                     = False
+
+  grabLams :: ([F.Symbol], F.Expr) -> ([F.Symbol], F.Expr)
+  grabLams (bs, F.ELam (b, _) e) = grabLams (b : bs, e)
+  grabLams bse                   = bse
+  -- dropBinderUnique :: [F.Symbol] -> F.Expr -> F.Expr
+  -- dropBinderUnique binders = F.notracepp "ElaboratedExpr"
+  --   . F.substa (\x -> if L.elem x binders then GM.dropModuleUnique x else x)
+
+renameBinderCoerc :: (F.Symbol -> F.Symbol) -> F.Expr -> F.Expr
+renameBinderCoerc f = rename
+ where
+  renameSort = renameBinderSort f
+  rename e'@(F.ESym _          ) = e'
+  rename e'@(F.ECon _          ) = e'
+  rename e'@(F.EVar _          ) = e'
+  rename (   F.EApp e0 e1      ) = F.EApp (rename e0) (rename e1)
+  rename (   F.ENeg e0         ) = F.ENeg (rename e0)
+  rename (   F.EBin bop e0 e1  ) = F.EBin bop (rename e0) (rename e1)
+  rename (   F.EIte e0  e1 e2  ) = F.EIte (rename e0) (rename e1) (rename e2)
+  rename (   F.ECst e' t       ) = F.ECst (rename e') (renameSort t)
+  -- rename (F.ELam (x, t) e') = F.ELam (x, renameSort t) (rename e')
+  rename (   F.PAnd es         ) = F.PAnd (rename <$> es)
+  rename (   F.POr  es         ) = F.POr (rename <$> es)
+  rename (   F.PNot e'         ) = F.PNot (rename e')
+  rename (   F.PImp e0 e1      ) = F.PImp (rename e0) (rename e1)
+  rename (   F.PIff e0 e1      ) = F.PIff (rename e0) (rename e1)
+  rename (   F.PAtom brel e0 e1) = F.PAtom brel (rename e0) (rename e1)
+  rename (F.ECoerc t0 t1 e') =
+    F.ECoerc (renameSort t0) (renameSort t1) (rename e')
+  rename e = panic
+    Nothing
+    ("renameBinderCoerc: Not sure how to handle the expression " ++ F.showpp e)
+
+
+
+renameBinderSort :: (F.Symbol -> F.Symbol) -> F.Sort -> F.Sort
+renameBinderSort f = rename
+ where
+  rename F.FInt             = F.FInt
+  rename F.FReal            = F.FReal
+  rename F.FNum             = F.FNum
+  rename F.FFrac            = F.FFrac
+  rename (   F.FObj s     ) = F.FObj (f s)
+  rename t'@(F.FVar _     ) = t'
+  rename (   F.FFunc t0 t1) = F.FFunc (rename t0) (rename t1)
+  rename (   F.FAbs  x  t') = F.FAbs x (rename t')
+  rename t'@(F.FTC _      ) = t'
+  rename (   F.FApp t0 t1 ) = F.FApp (rename t0) (rename t1)
+
+
+
+
+
+-- | Embed fixpoint expressions into parsed haskell expressions.
+--   It allows us to bypass the GHC parser and use arbitrary symbols
+--   for identifiers (compared to using the string API)
+fixExprToHsExpr :: S.HashSet F.Symbol -> F.Expr -> LHsExpr GhcPs
+fixExprToHsExpr env (F.ECon c) = constantToHsExpr c
+fixExprToHsExpr env (F.EVar x) = nlHsVar (symbolToRdrName env x)
+fixExprToHsExpr env (F.EApp e0 e1) =
+  mkHsApp (fixExprToHsExpr env e0) (fixExprToHsExpr env e1)
+fixExprToHsExpr env (F.ENeg e) =
+  mkHsApp (nlHsVar (nameRdrName negateName)) (fixExprToHsExpr env e)
+
+fixExprToHsExpr env (F.EBin bop e0 e1) = mkHsApp
+  (mkHsApp (bopToHsExpr bop) (fixExprToHsExpr env e0))
+  (fixExprToHsExpr env e1)
+fixExprToHsExpr env (F.EIte p e0 e1) = nlHsIf (fixExprToHsExpr env p)
+                                              (fixExprToHsExpr env e0)
+                                              (fixExprToHsExpr env e1)
+
+-- FIXME: convert sort to HsType
+-- This is currently not doable because how do we know if FInt corresponds to
+-- Int or Integer?
+fixExprToHsExpr env (F.ECst e0 _    ) = fixExprToHsExpr env e0
+-- fixExprToHsExpr env (F.PAnd []      ) = nlHsVar true_RDR
+fixExprToHsExpr env (F.PAnd []      ) = nlHsVar true_RDR
+fixExprToHsExpr env (F.PAnd (e : es)) = L.foldr f (fixExprToHsExpr env e) es
+ where
+  f x acc = mkHsApp (mkHsApp (nlHsVar and_RDR) (fixExprToHsExpr env x)) acc
+
+-- This would work in the latest commit
+-- fixExprToHsExpr env (F.PAnd es  ) = mkHsApp
+--   (nlHsVar (varQual_RDR dATA_FOLDABLE (fsLit "and")))
+--   (nlList $ fixExprToHsExpr env <$> es)
+fixExprToHsExpr env (F.POr es) = mkHsApp
+  (nlHsVar (varQual_RDR dATA_FOLDABLE (fsLit "or")))
+  (nlList $ fixExprToHsExpr env <$> es)
+fixExprToHsExpr env (F.PIff e0 e1) = mkHsApp
+  (mkHsApp (nlHsVar (mkVarUnqual (mkFastString "<=>"))) (fixExprToHsExpr env e0)
+  )
+  (fixExprToHsExpr env e1)
+fixExprToHsExpr env (F.PNot e) =
+  mkHsApp (nlHsVar not_RDR) (fixExprToHsExpr env e)
+fixExprToHsExpr env (F.PAtom brel e0 e1) = mkHsApp
+  (mkHsApp (brelToHsExpr brel) (fixExprToHsExpr env e0))
+  (fixExprToHsExpr env e1)
+fixExprToHsExpr env (F.PImp e0 e1) = mkHsApp
+  (mkHsApp (nlHsVar (mkVarUnqual (mkFastString "==>"))) (fixExprToHsExpr env e0)
+  )
+  (fixExprToHsExpr env e1)
+
+fixExprToHsExpr env e =
+  todo Nothing ("toGhcExpr: Don't know how to handle " ++ show e)
+
+constantToHsExpr :: F.Constant -> LHsExpr GhcPs
+-- constantToHsExpr (F.I c) = noLoc (HsLit NoExt (HsInt NoExt (mkIntegralLit c)))
+constantToHsExpr (F.I i) =
+  noLoc (HsOverLit NoExtField (mkHsIntegral (mkIntegralLit i)))
+constantToHsExpr (F.R d) =
+  noLoc (HsOverLit NoExtField (mkHsFractional (mkFractionalLit d)))
+constantToHsExpr _ =
+  todo Nothing "constantToHsExpr: Not sure how to handle constructor L"
+
+-- This probably won't work because of the qualifiers
+bopToHsExpr :: F.Bop -> LHsExpr GhcPs
+bopToHsExpr bop = noLoc (HsVar NoExtField (noLoc (f bop)))
+ where
+  f F.Plus   = plus_RDR
+  f F.Minus  = minus_RDR
+  f F.Times  = times_RDR
+  f F.Div    = mkVarUnqual (fsLit "/")
+  f F.Mod    = varQual_RDR gHC_REAL (fsLit "mod")
+  f F.RTimes = times_RDR
+  f F.RDiv   = varQual_RDR gHC_REAL (fsLit "/")
+
+brelToHsExpr :: F.Brel -> LHsExpr GhcPs
+brelToHsExpr brel = noLoc (HsVar NoExtField (noLoc (f brel)))
+ where
+  f F.Eq = mkVarUnqual (mkFastString "==")
+  f F.Gt = gt_RDR
+  f F.Lt = lt_RDR
+  f F.Ge = ge_RDR
+  f F.Le = le_RDR
+  f F.Ne = mkVarUnqual (mkFastString "/=")
+  f _    = impossible Nothing "brelToExpr: Unsupported operation"
+
+symbolToRdrNameNs :: NameSpace -> F.Symbol -> RdrName
+symbolToRdrNameNs ns x
+  | F.isNonSymbol modName = mkUnqual ns (mkFastString (F.symbolString s))
+  | otherwise = mkQual
+    ns
+    (mkFastString (F.symbolString modName), mkFastString (F.symbolString s))
+  where (modName, s) = GM.splitModuleName x
+
+
+varSymbolToRdrName :: F.Symbol -> RdrName
+varSymbolToRdrName = symbolToRdrNameNs varName
+
+
+-- don't use this function...
+symbolToRdrName :: S.HashSet F.Symbol -> F.Symbol -> RdrName
+symbolToRdrName env x
+  | F.isNonSymbol modName = mkUnqual ns (mkFastString (F.symbolString s))
+  | otherwise = mkQual
+    ns
+    (mkFastString (F.symbolString modName), mkFastString (F.symbolString s))
+ where
+  (modName, s) = GM.splitModuleName x
+  ns | not (S.member x env), Just (c, _) <- F.unconsSym s, isUpper c = dataName
+     | otherwise = varName
+
+
+specTypeToLHsType :: SpecType -> LHsType GhcPs
+-- surprised that the type application is necessary
+specTypeToLHsType =
+  flip (ghylo (distPara @SpecType) distAna) (fmap pure . project) $ \case
+    RVarF (RTV tv) _ -> nlHsTyVar
+      -- (GM.notracePpr ("varRdr" ++ F.showpp (F.symbol tv)) $ getRdrName tv)
+      (symbolToRdrNameNs tvName (F.symbol tv)) 
+    RFunF _ (tin, tin') (_, tout) _
+      | isClassType tin -> noLoc $ HsQualTy NoExtField (noLoc [tin']) tout
+      | otherwise       -> nlHsFunTy tin' tout
+    RImpFF _ (_, tin) (_, tout) _              -> nlHsFunTy tin tout
+    RAllTF (ty_var_value -> (RTV tv)) (_, t) _ -> noLoc $ HsForAllTy
+      NoExtField
+      ForallInvis
+      [noLoc $ UserTyVar NoExtField (noLoc $ symbolToRdrNameNs tvName (F.symbol tv))]
+      t
+    RAllPF _ (_, ty)                    -> ty
+    RAppF RTyCon { rtc_tc = tc } ts _ _ -> nlHsTyConApp
+      (getRdrName tc)
+      [ hst | (t, hst) <- ts, notExprArg t ]
+     where
+      notExprArg (RExprArg _) = False
+      notExprArg _            = True
+    RAllEF _ (_, tin) (_, tout) -> nlHsFunTy tin tout
+    RExF   _ (_, tin) (_, tout) -> nlHsFunTy tin tout
+    -- impossible
+    RAppTyF _ (RExprArg _, _) _ ->
+      impossible Nothing "RExprArg should not appear here"
+    RAppTyF (_, t) (_, t') _ -> nlHsAppTy t t'
+    -- YL: todo..
+    RRTyF _ _ _ (_, t)       -> t
+    RHoleF _                 -> noLoc $ HsWildCardTy NoExtField
+    RExprArgF _ ->
+      todo Nothing "Oops, specTypeToLHsType doesn't know how to handle RExprArg"
+
+-- the core expression returned by ghc might be eta-expanded
+-- we need to do elimination so Pred doesn't contain lambda terms
+eliminateEta :: F.Expr -> F.Expr
+eliminateEta (F.EApp e0 e1) = F.EApp (eliminateEta e0) (eliminateEta e1)
+eliminateEta (F.ENeg e    ) = F.ENeg (eliminateEta e)
+eliminateEta (F.EBin bop e0 e1) =
+  F.EBin bop (eliminateEta e0) (eliminateEta e1)
+eliminateEta (F.EIte e0 e1 e2) =
+  F.EIte (eliminateEta e0) (eliminateEta e1) (eliminateEta e2)
+eliminateEta (F.ECst e0 s) = F.ECst (eliminateEta e0) s
+eliminateEta (F.ELam (x, t) body)
+  | F.EApp e0 (F.EVar x') <- ebody, x == x' && notElem x (F.syms e0) = e0
+  | otherwise = F.ELam (x, t) ebody
+  where ebody = eliminateEta body
+eliminateEta (F.PAnd es   ) = F.PAnd (eliminateEta <$> es)
+eliminateEta (F.POr  es   ) = F.POr (eliminateEta <$> es)
+eliminateEta (F.PNot e    ) = F.PNot (eliminateEta e)
+eliminateEta (F.PImp e0 e1) = F.PImp (eliminateEta e0) (eliminateEta e1)
+eliminateEta (F.PAtom brel e0 e1) =
+  F.PAtom brel (eliminateEta e0) (eliminateEta e1)
+eliminateEta e = e
diff --git a/src/Language/Haskell/Liquid/Bare/Expand.hs b/src/Language/Haskell/Liquid/Bare/Expand.hs
index 09f7745e45..d39d535651 100644
--- a/src/Language/Haskell/Liquid/Bare/Expand.hs
+++ b/src/Language/Haskell/Liquid/Bare/Expand.hs
@@ -63,7 +63,12 @@ makeRTEnv env m mySpec iSpecs lmap
   where
     tAs   = [ t                   | (_, s)  <- specs, t <- Ms.aliases  s ]
     eAs   = [ specREAlias env m e | (m, s)  <- specs, e <- Ms.ealiases s ]
-         ++ [ specREAlias env m e | (_, xl) <- M.toList (lmSymDefs lmap)
+         ++ if typeclass (getConfig env) then []
+                                              -- lmap expansion happens during elaboration
+                                              -- this clearly breaks things if a signature
+                                              -- contains lmap functions but never gets
+                                              -- elaborated
+              else [ specREAlias env m e | (_, xl) <- M.toList (lmSymDefs lmap)
                                   , let e    = lmapEAlias xl             ]
     specs = (m, mySpec) : M.toList iSpecs
 
@@ -481,14 +486,17 @@ cookSpecTypeE :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> Lo
 -----------------------------------------------------------------------------------------
 cookSpecTypeE env sigEnv name x bt
   = id 
-  . fmap (plugHoles sigEnv name x)
+  . fmap (plugHoles (typeclass (getConfig env)) sigEnv name x)
   . fmap (fmap (addTyConInfo   embs tyi))
   . fmap (Bare.txRefSort tyi embs)     
   . fmap (fmap txExpToBind)      -- What does this function DO
   . fmap (specExpandType rtEnv)                        
   . fmap (fmap (generalizeWith x))
-  . fmap (maybePlug       sigEnv name x)
-  . fmap (Bare.qualifyTop    env name l) 
+  . fmap (maybePlug (typeclass (getConfig env))  sigEnv name x)
+  -- we do not qualify/resolve Expr/Pred when typeclass is enabled
+  -- since ghci will not be able to recognize fully qualified names
+  -- instead, we leave qualification to ghc elaboration
+  . fmap (if typeclass (getConfig env) then id else Bare.qualifyTop env name l) 
   . bareSpecType       env name 
   . bareExpandType     rtEnv
   $ bt 
@@ -531,13 +539,13 @@ bareSpecType env name bt = case Bare.ofBareTypeE env name (F.loc bt) Nothing (va
   Left e  -> Left e 
   Right t -> Right (F.atLoc bt t)
 
-maybePlug :: Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType 
-maybePlug sigEnv name kx = case Bare.plugSrc kx of 
+maybePlug :: Bool -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType 
+maybePlug allowTC sigEnv name kx = case Bare.plugSrc kx of 
                              Nothing -> id  
-                             Just _  -> plugHoles sigEnv name kx 
+                             Just _  -> plugHoles allowTC sigEnv name kx 
 
-plugHoles :: Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType 
-plugHoles sigEnv name = Bare.makePluggedSig name embs tyi exports
+plugHoles :: Bool -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType 
+plugHoles allowTC sigEnv name = Bare.makePluggedSig allowTC name embs tyi exports
   where 
     embs              = Bare.sigEmbs     sigEnv 
     tyi               = Bare.sigTyRTyMap sigEnv 
diff --git a/src/Language/Haskell/Liquid/Bare/Measure.hs b/src/Language/Haskell/Liquid/Bare/Measure.hs
index 5a96948e25..61d9db0590 100644
--- a/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/src/Language/Haskell/Liquid/Bare/Measure.hs
@@ -48,29 +48,29 @@ import qualified Language.Haskell.Liquid.Bare.DataType as Bare
 import qualified Language.Haskell.Liquid.Bare.ToBare   as Bare 
 
 --------------------------------------------------------------------------------
-makeHaskellMeasures :: GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
+makeHaskellMeasures :: Bool -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
                     -> [Measure (Located BareType) LocSymbol]
 --------------------------------------------------------------------------------
-makeHaskellMeasures src tycEnv lmap spec 
+makeHaskellMeasures allowTC src tycEnv lmap spec 
           = Bare.measureToBare <$> ms
   where 
-    ms    = makeMeasureDefinition tycEnv lmap cbs <$> mSyms 
+    ms    = makeMeasureDefinition allowTC tycEnv lmap cbs <$> mSyms 
     cbs   = nonRecCoreBinds   (_giCbs src) 
     mSyms = S.toList (Ms.hmeas spec)
   
-makeMeasureDefinition :: Bare.TycEnv -> LogicMap -> [Ghc.CoreBind] -> LocSymbol 
+makeMeasureDefinition :: Bool -> Bare.TycEnv -> LogicMap -> [Ghc.CoreBind] -> LocSymbol 
                       -> Measure LocSpecType Ghc.DataCon
-makeMeasureDefinition tycEnv lmap cbs x = 
+makeMeasureDefinition allowTC tycEnv lmap cbs x = 
   case GM.findVarDef (val x) cbs of
     Nothing       -> Ex.throw $ errHMeas x "Cannot extract measure from haskell function"
-    Just (v, def) -> Ms.mkM vx vinfo mdef MsLifted (makeUnSorted (Ghc.varType v) mdef) 
+    Just (v, def) -> Ms.mkM vx vinfo mdef MsLifted (makeUnSorted allowTC (Ghc.varType v) mdef) 
                      where 
                        vx           = F.atLoc x (F.symbol v)
-                       mdef         = coreToDef' tycEnv lmap vx v def
-                       vinfo        = GM.varLocInfo logicType v
+                       mdef         = coreToDef' allowTC tycEnv lmap vx v def
+                       vinfo        = GM.varLocInfo (logicType allowTC) v
 
-makeUnSorted :: Ghc.Type -> [Def LocSpecType Ghc.DataCon] -> UnSortedExprs
-makeUnSorted t defs
+makeUnSorted :: Bool -> Ghc.Type -> [Def LocSpecType Ghc.DataCon] -> UnSortedExprs
+makeUnSorted allowTC t defs
   | isMeasureType ta 
   = mempty
   | otherwise
@@ -79,7 +79,7 @@ makeUnSorted t defs
     ta = go $ Ghc.expandTypeSynonyms t
 
     go (Ghc.ForAllTy _ t) = go t 
-    go (Ghc.FunTy { Ghc.ft_arg = p, Ghc.ft_res = t}) | Ghc.isClassPred p = go t 
+    go (Ghc.FunTy { Ghc.ft_arg = p, Ghc.ft_res = t}) | isErasable p = go t 
     go (Ghc.FunTy { Ghc.ft_arg = t }) = t 
     go t                  = t -- this should never happen!
 
@@ -90,11 +90,12 @@ makeUnSorted t defs
                              Ms.bodyPred (F.mkEApp (measure def) [F.expr xx]) (body def)) 
 
     xx = F.vv $ Just 10000
+    isErasable = if allowTC then GM.isEmbeddedDictType else Ghc.isClassPred
 
-coreToDef' :: Bare.TycEnv -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr 
+coreToDef' :: Bool -> Bare.TycEnv -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr 
            -> [Def LocSpecType Ghc.DataCon] 
-coreToDef' tycEnv lmap vx v def = 
-  case runToLogic embs lmap dm (errHMeas vx) (coreToDef vx v def) of
+coreToDef' allowTC tycEnv lmap vx v def = 
+  case runToLogic embs lmap dm (errHMeas vx) (coreToDef allowTC vx v def) of
     Right l -> l
     Left e  -> Ex.throw e
   where 
@@ -105,21 +106,21 @@ errHMeas :: LocSymbol -> String -> Error
 errHMeas x str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str)
 
 --------------------------------------------------------------------------------
-makeHaskellInlines :: GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec 
+makeHaskellInlines :: Bool -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec 
                    -> [(LocSymbol, LMap)]
 --------------------------------------------------------------------------------
-makeHaskellInlines src embs lmap spec 
-         = makeMeasureInline embs lmap cbs <$> inls 
+makeHaskellInlines allowTC src embs lmap spec 
+         = makeMeasureInline allowTC embs lmap cbs <$> inls 
   where
     cbs  = nonRecCoreBinds (_giCbs src) 
     inls = S.toList        (Ms.inlines spec)
 
-makeMeasureInline :: F.TCEmb Ghc.TyCon -> LogicMap -> [Ghc.CoreBind] -> LocSymbol
+makeMeasureInline :: Bool -> F.TCEmb Ghc.TyCon -> LogicMap -> [Ghc.CoreBind] -> LocSymbol
                   -> (LocSymbol, LMap)
-makeMeasureInline embs lmap cbs x = 
+makeMeasureInline allowTC embs lmap cbs x = 
   case GM.findVarDef (val x) cbs of 
     Nothing       -> Ex.throw $ errHMeas x "Cannot inline haskell function"
-    Just (v, def) -> (vx, coreToFun' embs Nothing lmap vx v def ok)
+    Just (v, def) -> (vx, coreToFun' allowTC embs Nothing lmap vx v def ok)
                      where 
                        vx         = F.atLoc x (F.symbol v)
                        ok (xs, e) = LMap vx (F.symbol <$> xs) (either id id e)
@@ -129,12 +130,12 @@ makeMeasureInline embs lmap cbs x =
 --   but NOT when lifting inlines (which do not have case-of). 
 --   For details, see [NOTE:Lifting-Stages] 
 
-coreToFun' :: F.TCEmb Ghc.TyCon -> Maybe Bare.DataConMap -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
+coreToFun' :: Bool -> F.TCEmb Ghc.TyCon -> Maybe Bare.DataConMap -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
            -> (([Ghc.Var], Either F.Expr F.Expr) -> a) -> a
-coreToFun' embs dmMb lmap x v def ok = either Ex.throw ok act 
+coreToFun' allowTC embs dmMb lmap x v def ok = either Ex.throw ok act 
   where 
     act  = runToLogic embs lmap dm err xFun 
-    xFun = coreToFun x v def  
+    xFun = coreToFun allowTC x v def  
     err  = errHMeas x  
     dm   = Mb.fromMaybe mempty dmMb 
 
@@ -336,12 +337,12 @@ makeMeasureChecker x s0 dc n = M { msName = x, msSort = s, msEqns = eqn : (eqns
 
 
 ----------------------------------------------------------------------------------------------
-makeMeasureSpec' :: MSpec SpecType Ghc.DataCon -> ([(Ghc.Var, SpecType)], [(LocSymbol, RRType F.Reft)])
+makeMeasureSpec' :: Bool -> MSpec SpecType Ghc.DataCon -> ([(Ghc.Var, SpecType)], [(LocSymbol, RRType F.Reft)])
 ----------------------------------------------------------------------------------------------
-makeMeasureSpec' mspec0 = (ctorTys, measTys) 
+makeMeasureSpec' allowTC mspec0 = (ctorTys, measTys) 
   where 
     ctorTys             = Misc.mapSnd RT.uRType <$> ctorTys0
-    (ctorTys0, measTys) = Ms.dataConTypes mspec 
+    (ctorTys0, measTys) = Ms.dataConTypes allowTC mspec 
     mspec               = first (mapReft ur_reft) mspec0
 
 ----------------------------------------------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/Bare/Misc.hs b/src/Language/Haskell/Liquid/Bare/Misc.hs
index 3dc828558a..3fca560cc5 100644
--- a/src/Language/Haskell/Liquid/Bare/Misc.hs
+++ b/src/Language/Haskell/Liquid/Bare/Misc.hs
@@ -1,8 +1,7 @@
 {-# LANGUAGE FlexibleContexts         #-}
 
 module Language.Haskell.Liquid.Bare.Misc 
-  ( freeSymbols
-  , joinVar
+  ( joinVar
   , mkVarExpr
   , vmap
   , runMapTyVars
@@ -52,75 +51,76 @@ makeSymbols f vs xs
 
 -} 
 
-freeSymbols :: (F.Reftable r, F.Reftable r1, F.Reftable r2, TyConable c, TyConable c1, TyConable c2)
-            => [F.Symbol]
-            -> [(a1, Located (RType c2 tv2 r2))]
-            -> [(a, Located (RType c1 tv1 r1))]
-            -> [(Located (RType c tv r))]
-            -> [LocSymbol]
-freeSymbols xs' xts yts ivs =  [ lx | lx <- Misc.sortNub $ zs ++ zs' ++ zs'' , not (M.member (val lx) knownM) ]
-  where
-    knownM                  = M.fromList [ (x, ()) | x <- xs' ]
-    zs                      = concatMap freeSyms (snd <$> xts)
-    zs'                     = concatMap freeSyms (snd <$> yts)
-    zs''                    = concatMap freeSyms ivs
+-- freeSymbols :: (F.Reftable r, F.Reftable r1, F.Reftable r2, TyConable c, TyConable c1, TyConable c2)
+--             => [F.Symbol]
+--             -> [(a1, Located (RType c2 tv2 r2))]
+--             -> [(a, Located (RType c1 tv1 r1))]
+--             -> [(Located (RType c tv r))]
+--             -> [LocSymbol]
+-- freeSymbols xs' xts yts ivs =  [ lx | lx <- Misc.sortNub $ zs ++ zs' ++ zs'' , not (M.member (val lx) knownM) ]
+--   where
+--     knownM                  = M.fromList [ (x, ()) | x <- xs' ]
+--     zs                      = concatMap freeSyms (snd <$> xts)
+--     zs'                     = concatMap freeSyms (snd <$> yts)
+--     zs''                    = concatMap freeSyms ivs
 
 
 
-freeSyms :: (F.Reftable r, TyConable c) => Located (RType c tv r) -> [LocSymbol]
-freeSyms ty    = [ F.atLoc ty x | x <- tySyms ]
-  where
-    tySyms     = Misc.sortNub $ concat $ efoldReft (\_ _ -> True) False (\_ _ -> []) (\_ -> []) (const ()) f (const id) F.emptySEnv [] (val ty)
-    f γ _ r xs = let F.Reft (v, _) = F.toReft r in
-                 [ x | x <- F.syms r, x /= v, not (x `F.memberSEnv` γ)] : xs
+-- freeSyms :: (F.Reftable r, TyConable c) => Located (RType c tv r) -> [LocSymbol]
+-- freeSyms ty    = [ F.atLoc ty x | x <- tySyms ]
+--   where
+--     tySyms     = Misc.sortNub $ concat $ efoldReft (\_ _ -> True) False (\_ _ -> []) (\_ -> []) (const ()) f (const id) F.emptySEnv [] (val ty)
+--     f γ _ r xs = let F.Reft (v, _) = F.toReft r in
+--                  [ x | x <- F.syms r, x /= v, not (x `F.memberSEnv` γ)] : xs
 
 -------------------------------------------------------------------------------
 -- Renaming Type Variables in Haskell Signatures ------------------------------
 -------------------------------------------------------------------------------
-runMapTyVars :: Type -> SpecType -> (PJ.Doc -> PJ.Doc -> Error) -> Either Error MapTyVarST
-runMapTyVars τ t err = execStateT (mapTyVars τ t) (MTVST [] err) 
+runMapTyVars :: Bool -> Type -> SpecType -> (PJ.Doc -> PJ.Doc -> Error) -> Either Error MapTyVarST
+runMapTyVars allowTC τ t err = execStateT (mapTyVars allowTC τ t) (MTVST [] err) 
 
 data MapTyVarST = MTVST
   { vmap   :: [(Var, RTyVar)]
   , errmsg :: PJ.Doc -> PJ.Doc -> Error
   }
 
-mapTyVars :: Type -> SpecType -> StateT MapTyVarST (Either Error) ()
-mapTyVars t (RImpF _ _ t' _)
-   = mapTyVars t t'
-mapTyVars (FunTy { ft_arg = τ, ft_res = τ'}) t 
-  | isClassPred τ
-  = mapTyVars τ' t
-mapTyVars (FunTy { ft_arg = τ, ft_res = τ'}) (RFun _ t t' _)
-   = mapTyVars τ t >> mapTyVars τ' t'
-mapTyVars τ (RAllT _ t _)
-  = mapTyVars τ t
-mapTyVars (TyConApp _ τs) (RApp _ ts _ _)
-   = zipWithM_ mapTyVars τs (matchKindArgs' τs ts)
-mapTyVars (TyVarTy α) (RVar a _)
+mapTyVars :: Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
+mapTyVars allowTC t (RImpF _ _ t' _)
+   = mapTyVars allowTC t t'
+mapTyVars allowTC (FunTy { ft_arg = τ, ft_res = τ'}) t 
+  | isErasable τ
+  = mapTyVars allowTC τ' t
+  where isErasable = if allowTC then isEmbeddedDictType else isClassPred
+mapTyVars allowTC (FunTy { ft_arg = τ, ft_res = τ'}) (RFun _ t t' _)
+   = mapTyVars allowTC τ t >> mapTyVars allowTC τ' t'
+mapTyVars allowTC τ (RAllT _ t _)
+  = mapTyVars allowTC τ t
+mapTyVars allowTC (TyConApp _ τs) (RApp _ ts _ _)
+   = zipWithM_ (mapTyVars allowTC) τs (matchKindArgs' τs ts)
+mapTyVars allowTC (TyVarTy α) (RVar a _)
    = do s  <- get
         s' <- mapTyRVar α a s
         put s'
-mapTyVars τ (RAllP _ t)
-  = mapTyVars τ t
-mapTyVars τ (RAllE _ _ t)
-  = mapTyVars τ t
-mapTyVars τ (RRTy _ _ _ t)
-  = mapTyVars τ t
-mapTyVars τ (REx _ _ t)
-  = mapTyVars τ t
-mapTyVars _ (RExprArg _)
+mapTyVars allowTC τ (RAllP _ t)
+  = mapTyVars allowTC τ t
+mapTyVars allowTC τ (RAllE _ _ t)
+  = mapTyVars allowTC τ t
+mapTyVars allowTC τ (RRTy _ _ _ t)
+  = mapTyVars allowTC τ t
+mapTyVars allowTC τ (REx _ _ t)
+  = mapTyVars allowTC τ t
+mapTyVars allowTC _ (RExprArg _)
   = return ()
-mapTyVars (AppTy τ τ') (RAppTy t t' _)
-  = do  mapTyVars τ t
-        mapTyVars τ' t'
-mapTyVars _ (RHole _)
+mapTyVars allowTC (AppTy τ τ') (RAppTy t t' _)
+  = do  mapTyVars allowTC τ t
+        mapTyVars allowTC τ' t'
+mapTyVars allowTC _ (RHole _)
   = return ()
-mapTyVars k _ | isKind k
+mapTyVars allowTC k _ | isKind k
   = return ()
-mapTyVars (ForAllTy _ τ) t
-  = mapTyVars τ t
-mapTyVars hsT lqT
+mapTyVars allowTC (ForAllTy _ τ) t
+  = mapTyVars allowTC τ t
+mapTyVars allowTC hsT lqT
   = do err <- errmsg <$> get
        throwError (err (F.pprint hsT) (F.pprint lqT)) 
 
diff --git a/src/Language/Haskell/Liquid/Bare/Plugged.hs b/src/Language/Haskell/Liquid/Bare/Plugged.hs
index 18b3b21ae8..05caf886fb 100644
--- a/src/Language/Haskell/Liquid/Bare/Plugged.hs
+++ b/src/Language/Haskell/Liquid/Bare/Plugged.hs
@@ -46,16 +46,16 @@ import qualified Language.Haskell.Liquid.Bare.Misc  as Bare
 --   this module is responsible for plugging the holes we obviously cannot
 --   assume, as in e.g. L.H.L.Constraint.* that they do not appear.
 --------------------------------------------------------------------------------
-makePluggedSig :: ModName -> F.TCEmb Ghc.TyCon -> TyConMap -> Ghc.NameSet
+makePluggedSig :: Bool -> ModName -> F.TCEmb Ghc.TyCon -> TyConMap -> Ghc.NameSet
                -> Bare.PlugTV Ghc.Var -> LocSpecType
                -> LocSpecType
 
-makePluggedSig name embs tyi exports kx t 
+makePluggedSig allowTC name embs tyi exports kx t 
   | Just x <- kxv = mkPlug x 
   | otherwise     = t
   where 
     kxv           = Bare.plugSrc kx
-    mkPlug x      = plugHoles kx embs tyi  r τ t
+    mkPlug x      = plugHoles allowTC kx embs tyi  r τ t
       where
         τ         = Ghc.expandTypeSynonyms (Ghc.varType x)
         r         = maybeTrue x name exports
@@ -69,20 +69,21 @@ makePluggedSig name embs tyi exports kx t
 -- plugHoles _         = plugHoles_old
 
 plugHoles :: (Ghc.NamedThing a, PPrint a, Show a) 
-          => Bare.PlugTV a
+          => Bool
+          -> Bare.PlugTV a
           -> F.TCEmb Ghc.TyCon
           -> Bare.TyConMap
           -> (SpecType -> RReft -> RReft)
           -> Ghc.Type
           -> LocSpecType
           -> LocSpecType
-plugHoles (Bare.HsTV x) a b = plugHoles_old a b x 
-plugHoles (Bare.LqTV x) a b = plugHoles_new a b x 
-plugHoles _             _ _ = \_ _ t -> t
+plugHoles allowTC (Bare.HsTV x) a b = plugHoles_old allowTC a b x 
+plugHoles allowTC (Bare.LqTV x) a b = plugHoles_new allowTC a b x 
+plugHoles _ _                   _ _ = \_ _ t -> t
 
 
-makePluggedDataCon :: F.TCEmb Ghc.TyCon -> Bare.TyConMap -> Located DataConP -> Located DataConP
-makePluggedDataCon embs tyi ldcp 
+makePluggedDataCon :: Bool -> F.TCEmb Ghc.TyCon -> Bare.TyConMap -> Located DataConP -> Located DataConP
+makePluggedDataCon allowTC embs tyi ldcp 
   | mismatchFlds      = Ex.throw (err "fields")
   | mismatchTyVars    = Ex.throw (err "type variables")
   | otherwise         = F.atLoc ldcp $ F.notracepp "makePluggedDataCon" $ dcp 
@@ -91,9 +92,9 @@ makePluggedDataCon embs tyi ldcp
                           , dcpTyRes      = tRes 
                           }
   where 
-    (tArgs, tRes)     = plugMany       embs tyi ldcp (das, dts, dt) (dcVars, dcArgs, dcpTyRes dcp)
+    (tArgs, tRes)     = plugMany allowTC  embs tyi ldcp (das, dts, dt) (dcVars, dcArgs, dcpTyRes dcp)
     (das, _, dts, dt) = {- F.notracepp ("makePluggedDC: " ++ F.showpp dc) $ -} Ghc.dataConSig dc
-    dcArgs            = filter (not . isClassType . snd) $ reverse (dcpTyArgs dcp)
+    dcArgs            = filter (not . (if allowTC then isEmbeddedClass else isClassType) . snd) $ reverse (dcpTyArgs dcp)
     dcVars            = if isGADT 
                           then padGADVars $ L.nub (dcpFreeTyVars dcp ++ (concatMap (map ty_var_value . freeTyVars) (dcpTyRes dcp:(snd <$> dcArgs))))
                           else dcpFreeTyVars dcp 
@@ -125,16 +126,16 @@ makePluggedDataCon embs tyi ldcp
 -- 
 --   and not, forall b. a -> a -> Bool.
 
-plugMany :: F.TCEmb Ghc.TyCon -> Bare.TyConMap 
+plugMany :: Bool -> F.TCEmb Ghc.TyCon -> Bare.TyConMap 
          -> Located DataConP            
          -> ([Ghc.Var], [Ghc.Type],             Ghc.Type)   -- ^ hs type 
          -> ([RTyVar] , [(F.Symbol, SpecType)], SpecType)   -- ^ lq type 
          -> ([(F.Symbol, SpecType)], SpecType)              -- ^ plugged lq type
-plugMany embs tyi ldcp (hsAs, hsArgs, hsRes) (lqAs, lqArgs, lqRes) 
+plugMany allowTC embs tyi ldcp (hsAs, hsArgs, hsRes) (lqAs, lqArgs, lqRes) 
                      = F.notracepp msg (drop nTyVars (zip xs ts), t) 
   where 
     (_,(xs,ts,_), t) = bkArrow (val pT) 
-    pT               = plugHoles (Bare.LqTV dcName) embs tyi (const killHoles) hsT (F.atLoc ldcp lqT)
+    pT               = plugHoles allowTC (Bare.LqTV dcName) embs tyi (const killHoles) hsT (F.atLoc ldcp lqT)
     hsT              = foldr (Ghc.mkFunTy Ghc.VisArg) hsRes hsArgs' 
     lqT              = foldr (uncurry rFun) lqRes lqArgs' 
     hsArgs'          = [ Ghc.mkTyVarTy a               | a <- hsAs] ++ hsArgs 
@@ -145,25 +146,26 @@ plugMany embs tyi ldcp (hsAs, hsArgs, hsRes) (lqAs, lqArgs, lqRes)
 
 plugHoles_old, plugHoles_new 
   :: (Ghc.NamedThing a, PPrint a, Show a)
-  => F.TCEmb Ghc.TyCon
+  => Bool
+  -> F.TCEmb Ghc.TyCon
   -> Bare.TyConMap 
   -> a
   -> (SpecType -> RReft -> RReft)
   -> Ghc.Type
   -> LocSpecType
   -> LocSpecType
-  
+
 -- NOTE: this use of toType is safe as rt' is derived from t.
-plugHoles_old tce tyi x f t0 zz@(Loc l l' st0) 
+plugHoles_old allowTC tce tyi x f t0 zz@(Loc l l' st0) 
     = Loc l l' 
     . mkArrow (zip (updateRTVar <$> αs') rs) ps' [] [] 
     . makeCls cs' 
     . goPlug tce tyi err f (subts su rt) 
     . mapExprReft (\_ -> F.applyCoSub coSub) 
     . subts su 
-    $ st 
+    $ st
   where 
-    tyvsmap      = case Bare.runMapTyVars (toType rt) st err of
+    tyvsmap      = case Bare.runMapTyVars allowTC (toType rt) st err of
                           Left e  -> Ex.throw e 
                           Right s -> Bare.vmap s
     su           = [(y, rTyVar x)           | (x, y) <- tyvsmap]
@@ -184,7 +186,7 @@ plugHoles_old tce tyi x f t0 zz@(Loc l l' st0)
                           (Ghc.getSrcSpan x) 
 
 
-plugHoles_new tce tyi x f t0 zz@(Loc l l' st0) 
+plugHoles_new allowTC tce tyi x f t0 zz@(Loc l l' st0) 
     = Loc l l' 
     . mkArrow (zip (updateRTVar <$> as'') rs) ps [] [] 
     . makeCls cs' 
@@ -196,7 +198,7 @@ plugHoles_new tce tyi x f t0 zz@(Loc l l' st0)
     (as',rs)     = unzip as 
     cs'          = [ (F.dummySymbol, ct) | (c, t) <- cs, let ct = tx (RApp c t [] mempty) ]
     tx           = subts su
-    su           = case Bare.runMapTyVars (toType rt) st err of
+    su           = case Bare.runMapTyVars allowTC (toType rt) st err of
                           Left e  -> Ex.throw e 
                           Right s -> [ (rTyVar x, y) | (x, y) <- Bare.vmap s]
     (as,_,cs,rt) = bkUnivClass (ofType (Ghc.expandTypeSynonyms t0) :: SpecType)
diff --git a/src/Language/Haskell/Liquid/Bare/Resolve.hs b/src/Language/Haskell/Liquid/Bare/Resolve.hs
index ab5ba28b19..8ae7749d86 100644
--- a/src/Language/Haskell/Liquid/Bare/Resolve.hs
+++ b/src/Language/Haskell/Liquid/Bare/Resolve.hs
@@ -692,8 +692,9 @@ ofBareType env name l ps t = either fail id (ofBareTypeE env name l ps t)
     fail                   = Ex.throw 
     -- fail                   = Misc.errorP "error-ofBareType" . F.showpp 
 
-ofBareTypeE :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> Either UserError SpecType 
-ofBareTypeE env name l ps t = ofBRType env name (resolveReft env name l ps t) l t 
+ofBareTypeE :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> Either UserError SpecType
+ofBareTypeE env name l ps t = ofBRType env name (if allowTC then const id else resolveReft env name l ps t) l t
+  where allowTC = typeclass (getConfig env) -- don't resolve here. resolve later using elaboration instead
 
 resolveReft :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> [F.Symbol] -> RReft -> RReft 
 resolveReft env name l ps t bs
diff --git a/src/Language/Haskell/Liquid/Bare/Typeclass.hs b/src/Language/Haskell/Liquid/Bare/Typeclass.hs
new file mode 100644
index 0000000000..0f55fb414b
--- /dev/null
+++ b/src/Language/Haskell/Liquid/Bare/Typeclass.hs
@@ -0,0 +1,390 @@
+{-# LANGUAGE OverloadedStrings         #-}
+{-# LANGUAGE FlexibleContexts          #-}
+module Language.Haskell.Liquid.Bare.Typeclass
+  ( compileClasses
+  , elaborateClassDcp
+  , makeClassAuxTypes
+  -- , makeClassSelectorSigs
+  )
+where
+
+-- TODO: Handle typeclasses with a single method (newtype)
+
+import           Control.Monad                  ( forM, guard )
+import qualified Data.List                     as L
+import qualified Data.HashSet                  as S
+import qualified Data.Maybe                    as Mb
+import qualified Language.Fixpoint.Types       as F
+import qualified Language.Fixpoint.Misc        as Misc
+import           Language.Haskell.Liquid.Bare.Elaborate
+import qualified Language.Haskell.Liquid.GHC.Misc
+                                               as GM
+import qualified Language.Haskell.Liquid.GHC.API
+                                               as Ghc
+import qualified Language.Haskell.Liquid.Misc  as Misc
+import           Language.Haskell.Liquid.Types
+import qualified Language.Haskell.Liquid.Types.RefType
+                                               as RT
+import qualified Language.Haskell.Liquid.Bare.Types
+                                               as Bare
+import qualified Language.Haskell.Liquid.Bare.Resolve
+                                               as Bare
+import qualified Language.Haskell.Liquid.Measure
+                                               as Ms
+-- import           Language.Haskell.Liquid.Types.Types
+import qualified Data.HashMap.Strict           as M
+
+
+
+compileClasses
+  :: GhcSrc
+  -> Bare.Env
+  -> (ModName, Ms.BareSpec)
+  -> [(ModName, Ms.BareSpec)]
+  -> (Ms.BareSpec, [(Ghc.ClsInst, [Ghc.Var])])
+compileClasses src env (name, spec) rest =
+  (spec { sigs = sigs' } <> clsSpec, instmethods)
+ where
+  clsSpec = mempty
+    { dataDecls = clsDecls
+    , reflects  = F.notracepp "reflects " $ S.fromList
+                    (  fmap
+                        ( fmap GM.dropModuleNames
+                        . GM.namedLocSymbol
+                        . Ghc.instanceDFunId
+                        . fst
+                        )
+                        instClss
+                    ++ methods
+                    )
+    }
+  clsDecls                = makeClassDataDecl (M.toList refinedMethods)
+      -- class methods
+  (refinedMethods, sigs') = foldr grabClassSig (mempty, mempty) (sigs spec)
+  grabClassSig
+    :: (F.LocSymbol, ty)
+    -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.LocSymbol, ty)])
+    -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.LocSymbol, ty)])
+  grabClassSig sig@(lsym, ref) (refs, sigs') = case clsOp of
+    Nothing         -> (refs, sig : sigs')
+    Just (cls, sig) -> (M.alter (merge sig) cls refs, sigs')
+   where
+    clsOp = do
+      var <- Bare.maybeResolveSym env name "grabClassSig" lsym
+      cls <- Ghc.isClassOpId_maybe var
+      pure (cls, (var, ref))
+    merge sig v = case v of
+      Nothing -> Just [sig]
+      Just vs -> Just (sig : vs)
+  methods = [ GM.namedLocSymbol x | (_, xs) <- instmethods, x <- xs ]
+      -- instance methods
+
+  mkSymbol x
+    | Ghc.isDictonaryId x = F.mappendSym "$" (F.dropSym 2 $ GM.simplesymbol x)
+    | otherwise           = F.dropSym 2 $ GM.simplesymbol x
+
+  instmethods :: [(Ghc.ClsInst, [Ghc.Var])]
+  instmethods =
+    [ (inst, ms)
+    | (inst, cls) <- instClss
+    , let selIds = GM.dropModuleNames . F.symbol <$> Ghc.classAllSelIds cls
+    , (_, e) <- Mb.maybeToList
+      (GM.findVarDefMethod
+        (GM.dropModuleNames . F.symbol $ Ghc.instanceDFunId inst)
+        (_giCbs src)
+      )
+    , let ms = filter (\x -> GM.isMethod x && elem (mkSymbol x) selIds)
+                      (freeVars mempty e)
+    ]
+  instClss :: [(Ghc.ClsInst, Ghc.Class)]
+  instClss =
+    [ (inst, cls)
+    | inst <- mconcat . Mb.maybeToList . _gsCls $ src
+    , Ghc.moduleName (Ghc.nameModule (Ghc.getName inst)) == getModName name
+    , let cls = Ghc.is_cls inst
+    , cls `elem` refinedClasses
+    ]
+  refinedClasses :: [Ghc.Class]
+  refinedClasses =
+    Mb.mapMaybe resolveClassMaybe clsDecls
+      ++ concatMap (Mb.mapMaybe resolveClassMaybe . dataDecls . snd) rest
+  resolveClassMaybe :: DataDecl -> Maybe Ghc.Class
+  resolveClassMaybe d =
+    Bare.maybeResolveSym env
+                         name
+                         "resolveClassMaybe"
+                         (dataNameSymbol . tycName $ d)
+      >>= Ghc.tyConClass_maybe
+
+
+-- a list of class with user defined refinements
+makeClassDataDecl :: [(Ghc.Class, [(Ghc.Id, LocBareType)])] -> [DataDecl]
+makeClassDataDecl = fmap (uncurry classDeclToDataDecl)
+
+-- TODO: I should have the knowledge to construct DataConP manually than
+-- following the rather unwieldy pipeline: Resolved -> Unresolved -> Resolved.
+-- maybe this should be fixed right after the GHC API refactoring?
+classDeclToDataDecl :: Ghc.Class -> [(Ghc.Id, LocBareType)] -> DataDecl
+classDeclToDataDecl cls refinedIds = DataDecl
+  { tycName   = DnName (F.symbol <$> GM.locNamedThing cls)
+  , tycTyVars = tyVars
+  , tycPVars  = []
+  , tycDCons  = [dctor]
+  , tycSrcPos = F.loc . GM.locNamedThing $ cls
+  , tycSFun   = Nothing
+  , tycPropTy = Nothing
+  , tycKind   = DataUser
+  }
+ where
+  dctor = DataCtor { dcName   = F.dummyLoc $ F.symbol classDc
+    -- YL: same as class tyvars??
+    -- Ans: it's been working so far so probably yes
+                   , dcTyVars = tyVars
+    -- YL: what is theta?
+    -- Ans: where class constraints should go yet remain unused
+    -- maybe should factor this out?
+                   , dcTheta  = []
+                   , dcFields = fields
+                   , dcResult = Nothing
+                   }
+
+  tyVars = F.symbol <$> Ghc.classTyVars cls
+
+  fields = fmap attachRef classIds
+  attachRef sid
+    | Just ref <- L.lookup sid refinedIds
+    = (F.symbol sid, RT.subts tyVarSubst (F.val ref))
+    | otherwise
+    = (F.symbol sid, RT.bareOfType . dropTheta . Ghc.varType $ sid)
+
+  tyVarSubst = [ (GM.dropModuleUnique v, v) | v <- tyVars ]
+
+  -- FIXME: dropTheta should not be needed as long as we 
+  -- handle classes and ordinary data types separately
+  -- Might be helpful if we add an additional field for
+  -- typeclasses
+  dropTheta :: Ghc.Type -> Ghc.Type
+  dropTheta = Misc.thd3 . Ghc.tcSplitMethodTy
+
+  classIds  = Ghc.classAllSelIds cls
+  classDc   = Ghc.classDataCon cls
+
+-- | 'elaborateClassDcp' behaves differently from other datacon
+--    functions. Each method type contains the full forall quantifiers
+--    instead of having them chopped off
+elaborateClassDcp
+  :: (Ghc.CoreExpr -> F.Expr)
+  -> (Ghc.CoreExpr -> Ghc.Ghc Ghc.CoreExpr)
+  -> DataConP
+  -> Ghc.Ghc (DataConP, DataConP)
+elaborateClassDcp coreToLg simplifier dcp = do
+  t' <- flip (zipWith addCoherenceOblig) prefts
+    <$> forM fts (elaborateSpecType coreToLg simplifier)
+  let ts' = elaborateMethod (F.symbol dc) (S.fromList xs) <$> t'
+  pure
+    ( dcp { dcpTyArgs = zip xs (stripPred <$> ts') }
+    , dcp { dcpTyArgs = fmap (\(x, t) -> (x, strengthenTy x t)) (zip xs t') }
+    )
+ where
+  addCoherenceOblig :: SpecType -> Maybe RReft -> SpecType
+  addCoherenceOblig t Nothing  = t
+  addCoherenceOblig t (Just r) = fromRTypeRep rrep
+    { ty_res = res `RT.strengthen` r
+    }
+   where
+    rrep = toRTypeRep t
+    res  = ty_res rrep
+  prefts =
+    L.reverse
+      .  take (length fts)
+      $  fmap (Just . flip MkUReft mempty . mconcat) preftss
+      ++ repeat Nothing
+  preftss = (fmap . fmap) (uncurry (GM.coherenceObligToRef recsel))
+                          (GM.buildCoherenceOblig cls)
+
+  -- ugly, should have passed cls as an argument
+  cls      = Mb.fromJust $ Ghc.tyConClass_maybe (Ghc.dataConTyCon dc)
+  recsel   = F.symbol ("lq$recsel" :: String)
+  resTy    = dcpTyRes dcp
+  dc       = dcpCon dcp
+  tvars    = (\x -> (makeRTVar x, mempty)) <$> dcpFreeTyVars dcp
+      -- check if the names are qualified
+  (xs, ts) = unzip (dcpTyArgs dcp)
+  fts      = fullTy <$> ts
+      -- turns forall a b. (a -> b) -> f a -> f b into
+      -- forall f. Functor f => forall a b. (a -> b) -> f a -> f b
+  stripPred :: SpecType -> SpecType
+  stripPred = Misc.fourth4 . bkUnivClass
+  fullTy :: SpecType -> SpecType
+  fullTy t = mkArrow
+    tvars
+    []
+    []
+    [ ( recsel{- F.symbol dc-}
+      , resTy
+      , mempty
+      )
+    ]
+    t
+  -- YL: is this redundant if we already have strengthenClassSel?
+  strengthenTy :: F.Symbol -> SpecType -> SpecType
+  strengthenTy x t = mkUnivs tvs pvs (RFun z cls (t' `RT.strengthen` mt) r)
+   where
+    (tvs, pvs, RFun z cls t' r) = bkUniv t
+    vv = rTypeValueVar t'
+    mt = RT.uReft (vv, F.PAtom F.Eq (F.EVar vv) (F.EApp (F.EVar x) (F.EVar z)))
+
+
+elaborateMethod :: F.Symbol -> S.HashSet F.Symbol -> SpecType -> SpecType
+elaborateMethod dc methods t = mapExprReft
+  (\_ -> substClassOpBinding tcbind dc methods)
+  t
+ where
+  tcbind = grabtcbind t
+  grabtcbind :: SpecType -> F.Symbol
+  grabtcbind t =
+    F.notracepp "grabtcbind"
+      $ case Misc.fst3 . Misc.snd3 . bkArrow . Misc.thd3 . bkUniv $ t of
+          tcbind : _ -> tcbind
+          []         -> impossible
+            Nothing
+            (  "elaborateMethod: inserted dictionary binder disappeared:"
+            ++ F.showpp t
+            )
+
+
+-- Before: Functor.fmap ($p1Applicative $dFunctor)
+-- After: Funcctor.fmap ($p1Applicative##GHC.Base.Applicative)
+substClassOpBinding
+  :: F.Symbol -> F.Symbol -> S.HashSet F.Symbol -> F.Expr -> F.Expr
+substClassOpBinding tcbind dc methods e = go e
+ where
+  go :: F.Expr -> F.Expr
+  go (F.EApp e0 e1)
+    | F.EVar x <- e0, F.EVar y <- e1, y == tcbind, S.member x methods = F.EVar
+      (x `F.suffixSymbol` dc)
+    | otherwise = F.EApp (go e0) (go e1)
+  go (F.ENeg e          ) = F.ENeg (go e)
+  go (F.EBin bop e0 e1  ) = F.EBin bop (go e0) (go e1)
+  go (F.EIte e0  e1 e2  ) = F.EIte (go e0) (go e1) (go e2)
+  go (F.ECst e0     s   ) = F.ECst (go e0) s
+  go (F.ELam (x, t) body) = F.ELam (x, t) (go body)
+  go (F.PAnd es         ) = F.PAnd (go <$> es)
+  go (F.POr  es         ) = F.POr (go <$> es)
+  go (F.PNot e          ) = F.PNot (go e)
+  go (F.PImp e0 e1      ) = F.PImp (go e0) (go e1)
+  go (F.PIff e0 e1      ) = F.PIff (go e0) (go e1)
+  go (F.PAtom brel e0 e1) = F.PAtom brel (go e0) (go e1)
+  -- a catch-all binding is not a good idea
+  go e                    = e
+
+
+makeClassAuxTypes ::
+     (SpecType -> Ghc.Ghc SpecType)
+  -> [F.Located DataConP]
+  -> [(Ghc.ClsInst, [Ghc.Var])]
+  -> Ghc.Ghc [(Ghc.Var, LocSpecType)]
+makeClassAuxTypes elab dcps xs = Misc.concatMapM (makeClassAuxTypesOne elab) dcpInstMethods
+  where
+    dcpInstMethods = do
+      dcp <- dcps
+      (inst, methods) <- xs
+      let dc = dcpCon . F.val $ dcp
+              -- YL: only works for non-newtype class
+          dc' = Ghc.classDataCon $ Ghc.is_cls inst
+      guard $ dc == dc'
+      pure (dcp, inst, methods)
+
+      
+makeClassAuxTypesOne ::
+     (SpecType -> Ghc.Ghc SpecType)
+  -> (F.Located DataConP, Ghc.ClsInst, [Ghc.Var])
+  -> Ghc.Ghc [(Ghc.Var, LocSpecType)]
+makeClassAuxTypesOne elab (ldcp, inst, methods) =
+  forM methods $ \method -> do
+    let (headlessSig, preft) =
+          case L.lookup (mkSymbol method) yts' of
+            Nothing ->
+              impossible Nothing ("makeClassAuxTypesOne : unreachable?" ++ F.showpp (mkSymbol method) ++ " " ++ F.showpp yts)
+            Just sig -> sig
+        -- dict binder will never be changed because we optimized PAnd[]
+        -- lq0 lq1 ...
+        ptys    = [(F.vv (Just i), pty, mempty) | (i,pty) <- zip [0,1..] isPredSpecTys]
+        fullSig =
+          mkArrow
+            (zip isRTvs (repeat mempty))
+            []
+            []
+            ptys .
+          subst (zip clsTvs isSpecTys) $
+          headlessSig
+    elaboratedSig  <- flip addCoherenceOblig preft <$> elab fullSig
+
+    let retSig =  mapExprReft (\_ -> substAuxMethod dfunSym methodsSet) (F.notracepp ("elaborated" ++ GM.showPpr method) elaboratedSig)
+    pure (method, F.dummyLoc retSig)
+
+  -- "is" is used as a shorthand for instance, following the convention of the Ghc api
+  where
+    -- recsel = F.symbol ("lq$recsel" :: String)
+    (_,predTys,_,_) = Ghc.instanceSig inst
+    dfunApped = F.mkEApp dfunSymL [F.eVar $ F.vv (Just i) | (i,_) <- zip [0,1..] predTys]
+    prefts  = L.reverse . take (length yts) $ fmap (F.notracepp "prefts" . Just . (flip MkUReft mempty) . mconcat) preftss ++ repeat Nothing
+    preftss = F.notracepp "preftss" $ (fmap.fmap) (uncurry (GM.coherenceObligToRefE dfunApped)) (GM.buildCoherenceOblig cls)
+    yts' = zip (fst <$> yts) (zip (snd <$> yts) prefts)
+    cls = Mb.fromJust . Ghc.tyConClass_maybe $ Ghc.dataConTyCon (dcpCon dcp)
+    addCoherenceOblig  :: SpecType -> Maybe RReft -> SpecType
+    addCoherenceOblig t Nothing = t
+    addCoherenceOblig t (Just r) = F.notracepp "SCSel" . fromRTypeRep $ rrep {ty_res = res `strengthen` r}
+      where rrep = toRTypeRep t
+            res  = ty_res rrep    -- (Monoid.mappend -> $cmappend##Int, ...)
+    -- core rewriting mark2: do the same thing except they don't have to be symbols
+    -- YL: poorly written. use a comprehension instead of assuming 
+    methodsSet = F.notracepp "methodSet" $ M.fromList (zip (F.symbol <$> clsMethods) (F.symbol <$> methods))
+    -- core rewriting mark1: dfunId
+    -- ()
+    dfunSymL = GM.namedLocSymbol $ Ghc.instanceDFunId inst
+    dfunSym = F.val dfunSymL
+    (isTvs, isPredTys, _, isTys) = Ghc.instanceSig inst
+    isSpecTys = ofType <$> isTys
+    isPredSpecTys = ofType <$> isPredTys
+    isRTvs = makeRTVar . rTyVar <$> isTvs
+    dcp = F.val ldcp
+    -- Monoid.mappend, ...
+    clsMethods = filter (\x -> GM.dropModuleNames (F.symbol x) `elem` fmap mkSymbol methods) $
+      Ghc.classAllSelIds (Ghc.is_cls inst)
+    yts = [(GM.dropModuleNames y, t) | (y, t) <- dcpTyArgs dcp]
+    mkSymbol x
+      -- | "$cp" `F.isPrefixOfSym` F.symbol x = F.mappendSym "$" (F.dropSym 2 $ GM.simplesymbol x)
+      | F.notracepp ("isDictonaryId:" ++ GM.showPpr x) $ Ghc.isDictonaryId x = F.mappendSym "$" (F.dropSym 2 $ GM.simplesymbol x)
+      | otherwise = F.dropSym 2 $ GM.simplesymbol x
+        -- res = dcpTyRes dcp
+    clsTvs = dcpFreeTyVars dcp
+        -- copy/pasted from Bare/Class.hs
+    subst [] t = t
+    subst ((a, ta):su) t = subsTyVar_meet' (a, ta) (subst su t)
+
+substAuxMethod :: F.Symbol -> M.HashMap F.Symbol F.Symbol -> F.Expr -> F.Expr
+substAuxMethod dfun methods e = F.notracepp "substAuxMethod" $ go e
+  where go :: F.Expr -> F.Expr
+        go (F.EApp e0 e1)
+          | F.EVar x <- F.notracepp "e0" e0
+          , (F.EVar dfun_mb, args)  <- F.splitEApp e1
+          , dfun_mb == dfun
+          , Just method <- M.lookup x methods
+              -- Before: Functor.fmap ($p1Applicative $dFunctor)
+              -- After: Funcctor.fmap ($p1Applicative##GHC.Base.Applicative)
+           = F.eApps (F.EVar method) args
+          | otherwise
+          = F.EApp (go e0) (go e1)
+        go (F.ENeg e) = F.ENeg (go e)
+        go (F.EBin bop e0 e1) = F.EBin bop (go e0) (go e1)
+        go (F.EIte e0 e1 e2) = F.EIte (go e0) (go e1) (go e2)
+        go (F.ECst e0 s) = F.ECst (go e0) s
+        go (F.ELam (x, t) body) = F.ELam (x, t) (go body)
+        go (F.PAnd es) = F.PAnd (go <$> es)
+        go (F.POr es) = F.POr (go <$> es)
+        go (F.PNot e) = F.PNot (go e)
+        go (F.PImp e0 e1) = F.PImp (go e0) (go e1)
+        go (F.PIff e0 e1) = F.PIff (go e0) (go e1)
+        go (F.PAtom brel e0 e1) = F.PAtom brel (go e0) (go e1)
+        go e = F.notracepp "LEAF" e
diff --git a/src/Language/Haskell/Liquid/Constraint/Fresh.hs b/src/Language/Haskell/Liquid/Constraint/Fresh.hs
index e736e653e8..6594cf51f4 100644
--- a/src/Language/Haskell/Liquid/Constraint/Fresh.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Fresh.hs
@@ -70,15 +70,15 @@ refreshArgsTop (x, t)
 --   invariant is /obviously/ enforced.
 --   Constraint generation should ONLY use @freshTy_type@ and @freshTy_expr@
 
-freshTy_type        :: KVKind -> CoreExpr -> Type -> CG SpecType
-freshTy_type k e τ  =  F.notracepp ("freshTy_type: " ++ F.showpp k ++ GM.showPpr e) 
-                   <$> freshTy_reftype k (ofType τ)
+freshTy_type        :: Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
+freshTy_type allowTC k e τ  =  F.notracepp ("freshTy_type: " ++ F.showpp k ++ GM.showPpr e) 
+                   <$> freshTy_reftype allowTC k (ofType τ)
 
-freshTy_expr        :: KVKind -> CoreExpr -> Type -> CG SpecType
-freshTy_expr k e _  = freshTy_reftype k $ exprRefType e
+freshTy_expr        :: Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
+freshTy_expr allowTC k e _  = freshTy_reftype allowTC k $ exprRefType e
 
-freshTy_reftype     :: KVKind -> SpecType -> CG SpecType
-freshTy_reftype k _t = (fixTy t >>= refresh) =>> addKVars k
+freshTy_reftype     :: Bool -> KVKind -> SpecType -> CG SpecType
+freshTy_reftype allowTC k _t = (fixTy t >>= refresh allowTC) =>> addKVars k
   where
     t                = {- F.tracepp ("freshTy_reftype:" ++ show k) -} _t
 
@@ -106,12 +106,12 @@ addKuts _x t = modify $ \s -> s { kuts = mappend (F.KS ks) (kuts s)   }
        | otherwise  = {- F.tracepp ("addKuts: " ++ showpp _x) -} ks'
 
 specTypeKVars :: SpecType -> [F.KVar]
-specTypeKVars = foldReft False (\ _ r ks -> (kvars $ ur_reft r) ++ ks) []
+specTypeKVars = foldReft (const False) False (\ _ r ks -> (kvars $ ur_reft r) ++ ks) []
 
 --------------------------------------------------------------------------------
-trueTy  :: Type -> CG SpecType
+trueTy  :: Bool -> Type -> CG SpecType
 --------------------------------------------------------------------------------
-trueTy = ofType' >=> true
+trueTy allowTC = ofType' >=> true allowTC
 
 ofType' :: Type -> CG SpecType
 ofType' = fixTy . ofType
diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs
index d92ec678e2..8d309d1c0d 100644
--- a/src/Language/Haskell/Liquid/Constraint/Generate.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs
@@ -94,14 +94,14 @@ consAct cfg info = do
   let gSrc = giSrc info
   when (gradual cfg) (mapM_ (addW . WfC γ . val . snd) (gsTySigs sSpc ++ gsAsmSigs sSpc))
   foldM_ (consCBTop cfg info) γ (giCbs gSrc)
-  mapM (consClass γ) (gsMethods $ gsSig $ giSpec info) 
-  hcs <- hsCs  <$> get
-  hws <- hsWfs <$> get
-  fcs <- concat <$> mapM splitC hcs
+  mapM_ (consClass γ) (gsMethods $ gsSig $ giSpec info) 
+  hcs <- gets hsCs
+  hws <- gets hsWfs
+  fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs
   fws <- concat <$> mapM splitW hws
   modify $ \st -> st { fEnv     = feEnv (fenv γ)
                      , cgLits   = litEnv   γ
-                     , cgConsts = (cgConsts st) `mappend` (constEnv γ)
+                     , cgConsts = cgConsts st `mappend` constEnv γ
                      , fixCs    = fcs
                      , fixWfs   = fws }
 
@@ -264,7 +264,7 @@ consCBTop cfg info γ cb
   = foldM addB γ xs
     where
        xs   = bindersOf cb
-       tt   = trueTy . varType
+       tt   = trueTy (typeclass cfg) . varType
        addB γ x = tt x >>= (\t -> γ += ("derived", F.symbol x, t))
 
 consCBTop _ _ γ cb
@@ -292,10 +292,11 @@ doTermCheck :: Config -> Bind Var -> CG Bool
 doTermCheck cfg bind = do 
   lazyVs    <- specLazy   <$> get 
   termVs    <- specTmVars <$> get
-  let skip   = any (\x -> S.member x lazyVs || GM.isInternal x) xs
+  let skip   = any (\x -> S.member x lazyVs || nocheck x) xs
   let chk    = not (structuralTerm cfg) || any (\x -> S.member x termVs) xs
   return     $ chk && not skip
-  where 
+  where
+    nocheck  = if typeclass cfg then GM.isEmbeddedDictVar else GM.isInternal
     xs       = bindersOf bind
 
 -- nonStructTerm && not skip
@@ -313,11 +314,13 @@ consCBSizedTys γ xes
        let rts   = (recType autoenv <$>) <$> xeets
        let xts   = zip xs ts
        γ'       <- foldM extender γ xts
-       let γs    = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . GM.isPredVar) <$> vs)
+       let γs    = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . noMakeRec) <$> vs)
        let xets' = zip3 xs es ts
        mapM_ (uncurry $ consBind True) (zip γs xets')
        return γ'
   where
+       noMakeRec      = if allowTC then GM.isEmbeddedDictVar else GM.isPredVar
+       allowTC        = typeclass (getConfig γ)
        (xs, es)       = unzip xes
        dxs            = F.pprint <$> xs
        collectArgs    = GM.collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate
@@ -419,7 +422,7 @@ consCB _ _ γ (Rec xes)
 -- | NV: Dictionaries are not checked, because
 -- | class methods' preconditions are not satisfied
 consCB _ _ γ (NonRec x _) | isDictionary x
-  = do t  <- trueTy (varType x)
+  = do t  <- trueTy (typeclass (getConfig γ)) (varType x)
        extender γ (x, Assumed t)
     where
        isDictionary = isJust . dlookup (denv γ)
@@ -428,11 +431,11 @@ consCB _ _ γ (NonRec x _) | isDictionary x
 consCB _ _ γ (NonRec x def)
   | Just (w, τ) <- grepDictionary def
   , Just d      <- dlookup (denv γ) w
-  = do t        <- trueTy τ
+  = do t        <- trueTy (typeclass (getConfig γ)) τ
        addW      $ WfC γ t
        let xts   = dmap (fmap (f t)) d
        let  γ'   = γ { denv = dinsert (denv γ) x xts }
-       t        <- trueTy (varType x)
+       t        <- trueTy (typeclass (getConfig γ)) (varType x)
        extender γ' (x, Assumed t)
    where
     f t' (RAllT α te _) = subsTyVar_meet' (ty_var_value α, t') te
@@ -465,7 +468,7 @@ consBind isRec γ (x, e, Asserted spect)
        let spect' = fromRTypeRep (tyr { ty_ebinds = [], ty_eargs = [], ty_erefts = [] })
        γπ <- foldM (+=) γπ $ (\(y,t)->("implicitError",y,t)) <$> zip (ty_ebinds tyr) (ty_eargs tyr)
 
-       cconsE γπ e (weakenResult x spect')
+       cconsE γπ e (weakenResult (typeclass (getConfig γ)) x spect')
        when (F.symbol x `elemHEnv` holes γ) $
          -- have to add the wf constraint here for HOLEs so we have the proper env
          addW $ WfC γπ $ fmap killSubst spect
@@ -489,7 +492,7 @@ consBind isRec γ (x, e, Internal spect)
 consBind isRec γ (x, e, Assumed spect)
   = do let γ' = γ `setBind` x
        γπ    <- foldM addPToEnv γ' πs
-       cconsE γπ e =<< true spect
+       cconsE γπ e =<< true (typeclass (getConfig γ)) spect
        addIdA x (defAnn isRec spect)
        return $ Asserted spect
     where πs   = ty_preds $ toRTypeRep spect
@@ -583,7 +586,7 @@ varTemplate' γ (x, eo)
       (_, Just t, _, _) -> Asserted <$> refreshArgsTop (x, t)
       (_, _, _, Just t) -> Internal <$> refreshArgsTop (x, t)
       (_, _, Just t, _) -> Assumed  <$> refreshArgsTop (x, t)
-      (Just e, _, _, _) -> do t  <- freshTy_expr (RecBindE x) e (exprType e)
+      (Just e, _, _, _) -> do t  <- freshTy_expr (typeclass (getConfig γ)) (RecBindE x) e (exprType e)
                               addW (WfC γ t)
                               Asserted <$> refreshArgsTop (x, t)
       (_,      _, _, _) -> return Unknown
@@ -627,7 +630,7 @@ cconsE' γ e (RAllP p t)
   where
     t'         = replacePredsWithRefs su <$> t
     su         = (uPVar p, pVartoRConc p)
-    (css, t'') = splitConstraints t'
+    (css, t'') = splitConstraints (typeclass (getConfig γ)) t'
     γ'         = L.foldl' addConstraints γ css
 
 cconsE' γ (Let b e) t
@@ -691,7 +694,7 @@ addForAllConstraint γ _ _ (RAllT a t r)
   | F.isTauto r 
   = return ()
   | otherwise
-  = do t'       <- true t
+  = do t'       <- true (typeclass (getConfig γ)) t
        let truet = RAllT a $ unRAllP t'
        addC (SubC γ (truet mempty) $ truet r) "forall constraint true"
   where unRAllP (RAllT a t r) = RAllT a (unRAllP t) r  
@@ -703,8 +706,8 @@ addForAllConstraint γ _ _ _
   
 addFunctionConstraint :: CGEnv -> Var -> CoreExpr -> SpecType -> CG ()
 addFunctionConstraint γ x e (RFun y ty t r)
-  = do ty'      <- true ty
-       t'       <- true t
+  = do ty'      <- true (typeclass (getConfig γ)) ty
+       t'       <- true (typeclass (getConfig γ)) t
        let truet = RFun y ty' t'
        case (lamExpr γ e, higherOrderFlag γ) of
           (Just e', True) -> do tce    <- tyConEmbed <$> get
@@ -716,12 +719,13 @@ addFunctionConstraint γ _ _ _
   = impossible (Just $ getLocation γ) "addFunctionConstraint: called on non function argument"
 
 splitConstraints :: TyConable c
-                 => RType c tv r -> ([[(F.Symbol, RType c tv r)]], RType c tv r)
-splitConstraints (RRTy cs _ OCons t)
-  = let (css, t') = splitConstraints t in (cs:css, t')
-splitConstraints (RFun x tx@(RApp c _ _ _) t r) | isClass c
-  = let (css, t') = splitConstraints t in (css, RFun x tx t' r)
-splitConstraints t
+                 => Bool -> RType c tv r -> ([[(F.Symbol, RType c tv r)]], RType c tv r)
+splitConstraints allowTC (RRTy cs _ OCons t)
+  = let (css, t') = splitConstraints allowTC t in (cs:css, t')
+splitConstraints allowTC (RFun x tx@(RApp c _ _ _) t r) | isErasable c
+  = let (css, t') = splitConstraints allowTC  t in (css, RFun x tx t' r)
+  where isErasable = if allowTC then isEmbeddedDict else isClass
+splitConstraints _ t
   = ([], t)
 
 -------------------------------------------------------------------
@@ -773,7 +777,7 @@ cconsLazyLet :: CGEnv
              -> SpecType
              -> CG ()
 cconsLazyLet γ (Let (NonRec x ex) e) t
-  = do tx <- trueTy (varType x)
+  = do tx <- trueTy (typeclass (getConfig γ)) (varType x)
        γ' <- (γ, "Let NonRec") +++= (x', ex, tx)
        cconsE γ' e t
     where
@@ -810,8 +814,8 @@ consE _ (Lit c)
 consE γ e'@(App e a@(Type τ))
   = do RAllT α te _ <- checkAll ("Non-all TyApp with expr", e) γ <$> consE γ e
        t            <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te 
-                         then freshTy_type TypeInstE e τ 
-                         else trueTy τ
+                         then freshTy_type (typeclass (getConfig γ)) TypeInstE e τ 
+                         else trueTy (typeclass (getConfig γ)) τ
        addW          $ WfC γ t
        t'           <- refreshVV t
        tt0          <- instantiatePreds γ e' (subsTyVar_meet' (ty_var_value α, t') te)
@@ -847,7 +851,7 @@ consE γ e'@(App e a)
        tout <- makeSingleton γ'' (simplify e') <$> (addPost γ'' $ maybe (checkUnbound γ'' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a))
        if hasGhost
           then do
-           tk   <- freshTy_type ImplictE e' $ exprType e'
+           tk   <- freshTy_type (typeclass (getConfig γ)) ImplictE e' $ exprType e'
            addW $ WfC γ tk
            addC (SubC γ'' tout tk) ""
            return tk
@@ -859,7 +863,7 @@ consE γ (Lam α e) | isTyVar α
        return $ RAllT (makeRTVar $ rTyVar α) t' mempty
 
 consE γ  e@(Lam x e1)
-  = do tx      <- freshTy_type LamE (Var x) τx
+  = do tx      <- freshTy_type (typeclass (getConfig γ)) LamE (Var x) τx
        γ'      <- γ += ("consE", F.symbol x, tx)
        t1      <- consE γ' e1
        addIdA x $ AnnDef tx
@@ -892,8 +896,8 @@ consE γ (Cast e co)
 consE γ e@(Cast e' c)
   = castTy γ (exprType e) e' c
 
-consE _ e@(Coercion _)
-   = trueTy $ exprType e
+consE γ e@(Coercion _)
+   = trueTy (typeclass (getConfig γ)) $ exprType e
 
 consE _ e@(Type t)
   = panic Nothing $ "consE cannot handle type " ++ GM.showPpr (e, t)
@@ -970,8 +974,8 @@ consPattern γ (Rs.PatBind e1 x e2 _ _ _ _ _) _ = do
  -}
 consPattern γ (Rs.PatReturn e m _ _ _) t = do
   et    <- F.notracepp "Cons-Pattern-Ret" <$> consE γ e
-  mt    <- trueTy  m
-  tt    <- trueTy  t
+  mt    <- trueTy (typeclass (getConfig γ))  m
+  tt    <- trueTy (typeclass (getConfig γ))  t
   return (mkRAppTy mt et tt) -- /// {-    $ RAppTy mt et mempty -}
 
 {- [NOTE] special type rule for field projection, is
@@ -982,7 +986,7 @@ consPattern γ (Rs.PatReturn e m _ _ _) t = do
 
 consPattern γ (Rs.PatProject xe _ τ c ys i) _ = do
   let yi = ys !! i
-  t    <- (addW . WfC γ) <<= freshTy_type ProjectE (Var yi) τ
+  t    <- (addW . WfC γ) <<= freshTy_type (typeclass (getConfig γ)) ProjectE (Var yi) τ
   γ'   <- caseEnv γ xe [] (DataAlt c) ys (Just [i])
   ti   <- {- γ' ??= yi -} varRefType γ' yi
   addC (SubC γ' ti t) "consPattern:project"
@@ -1030,7 +1034,7 @@ castTy γ t e _
 
 
 castTy' γ τ (Var x)
-  = do t <- trueTy τ
+  = do t <- trueTy (typeclass (getConfig γ)) τ
        -- tx <- varRefType γ x -- NV HERE: the refinements of the var x do not get into the 
        --                      -- environment. Check 
        let ce = eCoerc (typeSort (emb γ) $ Ghc.expandTypeSynonyms $ varType x) 
@@ -1106,7 +1110,7 @@ isClassConCo co
 --------------------------------------------------------------------------------
 cconsFreshE :: KVKind -> CGEnv -> CoreExpr -> CG SpecType
 cconsFreshE kvkind γ e = do
-  t   <- freshTy_type kvkind e $ exprType e
+  t   <- freshTy_type (typeclass (getConfig γ)) kvkind e $ exprType e
   addW $ WfC γ t
   cconsE γ e t
   return t
@@ -1127,8 +1131,10 @@ dropExists γ (REx x tx t) =         (, t) <$> γ += ("dropExists", x, tx)
 dropExists γ t            = return (γ, t)
 
 dropConstraints :: CGEnv -> SpecType -> CG SpecType
-dropConstraints γ (RFun x tx@(RApp c _ _ _) t r) | isClass c
+dropConstraints γ (RFun x tx@(RApp c _ _ _) t r) | isErasable c
   = (flip (RFun x tx)) r <$> dropConstraints γ t
+  where
+    isErasable = if typeclass (getConfig γ) then isEmbeddedDict else isClass
 dropConstraints γ (RRTy cts _ OCons t)
   = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ xts
        addC (SubC  γ' t1 t2)  "dropConstraints"
@@ -1165,14 +1171,15 @@ caseEnv γ x _   (DataAlt c) ys pIs = do
   let xt           = shiftVV xt0 x'
   tdc             <- (γ ??= (dataConWorkId c) >>= refreshVV)
   let (rtd,yts',_) = unfoldR tdc xt ys
-  yts             <- projectTypes pIs yts'
-  let ys''         = F.symbol <$> filter (not . GM.isEvVar) ys
+  yts             <- projectTypes (typeclass (getConfig γ))  pIs yts'
+  let ys''         = F.symbol <$> filter (not . if allowTC then GM.isEmbeddedDictVar else GM.isEvVar) ys
   let r1           = dataConReft   c   ys''
   let r2           = dataConMsReft rtd ys''
   let xt           = (xt0 `F.meet` rtd) `strengthen` (uTop (r1 `F.meet` r2))
   let cbs          = safeZip "cconsCase" (x':ys') (xt0 : yts)
   cγ'             <- addBinders γ   x' cbs
   addBinders cγ' x' [(x', xt)]
+  where allowTC    = typeclass (getConfig γ)
   
 caseEnv γ x acs a _ _ = do 
   let x'  = F.symbol x
@@ -1185,13 +1192,13 @@ caseEnv γ x acs a _ _ = do
 --   at given indices; it is used to simplify the environment used
 --   when projecting out fields of single-ctor datatypes.
 --------------------------------------------------------------------------------
-projectTypes :: Maybe [Int] -> [SpecType] -> CG [SpecType]
-projectTypes Nothing   ts = return ts
-projectTypes (Just is) ts = mapM (projT is) (zip [0..] ts)
+projectTypes :: Bool -> Maybe [Int] -> [SpecType] -> CG [SpecType]
+projectTypes allowTC Nothing   ts = return ts
+projectTypes allowTC (Just is) ts = mapM (projT is) (zip [0..] ts)
   where
     projT is (j, t)
       | j `elem` is       = return t
-      | otherwise         = true t
+      | otherwise         = true allowTC t
 
 altReft :: CGEnv -> [AltCon] -> AltCon -> F.Reft
 altReft _ _ (LitAlt l)   = literalFReft l
@@ -1259,7 +1266,7 @@ varAnn γ x t
 -----------------------------------------------------------------------
 freshPredRef :: CGEnv -> CoreExpr -> PVar RSort -> CG SpecProp
 freshPredRef γ e (PV _ (PVProp τ) _ as)
-  = do t    <- freshTy_type PredInstE e (toType τ)
+  = do t    <- freshTy_type (typeclass (getConfig γ))  PredInstE e (toType τ)
        args <- mapM (\_ -> fresh) as
        let targs = [(x, s) | (x, (s, y, z)) <- zip args as, (F.EVar y) == z ]
        γ' <- foldM (+=) γ [("freshPredRef", x, ofRSort τ) | (x, τ) <- targs]
@@ -1302,10 +1309,11 @@ lamExpr γ (Lit c)     = snd  $ literalConst (emb γ) c
 lamExpr γ (Tick _ e)  = lamExpr γ e
 lamExpr γ (App e (Type _)) = lamExpr γ e
 lamExpr γ (App e1 e2) = case (lamExpr γ e1, lamExpr γ e2) of
-                              (Just p1, Just p2) | not (GM.isPredExpr e2) -- (isClassPred $ exprType e2)
+                              (Just p1, Just p2) | not ((if allowTC then GM.isEmbeddedDictExpr else GM.isPredExpr) e2) -- (isClassPred $ exprType e2)
                                                  -> Just $ F.EApp p1 p2
                               (Just p1, Just _ ) -> Just p1
                               _  -> Nothing
+  where allowTC = typeclass (getConfig γ)
 lamExpr γ (Let (NonRec x ex) e) = case (lamExpr γ ex, lamExpr γ e) of
                                        (Just px, Just p) -> Just (p `F.subst1` (F.symbol x, px))
                                        _  -> Nothing
@@ -1354,7 +1362,7 @@ makeSingleton γ e t
   | higherOrderFlag γ, App f x <- simplify e
   = case (funExpr γ f, argForAllExpr x) of
       (Just f', Just x')
-                 | not (GM.isPredExpr x) -- (isClassPred $ exprType x)
+                 | not (if (typeclass (getConfig γ)) then GM.isEmbeddedDictExpr x else GM.isPredExpr x) -- (isClassPred $ exprType x)
                  -> strengthenMeet t (uTop $ F.exprReft (F.EApp f' x'))
       (Just f', Just _)
                  -> strengthenMeet t (uTop $ F.exprReft f')
@@ -1382,7 +1390,7 @@ funExpr _ (Var v)
 
 funExpr γ (App e1 e2)
   = case (funExpr γ e1, argExpr γ e2) of
-      (Just e1', Just e2') | not (GM.isPredExpr e2) -- (isClassPred $ exprType e2)
+      (Just e1', Just e2') | not (if typeclass (getConfig γ) then GM.isEmbeddedDictExpr e2 else GM.isPredExpr e2) -- (isClassPred $ exprType e2)
                            -> Just (F.EApp e1' e2')
       (Just e1', Just _)
                            -> Just e1'
diff --git a/src/Language/Haskell/Liquid/Constraint/Init.hs b/src/Language/Haskell/Liquid/Constraint/Init.hs
index 1c80310530..e59aec0046 100644
--- a/src/Language/Haskell/Liquid/Constraint/Init.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Init.hs
@@ -62,10 +62,10 @@ initEnv info
        let fVars = giImpVars (giSrc info)
        let dcs   = filter isConLikeId (snd <$> gsFreeSyms (gsName sp))
        let dcs'  = filter isConLikeId fVars
-       defaults <- forM fVars $ \x -> liftM (x,) (trueTy $ varType x)
-       dcsty    <- forM dcs   makeDataConTypes
-       dcsty'   <- forM dcs'  makeDataConTypes
-       (hs,f0)  <- refreshHoles $ grty info                           -- asserted refinements     (for defined vars)
+       defaults <- forM fVars $ \x -> liftM (x,) (trueTy allowTC $ varType x)
+       dcsty    <- forM dcs   (makeDataConTypes allowTC)
+       dcsty'   <- forM dcs'  (makeDataConTypes allowTC)
+       (hs,f0)  <- refreshHoles allowTC $ grty info                           -- asserted refinements     (for defined vars)
        f0''     <- refreshArgs' =<< grtyTop info                      -- default TOP reftype      (for exported vars without spec)
        let f0'   = if notruetypes $ getConfig sp then [] else f0''
        f1       <- refreshArgs'   defaults                            -- default TOP reftype      (for all vars)
@@ -87,11 +87,12 @@ initEnv info
        let lt2s  = [ (F.symbol x, rTypeSort tce t) | (x, t) <- f1' ]
        let tcb   = mapSnd (rTypeSort tce) <$> concat bs
        let cbs   = giCbs . giSrc $ info
-       rTrue   <- mapM (mapSndM true) f6 
+       rTrue   <- mapM (mapSndM (true allowTC)) f6 
        let γ0    = measEnv sp (head bs) cbs tcb lt1s lt2s (f6 ++ bs!!3) (bs!!5) hs info
        γ  <- globalize <$> foldM (+=) γ0 ( [("initEnv", x, y) | (x, y) <- concat $ (rTrue:tail bs)])
        return γ {invs = is (invs1 ++ invs2)}
   where
+    allowTC        = typeclass (getConfig info)
     sp           = giSpec info
     ialias       = mkRTyConIAl (gsIaliases (gsData sp))
     vals f       = map (mapSnd val) . f
@@ -109,8 +110,8 @@ addPolyInfo t = mkUnivs (go <$> as) ps t'
                then (setRtvPol a False,r)  
                else (a,r) 
 
-makeDataConTypes :: Var -> CG (Var, SpecType)
-makeDataConTypes x = (x,) <$> (trueTy $ varType x)
+makeDataConTypes :: Bool -> Var -> CG (Var, SpecType)
+makeDataConTypes allowTC x = (x,) <$> (trueTy allowTC $ varType x)
 
 makeAutoDecrDataCons :: [(Id, SpecType)] -> S.HashSet TyCon -> [Id] -> ([LocSpecType], [(Id, SpecType)])
 makeAutoDecrDataCons dcts specenv dcs
@@ -234,7 +235,7 @@ assmGrty f info = [ (x, val t) | (x, t) <- sigs, x `S.member` xs ]
 
 
 recSelectorsTy :: TargetInfo -> CG [(Var, SpecType)]
-recSelectorsTy info = forM topVs $ \v -> (v,) <$> trueTy (varType v)
+recSelectorsTy info = forM topVs $ \v -> (v,) <$> trueTy (typeclass (getConfig info)) (varType v)
   where
     topVs        = filter isTop $ giDefVars (giSrc info)
     isTop v      = isExportedVar (giSrc info) v && not (v `S.member` sigVs) &&  isRecordSelector v
@@ -244,7 +245,7 @@ recSelectorsTy info = forM topVs $ \v -> (v,) <$> trueTy (varType v)
 
 
 grtyTop :: TargetInfo -> CG [(Var, SpecType)]
-grtyTop info     = forM topVs $ \v -> (v,) <$> trueTy (varType v)
+grtyTop info     = forM topVs $ \v -> (v,) <$> trueTy (typeclass (getConfig info)) (varType v)
   where
     topVs        = filter isTop $ giDefVars (giSrc info)
     isTop v      = isExportedVar (giSrc info) v && not (v `S.member` sigVs) && not (isRecordSelector v)
diff --git a/src/Language/Haskell/Liquid/Constraint/Split.hs b/src/Language/Haskell/Liquid/Constraint/Split.hs
index 6f65a33361..55d64c68f8 100644
--- a/src/Language/Haskell/Liquid/Constraint/Split.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Split.hs
@@ -151,98 +151,98 @@ updateEnv γ a
   = return γ
 
 ------------------------------------------------------------
-splitC :: SubC -> CG [FixSubC]
+splitC :: Bool -> SubC -> CG [FixSubC]
 ------------------------------------------------------------
 
-splitC (SubC γ (REx x tx t1) (REx x2 _ t2)) | x == x2
+splitC allowTC (SubC γ (REx x tx t1) (REx x2 _ t2)) | x == x2
   = do γ' <- γ += ("addExBind 0", x, forallExprRefType γ tx)
-       splitC (SubC γ' t1 t2)
+       splitC allowTC (SubC γ' t1 t2)
 
-splitC (SubC γ t1 (REx x tx t2))
+splitC allowTC (SubC γ t1 (REx x tx t2))
   = do y <- fresh
        γ' <- γ += ("addExBind 1", y, forallExprRefType γ tx)
-       splitC (SubC γ' t1 (F.subst1 t2 (x, F.EVar y)))
+       splitC allowTC (SubC γ' t1 (F.subst1 t2 (x, F.EVar y)))
 
 -- existential at the left hand side is treated like forall
-splitC (SubC γ (REx x tx t1) t2)
-  = do -- let tx' = traceShow ("splitC: " ++ showpp z) tx
+splitC allowTC (SubC γ (REx x tx t1) t2)
+  = do -- let tx' = traceShow ("splitC allowTC: " ++ showpp z) tx
        y <- fresh
        γ' <- γ += ("addExBind 2", y, forallExprRefType γ tx)
-       splitC (SubC γ' (F.subst1 t1 (x, F.EVar y)) t2)
+       splitC allowTC (SubC γ' (F.subst1 t1 (x, F.EVar y)) t2)
 
-splitC (SubC γ (RAllE x tx t1) (RAllE x2 _ t2)) | x == x2
+splitC allowTC (SubC γ (RAllE x tx t1) (RAllE x2 _ t2)) | x == x2
   = do γ' <- γ += ("addAllBind 3", x, forallExprRefType γ tx)
-       splitC (SubC γ' t1 t2)
+       splitC allowTC (SubC γ' t1 t2)
 
-splitC (SubC γ (RAllE x tx t1) t2)
+splitC allowTC (SubC γ (RAllE x tx t1) t2)
   = do y  <- fresh
        γ' <- γ += ("addAABind 1", y, forallExprRefType γ tx)
-       splitC (SubC γ' (t1 `F.subst1` (x, F.EVar y)) t2)
+       splitC allowTC (SubC γ' (t1 `F.subst1` (x, F.EVar y)) t2)
 
-splitC (SubC γ t1 (RAllE x tx t2))
+splitC allowTC (SubC γ t1 (RAllE x tx t2))
   = do y  <- fresh
        γ' <- γ += ("addAllBind 2", y, forallExprRefType γ tx)
-       splitC (SubC γ' t1 (F.subst1 t2 (x, F.EVar y)))
+       splitC allowTC (SubC γ' t1 (F.subst1 t2 (x, F.EVar y)))
 
-splitC (SubC γ (RRTy env _ OCons t1) t2)
+splitC allowTC (SubC γ (RRTy env _ OCons t1) t2)
   = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ xts
-       c1 <- splitC (SubC γ' t1' t2')
-       c2 <- splitC (SubC γ  t1  t2 )
+       c1 <- splitC allowTC (SubC γ' t1' t2')
+       c2 <- splitC allowTC (SubC γ  t1  t2 )
        return $ c1 ++ c2
   where
     (xts, t1', t2') = envToSub env
 
-splitC (SubC γ (RRTy e r o t1) t2)
+splitC allowTC (SubC γ (RRTy e r o t1) t2)
   = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ e
-       c1 <- splitC (SubR γ' o  r)
-       c2 <- splitC (SubC γ t1 t2)
+       c1 <- splitC allowTC (SubR γ' o  r)
+       c2 <- splitC allowTC (SubC γ t1 t2)
        return $ c1 ++ c2
 
-splitC (SubC γ (RFun x1 t1 t1' r1) (RFun x2 t2 t2' r2))
-  =  do cs'      <- splitC  (SubC γ t2 t1)
-        γ'       <- γ+= ("splitC", x2, t2)
+splitC allowTC (SubC γ (RFun x1 t1 t1' r1) (RFun x2 t2 t2' r2))
+  =  do cs'      <- splitC allowTC  (SubC γ t2 t1)
+        γ'       <- γ+= ("splitC allowTC", x2, t2)
         cs       <- bsplitC γ (RFun x1 t1 t1' (r1 `F.subst1` (x1, F.EVar x2)))
                               (RFun x2 t2 t2'  r2)
         let t1x2' = t1' `F.subst1` (x1, F.EVar x2)
-        cs''     <- splitC  (SubC γ' t1x2' t2')
+        cs''     <- splitC allowTC  (SubC γ' t1x2' t2')
         return    $ cs ++ cs' ++ cs''
 
-splitC (SubC γ (RImpF x1 t1 t1' r1) (RImpF x2 t2 t2' r2))
-  =  do cs'      <- splitC  (SubC γ t2 t1)
-        γ'       <- γ+= ("splitC", x2, t2)
+splitC allowTC (SubC γ (RImpF x1 t1 t1' r1) (RImpF x2 t2 t2' r2))
+  =  do cs'      <- splitC allowTC  (SubC γ t2 t1)
+        γ'       <- γ+= ("splitC allowTC", x2, t2)
         cs       <- bsplitC γ (RImpF x1 t1 t1' (r1 `F.subst1` (x1, F.EVar x2)))
                               (RImpF x2 t2 t2'  r2)
         let t1x2' = t1' `F.subst1` (x1, F.EVar x2)
-        cs''     <- splitC  (SubC γ' t1x2' t2')
+        cs''     <- splitC allowTC  (SubC γ' t1x2' t2')
         return    $ cs ++ cs' ++ cs''
 
 
-splitC (SubC γ t1@(RAppTy r1 r1' _) t2@(RAppTy r2 r2' _))
+splitC allowTC (SubC γ t1@(RAppTy r1 r1' _) t2@(RAppTy r2 r2' _))
   =  do cs    <- bsplitC γ t1 t2
-        cs'   <- splitC  (SubC γ r1 r2)
-        cs''  <- splitC  (SubC γ r1' r2')
-        cs''' <- splitC  (SubC γ r2' r1')
+        cs'   <- splitC allowTC  (SubC γ r1 r2)
+        cs''  <- splitC allowTC  (SubC γ r1' r2')
+        cs''' <- splitC allowTC  (SubC γ r2' r1')
         return $ cs ++ cs' ++ cs'' ++ cs'''
 
-splitC (SubC γ t1 (RAllP p t))
-  = splitC $ SubC γ t1 t'
+splitC allowTC (SubC γ t1 (RAllP p t))
+  = splitC allowTC $ SubC γ t1 t'
   where
     t' = fmap (replacePredsWithRefs su) t
     su = (uPVar p, pVartoRConc p)
 
-splitC (SubC γ t1@(RAllP _ _) t2)
+splitC _ (SubC γ t1@(RAllP _ _) t2)
   = panic (Just $ getLocation γ) $ "Predicate in lhs of constraint:" ++ showpp t1 ++ "\n<:\n" ++ showpp t2
 
-splitC (SubC γ t1'@(RAllT α1 t1 _) t2'@(RAllT α2 t2 _))
+splitC allowTC (SubC γ t1'@(RAllT α1 t1 _) t2'@(RAllT α2 t2 _))
   |  α1 ==  α2
   = do γ'  <- updateEnv γ α2
        cs  <- bsplitC γ t1' t2'
-       cs' <- splitC $ SubC γ' t1 (F.subst su t2)
+       cs' <- splitC allowTC $ SubC γ' t1 (F.subst su t2)
        return (cs ++ cs')
   | otherwise
   = do γ'  <- updateEnv γ α2
        cs  <- bsplitC γ t1' t2'
-       cs' <- splitC $ SubC γ' t1 (F.subst su t2'')
+       cs' <- splitC allowTC $ SubC γ' t1 (F.subst su t2'')
        return (cs ++ cs')
   where
     t2'' = subsTyVar_meet' (ty_var_value α2, RVar (ty_var_value α1) mempty) t2
@@ -250,10 +250,10 @@ splitC (SubC γ t1'@(RAllT α1 t1 _) t2'@(RAllT α2 t2 _))
           (Just (x1, _), Just (x2, _)) -> F.mkSubst [(x1, F.EVar x2)]
           _                            -> F.mkSubst []
 
-splitC (SubC _ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isClass c1 && c1 == c2
+splitC allowTC (SubC _ (RApp c1 _ _ _) (RApp c2 _ _ _)) | (if allowTC then isEmbeddedDict else isClass) c1 && c1 == c2
   = return []
 
-splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _))
+splitC _ (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _))
   = do (t1',t2') <- unifyVV t1 t2
        cs    <- bsplitC γ t1' t2'
        γ'    <- if (bscope (getConfig γ)) then γ `extendEnvWithVV` t1' else return γ
@@ -265,14 +265,14 @@ splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _))
        csvar' <- rsplitsCWithVariance isapplied γ' r1s r2s $ variancePsArgs tyInfo
        return $ cs ++ csvar ++ csvar'
 
-splitC (SubC γ t1@(RVar a1 _) t2@(RVar a2 _))
+splitC _ (SubC γ t1@(RVar a1 _) t2@(RVar a2 _))
   | a1 == a2
   = bsplitC γ t1 t2
 
-splitC (SubC γ t1 t2)
+splitC _ (SubC γ t1 t2)
   = panic (Just $ getLocation γ) $ "(Another Broken Test!!!) splitc unexpected:\n" ++ traceTy t1 ++ "\n  <:\n" ++ traceTy t2
 
-splitC (SubR γ o r)
+splitC _ (SubR γ o r)
   = do ts     <- getTemplates
        let r1' = pruneUnsortedReft γ'' ts r1
        return $ F.subC γ' r1' r2 Nothing tag ci
@@ -316,7 +316,7 @@ splitsCWithVariance :: CGEnv
                     -> [Variance]
                     -> CG [FixSubC]
 splitsCWithVariance γ t1s t2s variants
-  = concatMapM (\(t1, t2, v) -> splitfWithVariance (\s1 s2 -> (splitC (SubC γ s1 s2))) t1 t2 v) (zip3 t1s t2s variants)
+  = concatMapM (\(t1, t2, v) -> splitfWithVariance (\s1 s2 -> (splitC (typeclass (getConfig γ)) (SubC γ s1 s2))) t1 t2 v) (zip3 t1s t2s variants)
 
 rsplitsCWithVariance :: Bool
                      -> CGEnv
@@ -390,7 +390,7 @@ rsplitC _ (RProp _ (RHole _)) _
 
 rsplitC γ (RProp s1 r1) (RProp s2 r2)
   = do γ'  <-  foldM (+=) γ [("rsplitC1", x, ofRSort s) | (x, s) <- s2]
-       splitC (SubC γ' (F.subst su r1) r2)
+       splitC (typeclass (getConfig γ)) (SubC γ' (F.subst su r1) r2)
   where su = F.mkSubst [(x, F.EVar y) | ((x,_), (y,_)) <- zip s1 s2]
 
 
diff --git a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs
index 10cb730ad1..4e5eb4a68a 100644
--- a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs
+++ b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs
@@ -7,7 +7,6 @@ module Language.Haskell.Liquid.Constraint.ToFixpoint
   ) where
 
 import           Prelude hiding (error)
-import qualified Language.Haskell.Liquid.GHC.API as Ghc
 import qualified Language.Fixpoint.Types.Config as FC
 import           System.Console.CmdArgs.Default (def)
 import qualified Language.Fixpoint.Types        as F
@@ -90,8 +89,8 @@ makeAxiomEnvironment info xts fcs
            (doExpand sp cfg <$> fcs)
            (makeRewrites info <$> fcs)
   where
-    eqs      = if (oldPLE cfg) 
-                then (makeEquations sp ++ map (uncurry $ specTypeEq emb) xts)
+    eqs      = if oldPLE cfg
+                then makeEquations (typeclass cfg) sp ++ map (uncurry $ specTypeEq emb) xts
                 else axioms  
     emb      = gsTcEmbeds (gsName sp)
     cfg      = getConfig  info
@@ -165,17 +164,6 @@ makeRewriteOne tce (_,t)
        
     tRep = toRTypeRep $ val t 
 
-_isClassOrDict :: Id -> Bool
-_isClassOrDict x = F.tracepp ("isClassOrDict: " ++ F.showpp x) 
-                    $ (hasClassArg x || GM.isDictionary x || Mb.isJust (Ghc.isClassOpId_maybe x))
-
-hasClassArg :: Id -> Bool
-hasClassArg x = F.tracepp msg $ (GM.isDataConId x && any Ghc.isClassPred (t:ts))
-  where 
-    msg       = "hasClassArg: " ++ showpp (x, t:ts)
-    (ts, t)   = Ghc.splitFunTys . snd . Ghc.splitForAllTys . Ghc.varType $ x
-
-
 doExpand :: TargetSpec -> Config -> F.SubC Cinfo -> Bool
 doExpand sp cfg sub = Config.allowGlobalPLE cfg
                    || (Config.allowLocalPLE cfg && maybe False (isPLEVar sp) (subVar sub))
@@ -227,8 +215,8 @@ makeSimplify (x, t)
     fromEVar (F.EVar x) = x
     fromEVar _ = impossible Nothing "makeSimplify.fromEVar"
 
-makeEquations :: TargetSpec -> [F.Equation]
-makeEquations sp = [ F.mkEquation f xts (equationBody (F.EVar f) xArgs e mbT) t
+makeEquations :: Bool -> TargetSpec -> [F.Equation]
+makeEquations allowTC sp = [ F.mkEquation f xts (equationBody allowTC (F.EVar f) xArgs e mbT) t
                       | F.Equ f xts e t _ <- axioms 
                       , let xArgs          = F.EVar . fst <$> xts
                       , let mbT            = if null xArgs then Nothing else M.lookup f sigs
@@ -238,18 +226,18 @@ makeEquations sp = [ F.mkEquation f xts (equationBody (F.EVar f) xArgs e mbT) t
     refl         = gsRefl sp
     sigs         = M.fromList [ (GM.simplesymbol v, t) | (v, t) <- gsTySigs (gsSig sp) ]
 
-equationBody :: F.Expr -> [F.Expr] -> F.Expr -> Maybe LocSpecType -> F.Expr
-equationBody f xArgs e mbT
+equationBody :: Bool -> F.Expr -> [F.Expr] -> F.Expr -> Maybe LocSpecType -> F.Expr
+equationBody allowTC f xArgs e mbT
   | Just t <- mbT = F.pAnd [eBody, rBody t]
   | otherwise     = eBody
   where
     eBody         = F.PAtom F.Eq (F.eApps f xArgs) e
-    rBody t       = specTypeToLogic xArgs (F.eApps f xArgs) (val t)
+    rBody t       = specTypeToLogic allowTC xArgs (F.eApps f xArgs) (val t)
 
 -- NV Move this to types?
 -- sound but imprecise approximation of a type in the logic
-specTypeToLogic :: [F.Expr] -> F.Expr -> SpecType -> F.Expr
-specTypeToLogic es e t
+specTypeToLogic :: Bool -> [F.Expr] -> F.Expr -> SpecType -> F.Expr
+specTypeToLogic allowTC es e t
   | ok        = F.subst su (F.PImp (F.pAnd args) res)
   | otherwise = F.PTrue
   where
@@ -270,7 +258,7 @@ specTypeToLogic es e t
 
 
     su           = F.mkSubst $ zip xs es
-    (cls, nocls) = L.partition (isClassType.snd) $ zip (ty_binds trep) (ty_args trep)
+    (cls, nocls) = L.partition ((if allowTC then isEmbeddedClass else isClassType).snd) $ zip (ty_binds trep) (ty_args trep)
                  :: ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)])
     (xs, ts)     = unzip nocls :: ([F.Symbol], [SpecType])
 
diff --git a/src/Language/Haskell/Liquid/GHC/API.hs b/src/Language/Haskell/Liquid/GHC/API.hs
index 9b1bed0892..8b6dfc536c 100644
--- a/src/Language/Haskell/Liquid/GHC/API.hs
+++ b/src/Language/Haskell/Liquid/GHC/API.hs
@@ -31,7 +31,7 @@ module Language.Haskell.Liquid.GHC.API (
   , isEvVarType
   , isEqPrimPred
   , dataConExTyVars
-
+  , gHC_REAL
   ) where 
 
 import GHC            as Ghc
@@ -45,7 +45,7 @@ import CoreSyn        as Ghc hiding (AnnExpr, AnnExpr' (..), AnnRec, AnnCase)
 import NameSet        as Ghc
 import InstEnv        as Ghc 
 import Literal        as Ghc
-import TcType         as Ghc (isClassPred)
+import TcType         as Ghc (isClassPred, tcSplitMethodTy, tcSplitAppTys)
 import Class          as Ghc
 import Unique         as Ghc
 import RdrName        as Ghc
@@ -98,7 +98,7 @@ import FastString     as Ghc
 import Predicate      as Ghc (isEqPred, getClassPredTys_maybe, isEvVarType, isEqPrimPred)
 import Data.Foldable  (asum)
 import Util           (lengthIs)
-import PrelNames      (eqPrimTyConKey, eqReprPrimTyConKey)
+import PrelNames      (eqPrimTyConKey, eqReprPrimTyConKey, gHC_REAL)
 #endif
 #endif
 
diff --git a/src/Language/Haskell/Liquid/GHC/Interface.hs b/src/Language/Haskell/Liquid/GHC/Interface.hs
index 10580d34ee..6c612e2d99 100644
--- a/src/Language/Haskell/Liquid/GHC/Interface.hs
+++ b/src/Language/Haskell/Liquid/GHC/Interface.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE NoMonomorphismRestriction  #-}
+{-# LANGUAGE LambdaCase                 #-}
 {-# LANGUAGE TypeSynonymInstances       #-}
 {-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE FlexibleInstances          #-}
@@ -438,7 +439,7 @@ processTargetModule cfg0 logicMap depGraph specEnv file typechecked bareSpec = d
   
   let targetSrc = view targetSrcIso ghcSrc
 
-  case makeTargetSpec cfg logicMap targetSrc (view bareSpecIso bareSpec) dependencies of
+  makeTargetSpec cfg logicMap targetSrc (view bareSpecIso bareSpec) dependencies >>= \case
     Left  validationErrors -> Bare.checkThrow (Left validationErrors)
     Right (targetSpec, liftedSpec) -> do
       -- The call below is temporary, we should really load & save directly 'LiftedSpec's.
diff --git a/src/Language/Haskell/Liquid/GHC/Misc.hs b/src/Language/Haskell/Liquid/GHC/Misc.hs
index 6364905a84..3b576a2af6 100644
--- a/src/Language/Haskell/Liquid/GHC/Misc.hs
+++ b/src/Language/Haskell/Liquid/GHC/Misc.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE CPP                       #-}
 {-# LANGUAGE OverloadedStrings         #-}
 {-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE FlexibleContexts          #-}
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE RankNTypes                #-}
@@ -19,7 +20,7 @@ module Language.Haskell.Liquid.GHC.Misc where
 import           Class                                      (classKey)
 import           Data.String
 import qualified Data.List as L
-import           PrelNames                                  (fractionalClassKeys)
+import           PrelNames                                  (fractionalClassKeys, itName, ordClassKey, numericClassKeys, eqClassKey)
 import           FamInstEnv
 import           Debug.Trace
 -- import qualified ConLike                                    as Ghc
@@ -48,16 +49,30 @@ import           Module                                     (moduleNameFS)
 import           Finder                                     (findImportedModule, cannotFindModule)
 import           Panic                                      (throwGhcException)
 import           TcRnDriver
+import           TcRnMonad                                  (failIfErrsM, newUnique, pushLevelAndCaptureConstraints, unsetWOptM)
+import           TcExpr                                     (tcInferSigma)
+import           TcOrigin                                   (lexprCtOrigin)
+import           Inst                                       (deeplyInstantiate)
+import           TcSimplify                                 (simplifyInfer, simplifyInteractive, InferMode(..))
+import           TcHsSyn                                    (zonkTopLExpr)
+import           TcEvidence                                 (TcEvBinds(EvBinds))
+import           DsMonad                                    (initDsTc)
+import           DsExpr                                     (dsLExpr)
+import           Predicate                                  (getClassPredTys, mkClassPred)
 -- import           TcRnTypes
 
 
 import           Type                                       (expandTypeSynonyms, liftedTypeKind)
 import           IdInfo
 import qualified TyCon                                      as TC
+import           GhcMonad                                   (withSession)
+import           RnExpr                                     (rnLExpr)
 import           Data.Char                                  (isLower, isSpace, isUpper)
 import           Data.Maybe                                 (isJust, fromMaybe, fromJust)
 import           Data.Hashable
 import qualified Data.HashSet                               as S
+import qualified Data.Map.Strict                            as OM
+import           Control.Monad.State                        (evalState, get, modify)
 
 import qualified Data.Text.Encoding.Error                   as TE
 import qualified Data.Text.Encoding                         as T
@@ -209,6 +224,9 @@ unTickExpr x                  = x
 isFractionalClass :: Class -> Bool
 isFractionalClass clas = classKey clas `elem` fractionalClassKeys
 
+isOrdClass :: Class -> Bool
+isOrdClass clas = classKey clas == ordClassKey
+
 --------------------------------------------------------------------------------
 -- | Pretty Printers -----------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -580,6 +598,9 @@ instance Hashable Var where
 instance Hashable TyCon where
   hashWithSalt = uniqueHash
 
+instance Hashable Class where
+  hashWithSalt = uniqueHash
+
 instance Hashable DataCon where
   hashWithSalt = uniqueHash
 
@@ -712,7 +733,8 @@ isWorker s = notracepp ("isWorkerSym: s = " ++ ss) $ "$W" `L.isInfixOf` ss
   where 
     ss     = symbolString (symbol s)
 
-
+isSCSel :: Symbolic a => a -> Bool
+isSCSel  = isPrefixOfSym "$p" . dropModuleNames . symbol
 
 stripParens :: T.Text -> T.Text
 stripParens t = fromMaybe t (strip t)
@@ -780,6 +802,32 @@ findVarDef x cbs = case xCbs of
     unRec nonRec    = [nonRec]
 
 
+findVarDefMethod :: Symbol -> [CoreBind] -> Maybe (Var, CoreExpr)
+findVarDefMethod x cbs =
+  case rcbs  of
+                     (NonRec v def   : _ ) -> Just (v, def)
+                     (Rec [(v, def)] : _ ) -> Just (v, def)
+                     _                     -> Nothing
+  where
+    rcbs | isMethod x = mCbs
+         | isDictionary (dropModuleNames x) = dCbs
+         | otherwise  = xCbs
+    xCbs            = [ cb | cb <- concatMap unRec cbs, x `elem` coreBindSymbols cb 
+                           ]
+    mCbs            = [ cb | cb <- concatMap unRec cbs, x `elem` methodSymbols cb]
+    dCbs            = [ cb | cb <- concatMap unRec cbs, x `elem` dictionarySymbols cb]
+    unRec (Rec xes) = [NonRec x es | (x,es) <- xes]
+    unRec nonRec    = [nonRec]
+
+dictionarySymbols :: CoreBind -> [Symbol]
+dictionarySymbols = filter isDictionary . map (dropModuleNames . symbol) . binders
+
+
+methodSymbols :: CoreBind -> [Symbol]
+methodSymbols = filter isMethod . map (dropModuleNames . symbol) . binders
+
+
+
 coreBindSymbols :: CoreBind -> [Symbol]
 coreBindSymbols = map (dropModuleNames . simplesymbol) . binders
 
@@ -792,6 +840,48 @@ binders (Rec xes)    = fst <$> xes
 
 expandVarType :: Var -> Type
 expandVarType = expandTypeSynonyms . varType
+
+--------------------------------------------------------------------------------
+-- | The following functions test if a `CoreExpr` or `CoreVar` can be
+--   embedded in logic. With type-class support, we can no longer erase
+--   such expressions arbitrarily.
+--------------------------------------------------------------------------------
+isEmbeddedDictExpr :: CoreExpr -> Bool
+isEmbeddedDictExpr = isEmbeddedDictType . CoreUtils.exprType
+
+isEmbeddedDictVar :: Var -> Bool
+isEmbeddedDictVar v = F.notracepp msg . isEmbeddedDictType . varType $ v
+  where
+    msg     =  "isGoodCaseBind v = " ++ show v
+
+isEmbeddedDictType :: Type -> Bool
+isEmbeddedDictType = anyF [isOrdPred, isNumericPred, isEqPred, isPrelEqPred]
+
+-- unlike isNumCls, isFracCls, these two don't check if the argument's
+-- superclass is Ord or Num. I believe this is the more predictable behavior
+
+isPrelEqPred :: Type -> Bool
+isPrelEqPred ty = case tyConAppTyCon_maybe ty of
+  Just tyCon -> isPrelEqTyCon tyCon
+  _          -> False
+
+
+isPrelEqTyCon :: TyCon -> Bool
+isPrelEqTyCon tc = tc `hasKey` eqClassKey
+
+isOrdPred :: Type -> Bool
+isOrdPred ty = case tyConAppTyCon_maybe ty of
+  Just tyCon -> tyCon `hasKey` ordClassKey
+  _          -> False
+
+-- Not just Num, but Fractional, Integral as well
+isNumericPred :: Type -> Bool
+isNumericPred ty = case tyConAppTyCon_maybe ty of
+  Just tyCon -> getUnique tyCon `elem` numericClassKeys
+  _          -> False
+
+
+
 --------------------------------------------------------------------------------
 -- | The following functions test if a `CoreExpr` or `CoreVar` are just types
 --   in disguise, e.g. have `PredType` (in the GHC sense of the word), and so
@@ -829,3 +919,107 @@ defaultDataCons _ _ =
 
 isEvVar :: Id -> Bool 
 isEvVar x = isPredVar x || isTyVar x || isCoVar x
+
+
+--------------------------------------------------------------------------------
+-- | Elaboration
+--------------------------------------------------------------------------------
+
+-- FIXME: the handling of exceptions seems to be broken
+
+-- partially stolen from GHC'sa exprType
+
+elaborateHsExprInst
+  :: GhcMonad m => LHsExpr GhcPs -> m (Messages, Maybe CoreExpr)
+elaborateHsExprInst expr = elaborateHsExpr TM_Inst expr
+
+
+elaborateHsExpr
+  :: GhcMonad m => TcRnExprMode -> LHsExpr GhcPs -> m (Messages, Maybe CoreExpr)
+elaborateHsExpr mode expr =
+  withSession $ \hsc_env -> liftIO $ hscElabHsExpr hsc_env mode expr
+
+hscElabHsExpr :: HscEnv -> TcRnExprMode -> LHsExpr GhcPs -> IO (Messages, Maybe CoreExpr)
+hscElabHsExpr hsc_env0 mode expr = runInteractiveHsc hsc_env0 $ do
+  hsc_env <- Ghc.getHscEnv
+  liftIO $ elabRnExpr hsc_env mode expr
+
+
+elabRnExpr
+  :: HscEnv -> TcRnExprMode -> LHsExpr GhcPs -> IO (Messages, Maybe CoreExpr)
+elabRnExpr hsc_env mode rdr_expr =
+  runTcInteractive hsc_env $ do
+    (rn_expr, _fvs) <- rnLExpr rdr_expr
+    failIfErrsM
+    uniq <- newUnique
+    let fresh_it = itName uniq (getLoc rdr_expr)
+        orig     = lexprCtOrigin rn_expr
+    (tclvl, lie, (tc_expr, res_ty)) <- pushLevelAndCaptureConstraints $ do
+      (_tc_expr, expr_ty) <- tcInferSigma rn_expr
+      expr_ty'            <- if inst
+        then snd <$> deeplyInstantiate orig expr_ty
+        else return expr_ty
+      return (_tc_expr, expr_ty')
+    (_, _, evbs, residual, _) <- simplifyInfer tclvl
+                                            infer_mode
+                                            []    {- No sig vars -}
+                                            [(fresh_it, res_ty)]
+                                            lie
+    evbs' <- perhaps_disable_default_warnings $ simplifyInteractive residual
+    full_expr <- zonkTopLExpr (mkHsDictLet (EvBinds evbs') (mkHsDictLet evbs tc_expr))
+    initDsTc $ dsLExpr full_expr
+ where
+  (inst, infer_mode, perhaps_disable_default_warnings) = case mode of
+    TM_Inst    -> (True, NoRestrictions, id)
+    TM_NoInst  -> (False, NoRestrictions, id)
+    TM_Default -> (True, EagerDefaulting, unsetWOptM Opt_WarnTypeDefaults)
+
+newtype HashableType = HashableType {getHType :: Type}
+
+instance Eq HashableType where
+  x == y = eqType (getHType x) (getHType y)
+
+instance Ord HashableType where
+  compare x y = nonDetCmpType (getHType x) (getHType y)
+
+instance Outputable HashableType where
+  ppr = ppr . getHType
+
+
+--------------------------------------------------------------------------------
+-- | Superclass coherence
+--------------------------------------------------------------------------------
+
+canonSelectorChains :: PredType -> OM.Map HashableType [Id]
+canonSelectorChains t = foldr (OM.unionWith const) mempty (zs : xs)
+ where
+  (cls, ts) = getClassPredTys t
+  scIdTys   = classSCSelIds cls
+  ys        = fmap (\d -> (d, piResultTys (idType d) (ts ++ [t]))) scIdTys
+  zs        = OM.fromList $ fmap (\(x, y) -> (HashableType y, [x])) ys
+  xs        = fmap (\(d, t') -> fmap (d :) (canonSelectorChains t')) ys
+
+buildCoherenceOblig :: Class -> [[([Id], [Id])]]
+buildCoherenceOblig cls = evalState (mapM f xs) OM.empty
+ where
+  (ts, _, selIds, _) = classBigSig cls
+  tts                = mkTyVarTy <$> ts
+  t                  = mkClassPred cls tts
+  ys = fmap (\d -> (d, piResultTys (idType d) (tts ++ [t]))) selIds
+  xs                 = fmap (\(d, t') -> fmap (d:) (canonSelectorChains t')) ys
+  f tid = do
+    ctid' <- get
+    modify (flip (OM.unionWith const) tid)
+    pure . OM.elems $ OM.intersectionWith (,) ctid' (fmap tail tid)
+
+
+-- to be zipped onto the super class selectors
+coherenceObligToRef :: (F.Symbolic s) => s -> [Id] -> [Id] -> F.Reft
+coherenceObligToRef d = coherenceObligToRefE (F.eVar $ F.symbol d)
+
+coherenceObligToRefE :: F.Expr -> [Id] -> [Id] -> F.Reft
+coherenceObligToRefE e rps0 rps1 = F.Reft (F.vv_, F.PAtom F.Eq lhs rhs)
+  where lhs = L.foldr EApp e ps0
+        rhs = L.foldr EApp (F.eVar F.vv_) ps1
+        ps0 = F.eVar . F.symbol <$> L.reverse rps0
+        ps1 = F.eVar . F.symbol <$> L.reverse rps1
diff --git a/src/Language/Haskell/Liquid/Measure.hs b/src/Language/Haskell/Liquid/Measure.hs
index 0125e14237..057b5fc1ac 100644
--- a/src/Language/Haskell/Liquid/Measure.hs
+++ b/src/Language/Haskell/Liquid/Measure.hs
@@ -81,26 +81,26 @@ checkDuplicateMeasure ms
       err m ms   = ErrDupMeas (fSrcSpan m) (pprint (val m)) (fSrcSpan <$> ms)
 
 
-dataConTypes :: MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)])
-dataConTypes  s = (ctorTys, measTys)
+dataConTypes :: Bool -> MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)])
+dataConTypes allowTC  s = (ctorTys, measTys)
   where
     measTys     = [(msName m, msSort m) | m <- M.elems (measMap s) ++ imeas s]
-    ctorTys     = concatMap makeDataConType (notracepp "HOHOH" . snd <$> M.toList (ctorMap s))
+    ctorTys     = concatMap (makeDataConType allowTC) (notracepp "HOHOH" . snd <$> M.toList (ctorMap s))
 
-makeDataConType :: [Def (RRType Reft) DataCon] -> [(Var, RRType Reft)]
-makeDataConType []
+makeDataConType :: Bool -> [Def (RRType Reft) DataCon] -> [(Var, RRType Reft)]
+makeDataConType _ []
   = []
-makeDataConType ds | Mb.isNothing (dataConWrapId_maybe dc)
+makeDataConType allowTC ds | Mb.isNothing (dataConWrapId_maybe dc)
   = notracepp _msg [(woId, notracepp _msg $ combineDCTypes "cdc0" t ts)]
   where
     dc   = ctor (head ds)
     woId = dataConWorkId dc
     t    = varType woId
-    ts   = defRefType t <$> ds
+    ts   = defRefType allowTC t <$> ds
     _msg  = "makeDataConType0" ++ showpp (woId, t, ts)
 
-makeDataConType ds
-  = [(woId, extend loci woRType wrRType), (wrId, extend loci wrRType woRType)]
+makeDataConType allowTC ds
+  = [(woId, extend allowTC loci woRType wrRType), (wrId, extend allowTC loci wrRType woRType)]
   where
     (wo, wr) = L.partition isWorkerDef ds
     dc       = ctor $ head ds
@@ -109,8 +109,8 @@ makeDataConType ds
     wot      = varType woId
     wrId     = dataConWrapId dc
     wrt      = varType wrId
-    wots     = defRefType wot <$> wo
-    wrts     = defRefType wrt <$> wr
+    wots     = defRefType allowTC wot <$> wo
+    wrts     = defRefType allowTC wrt <$> wr
 
     wrRType  = combineDCTypes "cdc1" wrt wrts
     woRType  = combineDCTypes "cdc2" wot wots
@@ -125,12 +125,13 @@ makeDataConType ds
       = length (binds def) == length (fst $ splitFunTys $ snd $ splitForAllTys wot)
 
 
-extend :: SourcePos
+extend :: Bool
+       -> SourcePos
        -> RType RTyCon RTyVar Reft
        -> RRType Reft
        -> RType RTyCon RTyVar Reft
-extend lc t1' t2
-  | Just su <- mapArgumens lc t1 t2
+extend allowTC lc t1' t2
+  | Just su <- mapArgumens allowTC lc t1 t2
   = t1 `strengthenResult` subst su (Mb.fromMaybe mempty (stripRTypeBase $ resultTy t2))
   | otherwise
   = t1
@@ -161,8 +162,8 @@ noDummySyms t
 combineDCTypes :: String -> Type -> [RRType Reft] -> RRType Reft
 combineDCTypes _msg t ts = L.foldl' strengthenRefTypeGen (ofType t) ts
 
-mapArgumens :: SourcePos -> RRType Reft -> RRType Reft -> Maybe Subst
-mapArgumens lc t1 t2 = go xts1' xts2'
+mapArgumens :: Bool -> SourcePos -> RRType Reft -> RRType Reft -> Maybe Subst
+mapArgumens allowTC lc t1 t2 = go xts1' xts2'
   where
     xts1 = zip (ty_binds rep1) (ty_args rep1)
     xts2 = zip (ty_binds rep2) (ty_args rep2)
@@ -172,7 +173,7 @@ mapArgumens lc t1 t2 = go xts1' xts2'
     xts1' = dropWhile canDrop xts1
     xts2' = dropWhile canDrop xts2
 
-    canDrop (_, t) = isClassType t || isEqType t
+    canDrop (_, t) = if allowTC then isEmbeddedClass t else isClassType t || isEqType t
 
     go xs ys
       | length xs == length ys && and (zipWith (==) (toRSort . snd <$> xts1') (toRSort . snd <$> xts2'))
@@ -182,11 +183,11 @@ mapArgumens lc t1 t2 = go xts1' xts2'
           ++ show t1 ++ "\n" ++ show t2 )
 
 -- should constructors have implicits? probably not
-defRefType :: Type -> Def (RRType Reft) DataCon -> RRType Reft
-defRefType tdc (Def f dc mt xs body)
+defRefType :: Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft
+defRefType allowTC tdc (Def f dc mt xs body)
                     = generalize $ mkArrow as' [] [] xts t'
   where
-    xts             = stitchArgs (fSrcSpan f) dc xs ts 
+    xts             = stitchArgs allowTC (fSrcSpan f) dc xs ts 
     t'              = refineWithCtorBody dc f body t
     t               = Mb.fromMaybe (ofType tr) mt
     (αs, ts, tr)    = splitType tdc
@@ -200,24 +201,25 @@ splitType t  = (αs, ts, tr)
     (ts, tr) = splitFunTys tb
 
 stitchArgs :: (Monoid t1, PPrint a)
-           => SrcSpan
+           => Bool
+           -> SrcSpan
            -> a
            -> [(Symbol, Maybe (RRType Reft))]
            -> [Type]
            -> [(Symbol, RRType Reft, t1)]
-stitchArgs sp dc allXs allTs
+stitchArgs allowTC sp dc allXs allTs
   | nXs == nTs         = (g (dummySymbol, Nothing) . ofType <$> pts)
                       ++ zipWith g xs (ofType <$> ts)
   | otherwise          = panicFieldNumMismatch sp dc nXs nTs
     where
-      (pts, ts)        = L.partition (\t -> notracepp ("isPredTy: " ++ showpp t) $ Ghc.isEvVarType t) allTs
+      (pts, ts)        = L.partition (\t -> notracepp ("isPredTy: " ++ showpp t) $ (if allowTC then isEmbeddedDictType else Ghc.isEvVarType ) t) allTs
       (_  , xs)        = L.partition (coArg . snd) allXs
       nXs              = length xs
       nTs              = length ts
       g (x, Just t) _  = (x, t, mempty)
       g (x, _)      t  = (x, t, mempty)
       coArg Nothing    = False
-      coArg (Just t)   = Ghc.isEvVarType . toType $ t
+      coArg (Just t)   = (if allowTC then isEmbeddedDictType else Ghc.isEvVarType ). toType $ t
 
 panicFieldNumMismatch :: (PPrint a, PPrint a1, PPrint a3)
                       => SrcSpan -> a3 -> a1 -> a -> a2
diff --git a/src/Language/Haskell/Liquid/Transforms/ANF.hs b/src/Language/Haskell/Liquid/Transforms/ANF.hs
index 4f9ce1f2bb..86633de5e7 100644
--- a/src/Language/Haskell/Liquid/Transforms/ANF.hs
+++ b/src/Language/Haskell/Liquid/Transforms/ANF.hs
@@ -42,6 +42,7 @@ import           Language.Haskell.Liquid.UX.Config  as UX
 import qualified Language.Haskell.Liquid.Misc       as Misc 
 import           Language.Haskell.Liquid.GHC.Misc   as GM
 import           Language.Haskell.Liquid.Transforms.Rec
+import           Language.Haskell.Liquid.Transforms.InlineAux
 import           Language.Haskell.Liquid.Transforms.Rewrite
 import           Language.Haskell.Liquid.Types.Errors
 
@@ -71,7 +72,8 @@ anormalize cfg hscEnv modGuts = do
       act      = Misc.concatMapM (normalizeTopBind γ0) rwr_cbs
       γ0       = emptyAnfEnv cfg
       rwr_cbs  = rewriteBinds cfg orig_cbs
-      orig_cbs = transformRecExpr $ mg_binds modGuts
+      orig_cbs = transformRecExpr inl_cbs
+      inl_cbs  = inlineAux (mg_module modGuts) $ mg_binds modGuts
       untidy   = UX.untidyCore cfg
 
 {-
diff --git a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
index 1b1fceb36c..48b3821db9 100644
--- a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
+++ b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
@@ -20,16 +20,16 @@ module Language.Haskell.Liquid.Transforms.CoreToLogic
 
 import           Data.ByteString                       (ByteString)
 import           Prelude                               hiding (error)
-import           Language.Haskell.Liquid.GHC.TypeRep
 import           Language.Haskell.Liquid.GHC.API       hiding (Expr, Located)
 -- import qualified Id 
 import qualified Var
 import qualified TyCon 
 import           Coercion
+import qualified Outputable                            as O
+import qualified CoreSubst                             as C
 import qualified Pair
 -- import qualified Text.Printf as Printf
 import qualified CoreSyn                               as C
-import           Literal
 import           IdInfo
 import qualified Data.List                             as L
 import           Data.Maybe                            (listToMaybe) 
@@ -38,8 +38,6 @@ import qualified Data.Char
 import qualified Text.Printf as Printf 
 import           Data.Text.Encoding
 import           Data.Text.Encoding.Error
-import           TysWiredIn
-import           Name                                  (getSrcSpan)
 import           Control.Monad.State
 import           Control.Monad.Except
 import           Control.Monad.Identity
@@ -58,25 +56,27 @@ import           Language.Haskell.Liquid.Types.RefType
 
 import qualified Data.HashMap.Strict                   as M
 
-logicType :: (Reftable r) => Type -> RRType r
-logicType τ      = fromRTypeRep $ t { ty_binds = bs, ty_args = as, ty_refts = rs}
+logicType :: (Reftable r) => Bool -> Type -> RRType r
+logicType allowTC τ      = fromRTypeRep $ t { ty_binds = bs, ty_args = as, ty_refts = rs}
   where
     t            = toRTypeRep $ ofType τ
-    (bs, as, rs) = unzip3 $ dropWhile (isClassType . Misc.snd3) $ zip3 (ty_binds t) (ty_args t) (ty_refts t)
+    (bs, as, rs) = unzip3 $ dropWhile (isErasable . Misc.snd3) $ zip3 (ty_binds t) (ty_args t) (ty_refts t)
+    isErasable   = if allowTC then isEmbeddedClass else isClassType
 
 {- | [NOTE:inlineSpecType type]: the refinement depends on whether the result type is a Bool or not:
       CASE1: measure f@logic :: X -> Bool <=> f@haskell :: x:X -> {v:Bool | v <=> (f@logic x)}
      CASE2: measure f@logic :: X -> Y    <=> f@haskell :: x:X -> {v:Y    | v = (f@logic x)}
  -}
 -- formerly: strengthenResult
-inlineSpecType :: Var -> SpecType
-inlineSpecType v = fromRTypeRep $ rep {ty_res = res `strengthen` r , ty_binds = xs}
+inlineSpecType :: Bool -> Var -> SpecType
+inlineSpecType  allowTC v = fromRTypeRep $ rep {ty_res = res `strengthen` r , ty_binds = xs}
   where
     r              = MkUReft (mkR (mkEApp f (mkA <$> vxs))) mempty
     rep            = toRTypeRep t
     res            = ty_res rep
     xs             = intSymbol (symbol ("x" :: String)) <$> [1..length $ ty_binds rep]
-    vxs            = dropWhile (isClassType . snd) $ zip xs (ty_args rep)
+    vxs            = dropWhile (isErasable . snd) $ zip xs (ty_args rep)
+    isErasable     = if allowTC then isEmbeddedClass else isClassType
     f              = dummyLoc (symbol v)
     t              = ofType (GM.expandVarType v) :: SpecType
     mkA            = EVar . fst 
@@ -90,8 +90,8 @@ inlineSpecType v = fromRTypeRep $ rep {ty_res = res `strengthen` r , ty_binds =
 --   TODO: SIMPLIFY by dropping support for multi parameter measures
 
 -- formerly: strengthenResult'
-measureSpecType :: Var -> SpecType
-measureSpecType v = go mkT [] [1..] t
+measureSpecType :: Bool -> Var -> SpecType
+measureSpecType allowTC v = go mkT [] [1..] t
   where 
     mkR | boolRes   = propReft 
         | otherwise = exprReft  
@@ -103,14 +103,14 @@ measureSpecType v = go mkT [] [1..] t
     go f args i (RAllT a t r)    = RAllT a (go f args i t) r 
     go f args i (RAllP p t)      = RAllP p $ go f args i t
     go f args i (RFun x t1 t2 r)
-     | isClassType t1           = RFun x t1 (go f args i t2) r
+     | (if allowTC then isEmbeddedClass else isClassType) t1           = RFun x t1 (go f args i t2) r
     go f args i t@(RFun _ t1 t2 r)
      | hasRApps t               = RFun x' t1 (go f (x':args) (tail i) t2) r
                                        where x' = intSymbol (symbol ("x" :: String)) (head i)
     go f args _ t                = t `strengthen` f args
 
     hasRApps (RFun _ t1 t2 _) = hasRApps t1 || hasRApps t2
-    hasRApps (RApp {})        = True
+    hasRApps RApp {}          = True
     hasRApps _                = False
     
    
@@ -118,15 +118,15 @@ measureSpecType v = go mkT [] [1..] t
 --   that is added, e.g. for measures in /strengthenResult'. 
 --   This should only be used _when_ checking the body of 'foo' 
 --   where the output, is, by definition, equal to the singleton.
-weakenResult :: Var -> SpecType -> SpecType 
-weakenResult v t = F.notracepp msg t'
+weakenResult :: Bool -> Var -> SpecType -> SpecType 
+weakenResult allowTC v t = F.notracepp msg t'
   where 
     msg          = "weakenResult v =" ++ GM.showPpr v ++ " t = " ++ showpp t
     t'           = fromRTypeRep $ rep { ty_res = mapExprReft weaken (ty_res rep) } 
     rep          = toRTypeRep t
     weaken x     = pAnd . filter ((Just vE /=) . isSingletonExpr x) . conjuncts 
     vE           = mkEApp vF xs
-    xs           = EVar . fst <$> dropWhile (isClassType . snd) xts 
+    xs           = EVar . fst <$> dropWhile ((if allowTC then isEmbeddedClass else isClassType) . snd) xts 
     xts          = zip (ty_binds rep) (ty_args rep)
     vF           = dummyLoc (symbol v)
 
@@ -165,9 +165,9 @@ runToLogicWithBoolBinds xs tce lmap dm ferror m
       , lsDCMap  = dm
       }
 
-coreAltToDef :: (Reftable r) => LocSymbol -> Var -> [Var] -> Var -> Type -> [C.CoreAlt] 
+coreAltToDef :: (Reftable r) => Bool -> LocSymbol -> Var -> [Var] -> Var -> Type -> [C.CoreAlt] 
              -> LogicM [Def (Located (RRType r)) DataCon]
-coreAltToDef x z zs y t alts  
+coreAltToDef allowTC x z zs y t alts  
   | not (null litAlts) = measureFail x "Cannot lift definition with literal alternatives" 
   | otherwise          = do 
       d1s <- F.notracepp "coreAltDefs-1" <$> mapM (mkAlt x cc myArgs z) dataAlts 
@@ -186,13 +186,13 @@ coreAltToDef x z zs y t alts
       = Def x {- (toArgs id args) -} d (Just $ varRType dx) (toArgs Just xs') 
       . ctor 
       . (`subst1` (F.symbol dx, F.mkEApp (GM.namedLocSymbol d) (F.eVar <$> xs'))) 
-     <$> coreToLg e
-      where xs' = filter (not . GM.isEvVar) xs
+     <$> coreToLg allowTC e
+      where xs' = filter (not . if allowTC then GM.isEmbeddedDictVar else GM.isEvVar) xs
     mkAlt _ _ _ _ alt 
       = throw $ "Bad alternative" ++ GM.showPpr alt
 
     mkDef x ctor _args dx (Just dtss) (Just e) = do  
-      eDef   <- ctor <$> coreToLg e
+      eDef   <- ctor <$> coreToLg allowTC e
       -- let ys  = toArgs id args
       let dxt = Just (varRType dx)
       return  [ Def x {- ys -} d dxt (defArgs x ts) eDef | (d, _, ts) <- dtss ]
@@ -209,15 +209,15 @@ defArgs x     = zipWith (\i t -> (defArg i, defRTyp t)) [0..]
     defArg    = tempSymbol (val x)
     defRTyp   = Just . F.atLoc x . ofType
 
-coreToDef :: Reftable r => LocSymbol -> Var -> C.CoreExpr
+coreToDef :: Reftable r => Bool -> LocSymbol -> Var -> C.CoreExpr
           -> LogicM [Def (Located (RRType r)) DataCon]
-coreToDef x _ e                   = go [] $ inlinePreds $ simplify e
+coreToDef allowTC x _ e                   = go [] $ inlinePreds $ simplify allowTC  e
   where
     go args   (C.Lam  x e)        = go (x:args) e
     go args   (C.Tick _ e)        = go args e
-    go (z:zs) (C.Case _ y t alts) = coreAltToDef x z zs y t alts 
+    go (z:zs) (C.Case _ y t alts) = coreAltToDef allowTC x z zs y t alts 
     go (z:zs) e                   
-      | Just t <- isMeasureArg z  = coreAltToDef x z zs z t [(C.DEFAULT, [], e)]
+      | Just t <- isMeasureArg z  = coreAltToDef allowTC x z zs z t [(C.DEFAULT, [], e)]
     go _ _                        = measureFail x "Does not have a case-of at the top-level" 
 
     inlinePreds   = inline (eqType boolTy . GM.expandVarType)
@@ -243,48 +243,51 @@ isMeasureArg x
 varRType :: (Reftable r) => Var -> Located (RRType r)
 varRType = GM.varLocInfo ofType
 
-coreToFun :: LocSymbol -> Var -> C.CoreExpr ->  LogicM ([Var], Either Expr Expr)
-coreToFun _ _v e = go [] $ normalize e
+coreToFun :: Bool -> LocSymbol -> Var -> C.CoreExpr ->  LogicM ([Var], Either Expr Expr)
+coreToFun allowTC _ _v e = go [] $ normalize allowTC e
   where
+    isE = if allowTC then GM.isEmbeddedDictVar else isErasable
     go acc (C.Lam x e)  | isTyVar    x = go acc e
-    go acc (C.Lam x e)  | isErasable x = go acc e
+    go acc (C.Lam x e)  | isE x = go acc e
     go acc (C.Lam x e)  = go (x:acc) e
     go acc (C.Tick _ e) = go acc e
-    go acc e            = (reverse acc,) . Right <$> coreToLg e
+    go acc e            = (reverse acc,) . Right <$> coreToLg allowTC e
     
 
 instance Show C.CoreExpr where
   show = GM.showPpr
 
-coreToLogic :: C.CoreExpr -> LogicM Expr
-coreToLogic cb = coreToLg (normalize cb)
+coreToLogic :: Bool -> C.CoreExpr -> LogicM Expr
+coreToLogic allowTC cb = coreToLg allowTC (normalize allowTC cb)
 
 
-coreToLg :: C.CoreExpr -> LogicM Expr
-coreToLg (C.Let b e)
-  = subst1 <$> coreToLg e <*>  makesub b
-coreToLg (C.Tick _ e)          = coreToLg e
-coreToLg (C.App (C.Var v) e)
-  | ignoreVar v                = coreToLg e
-coreToLg (C.Var x)
+coreToLg :: Bool -> C.CoreExpr -> LogicM Expr
+coreToLg allowTC  (C.Let (C.NonRec x (C.Coercion c)) e)
+  = coreToLg allowTC (C.substExpr O.empty (C.extendCvSubst C.emptySubst x c) e)
+coreToLg allowTC  (C.Let b e)
+  = subst1 <$> coreToLg allowTC e <*>  makesub allowTC b
+coreToLg allowTC (C.Tick _ e)          = coreToLg allowTC e
+coreToLg allowTC (C.App (C.Var v) e)
+  | ignoreVar v                = coreToLg allowTC e
+coreToLg allowTC (C.Var x)
   | x == falseDataConId        = return PFalse
   | x == trueDataConId         = return PTrue
   | otherwise                  = (lsSymMap <$> getState) >>= eVarWithMap x
-coreToLg e@(C.App _ _)         = toPredApp e
-coreToLg (C.Case e b _ alts)
-  | eqType (GM.expandVarType b) boolTy  = checkBoolAlts alts >>= coreToIte e
-coreToLg (C.Lam x e)           = do p     <- coreToLg e
-                                    tce   <- lsEmb <$> getState
-                                    return $ ELam (symbol x, typeSort tce (GM.expandVarType x)) p
-coreToLg (C.Case e b _ alts)   = do p <- coreToLg e
-                                    casesToLg b p alts
-coreToLg (C.Lit l)             = case mkLit l of
-                                   Nothing -> throw $ "Bad Literal in measure definition" ++ GM.showPpr l
-                                   Just i  -> return i
-coreToLg (C.Cast e c)          = do (s, t) <- coerceToLg c
-                                    e'     <- coreToLg   e
-                                    return (ECoerc s t e')
-coreToLg e                     = throw ("Cannot transform to Logic:\t" ++ GM.showPpr e)
+coreToLg allowTC e@(C.App _ _)         = toPredApp allowTC e
+coreToLg allowTC (C.Case e b _ alts)
+  | eqType (GM.expandVarType b) boolTy  = checkBoolAlts alts >>= coreToIte allowTC e
+coreToLg allowTC (C.Lam x e)           = do p     <- coreToLg allowTC e
+                                            tce   <- lsEmb <$> getState
+                                            return $ ELam (symbol x, typeSort tce (GM.expandVarType x)) p
+coreToLg allowTC (C.Case e b _ alts)   = do p <- coreToLg allowTC e
+                                            casesToLg allowTC b p alts
+coreToLg allowTC (C.Lit l)             = case mkLit l of
+                                           Nothing -> throw $ "Bad Literal in measure definition" ++ GM.showPpr l
+                                           Just i  -> return i
+coreToLg allowTC (C.Cast e c)          = do (s, t) <- coerceToLg c
+                                            e'     <- coreToLg allowTC   e
+                                            return (ECoerc s t e')
+coreToLg _       e                     = throw ("Cannot transform to Logic:\t" ++ GM.showPpr e)
 
 
 
@@ -315,8 +318,8 @@ checkBoolAlts [(C.DataAlt true, [], etrue), (C.DataAlt false, [], efalse)]
 checkBoolAlts alts
   = throw ("checkBoolAlts failed on " ++ GM.showPpr alts)
 
-casesToLg :: Var -> Expr -> [C.CoreAlt] -> LogicM Expr
-casesToLg v e alts = mapM (altToLg e) normAlts >>= go
+casesToLg :: Bool -> Var -> Expr -> [C.CoreAlt] -> LogicM Expr
+casesToLg allowTC v e alts = mapM (altToLg allowTC e) normAlts >>= go
   where
     normAlts       = normalizeAlts alts
     go :: [(C.AltCon, Expr)] -> LogicM Expr
@@ -341,15 +344,15 @@ normalizeAlts alts      = ctorAlts ++ defAlts
     (defAlts, ctorAlts) = L.partition isDefault alts 
     isDefault (c,_,_)   = c == C.DEFAULT 
 
-altToLg :: Expr -> C.CoreAlt -> LogicM (C.AltCon, Expr)
-altToLg de (a@(C.DataAlt d), xs, e) = do 
-  p  <- coreToLg e
+altToLg :: Bool -> Expr -> C.CoreAlt -> LogicM (C.AltCon, Expr)
+altToLg allowTC de (a@(C.DataAlt d), xs, e) = do 
+  p  <- coreToLg allowTC e
   dm <- gets lsDCMap
-  let su = mkSubst $ concat [ dataConProj dm de d x i | (x, i) <- zip (filter (not . GM.isEvVar) xs) [1..]]
+  let su = mkSubst $ concat [ dataConProj dm de d x i | (x, i) <- zip (filter (not . if allowTC then GM.isEmbeddedDictVar else GM.isEvVar) xs) [1..]]
   return (a, subst su p)
 
-altToLg _ (a, _, e)
-  = (a, ) <$> coreToLg e
+altToLg allowTC _ (a, _, e)
+  = (a, ) <$> coreToLg allowTC e
 
 dataConProj :: DataConMap -> Expr -> DataCon -> Var -> Int -> [(Symbol, Expr)]
 dataConProj dm de d x i = [(symbol x, t), (GM.simplesymbol x, t)]
@@ -360,37 +363,39 @@ dataConProj dm de d x i = [(symbol x, t), (GM.simplesymbol x, t)]
 primDataCon :: DataCon -> Bool 
 primDataCon d = d == intDataCon
 
-coreToIte :: C.CoreExpr -> (C.CoreExpr, C.CoreExpr) -> LogicM Expr
-coreToIte e (efalse, etrue)
-  = do p  <- coreToLg e
-       e1 <- coreToLg efalse
-       e2 <- coreToLg etrue
+coreToIte :: Bool -> C.CoreExpr -> (C.CoreExpr, C.CoreExpr) -> LogicM Expr
+coreToIte allowTC e (efalse, etrue)
+  = do p  <- coreToLg allowTC e
+       e1 <- coreToLg allowTC efalse
+       e2 <- coreToLg allowTC etrue
        return $ EIte p e2 e1
 
-toPredApp :: C.CoreExpr -> LogicM Expr
-toPredApp p = go . Misc.mapFst opSym . splitArgs $ p
+toPredApp :: Bool -> C.CoreExpr -> LogicM Expr
+toPredApp allowTC p = go . Misc.mapFst opSym . splitArgs allowTC $ p
   where
     opSym = fmap GM.dropModuleNames . tomaybesymbol
     go (Just f, [e1, e2])
       | Just rel <- M.lookup f brels
-      = PAtom rel <$> coreToLg e1 <*> coreToLg e2
+      = PAtom rel <$> coreToLg allowTC e1 <*> coreToLg allowTC e2
     go (Just f, [e])
       | f == symbol ("not" :: String)
-      = PNot <$>  coreToLg e
+      = PNot <$>  coreToLg allowTC e
     go (Just f, [e1, e2])
       | f == symbol ("||" :: String)
-      = POr <$> mapM coreToLg [e1, e2]
+      = POr <$> mapM (coreToLg allowTC) [e1, e2]
       | f == symbol ("&&" :: String)
-      = PAnd <$> mapM coreToLg [e1, e2]
+      = PAnd <$> mapM (coreToLg allowTC) [e1, e2]
       | f == symbol ("==>" :: String)
-      = PImp <$> coreToLg e1 <*> coreToLg e2
+      = PImp <$> coreToLg allowTC e1 <*> coreToLg allowTC e2
+      | f == symbol ("<=>" :: String)
+      = PIff <$> coreToLg allowTC e1 <*> coreToLg allowTC e2
     go (Just f, [es])
       | f == symbol ("or" :: String)
-      = POr  . deList <$> coreToLg es
+      = POr  . deList <$> coreToLg allowTC es
       | f == symbol ("and" :: String)
-      = PAnd . deList <$> coreToLg es
+      = PAnd . deList <$> coreToLg allowTC es
     go (_, _)
-      = toLogicApp p
+      = toLogicApp allowTC p
     
     deList :: Expr -> [Expr]
     deList (EApp (EApp (EVar cons) e) es)
@@ -402,23 +407,33 @@ toPredApp p = go . Misc.mapFst opSym . splitArgs $ p
     deList e 
       = [e]
 
-toLogicApp :: C.CoreExpr -> LogicM Expr
-toLogicApp e = do
-  let (f, es) = splitArgs e
+toLogicApp :: Bool -> C.CoreExpr -> LogicM Expr
+toLogicApp allowTC e = do
+  let (f, es) = splitArgs allowTC e
   case f of
-    C.Var _ -> do args <- mapM coreToLg es
+    C.Var _ -> do args <- mapM (coreToLg allowTC) es
                   lmap <- lsSymMap <$> getState
                   def  <- (`mkEApp` args) <$> tosymbol f
                   ((\x -> makeApp def lmap x args) <$> (tosymbol' f))
-    _       -> do fe   <- coreToLg f
-                  args <- mapM coreToLg es
+    _       -> do fe   <- coreToLg allowTC f
+                  args <- mapM (coreToLg allowTC) es
                   return $ foldl EApp fe args
 
 makeApp :: Expr -> LogicMap -> Located Symbol-> [Expr] -> Expr
-makeApp _ _ f [e] | val f == symbol ("GHC.Num.negate" :: String)
+makeApp _ _ f [e]
+  | val f == symbol ("GHC.Num.negate" :: String)
   = ENeg e
+  | val f == symbol ("GHC.Num.fromInteger" :: String)
+  , ECon c <- e
+  = ECon c
 
-makeApp _ _ f [e1, e2] | Just op <- M.lookup (val f) bops
+makeApp _ _ f [e1, e2]
+  | Just op <- M.lookup (val f) bops
+  = EBin op e1 e2
+  -- Hack for typeclass support. (overriden == without Eq constraint defined at Ghci)
+  | (modName, sym) <- GM.splitModuleName (val f)
+  , symbol ("Ghci" :: String) `isPrefixOfSym` modName
+  , Just op <- M.lookup (mappendSym (symbol ("GHC.Num." :: String)) sym) bops
   = EBin op e1 e2
 
 makeApp def lmap f es
@@ -472,13 +487,13 @@ bops = M.fromList [ (numSymbol "+", Plus)
     realSymbol :: String -> Symbol
     realSymbol =  symbol . (++) "GHC.Real."
 
-splitArgs :: C.Expr t -> (C.Expr t, [C.Arg t])
-splitArgs e = (f, reverse es)
+splitArgs :: Bool -> C.Expr t -> (C.Expr t, [C.Arg t])
+splitArgs allowTC e = (f, reverse es)
  where
     (f, es) = go e
 
     go (C.App (C.Var i) e) | ignoreVar i       = go e
-    go (C.App f (C.Var v)) | isErasable v      = go f
+    go (C.App f (C.Var v)) | if allowTC then GM.isEmbeddedDictVar v else isErasable v   = go f
     go (C.App f e) = (f', e:es) where (f', es) = go f
     go f           = (f, [])
 
@@ -496,9 +511,9 @@ tosymbol' :: C.CoreExpr -> LogicM (Located Symbol)
 tosymbol' (C.Var x) = return $ dummyLoc $ symbol x 
 tosymbol' e        = throw ("Bad Measure Definition:\n" ++ GM.showPpr e ++ "\t cannot be applied")
 
-makesub :: C.CoreBind -> LogicM (Symbol, Expr)
-makesub (C.NonRec x e) =  (symbol x,) <$> coreToLg e
-makesub  _             = throw "Cannot make Logical Substitution of Recursive Definitions"
+makesub :: Bool -> C.CoreBind -> LogicM (Symbol, Expr)
+makesub allowTC (C.NonRec x e) =  (symbol x,) <$> coreToLg allowTC e
+makesub _       _              = throw "Cannot make Logical Substitution of Recursive Definitions"
 
 mkLit :: Literal -> Maybe Expr
 mkLit (LitNumber _ n _) = mkI n
@@ -557,52 +572,52 @@ isDead :: Id -> Bool
 isDead     = isDeadOcc . occInfo . Var.idInfo
 
 class Simplify a where
-  simplify :: a -> a
+  simplify :: Bool -> a -> a
   inline   :: (Id -> Bool) -> a -> a
 
-  normalize :: a -> a
-  normalize = inline_preds . inline_anf . simplify
+  normalize :: Bool -> a -> a
+  normalize allowTC = inline_preds . inline_anf . simplify allowTC
    where
     inline_preds = inline (eqType boolTy . GM.expandVarType)
     inline_anf   = inline isANF
 
 instance Simplify C.CoreExpr where
-  simplify e@(C.Var _)
+  simplify allowTC e@(C.Var _)
     = e
-  simplify e@(C.Lit _)
+  simplify allowTC e@(C.Lit _)
     = e
-  simplify (C.App e (C.Type _))
-    = simplify e
-  simplify (C.App e (C.Var dict))  | isErasable 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) | isErasable x
-    = simplify e
-  simplify (C.Lam x e)
-    = C.Lam x (simplify e)
-  simplify (C.Let (C.NonRec x _) e) | isErasable x
-    = simplify e
-  simplify (C.Let (C.Rec xes) e)    | all (isErasable . fst) xes
-    = simplify e
-  simplify (C.Let xes e)
-    = C.Let (simplify xes) (simplify e)
-  simplify (C.Case e x _t alts@[(_,_,ee),_,_]) | isBangInteger alts
-    = Misc.traceShow ("To simplify case") $ 
-       sub (M.singleton x (simplify e)) (simplify ee)
-  simplify (C.Case e x t alts)
-    = C.Case (simplify e) x t (filter (not . isUndefined) (simplify <$> alts))
-  simplify (C.Cast e c)
-    = C.Cast (simplify e) c
-  simplify (C.Tick _ e)
-    = simplify e
-  simplify (C.Coercion c)
+  simplify allowTC (C.App e (C.Type _))
+    = simplify allowTC e
+  simplify allowTC (C.App e (C.Var dict))  | (if allowTC then GM.isEmbeddedDictVar else isErasable) dict
+    = simplify allowTC e
+  simplify allowTC (C.App (C.Lam x e) _)   | isDead x
+    = simplify allowTC e
+  simplify allowTC (C.App e1 e2)
+    = C.App (simplify allowTC e1) (simplify allowTC e2)
+  simplify allowTC (C.Lam x e) | isTyVar x
+    = simplify allowTC e
+  simplify allowTC (C.Lam x e) | (if allowTC then GM.isEmbeddedDictVar else isErasable) x
+    = simplify allowTC e
+  simplify allowTC (C.Lam x e)
+    = C.Lam x (simplify allowTC e)
+  simplify allowTC (C.Let (C.NonRec x _) e) | (if allowTC then GM.isEmbeddedDictVar else isErasable) x
+    = simplify allowTC e
+  simplify allowTC (C.Let (C.Rec xes) e)    | all ((if allowTC then GM.isEmbeddedDictVar else isErasable) . fst) xes
+    = simplify allowTC e
+  simplify allowTC (C.Let xes e)
+    = C.Let (simplify allowTC xes) (simplify allowTC e)
+  simplify allowTC (C.Case e x _t alts@[(_,_,ee),_,_]) | isBangInteger alts
+    = Misc.traceShow ("To simplify allowTC case") $ 
+       sub (M.singleton x (simplify allowTC e)) (simplify allowTC ee)
+  simplify allowTC (C.Case e x t alts)
+    = C.Case (simplify allowTC e) x t (filter (not . isUndefined) (simplify allowTC <$> alts))
+  simplify allowTC (C.Cast e c)
+    = C.Cast (simplify allowTC e) c
+  simplify allowTC (C.Tick _ e)
+    = simplify allowTC e
+  simplify allowTC (C.Coercion c)
     = C.Coercion c
-  simplify (C.Type t)
+  simplify allowTC (C.Type t)
     = C.Type t
 
   inline p (C.Let (C.NonRec x ex) e) | p x
@@ -631,14 +646,14 @@ isUndefined (_, _, e) = isUndefinedExpr e
 
 
 instance Simplify C.CoreBind where
-  simplify (C.NonRec x e) = C.NonRec x (simplify e)
-  simplify (C.Rec xes)    = C.Rec (Misc.mapSnd simplify <$> xes )
+  simplify allowTC (C.NonRec x e) = C.NonRec x (simplify allowTC e)
+  simplify allowTC (C.Rec xes)    = C.Rec (Misc.mapSnd (simplify allowTC) <$> xes )
 
   inline p (C.NonRec x e) = C.NonRec x (inline p e)
   inline p (C.Rec xes)    = C.Rec (Misc.mapSnd (inline p) <$> xes)
 
 instance Simplify C.CoreAlt where
-  simplify (c, xs, e) = (c, xs, simplify e)
+  simplify allowTC (c, xs, e) = (c, xs, simplify allowTC e)
     -- where xs   = F.tracepp _msg xs0
     --      _msg = "isCoVars? " ++ F.showpp [(x, isCoVar x, varType x) | x <- xs0]
   inline p (c, xs, e) = (c, xs, inline p e)
diff --git a/src/Language/Haskell/Liquid/Transforms/InlineAux.hs b/src/Language/Haskell/Liquid/Transforms/InlineAux.hs
new file mode 100644
index 0000000000..456e5816c3
--- /dev/null
+++ b/src/Language/Haskell/Liquid/Transforms/InlineAux.hs
@@ -0,0 +1,175 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+module Language.Haskell.Liquid.Transforms.InlineAux
+  ( inlineAux
+  , inlineDFun
+  )
+where
+
+import           CoreSyn
+import           DynFlags
+import qualified Outputable                    as O
+import           MkCore
+import           Control.Arrow                  ( second )
+import           OccurAnal                      ( occurAnalysePgm )
+import qualified Language.Haskell.Liquid.GHC.Misc
+                                               as GM
+import           Class                          ( classAllSelIds )
+import           Id
+import           CoreFVs                        ( exprFreeVarsList )
+import           InstEnv
+import           TcType                         ( tcSplitDFunTy )
+import           GhcPlugins                     ( isDFunId
+                                                , exprType
+                                                , OccName
+                                                , Module
+                                                , occNameString
+                                                , getOccName
+                                                , mkCoreApps
+                                                )
+import           Predicate                      ( isDictId )
+import qualified Data.HashMap.Strict           as M
+import           CoreSubst
+import           GHC                            ( isDictonaryId )
+import           SimplMonad
+import           SimplCore
+import           Control.Monad.State
+import           Data.Functor.Foldable
+
+buildDictSubst :: CoreProgram -> M.HashMap Id CoreExpr
+buildDictSubst = cata f
+ where
+  f Nil = M.empty
+  f (Cons b s) | NonRec x e <- b, isDFunId x || isDictonaryId x = M.insert x e s
+               | otherwise = s
+
+
+inlineAux :: Module -> CoreProgram -> CoreProgram
+inlineAux m cbs =  (map f cbs)
+ where
+  f :: CoreBind -> CoreBind
+  f all@(NonRec x e)
+    | Just (dfunId, methodToAux) <- M.lookup x auxToMethodToAux = NonRec
+      x
+      (inlineAuxExpr dfunId methodToAux e)
+    | otherwise = all
+  f (Rec bs) = Rec (fmap g bs)
+   where
+    g all@(x, e)
+      | Just (dfunId, methodToAux) <- M.lookup x auxToMethodToAux
+      = (x, inlineAuxExpr dfunId methodToAux e)
+      | otherwise
+      = all
+  auxToMethodToAux = mconcat $ fmap (uncurry dfunIdSubst) (grepDFunIds cbs)
+
+
+inlineDFun :: DynFlags -> CoreProgram -> IO CoreProgram
+inlineDFun df cbs = pure cbs-- mapM go cbs
+ -- where
+ --  go orig@(NonRec x e) | isDFunId x = do
+ --                           -- e''' <- simplifyExpr df e''
+ --                           let newBody = mkCoreApps (GM.tracePpr ("substituted type:" ++ GM.showPpr (exprType (mkCoreApps e' binders))) e') (fmap Var binders)
+ --                               bind = NonRec (mkWildValBinder (exprType newBody)) newBody
+ --                           pure $ NonRec x (mkLet bind e)
+ --                       | otherwise  = pure orig
+ --   where
+ --    -- wcBinder = mkWildValBinder t
+ --    (binders, _) = GM.tracePpr "collectBinders"$ collectBinders e
+ --    e' = substExprAll O.empty subst e
+ --  go recs = pure recs
+ --  subst = buildDictSubst cbs
+
+
+
+lookupIdSubstAll :: O.SDoc -> M.HashMap Id CoreExpr -> Id -> CoreExpr
+lookupIdSubstAll doc env v | Just e <- M.lookup v env = e
+                           | otherwise                = Var v
+        -- Vital! See Note [Extending the Subst]
+  -- | otherwise = WARN( True, text "CoreSubst.lookupIdSubst" <+> doc <+> ppr v
+  --                           $$ ppr in_scope)
+
+substExprAll :: O.SDoc -> M.HashMap Id CoreExpr -> CoreExpr -> CoreExpr
+substExprAll doc subst orig_expr = subst_expr_all doc subst orig_expr
+
+
+subst_expr_all :: O.SDoc -> M.HashMap Id CoreExpr -> CoreExpr -> CoreExpr
+subst_expr_all doc subst expr = go expr
+ where
+  go (Var v) = lookupIdSubstAll (doc O.$$ O.text "subst_expr_all") subst v
+  go (Type     ty      ) = Type ty
+  go (Coercion co      ) = Coercion co
+  go (Lit      lit     ) = Lit lit
+  go (App  fun     arg ) = App (go fun) (go arg)
+  go (Tick tickish e   ) = Tick tickish (go e)
+  go (Cast e       co  ) = Cast (go e) co
+     -- Do not optimise even identity coercions
+     -- Reason: substitution applies to the LHS of RULES, and
+     --         if you "optimise" an identity coercion, you may
+     --         lose a binder. We optimise the LHS of rules at
+     --         construction time
+
+  go (Lam  bndr    body) = Lam bndr (subst_expr_all doc subst body)
+
+  go (Let  bind    body) = Let (mapBnd go bind) (subst_expr_all doc subst body)
+
+  go (Case scrut bndr ty alts) =
+    Case (go scrut) bndr ty (map (go_alt subst) alts)
+
+  go_alt subst (con, bndrs, rhs) = (con, bndrs, subst_expr_all doc subst rhs)
+
+
+
+-- grab the dictionaries
+grepDFunIds :: CoreProgram -> [(DFunId, CoreExpr)]
+grepDFunIds = filter (isDFunId . fst) . flattenBinds
+
+isClassOpAuxOccName :: OccName -> Bool
+isClassOpAuxOccName occ = case occNameString occ of
+  '$' : 'c' : _ -> True
+  _             -> False
+
+isClassOpAuxOf :: Id -> Id -> Bool
+isClassOpAuxOf aux method = case occNameString $ getOccName aux of
+  '$' : 'c' : rest -> rest == occNameString (getOccName method)
+  _                -> False
+
+dfunIdSubst :: DFunId -> CoreExpr -> M.HashMap Id (Id, M.HashMap Id Id)
+dfunIdSubst dfunId e = M.fromList $ zip auxIds (repeat (dfunId, methodToAux))
+ where
+  methodToAux = M.fromList
+    [ (m, aux) | m <- methods, aux <- auxIds, aux `isClassOpAuxOf` m ]
+  (_, _, cls, _) = tcSplitDFunTy (idType dfunId)
+  auxIds = filter (isClassOpAuxOccName . getOccName) (exprFreeVarsList e)
+  methods = classAllSelIds cls
+
+inlineAuxExpr :: DFunId -> M.HashMap Id Id -> CoreExpr -> CoreExpr
+inlineAuxExpr dfunId methodToAux e = go e
+ where
+  go :: CoreExpr -> CoreExpr
+  go (Lam b body) = Lam b (go body)
+  go (Let b body)
+    | NonRec x e <- b, isDictId x = go
+    $ substExpr O.empty (extendIdSubst emptySubst x e) body
+    | otherwise = Let (mapBnd go b) (go body)
+  go (Case e x t alts) = Case (go e) x t (fmap (mapAlt go) alts)
+  go (Cast e c       ) = Cast (go e) c
+  go (Tick t e       ) = Tick t (go e)
+  go e
+    | (Var m, args) <- collectArgs e
+    , Just aux <- M.lookup m methodToAux
+    , arg : argsNoTy <- dropWhile isTypeArg args
+    , (Var x, argargs) <- collectArgs arg
+    , x == dfunId
+    = GM.notracePpr ("inlining in" ++ GM.showPpr e)
+      $ mkCoreApps (Var aux) (argargs ++ (go <$> argsNoTy))
+  go (App e0 e1) = App (go e0) (go e1)
+  go e           = e
+
+
+-- modified from Rec.hs
+mapBnd :: (Expr b -> Expr b) -> Bind b -> Bind b
+mapBnd f (NonRec b e) = NonRec b (f e)
+mapBnd f (Rec bs    ) = Rec (map (second f) bs)
+
+mapAlt :: (Expr b -> Expr b) -> (t, t1, Expr b) -> (t, t1, Expr b)
+mapAlt f (d, bs, e) = (d, bs, f e)
diff --git a/src/Language/Haskell/Liquid/Types/Fresh.hs b/src/Language/Haskell/Liquid/Types/Fresh.hs
index d1df82b137..fe9a307b17 100644
--- a/src/Language/Haskell/Liquid/Types/Fresh.hs
+++ b/src/Language/Haskell/Liquid/Types/Fresh.hs
@@ -42,10 +42,10 @@ import           Language.Haskell.Liquid.Types.RefType
 
 class (Applicative m, Monad m) => Freshable m a where
   fresh   :: m a
-  true    :: a -> m a
-  true    = return
-  refresh :: a -> m a
-  refresh = return
+  true    :: Bool -> a -> m a
+  true _  = return
+  refresh :: Bool -> a -> m a
+  refresh _ = return
 
 
 instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Symbol where
@@ -61,15 +61,15 @@ instance (Freshable m Integer, Monad m, Applicative m) => Freshable m [F.Expr] w
 
 instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Reft where
   fresh                  = panic Nothing "fresh Reft"
-  true    (F.Reft (v,_)) = return $ F.Reft (v, mempty)
-  refresh (F.Reft (_,_)) = (F.Reft .) . (,) <$> freshVV <*> fresh
+  true    allowTC (F.Reft (v,_)) = return $ F.Reft (v, mempty)
+  refresh allowTC (F.Reft (_,_)) = (F.Reft .) . (,) <$> freshVV <*> fresh
     where
       freshVV            = F.vv . Just <$> fresh
 
 instance Freshable m Integer => Freshable m RReft where
   fresh             = panic Nothing "fresh RReft"
-  true (MkUReft r _)    = MkUReft <$> true r    <*> return mempty
-  refresh (MkUReft r _) = MkUReft <$> refresh r <*> return mempty
+  true allowTC (MkUReft r _)    = MkUReft <$> true allowTC r    <*> return mempty
+  refresh allowTC (MkUReft r _) = MkUReft <$> refresh allowTC r <*> return mempty
 
 instance (Freshable m Integer, Freshable m r, F.Reftable r ) => Freshable m (RRType r) where
   fresh   = panic Nothing "fresh RefType"
@@ -77,101 +77,101 @@ instance (Freshable m Integer, Freshable m r, F.Reftable r ) => Freshable m (RRT
   true    = trueRefType
 
 -----------------------------------------------------------------------------------------------
-trueRefType :: (Freshable m Integer, Freshable m r, F.Reftable r) => RRType r -> m (RRType r)
+trueRefType :: (Freshable m Integer, Freshable m r, F.Reftable r) => Bool -> RRType r -> m (RRType r)
 -----------------------------------------------------------------------------------------------
-trueRefType (RAllT α t r)
-  = RAllT α <$> true t <*> true r 
+trueRefType allowTC (RAllT α t r)
+  = RAllT α <$> true allowTC t <*> true allowTC r 
 
-trueRefType (RAllP π t)
-  = RAllP π <$> true t
+trueRefType allowTC (RAllP π t)
+  = RAllP π <$> true allowTC t
 
-trueRefType (RImpF _ t t' _)
-  = rImpF <$> fresh <*> true t <*> true t'
+trueRefType allowTC (RImpF _ t t' _)
+  = rImpF <$> fresh <*> true allowTC t <*> true allowTC t'
 
-trueRefType (RFun _ t t' _)
-  = rFun <$> fresh <*> true t <*> true t'
+trueRefType allowTC (RFun _ t t' _)
+  = rFun <$> fresh <*> true allowTC t <*> true allowTC t'
 
-trueRefType (RApp c ts _  _) | isClass c
-  = rRCls c <$> mapM true ts
+trueRefType allowTC (RApp c ts _  _) | if allowTC then isEmbeddedDict c else isClass c
+  = rRCls c <$> mapM (true allowTC) ts
 
-trueRefType (RApp c ts rs r)
-  = RApp c <$> mapM true ts <*> mapM trueRef rs <*> true r
+trueRefType allowTC (RApp c ts rs r)
+  = RApp c <$> mapM (true allowTC) ts <*> mapM (trueRef allowTC) rs <*> true allowTC r
 
-trueRefType (RAppTy t t' _)
-  = RAppTy <$> true t <*> true t' <*> return mempty
+trueRefType allowTC (RAppTy t t' _)
+  = RAppTy <$> true allowTC t <*> true allowTC t' <*> return mempty
 
-trueRefType (RVar a r)
-  = RVar a <$> true r
+trueRefType allowTC (RVar a r)
+  = RVar a <$> true allowTC r
 
-trueRefType (RAllE y ty tx)
+trueRefType allowTC (RAllE y ty tx)
   = do y'  <- fresh
-       ty' <- true ty
-       tx' <- true tx
+       ty' <- true allowTC ty
+       tx' <- true allowTC tx
        return $ RAllE y' ty' (tx' `F.subst1` (y, F.EVar y'))
 
-trueRefType (RRTy e o r t)
-  = RRTy e o r <$> trueRefType t
+trueRefType allowTC (RRTy e o r t)
+  = RRTy e o r <$> trueRefType allowTC t
 
-trueRefType (REx _ t t')
-  = REx <$> fresh <*> true t <*> true t'
+trueRefType allowTC (REx _ t t')
+  = REx <$> fresh <*> true allowTC t <*> true allowTC t'
 
-trueRefType t@(RExprArg _)
+trueRefType allowTC t@(RExprArg _)
   = return t
 
-trueRefType t@(RHole _)
+trueRefType allowTC t@(RHole _)
   = return t
 
 trueRef :: (F.Reftable r, Freshable f r, Freshable f Integer)
-        => Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
-trueRef (RProp _ (RHole _)) = panic Nothing "trueRef: unexpected RProp _ (RHole _))"
-trueRef (RProp s t) = RProp s <$> trueRefType t
+        => Bool -> Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
+trueRef allowTC (RProp _ (RHole _)) = panic Nothing "trueRef: unexpected RProp _ (RHole _))"
+trueRef allowTC (RProp s t) = RProp s <$> trueRefType allowTC t
 
 
 -----------------------------------------------------------------------------------------------
-refreshRefType :: (Freshable m Integer, Freshable m r, F.Reftable r) => RRType r -> m (RRType r)
+refreshRefType :: (Freshable m Integer, Freshable m r, F.Reftable r) => Bool -> RRType r -> m (RRType r)
 -----------------------------------------------------------------------------------------------
-refreshRefType (RAllT α t r)
-  = RAllT α <$> refresh t <*> true r
+refreshRefType allowTC (RAllT α t r)
+  = RAllT α <$> refresh allowTC t <*> true allowTC r
 
-refreshRefType (RAllP π t)
-  = RAllP π <$> refresh t
+refreshRefType allowTC (RAllP π t)
+  = RAllP π <$> refresh allowTC t
 
-refreshRefType (RImpF b t t' _)
-  | b == F.dummySymbol = rImpF <$> fresh <*> refresh t <*> refresh t'
-  | otherwise          = rImpF     b     <$> refresh t <*> refresh t'
+refreshRefType allowTC (RImpF b t t' _)
+  | b == F.dummySymbol = rImpF <$> fresh <*> refresh allowTC t <*> refresh allowTC t'
+  | otherwise          = rImpF     b     <$> refresh allowTC t <*> refresh allowTC t'
 
-refreshRefType (RFun b t t' _)
-  | b == F.dummySymbol = rFun <$> fresh <*> refresh t <*> refresh t'
-  | otherwise          = rFun     b     <$> refresh t <*> refresh t'
+refreshRefType allowTC (RFun b t t' _)
+  | b == F.dummySymbol = rFun <$> fresh <*> refresh allowTC t <*> refresh allowTC t'
+  | otherwise          = rFun     b     <$> refresh allowTC t <*> refresh allowTC t'
 
-refreshRefType (RApp rc ts _ _) | isClass rc
+refreshRefType allowTC (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
+refreshRefType allowTC (RApp rc ts rs r)
+  = RApp rc <$> mapM (refresh allowTC) ts <*> mapM (refreshRef allowTC) rs <*> refresh allowTC r
 
-refreshRefType (RVar a r)
-  = RVar a <$> refresh r
+refreshRefType allowTC (RVar a r)
+  = RVar a <$> refresh allowTC r
 
-refreshRefType (RAppTy t t' r)
-  = RAppTy <$> refresh t <*> refresh t' <*> refresh r
+refreshRefType allowTC (RAppTy t t' r)
+  = RAppTy <$> refresh allowTC t <*> refresh allowTC t' <*> refresh allowTC r
 
-refreshRefType (RAllE y ty tx)
+refreshRefType allowTC (RAllE y ty tx)
   = do y'  <- fresh
-       ty' <- refresh ty
-       tx' <- refresh tx
+       ty' <- refresh allowTC ty
+       tx' <- refresh allowTC tx
        return $ RAllE y' ty' (tx' `F.subst1` (y, F.EVar y'))
 
-refreshRefType (RRTy e o r t)
-  = RRTy e o r <$> refreshRefType t
+refreshRefType allowTC (RRTy e o r t)
+  = RRTy e o r <$> refreshRefType allowTC t
 
-refreshRefType t
+refreshRefType allowTC t
   = return t
 
 refreshRef :: (F.Reftable r, Freshable f r, Freshable f Integer)
-           => Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
-refreshRef (RProp _ (RHole _)) = panic Nothing "refreshRef: unexpected (RProp _ (RHole _))"
-refreshRef (RProp s t) = RProp <$> mapM freshSym s <*> refreshRefType t
+           => Bool -> Ref τ (RType RTyCon RTyVar r) -> f (Ref τ (RRType r))
+refreshRef allowTC (RProp _ (RHole _)) = panic Nothing "refreshRef: unexpected (RProp _ (RHole _))"
+refreshRef allowTC (RProp s t) = RProp <$> mapM freshSym s <*> refreshRefType allowTC t
 
 freshSym :: Freshable f a => (t, t1) -> f (a, t1)
 freshSym (_, t)        = (, t) <$> fresh
@@ -268,20 +268,20 @@ refreshPs = mapPropM go
 
 --------------------------------------------------------------------------------
 refreshHoles :: (F.Symbolic t, F.Reftable r, TyConable c, Freshable f r)
-             => [(t, RType c tv r)] -> f ([F.Symbol], [(t, RType c tv r)])
-refreshHoles vts = first catMaybes . unzip . map extract <$> mapM refreshHoles' vts
+             => Bool -> [(t, RType c tv r)] -> f ([F.Symbol], [(t, RType c tv r)])
+refreshHoles allowTC vts = first catMaybes . unzip . map extract <$> mapM (refreshHoles' allowTC) vts
   where
   --   extract :: (t, t1, t2) -> (t, (t1, t2))
     extract (a,b,c) = (a,(b,c))
 
 refreshHoles' :: (F.Symbolic a, F.Reftable r, TyConable c, Freshable m r)
-              => (a, RType c tv r) -> m (Maybe F.Symbol, a, RType c tv r)
-refreshHoles' (x,t)
+              => Bool -> (a, RType c tv r) -> m (Maybe F.Symbol, a, RType c tv r)
+refreshHoles' allowTC (x,t)
   | noHoles t = return (Nothing, x, t)
   | otherwise = (Just $ F.symbol x,x,) <$> mapReftM tx t
   where
-    tx r | hasHole r = refresh r
+    tx r | hasHole r = refresh allowTC r
          | otherwise = return r
 
 noHoles :: (F.Reftable r, TyConable c) => RType c tv r -> Bool
-noHoles = and . foldReft False (\_ r bs -> not (hasHole r) : bs) []
+noHoles = and . foldReft (const False) False (\_ r bs -> not (hasHole r) : bs) []
diff --git a/src/Language/Haskell/Liquid/Types/PredType.hs b/src/Language/Haskell/Liquid/Types/PredType.hs
index 5e67dd40de..766f421003 100644
--- a/src/Language/Haskell/Liquid/Types/PredType.hs
+++ b/src/Language/Haskell/Liquid/Types/PredType.hs
@@ -84,13 +84,13 @@ mkRTyCon (TyConP _ tc αs' ps tyvariance predvariance size)
 --   a (refined) data constructor into a @SpecType@ for that constructor.
 --   TODO: duplicated with Liquid.Measure.makeDataConType
 -------------------------------------------------------------------------------
-dataConPSpecType :: DataConP -> [(Var, SpecType)]
+dataConPSpecType :: Bool -> DataConP -> [(Var, SpecType)]
 -------------------------------------------------------------------------------
-dataConPSpecType dcp    = [(workX, workT), (wrapX, wrapT) ]
+dataConPSpecType allowTC dcp    = [(workX, workT), (wrapX, wrapT) ]
   where
     workT | isVanilla   = wrapT
           | otherwise   = dcWorkSpecType   dc wrapT
-    wrapT               = dcWrapSpecType   dc dcp
+    wrapT               = dcWrapSpecType   allowTC  dc dcp
     workX               = dataConWorkId    dc            -- This is the weird one for GADTs
     wrapX               = dataConWrapId    dc            -- This is what the user expects to see
     isVanilla           = isVanillaDataCon dc
@@ -165,16 +165,20 @@ meetWorkWrapRep c workR wrapR
 strengthenRType :: SpecType -> SpecType -> SpecType
 strengthenRType wkT wrT = maybe wkT (strengthen wkT) (stripRTypeBase wrT)
 
-dcWrapSpecType :: DataCon -> DataConP -> SpecType
-dcWrapSpecType dc (DataConP _ _ vs ps cs yts rt _ _ _)
+
+-- maybe a tc flag is unnecessary but I don't know if {-@ class ... @-}
+-- would reach here
+dcWrapSpecType :: Bool -> DataCon -> DataConP -> SpecType
+dcWrapSpecType allowTC dc (DataConP _ _ vs ps cs yts rt _ _ _)
   = {- F.tracepp ("dcWrapSpecType: " ++ show dc ++ " " ++ F.showpp rt) $ -}
     mkArrow makeVars' ps [] ts' rt'
   where
+    isCls    = Ghc.isClassTyCon $ Ghc.dataConTyCon dc
     (xs, ts) = unzip (reverse yts)
     mkDSym z = (F.symbol z) `F.suffixSymbol` (F.symbol dc)
     ys       = mkDSym <$> xs
     tx _  []     []     []     = []
-    tx su (x:xs) (y:ys) (t:ts) = (y, F.subst (F.mkSubst su) t, mempty)
+    tx su (x:xs) (y:ys) (t:ts) = (y, if allowTC && isCls then t else F.subst (F.mkSubst su) t, mempty)
                                : tx ((x, F.EVar y):su) xs ys ts
     tx _ _ _ _ = panic Nothing "PredType.dataConPSpecType.tx called on invalid inputs"
     yts'     = tx [] xs ys ts
@@ -388,7 +392,7 @@ substRCon msg (_, RProp ss t1@(RApp c1 ts1 rs1 r1)) t2@(RApp c2 ts2 rs2 _) πs r
 
     su = F.mkSubst $ zipWith (\s1 s2 -> (s1, F.EVar s2)) (rvs t1) (rvs t2)
 
-    rvs      = foldReft False (\_ r acc -> rvReft r : acc) []
+    rvs      = foldReft (const False) False (\_ r acc -> rvReft r : acc) [] 
     rvReft r = let F.Reft(s,_) = F.toReft r in s
 
 substRCon msg su t _ _        = {- panic Nothing -} errorP "substRCon: " $ msg ++ " " ++ showpp (su, t)
diff --git a/src/Language/Haskell/Liquid/Types/RefType.hs b/src/Language/Haskell/Liquid/Types/RefType.hs
index fbdadf4b60..c438737d4a 100644
--- a/src/Language/Haskell/Liquid/Types/RefType.hs
+++ b/src/Language/Haskell/Liquid/Types/RefType.hs
@@ -1672,7 +1672,7 @@ grabArgs τs τ
   = reverse (τ:τs)
 
 isNonValueTy :: Type -> Bool
-isNonValueTy = GM.isPredType
+isNonValueTy = GM.isEmbeddedDictType -- GM.isPredType
 
 
 expandProductType :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r))
diff --git a/src/Language/Haskell/Liquid/Types/Types.hs b/src/Language/Haskell/Liquid/Types/Types.hs
index 7c2f488c32..1e7c112eea 100644
--- a/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/src/Language/Haskell/Liquid/Types/Types.hs
@@ -54,7 +54,7 @@ module Language.Haskell.Liquid.Types.Types (
   , rTyConPVs
   , rTyConPropVs
   -- , isClassRTyCon
-  , isClassType, isEqType, isRVar, isBool
+  , isClassType, isEqType, isRVar, isBool, isEmbeddedClass
 
   -- * Refinement Types
   , RType (..), Ref(..), RTProp, rPropP
@@ -641,6 +641,10 @@ isClassType :: TyConable c => RType c t t1 -> Bool
 isClassType (RApp c _ _ _) = isClass c
 isClassType _              = False
 
+isEmbeddedClass :: TyConable c => RType c t t1 -> Bool
+isEmbeddedClass (RApp c _ _ _) = isEmbeddedDict c
+isEmbeddedClass _              = False
+
 -- rTyConPVHPs = filter isHPropPV . rtc_pvars
 -- isHPropPV   = not . isPropPV
 
@@ -926,12 +930,18 @@ class (Eq c) => TyConable c where
   isTuple  :: c -> Bool
   ppTycon  :: c -> Doc
   isClass  :: c -> Bool
+  isEmbeddedDict :: c -> Bool
   isEqual  :: c -> Bool
+  isOrdCls  :: c -> Bool
+  isEqCls   :: c -> Bool
 
   isNumCls  :: c -> Bool
   isFracCls :: c -> Bool
 
   isClass   = const False
+  isEmbeddedDict c = isNumCls c || isEqual c || isOrdCls c || isEqCls c
+  isOrdCls  = const False
+  isEqCls   = const False
   isEqual   = const False
   isNumCls  = const False
   isFracCls = const False
@@ -963,6 +973,8 @@ instance TyConable RTyCon where
                 (tyConClass_maybe $ rtc_tc c)
   isFracCls c = maybe False (isClassOrSubClass isFractionalClass)
                 (tyConClass_maybe $ rtc_tc c)
+  isOrdCls  c = maybe False isOrdClass (tyConClass_maybe $ rtc_tc c)
+  isEqCls   c = isEqCls (rtc_tc c)
 
 
 instance TyConable TyCon where
@@ -977,7 +989,9 @@ instance TyConable TyCon where
                 (tyConClass_maybe $ c)
   isFracCls c = maybe False (isClassOrSubClass isFractionalClass)
                 (tyConClass_maybe $ c)
-
+  isOrdCls c  = maybe False isOrdClass
+                (tyConClass_maybe c)
+  isEqCls  c  = isPrelEqTyCon c
 
 isClassOrSubClass :: (Class -> Bool) -> Class -> Bool
 isClassOrSubClass p cls
@@ -1471,7 +1485,7 @@ instance (F.Reftable r, TyConable c) => F.Subable (RTProp c tv r) where
 
 
 instance (F.Subable r, F.Reftable r, TyConable c) => F.Subable (RType c tv r) where
-  syms        = foldReft False (\_ r acc -> F.syms r ++ acc) []
+  syms        = foldReft (const False) False (\_ r acc -> F.syms r ++ acc) []
   -- 'substa' will substitute bound vars
   substa f    = emapExprArg (\_ -> F.substa f) []      . mapReft  (F.substa f)
   -- 'substf' will NOT substitute bound vars
@@ -1514,8 +1528,10 @@ mapExprReft f = mapReft g
   where
     g (MkUReft (F.Reft (x, e)) p) = MkUReft (F.Reft (x, f x e)) p
 
+-- const False (not dropping dict) is probably fine since there will not be refinement on
+-- dictionaries
 isTrivial :: (F.Reftable r, TyConable c) => RType c tv r -> Bool
-isTrivial t = foldReft False (\_ r b -> F.isTauto r && b) True t
+isTrivial t = foldReft (const False) False (\_ r b -> F.isTauto r && b) True t
 
 mapReft ::  (r1 -> r2) -> RType c tv r1 -> RType c tv r2
 mapReft f = emapReft (const f) []
@@ -1660,20 +1676,21 @@ mapPropM f (RRTy xts r o t)   = liftM4  RRTy (mapM (mapSndM (mapPropM f)) xts) (
 -- foldReft f = efoldReft (\_ _ -> []) (\_ -> ()) (\_ _ -> f) (\_ γ -> γ) emptyF.SEnv
 
 --------------------------------------------------------------------------------
-foldReft :: (F.Reftable r, TyConable c) => BScope -> (F.SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
+foldReft :: (F.Reftable r, TyConable c) => (c -> Bool) -> BScope -> (F.SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
 --------------------------------------------------------------------------------
-foldReft  bsc f = foldReft' (\_ _ -> False) bsc id (\γ _ -> f γ)
+foldReft isErasable bsc f = foldReft' isErasable (\_ _ -> False) bsc id (\γ _ -> f γ)
 
 --------------------------------------------------------------------------------
 foldReft' :: (F.Reftable r, TyConable c)
-          => (Symbol -> RType c tv r -> Bool)
+          => (c -> Bool)
+          -> (Symbol -> RType c tv r -> Bool)
           -> BScope
           -> (RType c tv r -> b)
           -> (F.SEnv b -> Maybe (RType c tv r) -> r -> a -> a)
           -> a -> RType c tv r -> a
 --------------------------------------------------------------------------------
-foldReft' logicBind bsc g f 
-  = efoldReft logicBind bsc 
+foldReft' isErasable logicBind bsc g f 
+  = efoldReft isErasable logicBind bsc 
               (\_ _ -> [])
               (\_ -> [])
               g
@@ -1685,7 +1702,8 @@ foldReft' logicBind bsc g f
 
 -- efoldReft :: F.Reftable r =>(p -> [RType c tv r] -> [(Symbol, a)])-> (RType c tv r -> a)-> (SEnv a -> Maybe (RType c tv r) -> r -> c1 -> c1)-> SEnv a-> c1-> RType c tv r-> c1
 efoldReft :: (F.Reftable r, TyConable c)
-          => (Symbol -> RType c tv r -> Bool)
+          => (c -> Bool) -- ^ Determines which type constructors should be erased.
+          -> (Symbol -> RType c tv r -> Bool)
           -> BScope
           -> (c  -> [RType c tv r] -> [(Symbol, a)])
           -> (RTVar tv (RType c tv ()) -> [(Symbol, a)])
@@ -1696,7 +1714,7 @@ efoldReft :: (F.Reftable r, TyConable c)
           -> b
           -> RType c tv r
           -> b
-efoldReft logicBind bsc cb dty g f fp = go
+efoldReft isErasable logicBind bsc cb dty g f fp = go
   where
     -- folding over RType
     go γ z me@(RVar _ r)                = f γ (Just me) r z
@@ -1706,7 +1724,7 @@ efoldReft logicBind bsc cb dty g f fp = go
     go γ z (RAllP p t)                  = go (fp p γ) z t
     go γ z (RImpF x t t' r)             = go γ z (RFun x t t' r)
     go γ z me@(RFun _ (RApp c ts _ _) t' r)
-       | isClass c                      = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t')
+       | isErasable c               = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t')
     go γ z me@(RFun x t t' r)
        | logicBind x t                  = f γ (Just me) r (go γ' (go γ z t) t')
        | otherwise                      = f γ (Just me) r (go γ  (go γ z t) t')
diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs
index 689a686772..d86424fe90 100644
--- a/src/Language/Haskell/Liquid/UX/CmdLine.hs
+++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs
@@ -367,6 +367,10 @@ config = cmdArgsMode $ Config {
     = def 
         &= name "typed-holes"
         &= help "Use (refinement) typed-holes [currently warns on '_x' variables]"
+  , typeclass
+    = def
+        &= help "Enable Typeclass"
+        &= name "typeclass"
   } &= verbosity
     &= program "liquid"
     &= help    "Refinement Types for Haskell"
@@ -600,6 +604,7 @@ defConfig = Config
   , compileSpec       = False
   , noCheckImports    = False
   , typedHoles        = False
+  , typeclass         = False
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Language/Haskell/Liquid/UX/Config.hs b/src/Language/Haskell/Liquid/UX/Config.hs
index 4fe67854aa..406cd83050 100644
--- a/src/Language/Haskell/Liquid/UX/Config.hs
+++ b/src/Language/Haskell/Liquid/UX/Config.hs
@@ -93,6 +93,7 @@ data Config = Config
   , compileSpec     :: Bool        -- ^ Only "compile" the spec -- into .bspec file -- don't do any checking. 
   , noCheckImports  :: Bool        -- ^ Do not check the transitive imports  
   , typedHoles      :: Bool        -- ^ Warn about "typed-holes"
+  , typeclass       :: Bool        -- ^ enable typeclass support.
   } deriving (Generic, Data, Typeable, Show, Eq)
 
 instance Serialize SMTSolver
diff --git a/tests/pos/T1669.hs b/tests/pos/T1669.hs
new file mode 100644
index 0000000000..9aa043108a
--- /dev/null
+++ b/tests/pos/T1669.hs
@@ -0,0 +1,29 @@
+{-@ LIQUID "--reflection" @-}
+{-@ LIQUID "--ple" @-}
+{-@ LIQUID "--no-totality" @-}
+
+module A where
+import           Prelude                 hiding ( Semigroup
+                                                , mappend
+                                                )
+
+data PNat = Z | S PNat
+
+{-@ data Semigroup a = CSemigroup {mappend :: a -> a -> a} @-}
+data Semigroup a = CSemigroup {mappend :: a -> a -> a}
+
+{-@ reflect cmappend  @-}
+cmappend :: PNat -> PNat -> PNat
+cmappend Z     n = n
+cmappend (S m) n = S (cmappend m n)
+
+{-@ reflect semigroupPNat  @-}
+semigroupPNat :: Semigroup PNat
+semigroupPNat = CSemigroup cmappend
+
+
+{-@ clawAssociative :: v:PNat -> v':PNat -> v'':PNat  
+  -> { mappend semigroupPNat (mappend semigroupPNat v v') v'' == mappend semigroupPNat v (mappend semigroupPNat v' v'')}@-}
+clawAssociative :: PNat -> PNat -> PNat -> ()
+clawAssociative Z     _ _ = ()
+-- clawAssociative (S p) m n = clawAssociative p m n
diff --git a/tests/pos/T1670A.hs b/tests/pos/T1670A.hs
new file mode 100644
index 0000000000..aca389722c
--- /dev/null
+++ b/tests/pos/T1670A.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE TypeFamilies #-}
+{-@ LIQUID "--reflection" @-}
+{-@ LIQUID "--ple" @-}
+
+module B where
+
+data LWW t a = LWW {
+    lwwTime  :: t
+  , lwwValue :: a
+  }
+
+{-@ reflect cenabledLWW @-}
+cenabledLWW :: Ord t => LWW t a -> LWW t a -> Bool
+cenabledLWW (LWW t1 _) (LWW t2 _) = t1 /= t2
+
+
+{-@ reflect capplyLWW @-}
+capplyLWW :: Ord t => LWW t a -> LWW t a -> LWW t a
+capplyLWW l1@(LWW t1 _) l2@(LWW t2 _) 
+     | t1 > t2   = l1
+     | otherwise = l2
+
+{-@ clawCommutativityLWW :: Ord t => x : (LWW t a) -> op1 : LWW t a -> op2 : LWW t a -> {(cenabledLWW x op1 && cenabledLWW x op2  && cenabledLWW (capplyLWW x op1) op2 && cenabledLWW (capplyLWW x op2) op1) => capplyLWW (capplyLWW x op1) op2 == capplyLWW (capplyLWW x op2) op1} @-}
+clawCommutativityLWW :: Ord t => LWW t a -> LWW t a -> LWW t a -> ()
+clawCommutativityLWW x@(LWW t0 v0) op1@(LWW t1 v1) op2@(LWW t2 v2) = ()
\ No newline at end of file
diff --git a/tests/pos/T1670B.hs b/tests/pos/T1670B.hs
new file mode 100644
index 0000000000..1cfbd6ecab
--- /dev/null
+++ b/tests/pos/T1670B.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE TypeFamilies #-}
+
+{-@ LIQUID "--reflection" @-}
+{-@ LIQUID "--ple" @-}
+
+module B where
+
+data LWW t a = LWW {
+    lwwTime  :: t
+  , lwwValue :: a
+  }
+
+type family Operation t
+
+type instance Operation (LWW t a) = LWW t a
+
+{-@ reflect cenabledLWW @-}
+cenabledLWW :: Ord t => LWW t a -> Operation (LWW t a) -> Bool
+cenabledLWW (LWW t1 _) (LWW t2 _) = t1 /= t2
+
+
+{-@ reflect capplyLWW @-}
+capplyLWW :: Ord t => LWW t a -> Operation (LWW t a) -> LWW t a
+capplyLWW l1@(LWW t1 _) l2@(LWW t2 _) 
+     | t1 > t2   = l1
+     | otherwise = l2
+
+{-@ clawCommutativityLWW :: Ord t => x : (LWW t a) -> op1 : Operation (LWW t a) -> op2 : Operation (LWW t a) -> {(cenabledLWW x op1 && cenabledLWW x op2  && cenabledLWW (capplyLWW x op1) op2 && cenabledLWW (capplyLWW x op2) op1) => capplyLWW (capplyLWW x op1) op2 == capplyLWW (capplyLWW x op2) op1} @-}
+clawCommutativityLWW :: Ord t => LWW t a -> Operation (LWW t a) -> Operation (LWW t a) -> ()
+clawCommutativityLWW x@(LWW t0 v0) op1@(LWW t1 v1) op2@(LWW t2 v2) = ()
\ No newline at end of file