on master help sign in
Fix shadowing bug with dependent pair bindings
commit5ce8ee7ac74112926e5e839775f963b404f71081 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 27 Aug 2013, 16:00 (13 years ago) parent35268c1
2 files changed+5−1
src/Idris/AbsSyntax.hs+5 test/reg009/reg009.lidr−1
src/Idris/AbsSyntax.hs+5
@@ -623,6 +623,11 @@ expandParams dec ps ns infs tm = en tm
623623 = let n' = mkShadow n in
624624 PLet n' (en ty) (en v) (en (shadow n n' s))
625625 | otherwise = PLet n (en ty) (en v) (en s)
626+ -- FIXME: Should only do this in a type signature!
627+ en (PDPair f (PRef f' n) t r)
628+ | n `elem` (map fst ps ++ ns) && t /= Placeholder
629+ = let n' = mkShadow n in
630+ PDPair f (PRef f' n') (en t) (en (shadow n n' r))
626631 en (PEq f l r) = PEq f (en l) (en r)
627632 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
628633 en (PTyped l r) = PTyped (en l) (en r)
test/reg009/reg009.lidr−1
@@ -2,7 +2,6 @@
22> isAnyBy _ (_ ** Nil) = False
33> isAnyBy p (_ ** (a :: as)) = p a || isAnyBy p (_ ** as)
44
5−
65> filterTagP : (p : alpha -> Bool) ->
76> (as : Vect n alpha) ->
87> so (isAnyBy p (n ** as)) ->