Warnings for partial functions and holes

[bbarker]

I think it would be useful to have (the option, whether default or not) to report if there are partial functions or holes left in the code when compiling it.

Also, I'm very new to Idris2, so it is possible I missed something - this came to mind while looking at the following function in the crash course:

partial fromMaybe : Maybe a -> a
fromMaybe (Just x) = x

[bbarker]

Ah, looks like it is on the todo list here, I think: https://idris2.readthedocs.io/en/latest/tutorial/theorems.html#directives-and-compiler-flags-for-totality. For instance,

$ idris2 hello.idr --warnpartial -o hello

does not indicate any warnings for typed holes or for functions that are declared partial.

[gallais]

The machinery is already there as you can use :m from the REPL to see the leftover holes so it should not be too much work to get that printed from the command line.

The --warnpartial may be a bit more work though.

[falsifian]

This allows proving Void. (Example from z_snail on Discord.)

0 lemma : Void = a

ohNo : Void
ohNo = rewrite lemma in 0

There is no warning from the interpreter, as shown below. I think there is also no warning if you build a package with a similar problem.

I would love to see this implemented because I'm always worried I will forget to write a proof!

angel tmp $ ~/.idris2/bin/idris2 f.idr
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.5.1
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main> ohNo
0
Main> 

[gallais]

@falsifian Can you please post this as a separate bug report? This is accepted even with %default total which indeed makes it a proof of false in my book.