Regression when solving inequalities
rowanG077 opened this issue · 2 comments
2414721 introduces a regression.
I don't have a small reproducer but this is essentially what happens:
If we have the following givens:
fsk_akFr + fsk_akEb ~ fsk_akFt
fsk_akDn - 1 ~ fsk_akFr
1 <=? F a ~ True
1 <=? G b ~ True
1 <=? fsk_akEb ~ True
fsk_akEb ~ F a
fsk_akFt ~ G b
And this wanted 1 <= fsk_akFt.
Prior to that PR it can use the givens on the flattening skolems to solve the wanted. However the current master will unflatten the wanted to 1 <= F a + G b. The plugin does not recover or does use the other givens to allow the inequality to be solved.
Found when I tried to apply the most recent plugin version on https://github.com/rowanG077/clash-netlist-gen-bug
The traces are huge so I have attached the relevant fragment. fails.txt is with the commit that introduces the regression and works.txt without. The diff between fails.txt and works.txt is very small.
"ez fix" is just to try and solve both flattened and unflattened wanteds. But since we observe other, similar, problems. It might be better to rethink the approach.
From ghc 9.4 onwards, we only have unflattened constraints to begin with. So we’ll need a different solution than trying to solve both the flattened and unflattened version.