git.iko.soy/Idris-dev
on master help sign in
Fix parameter expansion in PEq case
6c39e35Edwin Brady
src/Idris/AbsSyntax.hs+1−1
compare with master
unifiedsplit
@@ -853,7 +853,7 @@ expandParams dec ps ns infs tm = en tm
853 | n `elem` (map fst ps ++ ns) && t /= Placeholder
853 | n `elem` (map fst ps ++ ns) && t /= Placeholder
854 = let n' = mkShadow n in
854 = let n' = mkShadow n in
855 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
855 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
856− en (PEq f lt rt l r) = PEq f (en lt) (en r) (en l) (en r)
856+ en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)
857 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
857 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
858 en (PTyped l r) = PTyped (en l) (en r)
858 en (PTyped l r) = PTyped (en l) (en r)
859 en (PPair f p l r) = PPair f p (en l) (en r)
859 en (PPair f p l r) = PPair f p (en l) (en r)
src/Idris/ElabTerm.hs+2−2
@@ -255,8 +255,8 @@ elab ist info emode opts fn tm
255 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
255 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
256 pimp (sMN 0 "x") t False])
256 pimp (sMN 0 "x") t False])
257 elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)
257 elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)
258− [pimp (sUN "A") Placeholder True,
258+ [pimp (sUN "A") lt True,
259− pimp (sUN "B") Placeholder False,
259+ pimp (sUN "B") rt False,
260 pexp l, pexp r])
260 pexp l, pexp r])
261 elab' ina@(_, a, inty, qq) (PPair fc _ l r)
261 elab' ina@(_, a, inty, qq) (PPair fc _ l r)
262 = do hnf_compute
262 = do hnf_compute