diff --git a/Makefile.am b/Makefile.am
index 8c8efba..35ae5c0 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -144,6 +144,7 @@ tock_SOURCES_hs += frontends/PreprocessOccam.hs
 tock_SOURCES_hs += frontends/RainPasses.hs
 tock_SOURCES_hs += frontends/RainTypes.hs
 tock_SOURCES_hs += frontends/StructureOccam.hs
+tock_SOURCES_hs += frontends/TypeUnification.hs
 tock_SOURCES_hs += pass/Pass.hs
 tock_SOURCES_hs += pass/PassList.hs
 tock_SOURCES_hs += pass/Properties.hs
diff --git a/frontends/RainTypesTest.hs b/frontends/RainTypesTest.hs
index 4a41f71..f01eb57 100644
--- a/frontends/RainTypesTest.hs
+++ b/frontends/RainTypesTest.hs
@@ -23,6 +23,7 @@ import Control.Monad.State
 import Control.Monad.Error
 import Control.Monad.Writer
 import Data.Generics
+import qualified Data.Map as Map
 import Test.HUnit hiding (State)
 
 import qualified AST as A
@@ -36,6 +37,7 @@ import TagAST
 import TestUtils
 import TreeUtils
 import Types
+import TypeUnification
 import Utils
 
 m :: Meta
@@ -479,6 +481,24 @@ checkExpressionTest = TestList
              defVar "t" $ A.Time
              markRainTest
 
+testUnify :: Test
+testUnify = TestList
+ [test [] [] $ Just []
+ ,test' [("a",A.Int)] []
+ ,test' [("a",A.Int)] [("a","a")]
+ ,test [("a", A.Int), ("b", A.Infer)] [("a","b")] $
+  Just [("a", A.Int), ("b", A.Int)]
+ ]
+ where
+   test :: [(String, A.Type)] -> [(String, String)] -> Maybe [(String, A.Type)]
+     -> Test
+   test im u om = TestCase $ assertEqual "testUnify" (fmap Map.fromList om) $ Just $ unifyRainTypes (Map.fromList
+     im) u
+
+   test' :: [(String, A.Type)] -> [(String, String)] -> Test
+   test' x y = test x y (Just x)
+
+
 tests :: Test
 tests = TestLabel "RainTypesTest" $ TestList
  [
@@ -486,4 +506,5 @@ tests = TestLabel "RainTypesTest" $ TestList
   ,annotateIntTest
   ,annotateListLiteralTest
   ,checkExpressionTest
+  ,testUnify
  ]
