-
Notifications
You must be signed in to change notification settings - Fork 375
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Totality checker inconsistency when using Inf #3345
Comments
I'd say that's a duplicate of #806 |
Yeah, sounds like the same thing, plus the way I'm not sure about the actual rules for implicit |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Problem
Sometimes the totality checker validates a function as total when it's not.
In particular, this happens when using
Inf
in the return type, combined with having the recursive path inside a lambda expression passed to another function.Steps to reproduce
The following example typechecks:
This makes it possible to prove
Void
:Additional notes
When
Inf
is not used as part of the return type ofneverReturn
, the behavior is correct:The same thing happens if we inline
$
:Or if we replace
$
with a hole:Or if we use
$
with its infix notation:📝 My Idris version is
Idris 2, version 0.7.0-c74f54c12
.The text was updated successfully, but these errors were encountered: