diff --git a/src/idris/Nova/Core/Context.idr b/src/idris/Nova/Core/Context.idr
index 4e2d2ea..5152e92 100644
--- a/src/idris/Nova/Core/Context.idr
+++ b/src/idris/Nova/Core/Context.idr
@@ -109,7 +109,7 @@ namespace VarName
   lookupSignatureE : Signature -> VarName -> M (Nat, SignatureEntry)
   lookupSignatureE sig x =
     case (lookupSignature sig x) of
-      Nothing => throw "Can't look up \{x} in Σ"
+      Nothing => criticalError "Can't look up \{x} in Σ"
       Just sig => return sig
 
   public export
@@ -131,7 +131,7 @@ namespace Index
   lookupSignatureE : Signature -> Nat -> M (VarName, SignatureEntry)
   lookupSignatureE sig x =
     case lookupSignature sig x of
-      Nothing => throw "lookupSignatureE failed"
+      Nothing => criticalError "lookupSignatureE failed"
       Just t => return t
 
   ||| Weakens the type.
diff --git a/src/idris/Nova/Core/Conversion.idr b/src/idris/Nova/Core/Conversion.idr
index 4bdd9db..9c76e21 100644
--- a/src/idris/Nova/Core/Conversion.idr
+++ b/src/idris/Nova/Core/Conversion.idr
@@ -24,8 +24,8 @@ mutual
     convNu sig omega OneTy OneTy = return True
     convNu sig omega UniverseTy UniverseTy = return True
     convNu sig omega (El a0) (El a1) = conv sig omega a0 a1
-    convNu sig omega (ContextSubstElim {}) b = throw "convNu(ContextSubstElim)"
-    convNu sig omega (SignatureSubstElim {}) b = throw "convNu(SignatureSubstElim)"
+    convNu sig omega (ContextSubstElim {}) b = criticalError "convNu(ContextSubstElim)"
+    convNu sig omega (SignatureSubstElim {}) b = criticalError "convNu(SignatureSubstElim)"
     convNu sig omega (OmegaVarElim x0 sigma) (OmegaVarElim x1 tau) =
      return (x0 == x1)
         `and`
@@ -84,8 +84,8 @@ mutual
       conv sig omega s0 s1
     convNu sig omega (ZeroElim _ t0) (ZeroElim _ t1) =
       conv sig omega t0 t1
-    convNu sig omega (ContextSubstElim {}) b = throw "convNu(ContextSubstElim)"
-    convNu sig omega (SignatureSubstElim {}) b = throw "convNu(SignatureSubstElim)"
+    convNu sig omega (ContextSubstElim {}) b = criticalError "convNu(ContextSubstElim)"
+    convNu sig omega (SignatureSubstElim {}) b = criticalError "convNu(SignatureSubstElim)"
     convNu sig omega (ContextVarElim x0) (ContextVarElim x1) =
       return (x0 == x1)
     convNu sig omega (SignatureVarElim x0 sigma) (SignatureVarElim x1 tau) =
@@ -112,8 +112,8 @@ mutual
     public export
     conv : Signature -> Omega -> Spine -> Spine -> M Bool
     conv sig omega [<] [<] = return True
-    conv sig omega (_ :< _) [<] = throw "conv(_ :< _, [<])"
-    conv sig omega [<] (_ :< _) = throw "conv([<], _ :< _)"
+    conv sig omega (_ :< _) [<] = criticalError "conv(_ :< _, [<])"
+    conv sig omega [<] (_ :< _) = criticalError "conv([<], _ :< _)"
     conv sig omega (ts0 :< t0) (ts1 :< t1) = conv sig omega ts0 ts1 `and` conv sig omega t0 t1
 
   namespace SubstContextNF
diff --git a/src/idris/Nova/Core/Evaluation.idr b/src/idris/Nova/Core/Evaluation.idr
index 0cd7207..d05a656 100644
--- a/src/idris/Nova/Core/Evaluation.idr
+++ b/src/idris/Nova/Core/Evaluation.idr
@@ -20,7 +20,7 @@ mutual
     closedEvalNu sig omega ZeroTy = return ZeroTy
     closedEvalNu sig omega OneTy = return OneTy
     closedEvalNu sig omega OneVal = return OneVal
-    closedEvalNu sig omega (ZeroElim ty t) = throw "closedEval(ZeroElim)"
+    closedEvalNu sig omega (ZeroElim ty t) = criticalError "closedEval(ZeroElim)"
     closedEvalNu sig omega (PiTy x a b) = return (PiTy x a b)
     closedEvalNu sig omega (ImplicitPiTy x a b) = return (ImplicitPiTy x a b)
     closedEvalNu sig omega (SigmaTy x a b) = return (SigmaTy x a b)
@@ -29,19 +29,19 @@ mutual
     closedEvalNu sig omega (SigmaVal x a b p q) = return (SigmaVal x a b p q)
     closedEvalNu sig omega (PiElim f x a b e) = M.do
       PiVal _ _ _ f <- closedEval sig omega f
-        | _ => throw "closedEval(PiElim)"
+        | _ => criticalError "closedEval(PiElim)"
       closedEval sig omega (ContextSubstElim f (Ext Terminal e))
     closedEvalNu sig omega (ImplicitPiElim f x a b e) = M.do
       ImplicitPiVal _ _ _ f <- closedEval sig omega f
-        | _ => throw "closedEval(ImplicitPiElim)"
+        | _ => criticalError "closedEval(ImplicitPiElim)"
       closedEval sig omega (ContextSubstElim f (Ext Terminal e))
     closedEvalNu sig omega (SigmaElim1 f x a b) = M.do
       SigmaVal _ _ _ p q <- closedEval sig omega f
-        | _ => throw "closedEval(SigmaElim1)"
+        | _ => criticalError "closedEval(SigmaElim1)"
       closedEval sig omega p
     closedEvalNu sig omega (SigmaElim2 f x a b) = M.do
       SigmaVal _ _ _ p q <- closedEval sig omega f
