Regression when solving inequalities

[rowanG077]

https://github.com/clash-lang/ghc-typelits-natnormalise/commit/2414721729a1f49dc4f7391433771138eeddd48d 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.