Incomprehensible Crash

[hafizhmakmur]

This code will result in an incomprehensible crash if the last two functions are uncommented. The error log looks something like this

LiquidHaskell Version 0.8.6.0, Git revision 1d8c11324bb718eb3bd5c41643ba4b1cc377abf2 (dirty) [develop@1d8c11324bb718eb3bd5c41643ba4b1cc377abf2 (Thu Jul 11 14:48:47 2019 -0700)] 
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: resources/custom/liquidhaskell/sandbox/1601445373_15938.hs
�[1;94m
**** [Checking: resources/custom/liquidhaskell/sandbox/1601445373_15938.hs] ****
�[0m�[1;94m
**** DONE:  A-Normalization ****************************************************
�[0m�[1;90m 
�[0m�[1;94m
**** DONE:  Extracted Core using GHC *******************************************
�[0m�[1;90m 
�[0m�[1;94m
**** DONE:  Transformed Core ***************************************************
�[0m�[1;90m 
�[0mliquid: safeBkArrow on RAllT(~# Nat Nat n2 (Incr c2 n), Valid c2 c1 c2) =>
lq_tmp$x##3459:(SColor c2) -> lq_tmp$x##3460:(CT n c1 a) -> lq_tmp$x##3461:a -> lq_tmp$x##3462:(CT n c2 a) -> (CT n2 c2 a)
CallStack (from HasCallStack):
  error, called at src/Language/Haskell/Liquid/Types/Types.hs:1344:29 in liquidhaskell-0.8.6.0-LMX9LR0Q36VD86X8vrSnMD:Language.Haskell.Liquid.Types.Types

Weirdly my own LH can compile this code just fine.

[adinapoli]

Hey, thanks for logging an issue 😉 A couple of questions:

1. It looks like you are using version 0.8.6.0 when 0.8.10.2 is out, which includes a lot of bug fixes and the new source plugin. Any chance you can try out the code and see if it breaks with the latest and greatest as well?

2. Maybe it's asking too much, but are you able to provide us with a smaller reproduction case? I have given your code a quick look and there are GADTs and type families involved, which I think are both problematic for LH, generally speaking. It would be great to have a trimmed-down version to pinpoint the root cause.

3. What do you mean with "Weirdly my own LH can compile this code just fine." ?

Thanks!

[hafizhmakmur]

@adinapoli

1. (& 3.) So I just use the compiler from browser in https://liquid-demo.programming.systems/index.html :D so I can't really upgrade the LH. So LH that's installed in my computer is already version 8.10.2 so maybe the error is already fixed in later version. I was having trouble somewhere else in the code so I was trying to see a second opinion by using a different LH but I was greeted with this crash instead. I may send an issue about that trouble later :D .

2. It's not really my code and I'm still analyzing it in hope of verifying it with LH. But I thought the problem is already because of GADT so the code may not be able to be trimmed further. I'll see how much I can trim it and if I can pinpoint the root cause even further. The most I may be able to is this code in which I erase all functions which are not connected directly and modify the code so that it doesn't need type families anymore but it still involves GADT, and if the last function is uncommented it still crashes.

[adinapoli]

So LH that's installed in my computer is already version 8.10.2 so maybe the error is already fixed in later version.

Ah, I see, good. @ranjitjhala perhaps it's time for us to update the version of LH that is running on the demo platform, for consistency with what we have released lately?

[ranjitjhala]

Yes updating the web demo is on my to do list!

…

On Tue, Sep 29, 2020 at 11:33 PM Alfredo Di Napoli ***@***.***> wrote: So LH that's installed in my computer is already version 8.10.2 so maybe the error is already fixed in later version. Ah, I see, good. @ranjitjhala <https://urldefense.com/v3/__https://github.com/ranjitjhala__;!!Mih3wA!Wdek1UFHM0rEPE805UucQIwqpFZSRNRX5CaQr5Wpb8ZY6g_hegH4UW_x111ppUb1$> perhaps it's time for us to update the version of LH that is running on the demo platform, for consistency with what we have released lately? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1770*issuecomment-701187515__;Iw!!Mih3wA!Wdek1UFHM0rEPE805UucQIwqpFZSRNRX5CaQr5Wpb8ZY6g_hegH4UW_x1xBKUiOg$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OCWWFPKE4Z6XPZEF6LSILGL3ANCNFSM4R6U472Q__;!!Mih3wA!Wdek1UFHM0rEPE805UucQIwqpFZSRNRX5CaQr5Wpb8ZY6g_hegH4UW_x1ynodgIW$> .

[facundominguez]

I'm closing this one since I cannot reproduce it. I created another issue to have LH updated in the demo: ucsd-progsys/liquid-server#22.