From 878187d7f7e7e20b6628a971b457d5d2a95cf1c1 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 5 Aug 2023 11:15:30 -0700
Subject: [PATCH 1/3] [ fix ] Totality checker misses indirect references to
 partial data

---
 CHANGELOG.md                          |  3 ++
 src/Core/Termination/CallGraph.idr    | 16 ++++++--
 src/Idris/REPL/Opts.idr               |  2 +
 tests/Main.idr                        |  2 +-
 tests/idris2/positivity004/expected   | 54 ++++++++++++++++++++++++++-
 tests/idris2/total020/Issue-3030.idr  | 33 ++++++++++++++++
 tests/idris2/total020/Issue-3030b.idr | 18 +++++++++
 tests/idris2/total020/Issue-524.idr   | 14 +++++++
 tests/idris2/total020/expected        | 27 ++++++++++++++
 tests/idris2/total020/run             |  6 +++
 10 files changed, 168 insertions(+), 7 deletions(-)
 create mode 100644 tests/idris2/total020/Issue-3030.idr
 create mode 100644 tests/idris2/total020/Issue-3030b.idr
 create mode 100644 tests/idris2/total020/Issue-524.idr
 create mode 100644 tests/idris2/total020/expected
 create mode 100755 tests/idris2/total020/run

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fc70675b4..dd75e0d9e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -101,6 +101,9 @@
 
 * Fixed a bug that caused `f` to sometimes be replaced by `fx` after matching `fx = f x`.
 
+* Fixed a bug in the totality checker that missed indirect references to
+  partial data.
+
 ### Library changes
 
 #### Prelude
diff --git a/src/Core/Termination/CallGraph.idr b/src/Core/Termination/CallGraph.idr
index 083bf62d5..1f92096b8 100644
--- a/src/Core/Termination/CallGraph.idr
+++ b/src/Core/Termination/CallGraph.idr
@@ -101,11 +101,19 @@ mutual
                  do scs <- traverse (findSC defs env Unguarded pats) args
                     pure (concat scs)
              (Guarded, Ref fc (DataCon _ _) cn, args) =>
-                 do scs <- traverse (findSC defs env Guarded pats) args
-                    pure (concat scs)
+                 do Just ty <- lookupTyExact cn (gamma defs)
+                         | Nothing => do
+                              log "totality" 50 $ "Lookup failed"
+                              findSCcall defs env Guarded pats fc cn 0 args
+                    arity <- getArity defs [] ty
+                    findSCcall defs env Guarded pats fc cn arity args
              (Toplevel, Ref fc (DataCon _ _) cn, args) =>
-                 do scs <- traverse (findSC defs env Guarded pats) args
-                    pure (concat scs)
+                 do Just ty <- lookupTyExact cn (gamma defs)
+                         | Nothing => do
+                              log "totality" 50 $ "Lookup failed"
+                              findSCcall defs env Guarded pats fc cn 0 args
+                    arity <- getArity defs [] ty
+                    findSCcall defs env Guarded pats fc cn arity args
              (_, Ref fc Func fn, args) =>
                  do logC "totality" 50 $
                        pure $ "Looking up type of " ++ show !(toFullNames fn)
diff --git a/src/Idris/REPL/Opts.idr b/src/Idris/REPL/Opts.idr
index dec692129..e339f2459 100644
--- a/src/Idris/REPL/Opts.idr
+++ b/src/Idris/REPL/Opts.idr
@@ -59,6 +59,7 @@ record REPLOpts where
 litStyle : Maybe String -> Maybe LiterateStyle
 litStyle = join . map isLitFile
 
+covering
 export
 defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts
 defaultOpts fname outmode cgs
@@ -108,6 +109,7 @@ setMainFile : {auto o : Ref ROpts REPLOpts} ->
 setMainFile src = update ROpts { mainfile      := src,
                                  literateStyle := litStyle src }
 
+covering
 export
 resetProofState : {auto o : Ref ROpts REPLOpts} -> Core ()
 resetProofState = update ROpts { psResult := Nothing,
diff --git a/tests/Main.idr b/tests/Main.idr
index 0944e6e61..a6bf92dbd 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -233,7 +233,7 @@ idrisTestsTotality = MkTestPool "Totality checking" [] Nothing
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009", "total010",
        "total011", "total012", "total013", "total014", "total015",
-       "total016", "total017", "total018", "total019"
+       "total016", "total017", "total018", "total019", "total020"
       ]
 
 -- This will only work with an Idris compiled via Chez or Racket, but at
