diff --git a/Abstract.hs b/Abstract.hs
--- a/Abstract.hs
+++ b/Abstract.hs
@@ -676,11 +676,11 @@
         succMeas (e:es) = e : succMeas es
 -}
 
-applyLastM :: Monad m => (a -> m a) -> Measure a -> m (Measure a)
-applyLastM f (Measure mu) = loop mu >>= return . Measure
+applyLastM :: (a -> Maybe a) -> Measure a -> Maybe (Measure a)
+applyLastM f (Measure mu) = Measure <$> loop mu
   where loop []     = fail "empty measure"
-        loop [e]    = f e >>= return . (:[])
-        loop (e:es) = loop es >>= return . (e:)
+        loop [e]    = (:[]) <$> f e
+        loop (e:es) = (e:)  <$> loop es
 
 instance HasPred a => HasPred (Measure a) where
   predecessor mu = applyLastM predecessor mu
diff --git a/Eval.hs b/Eval.hs
--- a/Eval.hs
+++ b/Eval.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TupleSections, FlexibleInstances, NamedFieldPuns #-}
+{-# LANGUAGE TupleSections, FlexibleInstances, FlexibleContexts, NamedFieldPuns #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE CPP #-}
 
@@ -12,10 +12,8 @@
 import Control.Applicative
 import Control.Monad.Identity hiding (mapM)
 import Control.Monad.State hiding (mapM)
-import Control.Monad.Error hiding (mapM)
+import Control.Monad.Except hiding (mapM)
 import Control.Monad.Reader hiding (mapM)
-import Control.Monad.IfElse  -- unlessM
--- import Control.Monad.HT      -- andLazy  -- because liftM2 (&&) is NOT lazy!
 
 import qualified Data.Array as Array
 import Data.Maybe -- fromMaybe
@@ -72,6 +70,9 @@
 traceSizeM msg = traceM msg
 -}
 
