[project @ 2001-05-21 09:19:14 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index 54cb451..3f6831b 100644 (file)
@@ -6,40 +6,36 @@
 \begin{code}
 module TcType (
   
-  TcTyVar, TcBox,
+  TcTyVar,
   TcTyVarSet,
-  newTcTyVar,
-  newTyVarTy,  -- Kind -> NF_TcM s (TcType s)
-  newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s]
+  newTyVar,
+  newTyVarTy,          -- Kind -> NF_TcM TcType
+  newTyVarTys,         -- Int -> Kind -> NF_TcM [TcType]
 
   -----------------------------------------
-  TcType, TcMaybe(..),
-  TcTauType, TcThetaType, TcRhoType,
+  TcType, 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)
+  tcPutTyVar,          -- :: TcTyVar -> TcType -> NF_TcM TcType
+  tcGetTyVar,          -- :: TcTyVar -> NF_TcM (Maybe TcType)  does shorting out
 
 
   tcSplitRhoTy,
 
-  tcInstTyVars,
-  tcInstTcType,
-
-  typeToTcType,
+  tcInstTyVar, tcInstTyVars,
+  tcInstSigVars,
+  tcInstType,
 
   --------------------------------
   TcKind,
-  newKindVar, newKindVars,
-  kindToTcKind,
-  zonkTcKind,
+  newKindVar, newKindVars, newBoxityVar,
 
   --------------------------------
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
-  zonkTcType, zonkTcTypes, zonkTcThetaType,
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
+  zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
+  zonkTcPredType,
 
-  zonkTcTypeToType, zonkTcTyVarToTyVar,
-  zonkTcKindToKind
+  zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv
 
   ) where
 
@@ -47,43 +43,34 @@ module TcType (
 
 
 -- friends:
-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
+import TypeRep         ( Type(..), Kind, TyNote(..) )  -- friend
+import Type            ( PredType(..),
+                         getTyVar, mkAppTy, mkUTy,
+                         splitPredTy_maybe, splitForAllTys, 
+                         isTyVarTy, mkTyVarTy, mkTyVarTys, 
+                         openTypeKind, liftedTypeKind, 
+                         superKind, superBoxity, tyVarsOfTypes,
+                         defaultKind, liftedBoxity
                        )
+import Subst           ( Subst, mkTopTyVarSubst, substTy )
+import TyCon           ( mkPrimTyCon )
+import PrimRep         ( PrimRep(VoidRep) )
+import Var             ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
 
 -- others:
-import TcMonad
-import Name            ( changeUnique )
-
+import TcMonad          -- TcType, amongst others
 import TysWiredIn      ( voidTy )
 
-import Name            ( NamedThing(..), changeUnique, mkSysLocalName )
-import Unique          ( Unique )
+import Name            ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
+                         mkLocalName, mkDerivedTyConOcc
+                       )
+import Unique          ( Uniquable(..) )
+import SrcLoc          ( noSrcLoc )
 import Util            ( nOfThem )
 import Outputable
 \end{code}
 
 
-
-Data types
-~~~~~~~~~~
-See TcMonad.lhs
-
-\begin{code}
-tcTyVarToTyVar :: TcTyVar s -> TyVar
-tcTyVarToTyVar = removeTyVarFlexi
-\end{code}
-
 Utility functions
 ~~~~~~~~~~~~~~~~~
 These tcSplit functions are like their non-Tc analogues, but they
@@ -93,73 +80,88 @@ No need for tcSplitForAllTy because a type variable can't be instantiated
 to a for-all type.
 
 \begin{code}
-tcSplitRhoTy :: TcType s -> NF_TcM s (TcThetaType s, TcType s)
+tcSplitRhoTy :: TcType -> NF_TcM (TcThetaType, TcType)
 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
+    go syn_t (FunTy arg res) ts = case splitPredTy_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 ->
+    go syn_t (TyVarTy tv)    ts = tcGetTyVar 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)
+                                   Just ty | not (isTyVarTy ty) -> go syn_t ty ts
+                                   other                        -> returnNF_Tc (reverse ts, syn_t)
+    go syn_t (UsageTy _ t)   ts = go syn_t t ts
     go syn_t t              ts = returnNF_Tc (reverse ts, syn_t)
 \end{code}
 
 
-New type variables
-~~~~~~~~~~~~~~~~~~
+%************************************************************************
+%*                                                                     *
+\subsection{New type variables}
+%*                                                                     *
+%************************************************************************
 
 \begin{code}
-newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
-newTcTyVar kind
+newTyVar :: Kind -> NF_TcM TcTyVar
+newTyVar kind
   = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutVar UnBound        `thenNF_Tc` \ box ->
-    let
-       name = mkSysLocalName uniq
-    in
-    returnNF_Tc (mkFlexiTyVar name kind box)
+    tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
 
-newTyVarTy  :: Kind -> NF_TcM s (TcType s)
+newTyVarTy  :: Kind -> NF_TcM TcType
 newTyVarTy kind
-  = newTcTyVar kind    `thenNF_Tc` \ tc_tyvar ->
+  = newTyVar kind      `thenNF_Tc` \ tc_tyvar ->
     returnNF_Tc (TyVarTy tc_tyvar)
 
-newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
+newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 
-newKindVar :: NF_TcM s (TcKind s)
-newKindVar = newTyVarTy superKind
+newKindVar :: NF_TcM TcKind
+newKindVar
+  = tcGetUnique                                                `thenNF_Tc` \ uniq ->
+    tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind    `thenNF_Tc` \ kv ->
+    returnNF_Tc (TyVarTy kv)
 
-newKindVars :: Int -> NF_TcM s [TcKind s]
+newKindVars :: Int -> NF_TcM [TcKind]
 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
+
+newBoxityVar :: NF_TcM TcKind
+newBoxityVar
+  = tcGetUnique                                                `thenNF_Tc` \ uniq ->
+    tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
+    returnNF_Tc (TyVarTy kv)
 \end{code}
 
-Type instantiation
-~~~~~~~~~~~~~~~~~~
+
+%************************************************************************
+%*                                                                     *
+\subsection{Type instantiation}
+%*                                                                     *
+%************************************************************************
 
 Instantiating a bunch of type variables
 
 \begin{code}
-tcInstTyVars :: [GenTyVar flexi] 
-            -> NF_TcM s ([TcTyVar s], [TcType s], TyVarEnv (TcType s))
+tcInstTyVars :: [TyVar] 
+            -> NF_TcM ([TcTyVar], [TcType], Subst)
 
 tcInstTyVars tyvars
-  = mapNF_Tc inst_tyvar tyvars `thenNF_Tc` \ tc_tyvars ->
+  = mapNF_Tc tcInstTyVar tyvars        `thenNF_Tc` \ tc_tyvars ->
     let
        tys = mkTyVarTys tc_tyvars
     in
-    returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys)
+    returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
+               -- Since the tyvars are freshly made,
+               -- they cannot possibly be captured by
+               -- any existing for-alls.  Hence mkTopTyVarSubst
 
-inst_tyvar tyvar       -- Could use the name from the tyvar?
+tcInstTyVar tyvar
   = tcGetUnique                `thenNF_Tc` \ uniq ->
-    tcNewMutVar UnBound                `thenNF_Tc` \ box ->
     let
