Check coverage after inferring postponed checks

Otherwise we risk missing some covered cases that were just postponed.

src/Elaboration.hs

@@ -172,6 +172,7 @@ inferDefinition context def =
 postProcessDefinition :: Context v -> Syntax.Definition -> M Syntax.Definition
 postProcessDefinition context def = do
   Context.inferAllPostponedChecks context
+  Context.reportCoverage context
   postponed <- readIORef context.postponed
   pure $ ZonkPostponedChecks.zonkDefinition postponed def
 
@@ -238,6 +239,7 @@ postProcessDataDefinition
   -> M Syntax.Definition
 postProcessDataDefinition outerContext boxity outerTele = do
   Context.inferAllPostponedChecks outerContext
+  Context.reportCoverage outerContext
   postponed <- readIORef outerContext.postponed
   Syntax.DataDefinition boxity <$> go outerContext postponed outerTele mempty
   where

src/Elaboration/Context.hs

@@ -34,6 +34,7 @@ import Data.IORef.Lifted
 import Data.IntSeq (IntSeq)
 import qualified Data.IntSeq as IntSeq
 import qualified Data.Kind
+import qualified Data.Set as Set
 import Data.Tsil (Tsil)
 import qualified Data.Tsil as Tsil
 import qualified Elaboration.Meta as Meta
@@ -79,6 +80,7 @@ data Context (v :: Data.Kind.Type) = Context
   , postponed :: !(IORef Postponed.Checks)
   , coveredConstructors :: CoveredConstructors
   , coveredLiterals :: CoveredLiterals
+  , coverageChecks :: !(IORef (Tsil CoverageCheck))
   , errors :: !(IORef (Tsil Error))
   }
 
@@ -89,6 +91,12 @@ type CoveredConstructors = EnumMap Var (HashSet Name.QualifiedConstructor)
 
 type CoveredLiterals = EnumMap Var (HashSet Literal)
 
+data CoverageCheck = CoverageCheck
+  { allClauses :: Set Span.Relative
+  , usedClauses :: IORef (Set Span.Relative)
+  , matchKind :: !Error.MatchKind
+  }
+
 toEnvironment
   :: Context v
   -> Domain.Environment v
@@ -104,6 +112,7 @@ empty definitionKind definitionName = do
   ms <- newIORef Meta.empty
   es <- newIORef mempty
   ps <- newIORef Postponed.empty
+  cs <- newIORef mempty
   pure
     Context
       { definitionKind
@@ -121,6 +130,7 @@ empty definitionKind definitionName = do
       , errors = es
       , coveredConstructors = mempty
       , coveredLiterals = mempty
+      , coverageChecks = cs
       }
 
 emptyFrom :: Context v -> Context Void
@@ -141,6 +151,7 @@ emptyFrom context =
     , errors = context.errors
     , coveredConstructors = mempty
     , coveredLiterals = mempty
+    , coverageChecks = context.coverageChecks
     }
 
 spanned :: Span.Relative -> Context v -> Context v
@@ -816,3 +827,11 @@ inferAllPostponedChecks context =
 
               (postponed'', do doIt; go $ index + 1)
             else (postponed', pure ())
+
+reportCoverage :: Context v -> M ()
+reportCoverage context = do
+  coverageChecks <- atomicModifyIORef' context.coverageChecks (mempty,)
+  forM_ coverageChecks \coverageCheck -> do
+    usedClauses <- readIORef coverageCheck.usedClauses
+    forM_ (Set.difference coverageCheck.allClauses usedClauses) \span ->
+      report (spanned span context) $ Error.RedundantMatch coverageCheck.matchKind

src/Elaboration/Matching.hs

@@ -330,16 +330,23 @@ checkSingle context scrutinee plicity pat@(Surface.Pattern patSpan _) rhs@(Surfa
 
 checkWithCoverage :: Context v -> Config -> M (Syntax.Term v)
 checkWithCoverage context config = do
-  result <- check context config Postponement.CanPostpone
-  let allClauseSpans =
+  let allClauses =
         Set.fromList
           [ span
           | Clause span _ _ <- config.clauses
           ]
-  usedClauseSpans <- readIORef config.usedClauses
-  forM_ (Set.difference allClauseSpans usedClauseSpans) \span ->
-    Context.report (Context.spanned span context) $ Error.RedundantMatch config.matchKind
-  pure result
+  atomicModifyIORef'
+    context.coverageChecks
+    \coverageChecks ->
+      ( coverageChecks
+          Tsil.:> Context.CoverageCheck
+            { Context.allClauses = allClauses
+            , Context.usedClauses = config.usedClauses
+            , Context.matchKind = config.matchKind
+            }
+      , ()
+      )
+  check context config Postponement.CanPostpone
 
 check :: Context v -> Config -> Postponement.CanPostpone -> M (Syntax.Term v)
 check context config canPostpone = do
@@ -359,7 +366,7 @@ check context config canPostpone = do
       splitEqualityOr context config' matches $
         splitConstructorOr context config' matches $ do
           let indeterminateIndexUnification = do
-                Context.report context $ Error.IndeterminateIndexUnification $ config.matchKind
+                Context.report context $ Error.IndeterminateIndexUnification config.matchKind
                 Elaboration.readback context $ Builtin.Unknown config.expectedType
           case solved matches of
             Nothing ->
@@ -378,7 +385,7 @@ check context config canPostpone = do
                     withPatternInstantiation inst context
               mapM_ (checkForcedPattern context') matches
               result <- Elaboration.check context' firstClause.rhs config.expectedType
-              modifyIORef config.usedClauses $ Set.insert firstClause.span
+              atomicModifyIORef' config.usedClauses \usedClauses -> (Set.insert firstClause.span usedClauses, ())
               pure result
 
 findPatternResolutionBlocker :: Context v -> [Clause] -> M (Maybe Meta.Index)

tests/singles/type-checking/ambiguous-constructor-in-pattern.vix

@@ -8,4 +8,4 @@ data List2 a where
 
 test x = -- unsolved meta error expected
   case x of
-    Nil -> 610 -- redundant match error expected, ambiguous name error expected
+    Nil -> 610 -- ambiguous name error expected