[ new ] Add compile.casetree.missing topic

This allows us to track when we're compiling non-covering case blocks.

CHANGELOG.md

@@ -79,6 +79,10 @@
 * The Lifted IR Representation now has a `HasNamespaces` implementation
   in `Compiler.Separate` so Compilation Units at that stage can be generated.
 
+* Added the `compile.casetree.missing` log topic, along with its use in
+  `TTImp.ProcessDef.genRunTime`. This allows us to track when incomplete `case`
+  blocks get the runtime error added.
+
 ### Library changes
 
 #### Prelude

src/Core/Options/Log.idr

@@ -50,8 +50,9 @@ knownTopics = [
     ("compile.casetree.getpmdef", Nothing),
     ("compile.casetree.intermediate", Nothing),
     ("compile.casetree.measure", Just "Log the node counts of each runtime case tree."),
-    ("compile.casetree.pick", Nothing),
+    ("compile.casetree.missing", Just "Log when we add an error case for uncovered branches."),
     ("compile.casetree.partition", Nothing),
+    ("compile.casetree.pick", Nothing),
     ("compiler.const-fold", Just "Log definitions before and after constant folding."),
     ("compiler.cse", Just "Log information about common sub-expression elimination."),
     ("compiler.identity", Just "Log definitions that are equivalent to identity at runtime."),

src/TTImp/ProcessDef.idr

@@ -801,9 +801,10 @@ mkRunTime fc n
                              pats
 
            let clauses_init = map (toClause (location gdef)) pats'
-           let clauses = case cov of
-                              MissingCases _ => addErrorCase clauses_init
-                              _ => clauses_init
+           clauses <- case cov of
+                           MissingCases _ => do log "compile.casetree.missing" 5 $ "Adding uncovered error to \{show clauses_init}"
+                                                pure $ addErrorCase clauses_init
+                           _ => pure clauses_init
 
            (rargs ** (tree_rt, _)) <- getPMDef (location gdef) RunTime n ty clauses
            logC "compile.casetree" 5 $ do