Merge pull request #3043 from dunhamsteve/issue-3030

[ fix ] Totality checker misses indirect references to negative data

CHANGELOG.md

@@ -107,6 +107,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.
+
 * Refactor the idris2protocols package to depend on fewer Idris2 modules.
   We can now export the package independently.
   To avoid confusing tooling about which `.ipkg` to use, the

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/idris2/casetree/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!

tests/idris2/coverage/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!

tests/idris2/debug/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!

tests/idris2/misc/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!

tests/idris2/misc/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!

tests/idris2/total/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/total/total021/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/total/total021/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/total/total021/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/total/total021/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/total/total021/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
+