Allowing Instances to Unify Types

[Matt Brown]

Hi all,
I've been hacking on GHC for a couple months now, experimenting with
some different ideas I find interesting.  One thing I'm trying to do
is allow instance unifs (when there's an unambiguous choice, a
question which is simplified in this case by there being only one),
and force the required unification.  Here's a simple example:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances, UndecidableInstances #-}
class Apply a b c | a b -> c where
  applyInst :: a -> b -> c

instance (Monad m) => Apply (a -> m b) (m a) (m b) where
  applyInst = (=<<)

apply :: (Monad m) => (a -> m b) -> (m a) -> (m b)
apply = (=<<)

ioStr :: IO String
ioStr = return "foo"

printStr :: String -> IO ()
printStr = print

main = do print `apply` (return "foo")
          printStr `applyInst` ioStr
          print `applyInst` (return "bar")  -- this fails


With my code to use the unif instance enabled, I get Ambiguous type
variable errors for "Show a" (from print) and "Monad m" (from return).

My question is:  in the case of apply (which isn't implemented by a
class), how does the typechecker propagate "a ~ String" and "m ~ IO"
to the predicates for print and return?  If someone (such as myself)
had sufficient time and energy to spend trying to achieve similar
behavior for applyInst, where might he/I start?

Thanks and Regards,
-matt