From a9ae952e647887c0108080ca48426cb35bdd8400 Mon Sep 17 00:00:00 2001
From: simonpj <unknown>
Date: Mon, 27 Jun 2005 12:59:52 +0000
Subject: [PATCH 1/1] [project @ 2005-06-27 12:59:52 by simonpj] MERGE TO
 STABLE

Fix a typechecker bug, which made the typechecker loop under certain
circumstances, notably when we have
	type Foo a = a
and try to unify
	b :=: Foo b

typecheck/should_compile/tc195 tests this case now.
---
 ghc/compiler/types/Unify.lhs |   24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/ghc/compiler/types/Unify.lhs b/ghc/compiler/types/Unify.lhs
index bb43ce0..255a7f1 100644
--- a/ghc/compiler/types/Unify.lhs
+++ b/ghc/compiler/types/Unify.lhs
@@ -344,22 +344,30 @@ uVar swap subst tv1 ty
      Just ty' | swap      -> unify subst ty ty' 
               | otherwise -> unify subst ty' ty
      -- No, continue
-     Nothing          -> uUnrefined subst tv1 ty
+     Nothing          -> uUnrefined subst tv1 ty ty
 
 
 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
            -> TyVar               -- Type variable to be unified
            -> Type                -- with this type
+           -> Type                -- (de-noted version)
            -> UM TvSubstEnv
 
 -- We know that tv1 isn't refined
-uUnrefined subst tv1 ty2@(TyVarTy tv2)
-  | tv1 == tv2    -- Same, do nothing
+
+uUnrefined subst tv1 ty2 (NoteTy _ ty2')
+  = uUnrefined subst tv1 ty2 ty2'	-- Unwrap synonyms
+		-- This is essential, in case we have
+		--	type Foo a = a
+		-- and then unify a :=: Foo a
+
+uUnrefined subst tv1 ty2 (TyVarTy tv2)
+  | tv1 == tv2		-- Same type variable
   = return subst
 
     -- Check to see whether tv2 is refined
   | Just ty' <- lookupVarEnv subst tv2
-  = uUnrefined subst tv1 ty'
+  = uUnrefined subst tv1 ty' ty'
 
   -- So both are unrefined; next, see if the kinds force the direction
   | k1 == k2	-- Can update either; so check the bind-flags
@@ -390,16 +398,16 @@ uUnrefined subst tv1 ty2@(TyVarTy tv2)
     k2 = tyVarKind tv2
     bind tv ty = return (extendVarEnv subst tv ty)
 
-uUnrefined subst tv1 ty2	-- ty2 is not a type variable
-  | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2)
+uUnrefined subst tv1 ty2 ty2'	-- ty2 is not a type variable
+  | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
   = failWith (occursCheck tv1 ty2)	-- Occurs check
   | not (k2 `isSubKind` k1)
   = failWith (kindMisMatch tv1 ty2)	-- Kind check
   | otherwise
-  = bindTv subst tv1 ty2
+  = bindTv subst tv1 ty2		-- Bind tyvar to the synonym if poss
   where
     k1 = tyVarKind tv1
-    k2 = typeKind ty2
+    k2 = typeKind ty2'
 
 substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
 -- Apply the non-idempotent substitution to a set of type variables,
-- 
1.7.10.4