[ elab ] More descriptive "Bad elaborator script" error message (#1427)

src/Core/Core.idr

@@ -133,7 +133,7 @@ data Error : Type where
                      FC -> Env Term vars -> DotReason -> Term vars -> Term vars -> Error
      BadImplicit : FC -> String -> Error
      BadRunElab : {vars : _} ->
-                  FC -> Env Term vars -> Term vars -> Error
+                  FC -> Env Term vars -> Term vars -> (description : String) -> Error
      GenericMsg : FC -> String -> Error
      TTCError : TTCErrorMsg -> Error
      FileErr : String -> FileError -> Error
@@ -303,7 +303,7 @@ Show Error where
            " (" ++ show reason ++ ")" ++
            " - it elaborates to " ++ show y
   show (BadImplicit fc str) = show fc ++ ":" ++ str ++ " can't be bound here"
-  show (BadRunElab fc env script) = show fc ++ ":Bad elaborator script " ++ show script
+  show (BadRunElab fc env script desc) = show fc ++ ":Bad elaborator script " ++ show script ++ " (" ++ desc ++ ")"
   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
@@ -389,7 +389,7 @@ getErrorLoc (CaseCompile loc _ _) = Just loc
 getErrorLoc (MatchTooSpecific loc _ _) = Just loc
 getErrorLoc (BadDotPattern loc _ _ _ _) = Just loc
 getErrorLoc (BadImplicit loc _) = Just loc
-getErrorLoc (BadRunElab loc _ _) = Just loc
+getErrorLoc (BadRunElab loc _ _ _) = Just loc
 getErrorLoc (GenericMsg loc _) = Just loc
 getErrorLoc (TTCError _) = Nothing
 getErrorLoc (FileErr _ _) = Nothing

src/Idris/Error.idr

@@ -411,8 +411,8 @@ perror (MatchTooSpecific fc env tm)
 perror (BadImplicit fc str)
     = pure $ errorDesc (reflow "Can't infer type for unbound implicit name" <++> code (pretty str) <+> dot)
         <+> line <+> !(ploc fc) <+> line <+> reflow "Suggestion: try making it a bound implicit."
-perror (BadRunElab fc env script)
-    = pure $ errorDesc (reflow "Bad elaborator script" <++> code !(pshow env script) <+> dot)
+perror (BadRunElab fc env script desc)
+    = pure $ errorDesc (reflow "Bad elaborator script" <++> code !(pshow env script) <++> parens (pretty desc) <+> dot)
         <+> line <+> !(ploc fc)
 perror (GenericMsg fc str) = pure $ pretty str <+> line <+> !(ploc fc)
 perror (TTCError msg)

src/TTImp/Elab/RunElab.idr

@@ -28,19 +28,20 @@ elabScript : {vars : _} ->
              FC -> NestedNames vars ->
              Env Term vars -> NF vars -> Maybe (Glued vars) ->
              Core (NF vars)
-elabScript fc nest env (NDCon nfc nm t ar args) exp
+elabScript fc nest env script@(NDCon nfc nm t ar args) exp
     = do defs <- get Ctxt
          fnm <- toFullNames nm
          case fnm of
               NS ns (UN n)
-                 => if ns == reflectionNS then elabCon defs n (map snd args) else failWith defs
-              _ => failWith defs
+                 => if ns == reflectionNS
+                      then elabCon defs n (map snd args)
+                      else failWith defs $ "bad reflection namespace " ++ show ns
+              _ => failWith defs $ "bad fullnames " ++ show fnm
   where
-    failWith : Defs -> Core a
-    failWith defs
-      = do defs <- get Ctxt
-           empty <- clearDefs defs
-           throw (BadRunElab fc env !(quote empty env (NDCon nfc nm t ar args)))
+    failWith : Defs -> String -> Core a
+    failWith defs desc
+      = do empty <- clearDefs defs
+           throw (BadRunElab fc env !(quote empty env script) desc)
 
     scriptRet : Reflect a => a -> Core (NF vars)
     scriptRet tm
@@ -59,7 +60,7 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp
                       elabScript fc nest env
                               !(sc defs (toClosure withAll env
                                               !(quote defs env act'))) exp
-                  _ => failWith defs
+                  x => failWith defs $ "non-function RHS of a Bind: " ++ show x
     elabCon defs "Fail" [_,msg]
         = do msg' <- evalClosure defs msg
              throw (GenericMsg fc ("Error during reflection: " ++
@@ -161,11 +162,12 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp
              decls <- reify defs d'
              traverse_ (processDecl [] (MkNested []) []) decls
              scriptRet ()
-    elabCon defs n args = failWith defs
+    elabCon defs n args = failWith defs $ "unexpected Elab constructor " ++ n ++
+                                          ", or incorrect count of arguments: " ++ show (length args)
 elabScript fc nest env script exp
     = do defs <- get Ctxt
          empty <- clearDefs defs
-         throw (BadRunElab fc env !(quote empty env script))
+         throw (BadRunElab fc env !(quote empty env script) "script is not a data value")
 
 export
 checkRunElab : {vars : _} ->