Proof of `Void` using holes the compiler never warns about

[falsifian]

Originally posted as a comment on #686. Credit to z_snail on Discord.

It's possible to prove Void by simply not bothering to prove a critical step.

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. %default total doesn't help.

I am always worried I will forget to prove something. I really wish the compiler would tell me!

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> 

[iacore]

Totality checker treat holes as total. Maybe there :t ohNo should show holes ohNo depend on, like lemma.

Try to type check this

total
n: Nat -- no definition

We can effects to formalize holes. total/partial is simply not enough to describe a function.

For example

Main> :total 1
no holes

Main> :total onNo
holes:
lemma : Void = a