Type Checker Plugin: Producing the correct evidence

[Jan Bracker]

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/MainPolymonad.hs
[3]
https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymonad/Plugin/Evidence.hs
[4]
http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect-State.html
[5]
http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151105/3f0cc75d/attachment.html>