@@ -268,9 +268,14 @@ elabClauses info' fc opts n_in cs =
268268 -- 'Partial NotCovering'
269269 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
270270 where
271− noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
271+ noMatch i cs tm = all (\x -> case trim_matchClause i (delab' i x True True) tm of
272272 Right _ -> False
273273 Left miss -> True) cs
274+ where
275+ trim_matchClause i (PApp fcl fl ls) (PApp fcr fr rs)
276+ = let args = min (length ls) (length rs) in
277+ matchClause i (PApp fcl fl (take args ls))
278+ (PApp fcr fr (take args rs))
274279
275280 checkUndefined n ctxt = case lookupDef n ctxt of
276281 [] -> return ()