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

[Simon Peyton-Jones]

I believe that you are asking about type functions.  Specifically, I think what you are asking is this:

  How can I normalise a type, by rewriting it exhaustively using
	the top-level type-function definitions

I think the function TcTyFuns.tcNormaliseFamInst (rather an odd name!) does this.  But it's not very helpful to you because it's in the main typechecker monad. 

-- |Normalise the given type as far as possible with toplevel equalities.
-- This results in a coercion witnessing the type equality, in addition to the
-- normalised type.
--
tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)

You probably wanted something like

   normaliseType :: FamInstEnv -> TcType -> (CoercionI, TcType)

where FamInstEnv contains the top-level type-function definitions.  

I believe that the only use of the monad is to carry the definitions around, so it should be easy to define the former in terms of the latter, although that'd need a bit of refactoring.

Manuel may know more

Simon

| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of Christiaan Baaij
| Sent: 02 July 2009 11:20
| To: glasgow-haskell-users at haskell.org
| Subject: GHC API: How to determine Type.Type equality when using type operators?
| 
| 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
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users