Set in stone the design of critical errors, fix some code around that

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.

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

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

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

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

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)

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,15 +1023,15 @@ 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!
   public export
   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

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 =