[project @ 1998-12-02 13:17:09 by simonm]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index eff458d..54cb451 100644 (file)
-\begin{code}
-#include "HsVersions.h"
+%
+% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
+%
+\section[TcType]{Types used in the typechecker}
 
+\begin{code}
 module TcType (
-
-  SYN_IE(TcTyVar),
+  
+  TcTyVar, TcBox,
+  TcTyVarSet,
   newTcTyVar,
   newTyVarTy,  -- Kind -> NF_TcM s (TcType s)
   newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s]
 
-
-  SYN_IE(TcTyVarSet),
-
   -----------------------------------------
-  SYN_IE(TcType), TcMaybe(..),
-  SYN_IE(TcTauType), SYN_IE(TcThetaType), SYN_IE(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)
 
 
+  tcSplitRhoTy,
+
   tcInstTyVars,
-  tcInstSigTyVars, 
-  tcInstType, tcInstSigType, tcInstTcType, tcInstSigTcType,
-  tcInstTheta, tcInstId,
+  tcInstTcType,
 
-  zonkTcTyVars,
-  zonkTcType,
-  zonkTcTypeToType,
-  zonkTcTyVar,
-  zonkTcTyVarToTyVar
+  typeToTcType,
+
+  --------------------------------
+  TcKind,
+  newKindVar, newKindVars,
+  kindToTcKind,
+  zonkTcKind,
+
+  --------------------------------
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
+  zonkTcType, zonkTcTypes, zonkTcThetaType,
+
+  zonkTcTypeToType, zonkTcTyVarToTyVar,
+  zonkTcKindToKind
 
   ) where
 
+#include "HsVersions.h"
 
 
 -- friends:
-import Type    ( SYN_IE(Type), SYN_IE(ThetaType), GenType(..),
-                 tyVarsOfTypes, getTyVar_maybe,
-                 splitForAllTy, splitRhoTy,
-                 mkForAllTys, instantiateTy
-               )
-import TyVar   ( SYN_IE(TyVar), GenTyVar(..), SYN_IE(TyVarSet), SYN_IE(GenTyVarSet), 
-                 SYN_IE(TyVarEnv), lookupTyVarEnv, addOneToTyVarEnv,
-                 nullTyVarEnv, mkTyVarEnv,
-                 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 Class   ( GenClass )
-import Id      ( idType )
-import Kind    ( Kind )
-import TcKind  ( TcKind )
-import TcMonad hiding ( rnMtoTcM )
-import Usage   ( SYN_IE(Usage), GenUsage, SYN_IE(UVar), duffUsage )
+import TcMonad
+import Name            ( changeUnique )
 
-import TysPrim         ( voidTy )
+import TysWiredIn      ( voidTy )
 
-IMP_Ubiq()
+import Name            ( NamedThing(..), changeUnique, mkSysLocalName )
 import Unique          ( Unique )
-import UniqFM          ( UniqFM )
-import Maybes          ( assocMaybe )
-import Util            ( zipEqual, nOfThem, panic{-, pprPanic, pprTrace ToDo:rm-} )
-
---import Outputable    ( Outputable(..) )      -- Debugging messages
---import PprType               ( GenTyVar, GenType )
---import Pretty                                        -- ditto
---import PprStyle              ( PprStyle(..) )        -- ditto
+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)
-              | DontBind               -- This variant is used for tyvars
-                                       -- arising from type signatures, or
-                                       -- existentially quantified tyvars;
-                                       -- The idea is that we must not unify
-                                       -- such tyvars with anything except
-                                       -- themselves.
-
--- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s),
--- because you get a synonym loop if you do!
-
-type TcTyVar s    = GenTyVar (Box s)
-type TcTyVarSet s = GenTyVarSet (Box s)
+tcTyVarToTyVar :: TcTyVar s -> TyVar
+tcTyVarToTyVar = removeTyVarFlexi
 \end{code}
 
+Utility functions
+~~~~~~~~~~~~~~~~~
+These tcSplit functions are like their non-Tc analogues, but they
+follow through bound type variables.
+
+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}
@@ -116,7 +119,10 @@ newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
 newTcTyVar kind
   = tcGetUnique        `thenNF_Tc` \ uniq ->
     tcNewMutVar UnBound        `thenNF_Tc` \ box ->