-        | _ => throw "closedEval(SigmaElim2)"
+        | _ => criticalError "closedEval(SigmaElim2)"
       closedEval sig omega q
     closedEvalNu sig omega NatVal0 = return NatVal0
     closedEvalNu sig omega (NatVal1 t) = return (NatVal1 t)
@@ -50,10 +50,10 @@ mutual
       case t of
         NatVal0 => closedEval sig omega z
         NatVal1 t => closedEval sig omega (ContextSubstElim s (Ext (Ext Terminal t) (NatElim x schema z y h s t)))
-        _ => throw "closedEval(NatElim)"
-    closedEvalNu sig omega (ContextSubstElim t sigma) = throw "closedEval(ContextSubstElim)"
-    closedEvalNu sig omega (SignatureSubstElim t sigma) = throw "closedEval(SignatureSubstElim)"
-    closedEvalNu sig omega (ContextVarElim x) = throw "closedEval(ContextVarElim)"
+        _ => criticalError "closedEval(NatElim)"
+    closedEvalNu sig omega (ContextSubstElim t sigma) = criticalError "closedEval(ContextSubstElim)"
+    closedEvalNu sig omega (SignatureSubstElim t sigma) = criticalError "closedEval(SignatureSubstElim)"
+    closedEvalNu sig omega (ContextVarElim x) = criticalError "closedEval(ContextVarElim)"
     closedEvalNu sig omega (SignatureVarElim k sigma) = M.do
       (_, LetElemEntry ctx rhs _) <- lookupSignatureE sig k
         | _ => return (SignatureVarElim k sigma)
@@ -62,7 +62,7 @@ mutual
     closedEvalNu sig omega (OmegaVarElim x sigma) = M.do
       case (lookup x omega) of
         Just (LetElem _ rhs _) => closedEval sig omega (ContextSubstElim rhs sigma)
-        _ => throw "closedEval(OmegaVarElim)"
+        _ => criticalError "closedEval(OmegaVarElim)"
     closedEvalNu sig omega (TyEqTy a0 a1) = return $ TyEqTy a0 a1
     closedEvalNu sig omega (ElEqTy a0 a1 ty) = return $ ElEqTy a0 a1 ty
     closedEvalNu sig omega (TyEqVal ty) = return (TyEqVal ty)
@@ -231,8 +231,8 @@ mutual
         NatVal0 => openEval sig omega z
         NatVal1 t => openEval sig omega (ContextSubstElim s (Ext (Ext Id t) (NatElim x schema z y h s t)))
         t => return (NatElim x schema z y h s t)
-    openEvalNu sig omega (ContextSubstElim t sigma) = throw "openEval(ContextSubstElim)"
-    openEvalNu sig omega (SignatureSubstElim t sigma) = throw "openEval(SignatureSubstElim)"
+    openEvalNu sig omega (ContextSubstElim t sigma) = criticalError "openEval(ContextSubstElim)"
+    openEvalNu sig omega (SignatureSubstElim t sigma) = criticalError "openEval(SignatureSubstElim)"
     openEvalNu sig omega (ContextVarElim x) = return (ContextVarElim x)
     openEvalNu sig omega (SignatureVarElim k sigma) = M.do
       return (SignatureVarElim k sigma)
@@ -241,12 +241,12 @@ mutual
       case (lookup k omega) of
         Just (LetElem _ rhs _) => openEval sig omega (ContextSubstElim rhs sigma)
         Just (MetaElem {}) => return (OmegaVarElim k sigma)
-        Just (LetType {}) => throw "openEval/Elem(OmegaVarElim(LetType))"
-        Just (MetaType {}) => throw "openEval/Elem(OmegaVarElim(MetaType))"
-        Just (TypeConstraint {}) => throw "openEval/Elem(OmegaVarElim(TypeConstraint))"
-        Just (ElemConstraint {}) => throw "openEval/Elem(OmegaVarElim(ElemConstraint))"
-        Just (SubstContextConstraint {}) => throw "openEval/Elem(OmegaVarElim(SubstConstraint))"
-        Nothing => throw "openEval/Elem(OmegaVarElim(Nothing))"
+        Just (LetType {}) => criticalError "openEval/Elem(OmegaVarElim(LetType))"
+        Just (MetaType {}) => criticalError "openEval/Elem(OmegaVarElim(MetaType))"
+        Just (TypeConstraint {}) => criticalError "openEval/Elem(OmegaVarElim(TypeConstraint))"
+        Just (ElemConstraint {}) => criticalError "openEval/Elem(OmegaVarElim(ElemConstraint))"
+        Just (SubstContextConstraint {}) => criticalError "openEval/Elem(OmegaVarElim(SubstConstraint))"
+        Nothing => criticalError "openEval/Elem(OmegaVarElim(Nothing))"
     openEvalNu sig omega (TyEqTy a0 a1) = return $ TyEqTy a0 a1
     openEvalNu sig omega (ElEqTy a0 a1 ty) = return $ ElEqTy a0 a1 ty
     openEvalNu sig omega (TyEqVal ty) = return (TyEqVal ty)
@@ -280,13 +280,13 @@ mutual
     closedEvalNu sig omega (PiTy x a b) = return (PiTy x a b)
     closedEvalNu sig omega (ImplicitPiTy x a b) = return (ImplicitPiTy x a b)
     closedEvalNu sig omega (SigmaTy x a b) = return (SigmaTy x a b)
