X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcType.lhs;h=54cb45175c23b950d9f40bf47ef69d022948584c;hb=438596897ebbe25a07e1c82085cfbc5bdb00f09e;hp=ed2794dc173d4203999441d88278c06269174bfd;hpb=6c381e873e222417d9a67aeec77b9555eca7b7a8;p=ghc-hetmet.git

diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index ed2794d..54cb451 100644
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -1,209 +1,206 @@
+%
+% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
+%
+\section[TcType]{Types used in the typechecker}
+
 \begin{code}
 module TcType (
-
-  TcTyVar(..),
+  
+  TcTyVar, TcBox,
+  TcTyVarSet,
   newTcTyVar,
   newTyVarTy,	-- Kind -> NF_TcM s (TcType s)
   newTyVarTys,	-- Int -> Kind -> NF_TcM s [TcType s]
 
-
-  TcTyVarSet(..),
-
   -----------------------------------------
-  TcType(..), TcMaybe(..),
-  TcTauType(..), TcThetaType(..), TcRhoType(..),
+  TcType, TcMaybe(..),
+  TcTauType, TcThetaType, TcRhoType,
 
 	-- Find the type to which a type variable is bound
   tcWriteTyVar,		-- :: TcTyVar s -> TcType s -> NF_TcM (TcType s)
   tcReadTyVar,		-- :: TcTyVar s -> NF_TcM (TcMaybe s)
 
 
-  tcInstTyVar,    -- TyVar -> NF_TcM s (TcTyVar s)
-  tcInstType, tcInstTcType, tcInstTheta,
+  tcSplitRhoTy,
+
+  tcInstTyVars,
+  tcInstTcType,
 
---  zonkTcType,		-- TcType s     -> NF_TcM s (TcType s)
---  zonkTcTheta,	-- TcThetaType s -> NF_TcM s (TcThetaType s)
+  typeToTcType,
 
-    zonkTcTyVars,	-- TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
-    zonkTcType,		-- TcType s -> NF_TcM s (TcType s)
-    zonkTcTypeToType,	-- TcType s -> NF_TcM s Type
-    zonkTcTyVarToTyVar	-- TcTyVar s -> NF_TcM s TyVar
+  --------------------------------
+  TcKind,
+  newKindVar, newKindVars,
+  kindToTcKind,
+  zonkTcKind,
+
+  --------------------------------
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
+  zonkTcType, zonkTcTypes, zonkTcThetaType,
+
+  zonkTcTypeToType, zonkTcTyVarToTyVar,
+  zonkTcKindToKind
 
   ) where
 
+#include "HsVersions.h"
 
 
 -- friends:
-import Type	( Type(..), ThetaType(..), GenType(..), tyVarsOfTypes, getTyVar_maybe )
-import TyVar	( TyVar(..), GenTyVar(..), TyVarSet(..), GenTyVarSet(..), 
-		  tyVarSetToList
-		)
+import PprType		()
+import Type		( Type, Kind, ThetaType, GenType(..), TyNote(..), 
+			  mkAppTy,
+			  splitDictTy_maybe, splitForAllTys,
+			  isTyVarTy, mkTyVarTys, 
+			  fullSubstTy, substFlexiTy, 
+			  boxedTypeKind, superKind
+			)
+import VarEnv
+import VarSet		( emptyVarSet )
+import Var		( TyVar, GenTyVar, tyVarKind, tyVarFlexi, tyVarName,
+			  mkFlexiTyVar, removeTyVarFlexi, isFlexiTyVar, isTyVar
+			)
 
 -- others:
-import Kind	( Kind )
-import Usage	( Usage(..), GenUsage, UVar(..), duffUsage )
-import Class	( GenClass )
-import TcKind	( TcKind )
 import TcMonad
+import Name		( changeUnique )
 
-import Ubiq
+import TysWiredIn	( voidTy )
+
+import Name		( NamedThing(..), changeUnique, mkSysLocalName )
 import Unique		( Unique )
