<div dir="ltr">Hello,<div><br></div><div>I am using type checker plugins to select specific instances in a program.</div><div><br></div><div>My current problem concerns the following instance:</div><div><br></div><div><div>class Polymonad m n p where</div><div>  (>>=) :: m a -> (a -> n b) -> p b</div></div><div><br></div><div><div>instance ( Effect m, E.Inv m f (Unit m), f ~ Plus m f (Unit m))</div><div>        => Polymonad (m (f :: [*])) Identity (m (f :: [*])) where</div><div>  ma >>= f = ma E.>>= (E.return . runIdentity . f)</div></div><div><br></div><div>'E', 'Unit' and 'Plus' refer to the module 'Control.Effect' [5] from the 'effect-monad' package.</div><div><br></div><div>At some point in my example program [2] GHC is uncertain which instance to use for the '>>=' operator. The wanted constraint is:</div><div><br></div><div><div>[W] $dPolymonad_a5Qp :: Polymonad</div><div>                            (State '[n :-> (a :! 'W)])</div><div>                            Identity</div><div>                            (State '[n :-> (a :! 'W)]) (CNonCanonical)</div></div><div><br></div><div>To select the instance above I produce the following evidence:</div><div><br></div><div><div>$fPolymonadmIdentitym @[State, '[n :-> (a :! 'W)]]</div><div>                         [$fEffect[]State @[] []]</div></div><div><br></div><div>'State' is from the module 'Control.Effect.State' [4]. This works so far, but during the core-lint phase I get the following error message:</div><div><br></div><div><div><no location info>: Warning:</div><div>    [RHS of $dPolymonad_a5Qp :: Polymonad</div><div>                                  (State '[n_a5PL :-> (a_a5PM :! 'W)])</div><div>                                  Identity</div><div>                                  (State '[n_a5PL :-> (a_a5PM :! 'W)])]</div><div>    The type of this binder doesn't match the type of its RHS: $dPolymonad_a5Qp</div><div>    Binder's type: Polymonad</div><div>                     (State '[n_a5PL :-> (a_a5PM :! 'W)])</div><div>                     Identity</div><div>                     (State '[n_a5PL :-> (a_a5PM :! 'W)])</div><div>    Rhs type: (Inv State '[n_a5PL :-> (a_a5PM :! 'W)] (Unit State),</div><div>               '[n_a5PL :-> (a_a5PM :! 'W)]</div><div>               ~ Plus State '[n_a5PL :-> (a_a5PM :! 'W)] (Unit State)) =></div><div>              Polymonad</div><div>                (State '[n_a5PL :-> (a_a5PM :! 'W)])</div><div>                Identity</div><div>                (State '[n_a5PL :-> (a_a5PM :! 'W)])</div></div><div><br></div><div>Which I parse as a missing proof that the instance constraints are fulfilled by the evidence.</div><div><br></div><div>From this I have a few questions:</div><div><br></div><div>1. Why doesn't the type checker prove these type equality constraints for me? (or how can I get the type checker to do so?) I checked them on paper and the constraints are solvable and the equalities are true.</div><div><br></div><div>2. If I can't get the type checker to solve this for me, how do I produce appropriate evidence?</div><div><br></div><div>3. Another issue I see is that I would need to expand the type synonym 'E.Inv' to see what constraints it contains. I there an easy way to do so in GHC? I could not find appropriate functionality. It would be very useful for me if there was a function 'Type -> TcM Type' that evaluates the type as far as possible (by evaluate I mean expand synonyms, evaluate type functions and remove equalities that hold).</div><div><br></div><div>The example program [2] and the plugin I am developing can be found [1] on GitHub (Commit fefc149ec6e1c1a3c3c2597c66d176854b94287d ). This is how I produce the evidence for my selected instance [3]. I hope this abstract description of my problem is enough.</div><div><br></div><div>Best regards,</div><div>Jan Bracker</div><div><br></div><div>[1] <a href="https://github.com/jbracker/polymonad-plugin">https://github.com/jbracker/polymonad-plugin</a></div><div>[2] <a href="https://github.com/jbracker/polymonad-plugin/blob/master/examples/effect/MainPolymonad.hs">https://github.com/jbracker/polymonad-plugin/blob/master/examples/effect/MainPolymonad.hs</a></div><div>[3] <a href="https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymonad/Plugin/Evidence.hs">https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymonad/Plugin/Evidence.hs</a></div><div>[4] <a href="http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect-State.html">http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect-State.html</a></div><div>[5] <a href="http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect.html">http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect.html</a></div><div><br></div></div>