"INTERNAL ERROR: Unknown reflection raw term"

[raingloom]

environment:

idris -v is 1.3.0-git:PRE

command line is: idris --nocolor -p pruviloj -p contrib AlgebraicBodies.idr

source:

-- AlgebraicBodies.idr
import Language.Reflection
import Pruviloj
import Pruviloj.Induction

%language ElabReflection

auto : Elab ()
auto =
  do compute
     attack
     try intros
     hs <- map fst <$> getEnv
     for_ hs $
       \ih => try (rewriteWith (Var ih))
     hypothesis <|> search
     solve

mush : Elab ()
mush =
   do attack
      x <- gensym "x"
      intro x
      try intros
      induction (Var x) `andThen` auto
      solve


Groupoid : Type
Groupoid = (t : Type ** t -> t -> t)

LeftUnit : (g : Groupoid) -> (fst g) -> Type
LeftUnit g s =
	let op = DPair.snd g in
	(e : fst g) -> (s `op` e) = e

RightUnit : (g : Groupoid) -> (fst g) -> Type
RightUnit g s =
	let op = DPair.snd g in
	(e : fst g) -> (e `op` s) = e

Unit : (g : Groupoid) -> (fst g) -> Type
Unit g s = (LeftUnit g s, RightUnit g s)

UnitIsUnique : (g : Groupoid) -> (s,s' : fst g) -> Unit g s -> Unit g s' -> s = s'
UnitIsUnique = %runElab mush

output:

     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.3.0-git:PRE
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Type checking /home/rain/coding/formal/AlgebraicBodies.idr
/home/rain/coding/formal/AlgebraicBodies.idr:45:16-28:
   |
45 | UnitIsUnique = %runElab mush
   |                ~~~~~~~~~~~~~
When checking right hand side of UnitIsUnique with expected type
        (g : Groupoid) ->
        (s : fst g) -> (s' : fst g) -> Unit g s -> Unit g s' -> s = s'

INTERNAL ERROR: Unknown reflection raw term in reifyRawApp: (Pruviloj.Renamers.alphaRaw,[\ value : Language.Reflection.TTName => Prelude.Maybe.Nothing Language.Reflection.TTName,Language.Reflection.Var (Language.Reflection.NS (Language.Reflection.UN "DPair") (Prelude.List.:: String "Builtins" (Prelude.List.Nil String)))])
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

idris: Network.Socket.bind: resource busy (Address already in use)
Holes: Main.UnitIsUnique
*/home/rain/coding/formal/AlgebraicBodies> Bye bye

The error message said I should report this so that's what I'm doing.