idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 643 forks source link

JS/Node codegen for Stream cause error #4491

Open luochen1990 opened 6 years ago

luochen1990 commented 6 years ago

Steps to Reproduce

the file bug1.idr:

symbols : Stream Char
symbols = cycle (unpack "abc")

main : IO ()
main = do
    print $ take 10 symbols

and the command:

$ idris --codegen node bug1.idr -o bug1.js
idris: Can't happen pickAlt - impossible case found
CallStack (from HasCallStack):
  error, called at src\IRTS\LangOpts.hs:241:25 in idris-1.3.0-CM7OgpWXYDl5DkSeW84F9Q:IRTS.LangOpts

Expected Behavior

Compiles successfully.

Observed Behavior

Compiles failed.

jfdm commented 6 years ago

@luochen1990

In case you were not aware, IO is short hand for IO' FFI_C, and as such IO is only for use with the C codegen. For other backends, i.e. JS, there should be an equivalent IO' FFI_JS instances.

Thus, what you are experiencing is expected behaviour. However, the error message could be made better, as it is not clear (from the message) why Idris itself is failing.

Jan

luochen1990 commented 6 years ago

@jfdm thanks for your explanation, but the IO and JS_IO problem seems not explain everything, consider the following test:

symbols : Stream Char
symbols = cycle (unpack "abc")

symbols2 : Stream Char
symbols2 = cycle ['a', 'b', 'c']

symbols3 : List Char
symbols3 = unpack "abc"

main : IO ()
main = do
    print $ take 10 symbols3

when I use symbols3, it works correctly and the correct js file is generated. and things works well on symbols2 too, but for symbols it is just not working. it seems weird for me, and I thought there must be something wrong when we use Stream and unpack and js codegen together.