bogus proof for stuck type family - Polysemy

I broke polysemy,

<no location info>: error:
    bogus proof for stuck type family
CallStack (from HasCallStack):
  error, called at src/Polysemy/Plugin/Fundep.hs:178:9 in polysemy-plugin-0.2.5.0-BT55LwSy8F0v20rojK9yr:Polysemy.Plugin.Fundep

How it happened?

Refactoring some code, using dependent-sum set of libraries

All I did was this change: https://gist.github.com/srid/2dc18afadea2cb09e8fedf202c6aba2e

What happens when you change declaration of Tracking back to annotated one?

Doesn't change anything.

It is arising right when compiling an unrelated module (not shown in the diff)

(And that module only uses the effects polysemy TH generated, and doesn't define any effects itself)

I wish I could share it, but it is a mix of private stuff (I literally have Haskell types for moods, feelings, private narratives).

Try passing corelint flag to polysemy-plugin

as a cabal flag? i'm starting from scratch, recreating that diff piecemeal ...

Figured out where it is coming from. I had to comment out the actual DSL use, to make compilation succeed.

This triggers the error:

didSet (Squat :/) `mapM_` [10, 10]

And fix (to get rid of the error) is:

(didSet . (Squat :/)) `mapM_` [10, 10]

Looks like I've identified a bug in polysemy-plugin?

The corresponding Effect constructor is DidSet :: DSum Move Identity -> MyEffect m ()

And Squat :/ n is just alias for Squat :=> Identity n (of type DSum Move Identity)

I guess that's one more reason for plugin rewrite - but honestly, eff is getting closer with required primops being submitted as GHC proposal and I wonder how much of polysemy's internals will stay relevant once it comes out...

Though, eff will have the same problems that we solve with it, so maybe we want to decouple it (at least fundep part)

Impressive

try turning off custom error messages and i think it will work just fine