%
% Comparison of Core expressions and types modulo alpha equivalence 
%

\begin{onlystandalone}
\documentstyle[pagesize, 12pt, literate]{article}
\begin{document}
\title{Comparison of Core expressions and types modulo alpha equivalence}
\author{Olaf Chitil}
\maketitle
\end{onlystandalone}

\section{Exports and Imports}

\begin{code}
#include "HsVersions.h"


module CoreCmpModAlpha (
         GenCoreBinding(..), GenCoreExpr(..),
         GenCoreArg(..), GenCoreBinder(..), GenCoreCaseAlts(..),
         GenCoreCaseDefault(..),
	 Coercion,
	 Alpha, emptyAlpha,
         cmpModAlphaBinding, cmpModAlphaExpr, cmpModAlphaArg,
         cmpModAlphaBinder, cmpModAlphaCaseAlts, cmpModAlphaCaseDefault
       ) where

import Pretty(PrettyRep)
import PprStyle(PprStyle)

import Bag(Bag)
import Util(Ord3(..))  -- class Ord3 
       -- class needed for Id's, TyVar's, Literal's, Unique's,..
import Outputable(Outputable(..)) 
       -- class needed for Id's, BinderInfo's, ...
import Name(NamedThing(..), Name, OrigName, RdrName) 
       -- class needed for Id's and TyVar's,.. and types
import UniqFM(Uniquable(..), UniqFM) 
       -- class needed for Id's, TyVar's, ...
import Literal(Literal)
import Unique(Unique)
import CostCentre(CostCentre)
import BinderInfo(BinderInfo)
import TyVar(SYN_IE(TyVar), GenTyVar)
import Id(SYN_IE(Id), GenId)
import TyCon(TyCon)
import Class(GenClass)

-- what is actually needed:
import PrimOp(PrimOp, tagOf_PrimOp) -- for comparison
import CoreSyn
--import FiniteMap (FiniteMap, emtpyFM, addToFM, lookupFM)
import FiniteMap 
import TyCon(TyCon, mkFunTyCon)
import Type(SYN_IE(Type), GenType(..)) 
       -- need internals for comparision
import Usage(SYN_IE(Usage), GenUsage(..)) -- need internals for comparison
\end{code}


\subsection{Assisting functions for @_CMP_TAG@}

\begin{code}
thenCmp :: _CMP_TAG -> _CMP_TAG -> _CMP_TAG
thenCmp _EQ   other = other
thenCmp first _     = first

lexicalCmp :: (a -> a -> _CMP_TAG) -> [a] -> [a] -> _CMP_TAG
lexicalCmp cmp []     []     = _EQ
lexicalCmp cmp []     (x:xs) = _LT
lexicalCmp cmp (x:xs) []     = _GT
lexicalCmp cmp (x:xs) (y:ys) = cmp x y `thenCmp` lexicalCmp cmp xs ys
\end{code}



\subsection{Equality and ordering for coercions}

Inside of coercions there are just id's of constructors. 
Hence equality modula alpha conversion is not necessary,
just simple instances of Eq and Ord.

\begin{code}
compareCoercion :: Coercion -> Coercion -> _CMP_TAG

compareCoercion (CoerceIn id1)  (CoerceIn id2)  = _tagCmp id1 id2
compareCoercion (CoerceIn id1)  _               = _LT
compareCoercion (CoerceOut id1) (CoerceOut id2) = _tagCmp id1 id2
compareCoercion _               _               = _GT


instance Eq Coercion where
  x == y = case (compareCoercion x y) of { _EQ -> True; _ -> False }	

instance Ord Coercion where
  x <= y = case (compareCoercion x y) of { _GT -> False; _ -> True }
  _tagCmp = compareCoercion
			
\end{code}


\subsection{The data type @Alpha@ for keeping track of equal variables}


Danger: implementation of instances depends on the two compared arguments 
never being swapped in recursive calls.


\begin{code}
data (Ord valVar, Ord tyVar, Ord uVar) => Alpha valVar tyVar uVar 
     = Alpha (FiniteMap valVar valVar) (FiniteMap tyVar tyVar) 
         (FiniteMap uVar uVar)

emptyAlpha :: Alpha valVar tyVar uVar
emptyAlpha = Alpha emptyFM emptyFM emptyFM
\end{code}



\begin{code}
addToAlphaValVar :: Ord valVar 
                 => Alpha valVar tyVar uVar -> valVar -> valVar 
                 -> Alpha valVar tyVar uVar

addToAlphaValVar (Alpha valVars tyVars uVars) valVar1 valVar2
  = Alpha (addToFM valVars valVar1 valVar2) tyVars uVars


addToAlphaTyVar :: Ord tyVar 
                => Alpha valVar tyVar uVar -> tyVar -> tyVar 
                -> Alpha valVar tyVar uVar

addToAlphaTyVar (Alpha valVars tyVars uVars) tyVar1 tyVar2
  = Alpha valVars (addToFM tyVars tyVar1 tyVar2) uVars

							  
addToAlphaUVar :: Ord uVar 
                 => Alpha valVar tyVar uVar -> uVar -> uVar 
                 -> Alpha valVar tyVar uVar

addToAlphaUVar (Alpha valVars tyVars uVars) uVar1 uVar2
  = Alpha valVars tyVars (addToFM uVars uVar1 uVar2)
\end{code}



\subsection{Binder and Binding}


\begin{code}
cmpModAlphaBinder :: (Ord valVar, Ord tyVar, Ord uVar)
                  => Alpha valVar tyVar uVar
                  -> GenCoreBinder valVar tyVar uVar 
                  -> GenCoreBinder valVar tyVar uVar 
                  -> (_CMP_TAG, Alpha valVar tyVar uVar)

cmpModAlphaBinder alpha  (ValBinder valBdr1) (ValBinder valBdr2)
  = (_EQ, addToAlphaValVar alpha valBdr1 valBdr2)
cmpModAlphaBinder alpha  (TyBinder tyVar1) (TyBinder tyVar2)
  = (_EQ, addToAlphaTyVar alpha tyVar1 tyVar2)
cmpModAlphaBinder alpha  (UsageBinder uVar1) (UsageBinder uVar2)
  = (_EQ, addToAlphaUVar alpha uVar1 uVar2)
cmpModAlphaBinder alpha _ _ = (_LT, alpha)



cmpModAlphaBinding :: (Ord valVar, Ord tyVar, Ord uVar)
                   => Alpha valVar tyVar uVar
                   -> GenCoreBinding valVar valVar tyVar uVar
                   -> GenCoreBinding valVar valVar tyVar uVar
		   -> (_CMP_TAG, Alpha valVar tyVar uVar)

