Regression when solving inequalities

[rowanG077]

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.

[rowanG077]

"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.

[christiaanb]

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.