Idris javascript codegen crash (pickAlt - impossible case found)

[leon-vv]

In a project I'm working on I ran into a bug of the Idris node/javascript code generator. While only using --check there is no problem and the code type checks.

Steps to Reproduce

I have tried to find the minimal amount of code that still triggers the compiler bug but I have a hard time getting it smaller than this. The compiler flags I used are: idris -p idrisscript --codegen node -o main.js ./Main.idr. Idris version: 1.2.0-git:06db7dc1

Expected Behavior

The correct production of main.js

Observed Behavior

The following error message:

idris: Can't happen pickAlt - impossible case found
CallStack (from HasCallStack):
  error, called at src/IRTS/LangOpts.hs:223:25 in idris-1.2.0-ek124hYSZX1HDxZk5PXQR:IRTS.LangOpts

[ahmadsalim]

Thanks for reporting the issue. Maybe your use of believe_me can be the cause, but consider asking @rbarreiro or @be5invis .

[rbarreiro]

Actually I already have checked this, did not posted anything because I did no reach the bottom of it. I will share what I was able to get, the IR expression that is causing the error is

case (Prelude.List.Nil()) of 
    | Prelude.List.::({in_15}, {in_16}) => case ({in_15}) of 
        | Builtins.MkPair({in_17}, {in_18}) => case (case (LStrEq({in_17}, "rows")) of 
            | 0 => Prelude.Bool.False()
            | _ => Prelude.Bool.True()) of 
            | Prelude.Bool.False() => Main.access({in_16}, {in_14}, "rows")
            | Prelude.Bool.True() => {in_13}

Usually I would expect a default clause, because the Nil constructor is not covered, and pickAlt is also expecting that: when the case expression is a constructor, to have it on one of the clauses or else to have default clause, hence the error. I will report here if I find something else.

Anyway this is before the js generator is called.

[be5invis]

LangOpts.hs is ran before the JS codegen. Does your issue reproduce in the C codegen?

[leon-vv]

This is really strange but I'm not able to reproduce this issue anymore. Something about my setup must have changed. I have no idea what changed, but I have not updated Idris or idrisscript

[leon-vv]

I figured out what changed. The issue is still here.

LangOpts.hs is ran before the JS codegen. Does your issue reproduce in the C codegen?

Indeed it does not matter what value I pass in for '--codegen'.