GHC API: How to determine Type.Type equality when using type operators?

[Christiaan Baaij]

Hi all,

I've been doing some work with the GHC API where I translate Haskell  
to VHDL,
and as such I have to translate Haskell Types to VHDL Types. I store the
translations in a Map as such:


-- A orderable equivalent of CoreSyn's Type for use as a map key
newtype OrdType = OrdType { getType :: Type.Type }
instance Eq OrdType where
   (OrdType a) == (OrdType b) = Type.tcEqType a b
instance Ord OrdType where
   compare (OrdType a) (OrdType b) = Type.tcCmpType a b

-- A map of a Core type to the corresponding type name
type TypeMap = Map.Map OrdType (AST.VHDLId, Either AST.TypeDef  
AST.SubtypeIn)


This solution work fine for 'simple' types and ensures that the VHDL  
Type
definitions are all unique. However, a problem rises when type  
operators come
in to play, as Type.tcEqType does not know the 'rules' of these type  
operators
and can thus not infer that two types are equal. Let me give some  
context for
my problem:

We use statically fixed-size vectors instead of lists, as we always  
want to
know the static length of an array. We use a vector implementation  
similar to
Data.Param.FSVec defined in the parameterized-data package [1], except  
that we
use type-level integers from the tfp library [2] to define the static  
vector
lenght. The tfp library support things like type-level multiplication,
something that we use in our vector library.

Now, say we have two bit vectors of length 12 defined as such:

a :: Vector D12 Bit
b :: Vector (D3 :*: D4) Bit

The GHC type checker can infer that 'a' and 'b' are of equal type, as  
it knows
the definitions for the ':*:' multiplication type-operator that is  
defined in
the tfp library. Of course, the only answer Type.tcEqType can give us  
if we
ask if the types of 'a' and 'b' are equals is False, as it does not  
know the
context provided by the type-operator.

So my question is:
Is there a functions in the GHC API that I can use to check the  
equality of
two types given the context provided by certain type operators? I have  
looked
at the Haddock documentation, the GHC Wiki, and the GHC code itself,  
but have
been unable to find such a function.

Regards,
Christiaan


[1] http://hackage.haskell.org/package/parameterized-data
[2] http://hackage.haskell.org/package/tfp