Simon's big boxy-type commit
[ghc-hetmet.git] / ghc / compiler / typecheck / TcHsSyn.lhs
index 00eb754..3bf8b4a 100644 (file)
@@ -1,5 +1,5 @@
 %
-% (c) The AQUA Project, Glasgow University, 1996
+% (c) The AQUA Project, Glasgow University, 1996-1998
 %
 \section[TcHsSyn]{Specialisations of the @HsSyn@ syntax for the typechecker}
 
@@ -7,140 +7,99 @@ This module is an extension of @HsSyn@ syntax, for use in the type
 checker.
 
 \begin{code}
-#include "HsVersions.h"
-
 module TcHsSyn (
-       SYN_IE(TcIdBndr), TcIdOcc(..),
+       mkHsTyApp, mkHsDictApp, mkHsConApp,
+       mkHsTyLam, mkHsDictLam, mkHsDictLet, mkHsApp,
+       hsLitType, hsPatType, mkHsAppTy, mkSimpleHsAlt,
+       nlHsIntLit, 
        
-       SYN_IE(TcMonoBinds), SYN_IE(TcHsBinds), SYN_IE(TcBind), SYN_IE(TcPat),
-       SYN_IE(TcExpr), SYN_IE(TcGRHSsAndBinds), SYN_IE(TcGRHS), SYN_IE(TcMatch),
-       SYN_IE(TcQual), SYN_IE(TcStmt), SYN_IE(TcArithSeqInfo), SYN_IE(TcRecordBinds),
-       SYN_IE(TcHsModule),
-       
-       SYN_IE(TypecheckedHsBinds), SYN_IE(TypecheckedBind),
-       SYN_IE(TypecheckedMonoBinds), SYN_IE(TypecheckedPat),
-       SYN_IE(TypecheckedHsExpr), SYN_IE(TypecheckedArithSeqInfo),
-       SYN_IE(TypecheckedQual), SYN_IE(TypecheckedStmt),
-       SYN_IE(TypecheckedMatch), SYN_IE(TypecheckedHsModule),
-       SYN_IE(TypecheckedGRHSsAndBinds), SYN_IE(TypecheckedGRHS),
-       SYN_IE(TypecheckedRecordBinds),
-
-       mkHsTyApp, mkHsDictApp,
-       mkHsTyLam, mkHsDictLam,
-       tcIdType, tcIdTyVars,
-
-       zonkBinds,
-       zonkDictBinds
+
+       -- re-exported from TcMonad
+       TcId, TcIdSet, TcDictBinds,
+
+       zonkTopDecls, zonkTopExpr, zonkTopLExpr,
+       zonkId, zonkTopBndrs
   ) where
 
-IMP_Ubiq(){-uitous-}
+#include "HsVersions.h"
 
 -- friends:
 import HsSyn   -- oodles of it
-import Id      ( GenId(..), IdDetails, -- Can meddle modestly with Ids
-                 SYN_IE(DictVar), idType,
-                 SYN_IE(IdEnv), growIdEnvList, lookupIdEnv
-               )
 
 -- others:
-import Name    ( Name{--O only-} )
-import TcMonad hiding ( rnMtoTcM )
-import TcType  ( SYN_IE(TcType), TcMaybe, SYN_IE(TcTyVar),
-                 zonkTcTypeToType, zonkTcTyVarToTyVar
-               )
-import Usage   ( SYN_IE(UVar) )
-import Util    ( zipEqual, panic, pprPanic, pprTrace )
-
-import PprType  ( GenType, GenTyVar )  -- instances
-import Type    ( mkTyVarTy, tyVarsOfType )
-import TyVar   ( GenTyVar {- instances -},
-                 SYN_IE(TyVarEnv), growTyVarEnvList, emptyTyVarSet )
-import TysPrim ( voidTy )
-import Unique  ( Unique )              -- instances
-import UniqFM
-import PprStyle
-import Pretty
-\end{code}
-
-
-Type definitions
-~~~~~~~~~~~~~~~~
-
-The @Tc...@ datatypes are the ones that apply {\em during} type checking.
-All the types in @Tc...@ things have mutable type-variables in them for
-unification.
-
-At the end of type checking we zonk everything to @Typechecked...@ datatypes,
-which have immutable type variables in them.
-
-\begin{code}
-type TcIdBndr s = GenId  (TcType s)    -- Binders are all TcTypes
-data TcIdOcc  s = TcId   (TcIdBndr s)  -- Bindees may be either
-               | RealId Id
-
-type TcHsBinds s       = HsBinds (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcBind s          = Bind (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcMonoBinds s     = MonoBinds (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcPat s           = OutPat (TcTyVar s) UVar (TcIdOcc s)
-type TcExpr s          = HsExpr (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcGRHSsAndBinds s = GRHSsAndBinds (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcGRHS s          = GRHS (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcMatch s         = Match (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcQual s          = Qualifier (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcStmt s          = Stmt (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcArithSeqInfo s  = ArithSeqInfo (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcRecordBinds s   = HsRecordBinds (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-type TcHsModule s      = HsModule (TcTyVar s) UVar (TcIdOcc s) (TcPat s)
-
-type TypecheckedPat            = OutPat        TyVar UVar Id
-type TypecheckedMonoBinds      = MonoBinds     TyVar UVar Id TypecheckedPat
-type TypecheckedHsBinds                = HsBinds       TyVar UVar Id TypecheckedPat
-type TypecheckedBind           = Bind          TyVar UVar Id TypecheckedPat
-type TypecheckedHsExpr         = HsExpr        TyVar UVar Id TypecheckedPat
-type TypecheckedArithSeqInfo   = ArithSeqInfo  TyVar UVar Id TypecheckedPat
-type TypecheckedQual           = Qualifier     TyVar UVar Id TypecheckedPat
-type TypecheckedStmt           = Stmt          TyVar UVar Id TypecheckedPat
-type TypecheckedMatch          = Match         TyVar UVar Id TypecheckedPat
-type TypecheckedGRHSsAndBinds  = GRHSsAndBinds TyVar UVar Id TypecheckedPat
-type TypecheckedGRHS           = GRHS          TyVar UVar Id TypecheckedPat
-type TypecheckedRecordBinds    = HsRecordBinds TyVar UVar Id TypecheckedPat
-type TypecheckedHsModule       = HsModule      TyVar UVar Id TypecheckedPat
+import Id      ( idType, setIdType, Id )
+
+import TcRnMonad
+import Type      ( Type )
+import TcType    ( TcType, TcTyVar, mkTyVarTy, mkTyConApp, isImmutableTyVar )
+import Kind      ( isLiftedTypeKind, liftedTypeKind, isSubKind )
+import qualified  Type
+import TcMType   ( zonkQuantifiedTyVar, zonkType, zonkTcType, writeMetaTyVar )
+import TysPrim   ( charPrimTy, intPrimTy, floatPrimTy,
+                   doublePrimTy, addrPrimTy
+                 )
+import TysWiredIn ( charTy, stringTy, intTy, 
+                   mkListTy, mkPArrTy, mkTupleTy, unitTy,
+                   voidTy, listTyCon, tupleTyCon )
+import TyCon     ( mkPrimTyCon, tyConKind, PrimRep(..) )
+import Kind      ( splitKindFunTys )
+import Name      ( Name, getOccName, mkInternalName, mkDerivedTyConOcc )
+import Var       ( Var, isId, isLocalVar, tyVarKind )
+import VarSet
+import VarEnv
+import BasicTypes ( Boxity(..), IPName(..), ipNameName, mapIPName )
+import Maybes    ( orElse )
+import Unique    ( Uniquable(..) )
+import SrcLoc    ( noSrcLoc, noLoc, Located(..), unLoc )
+import Util      ( mapSnd )
+import Bag
+import Outputable
 \end{code}
 
-\begin{code}
-mkHsTyApp expr []  = expr
-mkHsTyApp expr tys = TyApp expr tys
 
-mkHsDictApp expr []     = expr
-mkHsDictApp expr dict_vars = DictApp expr dict_vars
-
-mkHsTyLam []     expr = expr
-mkHsTyLam tyvars expr = TyLam tyvars expr
-
-mkHsDictLam []    expr = expr
-mkHsDictLam dicts expr = DictLam dicts expr
-
-tcIdType :: TcIdOcc s -> TcType s
-tcIdType (TcId   id) = idType id
-tcIdType (RealId id) = pprPanic "tcIdType:" (ppr PprDebug id)
-
-tcIdTyVars (TcId id)  = tyVarsOfType (idType id)
-tcIdTyVars (RealId _) = emptyTyVarSet          -- Top level Ids have no free type variables
-\end{code}
+%************************************************************************
+%*                                                                     *
+\subsection[mkFailurePair]{Code for pattern-matching and other failures}
+%*                                                                     *
+%************************************************************************
 
+Note: If @hsPatType@ doesn't bear a strong resemblance to @exprType@,
+then something is wrong.
 \begin{code}
-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
+hsPatType :: OutPat Id -> Type
+hsPatType pat = pat_type (unLoc pat)
+
+pat_type (ParPat pat)             = hsPatType pat
+pat_type (WildPat ty)             = ty
+pat_type (VarPat var)             = idType var
+pat_type (VarPatOut var _)        = idType var
+pat_type (LazyPat pat)            = hsPatType pat
+pat_type (LitPat lit)             = hsLitType lit
+pat_type (AsPat var pat)          = idType (unLoc var)
+pat_type (ListPat _ ty)                   = mkListTy ty
+pat_type (PArrPat _ ty)                   = mkPArrTy ty
+pat_type (TuplePat pats box)      = mkTupleTy box (length pats) (map hsPatType pats)
+pat_type (ConPatOut _ _ _ _ _ ty)  = ty
+pat_type (SigPatOut pat ty)       = ty
+pat_type (NPat lit _ _ ty)        = ty
+pat_type (NPlusKPat id _ _ _)      = idType (unLoc id)
+pat_type (DictPat ds ms)           = case (ds ++ ms) of
+                                      []  -> unitTy
+                                      [d] -> idType d
+                                      ds  -> mkTupleTy Boxed (length ds) (map idType ds)
+
+
+hsLitType :: HsLit -> TcType
+hsLitType (HsChar c)       = charTy
+hsLitType (HsCharPrim c)   = charPrimTy
+hsLitType (HsString str)   = stringTy
+hsLitType (HsStringPrim s) = addrPrimTy
+hsLitType (HsInt i)       = intTy
+hsLitType (HsIntPrim i)    = intPrimTy
+hsLitType (HsInteger i ty) = ty
+hsLitType (HsRat _ ty)    = ty
+hsLitType (HsFloatPrim f)  = floatPrimTy
+hsLitType (HsDoublePrim d) = doublePrimTy
 \end{code}
 
 
@@ -150,192 +109,234 @@ instance NamedThing (TcIdOcc s) where
 %*                                                                     *
 %************************************************************************
 
-This zonking pass runs over the bindings
+\begin{code}
+-- zonkId is used *during* typechecking just to zonk the Id's type
+zonkId :: TcId -> TcM TcId
+zonkId id
+  = zonkTcType (idType id) `thenM` \ ty' ->
+    returnM (setIdType id ty')
+\end{code}
+
+The rest of the zonking is done *after* typechecking.
+The main zonking pass runs over the bindings
 
  a) to convert TcTyVars to TyVars etc, dereferencing any bindings etc
  b) convert unbound TcTyVar to Void
+ c) convert each TcId to an Id by zonking its type
+
+The type variables are converted by binding mutable tyvars to immutable ones
+and then zonking as normal.
 
-We pass an environment around so that
- a) we know which TyVars are unbound
- b) we maintain sharing; eg an Id is zonked at its binding site and they
-    all occurrences of that Id point to the common zonked copy
+The Ids are converted by binding them in the normal Tc envt; that
+way we maintain sharing; eg an Id is zonked at its binding site and they
+all occurrences of that Id point to the common zonked copy
 
 It's all pretty boring stuff, because HsSyn is such a large type, and 
 the environment manipulation is tiresome.
 
-
 \begin{code}
-zonkIdBndr :: TyVarEnv Type -> TcIdOcc s -> NF_TcM s Id
-zonkIdBndr te (TcId (Id u n ty details prags info))
-  = zonkTcTypeToType te ty     `thenNF_Tc` \ ty' ->
-    returnNF_Tc (Id u n ty' details prags info)
-
-zonkIdBndr te (RealId id) = returnNF_Tc id
-
-zonkIdOcc :: IdEnv Id -> TcIdOcc s -> Id
-zonkIdOcc ve (RealId id) = id
-zonkIdOcc ve (TcId id)   = case (lookupIdEnv ve id) of
-                               Just id' -> id'
-                               Nothing  -> pprTrace "zonkIdOcc: " (ppr PprDebug id) $
-                                           Id u n voidTy details prags info
-                                        where
-                                           Id u n _ details prags info = id
-
-extend_ve ve ids    = growIdEnvList ve [(id,id) | id <- ids]
-extend_te te tyvars = growTyVarEnvList te [(tyvar, mkTyVarTy tyvar) | tyvar <- tyvars]
+data ZonkEnv = ZonkEnv (TcType -> TcM Type)    -- How to zonk a type
+                       (IdEnv Id)              -- What variables are in scope
+       -- Maps an Id to its zonked version; both have the same Name
+       -- Is only consulted lazily; hence knot-tying
+
+emptyZonkEnv = ZonkEnv zonkTypeZapping emptyVarEnv
+
+extendZonkEnv :: ZonkEnv -> [Id] -> ZonkEnv
+extendZonkEnv (ZonkEnv zonk_ty env) ids 
+  = ZonkEnv zonk_ty (extendVarEnvList env [(id,id) | id <- ids])
+
+extendZonkEnv1 :: ZonkEnv -> Id -> ZonkEnv
+extendZonkEnv1 (ZonkEnv zonk_ty env) id 
+  = ZonkEnv zonk_ty (extendVarEnv env id id)
+
+setZonkType :: ZonkEnv -> (TcType -> TcM Type) -> ZonkEnv
+setZonkType (ZonkEnv _ env) zonk_ty = ZonkEnv zonk_ty env
+
+zonkEnvIds :: ZonkEnv -> [Id]
+zonkEnvIds (ZonkEnv _ env) = varEnvElts env
+
+zonkIdOcc :: ZonkEnv -> TcId -> Id
+-- Ids defined in this module should be in the envt; 
+-- ignore others.  (Actually, data constructors are also
+-- not LocalVars, even when locally defined, but that is fine.)
+-- (Also foreign-imported things aren't currently in the ZonkEnv;
+--  that's ok because they don't need zonking.)
+--
+-- Actually, Template Haskell works in 'chunks' of declarations, and
+-- an earlier chunk won't be in the 'env' that the zonking phase 
+-- carries around.  Instead it'll be in the tcg_gbl_env, already fully
+-- zonked.  There's no point in looking it up there (except for error 
+-- checking), and it's not conveniently to hand; hence the simple
+-- 'orElse' case in the LocalVar branch.
+--
+-- Even without template splices, in module Main, the checking of
+-- 'main' is done as a separate chunk.
+zonkIdOcc (ZonkEnv zonk_ty env) id 
+  | isLocalVar id = lookupVarEnv env id `orElse` id
+  | otherwise    = id
+
+zonkIdOccs env ids = map (zonkIdOcc env) ids
+
+-- zonkIdBndr is used *after* typechecking to get the Id's type
+-- to its final form.  The TyVarEnv give 
+zonkIdBndr :: ZonkEnv -> TcId -> TcM Id
+zonkIdBndr env id
+  = zonkTcTypeToType env (idType id)   `thenM` \ ty' ->
+    returnM (setIdType id ty')
+
+zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id]
+zonkIdBndrs env ids = mappM (zonkIdBndr env) ids
+
+zonkTopBndrs :: [TcId] -> TcM [Id]
+zonkTopBndrs ids = zonkIdBndrs emptyZonkEnv ids
 \end{code}
 
-\begin{code}
-       -- Implicitly mutually recursive, which is overkill,
-       -- but it means that later ones see earlier ones
-zonkDictBinds te ve dbs 
-  = fixNF_Tc (\ ~(_,new_ve) ->
-       zonkDictBindsLocal te new_ve dbs        `thenNF_Tc` \ (new_binds, dict_ids) ->
-        returnNF_Tc (new_binds, extend_ve ve dict_ids)
-    )
-
-       -- The ..Local version assumes the caller has set up
-       -- a ve that contains all the things bound here
-zonkDictBindsLocal te ve [] = returnNF_Tc ([], [])
-
-zonkDictBindsLocal te ve ((dict,rhs) : binds)
-  = zonkIdBndr te dict                 `thenNF_Tc` \ new_dict ->
-    zonkExpr te ve rhs                 `thenNF_Tc` \ new_rhs ->
-    zonkDictBindsLocal te ve binds     `thenNF_Tc` \ (new_binds, dict_ids) ->
-    returnNF_Tc ((new_dict,new_rhs) : new_binds, 
-                new_dict:dict_ids)
-\end{code}
 
 \begin{code}
-zonkBinds :: TyVarEnv Type -> IdEnv Id 
-         -> TcHsBinds s -> NF_TcM s (TypecheckedHsBinds, IdEnv Id)
-
-zonkBinds te ve EmptyBinds = returnNF_Tc (EmptyBinds, ve)
-
-zonkBinds te ve (ThenBinds binds1 binds2)
-  = zonkBinds te ve binds1   `thenNF_Tc` \ (new_binds1, ve1) ->
-    zonkBinds te ve1 binds2  `thenNF_Tc` \ (new_binds2, ve2) ->
-    returnNF_Tc (ThenBinds new_binds1 new_binds2, ve2)
-
-zonkBinds te ve (SingleBind bind)
-  = fixNF_Tc (\ ~(_,new_ve) ->
-       zonkBind te new_ve bind  `thenNF_Tc` \ (new_bind, new_ids) ->
-       returnNF_Tc (SingleBind new_bind, extend_ve ve new_ids)
-    )
-
-zonkBinds te ve (AbsBinds tyvars dicts locprs dict_binds val_bind)
-  = mapNF_Tc zonkTcTyVarToTyVar tyvars `thenNF_Tc` \ new_tyvars ->
+zonkTopExpr :: HsExpr TcId -> TcM (HsExpr Id)
+zonkTopExpr e = zonkExpr emptyZonkEnv e
+
+zonkTopLExpr :: LHsExpr TcId -> TcM (LHsExpr Id)
+zonkTopLExpr e = zonkLExpr emptyZonkEnv e
+
+zonkTopDecls :: LHsBinds TcId -> [LRuleDecl TcId] -> [LForeignDecl TcId]
+            -> TcM ([Id], 
+                    Bag (LHsBind  Id),
+                    [LForeignDecl Id],
+                    [LRuleDecl    Id])
+zonkTopDecls binds rules fords
+  = do { (env, binds') <- zonkRecMonoBinds emptyZonkEnv binds
+                       -- Top level is implicitly recursive
+       ; rules' <- zonkRules env rules
+       ; fords' <- zonkForeignExports env fords
+       ; return (zonkEnvIds env, binds', fords', rules') }
+
+---------------------------------------------
+zonkLocalBinds :: ZonkEnv -> HsLocalBinds TcId -> TcM (ZonkEnv, HsLocalBinds Id)
+zonkLocalBinds env EmptyLocalBinds
+  = return (env, EmptyLocalBinds)
+
+zonkLocalBinds env (HsValBinds binds)
+  = do { (env1, new_binds) <- zonkValBinds env binds
+       ; return (env1, HsValBinds new_binds) }
+
+zonkLocalBinds env (HsIPBinds (IPBinds binds dict_binds))
+  = mappM (wrapLocM zonk_ip_bind) binds        `thenM` \ new_binds ->
     let
-       new_te = extend_te te new_tyvars
+       env1 = extendZonkEnv env [ipNameName n | L _ (IPBind n _) <- new_binds]
     in
-    mapNF_Tc (zonkIdBndr new_te) dicts         `thenNF_Tc` \ new_dicts ->
-    mapNF_Tc (zonkIdBndr new_te) globals       `thenNF_Tc` \ new_globals ->
-    let
-       ve1 = extend_ve ve  new_globals
-        ve2 = extend_ve ve1 new_dicts
-    in
-    fixNF_Tc (\ ~(_, ve3) ->
-       zonkDictBindsLocal new_te ve3 dict_binds  `thenNF_Tc` \ (new_dict_binds, ds) ->
-       zonkBind new_te ve3 val_bind              `thenNF_Tc` \ (new_val_bind, ls) ->
+    zonkRecMonoBinds env1 dict_binds   `thenM` \ (env2, new_dict_binds) -> 
+    returnM (env2, HsIPBinds (IPBinds new_binds new_dict_binds))
+  where
+    zonk_ip_bind (IPBind n e)
+       = mapIPNameTc (zonkIdBndr env) n        `thenM` \ n' ->
+         zonkLExpr env e                       `thenM` \ e' ->
+         returnM (IPBind n' e')
+
+
+---------------------------------------------
+zonkValBinds :: ZonkEnv -> HsValBinds TcId -> TcM (ZonkEnv, HsValBinds Id)
+zonkValBinds env bs@(ValBindsIn _ _) 
+  = panic "zonkValBinds"       -- Not in typechecker output
+zonkValBinds env (ValBindsOut binds sigs) 
+  = do         { (env1, new_binds) <- go env binds
+       ; return (env1, ValBindsOut new_binds sigs) }
+  where
+    go env []         = return (env, [])
+    go env ((r,b):bs) = do { (env1, b')  <- zonkRecMonoBinds env b
+                          ; (env2, bs') <- go env1 bs
+                          ; return (env2, (r,b'):bs') }
+
+---------------------------------------------
+zonkRecMonoBinds :: ZonkEnv -> LHsBinds TcId -> TcM (ZonkEnv, LHsBinds Id)
+zonkRecMonoBinds env binds 
+ = fixM (\ ~(_, new_binds) -> do 
+       { let env1 = extendZonkEnv env (collectHsBindBinders new_binds)
+        ; binds' <- zonkMonoBinds env1 binds
+        ; return (env1, binds') })
+
+---------------------------------------------
+zonkMonoBinds :: ZonkEnv -> LHsBinds TcId -> TcM (LHsBinds Id)
+zonkMonoBinds env binds = mapBagM (wrapLocM (zonk_bind env)) binds
+
+zonk_bind :: ZonkEnv -> HsBind TcId -> TcM (HsBind Id)
+zonk_bind env bind@(PatBind { pat_lhs = pat, pat_rhs = grhss, pat_rhs_ty = ty})
+  = do { (_env, new_pat) <- zonkPat env pat            -- Env already extended
+       ; new_grhss <- zonkGRHSs env grhss
+       ; new_ty    <- zonkTcTypeToType env ty
+       ; return (bind { pat_lhs = new_pat, pat_rhs = new_grhss, pat_rhs_ty = new_ty }) }
+
+zonk_bind env (VarBind { var_id = var, var_rhs = expr })
+  = zonkIdBndr env var                         `thenM` \ new_var ->
+    zonkLExpr env expr                 `thenM` \ new_expr ->
+    returnM (VarBind { var_id = new_var, var_rhs = new_expr })
+
+zonk_bind env bind@(FunBind { fun_id = var, fun_matches = ms, fun_co_fn = co_fn })
+  = wrapLocM (zonkIdBndr env) var      `thenM` \ new_var ->
+    zonkCoFn env co_fn                 `thenM` \ (env1, new_co_fn) ->
+    zonkMatchGroup env1 ms             `thenM` \ new_ms ->
+    returnM (bind { fun_id = new_var, fun_matches = new_ms, fun_co_fn = new_co_fn })
+
+zonk_bind env (AbsBinds { abs_tvs = tyvars, abs_dicts = dicts, 
+                         abs_exports = exports, abs_binds = val_binds })
+  = ASSERT( all isImmutableTyVar tyvars )
+    zonkIdBndrs env dicts              `thenM` \ new_dicts ->
+    fixM (\ ~(new_val_binds, _) ->
        let
-           new_locprs = zipEqual "zonkBinds" (map (zonkIdOcc ve3) locals) new_globals
-        in
-        returnNF_Tc (AbsBinds new_tyvars new_dicts new_locprs new_dict_binds new_val_bind,
-                    extend_ve ve2 (ds++ls))
-    )                                          `thenNF_Tc` \ (binds, _) ->
-    returnNF_Tc (binds, ve1)   -- Yes, the "ve1" is right (SLPJ)
+         env1 = extendZonkEnv env new_dicts
+         env2 = extendZonkEnv env1 (collectHsBindBinders new_val_binds)
+       in
+       zonkMonoBinds env2 val_binds            `thenM` \ new_val_binds ->
+        mappM (zonkExport env2) exports                `thenM` \ new_exports ->
+       returnM (new_val_binds, new_exports)
+    )                                          `thenM` \ (new_val_bind, new_exports) ->
+    returnM (AbsBinds { abs_tvs = tyvars, abs_dicts = new_dicts, 
+                       abs_exports = new_exports, abs_binds = new_val_bind })
   where
-    (locals, globals) = unzip locprs
-\end{code}
-
-\begin{code}
--------------------------------------------------------------------------
-zonkBind :: TyVarEnv Type -> IdEnv Id 
-        -> TcBind s -> NF_TcM s (TypecheckedBind, [Id])
-
-zonkBind te ve EmptyBind = returnNF_Tc (EmptyBind, [])
-
-zonkBind te ve (NonRecBind mbinds)
-  = zonkMonoBinds te ve mbinds `thenNF_Tc` \ (new_mbinds, new_ids) ->
-    returnNF_Tc (NonRecBind new_mbinds, new_ids)
-
-zonkBind te ve (RecBind mbinds)
-  = zonkMonoBinds te ve mbinds `thenNF_Tc` \ (new_mbinds, new_ids) ->
-    returnNF_Tc (RecBind new_mbinds, new_ids)
-
--------------------------------------------------------------------------
-zonkMonoBinds :: TyVarEnv Type -> IdEnv Id 
-             -> TcMonoBinds s -> NF_TcM s (TypecheckedMonoBinds, [Id])
-
-zonkMonoBinds te ve EmptyMonoBinds = returnNF_Tc (EmptyMonoBinds, [])
-
-zonkMonoBinds te ve (AndMonoBinds mbinds1 mbinds2)
-  = zonkMonoBinds te ve mbinds1  `thenNF_Tc` \ (new_mbinds1, ids1) ->
-    zonkMonoBinds te ve mbinds2  `thenNF_Tc` \ (new_mbinds2, ids2) ->
-    returnNF_Tc (AndMonoBinds new_mbinds1 new_mbinds2, ids1 ++ ids2)
-
-zonkMonoBinds te ve (PatMonoBind pat grhss_w_binds locn)
-  = zonkPat te ve pat                          `thenNF_Tc` \ (new_pat, ids) ->
-    zonkGRHSsAndBinds te ve grhss_w_binds      `thenNF_Tc` \ new_grhss_w_binds ->
-    returnNF_Tc (PatMonoBind new_pat new_grhss_w_binds locn, ids)
-
-zonkMonoBinds te ve (VarMonoBind var expr)
-  = zonkIdBndr te var          `thenNF_Tc` \ new_var ->
-    zonkExpr te ve expr                `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (VarMonoBind new_var new_expr, [new_var])
-
-zonkMonoBinds te ve (FunMonoBind var inf ms locn)
-  = zonkIdBndr te var                  `thenNF_Tc` \ new_var ->
-    mapNF_Tc (zonkMatch te ve) ms      `thenNF_Tc` \ new_ms ->
-    returnNF_Tc (FunMonoBind new_var inf new_ms locn, [new_var])
+    zonkExport env (tyvars, global, local, prags)
+       = zonkIdBndr env global                 `thenM` \ new_global ->
+         mapM zonk_prag prags                  `thenM` \ new_prags -> 
+         returnM (tyvars, new_global, zonkIdOcc env local, new_prags)
+    zonk_prag prag@(InlinePrag {})  = return prag
+    zonk_prag (SpecPrag expr ty ds inl) = do { expr' <- zonkExpr env expr 
+                                            ; ty'   <- zonkTcTypeToType env ty
+                                            ; let ds' = zonkIdOccs env ds
+                                            ; return (SpecPrag expr' ty' ds' inl) }
 \end{code}
 
 %************************************************************************
 %*                                                                     *
-\subsection[BackSubst-Match-GRHSs]{Match and GRHSsAndBinds}
+\subsection[BackSubst-Match-GRHSs]{Match and GRHSs}
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
-zonkMatch :: TyVarEnv Type -> IdEnv Id 
-         -> TcMatch s -> NF_TcM s TypecheckedMatch
-
-zonkMatch te ve (PatMatch pat match)
-  = zonkPat te ve pat          `thenNF_Tc` \ (new_pat, ids) ->
-    let
-       new_ve = extend_ve ve ids
-    in
-    zonkMatch te new_ve match          `thenNF_Tc` \ new_match ->
-    returnNF_Tc (PatMatch new_pat new_match)
-
-zonkMatch te ve (GRHSMatch grhss_w_binds)
-  = zonkGRHSsAndBinds te ve grhss_w_binds `thenNF_Tc` \ new_grhss_w_binds ->
-    returnNF_Tc (GRHSMatch new_grhss_w_binds)
-
-zonkMatch te ve (SimpleMatch expr)
-  = zonkExpr te ve expr   `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (SimpleMatch new_expr)
+zonkMatchGroup :: ZonkEnv -> MatchGroup TcId-> TcM (MatchGroup Id)
+zonkMatchGroup env (MatchGroup ms ty) 
+  = do { ms' <- mapM (zonkMatch env) ms
+       ; ty' <- zonkTcTypeToType env ty
+       ; return (MatchGroup ms' ty') }
+
+zonkMatch :: ZonkEnv -> LMatch TcId-> TcM (LMatch Id)
+zonkMatch env (L loc (Match pats _ grhss))
+  = do { (env1, new_pats) <- zonkPats env pats
+       ; new_grhss <- zonkGRHSs env1 grhss
+       ; return (L loc (Match new_pats Nothing new_grhss)) }
 
 -------------------------------------------------------------------------
-zonkGRHSsAndBinds :: TyVarEnv Type -> IdEnv Id 
-                 -> TcGRHSsAndBinds s
-                 -> NF_TcM s TypecheckedGRHSsAndBinds
+zonkGRHSs :: ZonkEnv -> GRHSs TcId -> TcM (GRHSs Id)
 
-zonkGRHSsAndBinds te ve (GRHSsAndBindsOut grhss binds ty)
-  = zonkBinds te ve binds              `thenNF_Tc` \ (new_binds, new_ve) ->
+zonkGRHSs env (GRHSs grhss binds)
+  = zonkLocalBinds env binds           `thenM` \ (new_env, new_binds) ->
     let
-       zonk_grhs (GRHS guard expr locn)
-         = zonkExpr te new_ve guard  `thenNF_Tc` \ new_guard ->
-           zonkExpr te new_ve expr   `thenNF_Tc` \ new_expr  ->
-           returnNF_Tc (GRHS new_guard new_expr locn)
-
-        zonk_grhs (OtherwiseGRHS expr locn)
-          = zonkExpr te new_ve expr   `thenNF_Tc` \ new_expr  ->
-           returnNF_Tc (OtherwiseGRHS new_expr locn)
+       zonk_grhs (GRHS guarded rhs)
+         = zonkStmts new_env guarded   `thenM` \ (env2, new_guarded) ->
+           zonkLExpr env2 rhs          `thenM` \ new_rhs ->
+           returnM (GRHS new_guarded new_rhs)
     in
-    mapNF_Tc zonk_grhs grhss   `thenNF_Tc` \ new_grhss ->
-    zonkTcTypeToType te ty     `thenNF_Tc` \ new_ty ->
-    returnNF_Tc (GRHSsAndBindsOut new_grhss new_binds new_ty)
+    mappM (wrapLocM zonk_grhs) grhss   `thenM` \ new_grhss ->
+    returnM (GRHSs new_grhss new_binds)
 \end{code}
 
 %************************************************************************
@@ -345,261 +346,334 @@ zonkGRHSsAndBinds te ve (GRHSsAndBindsOut grhss binds ty)
 %************************************************************************
 
 \begin{code}
-zonkExpr :: TyVarEnv Type -> IdEnv Id 
-        -> TcExpr s -> NF_TcM s TypecheckedHsExpr
-
-zonkExpr te ve (HsVar name)
-  = returnNF_Tc (HsVar (zonkIdOcc ve name))
-
-zonkExpr te ve (HsLit _) = panic "zonkExpr te ve:HsLit"
-
-zonkExpr te ve (HsLitOut lit ty)
-  = zonkTcTypeToType te ty         `thenNF_Tc` \ new_ty  ->
-    returnNF_Tc (HsLitOut lit new_ty)
-
-zonkExpr te ve (HsLam match)
-  = zonkMatch te ve match      `thenNF_Tc` \ new_match ->
-    returnNF_Tc (HsLam new_match)
-
-zonkExpr te ve (HsApp e1 e2)
-  = zonkExpr te ve e1  `thenNF_Tc` \ new_e1 ->
-    zonkExpr te ve e2  `thenNF_Tc` \ new_e2 ->
-    returnNF_Tc (HsApp new_e1 new_e2)
-
-zonkExpr te ve (OpApp e1 op e2)
-  = zonkExpr te ve e1  `thenNF_Tc` \ new_e1 ->
-    zonkExpr te ve op  `thenNF_Tc` \ new_op ->
-    zonkExpr te ve e2  `thenNF_Tc` \ new_e2 ->
-    returnNF_Tc (OpApp new_e1 new_op new_e2)
-
-zonkExpr te ve (NegApp _ _) = panic "zonkExpr te ve:NegApp"
-zonkExpr te ve (HsPar _)    = panic "zonkExpr te ve:HsPar"
-
-zonkExpr te ve (SectionL expr op)
-  = zonkExpr te ve expr        `thenNF_Tc` \ new_expr ->
-    zonkExpr te ve op          `thenNF_Tc` \ new_op ->
-    returnNF_Tc (SectionL new_expr new_op)
-
-zonkExpr te ve (SectionR op expr)
-  = zonkExpr te ve op          `thenNF_Tc` \ new_op ->
-    zonkExpr te ve expr                `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (SectionR new_op new_expr)
-
-zonkExpr te ve (HsCase expr ms src_loc)
-  = zonkExpr te ve expr            `thenNF_Tc` \ new_expr ->
-    mapNF_Tc (zonkMatch te ve) ms   `thenNF_Tc` \ new_ms ->
-    returnNF_Tc (HsCase new_expr new_ms src_loc)
-
-zonkExpr te ve (HsIf e1 e2 e3 src_loc)
-  = zonkExpr te ve e1  `thenNF_Tc` \ new_e1 ->
-    zonkExpr te ve e2  `thenNF_Tc` \ new_e2 ->
-    zonkExpr te ve e3  `thenNF_Tc` \ new_e3 ->
-    returnNF_Tc (HsIf new_e1 new_e2 new_e3 src_loc)
-
-zonkExpr te ve (HsLet binds expr)
-  = zonkBinds te ve binds      `thenNF_Tc` \ (new_binds, new_ve) ->
-    zonkExpr  te new_ve expr   `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (HsLet new_binds new_expr)
-
-zonkExpr te ve (HsDo _ _) = panic "zonkExpr te ve:HsDo"
-
-zonkExpr te ve (HsDoOut stmts then_id zero_id src_loc)
-  = zonkStmts te ve stmts      `thenNF_Tc` \ new_stmts ->
-    returnNF_Tc (HsDoOut new_stmts (zonkIdOcc ve then_id) (zonkIdOcc ve zero_id) src_loc)
-
-zonkExpr te ve (ListComp expr quals)
-  = zonkQuals te ve quals      `thenNF_Tc` \ (new_quals, new_ve) ->
-    zonkExpr te new_ve expr    `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (ListComp new_expr new_quals)
-
-zonkExpr te ve (ExplicitList _) = panic "zonkExpr te ve:ExplicitList"
-
-zonkExpr te ve (ExplicitListOut ty exprs)
-  = zonkTcTypeToType te ty             `thenNF_Tc` \ new_ty ->
-    mapNF_Tc (zonkExpr te ve) exprs    `thenNF_Tc` \ new_exprs ->
-    returnNF_Tc (ExplicitListOut new_ty new_exprs)
-
-zonkExpr te ve (ExplicitTuple exprs)
-  = mapNF_Tc (zonkExpr te ve) exprs  `thenNF_Tc` \ new_exprs ->
-    returnNF_Tc (ExplicitTuple new_exprs)
-
-zonkExpr te ve (RecordCon con rbinds)
-  = zonkExpr te ve con         `thenNF_Tc` \ new_con ->
-    zonkRbinds te ve rbinds    `thenNF_Tc` \ new_rbinds ->
-    returnNF_Tc (RecordCon new_con new_rbinds)
-
-zonkExpr te ve (RecordUpd _ _) = panic "zonkExpr te ve:RecordUpd"
-
-zonkExpr te ve (RecordUpdOut expr dicts rbinds)
-  = zonkExpr te ve expr                `thenNF_Tc` \ new_expr ->
-    zonkRbinds te ve rbinds    `thenNF_Tc` \ new_rbinds ->
-    returnNF_Tc (RecordUpdOut new_expr new_dicts new_rbinds)
-  where
-    new_dicts = map (zonkIdOcc ve) dicts
+zonkLExprs :: ZonkEnv -> [LHsExpr TcId] -> TcM [LHsExpr Id]
+zonkLExpr  :: ZonkEnv -> LHsExpr TcId   -> TcM (LHsExpr Id)
+zonkExpr   :: ZonkEnv -> HsExpr TcId    -> TcM (HsExpr Id)
 
-zonkExpr te ve (ExprWithTySig _ _) = panic "zonkExpr te ve:ExprWithTySig"
-zonkExpr te ve (ArithSeqIn _) = panic "zonkExpr te ve:ArithSeqIn"
+zonkLExprs env exprs = mappM (zonkLExpr env) exprs
+zonkLExpr  env expr  = wrapLocM (zonkExpr env) expr
 
-zonkExpr te ve (ArithSeqOut expr info)
-  = zonkExpr te ve expr        `thenNF_Tc` \ new_expr ->
-    zonkArithSeq te ve info    `thenNF_Tc` \ new_info ->
-    returnNF_Tc (ArithSeqOut new_expr new_info)
+zonkExpr env (HsVar id)
+  = returnM (HsVar (zonkIdOcc env id))
 
-zonkExpr te ve (CCall fun args may_gc is_casm result_ty)
-  = mapNF_Tc (zonkExpr te ve) args     `thenNF_Tc` \ new_args ->
-    zonkTcTypeToType te result_ty      `thenNF_Tc` \ new_result_ty ->
-    returnNF_Tc (CCall fun new_args may_gc is_casm new_result_ty)
+zonkExpr env (HsIPVar id)
+  = returnM (HsIPVar (mapIPName (zonkIdOcc env) id))
 
-zonkExpr te ve (HsSCC label expr)
-  = zonkExpr te ve expr        `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (HsSCC label new_expr)
+zonkExpr env (HsLit (HsRat f ty))
+  = zonkTcTypeToType env ty       `thenM` \ new_ty  ->
+    returnM (HsLit (HsRat f new_ty))
 
-zonkExpr te ve (TyLam tyvars expr)
-  = mapNF_Tc zonkTcTyVarToTyVar tyvars `thenNF_Tc` \ new_tyvars ->
-    let
-       new_te = extend_te te new_tyvars
-    in
-    zonkExpr new_te ve expr            `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (TyLam new_tyvars new_expr)
+zonkExpr env (HsLit lit)
+  = returnM (HsLit lit)
 
-zonkExpr te ve (TyApp expr tys)
-  = zonkExpr te ve expr                `thenNF_Tc` \ new_expr ->
-    mapNF_Tc (zonkTcTypeToType te) tys `thenNF_Tc` \ new_tys ->
-    returnNF_Tc (TyApp new_expr new_tys)
+zonkExpr env (HsOverLit lit)
+  = do { lit' <- zonkOverLit env lit
+       ; return (HsOverLit lit') }
 
-zonkExpr te ve (DictLam dicts expr)
-  = mapNF_Tc (zonkIdBndr te) dicts     `thenNF_Tc` \ new_dicts ->
-    let
-       new_ve = extend_ve ve new_dicts
-    in
-    zonkExpr te new_ve expr                    `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (DictLam new_dicts new_expr)
+zonkExpr env (HsLam matches)
+  = zonkMatchGroup env matches `thenM` \ new_matches ->
+    returnM (HsLam new_matches)
 
-zonkExpr te ve (DictApp expr dicts)
-  = zonkExpr te ve expr                `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (DictApp new_expr new_dicts)
-  where
-    new_dicts = map (zonkIdOcc ve) dicts
+zonkExpr env (HsApp e1 e2)
+  = zonkLExpr env e1   `thenM` \ new_e1 ->
+    zonkLExpr env e2   `thenM` \ new_e2 ->
+    returnM (HsApp new_e1 new_e2)
 
-zonkExpr te ve (ClassDictLam dicts methods expr)
-  = zonkExpr te ve expr            `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (ClassDictLam new_dicts new_methods new_expr)
+zonkExpr env (HsBracketOut body bs) 
+  = mappM zonk_b bs    `thenM` \ bs' ->
+    returnM (HsBracketOut body bs')
   where
-    new_dicts   = map (zonkIdOcc ve) dicts
-    new_methods = map (zonkIdOcc ve) methods
-    
+    zonk_b (n,e) = zonkLExpr env e     `thenM` \ e' ->
+                  returnM (n,e')
+
+zonkExpr env (HsSpliceE s) = WARN( True, ppr s )       -- Should not happen
+                            returnM (HsSpliceE s)
+
+zonkExpr env (OpApp e1 op fixity e2)
+  = zonkLExpr env e1   `thenM` \ new_e1 ->
+    zonkLExpr env op   `thenM` \ new_op ->
+    zonkLExpr env e2   `thenM` \ new_e2 ->
+    returnM (OpApp new_e1 new_op fixity new_e2)
+
+zonkExpr env (NegApp expr op)
+  = zonkLExpr env expr `thenM` \ new_expr ->
+    zonkExpr env op    `thenM` \ new_op ->
+    returnM (NegApp new_expr new_op)
+
+zonkExpr env (HsPar e)    
+  = zonkLExpr env e    `thenM` \new_e ->
+    returnM (HsPar new_e)
+
+zonkExpr env (SectionL expr op)
+  = zonkLExpr env expr `thenM` \ new_expr ->
+    zonkLExpr env op           `thenM` \ new_op ->
+    returnM (SectionL new_expr new_op)
+
+zonkExpr env (SectionR op expr)
+  = zonkLExpr env op           `thenM` \ new_op ->
+    zonkLExpr env expr         `thenM` \ new_expr ->
+    returnM (SectionR new_op new_expr)
+
+zonkExpr env (HsCase expr ms)
+  = zonkLExpr env expr         `thenM` \ new_expr ->
+    zonkMatchGroup env ms      `thenM` \ new_ms ->
+    returnM (HsCase new_expr new_ms)
+
+zonkExpr env (HsIf e1 e2 e3)
+  = zonkLExpr env e1   `thenM` \ new_e1 ->
+    zonkLExpr env e2   `thenM` \ new_e2 ->
+    zonkLExpr env e3   `thenM` \ new_e3 ->
+    returnM (HsIf new_e1 new_e2 new_e3)
+
+zonkExpr env (HsLet binds expr)
+  = zonkLocalBinds env binds   `thenM` \ (new_env, new_binds) ->
+    zonkLExpr new_env expr     `thenM` \ new_expr ->
+    returnM (HsLet new_binds new_expr)
+
+zonkExpr env (HsDo do_or_lc stmts body ty)
+  = zonkStmts env stmts        `thenM` \ (new_env, new_stmts) ->
+    zonkLExpr new_env body     `thenM` \ new_body ->
+    zonkTcTypeToType env ty    `thenM` \ new_ty   ->
+    returnM (HsDo (zonkDo env do_or_lc) 
+                 new_stmts new_body new_ty)
+
+zonkExpr env (ExplicitList ty exprs)
+  = zonkTcTypeToType env ty    `thenM` \ new_ty ->
+    zonkLExprs env exprs       `thenM` \ new_exprs ->
+    returnM (ExplicitList new_ty new_exprs)
+
+zonkExpr env (ExplicitPArr ty exprs)
+  = zonkTcTypeToType env ty    `thenM` \ new_ty ->
+    zonkLExprs env exprs       `thenM` \ new_exprs ->
+    returnM (ExplicitPArr new_ty new_exprs)
+
+zonkExpr env (ExplicitTuple exprs boxed)
+  = zonkLExprs env exprs       `thenM` \ new_exprs ->
+    returnM (ExplicitTuple new_exprs boxed)
+
+zonkExpr env (RecordCon data_con con_expr rbinds)
+  = zonkExpr env con_expr      `thenM` \ new_con_expr ->
+    zonkRbinds env rbinds      `thenM` \ new_rbinds ->
+    returnM (RecordCon data_con new_con_expr new_rbinds)
+
+zonkExpr env (RecordUpd expr rbinds in_ty out_ty)
+  = zonkLExpr env expr         `thenM` \ new_expr ->
+    zonkTcTypeToType env in_ty `thenM` \ new_in_ty ->
+    zonkTcTypeToType env out_ty        `thenM` \ new_out_ty ->
+    zonkRbinds env rbinds      `thenM` \ new_rbinds ->
+    returnM (RecordUpd new_expr new_rbinds new_in_ty new_out_ty)
+
+zonkExpr env (ExprWithTySigOut e ty) 
+  = do { e' <- zonkLExpr env e
+       ; return (ExprWithTySigOut e' ty) }
+
+zonkExpr env (ExprWithTySig _ _) = panic "zonkExpr env:ExprWithTySig"
+
+zonkExpr env (ArithSeq expr info)
+  = zonkExpr env expr          `thenM` \ new_expr ->
+    zonkArithSeq env info      `thenM` \ new_info ->
+    returnM (ArithSeq new_expr new_info)
+
+zonkExpr env (PArrSeq expr info)
+  = zonkExpr env expr          `thenM` \ new_expr ->
+    zonkArithSeq env info      `thenM` \ new_info ->
+    returnM (PArrSeq new_expr new_info)
+
+zonkExpr env (HsSCC lbl expr)
+  = zonkLExpr env expr `thenM` \ new_expr ->
+    returnM (HsSCC lbl new_expr)
+
+-- hdaume: core annotations
+zonkExpr env (HsCoreAnn lbl expr)
+  = zonkLExpr env expr   `thenM` \ new_expr ->
+    returnM (HsCoreAnn lbl new_expr)
+
+zonkExpr env (TyLam tyvars expr)
+  = ASSERT( all isImmutableTyVar tyvars )
+    zonkLExpr env expr                 `thenM` \ new_expr ->
+    returnM (TyLam tyvars new_expr)
+
+zonkExpr env (TyApp expr tys)
+  = zonkLExpr env expr         `thenM` \ new_expr ->
+    zonkTcTypeToTypes env tys  `thenM` \ new_tys ->
+    returnM (TyApp new_expr new_tys)
+
+zonkExpr env (DictLam dicts expr)
+  = zonkIdBndrs env dicts      `thenM` \ new_dicts ->
+    let
+       env1 = extendZonkEnv env new_dicts
+    in
+    zonkLExpr env1 expr        `thenM` \ new_expr ->
+    returnM (DictLam new_dicts new_expr)
+
+zonkExpr env (DictApp expr dicts)
+  = zonkLExpr env expr                 `thenM` \ new_expr ->
+    returnM (DictApp new_expr (zonkIdOccs env dicts))
+
+-- arrow notation extensions
+zonkExpr env (HsProc pat body)
+  = do { (env1, new_pat) <- zonkPat env pat
+       ; new_body <- zonkCmdTop env1 body
+       ; return (HsProc new_pat new_body) }
+
+zonkExpr env (HsArrApp e1 e2 ty ho rl)
+  = zonkLExpr env e1                   `thenM` \ new_e1 ->
+    zonkLExpr env e2                   `thenM` \ new_e2 ->
+    zonkTcTypeToType env ty            `thenM` \ new_ty ->
+    returnM (HsArrApp new_e1 new_e2 new_ty ho rl)
+
+zonkExpr env (HsArrForm op fixity args)
+  = zonkLExpr env op                   `thenM` \ new_op ->
+    mappM (zonkCmdTop env) args                `thenM` \ new_args ->
+    returnM (HsArrForm new_op fixity new_args)
+
+zonkExpr env (HsCoerce co_fn expr)
+  = zonkCoFn env co_fn `thenM` \ (env1, new_co_fn) ->
+    zonkExpr env1 expr `thenM` \ new_expr ->
+    return (HsCoerce new_co_fn new_expr)
+
+zonkExpr env other = pprPanic "zonkExpr" (ppr other)
+
+zonkCmdTop :: ZonkEnv -> LHsCmdTop TcId -> TcM (LHsCmdTop Id)
+zonkCmdTop env cmd = wrapLocM (zonk_cmd_top env) cmd
+
+zonk_cmd_top env (HsCmdTop cmd stack_tys ty ids)
+  = zonkLExpr env cmd                  `thenM` \ new_cmd ->
+    zonkTcTypeToTypes env stack_tys    `thenM` \ new_stack_tys ->
+    zonkTcTypeToType env ty            `thenM` \ new_ty ->
+    mapSndM (zonkExpr env) ids         `thenM` \ new_ids ->
+    returnM (HsCmdTop new_cmd new_stack_tys new_ty new_ids)
 
-zonkExpr te ve (Dictionary dicts methods)
-  = returnNF_Tc (Dictionary new_dicts new_methods)
-  where
-    new_dicts   = map (zonkIdOcc ve) dicts
-    new_methods = map (zonkIdOcc ve) methods
+-------------------------------------------------------------------------
+zonkCoFn :: ZonkEnv -> ExprCoFn -> TcM (ZonkEnv, ExprCoFn)
+zonkCoFn env CoHole = return (env, CoHole)
+zonkCoFn env (CoCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
+                                   ; (env2, c2') <- zonkCoFn env1 c2
+                                   ; return (env2, CoCompose c1' c2') }
+zonkCoFn env (CoLams ids c) = do { ids' <- zonkIdBndrs env ids
+                                ; let env1 = extendZonkEnv env ids'
+                                ; (env2, c') <- zonkCoFn env1 c
+                                ; return (env2, CoLams ids' c') }
+zonkCoFn env (CoTyLams tvs c) = ASSERT( all isImmutableTyVar tvs )
+                               do { (env1, c') <- zonkCoFn env c
+                                  ; return (env1, CoTyLams tvs c') }
+zonkCoFn env (CoApps c ids)   = do { (env1, c') <- zonkCoFn env c
+                                  ; return (env1, CoApps c' (zonkIdOccs env ids)) }
+zonkCoFn env (CoTyApps c tys) = do { tys' <- zonkTcTypeToTypes env tys
+                                  ; (env1, c') <- zonkCoFn env c
+                                  ; return (env1, CoTyApps c' tys') }
+zonkCoFn env (CoLet bs c)     = do { (env1, bs') <- zonkRecMonoBinds env bs
+                                  ; (env2, c')  <- zonkCoFn env1 c
+                                  ; return (env2, CoLet bs' c') }
 
-zonkExpr te ve (SingleDict name)
-  = returnNF_Tc (SingleDict (zonkIdOcc ve name))
 
-zonkExpr te ve (HsCon con tys vargs)
-  = mapNF_Tc (zonkTcTypeToType te) tys `thenNF_Tc` \ new_tys   ->
-    mapNF_Tc (zonkExpr te ve) vargs    `thenNF_Tc` \ new_vargs ->
-    returnNF_Tc (HsCon con new_tys new_vargs)
+-------------------------------------------------------------------------
+zonkDo :: ZonkEnv -> HsStmtContext Name -> HsStmtContext Name
+-- Only used for 'do', so the only Ids are in a MDoExpr table
+zonkDo env (MDoExpr tbl) = MDoExpr (mapSnd (zonkIdOcc env) tbl)
+zonkDo env do_or_lc      = do_or_lc
 
 -------------------------------------------------------------------------
-zonkArithSeq :: TyVarEnv Type -> IdEnv Id 
-            -> TcArithSeqInfo s -> NF_TcM s TypecheckedArithSeqInfo
+zonkOverLit :: ZonkEnv -> HsOverLit TcId -> TcM (HsOverLit Id)
+zonkOverLit env (HsIntegral i e)
+  = do { e' <- zonkExpr env e; return (HsIntegral i e') }
+zonkOverLit env (HsFractional r e)
+  = do { e' <- zonkExpr env e; return (HsFractional r e') }
 
-zonkArithSeq te ve (From e)
-  = zonkExpr te ve e           `thenNF_Tc` \ new_e ->
-    returnNF_Tc (From new_e)
+-------------------------------------------------------------------------
+zonkArithSeq :: ZonkEnv -> ArithSeqInfo TcId -> TcM (ArithSeqInfo Id)
 
-zonkArithSeq te ve (FromThen e1 e2)
-  = zonkExpr te ve e1  `thenNF_Tc` \ new_e1 ->
-    zonkExpr te ve e2  `thenNF_Tc` \ new_e2 ->
-    returnNF_Tc (FromThen new_e1 new_e2)
+zonkArithSeq env (From e)
+  = zonkLExpr env e            `thenM` \ new_e ->
+    returnM (From new_e)
 
-zonkArithSeq te ve (FromTo e1 e2)
-  = zonkExpr te ve e1  `thenNF_Tc` \ new_e1 ->
-    zonkExpr te ve e2  `thenNF_Tc` \ new_e2 ->
-    returnNF_Tc (FromTo new_e1 new_e2)
+zonkArithSeq env (FromThen e1 e2)
+  = zonkLExpr env e1   `thenM` \ new_e1 ->
+    zonkLExpr env e2   `thenM` \ new_e2 ->
+    returnM (FromThen new_e1 new_e2)
 
-zonkArithSeq te ve (FromThenTo e1 e2 e3)
-  = zonkExpr te ve e1  `thenNF_Tc` \ new_e1 ->
-    zonkExpr te ve e2  `thenNF_Tc` \ new_e2 ->
-    zonkExpr te ve e3  `thenNF_Tc` \ new_e3 ->
-    returnNF_Tc (FromThenTo new_e1 new_e2 new_e3)
+zonkArithSeq env (FromTo e1 e2)
+  = zonkLExpr env e1   `thenM` \ new_e1 ->
+    zonkLExpr env e2   `thenM` \ new_e2 ->
+    returnM (FromTo new_e1 new_e2)
 
--------------------------------------------------------------------------
-zonkQuals :: TyVarEnv Type -> IdEnv Id 
-         -> [TcQual s] -> NF_TcM s ([TypecheckedQual], IdEnv Id)
+zonkArithSeq env (FromThenTo e1 e2 e3)
+  = zonkLExpr env e1   `thenM` \ new_e1 ->
+    zonkLExpr env e2   `thenM` \ new_e2 ->
+    zonkLExpr env e3   `thenM` \ new_e3 ->
+    returnM (FromThenTo new_e1 new_e2 new_e3)
 
-zonkQuals te ve [] 
-  = returnNF_Tc ([], ve)
 
-zonkQuals te ve (GeneratorQual pat expr : quals)
-  = zonkPat te ve pat  `thenNF_Tc` \ (new_pat, ids) ->
-    zonkExpr te ve expr        `thenNF_Tc` \ new_expr ->
-    let
-       new_ve = extend_ve ve ids
+-------------------------------------------------------------------------
+zonkStmts :: ZonkEnv -> [LStmt TcId] -> TcM (ZonkEnv, [LStmt Id])
+zonkStmts env []     = return (env, [])
+zonkStmts env (s:ss) = do { (env1, s')  <- wrapLocSndM (zonkStmt env) s
+                         ; (env2, ss') <- zonkStmts env1 ss
+                         ; return (env2, s' : ss') }
+
+zonkStmt :: ZonkEnv -> Stmt TcId -> TcM (ZonkEnv, Stmt Id)
+zonkStmt env (ParStmt stmts_w_bndrs)
+  = mappM zonk_branch stmts_w_bndrs    `thenM` \ new_stmts_w_bndrs ->
+    let 
+       new_binders = concat (map snd new_stmts_w_bndrs)
+       env1 = extendZonkEnv env new_binders
     in
-    zonkQuals te new_ve quals  `thenNF_Tc` \ (new_quals, final_ve) ->
-    returnNF_Tc (GeneratorQual new_pat new_expr : new_quals, final_ve)
-
-zonkQuals te ve (FilterQual expr : quals)
-  = zonkExpr te ve expr        `thenNF_Tc` \ new_expr ->
-    zonkQuals te ve quals      `thenNF_Tc` \ (new_quals, final_ve) ->
-    returnNF_Tc (FilterQual new_expr : new_quals, final_ve)
-
-zonkQuals te ve (LetQual binds : quals)
-  = zonkBinds te ve binds      `thenNF_Tc` \ (new_binds, new_ve) ->
-    zonkQuals te new_ve quals  `thenNF_Tc` \ (new_quals, final_ve) ->
-    returnNF_Tc (LetQual new_binds : new_quals, final_ve)
+    return (env1, ParStmt new_stmts_w_bndrs)
+  where
+    zonk_branch (stmts, bndrs) = zonkStmts env stmts   `thenM` \ (env1, new_stmts) ->
+                                returnM (new_stmts, zonkIdOccs env1 bndrs)
 
--------------------------------------------------------------------------
-zonkStmts :: TyVarEnv Type -> IdEnv Id 
-         -> [TcStmt s] -> NF_TcM s [TypecheckedStmt]
-
-zonkStmts te ve [] = returnNF_Tc []
-
-zonkStmts te ve [ExprStmt expr locn]
-  = zonkExpr te ve expr                `thenNF_Tc` \ new_expr ->
-    returnNF_Tc [ExprStmt new_expr locn]
-
-zonkStmts te ve (ExprStmtOut expr locn a b : stmts)
-  = zonkExpr te ve      expr   `thenNF_Tc` \ new_expr  ->
-    zonkTcTypeToType te a      `thenNF_Tc` \ new_a     ->
-    zonkTcTypeToType te b      `thenNF_Tc` \ new_b     ->
-    zonkStmts te ve    stmts   `thenNF_Tc` \ new_stmts ->
-    returnNF_Tc (ExprStmtOut new_expr locn new_a new_b : new_stmts)
-
-zonkStmts te ve (LetStmt binds : stmts)
-  = zonkBinds te ve     binds  `thenNF_Tc` \ (new_binds, new_ve) ->
-    zonkStmts te new_ve stmts  `thenNF_Tc` \ new_stmts ->
-    returnNF_Tc (LetStmt new_binds : new_stmts)
-
-zonkStmts te ve (BindStmtOut pat expr locn a b : stmts)
-  = zonkPat te ve pat          `thenNF_Tc` \ (new_pat, ids) ->
-    zonkExpr te ve expr                `thenNF_Tc` \ new_expr ->
-    zonkTcTypeToType te a      `thenNF_Tc` \ new_a     ->
-    zonkTcTypeToType te b      `thenNF_Tc` \ new_b     ->
+zonkStmt env (RecStmt segStmts lvs rvs rets binds)
+  = zonkIdBndrs env rvs                `thenM` \ new_rvs ->
     let
-       new_ve = extend_ve ve ids
+       env1 = extendZonkEnv env new_rvs
     in
-    zonkStmts te new_ve stmts  `thenNF_Tc` \ new_stmts ->
-    returnNF_Tc (BindStmtOut new_pat new_expr locn new_a new_b : new_stmts)
+    zonkStmts env1 segStmts    `thenM` \ (env2, new_segStmts) ->
+       -- Zonk the ret-expressions in an envt that 
+       -- has the polymorphic bindings in the envt
+    mapM (zonkExpr env2) rets  `thenM` \ new_rets ->
+    let
+       new_lvs = zonkIdOccs env2 lvs
+       env3 = extendZonkEnv env new_lvs        -- Only the lvs are needed
+    in
+    zonkRecMonoBinds env3 binds        `thenM` \ (env4, new_binds) ->
+    returnM (env4, RecStmt new_segStmts new_lvs new_rvs new_rets new_binds)
+
+zonkStmt env (ExprStmt expr then_op ty)
+  = zonkLExpr env expr         `thenM` \ new_expr ->
+    zonkExpr env then_op       `thenM` \ new_then ->
+    zonkTcTypeToType env ty    `thenM` \ new_ty ->
+    returnM (env, ExprStmt new_expr new_then new_ty)
+
+zonkStmt env (LetStmt binds)
+  = zonkLocalBinds env binds   `thenM` \ (env1, new_binds) ->
+    returnM (env1, LetStmt new_binds)
 
+zonkStmt env (BindStmt pat expr bind_op fail_op)
+  = do { new_expr <- zonkLExpr env expr
+       ; (env1, new_pat) <- zonkPat env pat
+       ; new_bind <- zonkExpr env bind_op
+       ; new_fail <- zonkExpr env fail_op
+       ; return (env1, BindStmt new_pat new_expr new_bind new_fail) }
 
 
 -------------------------------------------------------------------------
-zonkRbinds :: TyVarEnv Type -> IdEnv Id 
-          -> TcRecordBinds s -> NF_TcM s TypecheckedRecordBinds
+zonkRbinds :: ZonkEnv -> HsRecordBinds TcId -> TcM (HsRecordBinds Id)
 
-zonkRbinds te ve rbinds
-  = mapNF_Tc zonk_rbind rbinds
+zonkRbinds env rbinds
+  = mappM zonk_rbind rbinds
   where
-    zonk_rbind (field, expr, pun)
-      = zonkExpr te ve expr    `thenNF_Tc` \ new_expr ->
-       returnNF_Tc (zonkIdOcc ve field, new_expr, pun)
+    zonk_rbind (field, expr)
+      = zonkLExpr env expr     `thenM` \ new_expr ->
+       returnM (fmap (zonkIdOcc env) field, new_expr)
+
+-------------------------------------------------------------------------
+mapIPNameTc :: (a -> TcM b) -> IPName a -> TcM (IPName b)
+mapIPNameTc f (Dupable n) = f n  `thenM` \ r -> returnM (Dupable r)
+mapIPNameTc f (Linear  n) = f n  `thenM` \ r -> returnM (Linear r)
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection[BackSubst-Pats]{Patterns}
@@ -607,77 +681,270 @@ zonkRbinds te ve rbinds
 %************************************************************************
 
 \begin{code}
-zonkPat :: TyVarEnv Type -> IdEnv Id 
-       -> TcPat s -> NF_TcM s (TypecheckedPat, [Id])
-
-zonkPat te ve (WildPat ty)
-  = zonkTcTypeToType te ty         `thenNF_Tc` \ new_ty ->
-    returnNF_Tc (WildPat new_ty, [])
-
-zonkPat te ve (VarPat v)
-  = zonkIdBndr te v        `thenNF_Tc` \ new_v ->
-    returnNF_Tc (VarPat new_v, [new_v])
-
-zonkPat te ve (LazyPat pat)
-  = zonkPat te ve pat      `thenNF_Tc` \ (new_pat, ids) ->
-    returnNF_Tc (LazyPat new_pat, ids)
-
-zonkPat te ve (AsPat n pat)
-  = zonkIdBndr te n        `thenNF_Tc` \ new_n ->
-    zonkPat te ve pat      `thenNF_Tc` \ (new_pat, ids) ->
-    returnNF_Tc (AsPat new_n new_pat, new_n:ids)
-
-zonkPat te ve (ConPat n ty pats)
-  = zonkTcTypeToType te ty     `thenNF_Tc` \ new_ty ->
-    zonkPats te ve pats                `thenNF_Tc` \ (new_pats, ids) ->
-    returnNF_Tc (ConPat n new_ty new_pats, ids)
-
-zonkPat te ve (ConOpPat pat1 op pat2 ty)
-  = zonkPat te ve pat1     `thenNF_Tc` \ (new_pat1, ids1) ->
-    zonkPat te ve pat2     `thenNF_Tc` \ (new_pat2, ids2) ->
-    zonkTcTypeToType te ty  `thenNF_Tc` \ new_ty ->
-    returnNF_Tc (ConOpPat new_pat1 op new_pat2 new_ty, ids1 ++ ids2)
-
-zonkPat te ve (ListPat ty pats)
-  = zonkTcTypeToType te ty     `thenNF_Tc` \ new_ty ->
-    zonkPats te ve pats                `thenNF_Tc` \ (new_pats, ids) ->
-    returnNF_Tc (ListPat new_ty new_pats, ids)
-
-zonkPat te ve (TuplePat pats)
-  = zonkPats te ve pats                `thenNF_Tc` \ (new_pats, ids) ->
-    returnNF_Tc (TuplePat new_pats, ids)
-
-zonkPat te ve (RecPat n ty rpats)
-  = zonkTcTypeToType te ty             `thenNF_Tc` \ new_ty ->
-    mapAndUnzipNF_Tc zonk_rpat rpats   `thenNF_Tc` \ (new_rpats, ids_s) ->
-    returnNF_Tc (RecPat n new_ty new_rpats, concat ids_s)
+zonkPat :: ZonkEnv -> OutPat TcId -> TcM (ZonkEnv, OutPat Id)
+-- Extend the environment as we go, because it's possible for one
+-- pattern to bind something that is used in another (inside or
+-- to the right)
+zonkPat env pat = wrapLocSndM (zonk_pat env) pat
+
+zonk_pat env (ParPat p)
+  = do { (env', p') <- zonkPat env p
+       ; return (env', ParPat p') }
+
+zonk_pat env (WildPat ty)
+  = do { ty' <- zonkTcTypeToType env ty
+       ; return (env, WildPat ty') }
+
+zonk_pat env (VarPat v)
+  = do { v' <- zonkIdBndr env v
+       ; return (extendZonkEnv1 env v', VarPat v') }
+
+zonk_pat env (VarPatOut v binds)
+  = do { v' <- zonkIdBndr env v
+       ; (env', binds') <- zonkRecMonoBinds (extendZonkEnv1 env v') binds
+       ; returnM (env', VarPatOut v' binds') }
+
+zonk_pat env (LazyPat pat)
+  = do { (env', pat') <- zonkPat env pat
+       ; return (env',  LazyPat pat') }
+
+zonk_pat env (AsPat (L loc v) pat)
+  = do { v' <- zonkIdBndr env v
+       ; (env', pat') <- zonkPat (extendZonkEnv1 env v') pat
+       ; return (env', AsPat (L loc v') pat') }
+
+zonk_pat env (ListPat pats ty)
+  = do { ty' <- zonkTcTypeToType env ty
+       ; (env', pats') <- zonkPats env pats
+       ; return (env', ListPat pats' ty') }
+
+zonk_pat env (PArrPat pats ty)
+  = do { ty' <- zonkTcTypeToType env ty
+       ; (env', pats') <- zonkPats env pats
+       ; return (env', PArrPat pats' ty') }
+
+zonk_pat env (TuplePat pats boxed)
+  = do { (env', pats') <- zonkPats env pats
+       ; return (env', TuplePat pats' boxed) }
+
+zonk_pat env (ConPatOut n tvs dicts binds stuff ty)
+  = ASSERT( all isImmutableTyVar tvs )
+    do { new_ty <- zonkTcTypeToType env ty
+       ; new_dicts <- zonkIdBndrs env dicts
+       ; let env1 = extendZonkEnv env new_dicts
+       ; (env2, new_binds) <- zonkRecMonoBinds env1 binds
+       ; (env', new_stuff) <- zonkConStuff env2 stuff
+       ; returnM (env', ConPatOut n tvs new_dicts new_binds new_stuff new_ty) }
+
+zonk_pat env (LitPat lit) = return (env, LitPat lit)
+
+zonk_pat env (SigPatOut pat ty)
+  = do { ty' <- zonkTcTypeToType env ty
+       ; (env', pat') <- zonkPat env pat
+       ; return (env', SigPatOut pat' ty') }
+
+zonk_pat env (NPat lit mb_neg eq_expr ty)
+  = do { lit' <- zonkOverLit env lit
+       ; mb_neg' <- case mb_neg of
+                       Nothing  -> return Nothing
+                       Just neg -> do { neg' <- zonkExpr env neg
+                                      ; return (Just neg') }
+       ; eq_expr' <- zonkExpr env eq_expr
+       ; ty' <- zonkTcTypeToType env ty
+       ; return (env, NPat lit' mb_neg' eq_expr' ty') }
+
+zonk_pat env (NPlusKPat (L loc n) lit e1 e2)
+  = do { n' <- zonkIdBndr env n
+       ; lit' <- zonkOverLit env lit
+       ; e1' <- zonkExpr env e1
+       ; e2' <- zonkExpr env e2
+       ; return (extendZonkEnv1 env n', NPlusKPat (L loc n') lit' e1' e2') }
+
+zonk_pat env (DictPat ds ms)
+  = do { ds' <- zonkIdBndrs env ds
+       ; ms' <- zonkIdBndrs env ms
+       ; return (extendZonkEnv env (ds' ++ ms'), DictPat ds' ms') }
+
+---------------------------
+zonkConStuff env (PrefixCon pats)
+  = do { (env', pats') <- zonkPats env pats
+       ; return (env', PrefixCon pats') }
+
+zonkConStuff env (InfixCon p1 p2)
+  = do { (env1, p1') <- zonkPat env  p1
+       ; (env', p2') <- zonkPat env1 p2
+       ; return (env', InfixCon p1' p2') }
+
+zonkConStuff env (RecCon rpats)
+  = do { (env', pats') <- zonkPats env pats
+       ; returnM (env', RecCon (fields `zip` pats')) }
   where
-    zonk_rpat (f, pat, pun)
-      = zonkPat te ve pat           `thenNF_Tc` \ (new_pat, ids) ->
-       returnNF_Tc ((f, new_pat, pun), ids)
+    (fields, pats) = unzip rpats
 
-zonkPat te ve (LitPat lit ty)
-  = zonkTcTypeToType te ty         `thenNF_Tc` \ new_ty  ->
-    returnNF_Tc (LitPat lit new_ty, [])
+---------------------------
+zonkPats env []                = return (env, [])
+zonkPats env (pat:pats) = do { (env1, pat') <- zonkPat env pat
+                            ; (env', pats') <- zonkPats env1 pats
+                            ; return (env', pat':pats') }
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+\subsection[BackSubst-Foreign]{Foreign exports}
+%*                                                                     *
+%************************************************************************
 
-zonkPat te ve (NPat lit ty expr)
-  = zonkTcTypeToType te ty     `thenNF_Tc` \ new_ty   ->
-    zonkExpr te ve expr                `thenNF_Tc` \ new_expr ->
-    returnNF_Tc (NPat lit new_ty new_expr, [])
 
-zonkPat te ve (DictPat ds ms)
-  = mapNF_Tc (zonkIdBndr te) ds    `thenNF_Tc` \ new_ds ->
-    mapNF_Tc (zonkIdBndr te) ms    `thenNF_Tc` \ new_ms ->
-    returnNF_Tc (DictPat new_ds new_ms, new_ds ++ new_ms)
+\begin{code}
+zonkForeignExports :: ZonkEnv -> [LForeignDecl TcId] -> TcM [LForeignDecl Id]
+zonkForeignExports env ls = mappM (wrapLocM (zonkForeignExport env)) ls
+
+zonkForeignExport :: ZonkEnv -> ForeignDecl TcId -> TcM (ForeignDecl Id)
+zonkForeignExport env (ForeignExport i hs_ty spec isDeprec) =
+   returnM (ForeignExport (fmap (zonkIdOcc env) i) undefined spec isDeprec)
+zonkForeignExport env for_imp 
+  = returnM for_imp    -- Foreign imports don't need zonking
+\end{code}
 
+\begin{code}
+zonkRules :: ZonkEnv -> [LRuleDecl TcId] -> TcM [LRuleDecl Id]
+zonkRules env rs = mappM (wrapLocM (zonkRule env)) rs
 
-zonkPats te ve [] 
-  = returnNF_Tc ([], [])
-zonkPats te ve (pat:pats) 
-  = zonkPat te ve pat  `thenNF_Tc` \ (pat', ids1) ->
-    zonkPats te ve pats        `thenNF_Tc` \ (pats', ids2) ->
-    returnNF_Tc (pat':pats', ids1 ++ ids2)
+zonkRule :: ZonkEnv -> RuleDecl TcId -> TcM (RuleDecl Id)
+zonkRule env (HsRule name act (vars::[RuleBndr TcId]) lhs rhs)
+  = mappM zonk_bndr vars               `thenM` \ new_bndrs ->
+    newMutVar emptyVarSet              `thenM` \ unbound_tv_set ->
+    let
+       env_rhs = extendZonkEnv env [id | b <- new_bndrs, let id = unLoc b, isId id]
+       -- Type variables don't need an envt
+       -- They are bound through the mutable mechanism
+
+       env_lhs = setZonkType env_rhs (zonkTypeCollecting unbound_tv_set)
+       -- We need to gather the type variables mentioned on the LHS so we can 
+       -- quantify over them.  Example:
+       --   data T a = C
+       -- 
+       --   foo :: T a -> Int
+       --   foo C = 1
+       --
+       --   {-# RULES "myrule"  foo C = 1 #-}
+       -- 
+       -- After type checking the LHS becomes (foo a (C a))
+       -- and we do not want to zap the unbound tyvar 'a' to (), because
+       -- that limits the applicability of the rule.  Instead, we
+       -- want to quantify over it!  
+       --
+       -- It's easiest to find the free tyvars here. Attempts to do so earlier
+       -- are tiresome, because (a) the data type is big and (b) finding the 
+       -- free type vars of an expression is necessarily monadic operation.
+       --      (consider /\a -> f @ b, where b is side-effected to a)
+    in
+    zonkLExpr env_lhs lhs              `thenM` \ new_lhs ->
+    zonkLExpr env_rhs rhs              `thenM` \ new_rhs ->
 
+    readMutVar unbound_tv_set          `thenM` \ unbound_tvs ->
+    let
+       final_bndrs :: [Located Var]
+       final_bndrs = map noLoc (varSetElems unbound_tvs) ++ new_bndrs
+    in
+    returnM (HsRule name act (map RuleBndr final_bndrs) new_lhs new_rhs)
+               -- I hate this map RuleBndr stuff
+  where
+   zonk_bndr (RuleBndr v) 
+       | isId (unLoc v) = wrapLocM (zonkIdBndr env)   v
+       | otherwise      = ASSERT( isImmutableTyVar (unLoc v) )
+                          return v
 \end{code}
 
 
+%************************************************************************
+%*                                                                     *
+\subsection[BackSubst-Foreign]{Foreign exports}
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
+zonkTcTypeToType (ZonkEnv zonk_ty _) ty = zonk_ty ty
+
+zonkTcTypeToTypes :: ZonkEnv -> [TcType] -> TcM [Type]
+zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
+
+zonkTypeCollecting :: TcRef TyVarSet -> TcType -> TcM Type
+-- This variant collects unbound type variables in a mutable variable
+zonkTypeCollecting unbound_tv_set
+  = zonkType zonk_unbound_tyvar
+  where
+    zonk_unbound_tyvar tv 
+       = zonkQuantifiedTyVar tv                                `thenM` \ tv' ->
+         readMutVar unbound_tv_set                             `thenM` \ tv_set ->
+         writeMutVar unbound_tv_set (extendVarSet tv_set tv')  `thenM_`
+         return (mkTyVarTy tv')
+
+zonkTypeZapping :: TcType -> TcM Type
+-- This variant is used for everything except the LHS of rules
+-- It zaps unbound type variables to (), or some other arbitrary type
+zonkTypeZapping ty 
+  = zonkType zonk_unbound_tyvar ty 
+  where
+       -- Zonk a mutable but unbound type variable to an arbitrary type
+       -- We know it's unbound even though we don't carry an environment,
+       -- because at the binding site for a type variable we bind the
+       -- mutable tyvar to a fresh immutable one.  So the mutable store
+       -- plays the role of an environment.  If we come across a mutable
+       -- type variable that isn't so bound, it must be completely free.
+    zonk_unbound_tyvar tv = do { writeMetaTyVar tv ty; return ty }
+                         where 
+                           ty = mkArbitraryType tv
+
+
+-- When the type checker finds a type variable with no binding,
+-- which means it can be instantiated with an arbitrary type, it
+-- usually instantiates it to Void.  Eg.
+-- 
+--     length []
+-- ===>
+--     length Void (Nil Void)
+-- 
+-- But in really obscure programs, the type variable might have
+-- a kind other than *, so we need to invent a suitably-kinded type.
+-- 
+-- This commit uses
+--     Void for kind *
+--     List for kind *->*
+--     Tuple for kind *->...*->*
+-- 
+-- which deals with most cases.  (Previously, it only dealt with
+-- kind *.)   
+-- 
+-- In the other cases, it just makes up a TyCon with a suitable
+-- kind.  If this gets into an interface file, anyone reading that
+-- file won't understand it.  This is fixable (by making the client
+-- of the interface file make up a TyCon too) but it is tiresome and
+-- never happens, so I am leaving it 
+
+mkArbitraryType :: TcTyVar -> Type
+-- Make up an arbitrary type whose kind is the same as the tyvar.
+-- We'll use this to instantiate the (unbound) tyvar.
+mkArbitraryType tv 
+  | liftedTypeKind `isSubKind` kind = voidTy           -- The vastly common case
+  | otherwise                      = mkTyConApp tycon []
+  where
+    kind       = tyVarKind tv
+    (args,res) = splitKindFunTys kind
+
+    tycon | kind == tyConKind listTyCon        --  *->*
+         = listTyCon                           -- No tuples this size
+
+         | all isLiftedTypeKind args && isLiftedTypeKind res
+         = tupleTyCon Boxed (length args)      --  *-> ... ->*->*
+
+         | otherwise
+         = pprTrace "Urk! Inventing strangely-kinded void TyCon:" (ppr tc_name $$ ppr kind) $
+           mkPrimTyCon tc_name kind 0 [] VoidRep
+               -- Same name as the tyvar, 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.
+
+    tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
+\end{code}