-    closedEvalNu sig omega (ContextSubstElim t sigma) = throw "closedEval(ContextSubstElim)"
-    closedEvalNu sig omega (SignatureSubstElim t sigma) = throw "closedEval(SignatureSubstElim)"
+    closedEvalNu sig omega (ContextSubstElim t sigma) = criticalError "closedEval(ContextSubstElim)"
+    closedEvalNu sig omega (SignatureSubstElim t sigma) = criticalError "closedEval(SignatureSubstElim)"
     -- Σ Ω₀ (Δ ⊦ x ≔ t : T) Ω₁ ⊦ x σ = t(σ)
     closedEvalNu sig omega (OmegaVarElim x sigma) = M.do
       case (lookup x omega) of
         Just (LetType _ rhs) => closedEval sig omega (ContextSubstElim rhs sigma)
-        _ => throw "closedEval(OmegaVarElim)"
+        _ => criticalError "closedEval(OmegaVarElim)"
     closedEvalNu sig omega (TyEqTy a0 a1) = return $ TyEqTy a0 a1
     closedEvalNu sig omega (ElEqTy a0 a1 ty) = return $ ElEqTy a0 a1 ty
     closedEvalNu sig omega (SignatureVarElim k sigma) = M.do
@@ -365,19 +365,19 @@ mutual
     openEvalNu sig omega (PiTy x a b) = return (PiTy x a b)
     openEvalNu sig omega (ImplicitPiTy x a b) = return (ImplicitPiTy x a b)
     openEvalNu sig omega (SigmaTy x a b) = return (SigmaTy x a b)
-    openEvalNu sig omega (ContextSubstElim t sigma) = throw "openEval(ContextSubstElim)"
-    openEvalNu sig omega (SignatureSubstElim t sigma) = throw "openEval(SignatureSubstElim)"
+    openEvalNu sig omega (ContextSubstElim t sigma) = criticalError "openEval(ContextSubstElim)"
+    openEvalNu sig omega (SignatureSubstElim t sigma) = criticalError "openEval(SignatureSubstElim)"
     -- Σ Ω₀ (Δ ⊦ x ≔ t : T) Ω₁ ⊦ x σ = t(σ)
     openEvalNu sig omega (OmegaVarElim k sigma) = M.do
       case (lookup k omega) of
         Just (LetType _ rhs) => openEval sig omega (ContextSubstElim rhs sigma)
         Just (MetaType {}) => return (OmegaVarElim k sigma)
-        Just (LetElem {}) => throw "openEval/Type(OmegaVarElim(LetElem(\{k})))"
-        Just (MetaElem {}) => throw "openEval/Type(OmegaVarElim(MetaElem))"
-        Just (TypeConstraint {}) => throw "openEval/Type(OmegaVarElim(TypeConstraint))"
-        Just (ElemConstraint {}) => throw "openEval/Type(OmegaVarElim(ElemConstraint))"
-        Just (SubstContextConstraint {}) => throw "openEval/Type(OmegaVarElim(SubstConstraint))"
-        Nothing => throw "openEval/Type(OmegaVarElim(Nothing))"
+        Just (LetElem {}) => criticalError "openEval/Type(OmegaVarElim(LetElem(\{k})))"
+        Just (MetaElem {}) => criticalError "openEval/Type(OmegaVarElim(MetaElem))"
+        Just (TypeConstraint {}) => criticalError "openEval/Type(OmegaVarElim(TypeConstraint))"
+        Just (ElemConstraint {}) => criticalError "openEval/Type(OmegaVarElim(ElemConstraint))"
+        Just (SubstContextConstraint {}) => criticalError "openEval/Type(OmegaVarElim(SubstConstraint))"
+        Nothing => criticalError "openEval/Type(OmegaVarElim(Nothing))"
     openEvalNu sig omega (TyEqTy a0 a1) = return $ TyEqTy a0 a1
     openEvalNu sig omega (ElEqTy a0 a1 ty) = return $ ElEqTy a0 a1 ty
     openEvalNu sig omega (SignatureVarElim k sigma) = M.do
diff --git a/src/idris/Nova/Core/Monad.idr b/src/idris/Nova/Core/Monad.idr
index ce4f6d5..cd5f1fe 100644
--- a/src/idris/Nova/Core/Monad.idr
+++ b/src/idris/Nova/Core/Monad.idr
@@ -8,10 +8,36 @@ import Data.SnocList
 
 import Nova.Core.Language
 
+||| Critical/unexpected/unrecoverable error.
+public export
+record CriticalError where
+  constructor MkCriticalError
+  msg : String
+
+public export
+Show CriticalError where
+  show (MkCriticalError x) = "Critical error:\n\{x}"
+
+||| The error type is a type represents critical unexpected unrecoverable errors.
+||| By design, we are not supposed to ever try/catch those!
+||| Don't use CriticalError for any other kind of error (e.g. recoverable / expected).
+||| FIX: we should rename this one!
 public export
 M : Type -> Type
---               vvvvvv for critical errors only
-M = JustAMonad.M String ()
+M = JustAMonad.M CriticalError ()
+
+%inline
+public export
+criticalError : (msg : String) -> JustAMonad.M CriticalError st a
+criticalError msg = M.do
+  throw (MkCriticalError msg)
+
+public export
+asCriticalError : JustAMonad.M CriticalError st (Either String a) -> JustAMonad.M CriticalError st a
+asCriticalError f = M.do
+  case !f of
+    Left err => criticalError err
+    Right ok => return ok
 
 namespace M
   %inline
@@ -95,6 +121,13 @@ namespace MEither
   error : e' -> M e s (Either e' a)
   error x = M.return (Left x)
 
