diff --git a/digger.cabal b/digger.cabal
index 67448cfc3af1667f7c77f7899f7af13554e35f59..b58ef8f4f1b1534b27bde1b81fb1d14a4066f6b1 100644
--- a/digger.cabal
+++ b/digger.cabal
@@ -27,13 +27,14 @@ library
                        Language.Coq.Deep
   build-depends:       base >=4.9 && <4.12,
                        aeson >=0.11 && <1.4,
-                       containers >= 0.5.7 && <0.6,
+                       containers >=0.5.7 && <0.6,
+                       mtl >=2.2 && <2.3,
                        bytestring >=0.10 && <0.11,
-                       data-default >= 0.7 && < 0.8,
-                       text >= 1.2 && < 1.3,
-                       wl-pprint-text >= 1.1 && < 1.3,
-                       language-c >= 0.5 && < 0.9,
-                       pretty >= 1.1 && < 1.2
+                       data-default >=0.7 && <0.8,
+                       text >=1.2 && <1.3,
+                       wl-pprint-text >=1.1 && <1.3,
+                       language-c >=0.5 && <0.9,
+                       pretty >=1.1 && <1.2
   default-language:    Haskell2010
 
 executable digger
@@ -42,13 +43,13 @@ executable digger
   other-modules:       Paths_digger
   build-depends:       base >=4.9 && <4.12,
                        aeson >=0.11 && <1.4,
-                       containers >= 0.5.7 && <0.6,
+                       containers >=0.5.7 && <0.6,
                        bytestring >=0.10 && <0.11,
-                       data-default >= 0.7 && < 0.8,
+                       data-default >=0.7 && <0.8,
                        optparse-applicative >=0.12 && <0.15,
-                       text >= 1.2 && < 1.3,
-                       wl-pprint-text >= 1.1 && < 1.3,
-                       pretty >= 1.1 && < 1.2,
-                       language-c >= 0.5 && < 0.9,
+                       text >=1.2 && <1.3,
+                       wl-pprint-text >=1.1 && <1.3,
+                       pretty >=1.1 && <1.2,
+                       language-c >=0.5 && <0.9,
                        digger
   default-language:    Haskell2010
diff --git a/src/Language/Coq/Deep.hs b/src/Language/Coq/Deep.hs
index 47420712ba9d34bc7f3f5e81810be4efe189ece7..94e0688b51ded65dc05c5f278dc741b176db1e3a 100644
--- a/src/Language/Coq/Deep.hs
+++ b/src/Language/Coq/Deep.hs
@@ -59,6 +59,7 @@ module Language.Coq.Deep (
     ) where
 
 import           Control.Arrow                (second, (&&&))
+import           Control.Monad.Except
 import           Data.Default
 import           Data.Either                  (partitionEithers)
 import qualified Data.Map                     as Map
@@ -328,18 +329,18 @@ convertFunType cp = go
 -- - constructors for inline booleans
 
 convertFunBody :: ConversionParams -> Expr -> Either ErrorMsg Exp
-convertFunBody cp = go True
+convertFunBody cp = runExcept . go True
     where -- | Translate an expression
           -- Take as first argument whether the expression is monadic
           -- or not
-          go :: Bool -> Expr -> Either ErrorMsg Exp
+          go :: Bool -> Expr -> Except ErrorMsg Exp
           go True  (Apply (Global b) [e1, Lambda ["_"] e2]) | b == bind cp = BindN          <$> go True e1 <*> go True e2
           go True  (Apply (Global b) [e1, Lambda [v] e2])   | b == bind cp = Bind v Nothing <$> go True e1 <*> go True e2
           go True  (Apply (Global r) [e])                   | r == ret  cp = Return <$> go False e
           go _     (Apply (Global f) as)                                   = Call f <$> traverse (go False) as
-          go True  (Global v)                                              = Right (Call v [])
-          go False (Global v)                                              = Right (Var v)
-          go False (Rel v)                                                 = Right (Var v)
+          go True  (Global v)                                              = pure (Call v [])
+          go False (Global v)                                              = pure (Var v)
+          go False (Rel v)                                                 = pure (Var v)
           go True  (Case cond [C (ConstructorP c1 []) e1
                               ,C (ConstructorP c2 []) e2])  | checkIFT     = IfThenElse <$> go False cond
                                                                                         <*> go True thenE
@@ -347,9 +348,9 @@ convertFunBody cp = go True
                       where checkIFT = c1 == true  cp && c2 == false cp
                                     || c1 == false cp && c2 == true  cp
                             (thenE,elseE) = if c1 == true cp then (e1,e2) else (e2,e1)
-          go False (ConstructorE c []) | c `elem` consts cp                = Right (Const c)
+          go False (ConstructorE c []) | c `elem` consts cp                = pure (Const c)
 
-          go monadic e                                                     = Left $ impossibleExpr monadic e
+          go monadic e                                                     = throwError $ impossibleExpr monadic e
 
           impossibleExpr m ex = "Impossible to convert expression \"" ++ show ex ++ "\" " ++
                                 "in " ++ prefix m ++ "monadic context"