From: simonpj <unknown>
Date: Wed, 16 Nov 2005 12:55:59 +0000 (+0000)
Subject: [project @ 2005-11-16 12:55:58 by simonpj]
X-Git-Tag: Initial_conversion_from_CVS_complete~48
X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;h=cdea99491a8dedfc53fc2e8c4c8fbaf209802b27;p=ghc-hetmet.git

[project @ 2005-11-16 12:55:58 by simonpj]
Two significant changes to the representation of types

1. Change the representation of type synonyms

    Up to now, type synonym applications have been held in
    *both* expanded *and* un-expanded form.  Unfortunately, this
    has exponential (!) behaviour when type synonyms are deeply
    nested.  E.g.
	    type P a b = (a,b)
	    f :: P a (P b (P c (P d e)))

    This showed up in a program of Joel Reymont, now immortalised
    as typecheck/should_compile/syn-perf.hs

    So now synonyms are held as ordinary TyConApps, and expanded
    only on demand.

    SynNote has disappeared altogether, so the only remaining TyNote
    is a FTVNote.  I'm not sure if it's even useful.

2. Eta-reduce newtypes

    See the Note [Newtype eta] in TyCon.lhs

    If we have
	    newtype T a b = MkT (S a b)

    then, in Core land, we would like S = T, even though the application
    of T is then not saturated. This commit eta-reduces T's RHS, and
    keeps that inside the TyCon (in nt_etad_rhs).  Result is that
    coreEqType can be simpler, and has less need of expanding newtypes.
---

diff --git a/ghc/compiler/codeGen/ClosureInfo.lhs b/ghc/compiler/codeGen/ClosureInfo.lhs
index 48c4dde..b0e9e23 100644
--- a/ghc/compiler/codeGen/ClosureInfo.lhs
+++ b/ghc/compiler/codeGen/ClosureInfo.lhs
@@ -946,7 +946,6 @@ getTyDescription ty
       FunTy _ res      	     -> '-' : '>' : fun_result res
       TyConApp tycon _ 	     -> getOccString tycon
       NoteTy (FTVNote _) ty  -> getTyDescription ty
-      NoteTy (SynNote ty1) _ -> getTyDescription ty1
       PredTy sty	     -> getPredTyDescription sty
       ForAllTy _ ty          -> getTyDescription ty
     }
