@@ -692,24 +692,36 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
692692 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
693693 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
694694 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
695− n' = if n `elem` ns then dec n else n in
695+ n' = if n `elem` ns then dec n else n
696+ -- names bound on the lhs should not be expanded on the rhs
697+ ns' = removeBound lhs ns in
696698 PClause fc n' lhs'
697− (map (expandParams dec ps'' ns []) ws)
698− (expandParams dec ps'' ns [] rhs)
699− (map (expandParamsD True ist dec ps'' ns) ds)
699+ (map (expandParams dec ps'' ns' []) ws)
700+ (expandParams dec ps'' ns' [] rhs)
701+ (map (expandParamsD True ist dec ps'' ns') ds)
700702 expandParamsC (PWith fc n lhs ws wval ds)
701703 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
702704 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
703705 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
704− n' = if n `elem` ns then dec n else n in
706+ n' = if n `elem` ns then dec n else n
707+ ns' = removeBound lhs ns in
705708 PWith fc n' lhs'
706− (map (expandParams dec ps'' ns []) ws)
707− (expandParams dec ps'' ns [] wval)
708− (map (expandParamsD rhsonly ist dec ps'' ns) ds)
709+ (map (expandParams dec ps'' ns' []) ws)
710+ (expandParams dec ps'' ns' [] wval)
711+ (map (expandParamsD rhsonly ist dec ps'' ns') ds)
709712 updateps yn nm [] = []
710713 updateps yn nm (((a, t), i):as)
711714 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
712715 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
716+
717+ removeBound lhs ns = ns \\ nub (bnames lhs)
718+
719+ bnames (PRef _ n) = [n]
720+ bnames (PApp _ _ args) = concatMap bnames (map getTm args)
721+ bnames (PPair _ l r) = bnames l ++ bnames r
722+ bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
723+ bnames _ = []
724+
713725expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
714726 = PData doc syn fc co (expandPData pd)
715727 where