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