-import UniqFM		( UniqFM )
-import Name		( getNameShortName )
-import Maybes		( assocMaybe )
-import Util		( panic )
+import Util		( nOfThem )
+import Outputable
 \end{code}
 
 
 
 Data types
 ~~~~~~~~~~
+See TcMonad.lhs
 
 \begin{code}
-type TcType s = GenType (TcTyVar s) UVar	-- Used during typechecker
-	-- Invariant on ForAllTy in TcTypes:
-	-- 	forall a. T
-	-- a cannot occur inside a MutTyVar in T; that is,
-	-- T is "flattened" before quantifying over a
-
-type TcThetaType s = [(Class, TcType s)]
-type TcRhoType s   = TcType s		-- No ForAllTys
-type TcTauType s   = TcType s		-- No DictTys or ForAllTys
-
-type Box s = MutableVar s (TcMaybe s)
-
-data TcMaybe s = UnBound
-	       | BoundTo (TcType s)
+tcTyVarToTyVar :: TcTyVar s -> TyVar
+tcTyVarToTyVar = removeTyVarFlexi
+\end{code}
 
--- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s),
--- because you get a synonym loop if you do!
+Utility functions
+~~~~~~~~~~~~~~~~~
+These tcSplit functions are like their non-Tc analogues, but they
+follow through bound type variables.
 
-type TcTyVar s    = GenTyVar (Box s)
-type TcTyVarSet s = GenTyVarSet (Box s)
-\end{code}
+No need for tcSplitForAllTy because a type variable can't be instantiated
+to a for-all type.
 
 \begin{code}
-tcTyVarToTyVar :: TcTyVar s -> TyVar
-tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage
+tcSplitRhoTy :: TcType s -> NF_TcM s (TcThetaType s, TcType s)
+tcSplitRhoTy t
+  = go t t []
+ where
+	-- A type variable is never instantiated to a dictionary type,
+	-- so we don't need to do a tcReadVar on the "arg".
+    go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
+					Just pair -> go res res (pair:ts)
+					Nothing   -> returnNF_Tc (reverse ts, syn_t)
+    go syn_t (NoteTy _ t)    ts = go syn_t t ts
+    go syn_t (TyVarTy tv)    ts = tcReadTyVar tv	`thenNF_Tc` \ maybe_ty ->
+				  case maybe_ty of
+				    BoundTo ty | not (isTyVarTy ty) -> go syn_t ty ts
+				    other			    -> returnNF_Tc (reverse ts, syn_t)
+    go syn_t t		     ts = returnNF_Tc (reverse ts, syn_t)
 \end{code}
 
-Type instantiation
+
+New type variables
 ~~~~~~~~~~~~~~~~~~
 
 \begin{code}
-newTcTyVar :: Maybe ShortName -> Kind -> NF_TcM s (TcTyVar s)
-newTcTyVar name kind
+newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
+newTcTyVar kind
   = tcGetUnique 	`thenNF_Tc` \ uniq ->
     tcNewMutVar UnBound	`thenNF_Tc` \ box ->
-    returnNF_Tc (TyVar uniq kind name box)
+    let
+	name = mkSysLocalName uniq
+    in
+    returnNF_Tc (mkFlexiTyVar name kind box)
 
 newTyVarTy  :: Kind -> NF_TcM s (TcType s)
 newTyVarTy kind
-  = newTcTyVar Nothing kind	`thenNF_Tc` \ tc_tyvar ->
+  = newTcTyVar kind	`thenNF_Tc` \ tc_tyvar ->
     returnNF_Tc (TyVarTy tc_tyvar)
 
 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
-newTyVarTys n kind = mapNF_Tc newTyVarTy (take n (repeat kind))
+newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
+
+newKindVar :: NF_TcM s (TcKind s)
+newKindVar = newTyVarTy superKind
 
