[Haskell-cafe] flexible contexts problem

[Luke Palmer]

2009/9/12 Sean McLaughlin <seanmcl at gmail.com>:
> I'm having trouble understanding the following behavior.  The following
> program compiles:
> {-# OPTIONS_GHC -XMultiParamTypeClasses -XFlexibleContexts  #-}
> import Control.Monad.State
> class Has α s where
>   has :: s -> (α, s)
> project :: (MonadState s m, Has α s) => m α
> project = do (α, s) <- gets has
>              put s
>              return α
> f :: (MonadState s m, Has Int s) => m Int
> f = do x <- project
>           return x
> However, if you replace the function f with
> f :: (MonadState s m, Has Int s) => m Int
> f = do x <- project
>           y <- project
>           return x
> then it fails with the error
>     Could not deduce (Has α s)
>       from the context (MonadState s m, Has Int s)
>       arising from a use of `project'
>                    at /Users/sean/uploads/Weird.hs:16:12-18
>     Possible fix:
>       add (Has α s) to the context of the type signature for `f'
>     In a stmt of a 'do' expression: y <- project
>     In the expression:
>         do x <- project
>            y <- project
>            return x
>     In the definition of `f':
>         f = do x <- project
>                y <- project
>                return x
>
> I don't see how the second call to project could possibly make a difference.
>  Could
> someone please tell me what I'm doing wrong?

Look at the type signature of project:

project :: (MonadState s m, Has α s) => m α

The only way it can know what Has instance to use is by knowing α.
And the only way to know α is to know the return type.  You never use
y in your new f, which is the only thing that could have told the
compiler what type α was for the second project call (it's not
necessarily the same as in the first).

Possible solutions:

* Use fundeps to constrain Has so there is only one choice of α for
each choice of s.  Do this only if this constraint correctly models
the meaning of Has (which is... what?)
* Give the compiler some way of knowing what type y is, eg.

f :: (MonadState s m, Has Int s) => m Int
f = do x <- project
          y :: Int <- project
          return x

Returning it or taking something of its type as a parameter
(constraining with asTypeOf) is just as good, then a constraint can be
added to the context.

Luke