The inlineLoopBreaker transformation eliminates some auxiliary bindings that GHC produces that cause troubles to LH. Roughly,
v = \x1...xn ->
letrec v0 = \y0...ym -> e0
in v0 xj..xn
is converted to
v = \x1...xj y0...ym ->
e0 [ v0 := v x1...xj y0...ym ]
The difficulties for LH are explained in #2325, though I'm not sure that the description is exhaustive yet. This transformation does not always succeed. I've found that disabling -fbreak-points when compiling tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Fusion/T.hs produces an auxiliary binding that the current implementation cannot remove.
This PR arranges to call inlineLoopBreaker on inner lets, and makes it a bit more general as per the descriptions in the commits. These improvements are driven in turn by the opportunities to make LH more flexible to changes in GHC. One of the achievements is to get rid of an obscure transPg transformation on Core.
Another achievement is to make LH work without -fbreak-points in almost all tests. Breakpoints are inserted to make the desugarer more conservative on the auxiliary bindings that are introduced. I'm delivering the conclusion of it in another PR, though.
For now, I stop here with inlineLoopBreaker. It is possible that we can improve liquid-fixpoint so we don't have to be so strict about removing auxiliary bindings. And then we won't need to maintain a more complicated transformation here.
The
inlineLoopBreakertransformation eliminates some auxiliary bindings that GHC produces that cause troubles to LH. Roughly,is converted to
The difficulties for LH are explained in #2325, though I'm not sure that the description is exhaustive yet. This transformation does not always succeed. I've found that disabling
-fbreak-pointswhen compilingtests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Fusion/T.hsproduces an auxiliary binding that the current implementation cannot remove.This PR arranges to call
inlineLoopBreakeron inner lets, and makes it a bit more general as per the descriptions in the commits. These improvements are driven in turn by the opportunities to make LH more flexible to changes in GHC. One of the achievements is to get rid of an obscuretransPgtransformation on Core.Another achievement is to make LH work without
-fbreak-pointsin almost all tests. Breakpoints are inserted to make the desugarer more conservative on the auxiliary bindings that are introduced. I'm delivering the conclusion of it in another PR, though.For now, I stop here with
inlineLoopBreaker. It is possible that we can improveliquid-fixpointso we don't have to be so strict about removing auxiliary bindings. And then we won't need to maintain a more complicated transformation here.