@@ -988,7 +988,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
988 simpleCase tcase False reflect CompileTime fc atys pdef
988 simpleCase tcase False reflect CompileTime fc atys pdef
989 cov <- coverage
989 cov <- coverage
990 pmissing <-
990 pmissing <-
991− if cov
991+ if cov && not (hasDefault cs)
992 then do missing <- genClauses fc n (map getLHS pdef) cs
992 then do missing <- genClauses fc n (map getLHS pdef) cs
993 -- missing <- genMissing n scargs sc
993 -- missing <- genMissing n scargs sc
994 missing' <- filterM (checkPossible info fc True n) missing
994 missing' <- filterM (checkPossible info fc True n) missing
@@ -1092,6 +1092,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1092 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
1092 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
1093 depat acc x = (acc, x)
1093 depat acc x = (acc, x)
1095+ hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs
1096+ , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args
1097+ hasDefault _ = False
1095 getLHS (_, l, _) = l
1099 getLHS (_, l, _) = l
1097 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,
1101 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,