Interfaces with partial methods seen as total

[gallais]

The implementation of an interface with methods marked as partial will be seen as total
and so will the interface methods. And so, simply by wrapping/unwrapping a partial function
via an interface, we can get a total proof of Void.

%default total

interface Pointed a where
  partial
  point : a

partial
void : Nat -> Void
void (S n) = void n

Pointed Void where
  point = void 0

argh : Void
argh = point