[ fix ] Totality checker misses indirect references to negative data

[dunhamsteve]

Idris reports a function as total when it indirectly references a negative data type, resulting in a proof of Void. This issue is reported in #527 and #3030. For direct references, the code in References.idr detects the call, but it cuts when it hits an Unchecked.

The totality checking would detect the issue, but data constructor calls are not included in sizeChange list (they do show up in refersTo). I believe this is an oversight, but I may be missing something. My reasoning should be double-checked by someone who knows the totality checker.

This PR changes findSC in CallGraph.idr to include DCon applications in the sizechange graph. I've done this in the TopLevel and Guarded cases. I've also adjusted test cases to reflect the addition entries in size change, and I updated one test to reflect additional partial functions that are detected. I added covering to REPL/Opts.idr in two places because it refers to a negative data type.

It fixes #527, fixes #3030, and is likely to break code that relies on faulty totalily results.

I have an alternative approach in a different branch, where I recursively call calcTermination on each reference of the function at the end of calcTermination. If my assumptions are correct, I believe the present solution is cleaner and provides better error messages - showing the path that fails.

As an example of the issue from the discussion at #3030, this proof of Void is accepted by Idris:

data Oops = MkOops (Not Oops)

total
runOops : Oops -> Not Oops
runOops (MkOops nf) = nf

total
notOops : Not Oops
notOops x = runOops x x

oops : Oops
oops = MkOops notOops

total
boom : Void
boom = runOops oops oops

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG.md (and potentially also
  CONTRIBUTORS.md).

[andrevidela]

I'm assuming this is good to go

[mjustus]

I am currently porting this to Yaffle and I am wondering whether we should accept functions involving data types that fail the positivity check as total in the first place.

If we didn't, runOops would be considered non-total. Which, I think, is fine but it would probably force us to come up with a more precise positivity checker.