What happens with universal quantifications and typeclass constraints when composing functions?

Question

Lenses can be composed like any ordinary function. We have:

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

Now consider this example:

(.) :: Lens' Config Foo -> Lens' Foo String -> Lens' Config String

Expanding we get:

(.) :: (forall f. Functor f => (Foo -> f Foo) -> Config -> f Config)
    -> (forall f. Functor f => (String -> f String) -> Foo -> f Foo)
    -> (forall f. Functor f => (String -> f String) -> Config -> f Config)

And the type of function composition is:

(.) :: (b -> c) -> (a -> b) -> (a -> c)

Which lacks any universal quantification and typeclass constraints. Now my question is, how are these two features treated by the compiler/type-checker so that the function composition operator can be used for composing lenses?

My guess is that it is OK to have functions universally quantified and typeclass constraints, as long as these match for the two functions being composed.

Answer 1

Why don't we see what happens? Consider the following values:

(.) :: (b -> c) -> (a -> b) -> a -> c

foo :: Lens' A B

bar :: Lens' B C

The type of foo and bar will be expanded to:

foo :: Functor f => (B -> f B) -> A -> f A

bar :: Functor g => (C -> g C) -> B -> g B

Note that I left out the forall f. part because it's implicit. Also, I changed the name of f to g for bar to show that it's different from the f for foo.

Anyway, we'll first apply (.) to foo:

(.)     ::                 (b      ->    c)    -> (a ->    b)     -> a ->    c
                            |            |         |       |         |       |
                         --------     --------     |       |         |       |
                         |      |     |      |     |       |         |       |
foo     :: Functor f => (B -> f B) -> A -> f A     |    --------     |    --------
                                                   |    |      |     |    |      |
(.) foo :: Functor f =>                           (a -> B -> f B) -> a -> A -> f A

Thus, (.) foo has the type Functor f => (a -> B -> f B) -> a -> A -> f A. As you can see, the Functor constraint is simply copied as is.

Now, we apply (.) foo to bar:

(.) foo     :: Functor f =>    (a      -> B -> f B) ->     a      -> A -> f A
                       |        |         |    | |         |         |    | |
                       |     --------     |    | |         |         |    | |
                       |     |      |     |    | |         |         |    | |
bar         :: Functor g => (C -> g C) -> B -> g B      --------     |    | |
                                                        |      |     |    | |
(.) foo bar :: Functor g =>                            (C -> g C) -> A -> g A

Thus, (.) foo bar has the type Functor g => (C -> g C) -> A -> g A which means that it's a Lens' A C. As you can see Functor f is the same as Functor g which is why everything works out.