diff --git a/tests/idris2/positivity004/expected b/tests/idris2/positivity004/expected
index 6448c0954..0f3eef7d2 100644
--- a/tests/idris2/positivity004/expected
+++ b/tests/idris2/positivity004/expected
@@ -14,6 +14,26 @@ Issue1771-1:4:3--4:8
  4 |   MkFix : f (Fix f) -> Fix f
        ^^^^^
 
+Error: argh is not total, possibly not terminating due to function Main.MkFix being reachable via Main.yesF -> Main.MkFix
+
+Issue1771-1:15:1--15:12
+ 11 | 
+ 12 | notF : Not F
+ 13 | notF (MkFix f) = f (yesF f)
+ 14 | 
+ 15 | argh : Void
+      ^^^^^^^^^^^
+
+Error: notF is not total, possibly not terminating due to call to Main.yesF
+
+Issue1771-1:12:1--12:13
+ 08 | 
+ 09 | yesF : Not F -> F
+ 10 | yesF nf = MkFix nf
+ 11 | 
+ 12 | notF : Not F
+      ^^^^^^^^^^^^
+
 Error: yesF is not total, possibly not terminating due to call to Main.MkFix
 
 Issue1771-1:9:1--9:18
@@ -40,6 +60,26 @@ Issue1771-2:4:3--4:8
  4 |   MkFix : ((0 g : Type -> Type) -> g === Not -> g F) -> F
        ^^^^^
 
+Error: argh is not total, possibly not terminating due to function Main.MkFix being reachable via Main.yesF -> Main.MkFix
+
+Issue1771-2:14:1--14:12
+ 10 | notF (MkFix f) =
+ 11 |   let g = f Not Refl in
+ 12 |   g (yesF g)
+ 13 | 
+ 14 | argh : Void
+      ^^^^^^^^^^^
+
+Error: notF is not total, possibly not terminating due to call to Main.yesF
+
+Issue1771-2:9:1--9:13
+ 5 | 
+ 6 | yesF : Not F -> F
+ 7 | yesF nf = MkFix (\ g, Refl => nf)
+ 8 | 
+ 9 | notF : Not F
+     ^^^^^^^^^^^^
+
 Error: yesF is not total, possibly not terminating due to call to Main.MkFix
 
 Issue1771-2:6:1--6:18
@@ -67,7 +107,17 @@ Issue1771-3:10:3--10:6
  10 |   MkF : Wrap (Not F) -> F
         ^^^
 
-Error: notF is not total, possibly not terminating due to call to Main.F
+Error: argh is not total, possibly not terminating due to function Main.MkF being reachable via Main.yesF -> Main.MkF
+
+Issue1771-3:18:1--18:12
+ 14 | 
+ 15 | notF : Not F
+ 16 | notF (MkF f) = unwrap f (yesF $ unwrap f)
+ 17 | 
+ 18 | argh : Void
+      ^^^^^^^^^^^
+
+Error: notF is not total, possibly not terminating due to calls to Main.F, Main.yesF
 
 Issue1771-3:15:1--15:13
  11 | 
@@ -77,7 +127,7 @@ Issue1771-3:15:1--15:13
  15 | notF : Not F
       ^^^^^^^^^^^^
 
-Error: yesF is not total, possibly not terminating due to calls to Main.F, Main.MkF
+Error: yesF is not total, possibly not terminating due to call to Main.MkF
 
 Issue1771-3:12:1--12:18
  08 | 
