@@ -162,7 +162,7 @@ elabClauses info' fc opts n_in cs =
162 simpleCase tcase (UnmatchedCase "Error") reflect CompileTime fc inacc atys pdef erInfo
162 simpleCase tcase (UnmatchedCase "Error") reflect CompileTime fc inacc atys pdef erInfo
163 cov <- coverage
163 cov <- coverage
164 pmissing <-
164 pmissing <-
165− if cov && not (hasDefault cs)
165+ if cov && not (hasDefault pats_raw)
166 then do missing <- genClauses fc n (map getLHS pdef) cs_full
166 then do missing <- genClauses fc n (map getLHS pdef) cs_full
167 -- missing <- genMissing n scargs sc
167 -- missing <- genMissing n scargs sc
168 missing' <- filterM (checkPossible info fc True n) missing
168 missing' <- filterM (checkPossible info fc True n) missing
@@ -291,10 +291,20 @@ elabClauses info' fc opts n_in cs =
291 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
291 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
292 depat acc x = (acc, x)
292 depat acc x = (acc, x)
295+ getPVs (Bind x (PVar _) tm) = let (vs, tm') = getPVs tm
297+ getPVs tm = ([], tm)
299+ isPatVar vs (P Bound n _) = n `elem` vs
300+ isPatVar _ _ = False
294− hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs
302+ hasDefault cs | (Right (lhs, rhs) : _) <- reverse cs
295− , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args
303+ , (pvs, tm) <- getPVs (explicitNames lhs)
304+ , (f, args) <- unApply tm = all (isPatVar pvs) args
296 hasDefault _ = False
305 hasDefault _ = False
298 getLHS (_, l, _) = l
308 getLHS (_, l, _) = l
300 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
310 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)