[project @ 1997-11-24 20:08:14 by sof]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index ed2794d..3c10a45 100644 (file)
@@ -1,57 +1,73 @@
 \begin{code}
-module TcType (
+#include "HsVersions.h"
 
-  TcTyVar(..),
+module TcType (
+  SYN_IE(TcIdBndr), TcIdOcc(..),
+       
+  -----------------------------------------
+  SYN_IE(TcTyVar),
+  SYN_IE(TcTyVarSet),
   newTcTyVar,
   newTyVarTy,  -- Kind -> NF_TcM s (TcType s)
   newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s]
 
-
-  TcTyVarSet(..),
-
   -----------------------------------------
-  TcType(..), TcMaybe(..),
-  TcTauType(..), TcThetaType(..), TcRhoType(..),
+  SYN_IE(TcType), TcMaybe(..),
+  SYN_IE(TcTauType), SYN_IE(TcThetaType), SYN_IE(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,
+  tcSplitForAllTy, tcSplitRhoTy,
 
---  zonkTcType,                -- TcType s     -> NF_TcM s (TcType s)
---  zonkTcTheta,       -- TcThetaType s -> NF_TcM s (TcThetaType s)
+  tcInstTyVars,
+  tcInstSigTyVars, 
+  tcInstType, tcInstSigType, tcInstTcType, tcInstSigTcType,
+  tcInstTheta, tcInstId,
 
-    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
+  zonkTcTyVars, zonkSigTyVar,
+  zonkTcType, zonkTcTheta,
+  zonkTcTypeToType,
+  zonkTcTyVar,
+  zonkTcTyVarToTyVar
 
   ) where
 
 
 
 -- friends:
-import Type    ( Type(..), ThetaType(..), GenType(..), tyVarsOfTypes, getTyVar_maybe )
-import TyVar   ( TyVar(..), GenTyVar(..), TyVarSet(..), GenTyVarSet(..), 
+import Type    ( SYN_IE(Type), SYN_IE(ThetaType), GenType(..),
+                 tyVarsOfTypes, getTyVar_maybe,
+                 splitForAllTy, splitRhoTy, isTyVarTy,
+                 mkForAllTys, instantiateTy
+               )
+import TyVar   ( SYN_IE(TyVar), GenTyVar(..), SYN_IE(TyVarSet), SYN_IE(GenTyVarSet), 
+                 SYN_IE(TyVarEnv), lookupTyVarEnv, addOneToTyVarEnv,
+                 nullTyVarEnv, mkTyVarEnv,
                  tyVarSetToList
                )
+import PprType ( GenType, GenTyVar )   -- Instances only
 
 -- others:
+import Class   ( GenClass, SYN_IE(Class) )
+import TyCon   ( isFunTyCon )
+import Id      ( idType, GenId, SYN_IE(Id) )
 import Kind    ( Kind )
-import Usage   ( Usage(..), GenUsage, UVar(..), duffUsage )
-import Class   ( GenClass )
 import TcKind  ( TcKind )
 import TcMonad
+import Usage   ( SYN_IE(Usage), GenUsage, SYN_IE(UVar), duffUsage )
 
-import Ubiq
+import TysPrim         ( voidTy )
+
+IMP_Ubiq()
+import Name            ( NamedThing(..) )
 import Unique          ( Unique )
 import UniqFM          ( UniqFM )
-import Name            ( getNameShortName )
 import Maybes          ( assocMaybe )
-import Util            ( panic )
+import Outputable      ( Outputable(..) )
+import Util            ( zipEqual, nOfThem, panic{-, pprPanic, pprTrace ToDo:rm-} )
 \end{code}
 
 
@@ -60,6 +76,26 @@ Data types
 ~~~~~~~~~~
 
 \begin{code}
+type TcIdBndr s = GenId  (TcType s)    -- Binders are all TcTypes
+data TcIdOcc  s = TcId   (TcIdBndr s)  -- Bindees may be either
+               | RealId Id
+
+instance Eq (TcIdOcc s) where
+  (TcId id1)   == (TcId id2)   = id1 == id2
+  (RealId id1) == (RealId id2) = id1 == id2
+  _           == _            = False
+
+instance Outputable (TcIdOcc s) where
+  ppr sty (TcId id)   = ppr sty id
+  ppr sty (RealId id) = ppr sty id
+
+instance NamedThing (TcIdOcc s) where
+  getName (TcId id)   = getName id
+  getName (RealId id) = getName id
+\end{code}
+
+
+\begin{code}
 type TcType s = GenType (TcTyVar s) UVar       -- Used during typechecker
        -- Invariant on ForAllTy in TcTypes:
        --      forall a. T
@@ -74,6 +110,12 @@ 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!
@@ -87,121 +129,221 @@ tcTyVarToTyVar :: TcTyVar s -> TyVar
 tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage
 \end{code}
 
+Utility functions
+~~~~~~~~~~~~~~~~~
+These tcSplit functions are like their non-Tc analogues, but they
+follow through bound type variables.
+
+\begin{code}
+tcSplitForAllTy :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
+tcSplitForAllTy t 
+  = go t t []
+  where
+    go syn_t (ForAllTy tv t) tvs = go t t (tv:tvs)
+    go syn_t (SynTy _ _ t)   tvs = go syn_t t tvs
+    go syn_t (TyVarTy tv)    tvs = tcReadTyVar tv      `thenNF_Tc` \ maybe_ty ->
+                                  case maybe_ty of
+                                       BoundTo ty | not (isTyVarTy ty) -> go syn_t ty tvs
+                                       other                           -> returnNF_Tc (reverse tvs, syn_t)
+    go syn_t t              tvs = returnNF_Tc (reverse tvs, syn_t)
+
+tcSplitRhoTy :: TcType s -> NF_TcM s ([(Class,TcType s)], TcType s)
+tcSplitRhoTy t
+  = go t t []
+ where
+    go syn_t (FunTy (DictTy c t _) r _) ts = go r r ((c,t):ts)
+    go syn_t (AppTy (AppTy (TyConTy tycon _) (DictTy c t _)) r) ts
+                             | isFunTyCon tycon
+                             = go r r ((c,t):ts)
+    go syn_t (SynTy _ _ 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
 ~~~~~~~~~~~~~~~~~~
 
 \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)
+    returnNF_Tc (TyVar uniq kind Nothing 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))
-
-tcInstTyVar :: TyVar -> NF_TcM s (TcTyVar s)
-tcInstTyVar tyvar@(TyVar uniq kind name _)
-  = newTcTyVar name kind
+newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
+
+
+-- For signature type variables, mark them as "DontBind"
+tcInstTyVars, tcInstSigTyVars
+       :: [GenTyVar flexi] 
+       -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)])
+
+tcInstTyVars    tyvars = inst_tyvars UnBound  tyvars
+tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars
+
+inst_tyvars initial_cts tyvars
+  = mapNF_Tc (inst_tyvar initial_cts) tyvars   `thenNF_Tc` \ tc_tyvars ->
+    let
+       tys = map TyVarTy tc_tyvars
+    in
+    returnNF_Tc (tc_tyvars, tys, zipEqual "inst_tyvars" tyvars tys)
+
+inst_tyvar initial_cts (TyVar _ kind name _) 
+  = tcGetUnique                `thenNF_Tc` \ uniq ->
+    tcNewMutVar initial_cts    `thenNF_Tc` \ box ->
+    returnNF_Tc (TyVar uniq kind Nothing box)
+       -- The "Nothing" means that it'll always print with its 
+       -- unique (or something similar).  If we leave the original (Just Name)
+       -- in there then error messages will say "can't match (T a) against (T a)"
 \end{code}
 
