Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

Compiler accepts DivBy with impossible #4867

Open
Riateche opened this issue Jun 2, 2020 · 1 comment
Open

Compiler accepts DivBy with impossible #4867

Riateche opened this issue Jun 2, 2020 · 1 comment

Comments

@Riateche
Copy link

Riateche commented Jun 2, 2020

div_by_crash.idr.zip

Steps to Reproduce

import Data.Primitives.Views

total
bad: Int -> Int
bad x with (divides x 2)
  bad (_ + _) | (DivBy _) impossible

Expected Behavior

This should be a valid case. The function should not be considered total.

Observed Behavior

The compiler accepts this as a total function. It crashes at run time.
@Riateche
Copy link
Author

Can I get any confirmation or update on this?

# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Riateche