[Haskell-cafe] AT solution: rebinding >>= for restricted monads

[David Roundy]

I've now almost got a FD solution to this problem, except that it won't
work, and I don't know why.  Of course, it's possible that the AT solution
won't work either (I'm still compiling ghc, should have it in the
morning...), but at least it seems far simpler.  My FD solution is below.
My trouble is that I really don't understand the limitations on FDs, which
as I understand it is why Simon P.J. opposes adding them to Haskell':
they're hard to understand.

This all seems to work (although you'll see that I was reduced to using
unsafeCoerce# in the IO instance, which is embarrassing--to say the
least--but not unsafe), until I hit the RealWitness instance at the bottom,
at which point ghc bombs out with:

Witness.hs:33:0:
    Couldn't match expected type `m'' (a rigid variable)
           against inferred type `RealWitness a a''
      `m'' is bound by the type signature for `>>' at Witness.hs:11:29
    When using functional dependencies to combine
      Witness WitnessReally a b (RealWitness a b),
(and a screenful more)

Any suggestions?

{-# OPTIONS -fno-implicit-prelude -fglasgow-exts #-}

module Witness ( Witness ) where

import GHC.Exts (unsafeCoerce#)
import Prelude hiding ( (>>), (>>=), return, fail )
import qualified Prelude as P ( (>>), (>>=), return, fail )

class Witness w a b m | w a b -> m, m -> w a b where
    (>>=) :: (Witness w a a' m', Witness w a' b m'') => m' x -> (x -> m'' y) -> m y
    (>>) ::  (Witness w a a' m', Witness w a' b m'') => m' x -> m'' y -> m y
    f >> g = f >>= const g
    private_return :: x -> m x
    fail :: String -> m x

return :: Witness w a a m => x -> m x
return = private_return

data WitnessIO

instance Witness WitnessIO () () IO where
    private_return = P.return
    fail = P.fail
    f >>= g = x2io f P.>>= y2io g
        where x2io :: Witness WitnessIO a b m => m x -> IO x
              x2io = unsafeCoerce#
              y2io :: Witness WitnessIO a b m => (y -> m x) -> (y -> IO x)
              y2io = unsafeCoerce#

data RealWitness a b c -- this would be concrete
data WitnessReally

instance Witness WitnessReally a b (RealWitness a b) where

{-
The following monad is what I'd like to define if I could use associated type synonyms:

class Witness w where
    type W w a b
    (>>=) :: W w a b x -> (x -> W w b c y) -> W w a c y
    (>>) :: W w a b x -> W w b c y -> W w a c y
    f >> g = f >>= const g
    return :: x -> W w a a x
    fail :: String -> W w a b x

instance Monad m => Witness m where
    W m a b = m
    (>>=) = Prelude.(>>=)
    (>>) = Prelude.(>>)
    return = Prelude.return
    fail = Prelude.fail
-}