[Haskell-cafe] 6.4 -> 6.6, scoped type variables, prescribing poly-/mono-morphism

[Nicolas Frisby]

I've been writing some code that relies heavily on the type system.
Some of my polymorphic functions end up too polymorphic.

I'm looking for some tips and references regarding prescribing
poly-/mono-morphism. I know of three ways to do it:
 1) rely on the monomorphism-restriction -- kind of scary in that its
not explicitly obvious
 2) introducing scoped-type variables of interest -- explicit and modular
 3) introducing all type variables with a forall -- explicit but not modular

The rest of this email is a discussion of a particular problem I'm
having. Scoped-type variables worked in 6.4, but no longer in 6.6. I'm
sure there's good reasons for this (I think I found a Peyton-Jones
message regarding it in 6.4->6.5) I just didn't quite catch on to
them.

The problem is in the |bop| function:

class SubType a v where -- the lack of fundeps is required by design
  inj :: a -> v
  lazyPrj :: v -> Maybe a

bop :: forall x y z m c v .
       ( SubType x v, SubType y v, SubType z v
       , SubType (Fun m c v) v
       , Monad m, Comonad c
       ) => (x -> y -> z) -> Fun m c v
bop op = Fun fn
    where fn = wrap fn'
              where fn' v0 = (inj . Fun) (wrap fn'')
                        where fn'' v1 = inj (lazyPrj v0 `op` lazyPrj v1)
          wrap :: (v -> v) -> (c v -> m v)
          wrap = (return .) . (. counit)

The explicit forall is needed to introduce the scoped type variables
so that I can prescribe the type of |wrap|. After that, the
monomorphism restriction on |wrap| takes care of the rest of my
worries (that there is only one |m|, only one |c|, and only one |v|).

If I leave the types to inference (i.e. drop the forall and the type
ascription for |wrap|), then I end up with this type

bop :: ( SubType x v2, SubType y v1, SubType z v1
         , SubType (Fun m c v1) v2
         , Monad m, Comonad c
         ) => (x -> y -> z) -> Fun m c v2

Note the multiple |v|s; they wreak havoc in the rest of my code. (The
monomorphism restriction still takes care of the |m| and |c|.)

I'd like to not have to introduce the forall, because with that comes
introducing the entire context of the type. Thus I have to maintain
any changes to the context, which I would prefer to leave to inference
for modularity's sake.

In 6.4 I was able to fix this without having to introduce the forall;
I could introduce scoped type-variables in patterns to get the job
done. That felt a bit like voodoo, especially when trying to get it
right for 6.6--which I gave up on doing. I can post the code that
works with 6.4 if anyone would like to see it (I just can't find it at
the moment).

I know there's some work on introducing partial signatures (fun pat |
False = ...), but I don't see how to prescribe monomorphism for
particular type variables in that way.

Any thoughts on how to get the preferred signature using scoped-type
variables in 6.6? I'd also welcome any references you might think are
relevant.

Thanks for your time,
Nick