diff --git a/tests/idris2/total020/Issue-3030.idr b/tests/idris2/total020/Issue-3030.idr
new file mode 100644
index 000000000..46badcc9f
--- /dev/null
+++ b/tests/idris2/total020/Issue-3030.idr
@@ -0,0 +1,33 @@
+
+-- %default total
+
+record Oops where
+  constructor MkOops
+  runOops : Not Oops
+
+total
+notOops : Not Oops
+notOops x = runOops x x
+
+-- total
+oops : Oops
+oops = MkOops notOops
+
+total
+boom : Void
+boom = runOops oops oops
+
+data Foo = MkFoo (Not Foo)
+
+runFoo : Foo -> Not Foo
+runFoo (MkFoo nf) = nf
+
+notFoo : Not Foo
+notFoo x = runFoo x x
+
+foo : Foo
+foo = MkFoo notFoo
+
+total
+boom2 : Void
+boom2 = runFoo foo foo
diff --git a/tests/idris2/total020/Issue-3030b.idr b/tests/idris2/total020/Issue-3030b.idr
new file mode 100644
index 000000000..18ba1f759
--- /dev/null
+++ b/tests/idris2/total020/Issue-3030b.idr
@@ -0,0 +1,18 @@
+
+data Oops = MkOops (Not Oops)
+
+total
+runOops : Oops -> Not Oops
+runOops (MkOops nf) = nf
+
+total
+notOops : Not Oops
+notOops x = runOops x x
+
+covering
+oops : Oops
+oops = MkOops notOops
+
+total
+boom : Void
+boom = runOops oops oops
diff --git a/tests/idris2/total020/Issue-524.idr b/tests/idris2/total020/Issue-524.idr
new file mode 100644
index 000000000..23fd25297
--- /dev/null
+++ b/tests/idris2/total020/Issue-524.idr
@@ -0,0 +1,14 @@
+data Bad = MkBad (Not Bad)
+
+hmmm : Bad -> Not Bad
+hmmm (MkBad n) = n
+
+ok : Not Bad
+ok bad = hmmm bad bad
+
+bad : Bad
+bad = MkBad ok
+
+total
+ohno : Void
+ohno = ok bad
diff --git a/tests/idris2/total020/expected b/tests/idris2/total020/expected
new file mode 100644
index 000000000..2c4c2ca7d
--- /dev/null
+++ b/tests/idris2/total020/expected
@@ -0,0 +1,27 @@
+1/1: Building Issue-3030 (Issue-3030.idr)
+Error: boom is not total, possibly not terminating due to function Main.MkOops being reachable via Main.oops -> Main.MkOops
+
+Issue-3030:16:1--17:12
+ 16 | total
+ 17 | boom : Void
+
+Error: boom2 is not total, possibly not terminating due to function Main.MkFoo being reachable via Main.foo -> Main.MkFoo
+
+Issue-3030:31:1--32:13
+ 31 | total
+ 32 | boom2 : Void
+
+1/1: Building Issue-3030b (Issue-3030b.idr)
+Error: boom is not total, possibly not terminating due to function Main.MkOops being reachable via Main.oops -> Main.MkOops
+
+Issue-3030b:16:1--17:12
+ 16 | total
+ 17 | boom : Void
+
+1/1: Building Issue-524 (Issue-524.idr)
+Error: ohno is not total, possibly not terminating due to function Main.MkBad being reachable via Main.bad -> Main.MkBad
+
+Issue-524:12:1--13:12
+ 12 | total
+ 13 | ohno : Void
+
diff --git a/tests/idris2/total020/run b/tests/idris2/total020/run
new file mode 100755
index 000000000..1f977a622
--- /dev/null
+++ b/tests/idris2/total020/run
@@ -0,0 +1,6 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check Issue-3030.idr
+$1 --no-color --console-width 0 --no-banner --check Issue-3030b.idr
+$1 --no-color --console-width 0 --no-banner --check Issue-524.idr
+

From 0b3e04aef069fdadc4905e0891a2e8dfbc8e3ae7 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 12 Aug 2023 12:57:55 -0700
Subject: [PATCH 2/3] update tests for DCon in size change

---
 tests/idris2/casetree003/expected | 2 +-
 tests/idris2/coverage018/expected | 2 ++
 tests/idris2/debug001/expected    | 8 +++++---
 tests/idris2/inlining001/expected | 4 ++++
 tests/idris2/lazy003/expected     | 2 +-
 5 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/tests/idris2/casetree003/expected b/tests/idris2/casetree003/expected
index c737896b6..7545583cc 100644
--- a/tests/idris2/casetree003/expected
+++ b/tests/idris2/casetree003/expected
@@ -14,6 +14,6 @@ Compiled: \ {arg:1}, {arg:2} => case {arg:2} of
 Refers to: Main.view, Main.idL, Prelude.Basics.Nil, Prelude.Basics.(::)
 Refers to (runtime): Main.view, Main.idL, Main.Nil, Main.(::), Prelude.Basics.Nil, Prelude.Basics.(::)
 Flags: covering
-Size change: Main.idL: [Just (0, Same), Just (2, Smaller), Nothing]
+Size change: Prelude.Basics.Nil: [Just (0, Same)], Prelude.Basics.(::): [Just (0, Same), Just (2, Smaller), Nothing], Main.idL: [Just (0, Same), Just (2, Smaller), Nothing]
 Main> 
 Bye for now!
