[ fix ] Totality checker misses indirect references to partial data

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

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)

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,

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

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 | 

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

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

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

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
+

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
+