Search code examples
haskellhaskell-lenshigher-rank-types

Type error with rank-n types and lenses

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?

Solution

  • 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.