Open donald-pinckney opened 5 years ago
If this code is accepted, I fear that the totality checker might fail at the call site. In order to let it work we might need to distinguish total functions and non-total functions at the type level.
Yeah, I think its a bit of a subtle issue. I don't really need or expect a fix anytime soon, as I can just use believe_me
to force my proof of NonEmpty
.
Steps to Reproduce
Consider the following code:
Expected Behavior
Both
things
andthings2
should be checked to be total. Sinceexplode
is never actually called, it should not affect the totality ofthings2
.Observed Behavior
Totality checker rejects
things2
.Usability Impact
In my situation I have a list of functions as in
things2
above, and I need to prove that the list of functions isNonEmpty
. But since the totality checker rejectsthings2
, in type checkingthings2
is never reduced to aCons
, and thus it seems impossible to prove thatthings2
is non-empty.