diff --git a/frontends/TypeUnification.hs b/frontends/TypeUnification.hs
new file mode 100644
index 0000000..7f269c4
--- /dev/null
+++ b/frontends/TypeUnification.hs
@@ -0,0 +1,149 @@
+{-
+Tock: a compiler for parallel languages
+Copyright (C) 2008  University of Kent
+
+This program is free software; you can redistribute it and/or modify it
+under the terms of the GNU General Public License as published by the
+Free Software Foundation, either version 2 of the License, or (at your
+option) any later version.
+
+This program is distributed in the hope that it will be useful, but
+WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+General Public License for more details.
+
+You should have received a copy of the GNU General Public License along
+with this program.  If not, see <http://www.gnu.org/licenses/>.
+-}
+
+module TypeUnification where
+
+import Control.Monad.ST
+import Data.Generics
+import qualified Data.Map as Map
+import Data.STRef
+
+import qualified AST as A
+import Utils
+
+-- Much of the code in this module is taken from or based on Tim Sheard's Haskell
+-- listing of a simple type unification algorithm at the beginning of his
+-- paper "Generic Unification via Two-Level Types and Parameterized Modules Functional
+-- Pearl (2001)", citeseer: http://citeseer.ist.psu.edu/451401.html
+-- This in turn was taken from Luca Cardelli's "Basic Polymorphic Type Checking"
+
+unifyRainTypes :: Map.Map String A.Type -> [(String, String)] -> Map.Map String A.Type
+unifyRainTypes m prs
+  = runST $ do m' <- mapToST m
+               mapM_ (\(x,y) -> unifyType (lookupStartType x m') (lookupStartType y
+                 m')) prs
+               stToMap m'
+  where
+    lookupStartType :: String -> Map.Map String (TypeExp s A.Type) -> TypeExp
+      s A.Type
+    lookupStartType s m = case Map.lookup s m of
+      Just x -> x
+      Nothing -> error $ "Could not find type for variable in map before unification: "
+        ++ s
+
+    mapToST :: Map.Map String A.Type -> ST s (Map.Map String (TypeExp s A.Type))
+    mapToST = mapMapM typeToTypeExp
+
+    stToMap :: Map.Map String (TypeExp s A.Type) -> ST s (Map.Map String
+      A.Type)
+    stToMap = mapMapM (read <.< prune)
+      where
+        read :: TypeExp s A.Type -> ST s A.Type
+        read (OperType con vals) = do vals' <- mapM read vals
+                                      return $ fromConstr con -- vals'
+        read x = error $ "Type error in unification, found: " ++ show x
+
+ttte :: Data b => b -> A.Type -> ST s (TypeExp s A.Type)
+ttte c t = typeToTypeExp t >>= \t' -> return $ OperType (toConstr c) [t']
+
+-- Transforms the given type into a typeexp, such that the only inner types
+-- left will be the primitive types (integer types, float types, bool, time).  Arrays
+-- (which would require unification of dimensions and such) are not supported,
+-- neither are records.
+--  User data types should not be present in the input.
+typeToTypeExp :: A.Type -> ST s (TypeExp s A.Type)
+typeToTypeExp x@(A.List t) = ttte x t
+typeToTypeExp (A.Chan A.DirInput _ t) = ttte "?" t
+typeToTypeExp (A.Chan A.DirOutput _ t) = ttte "!" t
+typeToTypeExp (A.Chan A.DirUnknown _ t) = ttte "channel" t
+typeToTypeExp (A.Mobile t) = ttte "MOBILE" t
+typeToTypeExp (A.Infer) = do r <- newSTRef Nothing
+                             return $ MutVar r
+typeToTypeExp t = return $ OperType (toConstr t) []
+
+type Ptr s a = STRef s (Maybe (TypeExp s a))
+
+-- TODO add a special type for numeric literals
+data TypeExp s a
+ = MutVar (Ptr s a)
+ | GenVar Int
+ | OperType Constr [ TypeExp s a ]
+
+-- For debugging:
+instance Show (TypeExp s a) where
+  show (MutVar {}) = "MutVar"
+  show (GenVar {}) = "GenVar"
+  show (OperType {}) = "OperType"
+
+prune :: TypeExp s a -> ST s (TypeExp s a)
+prune t =
+ case t of
+   MutVar r ->
+     do m <- readSTRef r
+        case m of
+          Nothing -> return t
+          Just t2 ->
+            do t' <- prune t2
+               writeSTRef r (Just t')
+               return t'
+   _ -> return t
+
+occursInType :: Ptr s a -> TypeExp s a -> ST s Bool
+occursInType r t =
+  do t' <- prune t
+     case t' of
+       MutVar r2 -> return $ r == r2
+       GenVar n -> return False
+       OperType nm ts ->
+             do bs <- mapM (occursInType r) ts
+                return (or bs)
+
+unifyType :: TypeExp s a -> TypeExp s a -> ST s ()
+unifyType t1 t2
+  = do t1' <- prune t1
+       t2' <- prune t2
+       case (t1',t2') of
+         (MutVar r1, MutVar r2) ->
+           if r1 == r2
+             then return ()
+             else writeSTRef r1 (Just t2')
+         (MutVar r1, _) ->
+           do b <- occursInType r1 t2'
+              if b
+                then error "occurs in"
+                else writeSTRef r1 (Just t2')
+         (_,MutVar _) -> unifyType t2' t1'
+         (GenVar n,GenVar m) ->
+           if n == m then return () else error "different genvars"
+         (OperType n1 ts1,OperType n2 ts2) ->
+           if n1 == n2
+              then unifyArgs ts1 ts2
+              else error "different constructors"
+         (_,_) -> error "different types"
+  where
+    unifyArgs (x:xs) (y:ys) = do unifyType x y
+                                 unifyArgs xs ys
+    unifyArgs [] [] = return ()
+    unifyArgs _ _ = error "different lengths"
+
+instantiate :: [TypeExp s a] -> TypeExp s a -> TypeExp s a
+instantiate ts x = case x of
+  MutVar _ -> x
+  OperType nm xs -> OperType nm (map (instantiate ts) xs)
+  GenVar n -> ts !! n
+