@@ -356,7 +356,7 @@ varRule (v : vs) alts err =
356 repVar v (PV p : ps , (lhs, res)) = (ps, (lhs, subst p (P Bound v Erased) res))
356 repVar v (PV p : ps , (lhs, res)) = (ps, (lhs, subst p (P Bound v Erased) res))
357 repVar v (PAny : ps , res) = (ps, res)
357 repVar v (PAny : ps , res) = (ps, res)
359−-- fix: case e of S k -> f (S k) ==> case e of S k -. f e
359+-- fix: case e of S k -> f (S k) ==> case e of S k -> f e
360depatt :: [Name] -> SC -> SC
360depatt :: [Name] -> SC -> SC
361depatt ns tm = dp [] tm
361depatt ns tm = dp [] tm
@@ -376,7 +376,8 @@ depatt ns tm = dp [] tm
377 applyMap [] nt cn pty args' = mkApp (P nt cn pty) args'
377 applyMap [] nt cn pty args' = mkApp (P nt cn pty) args'
378 applyMap ((x, (n, args)) : ms) nt cn pty args'
378 applyMap ((x, (n, args)) : ms) nt cn pty args'
379+ | and ((length args == length args') :
379− | and ((n == cn) : zipWith same args args') = P Ref x Erased
380+ (n == cn) : zipWith same args args') = P Ref x Erased
380 | otherwise = applyMap ms nt cn pty args'
381 | otherwise = applyMap ms nt cn pty args'
381 same n (P _ n' _) = n == n'
382 same n (P _ n' _) = n == n'
382 same _ _ = False
383 same _ _ = False