diff --git a/requirements.cabal b/requirements.cabal
--- a/requirements.cabal
+++ b/requirements.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                requirements
-version:             0.7.0.2
+version:             0.7.0.3
 synopsis:            Abstraction to manage user defined Type Errors
 description:         requirements is a framework to build user-defined type errors.
                      Users condense the arguments of functions that can raise a
@@ -36,6 +36,6 @@
                   ,  TypeApplications      
                   ,  ScopedTypeVariables   
 
-  build-depends:       base >=4.12 && <4.18
+  build-depends:       base >=4.20 && < 4.21
   hs-source-dirs:      src
   default-language:    Haskell2010
diff --git a/src/Data/Type/Require.hs b/src/Data/Type/Require.hs
--- a/src/Data/Type/Require.hs
+++ b/src/Data/Type/Require.hs
@@ -189,7 +189,7 @@
 
 -- | A common constraint is to have a |Requirement| to be fullfilled,
 -- and something to unify with the result of the operation.  
-type RequireR (op :: Type) (ctx:: [ErrorMessage]) (res :: Type)
+type RequireR (op :: Type) (res :: Type) (ctx:: [ErrorMessage]) 
      = (Require op ctx, ReqR op ~ res)
 
 -- | 
@@ -214,31 +214,41 @@
                        :<>: Text "\n/= " :<>: ShowTE b)) ctx  
 
 
-
-data Exp (a :: Type) where Exp :: a -> Exp a
-type family Eval (exp :: Type) :: k
+type Exp a = a -> Type
+type family Eval (exp :: Exp a) :: a
 
 data CondEq (a ::Type) (b :: Type) where
   CondEq :: a -> b -> CondEq a b
 data RequireEqResF (a :: Type) (b :: Type) where
   RequireEqResF :: a -> b -> RequireEqResF a b
 
-data EqMsg (a::Type)(b::Type) where EqMsg :: a -> b -> EqMsg a b
+data EqMsg :: Exp a -> Exp b -> Exp ErrorMessage
 type instance Eval (EqMsg t1 t2) =
     (Text "\nEQMSG" :<>: ShowTE t1
                        :<>: Text "\n/= " :<>: ShowTE t2)
 
 
-type family RequireEqWithMsg (t :: k) (t' :: k) (msg :: k -> k -> Type)
+type family RequireEqWithMsg (t :: k) (t' :: k)
+  (msg :: k -> k -> ErrorMessage)
   (ctx :: [ErrorMessage]) :: Constraint
 type instance RequireEqWithMsg t t' f ctx =
   (AssertEq' t t' f ctx, t ~ t')
 type family AssertEq' (t1 :: k)(t2 :: k)
-                      (f :: k -> k -> Type) ctx :: Constraint
+                      (f :: k -> k -> ErrorMessage) ctx :: Constraint
   where
   AssertEq' a a f ctx = ()
-  AssertEq' a b f ctx = Require (OpError (Eval (f a b))) ctx
+  AssertEq' a b f ctx = Require (OpError ((f a b))) ctx
 
+type family RequireEqWithMsg' (t :: k) (t' :: k) (msg :: ErrorMessage)
+  (ctx :: [ErrorMessage]) :: Constraint
+type instance RequireEqWithMsg' t t' f ctx =
+  (AssertEq'' t t' f ctx, t ~ t')
+type family AssertEq'' (t1 :: k)(t2 :: k)
+                      (f :: ErrorMessage) ctx :: Constraint
+  where
+  AssertEq'' a a f ctx = ()
+  AssertEq'' a b f ctx = Require (OpError f) ctx
+
 -- Exported operators.
 
 -- | Equality operator.
@@ -266,7 +276,7 @@
 -- | overloaded type equality
 type family Equ (a :: k) (b :: k) :: Bool
 
-emptyCtx = Proxy :: Proxy '[ Text ""]
+emptyCtx = Proxy :: Proxy '[]
 
 appendCtx :: Proxy ctx -> Proxy ctx' -> Proxy (ctx :++ ctx')
 appendCtx Proxy Proxy = Proxy