@@ -59,6 +59,7 @@ import Data.List
5959import Data.Monoid
6060import Data.Char
6161import Data.Ord
62+import Data.Generics.Uniplate.Data (descendM)
6263import qualified Data.Map as M
6364import qualified Data.HashSet as HS
6465import qualified Data.Text as T
@@ -276,7 +277,7 @@ syntaxRule syn
276277 when (length ns /= length (nub ns))
277278 $ unexpected "repeated variable in syntax rule"
278279 lchar '='
279− tm <- typeExpr (allowImp syn)
280+ tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
280281 terminator
281282 return (Rule (mkSimple syms) tm sty)
282283 where
@@ -297,7 +298,51 @@ syntaxRule syn
297298 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
298299 mkSimple' (e : es) = e : mkSimple' es
299300 mkSimple' [] = []
300−
301+
302+ -- Prevent syntax variable capture by making all binders under syntax unique
303+ -- (the ol' Common Lisp GENSYM approach)
304+ uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
305+ uniquifyBinders userNames = fixBind []
306+ where
307+ fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
308+ fixBind rens (PRef fc n) | Just n' <- lookup n rens =
309+ return $ PRef fc n'
310+ fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
311+ return $ PPatvar fc n'
312+ fixBind rens (PLam fc n ty body)
313+ | n `elem` userNames = liftM2 (PLam fc n) (fixBind rens ty) (fixBind rens body)
314+ | otherwise =
315+ do ty' <- fixBind rens ty
316+ n' <- gensym n
317+ body' <- fixBind ((n,n'):rens) body
318+ return $ PLam fc n' ty' body'
319+ fixBind rens (PPi plic n argTy body)
320+ | n `elem` userNames = liftM2 (PPi plic n) (fixBind rens argTy) (fixBind rens body)
321+ | otherwise =
322+ do ty' <- fixBind rens argTy
323+ n' <- gensym n
324+ body' <- fixBind ((n,n'):rens) body
325+ return $ (PPi plic n' ty' body')
326+ fixBind rens (PLet fc n ty val body)
327+ | n `elem` userNames = liftM3 (PLet fc n)
328+ (fixBind rens ty)
329+ (fixBind rens val)
330+ (fixBind rens body)
331+ | otherwise =
332+ do ty' <- fixBind rens ty
333+ val' <- fixBind rens val
334+ n' <- gensym n
335+ body' <- fixBind ((n,n'):rens) body
336+ return $ (PLet fc n' ty' val' body')
337+ fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
338+ return $ PMatchApp fc n'
339+ fixBind rens x = descendM (fixBind rens) x
340+
341+ gensym :: Name -> IdrisParser Name
342+ gensym n = do ist <- get
343+ let idx = idris_name ist
344+ put ist { idris_name = idx + 1 }
345+ return $ sMN idx (show n)
301346
302347{- | Parses a syntax symbol (either binding variable, keyword or expression)
303348