@@ -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
280281 terminator
281282 return (Rule (mkSimple syms) tm sty)
282283 where
@@ -297,7 +298,42 @@ 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 :: PTerm -> IdrisParser PTerm
305+ uniquifyBinders = fixBind []
306+
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+ do ty' <- fixBind rens ty
314+ n' <- gensym n
315+ body' <- fixBind ((n,n'):rens) body
316+ return $ PLam fc n' ty' body'
317+ fixBind rens (PPi plic n argTy body) =
318+ do ty' <- fixBind rens argTy
319+ n' <- gensym n
320+ body' <- fixBind ((n,n'):rens) body
321+ return $ (PPi plic n' ty' body')
322+ fixBind rens (PLet fc n ty val body) =
323+ do ty' <- fixBind rens ty
324+ val' <- fixBind rens val
325+ n' <- gensym n
326+ body' <- fixBind ((n,n'):rens) body
327+ return $ (PLet fc n' ty' val' body')
328+ fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
329+ return $ PMatchApp fc n'
330+ fixBind rens x = descendM (fixBind rens) x
331+
332+ gensym :: Name -> IdrisParser Name
333+ gensym n = do ist <- get
334+ let idx = idris_name ist
335+ put ist { idris_name = idx + 1 }
336+ return $ sMN idx (show n)
301337
302338{- | Parses a syntax symbol (either binding variable, keyword or expression)
303339