-@tcInstType@ and @tcInstTcType@ both create a fresh instance of a
+@tcInstType@ and @tcInstSigType@ both create a fresh instance of a
 type, returning a @TcType@. All inner for-alls are instantiated with
 fresh TcTyVars.
 
-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.
+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}
-tcInstType :: [(TyVar,TcType s)] -> Type  -> NF_TcM s (TcType s)
+tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
+tcInstTcType ty
+  = tcSplitForAllTy ty         `thenNF_Tc` \ (tyvars, rho) -> 
+    case tyvars of
+       []    -> returnNF_Tc ([], ty)   -- Nothing to do
+       other -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
+                returnNF_Tc (tyvars', instantiateTy tenv rho)
+
+tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
+tcInstSigTcType ty
+  = tcSplitForAllTy ty         `thenNF_Tc` \ (tyvars, rho) ->
+    case tyvars of
+       []    -> returnNF_Tc ([], ty)   -- Nothing to do
+       other -> tcInstSigTyVars tyvars         `thenNF_Tc` \ (tyvars', _, tenv)  ->
+                returnNF_Tc (tyvars', instantiateTy tenv rho)
+    
+tcInstType :: [(GenTyVar flexi,TcType s)] 
+          -> GenType (GenTyVar flexi) UVar 
+          -> NF_TcM s (TcType s)
 tcInstType tenv ty_to_inst
-  = do [(uniq,ty) | (TyVar uniq _ _ _, ty) <- tenv] ty_to_inst
+  = tcConvert bind_fn occ_fn (mkTyVarEnv 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)
+    bind_fn = inst_tyvar UnBound
+    occ_fn env tyvar = case lookupTyVarEnv env tyvar of
+                        Just ty -> returnNF_Tc ty
+                        Nothing -> panic "tcInstType:1" --(vcat [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"-- (vcat [ppr PprDebug ty_to_inst, 
+                                                       --            ppr PprDebug tyvar])
 
-    do env (AppTy fun arg)       = do env fun          `thenNF_Tc` \ fun' ->
-                                   do env arg          `thenNF_Tc` \ arg' ->
-                                   returnNF_Tc (AppTy fun' arg')
+zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
+zonkTcTyVarToTyVar tv
+  = zonkTcTyVar tv     `thenNF_Tc` \ tv_ty ->
+    case tv_ty of      -- Should be a tyvar!
 
-    do env (DictTy clas ty usage)= do env ty           `thenNF_Tc` \ ty' ->
-                                  returnNF_Tc (DictTy clas ty' usage)
+      TyVarTy tv' ->    returnNF_Tc (tcTyVarToTyVar tv')
 
-    do env (TyVarTy (TyVar uniq kind name _))
-       = case assocMaybe env uniq of
-               Just tc_ty -> returnNF_Tc tc_ty
-               Nothing    -> panic "tcInstType"
+      _ -> --pprTrace "zonkTcTyVarToTyVar:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
+          returnNF_Tc (tcTyVarToTyVar tv)
 
-    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
+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
 
-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
+tcConvert bind_fn occ_fn env ty_to_convert
+  = doo env ty_to_convert
   where
-    do env ty@(TyConTy tycon usage) = returnNF_Tc ty
+    doo env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage)
 
--- 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' ->
+    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')
 
-    do env (FunTy arg res usage)  = do env arg         `thenNF_Tc` \ arg' ->
-                                   do env res          `thenNF_Tc` \ res' ->
-                                   returnNF_Tc (FunTy arg' res' usage)
+    doo env (FunTy arg res usage) = doo env arg                `thenNF_Tc` \ arg' ->
+                                  doo 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')
+    doo env (AppTy fun arg)     = doo env fun          `thenNF_Tc` \ fun' ->
+                                  doo env arg          `thenNF_Tc` \ arg' ->
+                                  returnNF_Tc (AppTy fun' arg')
 
-    do env (DictTy clas ty usage)= do env ty           `thenNF_Tc` \ ty' ->
+    doo env (DictTy clas ty usage)= doo env ty         `thenNF_Tc` \ ty' ->
                                   returnNF_Tc (DictTy clas ty' usage)
 
-    do env ty@(TyVarTy (TyVar uniq kind name _))
-       = case assocMaybe env uniq of
-               Just tc_ty -> returnNF_Tc tc_ty
-               Nothing    -> returnNF_Tc ty
+    doo env (ForAllUsageTy u us ty) = doo env ty       `thenNF_Tc` \ ty' ->
+                                    returnNF_Tc (ForAllUsageTy u us ty')
 
-    do env (ForAllTy (TyVar uniq kind name _) ty)
-       = newTcTyVar name kind  `thenNF_Tc` \ tc_tyvar ->
+       -- 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 = (uniq, TyVarTy tc_tyvar) : env
+               new_env = addOneToTyVarEnv env tyvar (TyVarTy tyvar')
          in
-         do new_env ty `thenNF_Tc` \ ty' ->
-         returnNF_Tc (ForAllTy tc_tyvar ty')
+         doo new_env ty                `thenNF_Tc` \ ty' ->
+         returnNF_Tc (ForAllTy 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)
+
+-- 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)         --
+
+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')
 \end{code}
 
 Reading and writing TcTyVars
@@ -232,91 +374,94 @@ We return Nothing iff the original box was unbound.
 tcReadTyVar (TyVar uniq kind name box)
   = 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
+
 short_out :: TcType s -> NF_TcM s (TcType s)
 short_out ty@(TyVarTy (TyVar uniq kind name box))
   = 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
+
 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.
-
 \begin{code}
-zonkTcTypeToType :: TcType s -> NF_TcM s Type
-zonkTcTypeToType ty = zonk tcTyVarToTyVar ty
-
-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 ->
+  = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars)       `thenNF_Tc` \ tys ->
     returnNF_Tc (tyVarsOfTypes tys)
 
-zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
-zonkTcTyVarToTyVar tyvar
-  = zonk_tv_to_tv tcTyVarToTyVar tyvar
+zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
+zonkTcTyVar 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)
+
+-- Signature type variables only get bound to each other,
+-- never to a type
+zonkSigTyVar :: TcTyVar s -> NF_TcM s (TcTyVar s)
+zonkSigTyVar tyvar 
+  = tcReadTyVar tyvar          `thenNF_Tc` \ maybe_ty ->
+    case maybe_ty of
+       BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc tyvar'       -- tcReadTyVar never returns a bound tyvar
+       BoundTo other               -> panic "zonkSigTyVar"     -- Should only be bound to another tyvar
+       other                       -> returnNF_Tc tyvar
 
+zonkTcType :: TcType s -> NF_TcM s (TcType s)
 
-zonk tyvar_fn (TyVarTy tyvar)
-  = zonk_tv tyvar_fn tyvar
+zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
 
-zonk tyvar_fn (AppTy ty1 ty2)
-  = zonk tyvar_fn ty1          `thenNF_Tc` \ ty1' ->
-    zonk tyvar_fn ty2          `thenNF_Tc` \ ty2' ->
+zonkTcType (AppTy ty1 ty2)
+  = zonkTcType ty1             `thenNF_Tc` \ ty1' ->
+    zonkTcType ty2             `thenNF_Tc` \ ty2' ->
     returnNF_Tc (AppTy ty1' ty2')
 
-zonk tyvar_fn (TyConTy tc u)
+zonkTcType (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' ->
+zonkTcType (SynTy tc tys ty)
+  = mapNF_Tc zonkTcType tys    `thenNF_Tc` \ tys' ->
+    zonkTcType 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')
-
-zonk tyvar_fn (ForAllUsageTy uv uvs ty)
+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:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
+          
+          returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
+
+zonkTcType (ForAllUsageTy uv uvs ty)
   = panic "zonk:ForAllUsageTy"
 
-zonk tyvar_fn (FunTy ty1 ty2 u)
-  = zonk tyvar_fn ty1          `thenNF_Tc` \ ty1' ->
-    zonk tyvar_fn ty2          `thenNF_Tc` \ ty2' ->
+zonkTcType (FunTy ty1 ty2 u)
+  = zonkTcType ty1             `thenNF_Tc` \ ty1' ->
+    zonkTcType ty2             `thenNF_Tc` \ ty2' ->
     returnNF_Tc (FunTy ty1' ty2' u)
 
-zonk tyvar_fn (DictTy c ty u)
-  = zonk tyvar_fn ty           `thenNF_Tc` \ ty' ->
+zonkTcType (DictTy c ty u)
+  = zonkTcType ty              `thenNF_Tc` \ ty' ->
     returnNF_Tc (DictTy c ty' u)
 
 
-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
-
-
-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
+zonkTcTheta  theta = mapNF_Tc zonk theta
+       where
+         zonk (c,t) = zonkTcType t     `thenNF_Tc` \ t' ->
+                      returnNF_Tc (c,t')
 \end{code}