From 5b8442aa58a1fd36152d7cde2fce42e4e70e86b6 Mon Sep 17 00:00:00 2001
From: Viktor Yudov <me@spcfox.com>
Date: Tue, 4 Mar 2025 19:18:53 +0300
Subject: [PATCH] [ fix ] Add cast localVars to `List` in `RunElab`

---
 src/TTImp/Elab/RunElab.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr
index cd1ec4622c..bf1ef2e4d9 100644
--- a/src/TTImp/Elab/RunElab.idr
+++ b/src/TTImp/Elab/RunElab.idr
@@ -274,7 +274,7 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
              ty <- getTerm gty
              scriptRet (Just $ map rawName $ !(unelabUniqueBinders env ty))
     elabCon defs "LocalVars" [<]
-        = scriptRet vars
+        = scriptRet (the (List Name) (cast vars))
     elabCon defs "GenSym" [<str]
         = do str' <- evalClosure defs str
              n <- genVarName !(reify defs str')