`simple-arith` executable won't compile with GHC 8.6.3 about ghc-typelits-presburger HOT 2 CLOSED

I slightly modified the code of the plugin to get more clear logs.
It looks like GHC 8.6 gives to the plugin only flatten Skolem variable. And it is impossible to get the real value of the variable. Look to the TC dump with 8.4: there are a few records like
eqPred_beg1 CmpNat n 0 ~ fsk0
and
eqPred_beg1 Case_6989586621679397119 n 0 fsk0 ~ fsk1
but then there are the following pieces text:
eqPred_beg1 CmpNat n 0 ~ CmpNat n 0
and
eqPred_beg1 Case_6989586621679397119 n 0 (CmpNat n 0) ~ 'True

But in TC dump with 8.6 there are only records like:

eqPred_beg1CmpNat n 0 ~ fsk0
and
eqPred_beg1Case_6989586621679603933 n 0 fsk0 ~ 'True

It looks that the plugin can't get unflattened value for fsk0. And adding <=< unsafeTcPluginTcM . zonkTcType (look at the attached file) does not help :-(

This issue could be related to this problem

If I am right then the plugin system in GHC is really broken, because we can't get unflattened values in the plugin. And it could be broken because it has experimental status now (

Full dumps are also attached. I removed all functions from simple-arith except natLeqZero' to get a
more clear dump.

Presburger.zip
TCDump-GHC804.zip
TCDump-GHC806.zip

from ghc-typelits-presburger.

I've just done, in these two days, an overhaul on this (these) package and it seems that the plugin becomes compiling with GHC >= 8.6 (even with GHC 8.8). The current version is released on Hackage as 0.3.0.0.
Actually, it seems that the treatment of type-variables in Given constraints has changed in GHC 8.6, and I could found the workaround for that change.

If anything is still wrong with the current version, please feel free to reopen this issue or creating new issue!

from ghc-typelits-presburger.