[ fix #1782 ] remove the case-specific code

I can't make sense of this code, it seems to try to convert the
case function corresponding to `let (a, b) = f n in ...` into a
different case function where `f n` and `(a, b)` have been unified.
But if `f n` is a bona fide stuck computation, there's no chance of
this happening.

Just turning this off solves the #1782 and only breaks one function
in the whole of the idris2 repo (I would have expected our current
termination oracle to be too weak to detect it as valid anyway!)
and one in frex (which, again, should not have been seen as terminating).

Also fixes #1460

Author: gallais

libs/base/Data/List1.idr

@@ -94,10 +94,12 @@ snoc xs x = xs ++ (singleton x)
 
 public export
 unsnoc : (xs : List1 a) -> (List a, a)
-unsnoc (h ::: Nil)       = (Nil, h)
-unsnoc (h ::: (x :: xs)) =
-  let (ini,lst) = unsnoc (x ::: xs)
-   in (h :: ini, lst)
+unsnoc (x ::: xs) = go x xs where
+
+  go : (x : a) -> (xs : List a) -> (List a, a)
+  go x [] = ([], x)
+  go x (y :: ys) = let (ini,lst) = go y ys
+                   in (x :: ini, lst)
 
 ------------------------------------------------------------------------
 -- Reverse

src/Core/Termination.idr

@@ -383,13 +383,15 @@ mutual
            let fn = fullname gdef
            log "totality.termination.sizechange" 10 $ "Looking under " ++ show !(toFullNames fn)
            aSmaller <- resolved (gamma defs) (NS builtinNS (UN "assert_smaller"))
-           cond [(fn == NS builtinNS (UN "assert_total"), pure []),
-              (caseFn fn,
-                  do mps <- getCasePats defs fn pats args
-                     case mps of
-                          Nothing => pure Prelude.Nil
-                          Just ps => do scs <- traverse (findInCase defs g) ps
-                                        pure (concat scs))]
+           cond [(fn == NS builtinNS (UN "assert_total"), pure [])
+              -- #1782: this breaks totality!
+              -- ,(caseFn fn,
+              --     do mps <- getCasePats defs fn pats args
+              --        case mps of
+              --             Nothing => pure Prelude.Nil
+              --             Just ps => do scs <- traverse (findInCase defs g) ps
+              --                           pure (concat scs))
+              ]
               (do scs <- traverse (findSC defs env g pats) args
                   pure ([MkSCCall fn
                            (expandToArity arity

src/Libraries/Data/List1.idr

@@ -6,9 +6,12 @@ import Data.List1
 
 -- TODO: Remove this, once Data.List1.unsnoc from base is available
 --       to the compiler
+
 export
 unsnoc : (xs : List1 a) -> (List a, a)
-unsnoc (h ::: Nil)       = (Nil, h)
-unsnoc (h ::: (x :: xs)) =
-  let (ini,lst) = Libraries.Data.List1.unsnoc (x ::: xs)
-   in (h :: ini, lst)
+unsnoc (x ::: xs) = go x xs where
+
+  go : (x : a) -> (xs : List a) -> (List a, a)
+  go x [] = ([], x)
+  go x (y :: ys) = let (ini,lst) = go y ys
+                   in (x :: ini, lst)

tests/Main.idr

@@ -171,7 +171,8 @@ idrisTestsTotality = MkTestPool "Totality checking" [] Nothing
       ["positivity001", "positivity002", "positivity003", "positivity004",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
-       "total006", "total007", "total008", "total009", "total010"
+       "total006", "total007", "total008", "total009", "total010",
+       "total011"
       ]
 
 idrisTests : TestPool

tests/idris2/total011/Issue1460.idr

@@ -0,0 +1,6 @@
+%default total
+
+nonproductive : Stream a -> (Stream a, ())
+nonproductive (x :: xs) =
+  case nonproductive xs of
+    (xs, ()) => (xs, ())

tests/idris2/total011/Issue1782.idr

@@ -0,0 +1,11 @@
+total
+notHack : Nat -> (Nat, Nat)
+notHack Z = (Z, Z)
+notHack (S n) = let (baz1, baz2) = notHack n
+                in (baz2, S baz1)
+
+
+total
+hack : Nat -> (Void, Void)
+hack n = let (baz1, baz2) = hack n
+         in (baz1, baz2)

tests/idris2/total011/expected

@@ -0,0 +1,16 @@
+1/1: Building Issue1782 (Issue1782.idr)
+Error: hack is not total, possibly not terminating due to recursive path Main.hack -> Main.hack
+
+Issue1782:8:1--9:27
+ 8 | total
+ 9 | hack : Nat -> (Void, Void)
+
+1/1: Building Issue1460 (Issue1460.idr)
+Error: nonproductive is not total, possibly not terminating due to recursive path Main.nonproductive -> Main.nonproductive -> Main.nonproductive
+
+Issue1460:3:1--3:43
+ 1 | %default total
+ 2 | 
+ 3 | nonproductive : Stream a -> (Stream a, ())
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+

tests/idris2/total011/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 Issue1782.idr --check
+$1 --no-color --console-width 0 Issue1460.idr --check