Andres Löh

I cannot reproduce this with released `liquidhaskell-0.8.10.2`, `liquid-base-4.14.1.0`. I don't think `liquid-prelude` is needed here. I'll try with the specified commit.

I cannot reproduce this with the given commit either. The file yields `SAFE (2 constraints checked)` for me.

Ok, that helps. I can now reproduce the crash both with the released version and with current `develop`: ```haskell {-@ LIQUID "--reflection" @-} module Bug where import Control.Arrow (first) {-@...

Sorry, I've only just seen this. Without having looked at the code yet, the problem with ```haskell {-@ data FEnv where FCons :: { g:Int | False } -> FEnv...

@nikivazou That sounds like a plausible workaround to me. The rules for identifiers are somewhat complicated in LH right now, so I'm not sure if this will be without problems,...

@nikivazou We may have a similar pitfall for class declarations though ...

@nikivazou One strange interaction I had not been aware of yet is that for `data ... where`, there's currently no new layout block being introduced for the constructors, and they're...

More speculation from my side: I suspect LH allows providing a refinement type signature for a constructor in isolation, and uses it in the local module, but does not write...

For the parsing, we actually have multiple possibilities, with different trade-offs. First, some terminology: - A *faithful* implementation of the layout rule allows a new block to start only on...

@nikivazou So the result of the call yesterday was a bit different, but we can still discuss it again: - Faithful layout rule. - Require classes and datatypes to list...