Skip to content
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

Lazy breaks data type #4579

Open
gittywithexcitement opened this issue Oct 29, 2018 · 1 comment
Open

Lazy breaks data type #4579

gittywithexcitement opened this issue Oct 29, 2018 · 1 comment

Comments

@gittywithexcitement
Copy link

gittywithexcitement commented Oct 29, 2018

Steps to Reproduce

Compile and run:
> idris --execute Bug.idr

Expected Behavior

> idris --execute Bug.idr
run
run
run
dry

Observed Behavior

It prints run only twice. The program seems to silently exit before printing more:

> idris --execute Bug.idr
run
run

The program

-- data Fuel = Dry | More Fuel
data Fuel = Dry | More (Lazy Fuel)

run : Fuel -> IO ()
run (More fuel) = do putStrLn "run"
                     run fuel
run Dry = putStrLn "dry"

main : IO ()
main = run (More $ More $ More Dry)

Notes

If you delete the 2nd line with Lazy Fuel, and uncomment the first line, it works as expected.

Bug observed in idris v1.3.0 and 1.3.1
OS: Debian 4.17

@atwupack
Copy link

atwupack commented Nov 1, 2018

There seems to be a difference between idris --execute and compiling to an executable and running it.
On Windows with version 1.3.1 (64bit) the excutable compiled from above code runs correctly. But using idris --execute stops after two lines with run as described above.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants