Haskell: Why does this type-check?

Question

This is a minimal example taken from the Reflection-0.5.

{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-}
{-# OPTIONS_GHC -fno-cse -fno-full-laziness -fno-float-in #-}

import Control.Applicative
import Data.Proxy

newtype Zero = Zero Zero deriving (Show)

class ReifiesNum s where
  reflectNum :: Num a => proxy s -> a

instance ReifiesNum Zero where
  reflectNum = pure 0

In GHCi, I get the following:

>:t Zero
Zero :: Zero -> Zero

This makes sense: I'm asking for the type of the constructor which takes a Zero and returns a Zero.

>:t reflectNum
reflectNum :: (ReifiesNum s, Num a) => proxy s -> a

It makes sense that I could write something like

>let x = Just (undefined::Zero)
>reflectNum x

because the type Just Zero matches the type variables 'proxy s'.

Finally, the confusing part:

>:t (reflectNum Zero)
(reflectNum Zero) :: Num a => a

I do not understand how the type of the constructor Zero :: Zero -> Zero apparently matches the type variables 'proxy s', but apparently it does because the type of (reflectNum Zero) is just 'a'.

I'd appreciate help understanding this example, and links to relevant concepts would be greatly appreciated.

Thanks

Answer 1

It's just the infix syntax of the function arrow throwing you off. First, here's an example with an easy-to-understand case: Maybe Int. To make it match proxy s, we just set:

proxy = Maybe
s = Int

Now let's pretend a -> b is instead written Fun a b, and so Zero has type Fun Zero Zero (i.e. (Fun Zero) Zero). To make it match proxy s, we set:

proxy = Fun Zero
s = Zero

In reality, proxy is (->) Zero, and so proxy s is ((->) Zero) Zero ≡ (->) Zero Zero ≡ Zero -> Zero.