[Haskell-cafe] Problem type checking class-method implementation

[Ralf Lammel]

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


> -----Original Message-----
> From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-
> bounces at 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
the
> 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
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.