[ fix ] Issue in totality checking

src/Core/Termination/SizeChange.idr

@@ -218,16 +218,16 @@ findLoops s
          -- Hence the following filter:
          let loops = filterEndos (\a => composeChange a.change a.change == a.change) s
          log "totality.termination.calc" 7 $ "Loops: " ++ show loops
-         let terms = map (foldMap (\a => checkDesc a.change a.path)) loops
+         let terms = map (foldMap (\a => checkDesc Z a.change a.path)) loops
          pure terms
     where
       filterEndos : (ArgChange -> Bool) -> SCSet -> NameMap (List ArgChange)
       filterEndos p = mapWithKey (\f, m => filter p (Data.SortedSet.toList (lookupSet f m)))
 
-      checkDesc : Change -> Path -> Maybe Path
-      checkDesc [] p = Just p
-      checkDesc (Just (_, Smaller) :: _) p = Nothing
-      checkDesc (_ :: xs) p = checkDesc xs p
+      checkDesc : Nat -> Change -> Path -> Maybe Path
+      checkDesc _ [] p = Just p
+      checkDesc n (Just (k, Smaller) :: xs) p = if n == k then Nothing else checkDesc (S n) xs p
+      checkDesc n (_ :: xs) p = checkDesc (S n) xs p
 
 findNonTerminatingLoop : {auto c : Ref Ctxt Defs} -> SCSet -> Core (Maybe (Name, Path))
 findNonTerminatingLoop s

tests/Main.idr

@@ -231,7 +231,7 @@ idrisTestsTotality = MkTestPool "Totality checking" [] Nothing
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009", "total010",
        "total011", "total012", "total013", "total014", "total015",
-       "total016", "total017", "total018"
+       "total016", "total017", "total018", "total019"
       ]
 
 -- This will only work with an Idris compiled via Chez or Racket, but at

tests/idris2/total019/Check.idr

@@ -0,0 +1,5 @@
+%default total
+
+foo : List Char -> List Char -> ()
+foo (c :: cs) _ = foo (c :: cs) cs
+foo _ _ = ()

tests/idris2/total019/expected

@@ -0,0 +1,9 @@
+1/1: Building Check (Check.idr)
+Error: foo is not total, possibly not terminating due to recursive path Main.foo
+
+Check:3:1--3:35
+ 1 | %default total
+ 2 | 
+ 3 | foo : List Char -> List Char -> ()
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+

tests/idris2/total019/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check Check.idr