@@ -1746,10 +1746,27 @@ addImpl' inpat env infns imp_meths ist ptm
17461746 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
17471747 ai inpat qq env ds (PCase fc c os)
17481748 = let c' = ai inpat qq env ds c in
1749− -- leave os alone, because they get lifted into a new pattern match
1750− -- definition which is passed through addImpl agai inpatn with more scope
1751− -- information
1752− PCase fc c' os
1749+ -- leave lhs alone, because they get lifted into a new pattern match
1750+ -- definition which is passed through addImpl again
1751+ PCase fc c' (map aiCase os)
1752+ where
1753+ aiCase (lhs, rhs)
1754+ = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)
1755+
1756+ -- Anything beginning with a lower case letter, not applied,
1757+ -- and no namespace is a pattern variable
1758+ patnames (PApp _ (PRef _ _ f) [])
1759+ | implicitable f = [(f, Nothing)]
1760+ patnames (PRef _ _ f)
1761+ | implicitable f = [(f, Nothing)]
1762+ patnames (PApp _ (PRef _ _ _) args)
1763+ = concatMap patnames (map getTm args)
1764+ patnames (PPair _ _ _ l r) = patnames l ++ patnames r
1765+ patnames (PDPair _ _ _ l t r) = patnames l ++ patnames t ++ patnames r
1766+ patnames (PAs _ _ t) = patnames t
1767+ patnames (PAlternative _ _ ts) = concatMap patnames ts
1768+ patnames _ = []
1769+
17531770
17541771 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
17551772 (ai inpat qq env ds t)