+failValInv :: (MonadError TraceError m) => Val -> m a
+failValInv v = throwErrorMsg $ "internal error: value " ++ show v ++ " violates representation invariant"
+
 -- evaluation with rewriting -------------------------------------
 
 {-
@@ -546,7 +547,7 @@
       bv  <- whnf env b -- not adding measure constraint to context!
       case (envBound env) of
         Nothing   -> return $ VMeasured muv bv
-           -- fail $ "panic: whnf " ++ show e ++ " : no measure in environment " ++ show env
+           -- throwErrorMsg $ "panic: whnf " ++ show e ++ " : no measure in environment " ++ show env
         Just muv' -> return $ VGuard (Bound Lt muv muv') bv
 
     Quant Pi (TBound (Bound ltle mu mu')) b -> do
@@ -603,7 +604,7 @@
         whnfClos (definingVal item)
 
     Def (DefId (ConK DefPat) n) -> whnfClos . definingVal =<< lookupSymbQ n
---    Def (DefId (ConK DefPat) n) -> fail $ "internal error: whnf of defined pattern " ++ show n
+--    Def (DefId (ConK DefPat) n) -> throwErrorMsg $ "internal error: whnf of defined pattern " ++ show n
     Def id   -> return $ vDef id
 {-
     Con co n -> return $ VCon co n
@@ -619,7 +620,7 @@
     Var y -> lookupEnv env y >>= whnfClos
     Ann e -> whnf env (unTag e) -- return VIrr -- NEED TO KEEP because of eta-exp!
     Irr -> return VIrr
-    e   -> fail $ "NYI whnf " ++ show e
+    e   -> throwErrorMsg $ "NYI whnf " ++ show e
 
 whnfMeasure :: Env -> Measure Expr -> TypeCheck (Measure Val)
 whnfMeasure rho (Measure mu) = mapM (whnf rho) mu >>= return . Measure
@@ -704,7 +705,7 @@
             VProj Pre n -> flip (app' expandDefs) (VProj Post n) =<< whnfClos v
             VRecord ri rho -> do
               let VProj Post n = v
-              maybe (fail $ "app: projection " ++ show n ++ " not found in " ++ show u)
+              maybe (throwErrorMsg $ "app: projection " ++ show n ++ " not found in " ++ show u)
                 whnfClos (lookup n rho)
             VDef (DefId FunK n) -> appDef_ n [v]
             VApp (VDef (DefId FunK n)) vl -> appDef_ n (vl ++ [v])
@@ -739,7 +740,7 @@
 
             VIrr -> return VIrr
 {- 2010-11-01 this breaks extraction for System U example
-            VIrr -> fail $ "app internal error: " ++ show (VApp u [v])
+            VIrr -> throwErrorMsg $ "app internal error: " ++ show (VApp u [v])
 -}
             _ -> return $ VApp u [v]
 --
@@ -764,7 +765,7 @@
 -- -- ALT: VIrr consumes applications
 --             (VIrr,_) -> return VIrr
 --  -}
---             (VIrr,_) -> fail $ "app internal error: " ++ show (VApp u c)
+--             (VIrr,_) -> throwErrorMsg $ "app internal error: " ++ show (VApp u c)
 --             _ -> return $ VApp u c
 
 
@@ -871,7 +872,7 @@
 matchingConstructors v@(VDef d) = failValInv v -- matchingConstructors' d []
 matchingConstructors (VApp (VDef (DefId DatK d)) vl) = matchingConstructors' d vl >>= return . Just
 matchingConstructors v = return Nothing
--- fail $ "matchingConstructors: not a data type: " ++ show v -- return []
+-- throwErrorMsg $ "matchingConstructors: not a data type: " ++ show v -- return []
 
 matchingConstructors' :: QName -> [Val] -> TypeCheck [(ConstructorInfo,Env)]
 matchingConstructors' n vl = do
@@ -1183,7 +1184,7 @@
 matchList env (p:pl) (v:vl) =
   match env p v `bindMaybe` \ env' ->
   matchList env' pl vl
-matchList env pl     vl     = fail $ "matchList internal error: inequal length while trying to match patterns " ++ show pl ++ " against values " ++ show vl
+matchList env pl     vl     = throwErrorMsg $ "matchList internal error: inequal length while trying to match patterns " ++ show pl ++ " against values " ++ show vl
 
 -- * Typed Non-linear Matching -----------------------------------------
 
@@ -1255,7 +1256,7 @@
     VQuant Pi x dom fv ->
       nonLinMatch undot symm st p v (typ dom) `bindMaybe` \ st' ->
       nonLinMatchList' undot symm st' pl vl =<< app fv v
-    _ -> fail $ "nonLinMatchList': cannot match in absence of pi-type"
+    _ -> throwErrorMsg $ "nonLinMatchList': cannot match in absence of pi-type"
 nonLinMatchList' _ _ _ _ _ _ = return Nothing
 
 
@@ -1264,7 +1265,7 @@
 expandDefPat p@(ConP pi c ps) | coPat pi == DefPat = do
   PatSig ns pat v <- lookupSymbQ c
   unless (length ns == length ps) $
-    fail ("underapplied defined pattern in " ++ show p)
+    throwErrorMsg ("underapplied defined pattern in " ++ show p)
   let pat' = if dottedPat pi then dotConstructors pat else pat
   return $ patSubst (zip ns ps) pat'
 expandDefPat p = return p
@@ -1341,7 +1342,7 @@
       VIrr                  -> mempty
       VCase v tv env cls    -> nocc ks $ v : tv : map snd (envMap env)
       -- impossible: closure (reduced away)
-      VClos{}               -> fail $ "internal error: nocc " ++ show (ks,v)
+      VClos{}               -> throwErrorMsg $ "internal error: nocc " ++ show (ks,v)
 
 
 -- heterogeneous typed equality and subtyping ------------------------
@@ -1450,7 +1451,7 @@
     Set   v -> ShSet   (One v)
     CoSet v -> ShCoSet (One v)
 
-typeView12 :: (Functor m, Error e, MonadError e m) => OneOrTwo TVal -> m TypeShape
+typeView12 :: (Functor m, Monad m, MonadError TraceError m) => OneOrTwo TVal -> m TypeShape
 -- typeView12 :: OneOrTwo TVal -> TypeCheck TypeShape
 typeView12 (One tv) = return $ typeView tv
 typeView12 (Two tv1 tv2) =
@@ -1465,16 +1466,16 @@
            (ShSort s1, ShSort s2) | s1 == s2 -> return $ ShSort $ s1
            (ShData n1 _, ShData n2 _) | n1 == n2 -> return $ ShData n1 (Two tv1 tv2)
            (ShNe{}     , ShNe{}     )            -> return $ ShNe (Two tv1 tv2)
-           _ -> throwError $ strMsg $ "type " ++ show tv1 ++ " has different shape than " ++ show tv2
+           _ -> throwErrorMsg $ "type " ++ show tv1 ++ " has different shape than " ++ show tv2
 
-sortView12 :: (Monad m) => OneOrTwo (Sort Val) -> m SortShape
+sortView12 :: (Monad m, MonadError TraceError m) => OneOrTwo (Sort Val) -> m SortShape
 sortView12 (One s) = return $ sortView s
 sortView12 (Two s1 s2) =
   case (s1, s2) of
     (SortC c1, SortC c2) | c1 == c2 -> return $ ShSortC c1
     (Set v1, Set v2)                -> return $ ShSet (Two v1 v2)
     (CoSet v1, CoSet v2)            -> return $ ShCoSet (Two v1 v2)
-    _ -> fail $ "sort " ++ show s1 ++ " has different shape than " ++ show s2
+    _ -> throwErrorMsg $ "sort " ++ show s1 ++ " has different shape than " ++ show s2
 
 whnf12 :: OneOrTwo Env -> OneOrTwo Expr -> TypeCheck (OneOrTwo Val)
 whnf12 env12 e12 = Traversable.traverse id $ zipWith12 whnf env12 e12
@@ -1514,9 +1515,9 @@
     mt12f <- mapM (mapM force) mt12 -- leads to LOOP, see HungryEta.ma
     sh12 <- case mt12f of
               Nothing -> return Nothing
-              Just tv12 -> case typeView12 tv12 of
+              Just tv12 -> case runExcept $ typeView12 tv12 of
                 Right sh -> return $ Just sh
-                Left err -> (recoverFail err) >> return Nothing
+                Left err -> (recoverFail $ show err) >> return Nothing
     case sh12 of
 
       -- subtyping directed by common type shape
@@ -1740,14 +1741,14 @@
             loop cls1' cls2'
 
 eqPattern :: Pattern -> Pattern -> TypeCheck ()
-eqPattern p1 p2 = if p1 == p2 then return () else fail $ "pattern " ++ show p1 ++ " != " ++ show p2
+eqPattern p1 p2 = if p1 == p2 then return () else throwErrorMsg $ "pattern " ++ show p1 ++ " != " ++ show p2
 -}
 
 type NameMap = [(Name,Name)]
 
 alphaPattern :: Pattern -> Pattern -> StateT NameMap TypeCheck ()
 alphaPattern p1 p2 = do
-  let failure = fail $ "pattern " ++ show p1 ++ " != " ++ show p2
+  let failure = throwErrorMsg $ "pattern " ++ show p1 ++ " != " ++ show p2
       alpha x1 x2 = do
         ns <- get
         case lookup x1 ns of
@@ -1836,7 +1837,7 @@
            <+> prettyTCM vl1 <+> text " to "
            <+> prettyTCM vl2 <+> text " at type "
            <+> prettyTCM tv12
---    _ -> fail $ "leqVals': not (compatible) function types or mismatch number of arguments when comparing  " ++ show vl1 ++ "  to  " ++ show vl2 ++ "  at type  " ++ show tv12
+--    _ -> throwErrorMsg $ "leqVals': not (compatible) function types or mismatch number of arguments when comparing  " ++ show vl1 ++ "  to  " ++ show vl2 ++ "  at type  " ++ show tv12
 
 {-
 leqVals' f q (VPi x1 dom1@(Domain av1 _ dec1) env1 b1,
@@ -2084,8 +2085,8 @@
          (v1,VMeta i rho n) -> addLe ltle v1 v2
          _ -> leSize'' ltle 0 v1 v2
 {- HANDLED BY leSize'' ltle
-         (VSucc{}, VGen{}) -> fail err
-         (VSucc{}, VPlus{}) -> fail err
+         (VSucc{}, VGen{}) -> throwErrorMsg err
+         (VSucc{}, VPlus{}) -> throwErrorMsg err
 -}
 -- leSize'' ltle bal v v'  checks whether  Succ^bal v `lt` v'
 -- invariant: bal is zero in cases for VMax and VMeta
@@ -2254,7 +2255,7 @@
     (True,False) -> ret LT -- THIS IS COMPLETE BOGUS!!!
     (True,True)  -> ret EQ
     (False,True) -> ret GT
-    (False,False) -> fail $ "compareSize (" ++ show a1 ++ ", " ++ show a2 ++ "): sizes incomparable"
+    (False,False) -> throwErrorMsg $ "compareSize (" ++ show a1 ++ ", " ++ show a2 ++ "): sizes incomparable"
 -}
 
 {- Bound entailment
diff --git a/Extract.hs b/Extract.hs
--- a/Extract.hs
+++ b/Extract.hs
@@ -152,7 +152,7 @@
 
 import Control.Applicative
 import Control.Monad
-import Control.Monad.Error
+import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.Writer
 import Control.Monad.State
@@ -176,7 +176,7 @@
 
 traceExtrM s = return ()
 
-runExtract sig k = runErrorT (runReaderT (runStateT k (initWithSig sig)) emptyContext)
+runExtract sig k = runExceptT (runReaderT (runStateT k (initWithSig sig)) emptyContext)
 
 -- extraction
 
@@ -198,7 +198,7 @@
 extractDecl d =
   case d of
     MutualDecl _ ds -> extractDecls ds -- TODO!
-    OverrideDecl{} -> fail $ "extractDecls internal error: overrides impossible"
+    OverrideDecl{} -> throwErrorMsg $ "extractDecls internal error: overrides impossible"
     MutualFunDecl _ co funs -> extractFuns co funs
     FunDecl co fun -> extractFun co fun
     LetDecl evl x tel (Just t) e | null tel -> extractLet evl x t e
@@ -354,7 +354,7 @@
             Prod av1 av2 ->
               extractPattern' av1 p1 $ \ [p1] -> do
                 extractPattern' av2 p2 $ \ [p2] -> cont [PairP p1 p2]
-            _ -> fail $ "extractPattern': IMPOSSIBLE: pattern " ++
+            _ -> throwErrorMsg $ "extractPattern': IMPOSSIBLE: pattern " ++
                           show p ++ " : " ++ show av
 -}
         ConP pi n ps -> do
@@ -369,7 +369,7 @@
   ConSig { conPars, extrTyp, dataPars } <- lookupSymbQ c
   traceExtrM ("extrConType " ++ show c ++ " has extrTyp = " ++ show extrTyp)
   tv <- whnf' extrTyp
-  numPars <- maybe (return dataPars) (const $ fail $ "NYI: extrConType for pattern parameters") conPars
+  numPars <- maybe (return dataPars) (const $ throwErrorMsg $ "NYI: extrConType for pattern parameters") conPars
   case numPars of
    0 -> return tv
    _ -> do
@@ -387,7 +387,7 @@
         piApps tv pars
 -}
       _ -> piApps tv $ replicate numPars VIrr
---      _ -> fail $ "extrConType " ++ show c ++ ": expected datatype, found " ++ show av
+--      _ -> throwErrorMsg $ "extrConType " ++ show c ++ ": expected datatype, found " ++ show av
 
 -- extracting a term from a term -------------------------------------
 
@@ -412,7 +412,7 @@
 
     Def f -> (Def f,) <$> do (whnf' . extrTyp) =<< lookupSymbQ (idName f)
 
-    Pair{} -> fail $ "extractInfer: IMPOSSIBLE: pair " ++ show e
+    Pair{} -> throwErrorMsg $ "extractInfer: IMPOSSIBLE: pair " ++ show e
     -- other expressions are erased or types
 
     _ -> return (Irr, VIrr)
@@ -458,7 +458,7 @@
 {-
       case view of
         Prod av1 av2 -> Pair <$> extractCheck e1 av1 <*> extractCheck e2 av2
-        _ -> fail $ "extractCheck: tuple type expected " ++ show e ++ " : " ++ show tv
+        _ -> throwErrorMsg $ "extractCheck: tuple type expected " ++ show e ++ " : " ++ show tv
 -}
 
     -- TODO: case
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -3,11 +3,11 @@
 files=Abstract Collection Concrete Eval Extract HsSyntax Lexer Main Parser Polarity PrettyTCM ScopeChecker Semiring SparseMatrix TCM Termination ToHaskell Tokens TraceError TreeShapedOrder TypeChecker Util Value Warshall
 hsfiles=$(foreach file,$(files),$(file).hs)
 ghcflags=-ignore-package monads-fd -rtsopts
-# -fglasgow-exts 
+# -fglasgow-exts
 optflags=
 # -O  #slow compilation, not much speedup
 profflags=-prof -auto-all
-distfiles=*.hs *.hs-boot Lexer.x Parser.y Makefile 
+distfiles=*.hs *.hs-boot Lexer.x Parser.y Makefile
 distdirs=test/succeed test/fail examples
 
 cabalp=cabal install -p --enable-executable-profiling
@@ -43,10 +43,10 @@
 #	Main test/fail/OverlappingPatternIndFam.ma # vec.ma # examples/List.ma
 
 # ship : ../dist/miniagda-2009-07-03.tgz # 06-27.tgz
-# 
+#
 # ../dist/%.tgz : $(distfiles)
 # 	tar czf $@ $^ $(distdirs)
-# 
+#
 
 miniagda-prof : Main.hs $(hsfiles)
 	ghc $(ghcflags) $(profflags) $< --make -o $@
@@ -76,13 +76,13 @@
 
 test : Main succeed fail
 
-succeed : 
+succeed :
 	@echo "======================================================================"
 	@echo "===================== Suite of successfull tests ====================="
 	@echo "======================================================================"
 	make -C test/succeed
 
-fail : 
+fail :
 	@echo "======================================================================"
 	@echo "======================= Suite of failing tests ======================="
 	@echo "======================================================================"
@@ -101,7 +101,7 @@
 	make -C lib
 
 
-clean : 
+clean :
 	-rm *.o *.hi Main miniagda-prof
 # 	make -C test/fail clean
 
diff --git a/MiniAgda.cabal b/MiniAgda.cabal
--- a/MiniAgda.cabal
+++ b/MiniAgda.cabal
@@ -1,7 +1,7 @@
 name:            MiniAgda
-version:         0.2014.5.5
+version:         0.2014.9.12
 build-type:      Simple
-cabal-version:   >= 1.8 
+cabal-version:   >= 1.8
 license:         OtherLicense
 license-file:    LICENSE
 author:          Andreas Abel and Karl Mehltretter
@@ -20,10 +20,9 @@
   arguments are discarded during equality checking and compilation.
 
   Recent features include bounded size quantification and destructor
-  patterns for a more general handling of coinduction. 
+  patterns for a more general handling of coinduction.
 
-tested-with:        GHC == 7.6.3,
-                    GHC == 7.8.2
+tested-with:        GHC == 7.8.3
 
 extra-source-files: Makefile
 
@@ -44,12 +43,9 @@
   build-depends:    array >= 0.3 && < 0.6,
                     base >= 4.2 && < 4.8,
                     containers >= 0.3 && < 0.6,
-                    haskell-src-exts >= 1.14 && < 1.15,
-                    -- mtl-2.1 contains a severe bug
-                    mtl >= 2.0 && < 2.1 || >= 2.1.1 && < 2.2,
-                    pretty >= 1.0 && < 1.2,
---                    utility-ht >= 0.0.1 && < 1.0,
-                    IfElse >= 0.85 && < 2.0
+                    haskell-src-exts >= 1.14 && < 1.16,
+                    mtl >= 2.2.0.1 && < 2.3,
+                    pretty >= 1.0 && < 1.2
   build-tools:      happy >= 1.15 && < 2,
                     alex >= 3.0 && < 4
   extensions:       CPP
diff --git a/ScopeChecker.hs b/ScopeChecker.hs
--- a/ScopeChecker.hs
+++ b/ScopeChecker.hs
@@ -9,12 +9,11 @@
 
 import Prelude hiding (mapM, null)
 
-import Control.Applicative -- <$>
-import Control.Monad.IfElse
+import Control.Applicative
 import Control.Monad.Identity hiding (mapM)
 import Control.Monad.Reader hiding (mapM)
 import Control.Monad.State hiding (mapM)
-import Control.Monad.Error hiding (mapM)
+import Control.Monad.Except hiding (mapM)
 
 import Data.List as List hiding (null)
 import Data.Maybe
@@ -153,7 +152,7 @@
 -- State monad (hidden) for global signature.
 -- Error monad for reporting scope violations.
 newtype ScopeCheck a = ScopeCheck { unScopeCheck ::
-  ReaderT SCCxt (StateT SCState (ErrorT TraceError Identity)) a }
+  ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a }
   deriving (Functor, Applicative, Monad,
     MonadReader SCCxt, MonadError TraceError)
 
@@ -162,7 +161,7 @@
   -> SCState        -- ^ Global identifier mapping.
   -> ScopeCheck a   -- ^ The computation.
   -> Either TraceError (a, SCState)
-runScopeCheck ctx st (ScopeCheck sc) = runIdentity $ runErrorT $
+runScopeCheck ctx st (ScopeCheck sc) = runIdentity $ runExceptT $
   runStateT (runReaderT sc ctx) st
 
 -- ** Local state.
@@ -419,7 +418,7 @@
   let (ns, mll) = unzip $ compressMaybes mmm
   let measured = null mll || isJust (head mll)
   let ok = null mll || all ((head mll)==) (tail mll)
-  when (not ok) $ fail $ "in a mutual function block, either all functions must be without measure or have a measure of the same length"
+  when (not ok) $ throwErrorMsg $ "in a mutual function block, either all functions must be without measure or have a measure of the same length"
 {-
   -- switch to internal fun ids
   let funNames = [ n | (FunK _ , A.TypeSig n _) <- ktsigs ] -- internal fun names
@@ -483,11 +482,11 @@
 
 mutualFlattenDecl :: C.Declaration -> ScopeCheck [C.Declaration]
 mutualFlattenDecl (C.MutualDecl ds) = mutualFlattenDecls ds
-mutualFlattenDecl (C.OverrideDecl Fail _) = fail $ "fail declaration not supported in mutual block"
+mutualFlattenDecl (C.OverrideDecl Fail _) = throwErrorMsg $ "fail declaration not supported in mutual block"
 mutualFlattenDecl (C.OverrideDecl o ds) = do
   ds' <- mutualFlattenDecls ds
   return $ map (\ d -> C.OverrideDecl o [d]) ds'
-mutualFlattenDecl (C.LetDecl{}) = fail $ "let in mutual block not supported"
+mutualFlattenDecl (C.LetDecl{}) = throwErrorMsg $ "let in mutual block not supported"
 mutualFlattenDecl d = return $ [d]
 
 -- extract type sigs of a mutual block in order, error on nested mutual
@@ -600,7 +599,7 @@
   r <- mapM (\ (C.FunDecl _ tysig _) -> scopeCheckFunSig tysig) l
   let (ml:mll, tsl') = unzip r
   let ok = all (ml==) mll
-  when (not ok) $ fail $ "in a mutual function block, either all functions must be without measure or have a measure of the same length"
+  when (not ok) $ throwErrorMsg $ "in a mutual function block, either all functions must be without measure or have a measure of the same length"
   -- add names as internal ids and check bodies
   let nxs = zipWith (\ (C.FunDecl _ (C.TypeSig n _) _) (A.TypeSig x _) -> (n,x)) l tsl'
   --let addFuns b = mapM (uncurry $ addAName $ FunK b) nxs
@@ -785,7 +784,7 @@
           A.Param   -> return dec
           A.Const   -> return dec
           A.PVar{}  -> return dec
-          _         -> fail $ "illegal polarity " ++ show (polarity dec) ++ " in type of constructor " ++ show a
+          _         -> throwErrorMsg $ "illegal polarity " ++ show (polarity dec) ++ " in type of constructor " ++ show a
 
 -- | Allow shadowing of previous locals.
 --   Always if we enter a subexpression which is not the body
@@ -827,7 +826,7 @@
       -- measure & bound
       -- measures can only appear in fun sigs!
       C.Quant pisig [C.TMeasure mu] e1 -> do
-        fail $ "measure not allowed in expression " ++ show e
+        throwErrorMsg $ "measure not allowed in expression " ++ show e
 
       -- measure bound mu < mu'
       C.Quant A.Pi [C.TBound beta] e1 -> do
@@ -836,7 +835,7 @@
         e1'   <- scopeCheckExpr' e1
         return $ A.pi (A.TBound beta') e1'
 
-      C.Quant A.Sigma [C.TBound beta] e1 -> fail $
+      C.Quant A.Sigma [C.TBound beta] e1 -> throwErrorMsg $
         "measure bound not allowed in expression " ++ show e
 
       C.Quant pisig tel e -> do
@@ -875,7 +874,7 @@
           Just x -> return $ A.Var x
           Nothing -> scopeCheckGlobalVar n
 
-      _ -> fail $ "NYI: scopeCheckExpr " ++ show e
+      _ -> throwErrorMsg $ "NYI: scopeCheckExpr " ++ show e
 
 scopeCheckGlobalVar :: C.QName -> ScopeCheck A.Expr
 scopeCheckGlobalVar n = do
@@ -1065,7 +1064,7 @@
     C.Record fs          -> mapM_ (scpField e) fs
     C.Ident n            -> scpApp e n []
     C.App (C.Ident n) es -> scpApp e n es
-    C.App C.App{} es     -> fail $ "scopeCheckParameter " ++ show e ++ ": internal invariant violated"
+    C.App C.App{} es     -> throwErrorMsg $ "scopeCheckParameter " ++ show e ++ ": internal invariant violated"
     _ -> errorInvalidParameter e
   where
     -- we can only treat a record expression as pattern
diff --git a/TCM.hs b/TCM.hs
--- a/TCM.hs
+++ b/TCM.hs
@@ -5,10 +5,9 @@
 import Prelude hiding (null)
 
 import Control.Monad
-import Control.Monad.IfElse
 import Control.Monad.Identity
 import Control.Monad.State
-import Control.Monad.Error
+import Control.Monad.Except
 import Control.Monad.Reader
 
 import Control.Applicative
@@ -226,7 +225,7 @@
 emptyPosGraph = []
 
 -- type TypeCheck = StateT TCState (ReaderT TCContext (CallStackT String IO))
-type TypeCheck = StateT TCState (ReaderT TCContext (ErrorT TraceError IO))
+type TypeCheck = StateT TCState (ReaderT TCContext (ExceptT TraceError IO))
 
 instance MonadAssert TypeCheck where
   assert b s = do
@@ -412,49 +411,21 @@
         -- upperDecs need not be updated
         }
 
-{-
--- only defined for single bindings
-cxtSetType :: Int -> Dec -> TVal -> SemCxt -> SemCxt
-cxtSetType k dec tv delta =
-  delta { cxt  = Map.insert k (One tv) (cxt delta)
-        , decs = Map.insert k (One dec) (decs delta)
-        -- upperDecs need not be updated
-        }
---        , decs = Map.insert k dec (decs delta) }
--}
-{-
-cxtLookupGen :: Monad m => SemCxt -> Int -> m Domain
-cxtLookupGen delta k = do
-  One tv  <- lookupM k (cxt delta)
-  One dec <- lookupM k (decs delta)
---  dec    <- lookupM k (decs delta)
-  return $ Domain { typ = tv, decor = dec }
+-- | Version of 'Map.lookup' that throws 'TraceError'.
+lookupM :: (MonadError TraceError m, Show k, Ord k) => k -> Map k v -> m v
+lookupM k m = maybe (throwErrorMsg $ "lookupM: unbound key " ++ show k) return $ Map.lookup k m
 
-cxtLookupGen :: Monad m => SemCxt -> Int -> m CxtEntry
-cxtLookupGen delta k = do
-  tv12  <- lookupM k (cxt delta)
-  dec12 <- lookupM k (decs delta)
-  udec  <- lookupM k (upperDecs delta)
-  return $ CxtEntry (zipWith12 Domain tv12 dec12) udec
--}
-cxtLookupGen :: Monad m => SemCxt -> Int -> m CxtEntry
+cxtLookupGen :: MonadError TraceError m => SemCxt -> Int -> m CxtEntry
 cxtLookupGen delta k = do
   dom12 <- lookupM k (cxt delta)
   udec  <- lookupM k (upperDecs delta)
   return $ CxtEntry dom12 udec
 
-cxtLookupName :: Monad m => SemCxt -> Ren -> Name -> m CxtEntry
+cxtLookupName :: MonadError TraceError m => SemCxt -> Ren -> Name -> m CxtEntry
 cxtLookupName delta ren x = do
   i <- lookupM x ren
   cxtLookupGen delta i
 
-{-
-cxtLookupName :: Monad m => SemCxt -> Ren -> Name -> m Domain
-cxtLookupName delta ren x = do
-  i <- lookupM x ren
-  cxtLookupGen delta i
--}
-
 -- apply decoration, possibly resurrecting (see Pfenning, LICS 2001)
 -- and changing polarities (see Abel, MSCS 2008)
 cxtApplyDec :: Dec -> SemCxt -> SemCxt
@@ -631,14 +602,14 @@
   genOfName x = do
     ce <- ask
     case Map.lookup x (renaming ce) of
-      Nothing -> fail $ "internal error: variable not bound: " ++ show x
+      Nothing -> throwErrorMsg $ "internal error: variable not bound: " ++ show x
       Just k -> return k
 
   nameOfGen k = do
     ce <- ask
     case Map.lookup k (naming ce) of
       Nothing -> return $ fresh $ "error_unnamed_gen" ++ show k
-       -- fail $ "internal error: no name for variable " ++ show k
+       -- throwErrorMsg $ "internal error: no name for variable " ++ show k
       Just x -> return x
 
 {-
@@ -784,7 +755,7 @@
            TSO.increasesHeight son (dist, father) <$> asks sizeRels) $ do
       recoverFail $ "cannot add hypothesis " ++ s ++ " because it is not satisfyable under all possible valuations of the current hypotheses"
     -- if the new son is an ancestor of the father, we are cyclic
-    awhenM (TSO.isAncestor father son <$> asks sizeRels) $ \ n -> -- n steps from father up to son
+    whenJustM (TSO.isAncestor father son <$> asks sizeRels) $ \ n -> -- n steps from father up to son
       when (dist > - n) $ -- still ok if dist == n == 0, otherwise fail
         recoverFail$ "cannot add hypothesis " ++ s ++ " because it makes the set of hyptheses unsatisfiable"
     local (\ cxt -> cxt
@@ -982,11 +953,11 @@
     VApp (VDef (DefId DatK d)) vl ->
       case p of
         ProjP n -> cont =<< projectType tv n VIrr -- no record value here
-        _       -> fail $ "introPatType: internal error, expected projection pattern, found " ++ show p ++ " at type " ++ show tv
+        _       -> throwErrorMsg $ "introPatType: internal error, expected projection pattern, found " ++ show p ++ " at type " ++ show tv
     VQuant Pi x dom fv -> do
        v  <- whnfClos v
        matchPatType (p,v) dom . cont =<< app fv v
-    _ -> fail $ "introPatType: internal error, expected Pi-type, found " ++ show tv
+    _ -> throwErrorMsg $ "introPatType: internal error, expected Pi-type, found " ++ show tv
 
 introPatTypes :: [(Pattern,Val)] -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a
 introPatTypes pvs tv f = do
@@ -1021,12 +992,12 @@
                  matchPatType (p1,v1) dom1 $ do
                    bv <- app fv v1
                    matchPatType (p2,v2) (Domain bv ki dec) cont
-               _ -> fail $ "matchPatType: IMPOSSIBLE " ++ show p ++ "  :  " ++ show dom
+               _ -> throwErrorMsg $ "matchPatType: IMPOSSIBLE " ++ show p ++ "  :  " ++ show dom
 
           (DotP e, _) -> cont
           (AbsurdP, _) -> cont
           (ErasedP p,_) -> matchPatType (p,v) dom cont
-          _ -> fail $ "matchPatType: IMPOSSIBLE " ++ show (p,v)
+          _ -> throwErrorMsg $ "matchPatType: IMPOSSIBLE " ++ show (p,v)
 
 
 -- Signature -----------------------------------------------------
@@ -1164,7 +1135,7 @@
       dv <- dataView tv
       case dv of
         Data d _ -> return $ Qual d n
-        _ -> fail $ "cannot resolve constructor " ++ show n
+        _ -> throwErrorMsg $ "cannot resolve constructor " ++ show n
 
 -- | @conType c tv@ returns the type of constructor @c@ at datatype @tv@
 --   with parameters instantiated.
@@ -1209,7 +1180,7 @@
     NoData    -> failDoc (text ("conType " ++ show c ++ ": expected")
                    <+> prettyTCM tv <+> text "to be a data type")
     Data d vs -> do
-      unless (d == dataName) $ fail $ "expected constructor of datatype " ++ show d ++ ", but found one of datatype " ++ show dataName
+      unless (d == dataName) $ throwErrorMsg $ "expected constructor of datatype " ++ show d ++ ", but found one of datatype " ++ show dataName
       let (pars, inds) = splitAt numPars vs
       unless (length pars == numPars) $
         failDoc (text ("conType " ++ show c ++ ": expected")
@@ -1247,8 +1218,8 @@
                    <+> prettyTCM tv <+> text "to be a data type")
     Data d vs -> do
       whenJust md $ \ d' ->
-        unless (d == d') $ fail $ "expected constructor of datatype " ++ show d ++ ", but found one of datatype " ++ show d'
-      -- whenJust conPars $ fail $ "NYI: constructor with pattern parameters"
+        unless (d == d') $ throwErrorMsg $ "expected constructor of datatype " ++ show d ++ ", but found one of datatype " ++ show d'
+      -- whenJust conPars $ throwErrorMsg $ "NYI: constructor with pattern parameters"
       let (pars, inds) = splitAt dataPars vs
       unless (length pars == dataPars) failure
       case (isSized, inds) of
@@ -1364,7 +1335,7 @@
       -- lookupSig :: Name -> Signature -> TypeCheck SigDef
       lookupSig n sig =
         case (Map.lookup n sig) of
-          Nothing -> fail $ "identifier " ++ show n ++ " not in signature "  ++ show (Map.keys sig)
+          Nothing -> throwErrorMsg $ "identifier " ++ show n ++ " not in signature "  ++ show (Map.keys sig)
           Just k -> return k
 
 
@@ -1411,8 +1382,8 @@
   mkConstraint v (VMax vs) = do
     bs <- mapM (errorToBool . leqSize' v) vs
     if any id bs then return Nothing else
-     fail $ "cannot handle constraint " ++ show v ++ " <= " ++ show (VMax vs)
-  mkConstraint w@(VMax vs) v = fail $ "cannot handle constraint " ++ show w ++ " <= " ++ show v
+     throwErrorMsg $ "cannot handle constraint " ++ show v ++ " <= " ++ show (VMax vs)
+  mkConstraint w@(VMax vs) v = throwErrorMsg $ "cannot handle constraint " ++ show w ++ " <= " ++ show v
   mkConstraint (VMeta i rho n) (VMeta j rho' m) = retret $ arc (Flex i) (m-n) (Flex j)
   mkConstraint (VMeta i rho n) VInfty      = retret $ arc (Flex i) 0 (Rigid (RConst Infinite))
   mkConstraint (VMeta i rho n) v           = retret $ arc (Flex i) (m-n) (Rigid (RVar j))
@@ -1420,7 +1391,7 @@
   mkConstraint VInfty (VMeta i rho n)      = retret $ arc (Rigid (RConst Infinite)) 0 (Flex i)
   mkConstraint v (VMeta j rho m)           = retret $ arc (Rigid (RVar i)) (m-n) (Flex j)
     where (i,n) = vGenSuccs v 0
-  mkConstraint v1 v2 = fail $ "mkConstraint undefined for " ++ show (v1,v2)
+  mkConstraint v1 v2 = throwErrorMsg $ "mkConstraint undefined for " ++ show (v1,v2)
 
   -- addMeta k x  adds a metavariable which can refer to VGens < k
   -- addMeta :: Ren -> MVar -> TypeCheck ()
@@ -1450,7 +1421,7 @@
      else case solve cs of
         Just subst -> traceMeta ("solution" ++ show subst) $
                       return subst
-        Nothing    -> fail $ "size constraints " ++ show cs ++ " unsolvable"
+        Nothing    -> throwErrorMsg $ "size constraints " ++ show cs ++ " unsolvable"
 
 
 nameOf :: EnvMap -> Int -> Maybe Name
diff --git a/TCM.hs-boot b/TCM.hs-boot
--- a/TCM.hs-boot
+++ b/TCM.hs-boot
@@ -5,7 +5,7 @@
 
 import Control.Monad.Identity
 import Control.Monad.State
-import Control.Monad.Error
+import Control.Monad.Except
 import Control.Monad.Reader
 
 data OneOrTwo a = One a | Two a a
@@ -14,4 +14,4 @@
 data TCState
 
 -- type TypeCheck = StateT TCState (ReaderT TCContext (CallStackT String IO))
-type TypeCheck = StateT TCState (ReaderT TCContext (ErrorT TraceError IO))
+type TypeCheck = StateT TCState (ReaderT TCContext (ExceptT TraceError IO))
diff --git a/ToHaskell.hs b/ToHaskell.hs
--- a/ToHaskell.hs
+++ b/ToHaskell.hs
@@ -45,7 +45,7 @@
 
 import Control.Applicative
 import Control.Monad
-import Control.Monad.Error
+import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.Writer
 import Control.Monad.State
@@ -66,7 +66,7 @@
 
 -- translation monad
 
-type Translate = StateT TState (ReaderT TContext (ErrorT TraceError IO))
+type Translate = StateT TState (ReaderT TContext (ExceptT TraceError IO))
 
 {- no longer needed with mtl-2
 instance Applicative Translate where
@@ -85,7 +85,7 @@
 initCxt = TContext
 
 runTranslate :: Translate a -> IO (Either TraceError a)
-runTranslate t = runErrorT (runReaderT (evalStateT t initSt) initCxt)
+runTranslate t = runExceptT (runReaderT (evalStateT t initSt) initCxt)
 
 -- translation
 
@@ -101,7 +101,7 @@
 translateDecl d =
   case d of
     MutualDecl _ ds -> translateDecls ds
-    OverrideDecl{} -> fail $ "translateDecls internal error: overrides impossible"
+    OverrideDecl{} -> throwErrorMsg $ "translateDecls internal error: overrides impossible"
     MutualFunDecl _ _ funs -> translateFuns funs
     FunDecl _ fun -> translateFun fun
     LetDecl _ x tel (Just t) e | null tel -> translateLet x t e
@@ -196,7 +196,7 @@
     _ -> return H.unit_tycon
 
 {- TODO:
-    _ -> fail $ "no Haskell representation for type " ++ show t
+    _ -> throwErrorMsg $ "no Haskell representation for type " ++ show t
  -}
 
 translateExpr :: FExpr -> Translate H.Exp
@@ -269,7 +269,7 @@
   (DefId DatK (QName x)) -> do
     let n = suggestion x
     unless (isUpper $ head n) $
-      fail $ "data names need to be capitalized"
+      throwErrorMsg $ "data names need to be capitalized"
     return $ H.Ident n
   (DefId (ConK co) (Qual d x)) -> do
     let n = suggestion x
@@ -283,7 +283,7 @@
     let n = suggestion $ unqual x
 {- ignore for now
      unless (isLower $ head n) $
-       fail $ "function names need to start with a lowercase letter"
+       throwErrorMsg $ "function names need to start with a lowercase letter"
  -}
     return $ H.Ident n
 
diff --git a/TraceError.hs b/TraceError.hs
--- a/TraceError.hs
+++ b/TraceError.hs
@@ -2,7 +2,7 @@
 
 module TraceError where
 
-import Control.Monad.Error
+import Control.Monad.Except
 import Debug.Trace
 
 import Util
@@ -10,9 +10,9 @@
 
 data TraceError = Err String | TrErr String TraceError
 
-instance Error TraceError where
-    noMsg = Err "no message"
-    strMsg s = Err s
+-- instance Error TraceError where
+--     noMsg = Err "no message"
+--     strMsg s = Err s
 
 instance Show TraceError where
     show (Err str) = str
@@ -35,8 +35,8 @@
   d <- md
   enter (render (pretty d)) cont
 
-failDoc :: (Monad m) => m Doc -> m a
-failDoc d = fail . render =<< d
+failDoc :: (MonadError TraceError m) => m Doc -> m a
+failDoc d = throwErrorMsg . render =<< d
 
 newErrorDoc :: (MonadError TraceError m) => m a -> m Doc -> m a
 newErrorDoc c d = c `catchError` (\ _ -> failDoc d)
@@ -47,13 +47,13 @@
 errorToBool :: (MonadError e m) => m () -> m Bool
 errorToBool m = (m >> return True) `catchError` (\ _ -> return False)
 
-boolToErrorDoc :: (Monad m) => m Doc -> Bool -> m ()
+boolToErrorDoc :: (MonadError TraceError m) => m Doc -> Bool -> m ()
 boolToErrorDoc d True  = return ()
 boolToErrorDoc d False = failDoc d
 
-boolToError :: (Monad m) => String -> Bool -> m ()
+boolToError :: (MonadError TraceError m) => String -> Bool -> m ()
 boolToError msg True  = return ()
-boolToError msg False = fail msg
+boolToError msg False = throwErrorMsg msg
 
 instance MonadError () Maybe where
   catchError Nothing k = k ()
@@ -68,13 +68,13 @@
 data AssertionHandling = Failure | Warning | Ignore
                        deriving (Eq,Ord,Show)
 
-assert' :: (MonadIO m) => AssertionHandling -> Bool -> String -> m ()
+assert' :: (MonadError TraceError m, MonadIO m) => AssertionHandling -> Bool -> String -> m ()
 assert' Ignore b s      = return ()
 assert' h True s        = return ()
 assert' Warning False s = liftIO $ putStrLn $ "warning: ignoring error: " ++ s
-assert' Failure False s = fail s
+assert' Failure False s = throwErrorMsg s
 
-assertDoc' :: (MonadIO m) => AssertionHandling -> Bool -> m Doc -> m ()
+assertDoc' :: (MonadError TraceError m, MonadIO m) => AssertionHandling -> Bool -> m Doc -> m ()
 assertDoc' h b md = assert' h b . render =<< md
 
 class Monad m => MonadAssert m where
diff --git a/TreeShapedOrder.hs b/TreeShapedOrder.hs
--- a/TreeShapedOrder.hs
+++ b/TreeShapedOrder.hs
@@ -61,7 +61,7 @@
 
 -- | @parent a o@ returns the immediate parent, if it exists.
 parent :: (Ord a, Eq a) => a -> TSO a -> Maybe (Int,a)
-parent a t = headM $ parents a t
+parent a t = headMaybe $ parents a t
 
 -- | @isAncestor a b o = Just n@ if there are n steps up from a to b.
 isAncestor :: (Ord a, Eq a) => a -> a -> TSO a -> Maybe Int
diff --git a/TypeChecker.hs b/TypeChecker.hs
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -7,10 +7,9 @@
 
 import Control.Applicative hiding (Const) -- ((<$>))
 import Control.Monad
-import Control.Monad.IfElse
 import Control.Monad.Identity
 import Control.Monad.State
-import Control.Monad.Error
+import Control.Monad.Except
 import Control.Monad.Reader
 
 import qualified Data.List as List
@@ -68,17 +67,17 @@
 
 {- DEAD CODE
 runWhnf :: Signature -> TypeCheck a -> IO (Either TraceError (a,Signature))
-runWhnf sig tc = (runErrorT (runStateT tc  sig))
+runWhnf sig tc = (runExceptT (runStateT tc  sig))
 -}
 
-doNf sig e = runErrorT (runReaderT (runStateT (whnf emptyEnv e >>= reify) (initWithSig sig)) emptyContext)
-doWhnf sig e = runErrorT (runReaderT (runStateT (whnf emptyEnv e >>= whnfClos) (initWithSig sig)) emptyContext)
+doNf sig e = runExceptT (runReaderT (runStateT (whnf emptyEnv e >>= reify) (initWithSig sig)) emptyContext)
+doWhnf sig e = runExceptT (runReaderT (runStateT (whnf emptyEnv e >>= whnfClos) (initWithSig sig)) emptyContext)
 
 
 -- top-level functions -------------------------------------------
 
 runTypeCheck :: TCState -> TypeCheck a -> IO (Either TraceError (a,TCState))
-runTypeCheck st tc = runErrorT (runReaderT (runStateT tc st) emptyContext)
+runTypeCheck st tc = runExceptT (runReaderT (runStateT tc st) emptyContext)
 -- runTypeCheck st tc = runCallStackT (runReaderT (runStateT tc st) emptyContext) []
 
 typeCheck dl = runTypeCheck initSt (typeCheckDecls dl)
@@ -130,7 +129,7 @@
   r <- (typeCheckDecls ds >> return True) `catchError`
         (\ s -> do liftIO $ putStrLn ("block fails as expected, error message:\n" ++ show s)
                    return False)
-  if r then fail "unexpected success" else do
+  if r then throwErrorMsg "unexpected success" else do
     put st
     return []
 
@@ -242,7 +241,7 @@
   newAssertionHandling Warning $ typeCheckMutualSig d
 typeCheckMutualSig (OverrideDecl Impredicative [d]) =
   goImpredicative $ typeCheckMutualSig d
-typeCheckMutualSig d = fail $ "typeCheckMutualSig: panic: unexpected declaration " ++ show d
+typeCheckMutualSig d = throwErrorMsg $ "typeCheckMutualSig: panic: unexpected declaration " ++ show d
 
 -- typeCheckMutualBody measured kindCandidate
 typeCheckMutualBody :: Bool -> Kind -> Declaration -> TypeCheck [EDeclaration]
@@ -272,7 +271,7 @@
                  -- insert correct polarity annotation if none was there
                  pol | pol `elem` [Param,Rec] -> return $ Quant Pi (TBind x $ Domain tSize kSize $ setPol polsz dec) b
                  pol | pol == polsz -> return t0
-                 pol -> fail $ "sized type " ++ show n ++ " has wrong polarity annotation " ++ show pol ++ " at Size argument, it should be " ++ show polsz
+                 pol -> throwErrorMsg $ "sized type " ++ show n ++ " has wrong polarity annotation " ++ show pol ++ " at Size argument, it should be " ++ show polsz
              t0 -> return t0
            return (params + 1, pos0 ++ [polsz], t)
          NotSized -> return (params, pos0, t0)
@@ -418,7 +417,7 @@
   return (cxt, ps)
 
   where
-    errorParamNotPattern e = fail $
+    errorParamNotPattern e = throwErrorMsg $
       "expected parameter to be a pattern, but I found " ++ show es
 
 -- |
@@ -683,7 +682,7 @@
              addBind (mapDec (const paramDec) tb) $ do  -- size is parametric in constructor type
                Kinded ki t2e <- checkConType' t2
                return $ Kinded ki $ Quant Pi (mapDec (const irrelevantDec) tb) t2e -- size is irrelevant in constructor
-      _ -> fail $ "checkConType: expecting size quantification, found " ++ show t
+      _ -> throwErrorMsg $ "checkConType: expecting size quantification, found " ++ show t
 
 checkConType' :: Expr -> TypeCheck (Kinded Extr)
 checkConType' t = do
@@ -691,7 +690,7 @@
   case s of
     Set{} -> return kte
     CoSet{} -> return kte
-    _ -> fail $ "checkConType: type " ++ show t ++ " of constructor not a universe"
+    _ -> throwErrorMsg $ "checkConType: type " ++ show t ++ " of constructor not a universe"
 
 -- check that the data type and the parameter arguments (written down like declared in telescope)
 -- precondition: target tg type checks in current context
@@ -704,7 +703,7 @@
       enter ("checking datatype parameters in constructor target") $
         leqVals' N mixed (One dv) (take (size tel) vs) telvs
       return ()
-    _ -> fail $ "constructor should produce something in data type " ++ show d
+    _ -> throwErrorMsg $ "constructor should produce something in data type " ++ show d
 
 {- RETIRED (syntactic check)
 checkTarget :: Name -> Telescope -> Type -> TypeCheck ()
@@ -1263,7 +1262,7 @@
   let parametric = checkingConType cxt  -- are we dealing with a parametric pi?
   let err = "ptsRule " ++ show (s1,s2) ++ " " ++ (if parametric then "(in type of constructor)" else "") ++ ": "
   case (s1,s2) of
-    (Set VInfty,_) -> fail $ err ++ "domain too big"
+    (Set VInfty,_) -> throwErrorMsg $ err ++ "domain too big"
     (Set v1, Set v2) ->
       if parametric then do
          unless er $ leqSize Pos v1 v2 -- when we are checking a constructor, to reject
@@ -1273,15 +1272,15 @@
     (CoSet v1, Set VZero)
        | parametric   -> return $ CoSet v1
        | v1 == VInfty -> return $ Set VZero
-       | otherwise    -> fail $ err ++ "domain cannot be sized"
+       | otherwise    -> throwErrorMsg $ err ++ "domain cannot be sized"
     (CoSet v1, CoSet v2)
        | parametric   -> do
            let v2' = maybe v2 id $ predSize v2
            case minSize v1 v2 of
              Just v  -> return $ CoSet v
-             Nothing -> fail $ err ++ "min" ++ show (v1,v2) ++ " does not exist"
+             Nothing -> throwErrorMsg $ err ++ "min" ++ show (v1,v2) ++ " does not exist"
        | v1 == VInfty -> return $ CoSet $ succSize v2
-       | otherwise    -> fail $ err ++ "domain cannot be sized"
+       | otherwise    -> throwErrorMsg $ err ++ "domain cannot be sized"
     _ -> return s2
 
 checkOrInfer :: Dec -> Expr -> Maybe Type -> TypeCheck (TVal, EType, Kinded Extr)
@@ -1302,7 +1301,7 @@
   (sv, te) <- inferExpr t
   case sv of
     VSort s | not (s `elem` map SortC [Tm,Size]) -> return (s,te)
-    _ -> fail $ "inferExpr: expected " ++ show t ++ " to be a type!"
+    _ -> throwErrorMsg $ "inferExpr: expected " ++ show t ++ " to be a type!"
 
 -- inferExpr e = (tv, s, ee)
 -- input : expr e | inferable e
@@ -1380,9 +1379,9 @@
         let dec = decor item
         let pol = polarity dec
         if erased dec then
-          fail $ err ++ ", because it is marked as erased"
+          throwErrorMsg $ err ++ ", because it is marked as erased"
          else if not (leqPol pol SPos) then
-          fail $ err ++ ", because it has polarity " ++ show pol
+          throwErrorMsg $ err ++ ", because it has polarity " ++ show pol
          else do
            -- traceCheckM ("infer variable " ++ x ++ " : " ++ show  (typ item))
            return $ (typ item, Var x) -- TODO: (typ item, kind item, Var x)
@@ -1408,7 +1407,7 @@
         checkCon <- asks checkingConType
 {- TODO
         when (checkCon && polarity dec /= Mixed) $
-          fail $ "constructor arguments must be declared mixed-variant"
+          throwErrorMsg $ "constructor arguments must be declared mixed-variant"
 -}
         (s1, Kinded ki0 t1e) <- (if pisig==Pi then checkingDom else id) $
           checkingCon False $ inferType t1 -- switch off parametric Pi
@@ -1579,7 +1578,7 @@
       case s of
         Set VZero -> return te
         CoSet{} -> return te
-        _ -> fail $ "expected " ++ show s ++ " to be Set or CoSet _"
+        _ -> throwErrorMsg $ "expected " ++ show s ++ " to be Set or CoSet _"
 
 {-
 -- small type
@@ -1620,8 +1619,8 @@
         tel <- getContextTele -- TODO!
         case (absp,mrhs) of
            (True,Nothing) -> return $ Kinded NoKind (Clause tel [pe] Nothing)
-           (False,Nothing) -> fail ("missing right hand side in case " ++ showCase cl)
-           (True,Just rhs) -> fail ("absurd pattern requires no right hand side in case " ++ showCase cl)
+           (False,Nothing) -> throwErrorMsg ("missing right hand side in case " ++ showCase cl)
+           (True,Just rhs) -> throwErrorMsg ("absurd pattern requires no right hand side in case " ++ showCase cl)
            (False,Just rhs) -> do
               -- pv <- whnf' (patternToExpr p) -- DIFFICULT FOR DOT PATTERNS!
       --        vp <- patternToVal p -- BUG: INTRODUCES FRESH GENS, BUT THEY HAVE ALREADY BEEN INTRODUCED IN checkPattern
@@ -1676,8 +1675,8 @@
       tel <- getContextTele -- WRONG TELE, has VGens for DotPs
       case (absp,mrhs) of
          (True,Nothing) -> return $ Kinded NoKind (Clause tel ple Nothing)
-         (False,Nothing) -> fail ("missing right hand side in clause " ++ show cl)
-         (True,Just rhs) -> fail ("absurd pattern requires no right hand side in clause " ++ show cl)
+         (False,Nothing) -> throwErrorMsg ("missing right hand side in clause " ++ show cl)
+         (True,Just rhs) -> throwErrorMsg ("absurd pattern requires no right hand side in clause " ++ show cl)
          (False,Just rhs) -> do
             Kinded ki rhse <- checkRHS ins rhs tv0
             env  <- getEnv
@@ -1712,7 +1711,7 @@
     VMeasured mu vb -> setMeasure mu $ checkPatterns dec0 flex ins vb pl
     VGuard beta vb -> addBoundHyp beta $ checkPatterns dec0 flex ins vb pl
 {-
-    VGuard beta vb -> fail $ "checkPattern at type " ++ show v ++ " --- introduction of constraints not supported"
+    VGuard beta vb -> throwErrorMsg $ "checkPattern at type " ++ show v ++ " --- introduction of constraints not supported"
 -}
     _ -> case pl of
       [] -> do cxt <- ask
@@ -1794,7 +1793,7 @@
 
                  co <- asks mutualCo
                  when (co /= CoInd) $
-                   fail ("successor pattern only allowed in cofun")
+                   throwErrorMsg ("successor pattern only allowed in cofun")
 
                  enterDoc (text ("checkPattern " ++ show p ++" : matching on size, checking that target") <+> prettyTCM tv <+> text "ends in correct coinductive sized type") $
                    underAbs x domEr fv $ \ i _ bv -> endsInSizedCo i bv
@@ -1911,7 +1910,7 @@
                  return (flex, ins, cxt', maybeErase $ SizeP e y, xv, False)
 
           AbsurdP -> do
-                 when (isFunType av) $ fail ("absurd pattern " ++ show p ++ " does not match function types, like " ++ show av)
+                 when (isFunType av) $ throwErrorMsg ("absurd pattern " ++ show p ++ " does not match function types, like " ++ show av)
                  cxt' <- ask
                  return (MaxMatches 0 av : flex, ins, cxt', maybeErase $ AbsurdP, VIrr, True)
 {-
@@ -1945,7 +1944,7 @@
 -}
                  (vc,(flex',ins',cxt',vc',ple,pvs,absp)) <- checkConstructorPattern co n pl
 
-                 when (isFunType vc') $ fail ("higher-order matching of pattern " ++ show p ++ " of type " ++ show vc' ++ " not allowed")
+                 when (isFunType vc') $ throwErrorMsg ("higher-order matching of pattern " ++ show p ++ " of type " ++ show vc' ++ " not allowed")
                  let flexgen = concat $ map (\ g -> case g of
                         DotFlex i _ _ -> [i]
                         _ -> []) flex'
@@ -2040,7 +2039,7 @@
       maybeErase p = if erased decEr then ErasedP p else p
 
       checkConstructorPattern co n pl = do
-                 when (isFunType av) $ fail ("higher-order matching of pattern " ++ show p ++ " at type " ++ show av ++ " not allowed")
+                 when (isFunType av) $ throwErrorMsg ("higher-order matching of pattern " ++ show p ++ " at type " ++ show av ++ " not allowed")
 -- TODO: ensure that matchings against erased arguments are forced
 --                 when (erased dec) $ throwErrorMsg $ "checkPattern: cannot match on erased argument " ++ show p ++ " : " ++ show av
 
@@ -2076,7 +2075,7 @@
         when (co == CoCons && isJust sz) $ do
           let sizep = head pl  -- 2012-01-22: WAS (pl !! nPars)
           unless (isDotPattern sizep) $
-            fail $ "in pattern " ++ show p  ++ ", coinductive size sub pattern " ++ show sizep ++ " must be dotted"
+            throwErrorMsg $ "in pattern " ++ show p  ++ ", coinductive size sub pattern " ++ show sizep ++ " must be dotted"
 
         when (not $ decEr `elem` map Dec [Const,Rec]) $
           recoverFail $ "cannot match pattern " ++ show p ++ " against non-computational argument"
@@ -2150,7 +2149,7 @@
 checkDot :: Substitution -> DotFlex -> TypeCheck ()
 checkDot subst (i,(e,it)) = enter ("dot pattern " ++ show e) $
   case (lookup i subst) of
-    Nothing -> fail $ "not instantiated"
+    Nothing -> throwErrorMsg $ "not instantiated"
     Just v -> do
       tv <- substitute subst (typ it)
       ask >>= \ ce -> traceCheckM ("checking dot pattern " ++ show ce ++ " |- " ++ show e ++ " : " ++ show (decor it) ++ " " ++ show tv)
@@ -2325,7 +2324,7 @@
       (VQuant Pi x dom fv) -> do
         vb   <- app fv v2
         instList' (np - 1) (tailPosl posl) flex vb vl1 vl2
-instList' np pos flex tv vl1 vl2 = fail $ "internal error: instList' " ++ show (np,pos,flex,tv,vl1,vl2) ++ " not handled"
+instList' np pos flex tv vl1 vl2 = throwErrorMsg $ "internal error: instList' " ++ show (np,pos,flex,tv,vl1,vl2) ++ " not handled"
 
 headPosl :: [Pol] -> Pol
 headPosl [] = mixed
@@ -2497,7 +2496,7 @@
        VQuant Pi x dom fv | isVSize (typ dom) ->
           underAbs x dom fv $ \ k xv bv -> do
             szSizeVarUsage n co p k bv
-       _ -> fail $ "not a valid sized constructor: expected size quantification"
+       _ -> throwErrorMsg $ "not a valid sized constructor: expected size quantification"
 
 szSizeVarUsage :: Name -> Co -> Int -> Int -> TVal -> TypeCheck ()
 szSizeVarUsage n co p i tv = enterDoc (text "szSizeVarUsage of" <+> prettyTCM (VGen i) <+> text "in" <+> prettyTCM tv) $
@@ -2637,7 +2636,7 @@
 admFunDef co cls tv = do
   (cls, inco) <- admClauses cls tv
   when (co==CoInd && not (co `elem` inco)) $
-    fail $ show tv ++ " is not a type of a cofun" -- ++ if co==Ind then "fun" else "cofun"
+    throwErrorMsg $ show tv ++ " is not a type of a cofun" -- ++ if co==Ind then "fun" else "cofun"
   return cls
 
 admClauses :: [Clause] -> TVal -> TypeCheck ([Clause], [Co])
@@ -2988,7 +2987,7 @@
       VApp (VDef (DefId DatK d)) vl -> do
          case p of
            ProjP n -> return (p, [])
-           _ -> fail "admPattern: IMPOSSIBLE: non-projection pattern for record type"
+           _ -> throwErrorMsg "admPattern: IMPOSSIBLE: non-projection pattern for record type"
       VQuant Pi x dom fv -> underAbs x dom fv $ \ k xv bv -> do
   {-
          if p is successor pattern
@@ -3004,7 +3003,7 @@
             else return (UnusableP p, inco)
           else return (p, [])
 
-      _ -> fail "admPattern: IMPOSSIBLE: pattern for a non-function type"
+      _ -> throwErrorMsg "admPattern: IMPOSSIBLE: pattern for a non-function type"
 
 cannotMatchDeep p tv = recoverFailDoc $
   text "cannot match against deep successor pattern"
@@ -3297,6 +3296,6 @@
                       do s <- whnfClos $ vl !! p
                          case s of
                            VGen i' | i == i' -> return ()
-                           _ -> fail $ "expected size variable"
-                  _ -> fail $ "expected (co)inductive sized type"
-         _ -> fail $ "expected (co)inductive sized type"
+                           _ -> throwErrorMsg $ "expected size variable"
+                  _ -> throwErrorMsg $ "expected (co)inductive sized type"
+         _ -> throwErrorMsg $ "expected (co)inductive sized type"
diff --git a/Util.hs b/Util.hs
--- a/Util.hs
+++ b/Util.hs
@@ -7,6 +7,7 @@
 import Prelude hiding (showList, null)
 
 import Control.Applicative hiding (empty)
+import Control.Monad
 import Control.Monad.Writer (Writer, runWriter, All, getAll)
 
 import qualified Data.List as List
@@ -68,9 +69,15 @@
 (<.>) :: Functor m => (b -> c) -> (a -> m b) -> a -> m c
 (f <.> g) a = f <$> g a
 
-liftMaybe :: (Monad m) => Maybe a -> m a
-liftMaybe = maybe (fail "Util.liftMaybe: unexpected Nothing") return
+whenM :: Monad m => m Bool -> m () -> m ()
+whenM mb k = mb >>= (`when` k)
 
+unlessM :: Monad m => m Bool -> m () -> m ()
+unlessM mb k = mb >>= (`unless` k)
+
+whenJustM :: (Monad m) => m (Maybe a) -> (a -> m ()) -> m ()
+whenJustM mm k = mm >>= (`whenJust` k)
+
 whenJust :: (Monad m) => Maybe a -> (a -> m ()) -> m ()
 whenJust (Just a) k = k a
 whenJust Nothing  k = return ()
@@ -85,9 +92,6 @@
 ifJustM :: (Monad m) => m (Maybe a) -> (a -> m b) -> m b -> m b
 ifJustM mma f mb = maybe mb f =<< mma
 
-lookupM :: (Monad m, Show k, Ord k) => k -> Map k v -> m v
-lookupM k m = maybe (fail $ "lookupM: unbound key " ++ show k) return $ Map.lookup k m
-
 mapMapM :: (Monad m, Ord k) => (a -> m b) -> Map k a -> m (Map k b)
 mapMapM f = Map.foldrWithKey step (return $ Map.empty)
   where step k a m = do a' <- f a
@@ -164,10 +168,6 @@
 headMaybe :: [a] -> Maybe a
 headMaybe [] = Nothing
 headMaybe (a:as) = Just a
-
-headM :: Monad m => [a] -> m a
-headM [] = fail "headM"
-headM (a:as) = return a
 
 firstJust :: [Maybe a] -> Maybe a
 firstJust = headMaybe . compressMaybes
diff --git a/Value.hs b/Value.hs
--- a/Value.hs
+++ b/Value.hs
@@ -167,9 +167,6 @@
 vApp f vs = VApp f vs
 -}
 
-failValInv :: (Monad m) => Val -> m a
-failValInv v = fail $ "internal error: value " ++ show v ++ " violates representation invariant"
-
 vAbs :: Name -> Int -> Val -> FVal
 vAbs x i v = VAbs x i v emptyVal
 
diff --git a/test/succeed/AgdaIssue1052.ma b/test/succeed/AgdaIssue1052.ma
new file mode 100644
--- /dev/null
+++ b/test/succeed/AgdaIssue1052.ma
@@ -0,0 +1,49 @@
+
+data Eq [A : Set] (a : A) (b : A) : Set
+{ refl : Eq A a a }
+
+fun X : Set {}
+fun f : X -> X {}
+
+data StepsTo (x, z : X) : Set
+{ done : StepsTo x x
+; next : (y : X) -> Eq X (f y) z -> StepsTo x y -> StepsTo x z
+}
+
+fun trans : (x, y, z : X) -> StepsTo x y -> StepsTo y z -> StepsTo x z
+{ trans x y .y p done          = p
+; trans x y  z p (next z' r q) = next z' r (trans x y z' p q)
+}
+
+fun const : (x, y : X) -> StepsTo x y -> Eq X (f x) x -> Eq X x y
+{ const x .x done q = refl
+-- ; const _ _  (next _ r p) q = -- TODO
+}
+
+{-
+fun bad : (x, y, z : X) -> StepsTo x z -> Eq X (f z) x -> StepsTo x y -> StepsTo y x
+{ bad x y z (next z' p q) r s =
+  next z r (bad z y _ (trans _ _ _ (next _ r done) q) p (trans _ _ _ (next _ r done) s))
+}  -- Giving up, need unification!!
+
+-}
+{-
+data _=⟨_⟩⇒*_ {X : Set}(x : X)(f : X → X) : X → Set where
+  done : x =⟨ f ⟩⇒* x
+  next : ∀{y z} → f y ≡ z → x =⟨ f ⟩⇒* y → x =⟨ f ⟩⇒* z
+
+trans* : ∀{X}{x y z}{f : X → X} → x =⟨ f ⟩⇒* y → y =⟨ f ⟩⇒* z → x =⟨ f ⟩⇒* z
+trans* p done = p
+trans* p (next r q) = next r (trans* p q)
+
+const* : ∀{X}{x y}{f : X → X} → x =⟨ f ⟩⇒* y → f x ≡ x → x ≡ y
+const* done q = refl
+const* (next r p) q with const* p q
+const* (next r p) q | refl = trans (sym q) r
+
+bad : ∀{X}{x y z}{f : X → X} → x =⟨ f ⟩⇒* z → f z ≡ x → x =⟨ f ⟩⇒* y →
+      y =⟨ f ⟩⇒* x
+bad done p q rewrite const* q p = done
+bad (next p q) r s =
+  next r (bad (trans* (next r done) q) p (trans* (next r done) s))
+-}