-----Original Message----- From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe- bounces@haskell.org] On Behalf Of Stefan Holdermans Sent: Wednesday, August 03, 2005 1:01 AM To: haskell-cafe Subject: [Haskell-cafe] Problem type checking class-method implementation

Dear Haskellers,

Yesterday I stumbled upon a problem type checking a program involving multi-parameter type classes. GHC rejected the program; still, I was not immediately convinced it contained a type error. Having given it some more thoughts, I start to suspect that the type checker is in err and that the program is well-typed after all. But, well, I might be overlooking something obvious...

I have reduced my code to a small but hopelessly contrived example program exposing the problem. Please hang on.

Because we employ multi-parameter type classes, we need the Glasgow extensions:

{-# OPTIONS -fglasgow-exts #-}

Let's start easy and define the identity monad:

newtype Identity a = Identity {runIdentity :: a}

instance Monad Identity where return = Identity Identity a >>= f = f a

Then, let's introduce the foundations for the (contrived) example:

class (Monad m) => IsItem m i where processItem :: i -> m ()

class (Monad m) => IsProcessor p m | m -> p where process :: (IsItem m i) => i -> m () -- ...some more methods, possibly involving p...

So, an item is something that can be processed within the context of a certain monad, and a processor is something that can process an item of an appropriate type. Note the functional dependency from m to p: a processor type m uniquely determines the type of the processing context p.

Before we move on, consider this canonical item type, which is just a one-field record representing an implementation of the IsItem class:

newtype Item m = Item {processItemImpl :: m ()}

The corresponding instance declaration is obvious:

instance (Monad m) => IsItem m (Item m) where processItem = processItemImpl

Furthermore values of every type that is an instance of IsItem can be converted to corresponding Item values:

toItem :: (IsItem m i) => i -> Item m toItem = Item . processItem

Please stick with me, for we are now going to implement a monad transformer for processors (which, for this example, is really just

identity monad transformer):

newtype ProcessorT p m a = ProcessorT {runProcessorT :: m a}

instance (Monad m) => Monad (ProcessorT p m) where return = ProcessorT . return ProcessorT m >>= f = ProcessorT (m >>= runProcessorT . f)

instance (Monad m) => IsProcessor p (ProcessorT p m) where process = processItem

Then, finally, we use this transformer to derive a processor monad:

newtype Processor p a = Processor {unwrap :: ProcessorT p Identity a}

runProcessor :: Processor p a -> a runProcessor = runIdentity . runProcessorT . unwrap

So, we just make sure that Processor is a monad:

instance Monad (Processor p) where return = Processor . return Processor m >>= f = Processor (m >>= unwrap . f)

Now all what is left to do is declare Processor an instance of IsProcessor. To this end, we need to be able to cast items for Processor p to items for ProcessorT p Identity (for all p). The following function takes care of that:

castItem :: (IsItem (Processor p) i) => i -> Item (ProcessorT p Identity) castItem = Item . unwrap . processItem

Note that up 'til now everything is fine: GHC is happy, I am happy. But then, when all the hard work is done, and we just only have to connect

Stefan, the problem can be spotted in the following erased version of your program. data Identity a instance Monad Identity class (Monad m) => IsItem m i where processItem :: i -> m () class (Monad m) => IsProcessor p m | m -> p where process :: (IsItem m i) => i -> m () newtype Item m = Item {processItemImpl :: m ()} newtype ProcessorT p m a = ProcessorT {runProcessorT :: m a} instance (Monad m) => Monad (ProcessorT p m) instance (Monad m) => IsProcessor p (ProcessorT p m) newtype Processor p a = Processor {unwrap :: ProcessorT p Identity a} instance Monad (Processor p) where castItem :: (IsItem (Processor p) i) => i -> Item (ProcessorT p Identity) castItem = undefined instance IsProcessor p (Processor p) where process = Processor . process . castItem Recall the type error: Could not deduce (IsItem (Processor p1) i) from the context (IsProcessor p (Processor p), Monad (Processor p), IsItem (Processor p) i) The problem is basically in here: instance IsProcessor p (Processor p) where process = Processor . process . castItem By specializing function signatures according to the instance head, and by applying type checking constraints for functional composition, we get these types: Processor :: ProcessorT p Identity () -> Processor p () process :: process :: ( IsProcessor p (ProcessorT p Identity) , IsItem (ProcessorT p1 Identity) () ) => Item (ProcessorT p1 Identity) -> ProcessorT p Identity () castItem :: (IsItem (Processor p1) i) => i -> Item (ProcessorT p1 Identity) The problem is the type-scheme polymorphic result type of castItem which is consumed by a type-variable polymorphic but type-class bounded argument type of process. The constraint of this application process, i.e., IsItem (Processor p1) i is the one GHC asks for. (Do the hugs test :-)) Ralf the things

properly, it just breaks:

instance IsProcessor p (Processor p) where process = Processor . process . castItem

After adding this last instance declaration, GHC happily reports:

Processor.hs:56:24: Could not deduce (IsItem (ProcessorT p Identity) (Item (ProcessorT p1 Identity))) from the context (IsProcessor p (Processor p), Monad (Processor p), IsItem (Processor p) i) arising from use of `process' at Processor.hs:56:24-30 Probable fix: add (IsItem (ProcessorT p Identity) (Item (ProcessorT p1 Identity))) to the class or instance method `process' or add an instance declaration for (IsItem (ProcessorT p Identity) (Item (ProcessorT p1 Identity))) In the first argument of `(.)', namely `process' In the second argument of `(.)', namely `process . castItem' In the definition of `process': process = Processor . (process . castItem)

Processor.hs:56:34: Could not deduce (IsItem (Processor p1) i) from the context (IsProcessor p (Processor p), Monad (Processor p), IsItem (Processor p) i) arising from use of `castItem' at Processor.hs:56:34-41 Probable fix: add (IsItem (Processor p1) i) to the class or instance method `process' or add an instance declaration for (IsItem (Processor p1) i) In the second argument of `(.)', namely `castItem' In the second argument of `(.)', namely `process . castItem' In the definition of `process': process = Processor . (process . castItem)

It seems to me that the type checker fails to unify p and p1 where it really should. But once again: I may be wrong here. So, could you either explain to me what I'm missing here and why this program is indeed ill-typed, or confirm that it's really just GHC that should be accepting this program.

I have attached a file Processor.hs containing the example program.