Why Nothing == (pure Nothing) returns False in Haskell?

Question

Seems I understood something wrong, but I tried the following:

GHCi, version 8.6.5
Nothing == Nothing
=> True
Nothing == (pure Nothing)
=> False
pure Nothing
=> Nothing

Could you please explain what happens here?

Answer 1

The two pure Nothing in your code use a different pure.

If you examine the type of pure Nothing, you can see that the version of pure that is chosen depends on a type f.

GHCi> :t pure Nothing
pure Nothing :: Applicative f => f (Maybe a)

When you enter pure Nothing in interactive mode, f is inferred as IO and the result of the IO operation is printed. This is shortcut provided by GHCi that does not happen in regular Haskell code.

GHCi> pure Nothing
Nothing
GHCi> pure Nothing :: IO (Maybe ())
Nothing

However, when comparing pure Nothing with Nothing, f is inferred as Maybe. This creates two layers of Maybe, making the type Maybe (Maybe a)

GHCi> Nothing == pure Nothing
False
GHCi> Just Nothing == pure Nothing
True
GHCi> pure Nothing :: Maybe (Maybe ())
Just Nothing