cmpModAlphaBinding alpha binding1 binding2
  = ( lexicalCmp (cmpModAlphaExpr alpha') 
        (rhssOfBind binding1) (rhssOfBind binding2)
    , alpha' 
    )
    where
    alpha' = foldl add alpha (zip (bindersOf binding1) (bindersOf binding2))
    add :: (Ord valVar, Ord tyVar, Ord uVar) 
        => Alpha valVar tyVar uVar 
        -> (valVar, valVar) 
        -> Alpha valVar tyVar uVar
    add alpha (valVar1, valVar2) = addToAlphaValVar alpha valVar1 valVar2
\end{code}



\subsection{Problem with classes}

Would like to have something like that:

\begin{pseudocode}
class CmpModAlpha term uVar tyVar valVar where
  cmpModAlpha :: Alpha valVar tyVar uVar  
	      -> term 
	      -> term
	      -> _CMP_TAG 

instance Ord valVar => CmpModAlpha (valVar)  valVar tyVar uVar where ...
instance Ord tyVar  => CmpModAlpha (tyVar)   valVar tyVar uVar where ...
instance Ord uVar   => CmpModAlpha (uVar)    valVar tyVar uVar where ...

instance CmpModAlpha term uVar tyVar valVar 
      => CmpModAlpha [term] uVar tyVar valVar where ...
  
instance ( CmpModAlpha (valVar) valVar tyVar uVar
         , CmpModAlpha (GenCoreArg valVar tyVar uVar) valVar tyVar uVar
         , CmpModAlpha (GenCoreBinder valVar tyVar uVar) valVar tyVar uVar
         , CmpModAlpha (GenCoreCaseAlts valVar valVar tyVar uVar) valVar tyVar uVar
         , CmpModAlpha (GenType tyVar uVar) valVar tyVar uVar)
      => CmpModAlpha (GenCoreExpr valVar valVar tyVar uVar) valVar tyVar uVar
   where
   ...

instance ( CmpModAlpha (valVar) valVar tyVar uVar
         , CmpModAlpha (tyVar)  valVar tyVar uVar
         , CmpModAlpha (uVar)   valVar tyVar uVar)
      => CmpModAlpha (GenCoreBinder valVar tyVar uVar) valVar tyVar uVar

...
\end{pseudocode}



\subsection{Various kinds of variables}


\begin{code}
cmpModAlphaValVar :: Ord valVar 
		   => Alpha valVar tyVar uVar -> valVar -> valVar -> _CMP_TAG

cmpModAlphaValVar (Alpha valVars tyVars uVars) valVar1 valVar2
  = case lookupFM valVars valVar1 of
      Nothing     -> _tagCmp valVar1 valVar2 -- valVar1 is global variable
      Just valVar -> _tagCmp valVar valVar2  -- valVar1 is local variable


cmpModAlphaTyVar :: Ord tyVar 
		  => Alpha valVar tyVar uVar -> tyVar -> tyVar -> _CMP_TAG

cmpModAlphaTyVar (Alpha valVars tyVars uVars) tyVar1 tyVar2
  = case lookupFM tyVars tyVar1 of
      Nothing    -> _tagCmp tyVar1 tyVar2 -- tyVar1 is global variable
      Just tyVar -> _tagCmp tyVar tyVar2  -- tyVar1 is local variable


cmpModAlphaUVar :: Ord uVar 
	         => Alpha valVar tyVar uVar -> uVar -> uVar -> _CMP_TAG
cmpModAlphaUVar (Alpha valVars tyVars uVars) uVar1 uVar2
  = case lookupFM uVars uVar1 of
      Nothing   -> _tagCmp uVar1 uVar2 -- uVar1 is global variable
      Just uVar -> _tagCmp uVar uVar2  -- uVar1 is local variable
\end{code}


\subsection{Expressions}

Unfortunately there don't yet exist instances of Ord.
It would make defining the following function much easier and shorter

\begin{code}
cmpModAlphaExpr :: (Ord valVar, Ord tyVar, Ord uVar)
 		 => Alpha valVar tyVar uVar
	         -> GenCoreExpr valVar valVar tyVar uVar
	         -> GenCoreExpr valVar valVar tyVar uVar
	         -> _CMP_TAG		

cmpModAlphaExpr alpha (Var var1) (Var var2) 
  = cmpModAlphaValVar alpha var1 var2
cmpModAlphaExpr alpha (Var _) _ = _LT

cmpModAlphaExpr alpha (Lit lit1) (Lit lit2) = _tagCmp lit1 lit2
cmpModAlphaExpr alpha (Lit _) (Var _) = _GT
cmpModAlphaExpr alpha (Lit _) _       = _LT

cmpModAlphaExpr alpha (Con conId1 args1) (Con conId2 args2)
  = _tagCmp conId1 conId2 `thenCmp` -- constructors are directly compared
   lexicalCmp (cmpModAlphaArg alpha) args1 args2
cmpModAlphaExpr alpha (Con _ _) (Var _) = _GT
cmpModAlphaExpr alpha (Con _ _) (Lit _) = _GT
cmpModAlphaExpr alpha (Con _ _) _       = _LT  

cmpModAlphaExpr alpha (Prim primOp1 args1) (Prim primOp2 args2)
  | (tagOf_PrimOp primOp1) _EQ_ (tagOf_PrimOp primOp2) 
    = lexicalCmp (cmpModAlphaArg alpha) args1 args2
  | (tagOf_PrimOp primOp1) _LT_ (tagOf_PrimOp primOp2)
    = _LT
  | otherwise
    = _GT
cmpModAlphaExpr alpha (Prim _ _) (Var _)   = _GT
cmpModAlphaExpr alpha (Prim _ _) (Lit _)   = _GT
cmpModAlphaExpr alpha (Prim _ _) (Con _ _) = _GT
cmpModAlphaExpr alpha (Prim _ _) _         = _LT
  
cmpModAlphaExpr alpha (Lam binder1 expr1) (Lam binder2 expr2)
  = cmp `thenCmp` cmpModAlphaExpr alpha' expr1 expr2
    where
    (cmp, alpha') = cmpModAlphaBinder alpha binder1 binder2
cmpModAlphaExpr alpha (Lam _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (Lam _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (Lam _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (Lam _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (Lam _ _) _          = _LT

cmpModAlphaExpr alpha (App fun1 arg1) (App fun2 arg2)
  = cmpModAlphaExpr alpha fun1 fun2 `thenCmp` cmpModAlphaArg alpha arg1 arg2
cmpModAlphaExpr alpha (App _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (App _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (App _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (App _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (App _ _) (Lam _ _)  = _GT
cmpModAlphaExpr alpha (App _ _) _          = _LT

cmpModAlphaExpr alpha (Case expr1 alts1) (Case expr2 alts2)
  = cmpModAlphaExpr alpha expr1 expr2 `thenCmp` 
    cmpModAlphaCaseAlts alpha alts1 alts2
cmpModAlphaExpr alpha (Case _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (Case _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (Case _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (Case _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (Case _ _) (Lam _ _)  = _GT
cmpModAlphaExpr alpha (Case _ _) (App _ _)  = _GT
cmpModAlphaExpr alpha (Case _ _) _          = _LT

cmpModAlphaExpr alpha (Let binder1 expr1) (Let binder2 expr2)
  = cmp `thenCmp` cmpModAlphaExpr alpha' expr1 expr2
    where
    (cmp, alpha') = cmpModAlphaBinding alpha binder1 binder2
cmpModAlphaExpr alpha (Let _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (Let _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (Let _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (Let _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (Let _ _) (Lam _ _)  = _GT
cmpModAlphaExpr alpha (Let _ _) (App _ _)  = _GT
cmpModAlphaExpr alpha (Let _ _) (Case _ _) = _GT
cmpModAlphaExpr alpha (Let _ _) _          = _LT

-- does comparing cost centres make sense? should possibly be always unequal!
-- danger: order is not antisymmetric: x _GT y and y _GT x
cmpModAlphaExpr alpha (SCC costCentre1 expr1) (SCC costCentre2 expr2) = _GT
cmpModAlphaExpr alpha (SCC _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (SCC _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (SCC _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (SCC _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (SCC _ _) (Lam _ _)  = _GT
cmpModAlphaExpr alpha (SCC _ _) (App _ _)  = _GT
cmpModAlphaExpr alpha (SCC _ _) (Case _ _) = _GT
cmpModAlphaExpr alpha (SCC _ _) (Let _ _)  = _GT
cmpModAlphaExpr alpha (SCC _ _) _          = _LT

cmpModAlphaExpr alpha (Coerce coercion1 typeExpr1 expr1) 
		       (Coerce coercion2 typeExpr2 expr2)
  = _tagCmp coercion1 coercion2 `thenCmp`
    cmpModAlphaType alpha typeExpr1 typeExpr2 `thenCmp`
    cmpModAlphaExpr alpha expr1 expr2 
cmpModAlphaExpr alpha (Coerce _ _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Lam _ _)  = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (App _ _)  = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Case _ _) = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Let _ _)  = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (SCC _ _)  = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) _          = _LT
\end{code}


\subsection{Case expressions}

\begin{code}
cmpModAlphaCaseAlts :: (Ord valVar, Ord tyVar, Ord uVar)
		     => Alpha valVar tyVar uVar
		     -> GenCoreCaseAlts valVar valVar tyVar uVar
		     -> GenCoreCaseAlts valVar valVar tyVar uVar
		     -> _CMP_TAG
-- alternatives have to be in the same order

cmpModAlphaCaseAlts alpha (AlgAlts alts1 deflt1) (AlgAlts alts2 deflt2)
  = lexicalCmp (cmpModAlphaArgTriple alpha) alts1 alts2 `thenCmp`
    cmpModAlphaCaseDefault alpha deflt1 deflt2        
cmpModAlphaCaseAlts alpha (AlgAlts alts1 deflt1) _ = _LT
cmpModAlphaCaseAlts alpha (PrimAlts alts1 deflt1) (PrimAlts alts2 deflt2)
  = lexicalCmp (cmpModAlphaArgPair alpha) alts1 alts2 `thenCmp`
    cmpModAlphaCaseDefault alpha deflt1 deflt2
cmpModAlphaCaseAlts alpha (PrimAlts _ _) (AlgAlts _ _) = _GT
cmpModAlphaCaseAlts alpha (PrimAlts _ _) _             = _LT


cmpModAlphaArgTriple :: (Ord valVar, Ord tyVar, Ord uVar)
                     => Alpha valVar tyVar uVar
                     -> (Id, [valVar], GenCoreExpr valVar valVar tyVar uVar)
                     -> (Id, [valVar], GenCoreExpr valVar valVar tyVar uVar)
	   	     -> _CMP_TAG

cmpModAlphaArgTriple alpha (id1, valVars1, expr1) (id2, valVars2, expr2)
  = _tagCmp id1 id2 `thenCmp`
    cmpModAlphaExpr alpha' expr1 expr2
  where
  alpha' = foldl add alpha (zip valVars1 valVars2)
  add :: (Ord valVar, Ord tyVar, Ord uVar) 
      => Alpha valVar tyVar uVar 
      -> (valVar, valVar) 
      -> Alpha valVar tyVar uVar
  add alpha (valVar1, valVar2) = addToAlphaValVar alpha valVar1 valVar2


cmpModAlphaArgPair :: (Ord valVar, Ord tyVar, Ord uVar)
                   => Alpha valVar tyVar uVar
                   -> (Literal, GenCoreExpr valVar valVar tyVar uVar)
                   -> (Literal, GenCoreExpr valVar valVar tyVar uVar)
	   	   -> _CMP_TAG

cmpModAlphaArgPair alpha (lit1, expr1) (lit2, expr2)
  = _tagCmp lit1 lit2 `thenCmp`
    cmpModAlphaExpr alpha expr1 expr2



cmpModAlphaCaseDefault :: (Ord valVar, Ord tyVar, Ord uVar)
			=> Alpha valVar tyVar uVar
			-> GenCoreCaseDefault valVar valVar tyVar uVar
			-> GenCoreCaseDefault valVar valVar tyVar uVar
			-> _CMP_TAG

cmpModAlphaCaseDefault alpha NoDefault NoDefault = _EQ
cmpModAlphaCaseDefault alpha NoDefault _         = _LT
cmpModAlphaCaseDefault alpha (BindDefault valBdr1 expr1) 
                             (BindDefault valBdr2 expr2)
  = cmpModAlphaExpr (addToAlphaValVar alpha valBdr1 valBdr2) expr1 expr2
cmpModAlphaCaseDefault alpha (BindDefault _ _) NoDefault = _GT
\end{code}


\subsection{Arguments}


\begin{code}
cmpModAlphaArg :: (Ord valVar, Ord tyVar, Ord uVar)
	       => Alpha valVar tyVar uVar
	       -> GenCoreArg valVar tyVar uVar
	       -> GenCoreArg valVar tyVar uVar
               -> _CMP_TAG

cmpModAlphaArg alpha (LitArg lit1) (LitArg lit2)
  = _tagCmp lit1 lit2 
cmpModAlphaArg alpha (LitArg _) _ = _LT
cmpModAlphaArg alpha (VarArg valVar1) (VarArg valVar2)
  = cmpModAlphaValVar alpha valVar1 valVar2
cmpModAlphaArg alpha (VarArg _) (LitArg _) = _GT
cmpModAlphaArg alpha (VarArg _) _          = _LT
cmpModAlphaArg alpha (TyArg type1) (TyArg type2)
  = cmpModAlphaType alpha type1 type2
cmpModAlphaArg alpha (TyArg _) (VarArg _) = _GT
cmpModAlphaArg alpha (TyArg _) (LitArg _) = _GT
cmpModAlphaArg alpha (TyArg _) _          = _LT
cmpModAlphaArg alpha (UsageArg usage1) (UsageArg usage2)
  = cmpModAlphaUsage alpha usage1 usage2
cmpModAlphaArg alpha (UsageArg _) (VarArg _) = _GT
cmpModAlphaArg alpha (UsageArg _) (LitArg _) = _GT
cmpModAlphaArg alpha (UsageArg _) (TyArg _)  = _GT
cmpModAlphaArg alpha (UsageArg _) _          = _LT
\end{code}


\subsection{Types}

Compare for definition of @eqTy@ in module @Type@.

\begin{code}
cmpModAlphaType :: (Ord tyVar, Ord uVar)
		=> Alpha valVar tyVar uVar
		-> GenType tyVar uVar
		-> GenType tyVar uVar
		-> _CMP_TAG

cmpModAlphaType alpha (TyVarTy tyVar1) (TyVarTy tyVar2)
  = cmpModAlphaTyVar alpha tyVar1 tyVar2
cmpModAlphaType alpha (TyVarTy tyVar1) _ = _LT

cmpModAlphaType alpha (AppTy type11 type12) (AppTy type21 type22)
  = cmpModAlphaType alpha type11 type21 `thenCmp`
    cmpModAlphaType alpha type12 type22 
cmpModAlphaType alpha type1@(AppTy _ _) (FunTy type21 type22 usage2)
  -- expand function type just in case that version matches
  = cmpModAlphaType alpha type1 
      (AppTy (AppTy (TyConTy mkFunTyCon usage2) type21) type22)
cmpModAlphaType alpha (AppTy _ _) (TyVarTy _) = _GT
cmpModAlphaType alpha (AppTy _ _) _           = _LT
 
cmpModAlphaType alpha (TyConTy tyCon1 usage1) (TyConTy tyCon2 usage2)
  = _tagCmp tyCon1 tyCon2 `thenCmp`
    cmpModAlphaUsage alpha usage1 usage2
cmpModAlphaType alpha (TyConTy _ _) (TyVarTy _) = _GT
cmpModAlphaType alpha (TyConTy _ _) (AppTy _ _) = _GT
cmpModAlphaType alpha (TyConTy _ _) _           = _LT

cmpModAlphaType alpha (SynTy tyCon1 args1 expType1) 
                      (SynTy tyCon2 args2 expType2)
  = case _tagCmp tyCon1 tyCon2 `thenCmp` 
         lexicalCmp (cmpModAlphaType alpha) args1 args2 of
      _EQ -> _EQ
      _   -> cmpModAlphaType alpha expType1 expType2
cmpModAlphaType alpha (SynTy _ _ _) (TyVarTy _)   = _GT
cmpModAlphaType alpha (SynTy _ _ _) (AppTy _ _)   = _GT
cmpModAlphaType alpha (SynTy _ _ _) (TyConTy _ _) = _GT
cmpModAlphaType alpha (SynTy _ _ _) _             = _LT

cmpModAlphaType alpha (ForAllTy tyVar1 type1) (ForAllTy tyVar2 type2)
  = cmpModAlphaType (addToAlphaTyVar alpha tyVar1 tyVar2) type1 type2
cmpModAlphaType alpha (ForAllTy _ _) (TyVarTy _)   = _GT
cmpModAlphaType alpha (ForAllTy _ _) (AppTy _ _)   = _GT
cmpModAlphaType alpha (ForAllTy _ _) (TyConTy _ _) = _GT
cmpModAlphaType alpha (ForAllTy _ _) (SynTy _ _ _) = _GT
cmpModAlphaType alpha (ForAllTy _ _) _             = _LT

cmpModAlphaType alpha (ForAllUsageTy uVar1 bUsages1 type1)
                      (ForAllUsageTy uVar2 bUsages2 type2)
  = lexicalCmp (cmpModAlphaUVar alpha) bUsages1 bUsages2 `thenCmp`
    cmpModAlphaType (addToAlphaUVar alpha uVar1 uVar2) type1 type2
cmpModAlphaType alpha (ForAllUsageTy _ _ _) (TyVarTy _)    = _GT
cmpModAlphaType alpha (ForAllUsageTy _ _ _) (AppTy _ _)    = _GT
cmpModAlphaType alpha (ForAllUsageTy _ _ _) (TyConTy _ _)  = _GT
cmpModAlphaType alpha (ForAllUsageTy _ _ _) (SynTy _ _ _)  = _GT
cmpModAlphaType alpha (ForAllUsageTy _ _ _) (ForAllTy _ _) = _GT
cmpModAlphaType alpha (ForAllUsageTy _ _ _) _              = _LT

cmpModAlphaType alpha (FunTy type11 type12 usage1)
                      (FunTy type21 type22 usage2)
  = cmpModAlphaType alpha type11 type21 `thenCmp`
    cmpModAlphaType alpha type12 type22 `thenCmp`
    cmpModAlphaUsage alpha usage1 usage2
cmpModAlphaType alpha (FunTy type11 type12 usage1) type2@(AppTy _ _)
  -- expand function type just in case that version matches
  = cmpModAlphaType alpha 
      (AppTy (AppTy (TyConTy mkFunTyCon usage1) type11) type12) type2
cmpModAlphaType alpha (FunTy _ _ _) (TyVarTy _)           = _GT
cmpModAlphaType alpha (FunTy _ _ _) (TyConTy _ _)         = _GT
cmpModAlphaType alpha (FunTy _ _ _) (SynTy _ _ _)         = _GT
cmpModAlphaType alpha (FunTy _ _ _) (ForAllTy _ _)        = _GT
cmpModAlphaType alpha (FunTy _ _ _) (ForAllUsageTy _ _ _) = _GT
cmpModAlphaType alpha (FunTy _ _ _) _                     = _LT

cmpModAlphaType alpha (DictTy class1 type1 usage1)      
                      (DictTy class2 type2 usage2)
  = _tagCmp class1 class2 `thenCmp` 
    cmpModAlphaType alpha type1 type2 `thenCmp`
    cmpModAlphaUsage alpha usage1 usage2
  -- expansion too complicated
{-
  -- NB we use a guard for c1==c2 so that if they aren't equal we
  -- fall through into expanding the type. 
cmpModAlphaType alpha type1@(DictTy _ _ _) type2
  = cmpModAlphaType alpha (expandTy type1) type2
cmpModAlphaType alpha type1 type2@(DictTy _ _ _)
  = cmpModAlphaType alpha type1 (expandTy type2)
-}
cmpModAlphaType alpha (DictTy _ _ _) (TyVarTy _)           = _GT
cmpModAlphaType alpha (DictTy _ _ _) (AppTy _ _)           = _GT
cmpModAlphaType alpha (DictTy _ _ _) (TyConTy _ _)         = _GT
cmpModAlphaType alpha (DictTy _ _ _) (SynTy _ _ _)         = _GT
cmpModAlphaType alpha (DictTy _ _ _) (ForAllTy _ _)        = _GT
cmpModAlphaType alpha (DictTy _ _ _) (ForAllUsageTy _ _ _) = _GT
cmpModAlphaType alpha (DictTy _ _ _) (FunTy _ _ _)         = _GT
cmpModAlphaType alpha (DictTy _ _ _) _                     = _LT
\end{code}



\subsection{Usages}

\begin{code}
cmpModAlphaUsage :: Ord uVar
		 => Alpha valVar tyVar uVar
		 -> GenUsage uVar
		 -> GenUsage uVar
		 -> _CMP_TAG

cmpModAlphaUsage alpha (UsageVar uVar1) (UsageVar uVar2)
  = cmpModAlphaUVar alpha uVar1 uVar2
cmpModAlphaUsage alpha (UsageVar _) _ = _LT
cmpModAlphaUsage alpha UsageOne UsageOne     = _EQ
cmpModAlphaUsage alpha UsageOne (UsageVar _) = _GT
cmpModAlphaUsage alpha UsageOne _            = _LT
cmpModAlphaUsage alpha UsageOmega UsageOmega   = _EQ
cmpModAlphaUsage alpha UsageOmega (UsageVar _) = _GT
cmpModAlphaUsage alpha UsageOmega UsageOne     = _GT
cmpModAlphaUsage alpha UsageOmega _            = _LT
\end{code}


\begin{onlystandalone}
\end{document}
\end{onlystandalone}