@@ -223,6 +223,8 @@ missingAlternative env mn ca uncovered
224 mcases = missingCases env mn uncovered ca
224 mcases = missingCases env mn uncovered ca
227-- Main exhaustivity checking function
229-- Main exhaustivity checking function
228-- Starting with the set `uncovered = { _ }` (nothing covered, one `_` for each function argument),
230-- Starting with the set `uncovered = { _ }` (nothing covered, one `_` for each function argument),
@@ -235,9 +237,10 @@ checkExhaustive env mn numArgs cas = makeResult . first nub $ foldl' step ([init
235 step :: ([[Binder]], (Maybe Bool, [[Binder]])) -> CaseAlternative -> ([[Binder]], (Maybe Bool, [[Binder]]))
237 step :: ([[Binder]], (Maybe Bool, [[Binder]])) -> CaseAlternative -> ([[Binder]], (Maybe Bool, [[Binder]]))
236 step (uncovered, (nec, redundant)) ca =
238 step (uncovered, (nec, redundant)) ca =
237 let (missed, pr) = unzip (map (missingAlternative env mn ca) uncovered)
239 let (missed, pr) = unzip (map (missingAlternative env mn ca) uncovered)
240+ (missed', approx) = splitAt 10000 (concat missed)
238− cond = or <$> sequenceA pr
241+ cond = liftA2 (&&) (or <$> sequenceA pr) nec
239− in (concat missed, (liftA2 (&&) cond nec,
242+ in (missed', (if null approx then cond else Nothing,
240− if fromMaybe True cond then redundant else caseAlternativeBinders ca : redundant))
243+ if fromMaybe True cond then redundant else caseAlternativeBinders ca : redundant))
241#if __GLASGOW_HASKELL__ < 710
244#if __GLASGOW_HASKELL__ < 710
243 sequenceA = foldr (liftA2 (:)) (pure [])
246 sequenceA = foldr (liftA2 (:)) (pure [])