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