-       name = changeUnique (tyVarName tyvar) uniq
+       name = setNameUnique (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 
@@ -167,56 +169,67 @@ inst_tyvar tyvar  -- Could use the name from the tyvar?
        -- Better watch out for this.  If worst comes to worst, just
        -- use mkSysLocalName.
     in
-    returnNF_Tc (mkFlexiTyVar name (tyVarKind tyvar) box)
+    tcNewMutTyVar name (tyVarKind tyvar)
+
+tcInstSigVars tyvars   -- Very similar to tcInstTyVar
+  = tcGetUniques       `thenNF_Tc` \ uniqs ->
+    listTc [ ASSERT( not (kind == openTypeKind) )      -- Shouldn't happen
+            tcNewSigTyVar name kind 
+          | (tyvar, uniq) <- tyvars `zip` uniqs,
+            let name = setNameUnique (tyVarName tyvar) uniq, 
+            let kind = tyVarKind tyvar
+          ]
 \end{code}
 
-@tcInstTcType@ instantiates the outer-level for-alls of a TcType with
-fresh type variables, returning them and the instantiated body of the for-all.
-
+@tcInstType@ instantiates the outer-level for-alls of a TcType with
+fresh type variables, splits off the dictionary part, and returns the results.
 
 \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
+tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
+tcInstType ty
+  = case splitForAllTys ty of
+       ([],     rho) ->        -- There may be overloading but no type variables;
+                               --      (?x :: Int) => Int -> Int
+                        tcSplitRhoTy rho                       `thenNF_Tc` \ (theta, tau) ->
+                        returnNF_Tc ([], theta, tau)
+
+       (tyvars, rho) -> tcInstTyVars tyvars                    `thenNF_Tc` \ (tyvars', _, tenv)  ->
+                        tcSplitRhoTy (substTy tenv rho)        `thenNF_Tc` \ (theta, tau) ->
+                        returnNF_Tc (tyvars', theta, tau)
 \end{code}
 
-Sometimes we have to convert a Type to a TcType.  I wonder whether we could
-do this less than we do?
 
-\begin{code}
-typeToTcType :: Type -> TcType s
-typeToTcType t = substFlexiTy emptyVarEnv t
-
-kindToTcKind :: Kind -> TcKind s
-kindToTcKind = typeToTcType
-\end{code}
 
+%************************************************************************
+%*                                                                     *
+\subsection{Putting and getting  mutable type variables}
+%*                                                                     *
+%************************************************************************
 
-Reading and writing TcTyVars
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 \begin{code}
-tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
-tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
+tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
+tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
 \end{code}
 
-Writing is easy:
+Putting is easy:
 
 \begin{code}
-tcWriteTyVar tyvar ty = tcWriteMutVar (tyVarFlexi tyvar) (BoundTo ty)
+tcPutTyVar tyvar ty 
+  | not (isMutTyVar tyvar)
+  = pprTrace "tcPutTyVar" (ppr tyvar) $
+    returnNF_Tc ty
+
+  | otherwise
+  = ASSERT( isMutTyVar tyvar )
+    UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
+    tcWriteMutTyVar tyvar (Just ty)    `thenNF_Tc_`
+    returnNF_Tc ty
 \end{code}
 
-Reading is more interesting.  The easy thing to do is just to read, thus:
+Getting is more interesting.  The easy thing to do is just to read, thus:
+
 \begin{verbatim}
-tcReadTyVar tyvar = tcReadMutVar (tyVarFlexi tyvar)
+tcGetTyVar tyvar = tcReadMutTyVar tyvar
 \end{verbatim}
 
 But it's more fun to short out indirections on the way: If this
@@ -226,123 +239,185 @@ 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
-  = tcReadMutVar box   `thenNF_Tc` \ maybe_ty ->
+tcGetTyVar tyvar
+  | not (isMutTyVar tyvar)
+  = pprTrace "tcGetTyVar" (ppr tyvar) $
+    returnNF_Tc (Just (mkTyVarTy tyvar))
+
+  | otherwise
+  = ASSERT2( isMutTyVar tyvar, ppr tyvar )
+    tcReadMutTyVar tyvar                               `thenNF_Tc` \ maybe_ty ->
     case maybe_ty of
-       BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
-                     tcWriteMutVar box (BoundTo ty')   `thenNF_Tc_`
-                     returnNF_Tc (BoundTo ty')
+       Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
+                  tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
+                  returnNF_Tc (Just ty')
 
-       other      -> returnNF_Tc other
-  where
-    box = tyVarFlexi tyvar
+       Nothing    -> returnNF_Tc Nothing
 
-short_out :: TcType s -> NF_TcM s (TcType s)
+short_out :: TcType -> NF_TcM TcType
 short_out ty@(TyVarTy tyvar)
-  = tcReadMutVar box   `thenNF_Tc` \ maybe_ty ->
+  | not (isMutTyVar tyvar)
+  = returnNF_Tc ty
+
+  | otherwise
+  = tcReadMutTyVar tyvar       `thenNF_Tc` \ maybe_ty ->
     case maybe_ty of
-       BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
-                      tcWriteMutVar box (BoundTo ty')  `thenNF_Tc_`
-                      returnNF_Tc ty'
+       Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
+                   tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
+                   returnNF_Tc ty'
 
-       other       -> returnNF_Tc ty
-  where
-    box = tyVarFlexi tyvar
+       other    -> returnNF_Tc ty
 
 short_out other_ty = returnNF_Tc other_ty
 \end{code}
 
 
-Zonking Tc types to Tc types
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+%************************************************************************
+%*                                                                     *
+\subsection{Zonking -- the exernal interfaces}
+%*                                                                     *
+%************************************************************************
+
+-----------------  Type variables
+
 \begin{code}
-zonkTcTyVars :: [TcTyVar s] -> NF_TcM s [TcType s]
+zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
 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)
+zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
+zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
+                          returnNF_Tc (tyVarsOfTypes tys)
 
-  | 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
+zonkTcTyVar :: TcTyVar -> NF_TcM TcType
+zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
 
-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)
+zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
+-- This guy is to zonk the tyvars we're about to feed into tcSimplify
+-- Usually this job is done by checkSigTyVars, but in a couple of places
+-- that is overkill, so we use this simpler chap
+zonkTcSigTyVars tyvars
+  = zonkTcTyVars tyvars        `thenNF_Tc` \ tys ->
+    returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
+\end{code}
 
-zonkTcKind :: TcKind s -> NF_TcM s (TcKind s)
-zonkTcKind = zonkTcType
+-----------------  Types
 
-zonkTcType :: TcType s -> NF_TcM s (TcType s)
+\begin{code}
+zonkTcType :: TcType -> NF_TcM TcType
+zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 
-zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
+zonkTcTypes :: [TcType] -> NF_TcM [TcType]
+zonkTcTypes tys = mapNF_Tc zonkTcType tys
 
-zonkTcType (AppTy ty1 ty2)
-  = zonkTcType ty1             `thenNF_Tc` \ ty1' ->
-    zonkTcType ty2             `thenNF_Tc` \ ty2' ->
-    returnNF_Tc (mkAppTy ty1' ty2')
+zonkTcClassConstraints cts = mapNF_Tc zonk cts
+    where zonk (clas, tys)
+           = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
+             returnNF_Tc (clas, new_tys)
+
+zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
+zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
+
+zonkTcPredType :: TcPredType -> NF_TcM TcPredType
+zonkTcPredType (ClassP c ts) =
+    zonkTcTypes ts     `thenNF_Tc` \ new_ts ->
+    returnNF_Tc (ClassP c new_ts)
+zonkTcPredType (IParam n t) =
+    zonkTcType t       `thenNF_Tc` \ new_t ->
+    returnNF_Tc (IParam n new_t)
+\end{code}
 
-zonkTcType (TyConApp tc tys)
-  = mapNF_Tc zonkTcType tys    `thenNF_Tc` \ tys' ->
-    returnNF_Tc (TyConApp tc tys')
+-------------------  These ...ToType, ...ToKind versions
+                    are used at the end of type checking
 
-zonkTcType (NoteTy (SynNote ty1) ty2)
-  = zonkTcType ty1             `thenNF_Tc` \ ty1' ->
-    zonkTcType ty2             `thenNF_Tc` \ ty2' ->
-    returnNF_Tc (NoteTy (SynNote ty1') ty2')
+\begin{code}
+zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
+zonkKindEnv pairs 
+  = mapNF_Tc zonk_it pairs
+ where
+    zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
+                             returnNF_Tc (name, kind)
+
+       -- When zonking a kind, we want to
+       --      zonk a *kind* variable to (Type *)
+       --      zonk a *boxity* variable to *
+    zonk_unbound_kind_var kv | tyVarKind kv == superKind   = tcPutTyVar kv liftedTypeKind
+                            | tyVarKind kv == superBoxity = tcPutTyVar kv liftedBoxity
+                            | otherwise                   = pprPanic "zonkKindEnv" (ppr kv)
+                       
+zonkTcTypeToType :: TcType -> NF_TcM Type
+zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
+  where
+       -- Zonk a mutable but unbound type variable to
+       --      Void            if it has kind Lifted
+       --      :Void           otherwise
+    zonk_unbound_tyvar tv
+       | kind == liftedTypeKind || kind == openTypeKind
+       = tcPutTyVar tv voidTy  -- Just to avoid creating a new tycon in
+                               -- this vastly common case
+       | otherwise
+       = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
+       where
+         kind = tyVarKind tv
+
+    mk_void_tycon tv kind      -- Make a new TyCon with the same kind as the 
+                               -- type variable tv.  Same name too, apart from
+                               -- making it start with a colon (sigh)
+               -- I dread to think what will happen if this gets out into an 
+               -- interface file.  Catastrophe likely.  Major sigh.
+       = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
+         mkPrimTyCon tc_name kind 0 [] VoidRep
+       where
+         tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
+
+-- zonkTcTyVarToTyVar is applied to the *binding* occurrence 
+-- of a type variable, at the *end* of type checking.  It changes
+-- the *mutable* type variable into an *immutable* one.
+-- 
+-- It does this by making an immutable version of tv and binds tv to it.
+-- Now any bound occurences of the original type variable will get 
+-- zonked to the immutable version.
+
+zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
+zonkTcTyVarToTyVar tv
+  = let
+               -- Make an immutable version, defaulting 
+               -- the kind to lifted if necessary
+       immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
+       immut_tv_ty = mkTyVarTy immut_tv
 
-zonkTcType (NoteTy (FTVNote _) ty2) = zonkTcType ty2
+        zap tv = tcPutTyVar tv immut_tv_ty
+               -- Bind the mutable version to the immutable one
+    in 
+       -- If the type variable is mutable, then bind it to immut_tv_ty
+       -- so that all other occurrences of the tyvar will get zapped too
+    zonkTyVar zap tv           `thenNF_Tc` \ 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')
+    WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
 
-zonkTcType (FunTy ty1 ty2)
-  = zonkTcType ty1             `thenNF_Tc` \ ty1' ->
-    zonkTcType ty2             `thenNF_Tc` \ ty2' ->
-    returnNF_Tc (FunTy ty1' ty2')
+    returnNF_Tc immut_tv
 \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
+%************************************************************************
+%*                                                                     *
+\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
+%*                                                                     *
+%*             For internal use only!                                  *
+%*                                                                     *
+%************************************************************************
 
-zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
-zonkTcTyVarToTyVar tv
-  = zonkTcTyVarBndr tv `thenNF_Tc` \ tv' ->
-    returnNF_Tc (tcTyVarToTyVar tv')
+\begin{code}
+-- zonkType is used for Kinds as well
+
+-- For unbound, mutable tyvars, zonkType uses the function given to it
+-- For tyvars bound at a for-all, zonkType zonks them to an immutable
+--     type variable and zonks the kind too
 
--- zonkTcToType is used for Kinds as well
-zonkTcToType :: Type -> TyVarEnv Type -> TcType s -> NF_TcM s Type
-zonkTcToType unbound_var_ty env ty
+zonkType :: (TcTyVar -> NF_TcM Type)   -- What to do with unbound mutable type variables
+                                       -- see zonkTcType, and zonkTcTypeToType
+        -> TcType
+        -> NF_TcM Type
+zonkType unbound_var_fn ty
   = go ty
   where
     go (TyConApp tycon tys)      = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
@@ -354,6 +429,9 @@ zonkTcToType unbound_var_ty env ty
 
     go (NoteTy (FTVNote _) ty2)   = go ty2     -- Discard free-tyvar annotations
 
+    go (PredTy p)                = go_pred p           `thenNF_Tc` \ p' ->
+                                   returnNF_Tc (PredTy p')
+
     go (FunTy arg res)           = go arg              `thenNF_Tc` \ arg' ->
                                    go res              `thenNF_Tc` \ res' ->
                                    returnNF_Tc (FunTy arg' res')
@@ -362,29 +440,35 @@ zonkTcToType unbound_var_ty env ty
                                    go arg              `thenNF_Tc` \ arg' ->
                                    returnNF_Tc (mkAppTy fun' arg')
 
+    go (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
+                                    go ty               `thenNF_Tc` \ ty' ->
+                                    returnNF_Tc (mkUTy u' ty')
+
        -- 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}
+    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 
+    go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar  `thenNF_Tc` \ tyvar' ->
+                            go ty                      `thenNF_Tc` \ ty' ->
+                            returnNF_Tc (ForAllTy tyvar' ty')
+
+    go_pred (ClassP c tys) = mapNF_Tc go tys   `thenNF_Tc` \ tys' ->
+                            returnNF_Tc (ClassP c tys')
+    go_pred (IParam n ty) = go ty              `thenNF_Tc` \ ty' ->
+                           returnNF_Tc (IParam n ty')
+
+zonkTyVar :: (TcTyVar -> NF_TcM Type)          -- What to do for an unbound mutable variable
+         -> TcTyVar -> NF_TcM TcType
+zonkTyVar unbound_var_fn tyvar 
+  | not (isMutTyVar tyvar)     -- Not a mutable tyvar.  This can happen when
+                               -- zonking a forall type, when the bound type variable
+                               -- needn't be mutable
+  = ASSERT( isTyVar tyvar )            -- Should not be any immutable kind vars
+    returnNF_Tc (TyVarTy tyvar)
+
+  | otherwise
+  =  tcGetTyVar tyvar  `thenNF_Tc` \ maybe_ty ->
+     case maybe_ty of
+         Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
+         Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
+\end{code}