diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal
--- a/liquidhaskell.cabal
+++ b/liquidhaskell.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               liquidhaskell
-version:            0.8.10.1
+version:            0.8.10.2
 synopsis:           Liquid Types for Haskell
 description:        Liquid Types for Haskell.
 license:            BSD-3-Clause
@@ -224,9 +224,10 @@
                     , gitrev
                     , hashable             >= 1.3
                     , hscolour             >= 1.22
-                    , liquid-fixpoint      >= 0.8.0.0
+                    , liquid-fixpoint      >= 0.8.10.1
                     , mtl                  >= 2.1
                     , optics               >= 0.2
+                    , optparse-applicative < 0.16.0.0
                     , optparse-simple
                     , githash
                     , parsec               >= 3.1
@@ -297,7 +298,7 @@
   other-modules:    Paths_liquidhaskell
   hs-source-dirs:   tests
   build-depends:    base            >= 4.8.1.0 && < 5
-                  , liquid-fixpoint >= 0.8.0.0
+                  , liquid-fixpoint >= 0.8.10.1
                   , liquidhaskell
                   , parsec
                   , syb
@@ -313,7 +314,7 @@
   other-modules:    Paths_liquidhaskell
   hs-source-dirs:   tests
   build-depends:    base            >= 4.8.1.0 && < 5
-                  , liquid-fixpoint >= 0.8.0.0
+                  , liquid-fixpoint >= 0.8.10.1
                   , liquidhaskell
                   , tasty           >= 0.7
                   , tasty-hunit
diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs
--- a/src/Language/Haskell/Liquid/Constraint/Generate.hs
+++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs
@@ -437,14 +437,15 @@
 consCB _ _ γ (NonRec x def)
   | Just (w, τ) <- grepDictionary def
   , Just d      <- dlookup (denv γ) w
-  = do t        <- trueTy τ
-       addW      $ WfC γ t
+  = do t        <- mapM trueTy τ
+       mapM addW (WfC γ <$> t)
        let xts   = dmap (fmap (f t)) d
        let  γ'   = γ { denv = dinsert (denv γ) x xts }
        t        <- trueTy (varType x)
        extender γ' (x, Assumed t)
    where
