Type error with rank-n types and lenses

Question

I have a simple polymorphic datatype Foo

{-# LANGUAGE TemplateHaskell #-}
import Control.Lens

data Foo c = 
    Foo {
        _bar :: c,
        _baz :: c,
        _quux :: c
    }   

makeLenses ''Foo

The generated lenses are, of course, polymorphic in c. The type from GHCi is:

*Main> :t bar
bar :: Functor f => (c0 -> f c0) -> Foo c0 -> f (Foo c0)

I made a datatype Blah to wrap around the lens. This works fine in simple cases (with the RankNTypes extension, of course):

data Blah = Blah (forall c . Lens' (Foo c) c)

orange :: Blah
orange = Blah bar

But anything slightly more complicated doesn't work, for example

cheese :: [Blah]
cheese = map Blah [bar]

This last piece of code gives an error from GHC:

    Couldn't match type ‘(c0 -> f0 c0) -> Foo c0 -> f0 (Foo c0)’
                  with ‘forall c (f :: * -> *).
                        Functor f =>
                        (c -> f c) -> Foo c -> f (Foo c)’
    Expected type: ((c0 -> f0 c0) -> Foo c0 -> f0 (Foo c0)) -> Blah
      Actual type: (forall c. Lens' (Foo c) c) -> Blah
    In the first argument of ‘map’, namely ‘Blah’
    In the expression: map Blah [bar]

It seems like the forall c f . has disappeared from ‘(c0 -> f0 c0) -> Foo c0 -> f0 (Foo c0)’ but I don't understand why.

Why does this not compile, and what can I do to get something like this to work?

Well, I'm not sure I could give a correct enough explanation for why to warrant a full answer, but it seems to be a scoping problem with Blah. If you move the forall c. outside of the constructor as data Blah = forall c. Blah (Lens' (Foo c) c) then map Blah will typecheck, but map Blah [bar] won't. If you expand the Lens' type and manually do data Blah = forall c f. Functor f => Blah ((c -> f c) -> Foo c -> f (Foo c)) then you have :t map Blah as Functor f => [(c -> f c) -> Foo c -> f (Foo c)] -> [Blah] and :t [bar, baz] as [(c -> f c) -> Foo c -> f (Foo c)]... — bheklilr
... but it can't unify the Functor constraint in map Blah [bar, baz]. I believe this is because the Blah constructor is hiding too much from the type checker (essentially), so it can't figure out how to incorporate the Functor constraint. If the lens type were unconstrained then it might actually work. — bheklilr
The only way I can get anything to type-check is to add type parameters to Blah as data Blah f c where Blah :: Functor f => ((c -> f c) -> Foo c -> f (Foo c)) -> Blah f c, then you can do map Blah [bar, baz] and have the type Functor f => [Blah f c], but this doesn't mean that there isn't a way to hide those type variables. The important one here is f I think, because the Functor constraint. The compiler has to pick an instance for Functor, but has no way of picking just one, so it fails the type check. — bheklilr
You want [bar] to have type [forall c . Lens' (Foo c) c], but it actually has the type Functor f => [(c0 -> f c0) -> Foo c0 -> f (Foo c0)]. You can force [bar] to have the former type, by simply specifying that type signature - but you need to enable ImpredicativeTypes. The same goes for map Blah - it also has an impredictive type, so you will also need to specify it manually. For example; bar' :: [forall c . Lens' (Foo c) c]; bar' = [bar] ; mapBlah :: [forall c . Lens' (Foo c) c] -> [Blah]; mapBlah = map Blah typechecks, and so will mapBlah bar'. — user2407038
As an aside, I wouldn't recommend using impredictive types - you will have to write a type signature for every impredictive type and it doesn't give you much power. — user2407038

user2407038 user2407038 · Accepted Answer · 2015-03-02T21:48:22

You want [bar] to have type [forall c . Lens' (Foo c) c], but it actually has the type forall f c . Functor f => [(c -> f c) -> Foo c -> f (Foo c)]. The compiler infers the latter type signature because it is predicative. You can find resources on the technical details of (im)predictive types. In short, type inference is undecidable in the presence of impredictive types - so type signatures become mandatory - so by default they are not permitted. An impredictive type is one where a forall occurs inside a type constructor (like []).

You can force [bar] to have the former type, by simply specifying that type signature and enabling ImpredicativeTypes. The same goes for map Blah - it also has an impredictive type, so you will also need to specify it manually.

bar' :: [forall c . Lens' (Foo c) c]
bar' = [bar] 

mapBlah :: [forall c . Lens' (Foo c) c] -> [Blah]
mapBlah = map Blah

Then the following typechecks:

> mapBlah bar'

or even

> (map Blah :: [forall c . Lens' (Foo c) c] -> [Blah]) 
    ([bar] :: [forall c . Lens' (Foo c) c])

In fact, the deal with the problem of impredictive types, lens includes the module Control.Lens.Reified which declares newtypes for all the common lens types so that you can have lenses in containers. This actually won't help you in this particular use case, because you also want the c in Lens' (Foo c) c to be bound inside the list constructor, but it is useful in general.

Type error with rank-n types and lenses

1 Answers