diff --git a/src/Base/Types.hs b/src/Base/Types.hs
index e828377fdd491d358476713e6c189b890d28b498..ee15bb216ce41cfc741ee2a0a75edc4721e582f9 100644
--- a/src/Base/Types.hs
+++ b/src/Base/Types.hs
@@ -32,6 +32,7 @@ module Base.Types
   , emptyPredSet, partitionPredSet, minPredSet, maxPredSet, qualifyPredSet
   , unqualifyPredSet
   , unpredType
+  , predSet
     -- * Representation of data constructors
   , DataConstr (..)
   , constrIdent, constrTypes, recLabels, recLabelTypes, tupleData
@@ -312,6 +313,12 @@ unpredType :: Type -> Type
 unpredType (TypeContext _ ty) = ty
 unpredType ty                 = ty
 
+-- | Returns the predicate set in the beginning of the given type.
+predSet :: Type -> PredSet
+predSet (TypeContext ps ty) = Set.union ps (predSet ty)
+predSet (TypeForall _ ty)   = predSet ty
+predSet _                   = emptyPredSet
+
 -- -----------------------------------------------------------------------------
 -- Data constructors
 -- -----------------------------------------------------------------------------
diff --git a/src/Checks/TypeCheck.hs b/src/Checks/TypeCheck.hs
index f2bd9fed840b74086d308357dbf81ac17bf0fa19..eb3a6bbb533212cd397856bcfeb0d1f0603f6f47 100644
--- a/src/Checks/TypeCheck.hs
+++ b/src/Checks/TypeCheck.hs
@@ -5,7 +5,7 @@ Copyright   : (c) 1999–2004 Wolfgang Lux, Martin Engelke
                   2011–2015 Björn Peemöller
                   2014–2015 Jan Tikovsky
                   2016–2017 Finn Teegen
-                  2019 Jan-Hendrik Matthes
+                  2019–2020 Jan-Hendrik Matthes
 License     : BSD-3-Clause
 
 Maintainer  : fte@informatik.uni-kiel.de
@@ -49,12 +49,11 @@ import           Prelude             hiding ((<>))
 #if __GLASGOW_HASKELL__ < 710
 import           Control.Applicative ((<$>), (<*>))
 #endif
+import           Control.Monad.Extra (allM, eitherM, filterM, foldM, notM,
+                                      replicateM, unless, unlessM, when, (&&^))
+import qualified Control.Monad.State as S (State, StateT, evalStateT, get, gets,
+                                           modify, put, runState)
 import           Control.Monad.Trans (lift)
-import           Control.Monad.Extra (allM, eitherM, filterM, foldM, (&&^),
-                                      notM, replicateM, when, unless, unlessM)
-import qualified Control.Monad.State as S
-                                     (State, StateT, get, gets, put, modify,
-                                      runState, evalStateT)
 import           Data.Foldable       (foldrM)
 import           Data.Function       (on)
 import           Data.List           (nub, nubBy, partition, sortBy, (\\))
@@ -63,7 +62,7 @@ import           Data.Maybe          (fromJust, isJust)
 import qualified Data.Set.Extra      as Set (Set, concatMap, deleteMin, empty,
                                              filter, fromList, insert,
                                              isSubsetOf, map, member, notMember,
-                                             partition, singleton, toList,
+                                             null, partition, singleton, toList,
                                              union, unions)
 
 import           Curry.Base.Ident
@@ -1393,8 +1392,14 @@ tcExpr cm    p (Case spi li ct e as) = do
 
 tcArg :: HasPosition p => CheckMode -> p -> String -> Doc -> PredSet -> Type
       -> Expression a -> TCM (PredSet, Expression Type)