diff --git a/tests/idris2/coverage018/expected b/tests/idris2/coverage018/expected
index 2aab32ecc..1a5cb76d5 100644
--- a/tests/idris2/coverage018/expected
+++ b/tests/idris2/coverage018/expected
@@ -22,6 +22,7 @@ Compiled: \ {arg:0} => case {arg:0} of
   }
 Refers to: Prelude.Basics.True, Prelude.Basics.False
 Flags: allguarded, covering
+Size change: Prelude.Basics.True: [], Prelude.Basics.False: []
 Issue1831_1> 
 Bye for now!
 1/1: Building Issue1831_2 (Issue1831_2.idr)
@@ -48,5 +49,6 @@ Compiled: \ {arg:0} => case {arg:0} of
   }
 Refers to: Prelude.Basics.True, Prelude.Basics.False
 Flags: allguarded, covering
+Size change: Prelude.Basics.True: [], Prelude.Basics.False: []
 Issue1831_2> 
 Bye for now!
diff --git a/tests/idris2/debug001/expected b/tests/idris2/debug001/expected
index 1025d2aa9..865aed30c 100644
--- a/tests/idris2/debug001/expected
+++ b/tests/idris2/debug001/expected
@@ -11,6 +11,7 @@ Compiled: \ {arg:0} => case {arg:0} of
 Refers to: Prelude.Basics.True, Prelude.Basics.False
 Refers to (runtime): Prelude.Types.Nat
 Flags: allguarded, covering
+Size change: Prelude.Basics.True: [], Prelude.Basics.False: []
 Main> Main.isInt32
 Arguments [{arg:0}]
 Compile time tree: case {arg:0} of
@@ -23,6 +24,7 @@ Compiled: \ {arg:0} => case {arg:0} of
 Refers to: Prelude.Basics.True, Prelude.Basics.False
 Refers to (runtime): Int32
 Flags: allguarded, covering
+Size change: Prelude.Basics.True: [], Prelude.Basics.False: []
 Main> Prelude.Types.plus
 Arguments [{arg:0}, {arg:1}]
 Compile time tree: case {arg:0} of
@@ -35,7 +37,7 @@ Compiled: \ {arg:0}, {arg:1} => case {arg:0} of
   }
 Refers to: Prelude.Types.plus, Prelude.Types.S
 Flags: total
-Size change: Prelude.Types.plus: [Just (0, Smaller), Just (1, Same)]
+Size change: Prelude.Types.S: [Nothing], Prelude.Types.plus: [Just (0, Smaller), Just (1, Same)]
 Main> Prelude.Types.minus
 Arguments [{arg:0}, {arg:1}]
 Compile time tree: case {arg:0} of
@@ -63,7 +65,7 @@ Compiled: \ {arg:0}, {arg:1} => case {arg:0} of
 Refers to: Prelude.Types.minus, Prelude.Types.Z
 Refers to (runtime): Prelude.Types.prim__integerToNat
 Flags: total
-Size change: Prelude.Types.minus: [Just (0, Smaller), Just (1, Smaller)]
+Size change: Prelude.Types.Z: [], Prelude.Types.minus: [Just (0, Smaller), Just (1, Smaller)]
 Main> Prelude.Types.SnocList.filter
 Arguments [{arg:0}, {arg:1}, {arg:2}]
 Compile time tree: case {arg:2} of
@@ -78,6 +80,6 @@ Compiled: \ {arg:1}, {arg:2} => case {arg:2} of
 Refers to: Prelude.Basics.SnocList, Prelude.Basics.Lin, Prelude.Types.SnocList.case block in filter, Prelude.Types.SnocList.filter
 Refers to (runtime): Prelude.Basics.Lin, Prelude.Basics.(:<), Prelude.Types.SnocList.filter
 Flags: total
-Size change: Prelude.Types.SnocList.filter: [Just (0, Same), Just (1, Same), Just (2, Smaller)]
+Size change: Prelude.Basics.Lin: [Just (0, Same)], Prelude.Types.SnocList.filter: [Just (0, Same), Just (1, Same), Just (2, Smaller)], Prelude.Basics.(:<): [Just (0, Same), Nothing, Just (2, Smaller)]
 Main> 
 Bye for now!
