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
