Runtime type representation of terms with support for rank-1 polymorphic types with type variables of kind *.

The essence of this module is that we use the standard Typeable representation of Data.Typeable but we introduce a special (empty) data type TypVar which represents type variables. TypVar is indexed by an arbitrary other data type, giving you an unbounded number of type variables; for convenience, we define ANY, ANY1, .., ANY9.

Examples of isInstanceOf

 -- We CANNOT use a term of type 'Int -> Bool' as 'Int -> Int'
 > typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: Int -> Bool)
 Left "Cannot unify Int and Bool"
 
 -- We CAN use a term of type 'forall a. a -> Int' as 'Int -> Int'
 > typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: ANY -> Int)
 Right ()
 
 -- We CAN use a term of type 'forall a b. a -> b' as 'forall a. a -> a'
 > typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY1)
 Right ()
 
 -- We CANNOT use a term of type 'forall a. a -> a' as 'forall a b. a -> b'
 > typeOf (undefined :: ANY -> ANY1) `isInstanceOf` typeOf (undefined :: ANY -> ANY)
 Left "Cannot unify Succ and Zero"
 
 -- We CAN use a term of type 'forall a. a' as 'forall a. a -> a'
 > typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY)
 Right ()
 
 -- We CANNOT use a term of type 'forall a. a -> a' as 'forall a. a'
 > typeOf (undefined :: ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY)
 Left "Cannot unify Skolem and ->"

(Admittedly, the quality of the type errors could be improved.)

Examples of funResultTy

 -- Apply fn of type (forall a. a -> a) to arg of type Bool gives Bool 
 > funResultTy (typeOf (undefined :: ANY -> ANY)) (typeOf (undefined :: Bool))
 Right Bool
 
 -- Apply fn of type (forall a b. a -> b -> a) to arg of type Bool gives forall a. a -> Bool
 > funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: Bool))
 Right (ANY -> Bool) -- forall a. a -> Bool
 
 -- Apply fn of type (forall a. (Bool -> a) -> a) to argument of type (forall a. a -> a) gives Bool
 > funResultTy (typeOf (undefined :: (Bool -> ANY) -> ANY)) (typeOf (undefined :: ANY -> ANY))
 Right Bool

 -- Apply fn of type (forall a b. a -> b -> a) to arg of type (forall a. a -> a) gives (forall a b. a -> b -> b)
 > funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: ANY1 -> ANY1))
 Right (ANY -> ANY1 -> ANY1)

 -- Cannot apply function of type (forall a. (a -> a) -> a -> a) to arg of type (Int -> Bool)
 > funResultTy (typeOf (undefined :: (ANY -> ANY) -> (ANY -> ANY))) (typeOf (undefined :: Int -> Bool))
 Left "Cannot unify Int and Bool"