@@ -1311,17 +1311,21 @@ elab ist info emode opts fn tm
13111311 do unless (ElabReflection `elem` idris_language_extensions ist) $
13121312 lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")
13131313 attack
1314+ let elabName = sNS (sUN "Elab") ["Elab", "Reflection", "Language"]
13141315 n <- getNameFrom (sMN 0 "tacticScript")
1315− let scriptTy = RApp (Var (sNS (sUN "Elab")
1316− ["Elab", "Reflection", "Language"]))
1317− (Var unitTy)
1316+ let scriptTy = RApp (Var elabName) (Var unitTy)
13181317 claim n scriptTy
13191318 focus n
1319+ elabUnit <- goal
13201320 attack -- to get an extra hole
13211321 elab' ina (Just fc') tm
13221322 script <- get_guess
13231323 fullyElaborated script
13241324 solve -- eliminate the hole. Because there are no references, the script is only in the binding
1325+ ctxt <- get_context
1326+ env <- get_env
1327+ (scriptTm, scriptTy) <- lift $ check ctxt [] (forget script)
1328+ lift $ converts ctxt env elabUnit scriptTy
13251329 env <- get_env
13261330 runElabAction info ist (maybe fc' id fc) env script ns
13271331 solve