diff --git a/tests/idris2/inlining001/expected b/tests/idris2/inlining001/expected
index 118c7f2b5..f38209e97 100644
--- a/tests/idris2/inlining001/expected
+++ b/tests/idris2/inlining001/expected
@@ -19,22 +19,26 @@ Compile time tree: 10
 Compiled: 10
 Refers to: Prelude.Types.Z, Prelude.Types.S
 Flags: allguarded, covering, noinline
+Size change: Prelude.Types.S: [Nothing], Prelude.Types.Z: []
 Main> Main.heuristicPublicInline
 Arguments []
 Compile time tree: 2
 Compiled: 2
 Refers to: Prelude.Types.Z, Prelude.Types.S
 Flags: inline, allguarded, covering
+Size change: Prelude.Types.S: [Nothing], Prelude.Types.Z: []
 Main> Main.exportedForced
 Arguments []
 Compile time tree: 33
 Compiled: 33
 Refers to: Prelude.Types.Z, Prelude.Types.S
 Flags: allguarded, covering, inline
+Size change: Prelude.Types.S: [Nothing], Prelude.Types.Z: []
 Main> Main.exportedUnforced
 Arguments []
 Compile time tree: 66
 Compiled: 66
 Refers to: Prelude.Types.Z, Prelude.Types.S
 Flags: allguarded, covering
+Size change: Prelude.Types.S: [Nothing], Prelude.Types.Z: []
 Main> Bye for now!
diff --git a/tests/idris2/lazy003/expected b/tests/idris2/lazy003/expected
index d6f765214..bccbd8148 100644
--- a/tests/idris2/lazy003/expected
+++ b/tests/idris2/lazy003/expected
@@ -22,5 +22,5 @@ Compiled: \ {arg:0} => let f = Force Lazy (Main.switch {arg:0}) in
 Refers to: Main.case block in switch3, Main.{_:985}, Main.switch, Builtin.Pair, Prelude.Types.Nat
 Refers to (runtime): Main.switch, Builtin.MkPair
 Flags: covering
-Size change: Main.switch: [Just (0, Same)]
+Size change: Main.switch: [Just (0, Same)], Builtin.MkPair: [Nothing, Nothing, Nothing, Nothing]
 Main> Bye for now!

From 8c14e9527b48e1d7e18c4bb7e69c62dce71bc836 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Thu, 7 Sep 2023 20:26:18 -0700
Subject: [PATCH 3/3] [ test ] move test to correct location

---
 tests/idris2/{total020 => total/total021}/Issue-3030.idr  | 0
 tests/idris2/{total020 => total/total021}/Issue-3030b.idr | 0
 tests/idris2/{total020 => total/total021}/Issue-524.idr   | 0
 tests/idris2/{total020 => total/total021}/expected        | 0
 tests/idris2/{total020 => total/total021}/run             | 0
 5 files changed, 0 insertions(+), 0 deletions(-)
 rename tests/idris2/{total020 => total/total021}/Issue-3030.idr (100%)
 rename tests/idris2/{total020 => total/total021}/Issue-3030b.idr (100%)
 rename tests/idris2/{total020 => total/total021}/Issue-524.idr (100%)
 rename tests/idris2/{total020 => total/total021}/expected (100%)
 rename tests/idris2/{total020 => total/total021}/run (100%)

diff --git a/tests/idris2/total020/Issue-3030.idr b/tests/idris2/total/total021/Issue-3030.idr
similarity index 100%
rename from tests/idris2/total020/Issue-3030.idr
rename to tests/idris2/total/total021/Issue-3030.idr
diff --git a/tests/idris2/total020/Issue-3030b.idr b/tests/idris2/total/total021/Issue-3030b.idr
similarity index 100%
rename from tests/idris2/total020/Issue-3030b.idr
rename to tests/idris2/total/total021/Issue-3030b.idr
diff --git a/tests/idris2/total020/Issue-524.idr b/tests/idris2/total/total021/Issue-524.idr
similarity index 100%
rename from tests/idris2/total020/Issue-524.idr
rename to tests/idris2/total/total021/Issue-524.idr
diff --git a/tests/idris2/total020/expected b/tests/idris2/total/total021/expected
similarity index 100%
rename from tests/idris2/total020/expected
rename to tests/idris2/total/total021/expected
diff --git a/tests/idris2/total020/run b/tests/idris2/total/total021/run
similarity index 100%
rename from tests/idris2/total020/run
rename to tests/idris2/total/total021/run