[ fix ] Check totality after all declarations

Author: spcfox

CHANGELOG_NEXT.md

@@ -66,6 +66,7 @@ should target this file (`CHANGELOG_NEXT`).
   `impossible` clause.
 * Do not inline `Core.sequence`, because it is recursively defined.
 * Fixed coverage checker issues (#1800, #1998, #2318, #2822, #3679).
+* Fixed totality checking in namespace and mutual blocks (#2868, #3692).
 
 ### Building/Packaging changes
 

src/Idris/ProcessIdr.idr

@@ -87,11 +87,10 @@ processDecl decl
                         pure [err])
 
 processDecls decls
-    = do xs <- concat <$> traverse processDecl decls
+    = do errs <- concat <$> traverse processDecl decls
          Nothing <- checkDelayedHoles
-             | Just err => pure (if null xs then [err] else xs)
-         errs <- logTime 3 ("Totality check overall") getTotalityErrors
-         pure (xs ++ errs)
+             | Just err => pure (if null errs then [err] else errs)
+         pure errs
 
 readModule : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
@@ -388,6 +387,9 @@ processMod sourceFileName ttcFileName msg sourcecode origin
                 setNS (miAsNamespace ns)
                 errs <- logTime 2 "Processing decls" $
                             processDecls (decls mod)
+                totErrs <- logTime 3 ("Totality check overall")
+                            getTotalityErrors
+                let errs = errs ++ totErrs
 --                 coreLift $ gc
 
                 when (isNil errs) $

tests/idris2/error/error034/Issue3692.idr

@@ -0,0 +1,13 @@
+bad : Bool -> ()
+bad True = ()
+
+namespace X
+  foo : ()
+  foo = ()
+
+mutual
+  bar : ()
+  bar = baz
+
+  baz : ()
+  baz = bar

tests/idris2/error/error034/expected

@@ -0,0 +1,10 @@
+1/1: Building Issue3692 (Issue3692.idr)
+Error: bad is not covering.
+
+Issue3692:1:1--1:17
+ 1 | bad : Bool -> ()
+     ^^^^^^^^^^^^^^^^
+
+Missing cases:
+    bad False
+

tests/idris2/error/error034/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Issue3692.idr

tests/idris2/termination/termination001/expected

@@ -11,26 +11,6 @@ AgdaIssue6059:23:3--23:21
 
 Error: g is not total, possibly not terminating due to recursive path Main.f -> Main.f -> Main.g
 
-AgdaIssue6059:31:3--31:32
- 27 |   -- Base cases:
- 28 |   f (MkD 0 0) = ()
- 29 |   f (MkD 0 1) = ()
- 30 | 
- 31 |   g : (h : Nat -> D) -> P (h 2)
-        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-Error: f is not total, possibly not terminating due to call to Main.g
-
-AgdaIssue6059:23:3--23:21
- 19 | lem 0 = Refl
- 20 | lem (S n) = Refl
- 21 | 
- 22 | mutual
- 23 |   f : (x : D) -> P x
-        ^^^^^^^^^^^^^^^^^^
-
-Error: g is not total, possibly not terminating due to recursive path Main.f -> Main.f -> Main.g
-
 AgdaIssue6059:31:3--31:32
  27 |   -- Base cases:
  28 |   f (MkD 0 0) = ()

tests/idris2/total/total011/expected

@@ -62,22 +62,3 @@ Issue1828:8:3--8:14
  8 |   dummy : Nat
        ^^^^^^^^^^^
 
-Error: caseTest is not total, possibly not terminating due to call to Main.dummy
-
-Issue1828:4:3--4:25
- 1 | %default total
- 2 | 
- 3 | mutual
- 4 |   caseTest : Nat -> Bool
-       ^^^^^^^^^^^^^^^^^^^^^^
-
-Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy
-
-Issue1828:8:3--8:14
- 4 |   caseTest : Nat -> Bool
- 5 |   caseTest p with (dummy)
- 6 |    caseTest p | _ = True
- 7 | 
- 8 |   dummy : Nat
-       ^^^^^^^^^^^
-

tests/idris2/total/total012/expected

@@ -12,23 +12,6 @@ Issue1828:2:3--2:25
 
 Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy
 
-Issue1828:6:3--6:14
- 2 |   caseTest : Nat -> Bool
- 3 |   caseTest p with (dummy)
- 4 |    caseTest p | _ = True
- 5 | 
- 6 |   dummy : Nat
-       ^^^^^^^^^^^
-
-Error: caseTest is not total, possibly not terminating due to call to Main.dummy
-
-Issue1828:2:3--2:25
- 1 | mutual
- 2 |   caseTest : Nat -> Bool
-       ^^^^^^^^^^^^^^^^^^^^^^
-
-Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy
-
 Issue1828:6:3--6:14
  2 |   caseTest : Nat -> Bool
  3 |   caseTest p with (dummy)

tests/idris2/total/total030/Issue2868.idr

@@ -0,0 +1,17 @@
+%default total
+
+namespace Foo
+  public export
+  total
+  foo : ()
+
+namespace Bar
+  public export
+  total
+  bar : ()
+
+namespace Foo
+  foo = bar
+
+namespace Bar
+  bar = foo

tests/idris2/total/total030/ProofOfFalse.idr

@@ -0,0 +1,16 @@
+%default total
+
+namespace Foo
+  public export
+  foo : Void
+
+namespace Bar
+  public export
+  bar : Void
+  bar = foo
+
+namespace Foo
+  foo = bar
+
+boom : Void
+boom = foo