+  public export
+  mapError : (e -> e') -> M e0 s (Either e a) -> M e0 s (Either e' a)
+  mapError f m = M.do
+    case !m of
+      Left err => return (Left (f err))
+      Right ok => return ok
+
   public export
   liftM : M e s a -> M e s (Either e' a)
   liftM f = M.do
diff --git a/src/idris/Nova/Core/Pretty.idr b/src/idris/Nova/Core/Pretty.idr
index 8913155..f26b592 100644
--- a/src/idris/Nova/Core/Pretty.idr
+++ b/src/idris/Nova/Core/Pretty.idr
@@ -239,7 +239,7 @@ wrapElem (ElEqVal {}) lvl doc =
 ||| that have the *same root*.
 public export
 localise : SnocList VarName -> Nat -> M (VarName, Nat)
-localise [<] idx = throw "Exception in 'localise'"
+localise [<] idx = criticalError "Critical error in 'localise'"
 localise (xs :< x) Z = return (x, 0)
 localise (xs :< x) (S k) = M.do
   (name, idx) <- localise xs k
diff --git a/src/idris/Nova/Core/Shrinking.idr b/src/idris/Nova/Core/Shrinking.idr
index a51050a..93c71f5 100644
--- a/src/idris/Nova/Core/Shrinking.idr
+++ b/src/idris/Nova/Core/Shrinking.idr
@@ -77,8 +77,8 @@ mutual
       return OneTy
     shrinkNu UniverseTy gamma1Len gamma2Len = MMaybe.do
       return UniverseTy
-    shrinkNu (ContextSubstElim x y) gamma1Len gamma2Len = throw "shrink(ContextSubstElim)"
-    shrinkNu (SignatureSubstElim x y) gamma1Len gamma2Len = throw "shrink(SignatureSubstElim)"
+    shrinkNu (ContextSubstElim x y) gamma1Len gamma2Len = criticalError "shrink(ContextSubstElim)"
+    shrinkNu (SignatureSubstElim x y) gamma1Len gamma2Len = criticalError "shrink(SignatureSubstElim)"
     shrinkNu (OmegaVarElim k sigma) gamma1Len gamma2Len = MMaybe.do
       -- Σ₀ (Γ ⊦ χ : A) Σ₁ ⊦ σ : Δ ⇒ Γ
       -- Σ₀ (Γ ⊦ χ : A) Σ₁ Δ ⊦ χ σ
@@ -190,8 +190,8 @@ mutual
       ty <- shrink ty gamma1Len gamma2Len
       t <- shrink t gamma1Len gamma2Len
       return (ZeroElim ty t)
-    shrinkNu (ContextSubstElim x y) gamma1Len gamma2Len = throw "shrink(ContextSubstElim)"
-    shrinkNu (SignatureSubstElim x y) gamma1Len gamma2Len = throw "shrink(SignatureSubstElim)"
+    shrinkNu (ContextSubstElim x y) gamma1Len gamma2Len = criticalError "shrink(ContextSubstElim)"
+    shrinkNu (SignatureSubstElim x y) gamma1Len gamma2Len = criticalError "shrink(SignatureSubstElim)"
     shrinkNu (ContextVarElim k) gamma1Len gamma2Len =
       case k < gamma2Len of
         True => return (ContextVarElim k)
diff --git a/src/idris/Nova/Core/Unification.idr b/src/idris/Nova/Core/Unification.idr
index 33ec893..8851c08 100644
--- a/src/idris/Nova/Core/Unification.idr
+++ b/src/idris/Nova/Core/Unification.idr
@@ -36,10 +36,12 @@ public export
 initialUnifySt : UnifySt
 initialUnifySt = MkUnifySt 0
 
+||| The error type is a type represents critical unexpected unrecoverable errors.
+||| By design, we are not supposed to ever try/catch those!
+||| Don't use CriticalError for any other kind of error (e.g. recoverable / expected).
 public export
 UnifyM : Type -> Type
-  --                  vvvvvv for critical errors only
-UnifyM = JustAMonad.M String UnifySt
+UnifyM = JustAMonad.M CriticalError UnifySt
 
 namespace UnifyM
   public export
@@ -54,13 +56,6 @@ namespace UnifyM
     liftM f = M.do
       UnifyM.liftM f <&> Just
 
-public export
-liftMEither : M (Either String a) -> UnifyM a
-liftMEither f = M.do
- case !(UnifyM.liftM f) of
-   Right x => return x
-   Left err => throw err
-
 public export
 nextOmegaName : UnifyM OmegaName
 nextOmegaName = M.do
@@ -1028,7 +1023,7 @@ namespace Named
   newTypeMeta : Omega -> Context -> OmegaName -> MetaKind -> UnifyM Omega
   newTypeMeta omega ctx n k = M.do
     case lookup n omega of
-      Just _ => throw "newTypeMeta, name already exists: \{n}"
+      Just _ => criticalError "newTypeMeta, name already exists: \{n}"
       Nothing => return (insert (n, MetaType ctx k) omega)
 
   ||| The name must be unique!
@@ -1036,7 +1031,7 @@ namespace Named
   newElemMeta : Omega -> Context -> OmegaName -> Typ -> MetaKind -> UnifyM Omega
   newElemMeta omega ctx n ty k = M.do
     case lookup n omega of
-      Just _ => throw "newElemMeta, name already exists: \{n}"
+      Just _ => criticalError "newElemMeta, name already exists: \{n}"
       Nothing => return (insert (n, MetaElem ctx ty k) omega)
 
 namespace Nameless
diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Elem.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Elem.idr
index 21aa336..ad4c97c 100644
--- a/src/idris/Nova/Surface/Elaboration/Implementation/Elem.idr
+++ b/src/idris/Nova/Surface/Elaboration/Implementation/Elem.idr
@@ -456,7 +456,7 @@ elabElemNuOtherwise ops sig omega ctx (Tac r alpha) meta ty = M.do
     | Left (r, reason) => return (Stuck ("At" ++ show r ++ ", reason: " ++ renderDocTerm reason))
     | Right (_, interp) => return (Error "Source signature of the tactic must be ε, but it is not.")
   let [< ElemEntryInstance solution] = interp [<]
-    | _ => throw "elabElemNuOtherwise(Tac)"
+    | _ => criticalError "elabElemNuOtherwise(Tac)"
   let omega = instantiateByElaboration omega meta solution
   return (Success omega [])
 elabElemNuOtherwise ops sig omega ctx (App r (Underscore r0) _) meta ty =
diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/NormaliseCommutativeMonoid.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/NormaliseCommutativeMonoid.idr
index 7e13ef0..5aa8239 100644
--- a/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/NormaliseCommutativeMonoid.idr
+++ b/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/NormaliseCommutativeMonoid.idr
@@ -108,29 +108,33 @@ elabNormaliseComm ops sig omega r path (vars ** monoidTm) monoidInst (target :<
          ⨯ ((x y : A) → x + y ≡ y + x ∈ A)
     """
   let Right (_, synty) = parseFull' (MkParsingSt [<]) (term 0) synty
-    | Left err => throw (show err)
+    | Left err => criticalError (show err)
   (omega, tymidx) <- MEither.liftM $ liftUnifyM $ newTypeMeta omega [<] SolveByElaboration
   let commMonoidTy = Typ.OmegaVarElim tymidx Terminal
-  let prob1 = TypeElaboration [<] !(MEither.liftM $ Elab.liftM $ shunt (cast ops) synty 0 `M.(>>=)` M.fromEither) tymidx
+  let prob1 = TypeElaboration [<] !(MEither.mapError (\x => (r, pretty x)) $ Elab.liftM $ shunt (cast ops) synty 0) tymidx
   Success omega <- MEither.liftM $ solve @{MkParams Nothing {solveNamedHoles = False}} ops sig omega [prob1]
     | Stuck omega stuckElab stuckCons => M.do
          write "(Unexpected error) Result elaborating expected monoid type in elabNormaliseComm (stuck):"
          write (renderDocTerm !(Elab.liftM $ prettyTyp sig omega [<] commMonoidTy 0))
-         throw $ renderDocTerm !(Elab.liftM $ pretty sig (Stuck omega stuckElab stuckCons))
-    | Error omega (Left (elab, err)) => throw $ renderDocTerm !(Elab.liftM $ pretty sig (ElaborationError omega (elab, err)))
-    | Error omega (Right (con, err)) => throw $ renderDocTerm !(Elab.liftM $ pretty sig (UnificationError omega (con, err)))
+         criticalError $ renderDocTerm !(Elab.liftM $ pretty sig (Stuck omega stuckElab stuckCons))
+    | Error omega (Left (elab, err)) => MEither.do
+      error (r, !(MEither.liftM $ Elab.liftM $ pretty sig (ElaborationError omega (elab, err))))
+    | Error omega (Right (con, err)) => MEither.do
+      error (r, !(MEither.liftM $ Elab.liftM $ pretty sig (UnificationError omega (con, err))))
 
 
   (omega, monoidInstIdx) <- MEither.liftM $ liftUnifyM $ newElemMeta omega [<] commMonoidTy SolveByElaboration
   let monoidInstTm = Elem.OmegaVarElim monoidInstIdx Terminal
   let prob1 = ElemElaboration [<] monoidInst monoidInstIdx commMonoidTy
   Success omega <- MEither.liftM $ solve ops sig omega [prob1]
-    | Stuck omega stuckElab stuckCons => M.do
-         write "Result elaborating monoid type in elabNormaliseComm (stuck):"
-         write (renderDocTerm !(Elab.liftM $ prettyElem sig omega [<] monoidInstTm 0))
-         throw $ renderDocTerm !(Elab.liftM $ pretty sig (Stuck omega stuckElab stuckCons))
-    | Error omega (Left (elab, err)) => throw $ renderDocTerm !(Elab.liftM $ pretty sig (ElaborationError omega (elab, err)))
-    | Error omega (Right (con, err)) => throw $ renderDocTerm !(Elab.liftM $ pretty sig (UnificationError omega (con, err)))
+    | Stuck omega stuckElab stuckCons => MEither.do
+         MEither.liftM $ write "Result elaborating monoid type in elabNormaliseComm (stuck):"
+         MEither.liftM $ write (renderDocTerm !(MEither.liftM $ Elab.liftM $ prettyElem sig omega [<] monoidInstTm 0))
+         error (r, !(MEither.liftM $ Elab.liftM $ pretty sig (Stuck omega stuckElab stuckCons)))
+    | Error omega (Left (elab, err)) => MEither.do
+      error (r, !(MEither.liftM $ Elab.liftM $ pretty sig (ElaborationError omega (elab, err))))
+    | Error omega (Right (con, err)) => MEither.do
+      error (r, !(MEither.liftM $ Elab.liftM $ pretty sig (UnificationError omega (con, err))))
 
 
   -- FIX: I totally hate this. This will be fixed by nameless representation of Ω though. We should speed up the migration!
@@ -139,18 +143,18 @@ elabNormaliseComm ops sig omega r path (vars ** monoidTm) monoidInst (target :<
   pindex <- MEither.liftM $ liftUnifyM $ Unification.nextOmegaIdx
   let syntm0 = "?Aₘ\{natToSubscript aindex}, ?zₘ\{natToSubscript zindex}, ?pₘ\{natToSubscript pindex}, ?"
   let Right (_, syntm0) = parseFull' (MkParsingSt [<]) (term 0) syntm0
-    | Left err => throw (show err)
+    | Left err => criticalError (show err)
   (omega, midx0) <- MEither.liftM $ liftUnifyM $ newElemMeta omega [<] commMonoidTy SolveByElaboration
-  let prob2 = ElemElaboration [<] !(MEither.liftM $ Elab.liftM $ shunt (cast ops) syntm0 0 `M.(>>=)` M.fromEither) midx0 commMonoidTy
+  let prob2 = ElemElaboration [<] !(MEither.mapError (\x => (r, pretty x)) $ Elab.liftM $ shunt (cast ops) syntm0 0) midx0 commMonoidTy
   let el0 = OmegaVarElim midx0 Terminal
   omega <- MEither.liftM $ liftUnifyM $ addConstraint omega (ElemConstraint [<] el0 monoidInstTm commMonoidTy)
   Success omega <- MEither.liftM $ solve @{MkParams Nothing {solveNamedHoles = True}} ops sig omega [prob2]
-    | Stuck omega stuckElab stuckCons => M.do
-         write "Result of postProblem1 (stuck):"
-         write (renderDocTerm !(Elab.liftM $ prettyElem sig omega [<] el0 0))
-         throw $ renderDocTerm !(Elab.liftM $ pretty sig (Stuck omega stuckElab stuckCons))
-    | Error omega (Left (elab, err)) => throw $ renderDocTerm !(Elab.liftM $ pretty sig (ElaborationError omega (elab, err)))
-    | Error omega (Right (con, err)) => throw $ renderDocTerm !(Elab.liftM $ pretty sig (UnificationError omega (con, err)))
+    | Stuck omega stuckElab stuckCons => MEither.do
+         MEither.liftM $ write "Result of postProblem1 (stuck):"
+         MEither.liftM $ write (renderDocTerm !(MEither.liftM $ Elab.liftM $ prettyElem sig omega [<] el0 0))
+         error (r, !(MEither.liftM $ Elab.liftM $ pretty sig (Stuck omega stuckElab stuckCons)))
+    | Error omega (Left (elab, err)) => error (r, !(MEither.liftM $ Elab.liftM $ pretty sig (ElaborationError omega (elab, err))))
+    | Error omega (Right (con, err)) => error (r, !(MEither.liftM $ Elab.liftM $ pretty sig (UnificationError omega (con, err))))
   let monoidTy = El (Elem.OmegaVarElim "Aₘ\{natToSubscript aindex}" Terminal)
   let monoidZero = Elem.OmegaVarElim "zₘ\{natToSubscript zindex}" Terminal
   let monoidPlus = Elem.OmegaVarElim "pₘ\{natToSubscript pindex}" Terminal
diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/Unfold.idr b/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/Unfold.idr
index a49e18e..161e76a 100644
--- a/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/Unfold.idr
+++ b/src/idris/Nova/Surface/Elaboration/Implementation/Tactic/Unfold.idr
@@ -65,14 +65,14 @@ mutual
               case x == y of
                 True => return tm
                 False => error r
-            Nothing => throw "applyUnfoldNu(SignatureVarElim)"
+            Nothing => criticalError "applyUnfoldNu(SignatureVarElim)"
         False => error r
     applyUnfoldNu sig omega ctx tm@(SignatureVarElim x sigma) (App r (Box _) []) = MEither.do
       case lookupSignature sig x of
         Just (x, LetTypeEntry ctx rhs) =>
           return (ContextSubstElim rhs sigma)
         Just (x, _) => error r
-        Nothing => throw "applyUnfoldNu(SignatureVarElim)"
+        Nothing => criticalError "applyUnfoldNu(SignatureVarElim)"
     applyUnfoldNu sig omega ctx (SignatureVarElim x sigma) p = error (range p)
 
     public export
@@ -205,9 +205,9 @@ mutual
               case x == y of
                 True => return tm
                 False => error r
-            Nothing => throw "applyUnfoldNu(SignatureVarElim)"
+            Nothing => criticalError "applyUnfoldNu(SignatureVarElim)"
         False => error r
-    applyUnfoldNu sig omega ctx (SignatureVarElim x sigma) p = throw "applyUnfold(1): \{show p}"
+    applyUnfoldNu sig omega ctx (SignatureVarElim x sigma) p = criticalError "applyUnfold(1): \{show p}"
 
     public export
     applyUnfoldNuHelper : Signature -> Omega -> Elem -> Range -> M (Either Range Elem)
@@ -243,7 +243,7 @@ mutual
         Just (x, LetElemEntry ctx rhs ty) =>
           return (ContextSubstElim rhs sigma)
         Just (x, _) => error r
-        Nothing => throw "applyUnfoldNu(SignatureVarElim)"
+        Nothing => criticalError "applyUnfoldNu(SignatureVarElim)"
     applyUnfoldNuHelper sig omega (OmegaVarElim str x) r = error r
     applyUnfoldNuHelper sig omega (TyEqTy x y) r = error r
     applyUnfoldNuHelper sig omega (ElEqTy x y z) r = error r
diff --git a/src/idris/Nova/Surface/Elaboration/Implementation/TopLevel.idr b/src/idris/Nova/Surface/Elaboration/Implementation/TopLevel.idr
index 991493f..e47dc49 100644
--- a/src/idris/Nova/Surface/Elaboration/Implementation/TopLevel.idr
+++ b/src/idris/Nova/Surface/Elaboration/Implementation/TopLevel.idr
@@ -101,24 +101,25 @@ elabTopLevelSyn ops sig omega (Syntax r op) =
   return (Right (ops :< op, sig, omega))
 elabTopLevelSyn ops sig omega (TypingSignature r x ty) = M.do
   -- write "Before shunting:\n\{show (TypingSignature r x ty)}"
-  Right (sig, omega) <- elabTopLevelEntry ops sig omega !(liftMEither $ shuntTopLevel (cast ops) (TypingSignature r x ty))
+  -- FIX:                                                              vvvvvvvvvvvvvvv shouldn't be critical error
+  Right (sig, omega) <- elabTopLevelEntry ops sig omega !(Elab.liftM $ asCriticalError $ shuntTopLevel (cast ops) (TypingSignature r x ty))
     | Left err => return (Left (x, r, sig, err))
   return (Right (ops, sig, omega))
 elabTopLevelSyn ops sig omega (LetSignature r x ty rhs) = M.do
   -- write "Before shunting:\n\{show (LetSignature r x ty rhs)}"
-  Right (sig, omega) <- elabTopLevelEntry ops sig omega !(liftMEither $ shuntTopLevel (cast ops) (LetSignature r x ty rhs))
+  Right (sig, omega) <- elabTopLevelEntry ops sig omega !(Elab.liftM $ asCriticalError $ shuntTopLevel (cast ops) (LetSignature r x ty rhs))
     | Left err => return (Left (x, r, sig, err))
   return (Right (ops, sig, omega))
 elabTopLevelSyn ops sig omega (LetTypeSignature r x rhs) = M.do
-  Right (sig, omega) <- elabTopLevelEntry ops sig omega !(liftMEither $ shuntTopLevel (cast ops) (LetTypeSignature r x rhs))
+  Right (sig, omega) <- elabTopLevelEntry ops sig omega !(Elab.liftM $ asCriticalError $ shuntTopLevel (cast ops) (LetTypeSignature r x rhs))
     | Left err => return (Left (x, r, sig, err))
   return (Right (ops, sig, omega))
 elabTopLevelSyn ops sig omega (DefineTypeSignature r x rhs) = M.do
-  Right (sig, omega) <- elabTopLevelEntry ops sig omega !(liftMEither $ shuntTopLevel (cast ops) (DefineTypeSignature r x rhs))
+  Right (sig, omega) <- elabTopLevelEntry ops sig omega !(Elab.liftM $ asCriticalError $ shuntTopLevel (cast ops) (DefineTypeSignature r x rhs))
     | Left err => return (Left (x, r, sig, err))
   return (Right (ops, sig, omega))
 elabTopLevelSyn ops sig omega (DefineSignature r x ty rhs) = M.do
-  Right (sig, omega) <- elabTopLevelEntry ops sig omega !(liftMEither $ shuntTopLevel (cast ops) (DefineSignature r x ty rhs))
+  Right (sig, omega) <- elabTopLevelEntry ops sig omega !(Elab.liftM $ asCriticalError $ shuntTopLevel (cast ops) (DefineSignature r x ty rhs))
     | Left err => return (Left (x, r, sig, err))
   return (Right (ops, sig, omega))
 
diff --git a/src/idris/Nova/Surface/Elaboration/Interface.idr b/src/idris/Nova/Surface/Elaboration/Interface.idr
index 2ef2b30..614880c 100644
--- a/src/idris/Nova/Surface/Elaboration/Interface.idr
+++ b/src/idris/Nova/Surface/Elaboration/Interface.idr
@@ -42,9 +42,12 @@ public export
 initialElabSt : ElabSt
 initialElabSt = MkElabSt initialUnifySt [<] empty
 
+||| The error type is a type represents critical unexpected unrecoverable errors.
+||| By design, we are not supposed to ever try/catch those!
+||| Don't use CriticalError for any other kind of error (e.g. recoverable / expected).
 public export
 ElabM : Type -> Type
-ElabM = JustAMonad.M String ElabSt
+ElabM = JustAMonad.M CriticalError ElabSt
 
 namespace Elab
   public export
@@ -60,13 +63,6 @@ namespace ElabEither
     t <- Elab.liftM f
     return (Right t)
 
-public export
-liftMEither : M (Either String a) -> ElabM a
-liftMEither f = M.do
- case !(Elab.liftM f) of
-   Right x => return x
-   Left err => throw err
-
 public export
 liftUnifyM : UnifyM a -> ElabM a
 liftUnifyM f = M.do
diff --git a/src/idris/Nova/Surface/ModuleSystem.idr b/src/idris/Nova/Surface/ModuleSystem.idr
index 3d4e398..5f1fe13 100644
--- a/src/idris/Nova/Surface/ModuleSystem.idr
+++ b/src/idris/Nova/Surface/ModuleSystem.idr
@@ -72,19 +72,19 @@ postProblem1 ops sig omega = M.do
          ⨯ ((x y : A) → x + y ≡ y + x ∈ A)
     """
   let Right (_, syntm0) = parseFull' (MkParsingSt [<]) (term 0) syntm0
-    | Left err => throw (show err)
+    | Left err => criticalError (show err)
   let Right (_, syntm1) = parseFull' (MkParsingSt [<]) (term 0) syntm1
-    | Left err => throw (show err)
+    | Left err => criticalError (show err)
   let Right (_, synty) = parseFull' (MkParsingSt [<]) (term 0) synty
-    | Left err => throw (show err)
+    | Left err => criticalError (show err)
   let params = MkParams Nothing {solveNamedHoles = True}
   (omega, tymidx) <- liftUnifyM $ newTypeMeta omega [<] SolveByElaboration
   let ty = Typ.OmegaVarElim tymidx Terminal
   (omega, midx0) <- liftUnifyM $ newElemMeta omega [<] ty SolveByElaboration
   (omega, midx1) <- liftUnifyM $ newElemMeta omega [<] ty SolveByElaboration
-  let prob1 = TypeElaboration [<] !(Elab.liftM $ shunt (cast ops) synty 0 >>= M.fromEither) tymidx
-  let prob2 = ElemElaboration [<] !(Elab.liftM $ shunt (cast ops) syntm0 0 >>= M.fromEither) midx0 ty
-  let prob3 = ElemElaboration [<] !(Elab.liftM $ shunt (cast ops) syntm1 0 >>= M.fromEither) midx1 ty
+  let prob1 = TypeElaboration [<] !(Elab.liftM $ asCriticalError $ shunt (cast ops) synty 0) tymidx
+  let prob2 = ElemElaboration [<] !(Elab.liftM $ asCriticalError $ shunt (cast ops) syntm0 0) midx0 ty
+  let prob3 = ElemElaboration [<] !(Elab.liftM $ asCriticalError$ shunt (cast ops) syntm1 0) midx1 ty
   let el0 = OmegaVarElim midx0 Terminal
   let el1 = OmegaVarElim midx1 Terminal
   omega <- liftUnifyM $ addConstraint omega (ElemConstraint [<] el0 el1 ty)
@@ -92,9 +92,9 @@ postProblem1 ops sig omega = M.do
     | Stuck omega stuckElab stuckCons => M.do
          write "Result of postProblem1 (stuck):"
          write (renderDocTerm !(Elab.liftM $ prettyElem sig omega [<] el0 0))
-         throw $ renderDocTerm !(Elab.liftM $ pretty sig (Stuck omega stuckElab stuckCons))
-    | Error omega (Left (elab, err)) => throw $ renderDocTerm !(Elab.liftM $ pretty sig (ElaborationError omega (elab, err)))
-    | Error omega (Right (con, err)) => throw $ renderDocTerm !(Elab.liftM $ pretty sig (UnificationError omega (con, err)))
+         criticalError $ renderDocTerm !(Elab.liftM $ pretty sig (Stuck omega stuckElab stuckCons))
+    | Error omega (Left (elab, err)) => criticalError $ renderDocTerm !(Elab.liftM $ pretty sig (ElaborationError omega (elab, err)))
+    | Error omega (Right (con, err)) => criticalError $ renderDocTerm !(Elab.liftM $ pretty sig (UnificationError omega (con, err)))
   write "Result of postProblem1:"
   write (renderDocTerm !(Elab.liftM $ prettyElem sig omega [<] el0 0))
   return (sig, omega)
@@ -106,15 +106,15 @@ postProblem2 : SnocList Operator
             -> ElabM (Signature, Omega)
 postProblem2 ops sig omega = M.do
   let Right (_, syntm) = parseFull' (MkParsingSt [<]) (term 0) "four"
-    | Left err => throw (show err)
+    | Left err => criticalError (show err)
   let params = MkParams Nothing {solveNamedHoles = True}
   (omega, midx) <- liftUnifyM $ newElemMeta omega [<] NatTy SolveByElaboration
   let myResult = Elem.OmegaVarElim midx Terminal
-  let prob1 = ElemElaboration [<] !(Elab.liftM $ shunt (cast ops) syntm 0 >>= M.fromEither) midx NatTy
+  let prob1 = ElemElaboration [<] !(Elab.liftM $ asCriticalError $ shunt (cast ops) syntm 0) midx NatTy
   Success omega <- solve ops sig omega [prob1]
-    | Stuck omega stuckElab stuckCons => throw $ renderDocTerm !(Elab.liftM $ pretty sig (Stuck omega stuckElab stuckCons))
-    | Error omega (Left (elab, err)) => throw $ renderDocTerm !(Elab.liftM $ pretty sig (ElaborationError omega (elab, err)))
-    | Error omega (Right (con, err)) => throw $ renderDocTerm !(Elab.liftM $ pretty sig (UnificationError omega (con, err)))
+    | Stuck omega stuckElab stuckCons => criticalError $ renderDocTerm !(Elab.liftM $ pretty sig (Stuck omega stuckElab stuckCons))
+    | Error omega (Left (elab, err)) => criticalError $ renderDocTerm !(Elab.liftM $ pretty sig (ElaborationError omega (elab, err)))
+    | Error omega (Right (con, err)) => criticalError $ renderDocTerm !(Elab.liftM $ pretty sig (UnificationError omega (con, err)))
   write "Result of postProblem2:"
   write (renderDocTerm !(Elab.liftM $ prettyElem sig omega [<] !(Elab.liftM $ closedNormalise sig omega myResult) 0))
   return (sig, omega)
@@ -143,21 +143,21 @@ checkModule ops sig omega nextOmegaIdx namedHoles novaDirectory modName = Prelud
     | Right (MkElabSt (MkUnifySt nextOmegaIdx) moreToks namedHoles, Left (x, range, sig, err)) => Prelude.do
        Right doc <- eval (pretty sig err) ()
          | Left err => Prelude.do
-             pure $ Left (Just range, pretty ("Critical error:" ++ err))
+             pure $ Left (Just range, pretty ("Critical error:" ++ show err))
        pure (Left (Just range, pretty "Error while elaborating top-level definition (#\{show (length sig)}) \{x}" <+> hardline <+> doc))
     | Left err => Prelude.do
-        pure $ Left (Nothing, pretty ("Critical error:" ++ err))
+        pure $ Left (Nothing, pretty ("Critical error:" ++ show err))
   putStrLn "File elaborated successfully!"
   putStrLn "------------ Named holes ---------------"
   for_ (List.inorder omega) $ \(x, e) => Prelude.do
     case e of
       MetaType ctx NoSolve => Prelude.do
         Right doc <- eval (prettyOmegaEntry sig omega x e) ()
-          | Left err => die err -- Those should never fail
+          | Left err => die (show err) -- Those should never fail
         putStrLn (renderDocTerm doc)
       MetaElem ctx ty NoSolve => Prelude.do
         Right doc <- eval (prettyOmegaEntry sig omega x e) ()
-          | Left err => die err -- Those should never fail
+          | Left err => die (show err) -- Those should never fail
         putStrLn (renderDocTerm doc)
       _ => Prelude.do
         pure ()
@@ -201,7 +201,7 @@ checkEverything : SnocList Operator
 checkEverything ops sig omega nextOmegaIdx namedHoles toks novaDirectory modNames = IOEither.do
   (ops, sig, omega, nextOmegaIdx, namedHoles, ntoks) <- checkModules ops sig omega nextOmegaIdx namedHoles toks novaDirectory modNames
   (MkElabSt (MkUnifySt nextOmegaIdx) moreToks namedHoles, (sig, omega)) <-
-    map (bimap (\x => (Nothing, Nothing, pretty x)) id) (run (postProblem2 ops sig omega) (MkElabSt (MkUnifySt nextOmegaIdx) [<] namedHoles))
+    map (bimap (\x => (Nothing, Nothing, pretty (show x))) id) (run (postProblem2 ops sig omega) (MkElabSt (MkUnifySt nextOmegaIdx) [<] namedHoles))
   pure (ops, sig, omega, nextOmegaIdx, namedHoles, ntoks)