Error in C tmp file

[nicolabotta]

On a fresh copy of https://gitlab.pik-potsdam.de/botta/IdrisLibs, you should be able to do

$ cd SequentialDecisionProblems/applications/
$ make emissionsgame2.1

and compile EmissionsGame2.1.lidr with one warning. But replacing line 854:

>                      mxys <- pure (adHocPossibleStateCtrlSeqs (FZ, High, Unavailable, Good) ps)

with

>                      mxys <- pure (adHocPossibleStateCtrlSeqs1 (FZ, High, Unavailable, Good) ps)

yields

$ make emissionsgame2.1
idris -O3 --warnreach -i .. -i ../.. --sourcepath .. --sourcepath ../.. +RTS -K32000000 -RTS -p contrib -p effects -V EmissionsGame2.1.lidr -o emissionsgame2.1
Type checking ./EmissionsGame2.1.lidr
WARNING: There are incomplete holes:
 [SequentialDecisionProblems.applications.Main.kika]

Evaluation of any of these will crash at run time.
Control.Isomorphism.eitherFinPlus: inaccessible arguments reachable:
  m (no more information available)
Control.Isomorphism.finPairTimes: inaccessible arguments reachable:
  n (no more information available)
  m (no more information available)
/tmp/idris17871.c: In function ‘_idris__123_APPLY0_125_’:
/tmp/idris17871.c:17355:5: error: duplicate case value
     case 65797:
     ^
/tmp/idris17871.c:17343:5: error: previously used here
     case 65797:
     ^
FAILURE: "gcc" ["-O2","-fwrapv","-fno-strict-overflow","-DHAS_PTHREAD","-DIDRIS_ENABLE_STATS","-I.","/tmp/idris17871.c","-L/home/nicola/.cabal/share/x86_64-linux-ghc-7.6.3/idris-0.99.1/rts/","-lidris_rts","-lpthread","-I/home/nicola/.cabal/share/x86_64-linux-ghc-7.6.3/idris-0.99.1/rts/","-lm","-I.","-I../base","-I../prelude","-I../..","-I..","-I/home/nicola/.cabal/share/x86_64-linux-ghc-7.6.3/idris-0.99.1/libs/contrib","-I/home/nicola/.cabal/share/x86_64-linux-ghc-7.6.3/idris-0.99.1/libs/effects","-I.","-I/home/nicola/.cabal/share/x86_64-linux-ghc-7.6.3/idris-0.99.1/libs/prelude","-I/home/nicola/.cabal/share/x86_64-linux-ghc-7.6.3/idris-0.99.1/libs/base","-o","emissionsgame2.1"]

Any idea how to avoid this error?

[nicolabotta]

File moved. Please, do

$ cd issues/
$ make error_in_C_tmp_file

to reproduce the above results.

[ahmadsalim]

@nicolabotta Thanks for reporting the issue! I guess the workaround is to avoid the renaming? In any case, this should never happen, so I will file it as critical.

[nicolabotta]

@ahmadsalim which renaming do you mean? In the program that yields the error at the C code level, mxys is computed with adHocPossibleStateCtrlSeqs1. In the program that yields no error, mxys is computed with adHocPossibleStateCtrlSeqs. Here adHocPossibleStateCtrlSeqs1 and adHocPossibleStateCtrlSeqs are two different functions.

[ahmadsalim]

@nicolabotta I missed the fact that they were completely different functions, and not just the same function renamed.