Facundo Domínguez

I force-pushed a rehashing of the changes that preserves the old BulkSync mode, which the network team suggested in the last review call.

Here's another proposal: We should always link the spec to a recursive binding if there is more than one closest binding at the same source location. If there are no...

Here's another example that doesn't work with the above strategy. ``` {-@ LIQUID "--ple" @-} module Test where {-@ reflect one @-} one :: Int -> Int one 1 =...

Another complicated case arises when compiling `tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Fusion/T.hs` without `-fbreak-point`. [loopU](https://github.com/ucsd-progsys/liquidhaskell/blob/1fc2b2ec85718327a4c9b2778cc1420b48212283/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Fusion/T.hs#L254) has a recursive binding called `trans`, nested inside another binding `go`. Without break points, verification fails with ``` benchmarks/bytestring-0.9.2.1/Data/ByteString/Fusion/T.hs:262:65: error:...

Thanks @simonpj for having a look. I guess at this point it is a matter of quality of the user experience. Should we have LH complain when a spec is...

> Surely the Haskell type sig is just a subset of the LH spec? Easy! Yes ... when the spec is complete. Sometimes the user could leave it to GHC....

I imagine it should be possible to add a measure like ```Haskell data DynType = TBool | TInt | TList DynType | TFun DynType DynType {-@ measure dynType :: Dyn...

I cannot reproduce this failure in the latest LH. But I get s similar failure if I try ```haskell {-@ LIQUID "--reflect" @-} {-@ reflect bad @-} bad :: [Bool]...

The verification takes more than a minute to complete (didn't wait to see if it would finish) and GBs of memory in the latest LH. I had to disable the...

We can drop support for GHC