-    returnNF_Tc (TyVar uniq kind Nothing box)
+    let
+       name = mkSysLocalName uniq
+    in
+    returnNF_Tc (mkFlexiTyVar name kind box)
 
 newTyVarTy  :: Kind -> NF_TcM s (TcType s)
 newTyVarTy kind
@@ -126,169 +132,75 @@ newTyVarTy kind
 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 
+newKindVar :: NF_TcM s (TcKind s)
+newKindVar = newTyVarTy superKind
 
--- For signature type variables, mark them as "DontBind"
-tcInstTyVars, tcInstSigTyVars
-       :: [GenTyVar flexi] 
-       -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)])
+newKindVars :: Int -> NF_TcM s [TcKind s]
+newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
+\end{code}
 
-tcInstTyVars    tyvars = inst_tyvars UnBound  tyvars
-tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars
+Type instantiation
+~~~~~~~~~~~~~~~~~~
+
+Instantiating a bunch of type variables
+
+\begin{code}
+tcInstTyVars :: [GenTyVar flexi] 
+            -> NF_TcM s ([TcTyVar s], [TcType s], TyVarEnv (TcType s))
 
-inst_tyvars initial_cts tyvars
-  = mapNF_Tc (inst_tyvar initial_cts) tyvars   `thenNF_Tc` \ tc_tyvars ->
+tcInstTyVars tyvars
+  = mapNF_Tc inst_tyvar tyvars `thenNF_Tc` \ tc_tyvars ->
     let
-       tys = map TyVarTy tc_tyvars
+       tys = mkTyVarTys tc_tyvars
     in
-    returnNF_Tc (tc_tyvars, tys, zipEqual "inst_tyvars" tyvars tys)
+    returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys)
 
-inst_tyvar initial_cts (TyVar _ kind name _) 
+inst_tyvar tyvar       -- Could use the name from the tyvar?
   = tcGetUnique                `thenNF_Tc` \ uniq ->
-    tcNewMutVar initial_cts    `thenNF_Tc` \ box ->
-    returnNF_Tc (TyVar uniq kind name box)
+    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}
 
-@tcInstType@ and @tcInstSigType@ both create a fresh instance of a
-type, returning a @TcType@. All inner for-alls are instantiated with
-fresh TcTyVars.
+@tcInstTcType@ instantiates the outer-level for-alls of a TcType with
+fresh type variables, returning them and the instantiated body of the for-all.
 
-The difference is that tcInstType instantiates all forall'd type
-variables (and their bindees) with UnBound type variables, whereas
-tcInstSigType instantiates them with DontBind types variables.
-@tcInstSigType@ also doesn't take an environment.
-
-On the other hand, @tcInstTcType@ instantiates a TcType. It uses
-instantiateTy which could take advantage of sharing some day.
 
 \begin{code}
 tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 tcInstTcType ty
