Some potential and difficulties in the use of lenses in MonadState

What follows is a series of examples/exercises upon Lenses (by Edward Kmett) in MonadState, based on the solution of Petr Pudlak to my previous question.

In addition to demonstrate some uses and the power of the lenses, these examples show how difficult it is to understand the type signature generated by GHCi. There is hope that in the future things will improve?

{-# LANGUAGE TemplateHaskell, RankNTypes #-}

import Control.Lens
import Control.Monad.State

---------- Example by Petr Pudlak   ----------
-- | An example of a universal function that modifies any lens.
-- It reads a string and appends it to the existing value.
modif :: Lens' a String -> StateT a IO ()
modif l = do
    s <- lift getLine
    l %= (++ s)

-----------------------------------------------

The following comment type signatures are those produced by GHCi. The other are adaptations from those of Peter. Personally, I am struggling to understand than those produced by GHCi, and I wonder: why GHCi does not produce those simplified?

-------------------------------------------

-- modif2
  -- :: (Profunctor p, MonadTrans t, MonadState s (t IO)) =>
     -- (Int -> p a b) -> Setting p s s a b -> t IO ()
modif2 :: (Int -> Int -> Int) -> Lens' a Int -> StateT a IO ()     
modif2 f l = do
    s<- lift getLine
    l %= f (read s :: Int)

---------------------------------------

-- modif3
  -- :: (Profunctor p, MonadTrans t, MonadState s (t IO)) =>
     -- (String -> p a b) -> Setting p s s a b -> t IO ()
modif3 :: (String -> Int -> Int) -> Lens' a Int -> StateT a IO ()     
modif3 f l = do
    s <- lift getLine
    l %= f s
-- :t modif3 (\n -> (+) (read n :: Int)) == Lens' a Int -> StateT a IO ()

---------------------------------------

-- modif4 
  -- :: (Profunctor p, MonadTrans t, MonadState s (t IO)) =>
     -- (t1 -> p a b) -> (String -> t1) -> Setting p s s a b -> t IO ()
modif4 :: (Bool -> Bool -> Bool) -> (String -> Bool) -> Lens' a Bool -> StateT a IO ()
modif4 f f2 l = do
    s <- lift getLine
    l %= f (f2 s)
-- :t modif4 (&&) (\s -> read s :: Bool) == Lens' a Bool -> StateT a IO ()

---------------------------------------
-- modif5
  -- :: (Profunctor p, MonadTrans t, MonadState s (t IO)) =>
     -- (t1 -> p a b) -> (String -> t1) -> Setting p s s a b -> t IO ()
modif5 :: (b -> b -> b) -> (String -> b) -> Lens' a b -> StateT a IO ()
modif5 f f2 l = do
    s<- lift getLine
    l %= f (f2 s)
-- :t modif5 (&&) (\s -> read s :: Bool) == Lens' a Bool -> StateT a IO ()

---------------------------------------

-- modif6
  -- :: (Profunctor p, MonadState s m) =>
     -- (t -> p a b) -> (t1 -> t) -> t1 -> Setting p s s a b -> m ()
modif6 :: (b -> b -> b) -> (c -> b) -> c -> Lens' a b -> StateT a IO ()
modif6 f f2 x l = do
    l %= f (f2 x)
-- :t modif6 (&&) (\s -> read s :: Bool) "True" ==  MonadState s m => Setting (->) s s Bool Bool -> m ()
-- :t modif6 (&&) (\s -> read s :: Bool) "True" 

---------------------------------------

-- modif7
  -- :: (Profunctor p, MonadState s IO) =>
     -- (t -> p a b) -> (String -> t) -> Setting p s s a b -> IO ()
modif7 :: (b -> b -> b) -> (String -> b) -> Lens' a b -> StateT a IO ()
modif7 f f2 l = do
    s <- lift getLine
    l %= f (f2 s)
-- :t modif7 (&&) (\s -> read s :: Bool) == 
-- :t modif7 (+) (\s -> read s :: Int) == 

---------------------------------------

p7a :: StateT Int IO ()
p7a = do
  get
  modif7 (+) (\s -> read s :: Int) id

test7a = execStateT p7a 10  -- if input 30 then result 40

---------------------------------------

p7b :: StateT Bool IO ()
p7b = do
  get
  modif7 (||) (\s -> read s :: Bool) id

test7b = execStateT p7b False  -- if input "True" then result "True"

---------------------------------------

data Test = Test { _first :: Int
                 , _second :: Bool
                 }
    deriving Show

$(makeLenses ''Test)

dataTest :: Test
dataTest = Test  { _first = 1, _second = False }

monadTest :: StateT Test IO String
monadTest = do
  get
  lift . putStrLn $ "1) modify \"first\" (Int requested)"
  lift . putStrLn $ "2) modify \"second\" (Bool requested)"
  answ <- lift getLine
  case answ of
    "1" -> do lift . putStr $ "> Write an Int: "
              modif7 (+) (\s -> read s :: Int) first
    "2" -> do lift . putStr $ "> Write a Bool: "
              modif7 (||) (\s -> read s :: Bool) second
    _   -> error "Wrong choice!"
  return answ

testMonadTest :: IO Test  
testMonadTest = execStateT monadTest dataTest

Solution

As a family in the ML tradition, Haskell is specifically designed so that every toplevel binding has a most general type, and the Haskell implementation can and has to infer this most general type. This ensures that you can reuse the binding in as much places as possible. In a way, this means that type inference is never wrong, because whatever type you have in mind, type inference will figure out the same type or a more general type.

why GHCi does not produce those simplified?

It figures out the more general types instead. For example, you mention that GHC figures out the following type for some code:

modif2 :: (Profunctor p, MonadTrans t, MonadState s (t IO)) =>
  (Int -> p a b) -> Setting p s s a b -> t IO ()

This is a very general type, because every time I use modif2, I can choose different profunctors p, monad transformers t and states s. So modif2 is very reusable. You prefer this type signature:

modif2 :: (Int -> Int -> Int) -> Lens' a Int -> StateT a IO ()

I agree that this is more readable, but also less generic: Here you decided that p has to be -> and t has to be StateT, and as a user of modif2, I couldn't change that.

There is hope that in the future things will improve?

I'm sure that Haskell will continue to mandate most general types as the result of type inference. I could imagine that in addition to the most general type, ghci or a third-party tool could show you example instantiations. In this case, it would be nice to declare somehow that -> is a typical profunctor. I'm not aware of any work in this direction, though, so there is not much hope, no.