Hello, I am using type checker plugins to select specific instances in a program. My current problem concerns the following instance: class Polymonad m n p where (>>=) :: m a -> (a -> n b) -> p b instance ( Effect m, E.Inv m f (Unit m), f ~ Plus m f (Unit m)) => Polymonad (m (f :: [*])) Identity (m (f :: [*])) where ma >>= f = ma E.>>= (E.return . runIdentity . f) 'E', 'Unit' and 'Plus' refer to the module 'Control.Effect' [5] from the 'effect-monad' package. At some point in my example program [2] GHC is uncertain which instance to use for the '>>=' operator. The wanted constraint is: [W] $dPolymonad_a5Qp :: Polymonad (State '[n :-> (a :! 'W)]) Identity (State '[n :-> (a :! 'W)]) (CNonCanonical) To select the instance above I produce the following evidence: $fPolymonadmIdentitym @[State, '[n :-> (a :! 'W)]] [$fEffect[]State @[] []] '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: <no location info>: Warning: [RHS of $dPolymonad_a5Qp :: Polymonad (State '[n_a5PL :-> (a_a5PM :! 'W)]) Identity (State '[n_a5PL :-> (a_a5PM :! 'W)])] The type of this binder doesn't match the type of its RHS: $dPolymonad_a5Qp Binder's type: Polymonad (State '[n_a5PL :-> (a_a5PM :! 'W)]) Identity (State '[n_a5PL :-> (a_a5PM :! 'W)]) Rhs type: (Inv State '[n_a5PL :-> (a_a5PM :! 'W)] (Unit State), '[n_a5PL :-> (a_a5PM :! 'W)] ~ Plus State '[n_a5PL :-> (a_a5PM :! 'W)] (Unit State)) => Polymonad (State '[n_a5PL :-> (a_a5PM :! 'W)]) Identity (State '[n_a5PL :-> (a_a5PM :! 'W)]) Which I parse as a missing proof that the instance constraints are fulfilled by the evidence.

From this I have a few questions:

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. 2. If I can't get the type checker to solve this for me, how do I produce appropriate evidence? 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). 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. Best regards, Jan Bracker [1] https://github.com/jbracker/polymonad-plugin [2] https://github.com/jbracker/polymonad-plugin/blob/master/examples/effect/Mai... [3] https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymon... [4] http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect-St... [5] http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect.ht...