Haskell: Почему эта проверка типов?

Это минимальный пример, взятый из 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

В GHCi я получаю следующее:

>:t Zero
Zero :: Zero -> Zero

Это имеет смысл: я запрашиваю тип конструктора, который принимает ноль и возвращает ноль.

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

Имеет смысл написать что-то вроде

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

, потому что тип Just Zero соответствует типу переменных 'proxy s'.

Наконец, запутанная часть:

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

Я не понимаю, как тип конструктора Zero :: Zero -> Zero, по-видимому, соответствует типу переменных 'proxy s', но, по-видимому, это так, потому что тип (reflectionNum Zero ) просто "а".

Буду признателен за помощь в понимании этого примера, и ссылки на соответствующие концепции будут очень благодарны.

Спасибо