Function types as MonadReader

Question

I'm going through the lens tutorial and, in particular, trying to wrap my head around the types involved in view.

So, taking the definitions

data Atom = Atom { _element :: String, _point :: Point }
data Point = Point { _x :: Double, _y :: Double }
makeLenses ''Atom
makeLenses ''Point

let's inspect the type of the expression view (point . x):

*Main> :t view (point . x)
view (point . x) :: MonadReader Atom m => m Double

So, given an environment with an Atom we can produce a Double wrapped in a MonadReader. Nice, that's even more generic than a lens newbie could expect!

Now, let's try to apply this to some atom:

*Main> :t view (point . x) (Atom "C" (Point 1 2))
view (point . x) (Atom "C" (Point 1 2)) :: Double

How does this type-check given the above type for view (point . x)? I know there is an instance of MonadReader for the partially applied function type r ->, but how is ghc able to figure out that this particular instance shall be used in this case (if that's the one that's indeed used, of course)?

Answer 1

The key point is that you used the syntax for application.

When you write

view (point . x) (Atom "C" (Point 1 2))

you are essentially writing the application f a where f = view (point . x) and a = Atom "C" (Point 1 2). To type check f a GHC initially starts from

f :: t1 -> t2     -- in prefix for rm, this is written as (->) t1 t2
a :: t1

for some fresh type variables t1, t2. This is always done for all applications. (Well, almost. Some advanced types require a more careful algorithm, but I'll neglect that.)

However, GHC also knows

f :: MonadReader Atom m => m Double
a :: Atom

so it deduces t1 ~ Atom and m ~ (->) t1 ~ (->) Atom. Since this is indeed a MonadRead Atom instance, it proceeds with that.