@@ -871,15 +871,23 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in
871871 let recty = getRecTy cty_imp
872872 let recty_u = getRecTy cty
873873
874+ let paramNames = getPNames recty ppos
875+
874876 -- rename indices when we generate the getter/setter types, so
875877 -- that they don't clash with the names of the projections
876878 -- we're generating
877879 let index_names_in = getRecNameMap "_in" ppos recty
878880 let recty_in = substMatches index_names_in recty
879881
880− logLvl 1 $ show (recty, ptys)
881− let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
882− [pexp (PRef fc rec)])) ptys
882+ logLvl 3 $ show (recty, recty_u, ppos, paramNames, ptys)
883+ -- Substitute indices with projection functions, and parameters with
884+ -- the updated parameter name
885+ let substs = map (\ (n, _) ->
886+ if n `elem` paramNames
887+ then (n, PRef fc (mkp n))
888+ else (n, PApp fc (PRef fc n)
889+ [pexp (PRef fc rec)]))
890+ ptys
883891
884892 -- Generate projection functions
885893 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
@@ -900,6 +908,14 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in
900908 isNonImp (PExp _ _ _ _, a) = Just a
901909 isNonImp _ = Nothing
902910
911+ getPNames (PApp _ _ as) ppos = getpn as ppos
912+ where
913+ getpn as [] = []
914+ getpn as (i:is) | length as > i,
915+ PRef _ n <- getTm (as!!i) = n : getpn as is
916+ | otherwise = getpn as is
917+ getPNames _ _ = []
918+
903919 tryElabDecl info (fn, ty, val)
904920 = do i <- getIState
905921 idrisCatch (do elabDecl' EAll info ty