-  = case tyvars of
+  = 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', instantiateTy tenv rho)
-  where
-    (tyvars, rho) = splitForAllTy ty
-
-tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
-tcInstSigTcType ty
-  = case tyvars of
-       []    -> returnNF_Tc ([], ty)   -- Nothing to do
-       other -> tcInstSigTyVars tyvars         `thenNF_Tc` \ (tyvars', _, tenv)  ->
-                returnNF_Tc (tyvars', instantiateTy tenv rho)
-  where
-    (tyvars, rho) = splitForAllTy ty
-
-tcInstType :: [(GenTyVar flexi,TcType s)] 
-          -> GenType (GenTyVar flexi) UVar 
-          -> NF_TcM s (TcType s)
-tcInstType tenv ty_to_inst
-  = tcConvert bind_fn occ_fn (mkTyVarEnv tenv) ty_to_inst
-  where
-    bind_fn = inst_tyvar UnBound
-    occ_fn env tyvar = case lookupTyVarEnv env tyvar of
-                        Just ty -> returnNF_Tc ty
-                        Nothing -> panic "tcInstType:1" --(ppAboves [ppr PprDebug ty_to_inst, 
-                                                       --            ppr PprDebug tyvar])
-
-tcInstSigType :: GenType (GenTyVar flexi) UVar -> NF_TcM s (TcType s)
-tcInstSigType ty_to_inst
-  = tcConvert bind_fn occ_fn nullTyVarEnv ty_to_inst
-  where
-    bind_fn = inst_tyvar DontBind
-    occ_fn env tyvar = case lookupTyVarEnv env tyvar of
-                        Just ty -> returnNF_Tc ty
-                        Nothing -> panic "tcInstType:2"-- (ppAboves [ppr PprDebug ty_to_inst, 
-                                                       --            ppr PprDebug tyvar])
-
-zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
-zonkTcTyVarToTyVar tv
-  = zonkTcTyVar tv     `thenNF_Tc` \ tv_ty ->
-    case tv_ty of      -- Should be a tyvar!
-
-      TyVarTy tv' ->    returnNF_Tc (tcTyVarToTyVar tv')
-
-      _ -> --pprTrace "zonkTcTyVarToTyVar:" (ppCat [ppr PprDebug tv, ppr PprDebug tv_ty]) $
-          returnNF_Tc (tcTyVarToTyVar tv)
-
-
-zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
-zonkTcTypeToType env ty 
-  = tcConvert zonkTcTyVarToTyVar occ_fn env ty
-  where
-    occ_fn env tyvar 
-      =  tcReadTyVar tyvar     `thenNF_Tc` \ maybe_ty ->
-        case maybe_ty of
-          BoundTo (TyVarTy tyvar') -> lookup env tyvar'
-          BoundTo other_ty         -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
-          other                    -> lookup env tyvar
-
-    lookup env tyvar = case lookupTyVarEnv env tyvar of
-                         Just ty -> returnNF_Tc ty
-                         Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
-
-
-tcConvert bind_fn occ_fn env ty_to_convert
-  = doo env ty_to_convert
-  where
-    doo env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage)
-
-    doo env (SynTy tycon tys ty)  = mapNF_Tc (doo env) tys     `thenNF_Tc` \ tys' ->
-                                  doo env ty                   `thenNF_Tc` \ ty' ->
-                                  returnNF_Tc (SynTy tycon tys' ty')
-
-    doo env (FunTy arg res usage) = doo env arg                `thenNF_Tc` \ arg' ->
-                                  doo env res          `thenNF_Tc` \ res' ->
-                                  returnNF_Tc (FunTy arg' res' usage)
-
-    doo env (AppTy fun arg)     = doo env fun          `thenNF_Tc` \ fun' ->
-                                  doo env arg          `thenNF_Tc` \ arg' ->
-                                  returnNF_Tc (AppTy fun' arg')
-
-    doo env (DictTy clas ty usage)= doo env ty         `thenNF_Tc` \ ty' ->
-                                  returnNF_Tc (DictTy clas ty' usage)
-
-    doo env (ForAllUsageTy u us ty) = doo env ty       `thenNF_Tc` \ ty' ->
-                                    returnNF_Tc (ForAllUsageTy u us ty')
-
-       -- The two interesting cases!
-    doo env (TyVarTy tv)        = occ_fn env tv
-
-    doo env (ForAllTy tyvar ty)
-       = bind_fn tyvar         `thenNF_Tc` \ tyvar' ->
-         let
-               new_env = addOneToTyVarEnv env tyvar (TyVarTy tyvar')
-         in
-         doo new_env ty                `thenNF_Tc` \ ty' ->
-         returnNF_Tc (ForAllTy tyvar' ty')
+                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}
 
+Sometimes we have to convert a Type to a TcType.  I wonder whether we could
+do this less than we do?
 
-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)
-
--- A useful function that takes an occurrence of a global thing
--- and instantiates its type with fresh type variables
-tcInstId :: Id
-        -> NF_TcM s ([TcTyVar s],      -- It's instantiated type
-                     TcThetaType s,    --
-                     TcType s)         --
+\begin{code}
+typeToTcType :: Type -> TcType s
+typeToTcType t = substFlexiTy emptyVarEnv t
 
-tcInstId id
-  = let
-      (tyvars, rho) = splitForAllTy (idType id)
-    in
-    tcInstTyVars tyvars                `thenNF_Tc` \ (tyvars', arg_tys, tenv) ->
-    tcInstType tenv rho                `thenNF_Tc` \ rho' ->
-    let
-       (theta', tau') = splitRhoTy rho'
-    in
-    returnNF_Tc (tyvars', theta', tau')
+kindToTcKind :: Kind -> TcKind s
+kindToTcKind = typeToTcType
 \end{code}
 
+
 Reading and writing TcTyVars
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 \begin{code}
@@ -299,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
@@ -314,7 +226,7 @@ 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
        BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
@@ -322,9 +234,11 @@ tcReadTyVar (TyVar uniq kind name box)
                      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
        BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
@@ -332,27 +246,51 @@ short_out ty@(TyVarTy (TyVar uniq kind name box))
                       returnNF_Tc ty'
 
        other       -> returnNF_Tc ty
+  where
+    box = tyVarFlexi tyvar
 
 short_out other_ty = returnNF_Tc other_ty
 \end{code}
 
 
-Zonking
-~~~~~~~
+Zonking Tc types to Tc types
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 \begin{code}
-zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
-zonkTcTyVars tyvars
-  = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars)       `thenNF_Tc` \ tys ->
-    returnNF_Tc (tyVarsOfTypes tys)
+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
+       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 (TyVarTy tyvar) = zonkTcTyVar tyvar
@@ -360,35 +298,93 @@ zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
 zonkTcType (AppTy ty1 ty2)
   = zonkTcType ty1             `thenNF_Tc` \ ty1' ->
     zonkTcType ty2             `thenNF_Tc` \ ty2' ->
-    returnNF_Tc (AppTy ty1' ty2')
-
-zonkTcType (TyConTy tc u)
-  = returnNF_Tc (TyConTy tc u)
+    returnNF_Tc (mkAppTy ty1' ty2')
 
-zonkTcType (SynTy tc tys ty)
+zonkTcType (TyConApp tc tys)
   = mapNF_Tc zonkTcType tys    `thenNF_Tc` \ tys' ->
-    zonkTcType ty              `thenNF_Tc` \ ty' ->
-    returnNF_Tc (SynTy tc tys' ty')
+    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')
-      _ -> --pprTrace "zonkTcType:ForAllTy:" (ppCat [ppr PprDebug tv, ppr PprDebug tv_ty]) $
-          
-          returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
+      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 (ForAllUsageTy uv uvs ty)
-  = panic "zonk:ForAllUsageTy"
-
-zonkTcType (FunTy ty1 ty2 u)
+zonkTcType (FunTy ty1 ty2)
   = zonkTcType ty1             `thenNF_Tc` \ ty1' ->
     zonkTcType ty2             `thenNF_Tc` \ ty2' ->
-    returnNF_Tc (FunTy ty1' ty2' u)
+    returnNF_Tc (FunTy ty1' ty2')
+\end{code}
+
+Zonking Tc types to Type/Kind
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+\begin{code}
+zonkTcKindToKind :: TcKind s -> NF_TcM s Kind
+zonkTcKindToKind kind = zonkTcToType boxedTypeKind emptyVarEnv kind
+
+zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
+zonkTcTypeToType env ty = zonkTcToType voidTy env ty
+
+zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
+zonkTcTyVarToTyVar tv
+  = zonkTcTyVarBndr tv `thenNF_Tc` \ tv' ->
+    returnNF_Tc (tcTyVarToTyVar tv')
 
-zonkTcType (DictTy c ty u)
-  = zonkTcType ty              `thenNF_Tc` \ ty' ->
-    returnNF_Tc (DictTy c ty' u)
+-- 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')
+
+
+    lookup env tyvar = returnNF_Tc (case lookupVarEnv env tyvar of
+                                         Just ty -> ty
+                                         Nothing -> unbound_var_ty)
 \end{code}
+
+