[Haskell-beginners] Inferred type is less polymorphic than e

[Daniel Fischer]

Am Donnerstag 09 April 2009 13:16:01 schrieb Marco Túlio Gontijo e Silva:
> Em Qui, 2009-04-09 às 01:55 +0200, Daniel Fischer escreveu:
> Ok, I got it, so I tried changing class A in my example to:
> > class A a b where
> >   f :: forall m . Monad m => a -> m b
>
> so that the type of f would be as polymorphic as the type a -> M b.  But
> I got the same problem.

Because that's exactly the same type f had before.
To get a polymorphic result from f, you have to declare

{-# LANGUAGE Rank2Types #-}
-- or make it RankNTypes and be ready for more quantification

class A a b where
    f :: a -> (forall m. Monad m => m b)

>
> Your solution is good, but I can't do it in my real application where I
> find out this problem, because the type synonym M is defined after the
>
> class A, and it contains more than on type constraint:
> > type Interpret value
> >   = ( MonadReader Input monad
> >     , MonadState Machine monad
> >     , MonadWriter Stream monad)
> >   => monad value
>
> My use is that I have some classes defined in modules included by the
>
> one that defines type Interpret, like this:
> > class Value pointer value where
> >   getValue
> >
> >     :: (MonadReader Program monad, MonadState Machine monad)
> >
> >     => pointer -> monad value
>
> And even if they were defined in the same file, it would not be good to
> define them as Interpret, because it would restrict its type.
>
> Another thing:  I understand your explanation, but I don't get why this
> makes the other h definition valid.  Could you clarify me on that?

This definition?
> > > h :: IO ()
> > > h = (f "abc" :: M Char) >>= f >>= (print :: Int -> IO ())

Let's start on the left:

(f "abc" :: M Char) === (f "abc" :: forall m. Monad m => m Char)

Now we have

class A a b where
    f :: Monad m => a -> m b

instance A String Char where ...

We apply f to the String "abc", so an "instance A String b" has to be selected.

f will here be invoked at the type

(A String b, Monad m) => String -> m b
    === forall m b. (A String b, Monad m) => String -> m b

Therefore f "abc" has the type resulting from removing the argument type, namely

f "abc" :: forall m b. (A String b, Monad m) => m b

Note that although f does not have the type 
(A String b) => String -> (forall m. Monad m => m b)

the expression (f string) has the type forall b m. (A String b, Monad m) => m b.

It's the same with return, the type of return is
forall a m. Monad m => a -> m a
and not
forall a. a -> (forall m. Monad m => m a),
but the type of return value is (forall m. Monad m => m a), where a is the type of value.

Now f "abc" has a type annotation, f "abc" :: M Char, or 
f "abc" :: forall m. Monad m => m Char

That type must now be unified with the inferred type, 
forall mon b. (A String b, Monad mon) => mon b.

It is obvious that we must have b === Char, so the compiler looks for an 
instance A String Char where... (or a more general instance)

Since there is one, that is fine and the satisfied constraint (A String Char) can be 
removed. The two type(-constructor) variables m and mon are now unified and there contexts 
united. Since both contexts are the same, the result is

f "abc" :: forall m. Monad m => m Char,
exactly the specified signature (can't be anything else, if the inferred type were less 
polymorphic than the specified, it wouldn't compile, if it's more general, it's restricted 
to the specified type).

On to the next step, look at

(f "abc" :: M Char) >>= f

(>>=) :: Monad m => m u -> (u -> m v) -> m v
(f "abc") :: Monad mo => mo Char
f :: (A a b, Monad mon) => a -> mon b

Now we have to unify mo Char with m u (the contexts Monad m and Monad mo will be taken 
care of thereafter).
That's easy, u == Char and m === mo, contexts are the same, so

((f "abc" :: M Char) >>=) :: Monad m => (Char -> m v) -> m v

Next we must unify
Char -> m v
with
a -> mon b.
That's again easy, a === Char, mon === m, b === v.
Now take the contexts (Monad m) and (A a b, Monad mon) into account.
Substituting int f's context, we get the context (A Char v, Monad m) for f's type here,
so this f is called at the type (A Char v, Monad m) => Char -> m v, and we get the type

(f "abc" :: M Char) >>= f :: (A Char v, Monad m) => m v

Finally,

left :: (A Char v, Monad m) => m v
(>>=) :: Monad mo => mo a -> (a -> mo b) -> mo b
print :: Int -> IO ()         -- specified

We get the type

(left >>=) :: (A Char v, Monad m) => (v -> m b) -> m b

and then must unify (v -> m b) with (Int -> IO ()), giving v === Int, m === IO, b === ().
Substituting into the contexts gives

(left >>= print) :: (A Char Int, Monad IO) => IO ()

The context doesn't contain any type variables and the conditions are fulfilled, so the 
context is removed, leaving

(f "abc" :: M Char) >>= f >>= (print :: Int -> IO ()) :: IO ().

>
> Thanks.