INTERNAL ERROR when creating ElabReflection-produced definition twice in the REPL

[RyanGlScott]

$ idris -p pruviloj -XElabReflection
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.0
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Idris> :module Pruviloj.Derive.Eliminators
*Pruviloj/Derive/Eliminators> :let %runElab (deriveElim `{{List}} `{{elimList}})
*Pruviloj/Derive/Eliminators> :let %runElab (deriveElim `{{List}} `{{elimList}})
(input):1:6-14:While running an elaboration script, the following error occurred:
INTERNAL ERROR: elimList is already defined.
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

[RyanGlScott]

Now that I look closer at the actual error that this emits (elimList is already defined), the diagnosis is actually spot-on—the only sketchy part is the bit about it being an "INTERNAL" error. Given that this error message is actually quite feasible to trigger in practice, would a suitable resolution to this bug simply be to change the severity of the error? For example, if you apply this patch:

diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs
index 2908a9c..d320764 100644
--- a/src/Idris/Elab/Term.hs
+++ b/src/Idris/Elab/Term.hs
@@ -1846,7 +1846,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

     mustNotBeDefined ctxt n =
       case lookupDefExact n ctxt of
-        Just _ -> lift . tfail . InternalMsg $
+        Just _ -> lift . tfail . Msg $
                     show n ++ " is already defined."
         Nothing -> return ()

Then the error becomes this:

*Pruviloj/Derive/Eliminators> :let %runElab (deriveElim `{{List}} `{{elimList}})
*Pruviloj/Derive/Eliminators> :let %runElab (deriveElim `{{List}} `{{elimList}})
(input):1:6-13: While running an elaboration script, the following error occurred:
elimList is already defined.

That doesn't have any connotations of being an error that can only be triggered internally. I'm not familiar with the Idris codebase's conventions for which errors should have which severities, so I'm not sure if this is the right approach.