@@ -871,15 +871,23 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in
871 let recty = getRecTy cty_imp
871 let recty = getRecTy cty_imp
872 let recty_u = getRecTy cty
872 let recty_u = getRecTy cty
874+ let paramNames = getPNames recty ppos
874 -- rename indices when we generate the getter/setter types, so
876 -- rename indices when we generate the getter/setter types, so
875 -- that they don't clash with the names of the projections
877 -- that they don't clash with the names of the projections
876 -- we're generating
878 -- we're generating
877 let index_names_in = getRecNameMap "_in" ppos recty
879 let index_names_in = getRecNameMap "_in" ppos recty
878 let recty_in = substMatches index_names_in recty
880 let recty_in = substMatches index_names_in recty
880− logLvl 1 $ show (recty, 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
881− let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
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)
882− [pexp (PRef fc rec)])) ptys
889+ [pexp (PRef fc rec)]))
884 -- Generate projection functions
892 -- Generate projection functions
885 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
893 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
900 isNonImp (PExp _ _ _ _, a) = Just a
908 isNonImp (PExp _ _ _ _, a) = Just a
901 isNonImp _ = Nothing
909 isNonImp _ = Nothing
911+ getPNames (PApp _ _ as) ppos = getpn as ppos
914+ getpn as (i:is) | length as > i,
915+ PRef _ n <- getTm (as!!i) = n : getpn as is
916+ | otherwise = getpn as is
903 tryElabDecl info (fn, ty, val)
919 tryElabDecl info (fn, ty, val)
904 = do i <- getIState
920 = do i <- getIState
905 idrisCatch (do elabDecl' EAll info ty
921 idrisCatch (do elabDecl' EAll info ty