"Illegal polymorphic or qualified type" in Control.Lens

Question

I'm working with Control.Lens. The actual function I'm writing is rather complex, but for the purpose of this question, I've boiled it down to a minimal failing example:

import Control.Lens    

exampleFunc :: Lens s t a b -> String
exampleFunc _ = "Example"

This fails to compile, yielding the following error message:

Illegal polymorphic or qualified type: Lens s t a b
Perhaps you intended to use -XRankNTypes or -XRank2Types
In the type signature for `exampleFunc':
  exampleFunc :: Lens s t a b -> String

Why is this illegal? It seems awfully similar to the following, which does compile:

import Data.Maybe

exampleFunc' :: Maybe (s, t, a, b) -> String
exampleFunc' _ = "Example"

So I'm assuming the difference lies in the definition of Lens. But what about the Lens type makes exampleFunc's type illegal? I have a sneaking suspicion it has to do with the Functor qualification in the definition of Lens, but I could be wrong. For reference, the definition of Lens is:

type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t

So, do I have to somehow satisfy the Functor qualification in my definition of exampleFunc? If so, how? I'm not seeing where in my type signature I have the opportunity to declare this constraint. Or maybe I'm on the wrong track, and my problem has nothing to do with the Functor constraint.

I've read all the Stack Overflow questions I could find regarding the "illegal polymorphic etc" error message. Perhaps this is my lack of familiarity with Haskell showing, but I can't see any of those questions being applicable to my current situation.

Nor have I been able to find any documentation on what the error message means in general.

Surveying

RankNTypes is one of the extensions you can safely switch on when the compiler suggests so. This is ok for many other extensions too, though perhaps not for OverlappingInstances & IncoherentInstances. – Integrant

Answer 1

Lens uses rank 2 types and you have it to the left of an arrow so to use any of lenses types like this you have to make it legal to even utter something like

(forall a. foo) -> bar

Which you can too with

{-# LANGUAGE RankNTypes #-} -- Rank2Types is a synonym for RankNTypes

at the top of your file. Without it, it's illegal to even use a lens type synonym since they use a part of the language you must enable.

Rhapsodic

That's not what negative position means. For example, in (a -> r) -> r, a appears in positive position. – Polito

@BenMillwood It's a simplified version, and yes the negative and positive positions behave like multiplication, in that the negative position of a negative position is a positive position. But for this instance I felt a simplified description was sufficient. – Rhapsodic

Answer 2

exampleFunc fails to compile because the Lens type synonym is polymorphic and occurs in the signature in what is called "negative position", that is, to the left of the ->.

You can use Lens in a type signature even without having RankNTypes on. This typechecks:

import Control.Lens

lensy :: Lens' (a,b) a 
lensy = _1

But this fails to typecheck:

oops :: Lens' (a,b) a -> Int
oops = const 5 

Why? For the same reason this also fails to typecheck without RankNTypes:

{-# LANGUAGE ExplicitForAll #-}

fails :: (forall a. a -> Int) -> Int
fails = undefined

Here the forall is in negative position, and ranges only over the a -> Int. It is the implementation of fails, and not the caller of fails, the one who chooses the type of a. The caller must supply an argument function that works for all a. This feature requires the RankNTypes extension.

When the forall ranges over the whole signature (as when Lens is defined in isolation) there's no need for RankNTypes. This typechecks:

{-# LANGUAGE ExplicitForAll #-}

typechecks :: forall a. (a -> Int) -> Int
typechecks = undefined

But this function is different from the previous one, because here it is the caller who chooses the type of a. He can pass an argument function which works only for a particular a.

exampleFunc' worked because, when no forall is specified, there are implicit foralls for each variable, ranging over the whole signature.

This explanation from the Haskell mailing list may be useful.

Atomizer