-tcInstTyVar :: TyVar -> NF_TcM s (TcTyVar s)
-tcInstTyVar tyvar@(TyVar uniq kind name _)
-  = newTcTyVar name kind
+newKindVars :: Int -> NF_TcM s [TcKind s]
+newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 \end{code}
 
-@tcInstType@ and @tcInstTcType@ both create a fresh instance of a
-type, returning a @TcType@. All inner for-alls are instantiated with
-fresh TcTyVars.
+Type instantiation
+~~~~~~~~~~~~~~~~~~
 
-There are two versions, one for instantiating a @Type@, and one for a @TcType@.
-The former must instantiate everything; all tyvars must be bound either
-by a forall or by an environment passed in.  The latter can do some sharing,
-and is happy with free tyvars (which is vital when instantiating the type
-of local functions).  In the future @tcInstType@ may try to be clever about not
-instantiating constant sub-parts.
+Instantiating a bunch of type variables
 
 \begin{code}
-tcInstType :: [(TyVar,TcType s)] -> Type  -> NF_TcM s (TcType s)
-tcInstType tenv ty_to_inst
-  = do [(uniq,ty) | (TyVar uniq _ _ _, ty) <- tenv] ty_to_inst
-  where
-    do env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage)
-
-    do env (SynTy tycon tys ty)  = mapNF_Tc (do env) tys	`thenNF_Tc` \ tys' ->
-				   do env ty			`thenNF_Tc` \ ty' ->
-				   returnNF_Tc (SynTy tycon tys' ty')
-
-    do env (FunTy arg res usage)  = do env arg		`thenNF_Tc` \ arg' ->
-				    do env res		`thenNF_Tc` \ res' ->
-				    returnNF_Tc (FunTy arg' res' usage)
-
-    do env (AppTy fun arg)	  = do env fun		`thenNF_Tc` \ fun' ->
-				    do env arg		`thenNF_Tc` \ arg' ->
-				    returnNF_Tc (AppTy fun' arg')
-
-    do env (DictTy clas ty usage)= do env ty		`thenNF_Tc` \ ty' ->
-				   returnNF_Tc (DictTy clas ty' usage)
-
-    do env (TyVarTy (TyVar uniq kind name _))
-	= case assocMaybe env uniq of
-		Just tc_ty -> returnNF_Tc tc_ty
-		Nothing    -> panic "tcInstType"
-
-    do env (ForAllTy (TyVar uniq kind name _) ty)
-	= newTcTyVar name kind	`thenNF_Tc` \ tc_tyvar ->
-	  let
-		new_env = (uniq, TyVarTy tc_tyvar) : env
-	  in
-	  do new_env ty	`thenNF_Tc` \ ty' ->
-	  returnNF_Tc (ForAllTy tc_tyvar ty')
-
-   -- ForAllUsage impossible
-
-
-tcInstTheta :: [(TyVar,TcType s)] -> ThetaType -> NF_TcM s (TcThetaType s)
-tcInstTheta tenv theta
-  = mapNF_Tc go theta
-  where
-    go (clas,ty) = tcInstType tenv ty 	`thenNF_Tc` \ tc_ty ->
-		   returnNF_Tc (clas, tc_ty)
-
-tcInstTcType ::  [(TcTyVar s,TcType s)] -> TcType s -> NF_TcM s (TcType s)
-tcInstTcType tenv ty_to_inst
-  = do [(uniq,ty) | (TyVar uniq _ _ _, ty) <- tenv] ty_to_inst
-  where
-    do env ty@(TyConTy tycon usage) = returnNF_Tc ty
-
--- Could do clever stuff here to avoid instantiating constant types
-    do env (SynTy tycon tys ty)  = mapNF_Tc (do env) tys	`thenNF_Tc` \ tys' ->
-				   do env ty			`thenNF_Tc` \ ty' ->
-				   returnNF_Tc (SynTy tycon tys' ty')
+tcInstTyVars :: [GenTyVar flexi] 
+	     -> NF_TcM s ([TcTyVar s], [TcType s], TyVarEnv (TcType s))
+
+tcInstTyVars tyvars
+  = mapNF_Tc inst_tyvar tyvars	`thenNF_Tc` \ tc_tyvars ->
+    let
+	tys = mkTyVarTys tc_tyvars
+    in
+    returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys)
+
+inst_tyvar tyvar	-- Could use the name from the tyvar?
+  = tcGetUnique 		`thenNF_Tc` \ uniq ->
+    tcNewMutVar UnBound		`thenNF_Tc` \ box ->
+    let
+	name = changeUnique (tyVarName tyvar) uniq
+	-- Note that we don't change the print-name
+	-- This won't confuse the type checker but there's a chance
+	-- that two different tyvars will print the same way 
+	-- in an error message.  -dppr-debug will show up the difference
+	-- Better watch out for this.  If worst comes to worst, just
+	-- use mkSysLocalName.
+    in
+    returnNF_Tc (mkFlexiTyVar name (tyVarKind tyvar) box)
+\end{code}
 
-    do env (FunTy arg res usage)  = do env arg		`thenNF_Tc` \ arg' ->
-				    do env res		`thenNF_Tc` \ res' ->
-				    returnNF_Tc (FunTy arg' res' usage)
+@tcInstTcType@ instantiates the outer-level for-alls of a TcType with
+fresh type variables, returning them and the instantiated body of the for-all.
 
-    do env (AppTy fun arg)	  = do env fun		`thenNF_Tc` \ fun' ->
-				    do env arg		`thenNF_Tc` \ arg' ->
-				    returnNF_Tc (AppTy fun' arg')
 
-    do env (DictTy clas ty usage)= do env ty		`thenNF_Tc` \ ty' ->
-				   returnNF_Tc (DictTy clas ty' usage)
+\begin{code}
+tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
+tcInstTcType ty
+  = let
+	(tyvars, rho) = splitForAllTys ty
+    in
+    case tyvars of
+	[]    -> returnNF_Tc ([], ty)	-- Nothing to do
+	other -> tcInstTyVars tyvars		`thenNF_Tc` \ (tyvars', _, tenv)  ->
+		 returnNF_Tc (tyvars', fullSubstTy tenv emptyVarSet rho)
+					-- Since the tyvars are freshly made,
+					-- they cannot possibly be captured by
+					-- any existing for-alls.  Hence emptyVarSet
+\end{code}
 
-    do env ty@(TyVarTy (TyVar uniq kind name _))
-	= case assocMaybe env uniq of
-		Just tc_ty -> returnNF_Tc tc_ty
-		Nothing    -> returnNF_Tc ty
+Sometimes we have to convert a Type to a TcType.  I wonder whether we could
+do this less than we do?
 
-    do env (ForAllTy (TyVar uniq kind name _) ty)
-	= newTcTyVar name kind	`thenNF_Tc` \ tc_tyvar ->
-	  let
-		new_env = (uniq, TyVarTy tc_tyvar) : env
-	  in
-	  do new_env ty	`thenNF_Tc` \ ty' ->
-	  returnNF_Tc (ForAllTy tc_tyvar ty')
+\begin{code}
+typeToTcType :: Type -> TcType s
+typeToTcType t = substFlexiTy emptyVarEnv t
 
-   -- ForAllUsage impossible
+kindToTcKind :: Kind -> TcKind s
+kindToTcKind = typeToTcType
 \end{code}
 
+
 Reading and writing TcTyVars
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 \begin{code}
@@ -214,12 +211,12 @@ tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
 Writing is easy:
 
 \begin{code}
-tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
+tcWriteTyVar tyvar ty = tcWriteMutVar (tyVarFlexi tyvar) (BoundTo ty)
 \end{code}
 
 Reading is more interesting.  The easy thing to do is just to read, thus:
 \begin{verbatim}
-tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
+tcReadTyVar tyvar = tcReadMutVar (tyVarFlexi tyvar)
 \end{verbatim}
 
 But it's more fun to short out indirections on the way: If this
@@ -229,94 +226,165 @@ any other type, then there might be bound TyVars embedded inside it.
 We return Nothing iff the original box was unbound.
 
 \begin{code}
-tcReadTyVar (TyVar uniq kind name box)
+tcReadTyVar tyvar
   = tcReadMutVar box	`thenNF_Tc` \ maybe_ty ->
     case maybe_ty of
-	UnBound    -> returnNF_Tc UnBound
 	BoundTo ty -> short_out ty			`thenNF_Tc` \ ty' ->
 		      tcWriteMutVar box (BoundTo ty')	`thenNF_Tc_`
 		      returnNF_Tc (BoundTo ty')
 
+	other	   -> returnNF_Tc other
+  where
+    box = tyVarFlexi tyvar
+
 short_out :: TcType s -> NF_TcM s (TcType s)
-short_out ty@(TyVarTy (TyVar uniq kind name box))
+short_out ty@(TyVarTy tyvar)
   = tcReadMutVar box	`thenNF_Tc` \ maybe_ty ->
     case maybe_ty of
-	UnBound     -> returnNF_Tc ty
 	BoundTo ty' -> short_out ty' 			`thenNF_Tc` \ ty' ->
 		       tcWriteMutVar box (BoundTo ty')	`thenNF_Tc_`
 		       returnNF_Tc ty'
 
+	other       -> returnNF_Tc ty
+  where
+    box = tyVarFlexi tyvar
+
 short_out other_ty = returnNF_Tc other_ty
 \end{code}
 
 
-Zonking
-~~~~~~~
-@zonkTcTypeToType@ converts from @TcType@ to @Type@.  It follows through all
-the substitutions of course.
-
+Zonking Tc types to Tc types
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 \begin{code}
-zonkTcTypeToType :: TcType s -> NF_TcM s Type
-zonkTcTypeToType ty = zonk tcTyVarToTyVar ty
+zonkTcTyVars :: [TcTyVar s] -> NF_TcM s [TcType s]
+zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
+
+zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
+zonkTcTyVar tyvar 
+  | not (isFlexiTyVar tyvar)	-- Not a flexi tyvar.  This can happen when
+				-- zonking a forall type, when the bound type variable
+				-- needn't be a flexi.
+  = ASSERT( isTyVar tyvar )
+    returnNF_Tc (TyVarTy tyvar)
+
+  | otherwise	-- Is a flexi tyvar
+  = tcReadTyVar tyvar		`thenNF_Tc` \ maybe_ty ->
+    case maybe_ty of
+	BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty		-- tcReadTyVar never returns a bound tyvar
+	BoundTo other		    -> zonkTcType other
+	other			    -> returnNF_Tc (TyVarTy tyvar)
+
+zonkTcTyVarBndr :: TcTyVar s -> NF_TcM s (TcTyVar s)
+zonkTcTyVarBndr tyvar
+  = zonkTcTyVar tyvar	`thenNF_Tc` \ (TyVarTy tyvar') ->
+    returnNF_Tc tyvar'
+	
+zonkTcTypes :: [TcType s] -> NF_TcM s [TcType s]
+zonkTcTypes tys = mapNF_Tc zonkTcType tys
+
+zonkTcThetaType :: TcThetaType s -> NF_TcM s (TcThetaType s)
+zonkTcThetaType theta = mapNF_Tc zonk theta
+		    where
+		      zonk (c,ts) = zonkTcTypes ts	`thenNF_Tc` \ new_ts ->
+				    returnNF_Tc (c, new_ts)
+
+zonkTcKind :: TcKind s -> NF_TcM s (TcKind s)
+zonkTcKind = zonkTcType
 
 zonkTcType :: TcType s -> NF_TcM s (TcType s)
-zonkTcType ty = zonk (\tyvar -> tyvar) ty
-
-zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
-zonkTcTyVars tyvars
-  = mapNF_Tc (zonk_tv (\tyvar -> tyvar)) 
-	     (tyVarSetToList tyvars)		`thenNF_Tc` \ tys ->
-    returnNF_Tc (tyVarsOfTypes tys)
 
-zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
-zonkTcTyVarToTyVar tyvar
-  = zonk_tv_to_tv tcTyVarToTyVar tyvar
-
-
-zonk tyvar_fn (TyVarTy tyvar)
-  = zonk_tv tyvar_fn tyvar
-
-zonk tyvar_fn (AppTy ty1 ty2)
-  = zonk tyvar_fn ty1		`thenNF_Tc` \ ty1' ->
-    zonk tyvar_fn ty2		`thenNF_Tc` \ ty2' ->
-    returnNF_Tc (AppTy ty1' ty2')
-
-zonk tyvar_fn (TyConTy tc u)
-  = returnNF_Tc (TyConTy tc u)
-
-zonk tyvar_fn (SynTy tc tys ty)
-  = mapNF_Tc (zonk tyvar_fn) tys `thenNF_Tc` \ tys' ->
-    zonk tyvar_fn ty 		 `thenNF_Tc` \ ty' ->
-    returnNF_Tc (SynTy tc tys' ty')
-
-zonk tyvar_fn (ForAllTy tv ty)
-  = zonk_tv_to_tv tyvar_fn tv	`thenNF_Tc` \ tv' ->
-    zonk tyvar_fn ty 		`thenNF_Tc` \ ty' ->
-    returnNF_Tc (ForAllTy tv' ty')
+zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
+
+zonkTcType (AppTy ty1 ty2)
+  = zonkTcType ty1		`thenNF_Tc` \ ty1' ->
+    zonkTcType ty2		`thenNF_Tc` \ ty2' ->
+    returnNF_Tc (mkAppTy ty1' ty2')
+
+zonkTcType (TyConApp tc tys)
+  = mapNF_Tc zonkTcType tys	`thenNF_Tc` \ tys' ->
+    returnNF_Tc (TyConApp tc tys')
+
+zonkTcType (NoteTy (SynNote ty1) ty2)
+  = zonkTcType ty1 		`thenNF_Tc` \ ty1' ->
+    zonkTcType ty2 		`thenNF_Tc` \ ty2' ->
+    returnNF_Tc (NoteTy (SynNote ty1') ty2')
+
+zonkTcType (NoteTy (FTVNote _) ty2) = zonkTcType ty2
+
+zonkTcType (ForAllTy tv ty)
+  = zonkTcTyVar tv		`thenNF_Tc` \ tv_ty ->
+    zonkTcType ty 		`thenNF_Tc` \ ty' ->
+    case tv_ty of	-- Should be a tyvar!
+      TyVarTy tv' -> returnNF_Tc (ForAllTy tv' ty')
+      _ -> panic "zonkTcType"
+	   -- pprTrace "zonkTcType:ForAllTy:" (hsep [ppr tv, ppr tv_ty]) $
+	   -- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
+
+zonkTcType (FunTy ty1 ty2)
+  = zonkTcType ty1 		`thenNF_Tc` \ ty1' ->
+    zonkTcType ty2 		`thenNF_Tc` \ ty2' ->
+    returnNF_Tc (FunTy ty1' ty2')
+\end{code}
 
-zonk tyvar_fn (ForAllUsageTy uv uvs ty)
-  = panic "zonk:ForAllUsageTy"
+Zonking Tc types to Type/Kind
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+\begin{code}
+zonkTcKindToKind :: TcKind s -> NF_TcM s Kind
+zonkTcKindToKind kind = zonkTcToType boxedTypeKind emptyVarEnv kind
 
-zonk tyvar_fn (FunTy ty1 ty2 u)
-  = zonk tyvar_fn ty1 		`thenNF_Tc` \ ty1' ->
-    zonk tyvar_fn ty2 		`thenNF_Tc` \ ty2' ->
-    returnNF_Tc (FunTy ty1' ty2' u)
+zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
+zonkTcTypeToType env ty = zonkTcToType voidTy env ty
 
-zonk tyvar_fn (DictTy c ty u)
-  = zonk tyvar_fn ty 		`thenNF_Tc` \ ty' ->
-    returnNF_Tc (DictTy c ty' u)
+zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
+zonkTcTyVarToTyVar tv
+  = zonkTcTyVarBndr tv	`thenNF_Tc` \ tv' ->
+    returnNF_Tc (tcTyVarToTyVar tv')
+
+-- zonkTcToType is used for Kinds as well
+zonkTcToType :: Type -> TyVarEnv Type -> TcType s -> NF_TcM s Type
+zonkTcToType unbound_var_ty env ty
+  = go ty
+  where
+    go (TyConApp tycon tys)	  = mapNF_Tc go tys	`thenNF_Tc` \ tys' ->
+				    returnNF_Tc (TyConApp tycon tys')
+
+    go (NoteTy (SynNote ty1) ty2) = go ty1		`thenNF_Tc` \ ty1' ->
+				    go ty2		`thenNF_Tc` \ ty2' ->
+				    returnNF_Tc (NoteTy (SynNote ty1') ty2')
+
+    go (NoteTy (FTVNote _) ty2)   = go ty2	-- Discard free-tyvar annotations
+
+    go (FunTy arg res)      	  = go arg		`thenNF_Tc` \ arg' ->
+				    go res		`thenNF_Tc` \ res' ->
+				    returnNF_Tc (FunTy arg' res')
+ 
+    go (AppTy fun arg)	 	  = go fun		`thenNF_Tc` \ fun' ->
+				    go arg		`thenNF_Tc` \ arg' ->
+				    returnNF_Tc (mkAppTy fun' arg')
+
+	-- The two interesting cases!
+	-- c.f. zonkTcTyVar
+    go (TyVarTy tyvar)  
+	| not (isFlexiTyVar tyvar) = lookup env tyvar
+
+	| otherwise	=  tcReadTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
+			   case maybe_ty of
+			      BoundTo (TyVarTy tyvar') -> lookup env tyvar'
+			      BoundTo other_ty	       -> go other_ty
+			      other		       -> lookup env tyvar
+
+    go (ForAllTy tyvar ty)
+	= zonkTcTyVarToTyVar tyvar	`thenNF_Tc` \ tyvar' ->
+	  let
+	     new_env = extendVarEnv env tyvar (TyVarTy tyvar')
+	  in
+	  zonkTcToType unbound_var_ty new_env ty	`thenNF_Tc` \ ty' ->
+	  returnNF_Tc (ForAllTy tyvar' ty')
 
 
-zonk_tv tyvar_fn tyvar
-  = tcReadTyVar tyvar		`thenNF_Tc` \ maybe_ty ->
-    case maybe_ty of
-	UnBound    -> returnNF_Tc (TyVarTy (tyvar_fn tyvar))
-	BoundTo ty -> zonk tyvar_fn ty
+    lookup env tyvar = returnNF_Tc (case lookupVarEnv env tyvar of
+					  Just ty -> ty
+					  Nothing -> unbound_var_ty)
+\end{code}
 
 
-zonk_tv_to_tv tyvar_fn tyvar
-  = zonk_tv tyvar_fn tyvar	`thenNF_Tc` \ ty ->
-    case getTyVar_maybe ty of
-	Nothing    -> panic "zonk_tv_to_tv"
-	Just tyvar -> returnNF_Tc tyvar
-\end{code}