I think there is a type mismatch in default definition in instance Applicative Maybe in Haskell

Question

I am currently studying Haskell with Prof. Hutton's "Programming in Haskell", and I found something strange regarding the definition of Maybe as an instance of the class Applicative.

In GHC.Base, the instance Applicative Maybe is defined as follows:

instance Applicative Maybe where
  pure = Just

  Just f  <*> m       = fmap f m
  Nothing <*> _m      = Nothing

It is the line which defines the value of Nothing <\*> _ as Nothing that bothers me. Nothing is of type Maybe a, where the operator <*> actually requires f (a -> b) (in this case, Maybe (a -> b)) as its first argument's type. Therefore, this is a type mismatch, which Haskell should complain about. However, this is accepted as a default definition, and therefore Haskell does not complain about it where I think it should.

What am I missing?

Answer 1

The a in Maybe a is a type variable, and can be any type at all! So Nothing can have the type Maybe Int, or Maybe [x], or Maybe (p -> q), for example. Don't get confused by the fact that the variable name a is used in two places. The a in the type of Nothing is a completely different variable from the a in the type of <*>, and just happens to have the same name!

(That's exactly the same as if you wrote f x = x + 5 and then elsewhere, g x = "Hello, " ++ x. The use of x in both places doesn't matter, because they are in different scopes. Same with the a in this types. Different scopes, so they are different variables.)

Answer 2

Let's make things clearer by relabeling a type variable:

Nothing :: Maybe x

The type Maybe x unifies with Maybe (a -> b), with x ~ (a -> b). That is, Nothing is a value that can used as Maybe a for any a, including a function type. Thus it is a legal left-hand argument for <*> here.