Why does this lens function require a type signature?

Question

I'm writing a function which uses the lenses library, but curiously, the code doesn't compile when I remove the type annotation.

{-# LANGUAGE TemplateHaskell, Rank2Types #-}

import Control.Lens
import Control.Monad.State

import Data.List (elemIndex)

data MyRecord = MyRecord { _someField :: [Int], _anotherField :: [String] }
makeLenses ''MyRecord

updateRecord :: Eq a => a -> Lens' b [a] -> (Int -> c) -> State b c
updateRecord elem lens f = do field <- view lens <$> get
                              case elemIndex elem field of
                                Just index -> return $ f index
                                Nothing -> do modify (over lens (++[elem]))
                                              return . f $ length field

When I comment out the type signature for updateRecord, I get this error:

    • Couldn't match type ‘Const [a] s’ with ‘Identity s’
      Expected type: ASetter s s [a] [a]
        Actual type: Getting [a] s [a]

Why is the type signature required in this case?

Answer 1

The issue is that lens is used in two contexts, view lens, where it is required to have type:

Getting [a] s [a]
= ([a] -> Const [a] [a]) -> (s -> Const [a] s)

and over lens ... where it is required to have type:

ASetter s s [a] [a]
= ([a] -> Identity [a]) -> (a -> Identity s)

Unfortunately, these types don't unify. (In particular, the rightmost parts of these types, Const [a] s and Identity s, don't unify, which is what the error message is saying.) When GHC tries to infer the type of lens in typechecking updateRecord without an explicit type signature, it infers the first type above for lens based on its use in view but then is unable to unify this with the second type that arises in over.

However, even though the types don't unify, there is a higher rank polymorphic type that can be specialized to each one separately, namely:

Lens' s a
= Lens s s a a = forall f. Functor f => (a -> f s) -> (a -> f s)

As long as GHC can separately infer this type, say by means of an explicit type signature, it's able to unify this more general type with each of the uses.

This is just one of those things, a fundamental limitation of higher rank types. You can see the same phenomenon at work with a much smaller example. This function foo doesn't typecheck:

foo f = (f 10, f "hello")

but add a type signature and it's fine:

foo :: (forall a. a -> a) -> (Int, String)
foo f = (f 10, f "hello")