[ elab ] Make any error in elab script to produce a special error type

src/Core/Context.idr

@@ -778,6 +778,7 @@ HasNames Error where
     = BadDotPattern fc <$> full gam rho <*> pure x <*> full gam s <*> full gam t
   full gam (BadImplicit fc x) = pure (BadImplicit fc x)
   full gam (BadRunElab fc rho s desc) = BadRunElab fc <$> full gam rho <*> full gam s <*> pure desc
+  full gam (RunElabFail e) = RunElabFail <$> full gam e
   full gam (GenericMsg fc x) = pure (GenericMsg fc x)
   full gam (TTCError x) = pure (TTCError x)
   full gam (FileErr x y) = pure (FileErr x y)
@@ -866,6 +867,7 @@ HasNames Error where
     = BadDotPattern fc <$> resolved gam rho <*> pure x <*> resolved gam s <*> resolved gam t
   resolved gam (BadImplicit fc x) = pure (BadImplicit fc x)
   resolved gam (BadRunElab fc rho s desc) = BadRunElab fc <$> resolved gam rho <*> resolved gam s <*> pure desc
+  resolved gam (RunElabFail e) = RunElabFail <$> resolved gam e
   resolved gam (GenericMsg fc x) = pure (GenericMsg fc x)
   resolved gam (TTCError x) = pure (TTCError x)
   resolved gam (FileErr x y) = pure (FileErr x y)

src/Core/Core.idr

@@ -151,6 +151,7 @@ data Error : Type where
      BadImplicit : FC -> String -> Error
      BadRunElab : {vars : _} ->
                   FC -> Env Term vars -> Term vars -> (description : String) -> Error
+     RunElabFail : Error -> Error
      GenericMsg : FC -> String -> Error
      TTCError : TTCErrorMsg -> Error
      FileErr : String -> FileError -> Error
@@ -334,6 +335,7 @@ Show Error where
            " - it elaborates to " ++ show y
   show (BadImplicit fc str) = show fc ++ ":" ++ str ++ " can't be bound here"
   show (BadRunElab fc env script desc) = show fc ++ ":Bad elaborator script " ++ show script ++ " (" ++ desc ++ ")"
+  show (RunElabFail e) = "Error during reflection: " ++ show e
   show (GenericMsg fc str) = show fc ++ ":" ++ str
   show (TTCError msg) = "Error in TTC file: " ++ show msg
   show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err
@@ -438,6 +440,7 @@ getErrorLoc (MatchTooSpecific loc _ _) = Just loc
 getErrorLoc (BadDotPattern loc _ _ _ _) = Just loc
 getErrorLoc (BadImplicit loc _) = Just loc
 getErrorLoc (BadRunElab loc _ _ _) = Just loc
+getErrorLoc (RunElabFail e) = getErrorLoc e
 getErrorLoc (GenericMsg loc _) = Just loc
 getErrorLoc (TTCError _) = Nothing
 getErrorLoc (FileErr _ _) = Nothing
@@ -520,6 +523,7 @@ killErrorLoc (MatchTooSpecific fc x y) = MatchTooSpecific emptyFC x y
 killErrorLoc (BadDotPattern fc x y z w) = BadDotPattern emptyFC x y z w
 killErrorLoc (BadImplicit fc x) = BadImplicit emptyFC x
 killErrorLoc (BadRunElab fc x y description) = BadRunElab emptyFC x y description
+killErrorLoc (RunElabFail e) = RunElabFail $ killErrorLoc e
 killErrorLoc (GenericMsg fc x) = GenericMsg emptyFC x
 killErrorLoc (TTCError x) = TTCError x
 killErrorLoc (FileErr x y) = FileErr x y

src/Idris/Error.idr

@@ -106,6 +106,7 @@ Eq Error where
   BadDotPattern fc1 rho1 x1 s1 t1 == BadDotPattern fc2 rho2 x2 s2 t2 = fc1 == fc2
   BadImplicit fc1 x1 == BadImplicit fc2 x2 = fc1 == fc2 && x1 == x2
   BadRunElab fc1 rho1 s1 d1 == BadRunElab fc2 rho2 s2 d2 = fc1 == fc2 && d1 == d2
+  RunElabFail e1 == RunElabFail e2 = e1 == e2
   GenericMsg fc1 x1 == GenericMsg fc2 x2 = fc1 == fc2 && x1 == x2
   TTCError x1 == TTCError x2 = x1 == x2
   FileErr x1 y1 == FileErr x2 y2 = x1 == x2 && y1 == y2
@@ -595,6 +596,8 @@ perrorRaw (BadRunElab fc env script desc)
     = pure $ errorDesc (reflow "Bad elaborator script" <++> code !(pshow env script)
        <++> parens (pretty0 desc) <+> dot)
         <+> line <+> !(ploc fc)
+perrorRaw (RunElabFail e)
+    = pure $ reflow "Error during reflection" <+> colon <++> !(perrorRaw e)
 perrorRaw (GenericMsg fc str) = pure $ pretty0 str <+> line <+> !(ploc fc)
 perrorRaw (TTCError msg)
     = pure $ errorDesc (reflow "Error in TTC file" <+> colon <++> byShow msg)

src/TTImp/Elab/RunElab.idr

@@ -63,6 +63,10 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
               NS ns (UN (Basic n))
                  => if ns == reflectionNS
                       then elabCon defs n (map snd args)
+                             `catch` \case -- wrap into `RunElabFail` any non-elab error
+                               e@(BadRunElab _ _ _ _) => throw e
+                               e@(RunElabFail _)      => throw e
+                               e                      => throw $ RunElabFail e
                       else failWith defs $ "bad reflection namespace " ++ show ns
               _ => failWith defs $ "bad fullnames " ++ show fnm
   where
@@ -94,8 +98,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
              let customFC = case !(evalClosure defs mbfc >>= reify defs) of
                                EmptyFC => fc
                                x       => x
-             throw (GenericMsg customFC ("Error during reflection: " ++
-                                      !(reify defs msg')))
+             throw $ RunElabFail $ GenericMsg customFC !(reify defs msg')
     elabCon defs "Try" [_, elab1, elab2]
         = tryUnify (elabScript fc nest env !(evalClosure defs elab1) exp)
                    (elabScript fc nest env !(evalClosure defs elab2) exp)