@@ -502,7 +502,9 @@ syntaxRule syn
502 body' <- fixBind ((n,n'):rens) body
502 body' <- fixBind ((n,n'):rens) body
503 return $ PLam fc n' nfc ty' body'
503 return $ PLam fc n' nfc ty' body'
504 fixBind rens (PPi plic n nfc argTy body)
504 fixBind rens (PPi plic n nfc argTy body)
505− | n `elem` userNames = liftM2 (PPi plic n nfc) (fixBind rens argTy) (fixBind rens body)
505+ | n `elem` userNames = liftM2 (PPi plic n nfc)
506+ (fixBind rens argTy)
506 | otherwise =
508 | otherwise =
507 do ty' <- fixBind rens argTy
509 do ty' <- fixBind rens argTy
508 n' <- gensym n
510 n' <- gensym n
@@ -521,6 +523,10 @@ syntaxRule syn
521 return $ PLet fc n' nfc ty' val' body'
523 return $ PLet fc n' nfc ty' val' body'
522 fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
524 fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
523 return $ PMatchApp fc n'
525 return $ PMatchApp fc n'
526+ -- Also rename resolved quotations, to allow syntax rules to
527+ -- have quoted references to their own bindings.
528+ fixBind rens (PQuoteName n True fc) | Just n' <- lookup n rens =
529+ return $ PQuoteName n' True fc
524 fixBind rens x = descendM (fixBind rens) x
530 fixBind rens x = descendM (fixBind rens) x
526 gensym :: Name -> IdrisParser Name
532 gensym :: Name -> IdrisParser Name