diff --git a/ghc/compiler/iface/BuildTyCl.lhs b/ghc/compiler/iface/BuildTyCl.lhs
index 6fb8d92..f81f2e7 100644
--- a/ghc/compiler/iface/BuildTyCl.lhs
+++ b/ghc/compiler/iface/BuildTyCl.lhs
@@ -14,10 +14,10 @@ module BuildTyCl (
 import IfaceEnv		( newImplicitBinder )
 import TcRnMonad
 
-import DataCon		( DataCon, isNullarySrcDataCon,
+import DataCon		( DataCon, isNullarySrcDataCon, dataConTyVars,
 			  mkDataCon, dataConFieldLabels, dataConOrigArgTys )
 import Var		( tyVarKind, TyVar, Id )
-import VarSet		( isEmptyVarSet, intersectVarSet )
+import VarSet		( isEmptyVarSet, intersectVarSet, elemVarSet )
 import TysWiredIn  	( unitTy )
 import BasicTypes	( RecFlag, StrictnessMark(..) )
 import Name		( Name )
@@ -27,9 +27,12 @@ import MkId		( mkDataConIds, mkRecordSelId, mkDictSelId )
 import Class		( mkClass, Class( classTyCon), FunDep, DefMeth(..) )
 import TyCon		( mkSynTyCon, mkAlgTyCon, visibleDataCons, tyConStupidTheta,
 			  tyConDataCons, isNewTyCon, mkClassTyCon, TyCon( tyConTyVars ),
+			  isRecursiveTyCon,
 			  ArgVrcs, AlgTyConRhs(..), newTyConRhs )
-import Type		( mkArrowKinds, liftedTypeKind, typeKind, tyVarsOfTypes, tyVarsOfPred,
-			  splitTyConApp_maybe, mkPredTys, mkTyVarTys, ThetaType, Type,
+import Type		( mkArrowKinds, liftedTypeKind, typeKind, 
+			  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
+			  splitTyConApp_maybe, splitAppTy_maybe, getTyVar_maybe,
+			  mkPredTys, mkTyVarTys, ThetaType, Type, 
 			  substTyWith, zipTopTvSubst, substTheta )
 import Outputable
 import List		( nub )
@@ -67,19 +70,36 @@ mkAbstractTyConRhs = AbstractTyCon
 
 mkDataTyConRhs :: [DataCon] -> AlgTyConRhs
 mkDataTyConRhs cons
-  = DataTyCon cons (all isNullarySrcDataCon cons)
+  = DataTyCon { data_cons = cons, is_enum = all isNullarySrcDataCon cons }
 
 mkNewTyConRhs :: TyCon -> DataCon -> AlgTyConRhs
 mkNewTyConRhs tycon con 
-  = NewTyCon con rhs_ty (mkNewTyConRep tycon)
+  = NewTyCon { data_con = con, 
+	       nt_rhs = rhs_ty,
+	       nt_etad_rhs = eta_reduce tvs rhs_ty,
+	       nt_rep = mkNewTyConRep tycon rhs_ty }
   where
+    tvs    = dataConTyVars con
     rhs_ty = head (dataConOrigArgTys con)
 	-- Newtypes are guaranteed vanilla, so OrigArgTys will do
+
+    eta_reduce [] ty = ([], ty)
+    eta_reduce (a:as) ty | null as', 
+			   Just (fun, arg) <- splitAppTy_maybe ty',
+			   Just tv <- getTyVar_maybe arg,
+			   tv == a,
+			   not (a `elemVarSet` tyVarsOfType fun)
+			 = ([], fun)	-- Successful eta reduction
+			 | otherwise
+			 = (a:as', ty')
+	where
+  	  (as', ty') = eta_reduce as ty
 				
 mkNewTyConRep :: TyCon		-- The original type constructor
+	      -> Type		-- The arg type of its constructor
 	      -> Type		-- Chosen representation type
-				-- (guaranteed not to be another newtype)
-				-- Free vars of rep = tyConTyVars tc
+-- The "representation type" is guaranteed not to be another newtype
+-- at the outermost level; but it might have newtypes in type arguments
 
 -- Find the representation type for this newtype TyCon
 -- Remember that the representation type is the *ultimate* representation
@@ -92,24 +112,24 @@ mkNewTyConRep :: TyCon		-- The original type constructor
 -- The trick is to to deal correctly with recursive newtypes
 -- such as	newtype T = MkT T
 
-mkNewTyConRep tc
+mkNewTyConRep tc rhs_ty
   | null (tyConDataCons tc) = unitTy
 	-- External Core programs can have newtypes with no data constructors
-  | otherwise		    = go [] tc
+  | otherwise		    = go [tc] rhs_ty
   where
-	-- Invariant: tc is a NewTyCon
-	-- 	      tcs have been seen before
-    go tcs tc 
-	| tc `elem` tcs = unitTy
-	| otherwise
-	= case splitTyConApp_maybe rhs_ty of
-	    Just (tc1, tys) | isNewTyCon tc1
-			   -> ASSERT( length (tyConTyVars tc1) == length tys )
-			      substTyWith (tyConTyVars tc1) tys (go (tc:tcs) tc1)
-	    other 	   -> rhs_ty 
-	where
-	  (_tc_tvs, rhs_ty) = newTyConRhs tc
-
+	-- Invariant: tcs have been seen before
+    go tcs rep_ty 
+	= case splitTyConApp_maybe rep_ty of
+	    Just (tc, tys)
+		| tc `elem` tcs -> unitTy	-- Recursive loop
+		| isNewTyCon tc -> ASSERT( isRecursiveTyCon tc )
+					-- Non-recursive ones have been 
+					-- dealt with by splitTyConApp_maybe
+				   go (tc:tcs) (substTyWith tvs tys rhs_ty)
+		where
+		  (tvs, rhs_ty) = newTyConRhs tc
+
+	    other -> rep_ty 
 
 ------------------------------------------------------
 buildDataCon :: Name -> Bool -> Bool
diff --git a/ghc/compiler/iface/IfaceSyn.lhs b/ghc/compiler/iface/IfaceSyn.lhs
index 4434c5d..6975bac 100644
--- a/ghc/compiler/iface/IfaceSyn.lhs
+++ b/ghc/compiler/iface/IfaceSyn.lhs
@@ -518,9 +518,9 @@ tyThingToIfaceDecl ext (ATyCon tycon)
     tyvars      = tyConTyVars tycon
     (_, syn_ty) = getSynTyConDefn tycon
 
-    ifaceConDecls (NewTyCon con _ _) = IfNewTyCon  (ifaceConDecl con)
-    ifaceConDecls (DataTyCon cons _) = IfDataTyCon (map ifaceConDecl cons)
-    ifaceConDecls AbstractTyCon	     = IfAbstractTyCon
+    ifaceConDecls (NewTyCon { data_con = con })    = IfNewTyCon  (ifaceConDecl con)
+    ifaceConDecls (DataTyCon { data_cons = cons }) = IfDataTyCon (map ifaceConDecl cons)
+    ifaceConDecls AbstractTyCon			   = IfAbstractTyCon
 	-- The last case happens when a TyCon has been trimmed during tidying
 	-- Furthermore, tyThingToIfaceDecl is also used
 	-- in TcRnDriver for GHCi, when browsing a module, in which case the
diff --git a/ghc/compiler/iface/IfaceType.lhs b/ghc/compiler/iface/IfaceType.lhs
index e6471eb..2056a33 100644
--- a/ghc/compiler/iface/IfaceType.lhs
+++ b/ghc/compiler/iface/IfaceType.lhs
@@ -337,13 +337,13 @@ toIfaceBndr ext var
 
 ---------------------
 toIfaceType :: (Name -> IfaceExtName) -> Type -> IfaceType
+-- Synonyms are retained in the interface type
 toIfaceType ext (TyVarTy tv)     	     = IfaceTyVar (getOccName tv)
 toIfaceType ext (AppTy t1 t2)    	     = IfaceAppTy (toIfaceType ext t1) (toIfaceType ext t2)
 toIfaceType ext (FunTy t1 t2)    	     = IfaceFunTy (toIfaceType ext t1) (toIfaceType ext t2)
 toIfaceType ext (TyConApp tc tys) 	     = IfaceTyConApp (toIfaceTyCon ext tc) (toIfaceTypes ext tys)
 toIfaceType ext (ForAllTy tv t)  	     = IfaceForAllTy (toIfaceTvBndr tv) (toIfaceType ext t)
 toIfaceType ext (PredTy st)     	     = IfacePredTy (toIfacePred ext st)
-toIfaceType ext (NoteTy (SynNote tc_app) ty) = toIfaceType ext tc_app	-- Retain synonyms
 toIfaceType ext (NoteTy other_note ty)	     = toIfaceType ext ty
 
 ----------------
diff --git a/ghc/compiler/iface/TcIface.lhs b/ghc/compiler/iface/TcIface.lhs
index e10958b..f3f7e7f 100644
--- a/ghc/compiler/iface/TcIface.lhs
+++ b/ghc/compiler/iface/TcIface.lhs
@@ -547,9 +547,11 @@ mkIfTcApp :: TyCon -> [Type] -> Type
 -- foralls to the right of an arrow), so we must be careful to hoist them here.
 -- This hack should go away when we get rid of hoisting.
 -- Then we should go back to mkGenTyConApp or something like it
-mkIfTcApp tc tys
-  | isSynTyCon tc = hoistForAllTys (mkSynTy tc tys)
-  | otherwise	  = mkTyConApp tc tys
+-- 
+-- Nov 05: the type is now hoisted before being put into an interface file
+mkIfTcApp tc tys = mkTyConApp tc tys
+--  | isSynTyCon tc = hoistForAllTys (mkSynTy tc tys)
+--   | otherwise	  = mkTyConApp tc tys
 
 -----------------------------------------
 tcIfacePredType :: IfacePredType -> IfL PredType
diff --git a/ghc/compiler/main/Packages.lhs b/ghc/compiler/main/Packages.lhs
index 8324260..76d2f08 100644
--- a/ghc/compiler/main/Packages.lhs
+++ b/ghc/compiler/main/Packages.lhs
@@ -65,16 +65,9 @@ import System.Environment ( getEnv )
 import Distribution.InstalledPackageInfo
 import Distribution.Package
 import Distribution.Version
-import Data.Maybe	( isNothing )
 import System.Directory	( doesFileExist )
 import Control.Monad	( foldM )
-import Data.List	( nub, partition, sortBy )
-
-#ifdef mingw32_TARGET_OS
-import Data.List	( isPrefixOf )
-#endif
-import Data.List        ( isSuffixOf )
-
+import Data.List	( nub, partition, sortBy, isSuffixOf )
 import FastString
 import EXCEPTION	( throwDyn )
 import ErrUtils         ( debugTraceMsg, putMsg, Message )
diff --git a/ghc/compiler/ndpFlatten/Flattening.hs b/ghc/compiler/ndpFlatten/Flattening.hs
index 276b6a9..18daaa6 100644
--- a/ghc/compiler/ndpFlatten/Flattening.hs
+++ b/ghc/compiler/ndpFlatten/Flattening.hs
@@ -63,6 +63,8 @@ import FlattenMonad (Flatten, runFlatten, mkBind, extendContext, packContext,
 		     mk'indexOfP,mk'eq,mk'neq) 
 
 -- GHC
+import TcType	    ( tcIsForAllTy, tcView )
+import TypeRep	    ( Type(..) )
 import StaticFlags  (opt_Flatten)
 import Panic        (panic)
 import ErrUtils     (dumpIfSet_dyn)
@@ -72,7 +74,6 @@ import Literal      (Literal, literalType)
 import Var	    (Var(..), idType, isTyVar)
 import Id	    (setIdType)
 import DataCon	    (DataCon, dataConTag)
-import TypeRep      (Type(..))
 import HscTypes	    ( ModGuts(..), ModGuts, HscEnv(..), hscEPS )
 import CoreFVs	    (exprFreeVars)
 import CoreSyn	    (Expr(..), Bind(..), Alt(..), AltCon(..), Note(..),
@@ -246,7 +247,7 @@ vectorise (App expr arg) =
     (vexpr, vexprTy) <-  vectorise expr
     (varg,  vargTy)  <-  vectorise arg
 
-    if (isPolyType vexprTy)
+    if (tcIsForAllTy vexprTy)
       then do
         let resTy =  applyTypeToArg vexprTy varg
         return (App vexpr varg, resTy)
@@ -256,13 +257,6 @@ vectorise (App expr arg) =
         let resTy    = applyTypeToArg t1 varg   
         return  ((App vexpr' varg), resTy)  -- apply the first component of
                                             -- the vectorized function
-  where
-    isPolyType t =  
-        (case t  of
-           (ForAllTy _ _)  -> True
-           (NoteTy _ nt)   -> isPolyType nt
-           _               -> False)
-    
 
 vectorise  e@(Lam b expr)
   | isTyVar b
@@ -317,6 +311,10 @@ myShowTy (TyConApp _ t) =
 -}
 
 vectoriseTy :: Type -> Type 
+vectoriseTy ty | Just ty' <- tcView ty = vectoriseTy ty'
+	-- Look through notes and synonyms
+	-- NB: This will discard notes and synonyms, of course
+	-- ToDo: retain somehow?
 vectoriseTy t@(TyVarTy v)      =  t
 vectoriseTy t@(AppTy t1 t2)    = 
   AppTy (vectoriseTy t1) (vectoriseTy t2)
@@ -327,8 +325,6 @@ vectoriseTy t@(FunTy t1 t2)    =
                      (liftTy t)]
 vectoriseTy  t@(ForAllTy v ty)  = 
   ForAllTy v (vectoriseTy  ty)
-vectoriseTy t@(NoteTy note ty) =  -- FIXME: is the note still valid after
-  NoteTy note  (vectoriseTy ty)   --   this or should we just throw it away
 vectoriseTy  t =  t
 
 
@@ -336,9 +332,9 @@ vectoriseTy  t =  t
 --    on the *top level* (is this sufficient???)
 
 liftTy:: Type -> Type
+liftTy ty | Just ty' <- tcView ty = liftTy ty'
 liftTy (FunTy t1 t2)   = FunTy (liftTy t1) (liftTy t2)
 liftTy (ForAllTy tv t) = ForAllTy tv (liftTy t)
-liftTy (NoteTy n t)    = NoteTy n $ liftTy t
 liftTy  t              = mkPArrTy t
 
 
diff --git a/ghc/compiler/rename/RnTypes.lhs b/ghc/compiler/rename/RnTypes.lhs
index c30f1b7..a75d989 100644
--- a/ghc/compiler/rename/RnTypes.lhs
+++ b/ghc/compiler/rename/RnTypes.lhs
@@ -47,7 +47,7 @@ import SrcLoc		( SrcSpan, Located(..), unLoc, noLoc, combineLocs )
 import NameSet
 
 import Literal		( inIntRange, inCharRange )
-import BasicTypes	( compareFixity, funTyFixity, negateFixity, compareFixity,
+import BasicTypes	( compareFixity, funTyFixity, negateFixity, 
 			  Fixity(..), FixityDirection(..) )
 import ListSetOps	( removeDups )
 import Outputable
diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index fd0d1ca..4a800a2 100644
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -47,7 +47,7 @@ module TcMType (
 
 -- friends:
 import HsSyn		( LHsType )
-import TypeRep		( Type(..), PredType(..), TyNote(..),	 -- Friend; can see representation
+import TypeRep		( Type(..), PredType(..),  -- Friend; can see representation
 			  ThetaType
 			) 
 import TcType		( TcType, TcThetaType, TcTauType, TcPredType,
@@ -61,7 +61,7 @@ import TcType		( TcType, TcThetaType, TcTauType, TcPredType,
 			  typeKind, isFlexi, isSkolemTyVar,
 			  mkAppTy, mkTyVarTy, mkTyVarTys, 
 			  tyVarsOfPred, getClassPredTys_maybe,
-			  tyVarsOfType, tyVarsOfTypes, 
+			  tyVarsOfType, tyVarsOfTypes, tcView,
 			  pprPred, pprTheta, pprClassPred )
 import Kind		( Kind(..), KindVar, kindVarRef, mkKindVar, isSubKind,
 			  isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
@@ -527,11 +527,7 @@ zonkType unbound_var_fn rflag ty
     go (TyConApp tycon tys)	  = mappM go tys	`thenM` \ tys' ->
 				    returnM (TyConApp tycon tys')
 
-    go (NoteTy (SynNote ty1) ty2) = go ty1		`thenM` \ ty1' ->
-				    go ty2		`thenM` \ ty2' ->
-				    returnM (NoteTy (SynNote ty1') ty2')
-
-    go (NoteTy (FTVNote _) ty2)   = go ty2	-- Discard free-tyvar annotations
+    go (NoteTy _ ty2) 		  = go ty2	-- Discard free-tyvar annotations
 
     go (PredTy p)		  = go_pred p		`thenM` \ p' ->
 				    returnM (PredTy p')
@@ -825,29 +821,6 @@ check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 check_tau_type rank ubx_tup (AppTy ty1 ty2)
   = check_arg_type ty1 `thenM_` check_arg_type ty2
 
-check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
-	-- Synonym notes are built only when the synonym is 
-	-- saturated (see Type.mkSynTy)
-  = doptM Opt_GlasgowExts			`thenM` \ gla_exts ->
-    (if gla_exts then
-	-- If -fglasgow-exts then don't check the 'note' part.
-	-- This  allows us to instantiate a synonym defn with a 
-	-- for-all type, or with a partially-applied type synonym.
-	-- 	e.g.   type T a b = a
-	--	       type S m   = m ()
-	--	       f :: S (T Int)
-	-- Here, T is partially applied, so it's illegal in H98.
-	-- But if you expand S first, then T we get just 
-	--	       f :: Int
-	-- which is fine.
-	returnM ()
-    else
-	-- For H98, do check the un-expanded part
-	check_tau_type rank ubx_tup syn		
-    )						`thenM_`
-
-    check_tau_type rank ubx_tup ty
-
 check_tau_type rank ubx_tup (NoteTy other_note ty)
   = check_tau_type rank ubx_tup ty
 
@@ -856,8 +829,31 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   = 	-- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
 	-- synonym application, leaving it to checkValidType (i.e. right here)
 	-- to find the error
-    checkTc syn_arity_ok arity_msg	`thenM_`
-    mappM_ check_arg_type tys
+    do	{ 	-- It's OK to have an *over-applied* type synonym
+		--	data Tree a b = ...
+		--	type Foo a = Tree [a]
+		--	f :: Foo a b -> ...
+	; case tcView ty of
+	     Just ty' -> check_tau_type rank ubx_tup ty'	-- Check expansion
+	     Nothing  -> failWithTc arity_msg
+
+	; gla_exts <- doptM Opt_GlasgowExts
+	; if gla_exts then
+	-- If -fglasgow-exts then don't check the type arguments
+	-- This allows us to instantiate a synonym defn with a 
+	-- for-all type, or with a partially-applied type synonym.
+	-- 	e.g.   type T a b = a
+	--	       type S m   = m ()
+	--	       f :: S (T Int)
+	-- Here, T is partially applied, so it's illegal in H98.
+	-- But if you expand S first, then T we get just 
+	--	       f :: Int
+	-- which is fine.
+		returnM ()
+	  else
+		-- For H98, do check the type args
+		mappM_ check_arg_type tys
+	}
     
   | isUnboxedTupleTyCon tc
   = doptM Opt_GlasgowExts			`thenM` \ gla_exts ->
@@ -872,11 +868,6 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   where
     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 
-    syn_arity_ok = tc_arity <= n_args
-		-- It's OK to have an *over-applied* type synonym
-		--	data Tree a b = ...
-		--	type Foo a = Tree [a]
-		--	f :: Foo a b -> ...
     n_args    = length tys
     tc_arity  = tyConArity tc
 
diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs
index 904e34b..0660a68 100644
--- a/ghc/compiler/typecheck/TcSimplify.lhs
+++ b/ghc/compiler/typecheck/TcSimplify.lhs
@@ -1712,7 +1712,7 @@ reduceList (n,stack) try_me wanteds state
 #ifdef DEBUG
    (if n > 8 then
 	pprTrace "Interesting! Context reduction stack deeper than 8:" 
-		 (nest 2 (pprStack stack))
+		(int n $$ ifPprDebug (nest 2 (pprStack stack)))
     else (\x->x))
 #endif
     go wanteds state
diff --git a/ghc/compiler/typecheck/TcTyDecls.lhs b/ghc/compiler/typecheck/TcTyDecls.lhs
index 590ac2c..7e390b4 100644
--- a/ghc/compiler/typecheck/TcTyDecls.lhs
+++ b/ghc/compiler/typecheck/TcTyDecls.lhs
@@ -22,7 +22,7 @@ module TcTyDecls(
 import TypeRep          ( Type(..), TyNote(..), PredType(..) )  -- friend
 import HsSyn		( TyClDecl(..), HsPred(..), LTyClDecl, isClassDecl )
 import RnHsSyn		( extractHsTyNames )
-import Type		( predTypeRep )
+import Type		( predTypeRep, tcView )
 import HscTypes		( TyThing(..), ModDetails(..) )
 import TyCon            ( TyCon, ArgVrcs, tyConArity, tyConDataCons, tyConTyVars,
                           getSynTyConDefn, isSynTyCon, isAlgTyCon, 
@@ -94,19 +94,14 @@ synTyConsOfType ty
   where
      go :: Type -> NameEnv TyCon  -- The NameEnv does duplicate elim
      go (TyVarTy v)	  	  = emptyNameEnv
-     go (TyConApp tc tys) 	  = go_tc tc tys	-- See note (a)
+     go (TyConApp tc tys) 	  = go_tc tc tys
      go (AppTy a b)	  	  = go a `plusNameEnv` go b
      go (FunTy a b)	  	  = go a `plusNameEnv` go b
      go (PredTy (IParam _ ty))    = go ty	
      go (PredTy (ClassP cls tys)) = go_s tys	-- Ignore class
-     go (NoteTy (SynNote ty) _)	  = go ty	-- Don't look through it!
-     go (NoteTy other ty)	  = go ty	
+     go (NoteTy _ ty)		  = go ty	
      go (ForAllTy _ ty)	  	  = go ty
 
-	-- Note (a): the unexpanded branch of a SynNote has a
-	--	     TyConApp for the synonym, so the tc of
-	--	     a TyConApp must be tested for possible synonyms
-
      go_tc tc tys | isSynTyCon tc = extendNameEnv (go_s tys) (tyConName tc) tc
 		  | otherwise	  = go_s tys
      go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
@@ -313,14 +308,14 @@ tcTyConsOfType ty
   = nameEnvElts (go ty)
   where
      go :: Type -> NameEnv TyCon  -- The NameEnv does duplicate elim
-     go (TyVarTy v)	  	  = emptyNameEnv
-     go (TyConApp tc tys) 	  = go_tc tc tys
-     go (AppTy a b)	  	  = go a `plusNameEnv` go b
-     go (FunTy a b)	  	  = go a `plusNameEnv` go b
-     go (PredTy (IParam _ ty))    = go ty
-     go (PredTy (ClassP cls tys)) = go_tc (classTyCon cls) tys
-     go (NoteTy _ ty)		  = go ty
-     go (ForAllTy _ ty)	  	  = go ty
+     go ty | Just ty' <- tcView ty = go ty'
+     go (TyVarTy v)	  	   = emptyNameEnv
+     go (TyConApp tc tys) 	   = go_tc tc tys
+     go (AppTy a b)	  	   = go a `plusNameEnv` go b
+     go (FunTy a b)	  	   = go a `plusNameEnv` go b
+     go (PredTy (IParam _ ty))     = go ty
+     go (PredTy (ClassP cls tys))  = go_tc (classTyCon cls) tys
+     go (ForAllTy _ ty)	  	   = go ty
 
      go_tc tc tys = extendNameEnv (go_s tys) (tyConName tc) tc
      go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
@@ -422,10 +417,6 @@ vrcInTy :: (TyCon -> ArgVrcs)  -- function to get argVrcs of a tycon (break out
         -> Type                -- type to check for occ in
         -> (Bool,Bool)         -- (occurs positively, occurs negatively)
 
-vrcInTy fao v (NoteTy (SynNote _)   ty) = vrcInTy fao v ty
-    			-- SynTyCon doesn't neccessarily have vrcInfo at this point,
-    			-- so don't try and use it
-
 vrcInTy fao v (NoteTy (FTVNote ftv) ty) = if elemVarSet v ftv
     					  then vrcInTy fao v ty
     					  else (False,False)
diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index 08d122c..ca9cab6 100644
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -34,6 +34,7 @@ module TcType (
   --------------------------------
   -- Splitters  
   -- These are important because they do not look through newtypes
+  tcView,
   tcSplitForAllTys, tcSplitPhiTy, 
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
@@ -119,7 +120,7 @@ module TcType (
 #include "HsVersions.h"
 
 -- friends:
-import TypeRep		( Type(..), TyNote(..), funTyCon )  -- friend
+import TypeRep		( Type(..), funTyCon )  -- friend
 
 import Type		(	-- Re-exports
 			  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
@@ -140,7 +141,7 @@ import Type		(	-- Re-exports
 			  tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
 			  tidyTyVarBndr, tidyOpenTyVar,
 			  tidyOpenTyVars, tidyKind,
-			  isSubKind, deShadowTy,
+			  isSubKind, deShadowTy, tcView,
 
 			  tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
 			  tcEqPred, tcCmpPred, tcEqTypeX, 
@@ -409,22 +410,22 @@ mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
 
 \begin{code}
 isTauTy :: Type -> Bool
+isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
 isTauTy (TyVarTy v)	 = True
 isTauTy (TyConApp _ tys) = all isTauTy tys
 isTauTy (AppTy a b)	 = isTauTy a && isTauTy b
 isTauTy (FunTy a b)	 = isTauTy a && isTauTy b
 isTauTy (PredTy p)	 = True		-- Don't look through source types
-isTauTy (NoteTy _ ty)	 = isTauTy ty
 isTauTy other		 = False
 \end{code}
 
 \begin{code}
 getDFunTyKey :: Type -> OccName	-- Get some string from a type, to be used to 
 				-- construct a dictionary function name
+getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
 getDFunTyKey (TyVarTy tv)    = getOccName tv
 getDFunTyKey (TyConApp tc _) = getOccName tc
 getDFunTyKey (AppTy fun _)   = getDFunTyKey fun
-getDFunTyKey (NoteTy _ t)    = getDFunTyKey t
 getDFunTyKey (FunTy arg _)   = getOccName funTyCon
 getDFunTyKey (ForAllTy _ t)  = getDFunTyKey t
 getDFunTyKey ty		     = pprPanic "getDFunTyKey" (pprType ty)
@@ -450,21 +451,21 @@ variables.  It's up to you to make sure this doesn't matter.
 tcSplitForAllTys :: Type -> ([TyVar], Type)
 tcSplitForAllTys ty = split ty ty []
    where
+     split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
      split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
-     split orig_ty (NoteTy n  ty)   tvs = split orig_ty ty tvs
      split orig_ty t		    tvs = (reverse tvs, orig_ty)
 
+tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
 tcIsForAllTy (ForAllTy tv ty) = True
-tcIsForAllTy (NoteTy n ty)    = tcIsForAllTy ty
 tcIsForAllTy t		      = False
 
 tcSplitPhiTy :: Type -> ([PredType], Type)
 tcSplitPhiTy ty = split ty ty []
  where
+  split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
   split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
 					Just p  -> split res res (p:ts)
 					Nothing -> (reverse ts, orig_ty)
-  split orig_ty (NoteTy n ty)	ts = split orig_ty ty ts
   split orig_ty ty		ts = (reverse ts, orig_ty)
 
 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
@@ -483,26 +484,24 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
 			Nothing	   -> pprPanic "tcSplitTyConApp" (pprType ty)
 
 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 tcSplitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
-tcSplitTyConApp_maybe (NoteTy n ty)     = tcSplitTyConApp_maybe ty
 	-- Newtypes are opaque, so they may be split
 	-- However, predicates are not treated
 	-- as tycon applications by the type checker
-tcSplitTyConApp_maybe other	        	= Nothing
+tcSplitTyConApp_maybe other	      	= Nothing
 
 tcValidInstHeadTy :: Type -> Bool
 -- Used in Haskell-98 mode, for the argument types of an instance head
 -- These must not be type synonyms, but everywhere else type synonyms
 -- are transparent, so we need a special function here
-tcValidInstHeadTy ty 
+tcValidInstHeadTy ty
   = case ty of
-	TyConApp tc tys -> ASSERT( not (isSynTyCon tc) ) ok tys
-			   -- A synonym would be a NoteTy
-	FunTy arg res        -> ok [arg, res]
-	NoteTy (SynNote _) _ -> False
-	NoteTy other_note ty -> tcValidInstHeadTy ty
-	other		     -> False
+	NoteTy _ ty     -> tcValidInstHeadTy ty
+	TyConApp tc tys -> not (isSynTyCon tc) && ok tys
+	FunTy arg res   -> ok [arg, res]
+	other		-> False
   where
 	-- Check that all the types are type variables,
 	-- and that each is distinct
@@ -510,10 +509,9 @@ tcValidInstHeadTy ty
 	   where
 	     tvs = mapCatMaybes get_tv tys
 
-    get_tv (TyVarTy tv) 	  = Just tv	  -- Again, do not look
-    get_tv (NoteTy (SynNote _) _) = Nothing  	-- through synonyms
-    get_tv (NoteTy other_note ty) = get_tv ty
-    get_tv other  		  = Nothing
+    get_tv (NoteTy _ ty) = get_tv ty 	-- through synonyms
+    get_tv (TyVarTy tv)  = Just tv	-- Again, do not look
+    get_tv other  	 = Nothing
 
 tcSplitFunTys :: Type -> ([Type], Type)
 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
@@ -523,8 +521,8 @@ tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
 					  (args,res') = tcSplitFunTys res
 
 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
+tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
 tcSplitFunTy_maybe (FunTy arg res)  = Just (arg, res)
-tcSplitFunTy_maybe (NoteTy n ty)    = tcSplitFunTy_maybe ty
 tcSplitFunTy_maybe other	    = Nothing
 
 tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
@@ -532,9 +530,9 @@ tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
 
 
 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
+tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
 tcSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 tcSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
-tcSplitAppTy_maybe (NoteTy n ty)     = tcSplitAppTy_maybe ty
 tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
 					Just (tys', ty') -> Just (TyConApp tc tys', ty')
 					Nothing		 -> Nothing
@@ -553,8 +551,8 @@ tcSplitAppTys ty
 		   Nothing	   -> (ty,args)
 
 tcGetTyVar_maybe :: Type -> Maybe TyVar
+tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
 tcGetTyVar_maybe (TyVarTy tv) 	= Just tv
-tcGetTyVar_maybe (NoteTy _ t) 	= tcGetTyVar_maybe t
 tcGetTyVar_maybe other	        = Nothing
 
 tcGetTyVar :: String -> Type -> TyVar
@@ -587,7 +585,7 @@ tcSplitDFunHead tau
 \begin{code}
 tcSplitPredTy_maybe :: Type -> Maybe PredType
    -- Returns Just for predicates only
-tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
+tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty'
 tcSplitPredTy_maybe (PredTy p)    = Just p
 tcSplitPredTy_maybe other	  = Nothing
 	
@@ -624,8 +622,8 @@ mkDictTy :: Class -> [Type] -> Type
 mkDictTy clas tys = mkPredTy (ClassP clas tys)
 
 isDictTy :: Type -> Bool
+isDictTy ty | Just ty' <- tcView ty = isDictTy ty'
 isDictTy (PredTy p)   = isClassPred p
-isDictTy (NoteTy _ ty)	= isDictTy ty
 isDictTy other		= False
 \end{code}
 
@@ -687,20 +685,20 @@ any foralls.  E.g.
 
 \begin{code}
 isSigmaTy :: Type -> Bool
+isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
 isSigmaTy (ForAllTy tyvar ty) = True
 isSigmaTy (FunTy a b)	      = isPredTy a
-isSigmaTy (NoteTy n ty)	      = isSigmaTy ty
 isSigmaTy _		      = False
 
 isOverloadedTy :: Type -> Bool
+isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
 isOverloadedTy (FunTy a b)	   = isPredTy a
-isOverloadedTy (NoteTy n ty)	   = isOverloadedTy ty
 isOverloadedTy _		   = False
 
 isPredTy :: Type -> Bool	-- Belongs in TcType because it does 
 				-- not look through newtypes, or predtypes (of course)
-isPredTy (NoteTy _ ty) = isPredTy ty
+isPredTy ty | Just ty' <- tcView ty = isPredTy ty'
 isPredTy (PredTy sty)  = True
 isPredTy _	       = False
 \end{code}
@@ -753,28 +751,30 @@ tied.)
 \begin{code}
 hoistForAllTys :: Type -> Type
 hoistForAllTys ty
-  = go (deShadowTy ty)
-	-- Running over ty with an empty substitution gives it the
-	-- no-shadowing property.  This is important.  For example:
-	--	type Foo r = forall a. a -> r
-	--	foo :: Foo (Foo ())
-	-- Here the hoisting should give
-	--	foo :: forall a a1. a -> a1 -> ()
-	--
-	-- What about type vars that are lexically in scope in the envt?
-	-- We simply rely on them having a different unique to any
-	-- binder in 'ty'.  Otherwise we'd have to slurp the in-scope-tyvars
-	-- out of the envt, which is boring and (I think) not necessary.
+  = go ty
 
   where
-    go (TyVarTy tv)   		   = TyVarTy tv
-    go (TyConApp tc tys)	   = TyConApp tc (map go tys)
-    go (PredTy pred)  		   = PredTy pred    -- No nested foralls 
-    go (NoteTy (SynNote ty1) ty2)  = NoteTy (SynNote (go ty1)) (go ty2)
-    go (NoteTy (FTVNote _) ty2)    = go ty2	    -- Discard the free tyvar note
-    go (FunTy arg res)   	   = mk_fun_ty (go arg) (go res)
-    go (AppTy fun arg)   	   = AppTy (go fun) (go arg)
-    go (ForAllTy tv ty)		   = ForAllTy tv (go ty)
+    go	:: Type -> Type
+
+    go (TyVarTy tv)   	 = TyVarTy tv
+    go ty@(TyConApp tc tys) 
+	| isSynTyCon tc, any isSigmaTy tys'
+	= go (expectJust "hoistForAllTys" (tcView ty))
+		-- Revolting special case.  If a type synonym has foralls
+		-- at the top of its argument, then expanding the type synonym
+		-- might lead to more hositing.  So we just abandon the synonym
+		-- altogether right here.
+		-- Note that we must go back to hoistForAllTys, because
+		-- expanding the type synonym may expose new binders. Yuk.
+	| otherwise
+	= TyConApp tc tys'
+	where
+	  tys' = map go tys
+    go (PredTy pred)     = PredTy pred	-- No nested foralls 
+    go (NoteTy _ ty2)    = go ty2	-- Discard the free tyvar note
+    go (FunTy arg res)   = mk_fun_ty (go arg) (go res)
+    go (AppTy fun arg)   = AppTy (go fun) (go arg)
+    go (ForAllTy tv ty)  = ForAllTy tv (go ty)
 
  	-- mk_fun_ty does all the work.  
 	-- It's building t1 -> t2: 
@@ -784,14 +784,25 @@ hoistForAllTys ty
 	| not (isSigmaTy ty2)	 	-- No forall's, or context => 
 	= FunTy ty1 ty2 	
 	| PredTy p1 <- ty1		-- ty1 is a predicate
-	= if p1 `elem` theta then 	-- so check for duplicates
+	= if p1 `elem` theta2 then 	-- so check for duplicates
 		ty2
 	  else
-		mkSigmaTy tvs (p1:theta) tau
+		mkSigmaTy tvs2 (p1:theta2) tau2
 	| otherwise 	
-	= mkSigmaTy tvs theta (FunTy ty1 tau)
+	= mkSigmaTy tvs2 theta2 (FunTy ty1 tau2)
 	where
-	  (tvs, theta, tau) = tcSplitSigmaTy ty2
+	  (tvs2, theta2, tau2) = tcSplitSigmaTy $
+				 deShadowTy (tyVarsOfType ty1) $
+				 deNoteType ty2
+
+	-- deShadowTy is important.  For example:
+	--	type Foo r = forall a. a -> r
+	--	foo :: Foo (Foo ())
+	-- Here the hoisting should give
+	--	foo :: forall a a1. a -> a1 -> ()
+
+	-- deNoteType is important too, so that the deShadow sees that
+	-- synonym expanded!  Sigh
 \end{code}
 
 
@@ -804,8 +815,8 @@ hoistForAllTys ty
 \begin{code}
 deNoteType :: Type -> Type
 -- Remove *outermost* type synonyms and other notes
-deNoteType (NoteTy _ ty) = deNoteType ty
-deNoteType ty		 = ty
+deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
+deNoteType ty = ty
 \end{code}
 
 Find the free tycons and classes of a type.  This is used in the front
@@ -815,8 +826,7 @@ end of the compiler.
 tyClsNamesOfType :: Type -> NameSet
 tyClsNamesOfType (TyVarTy tv)		    = emptyNameSet
 tyClsNamesOfType (TyConApp tycon tys)	    = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
-tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
-tyClsNamesOfType (NoteTy other_note    ty2) = tyClsNamesOfType ty2
+tyClsNamesOfType (NoteTy _ ty2) 	    = tyClsNamesOfType ty2
 tyClsNamesOfType (PredTy (IParam n ty))     = tyClsNamesOfType ty
 tyClsNamesOfType (PredTy (ClassP cl tys))   = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
 tyClsNamesOfType (FunTy arg res)	    = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs
index 97487ce..f56c74d 100644
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/ghc/compiler/typecheck/TcUnify.lhs
@@ -30,18 +30,18 @@ import HsSyn		( HsExpr(..) , MatchGroup(..), HsMatchContext(..),
 			  hsLMatchPats, pprMatches, pprMatchContext )
 import TcHsSyn		( mkHsDictLet, mkHsDictLam,
 			  ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
-import TypeRep		( Type(..), PredType(..), TyNote(..) )
+import TypeRep		( Type(..), PredType(..) )
 
 import TcRnMonad         -- TcType, amongst others
 import TcType		( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
 			  TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),
 			  SkolemInfo( GenSkol ), MetaDetails(..), 
 			  pprTcTyVar, isTauTy, isSigmaTy, mkFunTy, mkFunTys, mkTyConApp,
-			  tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcEqType,
+			  tcSplitAppTy_maybe, tcEqType,
 			  tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, isMetaTyVar,
 			  typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
 			  tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
-			  pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar )
+			  pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, tcView )
 import Kind		( Kind(..), SimpleKind, KindVar, isArgTypeKind,
 			  openTypeKind, liftedTypeKind, mkArrowKind, 
 			  isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
@@ -54,7 +54,8 @@ import TcMType		( condLookupTcTyVar, LookupTyVarResult(..),
 import TcSimplify	( tcSimplifyCheck )
 import TcIface		( checkWiredInTyCon )
 import TcEnv		( tcGetGlobalTyVars, findGlobals )
-import TyCon		( TyCon, tyConArity, tyConTyVars, isFunTyCon )
+import TyCon		( TyCon, tyConArity, tyConTyVars, isFunTyCon, isSynTyCon,
+			  getSynTyConDefn )
 import TysWiredIn	( listTyCon )
 import Id		( Id, mkSysLocal )
 import Var		( Var, varName, tyVarKind )
@@ -245,8 +246,9 @@ unify_fun_ty use_refinement arity ty
   = do	{ res_ty <- wobblify use_refinement ty
 	; return (True, [], ty) }
 
-unify_fun_ty use_refinement arity (NoteTy _ ty)
-  = unify_fun_ty use_refinement arity ty
+unify_fun_ty use_refinement arity ty
+  | Just ty' <- tcView ty
+  = unify_fun_ty use_refinement arity ty'
 
 unify_fun_ty use_refinement arity ty@(TyVarTy tv)
   = do	{ details <- condLookupTcTyVar use_refinement tv
@@ -323,8 +325,9 @@ unifyListTy exp_ty = do	{ [elt_ty] <- unifyTyConApp listTyCon exp_ty
 			; return elt_ty }
 
 ----------
-unify_tc_app n_args use_refinement tc (NoteTy _ ty)
-  = unify_tc_app n_args use_refinement tc ty
+unify_tc_app n_args use_refinement tc ty
+  | Just ty' <- tcView ty
+  = unify_tc_app n_args use_refinement tc ty'
 
 unify_tc_app n_args use_refinement tc (TyConApp tycon arg_tys)
   | tycon == tc
@@ -363,7 +366,8 @@ unifyAppTy :: TcType			-- Type to split: m a
 
 unifyAppTy ty = unify_app_ty True ty
 
-unify_app_ty use (NoteTy _ ty) = unify_app_ty use ty
+unify_app_ty use ty
+  | Just ty' <- tcView ty = unify_app_ty use ty'
 
 unify_app_ty use ty@(TyVarTy tyvar)
   = do	{ details <- condLookupTcTyVar use tyvar
@@ -513,8 +517,10 @@ tc_sub :: TcSigmaType		-- expected_ty, before expanding synonyms
 
 -----------------------------------
 -- Expand synonyms
-tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
-tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
+tc_sub exp_sty exp_ty act_sty act_ty 
+  | Just exp_ty' <- tcView exp_ty = tc_sub exp_sty exp_ty' act_sty act_ty
+tc_sub exp_sty exp_ty act_sty act_ty
+  | Just act_ty' <- tcView act_ty = tc_sub exp_sty exp_ty act_sty act_ty'
 
 -----------------------------------
 -- Generalisation case
@@ -784,8 +790,10 @@ uTys :: Bool                    -- Allow refinements to ty1
 
 	-- Always expand synonyms (see notes at end)
         -- (this also throws away FTVs)
-uTys r1 ps_ty1 (NoteTy n1 ty1) r2 ps_ty2 ty2 = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
-uTys r1 ps_ty1 ty1 r2 ps_ty2 (NoteTy n2 ty2) = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
+uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2 
+  | Just ty1' <- tcView ty1 = uTys r1 ps_ty1 ty1' r2 ps_ty2 ty2
+uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
+  | Just ty2' <- tcView ty2 = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2'
 
 	-- Variables; go for uVar
 uTys r1 ps_ty1 (TyVarTy tyvar1) r2 ps_ty2 ty2 = uVar False r1 tyvar1 r2 ps_ty2 ty2
@@ -931,9 +939,10 @@ uDoneVar :: Bool 			-- Args are swapped
      	 -> TcM ()
 -- Invariant: tyvar 1 is not unified with anything
 
-uDoneVar swapped tv1 details1 r2 ps_ty2 (NoteTy n2 ty2)
+uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
+  | Just ty2' <- tcView ty2
   = 	-- Expand synonyms; ignore FTVs
-    uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
+    uDoneVar swapped tv1 details1 r2 ps_ty2 ty2'
 
 uDoneVar swapped tv1 details1 r2 ps_ty2 ty2@(TyVarTy tv2)
 	-- Same type variable => no-op
@@ -1084,21 +1093,22 @@ okToUnifyWith tv ty
   where
     ok (TyVarTy tv') | tv == tv' = Just OccurCheck
 		     | otherwise = Nothing
-    ok (AppTy t1 t2)   		= ok t1 `and` ok t2
-    ok (FunTy t1 t2)   		= ok t1 `and` ok t2
-    ok (TyConApp _ ts) 		= oks ts
-    ok (ForAllTy _ _)  		= Just NotMonoType
-    ok (PredTy st)   		= ok_st st
-    ok (NoteTy (FTVNote _) t)   = ok t
-    ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
-		-- Type variables may be free in t1 but not t2
-		-- A forall may be in t2 but not t1
+    ok (AppTy t1 t2)   	= ok t1 `and` ok t2
+    ok (FunTy t1 t2)   	= ok t1 `and` ok t2
+    ok (TyConApp tc ts) = oks ts `and` ok_syn tc
+    ok (ForAllTy _ _)  	= Just NotMonoType
+    ok (PredTy st)   	= ok_st st
+    ok (NoteTy _ t)     = ok t
 
     oks ts = foldr (and . ok) Nothing ts
 
     ok_st (ClassP _ ts) = oks ts
     ok_st (IParam _ t)  = ok t
 
+	-- Check that a type synonym doesn't have a forall in the RHS
+    ok_syn tc | not (isSynTyCon tc) = Nothing
+	      | otherwise = ok (snd (getSynTyConDefn tc))
+
     Nothing `and` m = m
     Just p  `and` m = Just p
 \end{code}
diff --git a/ghc/compiler/types/TyCon.lhs b/ghc/compiler/types/TyCon.lhs
index 3c1f923..9dbc8a4 100644
--- a/ghc/compiler/types/TyCon.lhs
+++ b/ghc/compiler/types/TyCon.lhs
@@ -16,7 +16,10 @@ module TyCon(
 	isAlgTyCon, isDataTyCon, isSynTyCon, isNewTyCon, isPrimTyCon,
 	isEnumerationTyCon, 
 	isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, tupleTyConBoxity,
-	isRecursiveTyCon, newTyConRep, newTyConRhs, newTyConRhs_maybe, isHiBootTyCon,
+	isRecursiveTyCon, newTyConRep, newTyConRhs, 
+	isHiBootTyCon,
+
+	tcExpandTyCon_maybe, coreExpandTyCon_maybe,
 
 	makeTyConAbstract, isAbstractTyCon,
 
@@ -65,7 +68,6 @@ import BasicTypes	( Arity, RecFlag(..), Boxity(..), isBoxed )
 import Name		( Name, nameUnique, NamedThing(getName) )
 import PrelNames	( Unique, Uniquable(..) )
 import Maybes		( orElse )
-import Util		( equalLength )
 import Outputable
 import FastString
 \end{code}
@@ -150,7 +152,7 @@ data TyCon
 	tyConArity  :: Arity,
 
 	tyConTyVars     :: [TyVar],	-- Bound tyvars
-	synTyConDefn    :: Type,	-- Right-hand side, mentioning these type vars.
+	synTcRhs    :: Type,	-- Right-hand side, mentioning these type vars.
 					-- Acts as a template for the expansion when
 					-- the tycon is applied to some types.
 	argVrcs :: ArgVrcs
@@ -167,40 +169,79 @@ data AlgTyConRhs
 			-- Used when we export a data type abstractly into
 			-- an hi file
 
-  | DataTyCon 
-	[DataCon]	-- The constructors; can be empty if the user declares
+  | DataTyCon {
+	data_cons :: [DataCon],
+			-- The constructors; can be empty if the user declares
 			--   the type to have no constructors
 			-- INVARIANT: Kept in order of increasing tag
 			--	      (see the tag assignment in DataCon.mkDataCon)
-	Bool		-- Cached: True <=> an enumeration type
-			--	   Includes data types with no constructors.
+	is_enum :: Bool 	-- Cached: True <=> an enumeration type
+    }			--	   Includes data types with no constructors.
+
+  | NewTyCon {
+	data_con :: DataCon,	-- The unique constructor; it has no existentials
 
-  | NewTyCon 		-- Newtypes always have exactly one constructor
-	DataCon		-- The unique constructor; it has no existentials
-	Type		-- Cached: the argument type of the constructor
-			--  = the representation type of the tycon
+	nt_rhs :: Type,		-- Cached: the argument type of the constructor
+				--  = the representation type of the tycon
 
-	Type		-- Cached: the *ultimate* representation type
-			-- By 'ultimate' I mean that the rep type is not itself
-			-- a newtype or type synonym.
+	nt_etad_rhs :: ([TyVar], Type) ,
+			-- The same again, but this time eta-reduced
+			-- hence the [TyVar] which may be shorter than the declared 
+			-- arity of the TyCon.  See Note [Newtype eta]
+
+	nt_rep :: Type	-- Cached: the *ultimate* representation type
+			-- By 'ultimate' I mean that the top-level constructor
+			-- of the rep type is not itself a newtype or type synonym.
 			-- The rep type isn't entirely simple:
 			--  for a recursive newtype we pick () as the rep type
 			--	newtype T = MkT T
-			--
-			-- The rep type has free type variables the tyConTyVars
+			-- 
+			-- This one does not need to be eta reduced; hence its
+			-- free type variables are conveniently tyConTyVars
 			-- Thus:
 			-- 	newtype T a = MkT [(a,Int)]
 			-- The rep type is [(a,Int)]
-	-- NB: the rep type isn't necessarily the original RHS of the
-	--     newtype decl, because the rep type looks through other
-	--     newtypes.
+			-- NB: the rep type isn't necessarily the original RHS of the
+			--     newtype decl, because the rep type looks through other
+    }			--     newtypes.
 
 visibleDataCons :: AlgTyConRhs -> [DataCon]
-visibleDataCons AbstractTyCon    = []
-visibleDataCons (DataTyCon cs _) = cs
-visibleDataCons (NewTyCon c _ _) = [c]
+visibleDataCons AbstractTyCon      	      = []
+visibleDataCons (DataTyCon{ data_cons = cs }) = cs
+visibleDataCons (NewTyCon{ data_con = c })    = [c]
 \end{code}
 
+Note [Newtype eta]
+~~~~~~~~~~~~~~~~~~
+Consider
+	newtype Parser m a = MkParser (Foogle m a)
+Are these two types equal (to Core)?
+	Monad (Parser m) 
+	Monad (Foogle m)
+Well, yes.  But to see that easily we eta-reduce the RHS type of
+Parser, in this case to ([], Froogle), so that even unsaturated applications
+of Parser will work right.  This eta reduction is done when the type 
+constructor is built, and cached in NewTyCon.  The cached field is
+only used in coreExpandTyCon_maybe.
+ 
+Here's an example that I think showed up in practice
+Source code:
+	newtype T a = MkT [a]
+	newtype Foo m = MkFoo (forall a. m a -> Int)
+
+	w1 :: Foo []
+	w1 = ...
+	
+	w2 :: Foo T
+	w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
+
+After desugaring, and discading the data constructors for the newtypes,
+we get:
+	w2 :: Foo T
+	w2 = w1
+And now Lint complains unless Foo T == Foo [], and that requires T==[]
+
+
 %************************************************************************
 %*									*
 \subsection{PrimRep}
@@ -352,7 +393,7 @@ mkSynTyCon name kind tyvars rhs argvrcs
 	tyConKind = kind,
 	tyConArity = length tyvars,
 	tyConTyVars = tyvars,
-	synTyConDefn = rhs,
+	synTcRhs = rhs,
 	argVrcs      = argvrcs
     }
 \end{code}
@@ -395,16 +436,16 @@ isDataTyCon :: TyCon -> Bool
 --		  unboxed tuples
 isDataTyCon tc@(AlgTyCon {algTcRhs = rhs})  
   = case rhs of
-	DataTyCon _ _  -> True
-	NewTyCon _ _ _ -> False
-	AbstractTyCon  -> pprPanic "isDataTyCon" (ppr tc)
+	DataTyCon {}  -> True
+	NewTyCon {}   -> False
+	AbstractTyCon -> pprPanic "isDataTyCon" (ppr tc)
 
 isDataTyCon (TupleTyCon {tyConBoxed = boxity}) = isBoxed boxity
 isDataTyCon other = False
 
 isNewTyCon :: TyCon -> Bool
-isNewTyCon (AlgTyCon {algTcRhs = NewTyCon _ _ _}) = True 
-isNewTyCon other			          = False
+isNewTyCon (AlgTyCon {algTcRhs = NewTyCon {}}) = True 
+isNewTyCon other			       = False
 
 isProductTyCon :: TyCon -> Bool
 -- A "product" tycon
@@ -415,9 +456,10 @@ isProductTyCon :: TyCon -> Bool
 -- 	may be  unboxed or not, 
 --	may be  recursive or not
 isProductTyCon tc@(AlgTyCon {}) = case algTcRhs tc of
-				    DataTyCon [data_con] _ -> isVanillaDataCon data_con
-				    NewTyCon _ _ _         -> True
-				    other		   -> False
+				    DataTyCon{ data_cons = [data_con] } 
+						-> isVanillaDataCon data_con
+				    NewTyCon {}	-> True
+				    other	-> False
 isProductTyCon (TupleTyCon {})  = True   
 isProductTyCon other		= False
 
@@ -426,8 +468,8 @@ isSynTyCon (SynTyCon {}) = True
 isSynTyCon _		 = False
 
 isEnumerationTyCon :: TyCon -> Bool
-isEnumerationTyCon (AlgTyCon {algTcRhs = DataTyCon _ is_enum}) = is_enum
-isEnumerationTyCon other				       = False
+isEnumerationTyCon (AlgTyCon {algTcRhs = DataTyCon { is_enum = res }}) = res
+isEnumerationTyCon other				       	       = False
 
 isTupleTyCon :: TyCon -> Bool
 -- The unit tycon didn't used to be classed as a tuple tycon
@@ -466,6 +508,47 @@ isForeignTyCon (PrimTyCon {tyConExtName = Just _}) = True
 isForeignTyCon other				   = False
 \end{code}
 
+
+-----------------------------------------------
+--	Expand type-constructor applications
+-----------------------------------------------
+
+\begin{code}
+tcExpandTyCon_maybe, coreExpandTyCon_maybe 
+	:: TyCon 
+	-> [Type]			-- Args to tycon
+	-> Maybe ([(TyVar,Type)], 	-- Substitution
+		  Type,			-- Body type (not yet substituted)
+		  [Type])		-- Leftover args
+
+-- For the *typechecker* view, we expand synonyms only
+tcExpandTyCon_maybe (SynTyCon {tyConTyVars = tvs, synTcRhs = rhs }) tys
+   = expand tvs rhs tys
+tcExpandTyCon_maybe other_tycon tys = Nothing
+
+---------------
+-- For the *Core* view, we expand synonyms *and* non-recursive newtypes
+coreExpandTyCon_maybe (AlgTyCon {algTcRec = NonRecursive,	-- Not recursive
+         algTcRhs = NewTyCon { nt_etad_rhs = etad_rhs }}) tys
+   = case etad_rhs of	-- Don't do this in the pattern match, lest we accidentally
+			-- match the etad_rhs of a *recursive* newtype
+	(tvs,rhs) -> expand tvs rhs tys
+	
+coreExpandTyCon_maybe tycon tys = tcExpandTyCon_maybe tycon tys
+
+----------------
+expand	:: [TyVar] -> Type 			-- Template
+	-> [Type]				-- Args
+	-> Maybe ([(TyVar,Type)], Type, [Type])	-- Expansion
+expand tvs rhs tys
+  = case n_tvs `compare` length tys of
+	LT -> Just (tvs `zip` tys, rhs, drop n_tvs tys)
+	EQ -> Just (tvs `zip` tys, rhs, [])
+	GT -> Nothing
+   where
+     n_tvs = length tvs
+\end{code}
+
 \begin{code}
 tyConHasGenerics :: TyCon -> Bool
 tyConHasGenerics (AlgTyCon {hasGenerics = hg})   = hg
@@ -478,15 +561,15 @@ tyConDataCons :: TyCon -> [DataCon]
 tyConDataCons tycon = tyConDataCons_maybe tycon `orElse` []
 
 tyConDataCons_maybe :: TyCon -> Maybe [DataCon]
-tyConDataCons_maybe (AlgTyCon {algTcRhs = DataTyCon cons _}) = Just cons
-tyConDataCons_maybe (AlgTyCon {algTcRhs = NewTyCon con _ _}) = Just [con]
-tyConDataCons_maybe (TupleTyCon {dataCon = con})	     = Just [con]
-tyConDataCons_maybe other			             = Nothing
+tyConDataCons_maybe (AlgTyCon {algTcRhs = DataTyCon { data_cons = cons }}) = Just cons
+tyConDataCons_maybe (AlgTyCon {algTcRhs = NewTyCon { data_con = con }})    = Just [con]
+tyConDataCons_maybe (TupleTyCon {dataCon = con})	       		   = Just [con]
+tyConDataCons_maybe other			               		   = Nothing
 
 tyConFamilySize  :: TyCon -> Int
-tyConFamilySize (AlgTyCon {algTcRhs = DataTyCon cons _}) = length cons
-tyConFamilySize (AlgTyCon {algTcRhs = NewTyCon _ _ _})   = 1
-tyConFamilySize (TupleTyCon {})	 			 = 1
+tyConFamilySize (AlgTyCon {algTcRhs = DataTyCon { data_cons = cons }}) = length cons
+tyConFamilySize (AlgTyCon {algTcRhs = NewTyCon {}}) = 1
+tyConFamilySize (TupleTyCon {})	 		    = 1
 #ifdef DEBUG
 tyConFamilySize other = pprPanic "tyConFamilySize:" (ppr other)
 #endif
@@ -497,33 +580,17 @@ tyConSelIds other_tycon		          = []
 
 algTyConRhs :: TyCon -> AlgTyConRhs
 algTyConRhs (AlgTyCon {algTcRhs = rhs})  = rhs
-algTyConRhs (TupleTyCon {dataCon = con}) = DataTyCon [con] False
+algTyConRhs (TupleTyCon {dataCon = con}) = DataTyCon { data_cons = [con], is_enum = False }
 algTyConRhs other = pprPanic "algTyConRhs" (ppr other)
 \end{code}
 
 \begin{code}
 newTyConRhs :: TyCon -> ([TyVar], Type)
-newTyConRhs (AlgTyCon {tyConTyVars = tvs, algTcRhs = NewTyCon _ rhs _}) = (tvs, rhs)
+newTyConRhs (AlgTyCon {tyConTyVars = tvs, algTcRhs = NewTyCon { nt_rhs = rhs }}) = (tvs, rhs)
 newTyConRhs tycon = pprPanic "newTyConRhs" (ppr tycon)
 
-newTyConRhs_maybe :: TyCon 
-		  -> [Type]			-- Args to tycon
-		  -> Maybe ([(TyVar,Type)], 	-- Substitution
-			    Type)		-- Body type (not yet substituted)
--- Non-recursive newtypes are transparent to Core; 
--- Given an application to some types, return Just (tenv, ty)
--- if it's a saturated, non-recursive newtype.
-newTyConRhs_maybe (AlgTyCon {tyConTyVars = tvs, 
-			     algTcRec = NonRecursive,	-- Not recursive
-			     algTcRhs = NewTyCon _ rhs _}) tys
-   | tvs `equalLength` tys 	-- Saturated
-   = Just (tvs `zip` tys, rhs)
-	
-newTyConRhs_maybe other_tycon tys = Nothing
-
-
 newTyConRep :: TyCon -> ([TyVar], Type)
-newTyConRep (AlgTyCon {tyConTyVars = tvs, algTcRhs = NewTyCon _ _ rep}) = (tvs, rep)
+newTyConRep (AlgTyCon {tyConTyVars = tvs, algTcRhs = NewTyCon { nt_rep = rep }}) = (tvs, rep)
 newTyConRep tycon = pprPanic "newTyConRep" (ppr tycon)
 
 tyConPrimRep :: TyCon -> PrimRep
@@ -553,18 +620,18 @@ tyConArgVrcs (SynTyCon   {argVrcs = oi})       = oi
 
 \begin{code}
 getSynTyConDefn :: TyCon -> ([TyVar], Type)
-getSynTyConDefn (SynTyCon {tyConTyVars = tyvars, synTyConDefn = ty}) = (tyvars,ty)
+getSynTyConDefn (SynTyCon {tyConTyVars = tyvars, synTcRhs = ty}) = (tyvars,ty)
 getSynTyConDefn tycon = pprPanic "getSynTyConDefn" (ppr tycon)
 \end{code}
 
 \begin{code}
 maybeTyConSingleCon :: TyCon -> Maybe DataCon
-maybeTyConSingleCon (AlgTyCon {algTcRhs = DataTyCon [c] _}) = Just c
-maybeTyConSingleCon (AlgTyCon {algTcRhs = NewTyCon c _ _})  = Just c
-maybeTyConSingleCon (AlgTyCon {})	        	    = Nothing
-maybeTyConSingleCon (TupleTyCon {dataCon = con}) 	    = Just con
-maybeTyConSingleCon (PrimTyCon {})               	    = Nothing
-maybeTyConSingleCon (FunTyCon {})                	    = Nothing  -- case at funty
+maybeTyConSingleCon (AlgTyCon {algTcRhs = DataTyCon {data_cons = [c] }}) = Just c
+maybeTyConSingleCon (AlgTyCon {algTcRhs = NewTyCon { data_con = c }})    = Just c
+maybeTyConSingleCon (AlgTyCon {})	         = Nothing
+maybeTyConSingleCon (TupleTyCon {dataCon = con}) = Just con
+maybeTyConSingleCon (PrimTyCon {})               = Nothing
+maybeTyConSingleCon (FunTyCon {})                = Nothing  -- case at funty
 maybeTyConSingleCon tc = pprPanic "maybeTyConSingleCon: unexpected tycon " $ ppr tc
 \end{code}
 
diff --git a/ghc/compiler/types/Type.lhs b/ghc/compiler/types/Type.lhs
index b911493..5a4fbb0 100644
--- a/ghc/compiler/types/Type.lhs
+++ b/ghc/compiler/types/Type.lhs
@@ -29,7 +29,7 @@ module Type (
 
 	mkSynTy, 
 
-	repType, typePrimRep, coreView, deepCoreView,
+	repType, typePrimRep, coreView, tcView,
 
 	mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, 
 	applyTy, applyTys, isForAllTy, dropForAlls,
@@ -97,15 +97,16 @@ import Class	( Class, classTyCon )
 import TyCon	( TyCon, isRecursiveTyCon, isPrimTyCon,
 		  isUnboxedTupleTyCon, isUnLiftedTyCon,
 		  isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs,
-		  isAlgTyCon, isSynTyCon, tyConArity, newTyConRhs_maybe,
-	          tyConKind, getSynTyConDefn, PrimRep(..), tyConPrimRep,
+		  isAlgTyCon, tyConArity, 
+		  tcExpandTyCon_maybe, coreExpandTyCon_maybe,
+	          tyConKind, PrimRep(..), tyConPrimRep,
 		)
 
 -- others
 import StaticFlags	( opt_DictsStrict )
 import SrcLoc		( noSrcLoc )
 import Unique		( Uniquable(..) )
-import Util		( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual )
+import Util		( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual, all2 )
 import Outputable
 import UniqSet		( sizeUniqSet )		-- Should come via VarSet
 import Maybe		( isJust )
@@ -127,27 +128,7 @@ coreView :: Type -> Maybe Type
 -- its underlying representation type. 
 -- Returns Nothing if there is nothing to look through.
 --
--- By being non-recursive and inlined, this case analysis gets efficiently
--- joined onto the case analysis that the caller is already doing
-coreView (NoteTy _ ty) 	   = Just ty
-coreView (PredTy p)    	   = Just (predTypeRep p)
-coreView (TyConApp tc tys) = expandNewTcApp tc tys
-coreView ty		   = Nothing
-
-deepCoreView :: Type -> Type
--- Apply coreView recursively
-deepCoreView ty
-  | Just ty' <- coreView ty    = deepCoreView ty'
-deepCoreView (TyVarTy tv)      = TyVarTy tv
-deepCoreView (TyConApp tc tys) = TyConApp tc (map deepCoreView tys)
-deepCoreView (AppTy t1 t2)     = AppTy (deepCoreView t1) (deepCoreView t2)
-deepCoreView (FunTy t1 t2)     = FunTy (deepCoreView t1) (deepCoreView t2)
-deepCoreView (ForAllTy tv ty)  = ForAllTy tv (deepCoreView ty)
-	-- No NoteTy, no PredTy
-
-expandNewTcApp :: TyCon -> [Type] -> Maybe Type
--- A local helper function (not exported)
--- Expands *the outermoset level of* a newtype application to 
+-- In the case of newtypes, it returns
 --	*either* a vanilla TyConApp (recursive newtype, or non-saturated)
 --	*or*     the newtype representation (otherwise), meaning the
 --			type written in the RHS of the newtype decl,
@@ -160,9 +141,25 @@ expandNewTcApp :: TyCon -> [Type] -> Maybe Type
 --	            on S gives Just T
 --		    on T gives Nothing	 (no expansion)
 
-expandNewTcApp tc tys = case newTyConRhs_maybe tc tys of
-			  Nothing          -> Nothing
-			  Just (tenv, rhs) -> Just (substTy (mkTopTvSubst tenv) rhs)
+-- By being non-recursive and inlined, this case analysis gets efficiently
+-- joined onto the case analysis that the caller is already doing
+coreView (NoteTy _ ty) 	   = Just ty
+coreView (PredTy p)    	   = Just (predTypeRep p)
+coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
+			   = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
+				-- Its important to use mkAppTys, rather than (foldl AppTy),
+				-- because the function part might well return a 
+				-- partially-applied type constructor; indeed, usually will!
+coreView ty		   = Nothing
+
+-----------------------------------------------
+{-# INLINE tcView #-}
+tcView :: Type -> Maybe Type
+-- Same, but for the type checker, which just looks through synonyms
+tcView (NoteTy _ ty) 	 = Just ty
+tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys 
+			 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
+tcView ty		 = Nothing
 \end{code}
 
 
@@ -330,18 +327,15 @@ as apppropriate.
 \begin{code}
 mkGenTyConApp :: TyCon -> [Type] -> Type
 mkGenTyConApp tc tys
-  | isSynTyCon tc = mkSynTy tc tys
-  | otherwise     = mkTyConApp tc tys
+  = mkTyConApp tc tys
 
 mkTyConApp :: TyCon -> [Type] -> Type
--- Assumes TyCon is not a SynTyCon; use mkSynTy instead for those
 mkTyConApp tycon tys
   | isFunTyCon tycon, [ty1,ty2] <- tys
   = FunTy ty1 ty2
 
   | otherwise
-  = ASSERT(not (isSynTyCon tycon))
-    TyConApp tycon tys
+  = TyConApp tycon tys
 
 mkTyConTy :: TyCon -> Type
 mkTyConTy tycon = mkTyConApp tycon []
@@ -374,7 +368,8 @@ splitTyConApp_maybe other	      = Nothing
 				~~~~~
 
 \begin{code}
-mkSynTy tycon tys
+mkSynTy tycon tys = panic "No longer used"
+{-	Delete in due course
   | n_args == arity	-- Exactly saturated
   = mk_syn tys
   | n_args >  arity	-- Over-saturated
@@ -397,6 +392,7 @@ mkSynTy tycon tys
     (tyvars, body) = ASSERT( isSynTyCon tycon ) getSynTyConDefn tycon
     arity 	   = tyConArity tycon
     n_args	   = length tys
+-}
 \end{code}
 
 Notes on type synonyms
@@ -627,7 +623,6 @@ tyVarsOfType :: Type -> TyVarSet
 tyVarsOfType (TyVarTy tv)		= unitVarSet tv
 tyVarsOfType (TyConApp tycon tys)	= tyVarsOfTypes tys
 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
-tyVarsOfType (NoteTy (SynNote ty1) ty2)	= tyVarsOfType ty2	-- See note [Syn] below
 tyVarsOfType (PredTy sty)		= tyVarsOfPred sty
 tyVarsOfType (FunTy arg res)		= tyVarsOfType arg `unionVarSet` tyVarsOfType res
 tyVarsOfType (AppTy fun arg)		= tyVarsOfType fun `unionVarSet` tyVarsOfType arg
@@ -721,7 +716,6 @@ tidyType env@(tidy_env, subst) ty
 			      where
 			        (envp, tvp) = tidyTyVarBndr env tv
 
-    go_note (SynNote ty)        = SynNote $! (go ty)
     go_note note@(FTVNote ftvs) = note	-- No need to tidy the free tyvars
 
 tidyTypes env tys = map (tidyType env) tys
@@ -875,7 +869,6 @@ seqTypes []       = ()
 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
 
 seqNote :: TyNote -> ()
-seqNote (SynNote ty)  = seqType ty
 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
 
 seqPred :: PredType -> ()
@@ -886,30 +879,58 @@ seqPred (IParam n ty)  = n  `seq` seqType ty
 
 %************************************************************************
 %*									*
-		Comparison of types
+		Equality for Core types 
 	(We don't use instances so that we know where it happens)
 %*									*
 %************************************************************************
 
-Two flavours:
+Note that eqType works right even for partial applications of newtypes.
+See Note [Newtype eta] in TyCon.lhs
+
+\begin{code}
+coreEqType :: Type -> Type -> Bool
+coreEqType t1 t2
+  = eq rn_env t1 t2
+  where
+    rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
+
+    eq env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
+    eq env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
+    eq env (AppTy s1 t1)       (AppTy s2 t2)     = eq env s1 s2 && eq env t1 t2
+    eq env (FunTy s1 t1)       (FunTy s2 t2)     = eq env s1 s2 && eq env t1 t2
+    eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
+	| tc1 == tc2, all2 (eq env) tys1 tys2 = True
+			-- The lengths should be equal because
+			-- the two types have the same kind
+	-- NB: if the type constructors differ that does not 
+	--     necessarily mean that the types aren't equal
+	--     (synonyms, newtypes)
+	-- Even if the type constructors are the same, but the arguments
+	-- differ, the two types could be the same (e.g. if the arg is just
+	-- ignored in the RHS).  In both these cases we fall through to an 
+	-- attempt to expand one side or the other.
+
+	-- Now deal with newtypes, synonyms, pred-tys
+    eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
+		 | Just t2' <- coreView t2 = eq env t1 t2'
+
+	-- Fall through case; not equal!
+    eq env t1 t2 = False
+\end{code}
 
-* tcEqType, tcCmpType do *not* look through newtypes, PredTypes
-* coreEqType *does* look through them
 
-Note that eqType can respond 'False' for partial applications of newtypes.
-Consider
-	newtype Parser m a = MkParser (Foogle m a)
-Does 	
-	Monad (Parser m) `eqType` Monad (Foogle m)
-Well, yes, but eqType won't see that they are the same. 
-I don't think this is harmful, but it's soemthing to watch out for.
+%************************************************************************
+%*									*
+		Comparision for source types 
+	(We don't use instances so that we know where it happens)
+%*									*
+%************************************************************************
 
-First, the external interface
+Note that 
+	tcEqType, tcCmpType 
+do *not* look through newtypes, PredTypes
 
 \begin{code}
-coreEqType :: Type -> Type -> Bool
-coreEqType t1 t2 = isEqual $ cmpType (deepCoreView t1) (deepCoreView t2)
-
 tcEqType :: Type -> Type -> Bool
 tcEqType t1 t2 = isEqual $ cmpType t1 t2
 
@@ -951,23 +972,8 @@ cmpPred p1 p2 = cmpPredX rn_env p1 p2
     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
 
 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering	-- Main workhorse
-
--- NB: we *cannot* short-cut the newtype comparison thus:
--- eqTypeX env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) 
---	| (tc1 == tc2) = (eqTypeXs env tys1 tys2)
---
--- Consider:
---	newtype T a = MkT [a]
---	newtype Foo m = MkFoo (forall a. m a -> Int)
---	w1 :: Foo []
---	w1 = ...
---	
---	w2 :: Foo T
---	w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
---
--- We end up with w2 = w1; so we need that Foo T = Foo []
--- but we can only expand saturated newtypes, so just comparing
--- T with [] won't do. 
+cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
+		   | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
 
 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
@@ -975,7 +981,6 @@ cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenC
 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
-cmpTypeX env (NoteTy _ t1)	t2		     = cmpTypeX env t1 t2
 cmpTypeX env t1			(NoteTy _ t2)	     = cmpTypeX env t1 t2
 
     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
@@ -1081,6 +1086,7 @@ composeTvSubst in_scope env1 env2
     subst1 = TvSubst in_scope env1
 
 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
+
 isEmptyTvSubst :: TvSubst -> Bool
 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
 
@@ -1197,9 +1203,6 @@ substTys :: TvSubst -> [Type] -> [Type]
 substTys subst tys | isEmptyTvSubst subst = tys
 	           | otherwise	          = map (subst_ty subst) tys
 
-deShadowTy :: Type -> Type		-- Remove any shadowing from the type
-deShadowTy ty = subst_ty emptyTvSubst ty
-
 substTheta :: TvSubst -> ThetaType -> ThetaType
 substTheta subst theta
   | isEmptyTvSubst subst = theta
@@ -1209,6 +1212,12 @@ substPred :: TvSubst -> PredType -> PredType
 substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
 
+deShadowTy :: TyVarSet -> Type -> Type	-- Remove any nested binders mentioning tvs
+deShadowTy tvs ty 
+  = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
+  where
+    in_scope = mkInScopeSet tvs
+
 -- Note that the in_scope set is poked only if we hit a forall
 -- so it may often never be fully computed 
 subst_ty subst ty
@@ -1220,7 +1229,6 @@ subst_ty subst ty
 
     go (PredTy p)  		   = PredTy $! (substPred subst p)
 
-    go (NoteTy (SynNote ty1) ty2)  = NoteTy (SynNote $! (go ty1)) $! (go ty2)
     go (NoteTy (FTVNote _) ty2)    = go ty2		-- Discard the free tyvar note
 
     go (FunTy arg res)   	   = (FunTy $! (go arg)) $! (go res)
diff --git a/ghc/compiler/types/TypeRep.lhs b/ghc/compiler/types/TypeRep.lhs
index 4c0d01b..dc53445 100644
--- a/ghc/compiler/types/TypeRep.lhs
+++ b/ghc/compiler/types/TypeRep.lhs
@@ -152,13 +152,15 @@ data Type
 	Type		-- It must be another AppTy, or TyVarTy
 			-- (or NoteTy of these)
 
-  | TyConApp		-- Application of a TyCon, including newtypes
+  | TyConApp		-- Application of a TyCon, including newtypes *and* synonyms
 	TyCon		--  *Invariant* saturated appliations of FunTyCon and
 			-- 	synonyms have their own constructors, below.
-			-- However, *unsaturated* type synonyms, and FunTyCons
-			-- 	do appear as TyConApps.  (Unsaturated type synonyms
-			--	can appear as the RHS of a type synonym, for exmaple.)
+			-- However, *unsaturated* FunTyCons do appear as TyConApps.  
+			-- 
 	[Type]		-- Might not be saturated.
+			-- Even type synonyms are not necessarily saturated;
+			-- for example unsaturated type synonyms can appear as the 
+			-- RHS of a type synonym.
 
   | FunTy		-- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 	Type
@@ -175,12 +177,7 @@ data Type
 	TyNote
 	Type		-- The expanded version
 
-data TyNote
-  = FTVNote TyVarSet	-- The free type variables of the noted expression
-
-  | SynNote Type	-- Used for type synonyms
-			-- The Type is always a TyConApp, and is the un-expanded form.
-			-- The type to which the note is attached is the expanded form.
+data TyNote = FTVNote TyVarSet	-- The free type variables of the noted expression
 \end{code}
 
 -------------------------------------
@@ -342,13 +339,10 @@ instance Outputable name => OutputableBndr (IPName name) where
 	-- OK, here's the main printer
 
 ppr_type :: Prec -> Type -> SDoc
-ppr_type p (TyVarTy tv)      	      = ppr tv
-ppr_type p (PredTy pred)     	      = braces (ppr pred)
-ppr_type p (NoteTy (SynNote ty1) ty2) = ppr_type p ty1 
-				  	<+> ifPprDebug (braces $ ptext SLIT("Syn:") <+> pprType ty2)
-ppr_type p (NoteTy other         ty2) = ppr_type p ty2
-
-ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
+ppr_type p (TyVarTy tv)       = ppr tv
+ppr_type p (PredTy pred)      = braces (ppr pred)
+ppr_type p (NoteTy other ty2) = ppr_type p ty2
+ppr_type p (TyConApp tc tys)  = ppr_tc_app p tc tys
 
 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
 			   pprType t1 <+> ppr_type TyConPrec t2
@@ -372,14 +366,14 @@ ppr_forall_type p ty
     (tvs,  rho) = split1 [] ty
     (ctxt, tau) = split2 [] rho
 
-    split1 tvs (ForAllTy tv ty)        = split1 (tv:tvs) ty
-    split1 tvs (NoteTy (FTVNote _) ty) = split1 tvs ty
-    split1 tvs ty		       = (reverse tvs, ty)
+    split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
+    split1 tvs (NoteTy _ ty)    = split1 tvs ty
+    split1 tvs ty		= (reverse tvs, ty)
  
-    split2 ps (NoteTy (FTVNote _) arg 	-- Rather a disgusting case
+    split2 ps (NoteTy _ arg 	-- Rather a disgusting case
 	       `FunTy` res) 	      = split2 ps (arg `FunTy` res)
     split2 ps (PredTy p `FunTy` ty)   = split2 (p:ps) ty
-    split2 ps (NoteTy (FTVNote _) ty) = split2 ps ty
+    split2 ps (NoteTy _ ty) 	      = split2 ps ty
     split2 ps ty		      = (reverse ps, ty)
 
 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
diff --git a/ghc/compiler/types/Unify.lhs b/ghc/compiler/types/Unify.lhs
index e6a0878..d5d6d1d 100644
--- a/ghc/compiler/types/Unify.lhs
+++ b/ghc/compiler/types/Unify.lhs
@@ -20,7 +20,8 @@ import VarEnv
 import VarSet
 import Kind		( isSubKind )
 import Type		( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, mkTyVarTys,
-			  TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX )
+			  TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX,
+			  tcView )
 import TypeRep          ( Type(..), PredType(..), funTyCon )
 import DataCon 		( DataCon, dataConInstResTy )
 import Util		( snocView )
@@ -127,8 +128,8 @@ match :: MatchEnv	-- For the most part this is pushed downwards
 -- This matcher works on source types; that is, 
 -- it respects NewTypes and PredType
 
-match menv subst (NoteTy _ ty1) ty2 = match menv subst ty1 ty2
-match menv subst ty1 (NoteTy _ ty2) = match menv subst ty1 ty2
+match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2
+match menv subst ty1 ty2 | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
 
 match menv subst (TyVarTy tv1) ty2
   | tv1 `elemVarSet` me_tmpls menv
@@ -294,8 +295,8 @@ unify subst ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> p
 unify_ subst (TyVarTy tv1) ty2  = uVar False subst tv1 ty2
 unify_ subst ty1 (TyVarTy tv2)  = uVar True  subst tv2 ty1
 
-unify_ subst (NoteTy _ ty1) ty2  = unify subst ty1 ty2
-unify_ subst ty1 (NoteTy _ ty2)  = unify subst ty1 ty2
+unify_ subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
+unify_ subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
 
 unify_ subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
 
@@ -368,8 +369,9 @@ uUnrefined :: TvSubstEnv          -- An existing substitution to extend
 
 -- We know that tv1 isn't refined
 
-uUnrefined subst tv1 ty2 (NoteTy _ ty2')
-  = uUnrefined subst tv1 ty2 ty2'	-- Unwrap synonyms
+uUnrefined subst tv1 ty2 ty2'
+  | Just ty2'' <- tcView 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
diff --git a/ghc/compiler/utils/Util.lhs b/ghc/compiler/utils/Util.lhs
index 1598c12..e692ff1 100644
--- a/ghc/compiler/utils/Util.lhs
+++ b/ghc/compiler/utils/Util.lhs
@@ -29,7 +29,7 @@ module Util (
 
 	-- accumulating
 	mapAccumL, mapAccumR, mapAccumB, 
-	foldl2, count,
+	foldl2, count, all2,
 	
 	takeList, dropList, splitAtList, split,
 
@@ -572,6 +572,13 @@ A combination of foldl with zip.  It works with equal length lists.
 foldl2 :: (acc -> a -> b -> acc) -> acc -> [a] -> [b] -> acc
 foldl2 k z [] [] = z
 foldl2 k z (a:as) (b:bs) = foldl2 k (k z a b) as bs
+
+all2 :: (a -> b -> Bool) -> [a] -> [b] -> Bool
+-- True if the lists are the same length, and 
+-- all corresponding elements satisfy the predicate
+all2 p []     []     = True
+all2 p (x:xs) (y:ys) = p x y && all2 p xs ys
+all2 p xs     ys     = False
 \end{code}
 
 Count the number of times a predicate is true