-    f t' (RAllT α te _) = subsTyVar_meet' (ty_var_value α, t') te
+    f [t']    (RAllT α te _) = subsTyVar_meet' (ty_var_value α, t') te
+    f (t':ts) (RAllT α te _) = f ts $ subsTyVar_meet' (ty_var_value α, t') te
     f _ _ = impossible Nothing "consCB on Dictionary: this should not happen"
 
 consCB _ _ γ (NonRec x e)
@@ -452,10 +453,13 @@
        to' <- consBind False γ (x, e, to) >>= (addPostTemplate γ)
        extender γ (x, makeSingleton γ (simplify e) <$> to')
 
-grepDictionary :: CoreExpr -> Maybe (Var, Type)
-grepDictionary (App (Var w) (Type t)) = Just (w, t)
-grepDictionary (App e (Var _))        = grepDictionary e
-grepDictionary _                      = Nothing
+grepDictionary :: CoreExpr -> Maybe (Var, [Type])
+grepDictionary = go [] 
+  where 
+    go ts (App (Var w) (Type t)) = Just (w, reverse (t:ts))
+    go ts (App e (Type t))       = go (t:ts) e
+    go ts (App e (Var _))        = go ts e
+    go _ _                       = Nothing
 
 --------------------------------------------------------------------------------
 consBind :: Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)
@@ -1448,14 +1452,13 @@
 
 -- | @isGenericVar@ determines whether the @RTyVar@ has no class constraints
 isGenericVar :: RTyVar -> SpecType -> Bool
-isGenericVar α t =  all (\(c, α') -> (α'/=α) || isOrd c || isEq c ) (classConstrs t)
+isGenericVar α t =  all (\(c, α') -> (α'/=α) || isGenericClass c ) (classConstrs t)
   where 
     classConstrs t = [(c, ty_var_value α')
                         | (c, ts) <- tyClasses t
                         , t'      <- ts
                         , α'      <- freeTyVars t']
-    isOrd          = (ordClassName ==) . className
-    isEq           = (eqClassName ==) . className
+    isGenericClass c = className c `elem` [ordClassName, eqClassName] -- , functorClassName, monadClassName]
 
 -- instance MonadFail CG where 
 --  fail msg = panic Nothing msg
diff --git a/tests/pos/T1697.hs b/tests/pos/T1697.hs
new file mode 100644
--- /dev/null
+++ b/tests/pos/T1697.hs
@@ -0,0 +1,58 @@
+{-@ LIQUID "--no-pattern-inline" @-}
+
+module B where
+
+data User = U
+
+{-@ measure currentUser :: User @-}
+
+{-@ data TaggedT user m a <label :: user -> Bool, clear :: user -> Bool> = TaggedT _ @-}
+data TaggedT user m a = TaggedT { unTag :: m a }
+{-@ data variance TaggedT invariant invariant covariant contravariant covariant @-}
+
+instance Functor m => Functor (TaggedT user m) where
+  fmap f = TaggedT . fmap f . unTag
+
+instance Applicative m => Applicative (TaggedT user m) where
+  pure = TaggedT . pure
+  f <*> x = TaggedT $ unTag f <*> unTag x
+
+{-@
+instance Monad m => Monad (TaggedT user m) where
+  >>= :: forall < p :: user -> Bool
+                , q :: user -> Bool
+                , r :: user -> Bool
+                , s :: user -> Bool
+                , t :: user -> Bool
+                , u :: user -> Bool
+                , rx :: a -> Bool
+                , rf :: a -> b -> Bool
+                , ro :: b -> Bool
+                >.
+    {content :: a<rx> |- b<rf content> <: b<ro>}
+    {content :: a<rx> |- b<ro> <: b<rf content>}
+    {{v : (user<s>) | True} <: {v : (user<p>) | True}}
+    {{v : (user<t>) | True} <: {v : (user<p>) | True}}
+    {{v : (user<t>) | True} <: {v : (user<r>) | True}}
+    {{v : (user<q>) | True} <: {v : (user<u>) | True}}
+    {{v : (user<s>) | True} <: {v : (user<u>) | True}}
+    x:TaggedT<p, q> user m (a<rx>)
+    -> (y:a -> TaggedT<r, s> user m (b<rf y>))
+    -> TaggedT<t, u> user m (b<ro>);
+
+  return :: a -> TaggedT<{\_ -> True}, {\_ -> False}> user m a
+@-}
+instance Monad m =>  Monad (TaggedT user m) where
+  x >>= f = TaggedT $ unTag x >>= \y -> unTag (f y)
+  
+-------------------------------------------------------------------------------------------
+-- | Test
+-------------------------------------------------------------------------------------------
+
+{-@ assume respondT :: String -> TaggedT<{\_ -> True}, {\v -> v == currentUser}> User m () @-}
+respondT :: String -> TaggedT User m ()
+respondT = undefined
+
+{-@ test :: TaggedT<{\_ -> True}, {\v -> v == currentUser}> User m () @-}
+test :: Monad m => TaggedT User m ()
+test = return "a" >>= respondT
diff --git a/tests/pos/T1697A.hs b/tests/pos/T1697A.hs
new file mode 100644
--- /dev/null
+++ b/tests/pos/T1697A.hs
@@ -0,0 +1,60 @@
+-------------------------------------------------------------------------------------------
+-- | Fixed User (WORKING)
+-------------------------------------------------------------------------------------------
+
+module A where
+
+data User = U
+
+{-@ measure currentUser :: User @-}
+
+{-@ data TaggedT m a <label :: User -> Bool, clear :: User -> Bool> = TaggedT _ @-}
+data TaggedT m a = TaggedT { unTag :: m a }
+{-@ data variance TaggedT invariant covariant contravariant covariant @-}
+
+instance Functor m => Functor (TaggedT m) where
+  fmap f = TaggedT . fmap f . unTag
+
+instance Applicative m => Applicative (TaggedT m) where
+  pure = TaggedT . pure
+  f <*> x = TaggedT $ unTag f <*> unTag x
+
+{-@
+instance Monad m => Monad (TaggedT m) where
+  >>= :: forall < p :: User -> Bool
+                , q :: User -> Bool
+                , r :: User -> Bool
+                , s :: User -> Bool
+                , t :: User -> Bool
+                , u :: User -> Bool
+                , rx :: a -> Bool
+                , rf :: a -> b -> Bool
+                , ro :: b -> Bool
+                >.
+    {content :: a<rx> |- b<rf content> <: b<ro>}
+    {content :: a<rx> |- b<ro> <: b<rf content>}
+    {{v : (User<s>) | True} <: {v : (User<p>) | True}}
+    {{v : (User<t>) | True} <: {v : (User<p>) | True}}
+    {{v : (User<t>) | True} <: {v : (User<r>) | True}}
+    {{v : (User<q>) | True} <: {v : (User<u>) | True}}
+    {{v : (User<s>) | True} <: {v : (User<u>) | True}}
+    x:TaggedT<p, q> m (a<rx>)
+    -> (y:a -> TaggedT<r, s> m (b<rf y>))
+    -> TaggedT<t, u> m (b<ro>);
+
+  return :: a -> TaggedT<{\_ -> True}, {\_ -> False}> m a
+@-}
+instance Monad m => Monad (TaggedT m) where
+  x >>= f = TaggedT $ unTag x >>= \y -> unTag (f y)
+  
+-------------------------------------------------------------------------------------------
+-- | Test
+-------------------------------------------------------------------------------------------
+
+{-@ assume respondT :: String -> TaggedT<{\_ -> True}, {\v -> v == currentUser}> m () @-}
+respondT :: String -> TaggedT m ()
+respondT = undefined
+
+{-@ test :: TaggedT<{\_ -> True}, {\v -> v == currentUser}> m () @-}
+test :: Monad m => TaggedT m ()
+test = return "a" >>= respondT
diff --git a/tests/pos/T1697C.hs b/tests/pos/T1697C.hs
new file mode 100644
--- /dev/null
+++ b/tests/pos/T1697C.hs
@@ -0,0 +1,54 @@
+-------------------------------------------------------------------------------------------
+-- | Polymorphic user but defining bind and return as normal functions (WORKING)
+-------------------------------------------------------------------------------------------
+
+module C where
+
+data User = U
+
+{-@ measure currentUser :: User @-}
+
+{-@ data TaggedT user m a <label :: user -> Bool, clear :: user -> Bool> = TaggedT _ @-}
+data TaggedT user m a = TaggedT { unTag :: m a }
+{-@ data variance TaggedT invariant invariant covariant contravariant covariant @-}
+
+{-@
+assume bindT :: forall < p :: user -> Bool
+                       , q :: user -> Bool
+                       , r :: user -> Bool
+                       , s :: user -> Bool
+                       , t :: user -> Bool
+                       , u :: user -> Bool
+                       , rx :: a -> Bool
+                       , rf :: a -> b -> Bool
+                       , ro :: b -> Bool
+                       >.
+    {content :: a<rx> |- b<rf content> <: b<ro>}
+    {content :: a<rx> |- b<ro> <: b<rf content>}
+    {{v : (user<s>) | True} <: {v : (user<p>) | True}}
+    {{v : (user<t>) | True} <: {v : (user<p>) | True}}
+    {{v : (user<t>) | True} <: {v : (user<r>) | True}}
+    {{v : (user<q>) | True} <: {v : (user<u>) | True}}
+    {{v : (user<s>) | True} <: {v : (user<u>) | True}}
+    x:TaggedT<p, q> user m (a<rx>)
+    -> (y:a -> TaggedT<r, s> user m (b<rf y>))
+    -> TaggedT<t, u> user m (b<ro>)
+@-}
+bindT :: Monad m => TaggedT user m a -> (a -> TaggedT user m b) -> TaggedT user m b
+bindT x f = TaggedT $ unTag x >>= \y -> unTag (f y)
+
+{-@ assume returnT :: a -> TaggedT<{\_ -> True}, {\_ -> False}> user m a @-}
+returnT :: Monad m => a -> TaggedT user m a
+returnT x = TaggedT (return x)
+
+-------------------------------------------------------------------------------------------
+-- | Test
+-------------------------------------------------------------------------------------------
+
+{-@ assume respondT :: String -> TaggedT<{\_ -> True}, {\v -> v == currentUser}> User m () @-}
+respondT :: String -> TaggedT User m ()
+respondT = undefined
+
+{-@ test :: TaggedT<{\_ -> True}, {\v -> v == currentUser}> User m () @-}
+test :: Monad m => TaggedT User m ()
+test = returnT "a" `bindT` respondT
diff --git a/tests/test.hs b/tests/test.hs
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -313,7 +313,8 @@
 
 benchTests :: IO TestTree
 benchTests = group "Benchmarks"
-  [ testGroup "esop"        <$> dirTests  "benchmarks/esop2013-submission"        esopIgnored               ExitSuccess
+  [ testGroup "cse230"      <$> dirTests   "benchmarks/cse230/src/Week10"         []                        ExitSuccess
+  , testGroup "esop"        <$> dirTests   "benchmarks/esop2013-submission"       esopIgnored               ExitSuccess
   , testGroup "vect-algs"   <$> odirTests  "benchmarks/vector-algorithms-0.5.4.2" []            vectOrder   ExitSuccess
   , testGroup "bytestring"  <$> odirTests  "benchmarks/bytestring-0.9.2.1"        bsIgnored     bsOrder     ExitSuccess
   , testGroup "text"        <$> odirTests  "benchmarks/text-0.11.2.3"             textIgnored   textOrder   ExitSuccess