sanitychecks.lean:1:8-1:15: error: fail to show termination for
  unsound
with errors
failed to infer structural recursion:
no parameters suitable for structural recursion

well-founded recursion cannot be used, `unsound` does not take any (non-fixed) arguments
sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed
sanitychecks.lean:10:0-10:23: error: failed to synthesize 'Inhabited' or 'Nonempty' instance for
  False

If this type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
sanitychecks.lean:18:12-18:20: error: invalid use of `partial`, `Foo.unsound3` is not a function
  False
sanitychecks.lean:20:0-20:54: error: failed to compile 'partial' definition `Foo.unsound4`, could not prove that the type
  ∀ (x : Unit), False
is nonempty.

This process uses multiple strategies:
- It looks for a parameter that matches the return type.
- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance.
- It tries unfolding the return type.

If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
sanitychecks.lean:22:12-22:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
sanitychecks.lean:25:12-25:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'