-tcArg cm p what doc ps ty e =
-  tcExpr cm p e >>- unify p what (doc $-$ text "Term:" <+> pPrintPrec 0 e) ps ty
+tcArg cm p what doc ps ty e = do
+  (ps', ty', expr) <- tcExpr cm p e
+  ps'' <- unify p what (doc $-$ text "Term:" <+> pPrintPrec 0 e) ps ty ps' ty'
+  let expr' = if Set.null (predSet ty) then expr else updateType ps' expr
+  return (ps'', expr')
+  where
+    updateType preds (Variable spi t v) = Variable spi (TypeContext preds t) v
+    updateType _     e                  = e
 
 tcAlt :: CheckMode -> Type -> Type -> PredSet -> Alt a
       -> TCM (PredSet, Alt Type)
@@ -1582,11 +1587,15 @@ unifyHelp b p what doc ps1 ty1 ps2 ty2 = do
     Left reason -> report $ errTypeMismatch p what doc m ty1' ty2' reason
     Right sigma -> modifyTypeSubst (compose sigma)
   theta' <- getTypeSubst
-  let ty1'' = subst theta' ty1'
-      ty2'' = subst theta' ty2'
+  let predicated = Set.null $ predSet ty1'
+      ty1'' = subst theta' ty1'
+      ty2'' = subst theta' (if predicated
+                              then ty2'
+                              else TypeContext (subst theta ps2) ty2')
   unlessM (subsumCheck b emptyPredSet emptyPredSet ty1'' ty2'') $
     report $ errSubsumption p what doc m ty2' ty1'
-  reducePredSet p what doc (ps1 `Set.union` ps2)
+  reducePredSet p what doc
+                (ps1 `Set.union` (if predicated then ps2 else emptyPredSet))
 
 subsumCheck :: Bool -> PredSet -> PredSet -> Type -> Type -> TCM Bool
 subsumCheck True ps1 ps2 (TypeArrow ty11@(TypeForall _ _) ty12) (TypeArrow ty21@(TypeForall _ _) ty22)
diff --git a/src/Transformations/Dictionary.hs b/src/Transformations/Dictionary.hs
index 0ad30ef635f20786fbbd20205557ef6bc773a075..45cc776191363299e1c8f42ef2ab6cde5e7747c8 100644
--- a/src/Transformations/Dictionary.hs
+++ b/src/Transformations/Dictionary.hs
@@ -812,11 +812,11 @@ instance DictTrans Rhs where
 
 instance DictTrans Pattern where
   dictTrans (LiteralPattern        _ pty l) =
-    return $ LiteralPattern NoSpanInfo (transformPredType $ unpredType pty) l
+    return $ LiteralPattern NoSpanInfo (transformPredType pty) l
   dictTrans (VariablePattern       _ pty v) =
-    return $ VariablePattern NoSpanInfo (transformPredType $ unpredType pty) v
+    return $ VariablePattern NoSpanInfo (transformPredType pty) v
   dictTrans (ConstructorPattern _ pty c ts) = do
-    let tpty = transformPredType (unpredType pty)
+    let tpty = transformPredType pty
     pls <- matchPredList (conType c) $ foldr (TypeArrow . typeOf) tpty ts
     ConstructorPattern NoSpanInfo tpty c <$> addDictArgs pls ts
   dictTrans (AsPattern               _ v t) =
@@ -826,15 +826,17 @@ instance DictTrans Pattern where
 
 instance DictTrans Expression where
   dictTrans (Literal     _ pty l) =
-    return $ Literal NoSpanInfo (transformPredType $ unpredType pty) l
+    return $ Literal NoSpanInfo (transformPredType pty) l
   dictTrans (Variable    _ pty v) = do
-    let tpty = transformPredType (unpredType pty)
-    pls <- matchPredList (funType v) tpty
+    let tpty = transformPredType pty
+    pls <- case pty of
+             TypeContext _ _ -> return []
+             _               -> matchPredList (funType v) tpty
     es <- mapM dictArg pls
     let ty = foldr (TypeArrow . typeOf) tpty es
     return $ apply (Variable NoSpanInfo ty v) es
   dictTrans (Constructor _ pty c) = do
-    let tpty = transformPredType (unpredType pty)
+    let tpty = transformPredType pty
     pls <- matchPredList (conType c) tpty
     es <- mapM dictArg pls
     let ty = foldr (TypeArrow . typeOf) tpty es
@@ -928,16 +930,11 @@ instPredList (Pred cls ty) = case unapplyType True ty of
 matchPredList :: (ValueEnv -> Type) -> Type -> DTM [Pred]
 matchPredList tySc ty2 = do
   pty <- tySc <$> getValueEnv
-  let ps = getPredSet pty
+  let ps = predSet pty
   return $ foldr (\(pls1, pls2) pls' ->
                    fromMaybe pls' $ qualMatch pls1 (rawType pty) pls2 ty2)
                  (internalError $ "Dictionary.matchPredList: " ++ show ps)
                  (splits $ Set.toAscList ps)
-  where
-    getPredSet :: Type -> PredSet
-    getPredSet (TypeForall _ ty)  = getPredSet ty
-    getPredSet (TypeContext ps _) = ps
-    getPredSet _                  = emptyPredSet
 
 qualMatch :: [Pred] -> Type -> [Pred] -> Type -> Maybe [Pred]
 qualMatch pls1 ty1 pls2 ty2 = case predListMatch pls2 ty2 of
@@ -1005,6 +1002,7 @@ instance Specialize Expression where
 
 specialize' :: Expression Type -> [Expression Type] -> DTM (Expression Type)
 specialize' l@(Literal     _ _ _) es = return $ apply l es
+specialize' v@(Variable    _ _ _) [] = return v
 specialize' v@(Variable   _ _ v') es = do
   spEnv <- getSpEnv
   return $ case Map.lookup (v', f) spEnv of
diff --git a/test/pass/RankNTypes.curry b/test/pass/RankNTypes.curry
index c0012847d6d7d17d1d35717b8f0f6b22ad147ef2..ddaa8afee812639ea3595e3a210420b7daeda633 100644
--- a/test/pass/RankNTypes.curry
+++ b/test/pass/RankNTypes.curry
@@ -109,6 +109,12 @@ applyFoo (Bar x) f = f $ Bar x
 applyEqFun :: Eq a => (forall b. Eq b => b -> b -> Bool) -> a -> a -> Bool
 applyEqFun f x y = x `f` y
 
+-- applyEqFunTest1 :: Bool
+-- applyEqFunTest1 = applyEqFun (==) True False
+
+-- applyEqFunTest2 :: Bool -> Bool -> Bool
+-- applyEqFunTest2 = applyEqFun (==)
+
 applyMaybe :: Maybe a -> (forall b. b -> b) -> a
 applyMaybe Nothing  _ = error "fail"
 applyMaybe (Just x) f = f x
@@ -170,3 +176,22 @@ constFun' = const
 
 constFunTest :: Bool
 constFunTest = (id `constFun` 73) True
+
+data Showable = Showable (forall b. (forall a. Show a => a -> b) -> b)
+
+showableTest :: Show a => a -> Showable
+showableTest g = Showable (\f -> f g)
+
+showableFun1 :: Showable -> String
+showableFun1 (Showable f) = let k x = show x in f k
+
+-- showableFun2 :: Showable -> String
+-- showableFun2 (Showable f) = f (\x -> show x)
+
+showableFun3 :: Showable -> String
+showableFun3 showable = case showable of
+  Showable f -> let k x = show x in f k
+
+showableFun4 :: Showable -> String
+showableFun4 showable = case showable of
+  Showable f -> f show