Implememt -fdefer-type-errors (Trac #5624)
[ghc.git] / compiler / typecheck / TcHsSyn.lhs
index 299d70f..73361ae 100644 (file)
@@ -9,6 +9,13 @@ This module is an extension of @HsSyn@ syntax, for use in the type
 checker.
 
 \begin{code}
 checker.
 
 \begin{code}
+{-# OPTIONS -fno-warn-tabs #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and
+-- detab the module (please do the detabbing in a separate patch). See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
+-- for details
+
 module TcHsSyn (
        mkHsConApp, mkHsDictLet, mkHsApp,
        hsLitType, hsLPatType, hsPatType, 
 module TcHsSyn (
        mkHsConApp, mkHsDictLet, mkHsApp,
        hsLitType, hsLPatType, hsPatType, 
@@ -16,12 +23,10 @@ module TcHsSyn (
        nlHsIntLit, 
        shortCutLit, hsOverLitName,
        
        nlHsIntLit, 
        shortCutLit, hsOverLitName,
        
-       mkArbitraryType,        -- Put this elsewhere?
-
        -- re-exported from TcMonad
        -- re-exported from TcMonad
-       TcId, TcIdSet, TcDictBinds,
+       TcId, TcIdSet, 
 
 
-       zonkTopDecls, zonkTopExpr, zonkTopLExpr,
+       zonkTopDecls, zonkTopExpr, zonkTopLExpr, mkZonkTcTyVar,
        zonkId, zonkTopBndrs
   ) where
 
        zonkId, zonkTopBndrs
   ) where
 
@@ -37,22 +42,26 @@ import TcRnMonad
 import PrelNames
 import TcType
 import TcMType
 import PrelNames
 import TcType
 import TcMType
+import TcEvidence
 import TysPrim
 import TysWiredIn
 import TysPrim
 import TysWiredIn
-import TyCon
+import Type
+import Kind
 import DataCon
 import Name
 import DataCon
 import Name
+import NameSet
 import Var
 import VarSet
 import VarEnv
 import Var
 import VarSet
 import VarEnv
+import DynFlags
 import Literal
 import BasicTypes
 import Maybes
 import SrcLoc
 import Literal
 import BasicTypes
 import Maybes
 import SrcLoc
-import Util
 import Bag
 import Bag
-import Outputable
 import FastString
 import FastString
+import Outputable
+-- import Data.Traversable( traverse )
 \end{code}
 
 \begin{code}
 \end{code}
 
 \begin{code}
@@ -60,9 +69,6 @@ import FastString
 thenM :: Monad a => a b -> (b -> a c) -> a c
 thenM = (>>=)
 
 thenM :: Monad a => a b -> (b -> a c) -> a c
 thenM = (>>=)
 
-thenM_ :: Monad a => a b -> a c -> a c
-thenM_ = (>>)
-
 returnM :: Monad m => a -> m a
 returnM = return
 
 returnM :: Monad m => a -> m a
 returnM = return
 
@@ -87,7 +93,6 @@ hsPatType :: Pat Id -> Type
 hsPatType (ParPat pat)                = hsLPatType pat
 hsPatType (WildPat ty)                = ty
 hsPatType (VarPat var)                = idType var
 hsPatType (ParPat pat)                = hsLPatType pat
 hsPatType (WildPat ty)                = ty
 hsPatType (VarPat var)                = idType var
-hsPatType (VarPatOut var _)           = idType var
 hsPatType (BangPat pat)               = hsLPatType pat
 hsPatType (LazyPat pat)               = hsLPatType pat
 hsPatType (LitPat lit)                = hsLitType lit
 hsPatType (BangPat pat)               = hsLPatType pat
 hsPatType (LazyPat pat)               = hsLPatType pat
 hsPatType (LitPat lit)                = hsLitType lit
@@ -111,6 +116,8 @@ hsLitType (HsStringPrim _) = addrPrimTy
 hsLitType (HsInt _)        = intTy
 hsLitType (HsIntPrim _)    = intPrimTy
 hsLitType (HsWordPrim _)   = wordPrimTy
 hsLitType (HsInt _)        = intTy
 hsLitType (HsIntPrim _)    = intPrimTy
 hsLitType (HsWordPrim _)   = wordPrimTy
+hsLitType (HsInt64Prim _)  = int64PrimTy
+hsLitType (HsWord64Prim _) = word64PrimTy
 hsLitType (HsInteger _ ty) = ty
 hsLitType (HsRat _ ty)     = ty
 hsLitType (HsFloatPrim _)  = floatPrimTy
 hsLitType (HsInteger _ ty) = ty
 hsLitType (HsRat _ ty)     = ty
 hsLitType (HsFloatPrim _)  = floatPrimTy
@@ -125,7 +132,7 @@ shortCutLit (HsIntegral i) ty
   | isIntTy ty && inIntRange i   = Just (HsLit (HsInt i))
   | isWordTy ty && inWordRange i = Just (mkLit wordDataCon (HsWordPrim i))
   | isIntegerTy ty              = Just (HsLit (HsInteger i ty))
   | isIntTy ty && inIntRange i   = Just (HsLit (HsInt i))
   | isWordTy ty && inWordRange i = Just (mkLit wordDataCon (HsWordPrim i))
   | isIntegerTy ty              = Just (HsLit (HsInteger i ty))
-  | otherwise                   = shortCutLit (HsFractional (fromInteger i)) ty
+  | otherwise                   = shortCutLit (HsFractional (integralFractionalLit i)) ty
        -- The 'otherwise' case is important
        -- Consider (3 :: Float).  Syntactically it looks like an IntLit,
        -- so we'll call shortCutIntLit, but of course it's a float
        -- The 'otherwise' case is important
        -- Consider (3 :: Float).  Syntactically it looks like an IntLit,
        -- so we'll call shortCutIntLit, but of course it's a float
@@ -184,27 +191,45 @@ It's all pretty boring stuff, because HsSyn is such a large type, and
 the environment manipulation is tiresome.
 
 \begin{code}
 the environment manipulation is tiresome.
 
 \begin{code}
-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
+type UnboundTyVarZonker = TcTyVar-> TcM Type 
+       -- How to zonk an unbound type variable
+        -- Note [Zonking the LHS of a RULE]
+
+data ZonkEnv 
+  = ZonkEnv 
+      UnboundTyVarZonker
+      (TyVarEnv TyVar)          -- 
+      (IdEnv Var)              -- What variables are in scope
+       -- Maps an Id or EvVar to its zonked version; both have the same Name
+       -- Note that all evidence (coercion variables as well as dictionaries)
+       --      are kept in the ZonkEnv
+       -- Only *type* abstraction is done by side effect
        -- Is only consulted lazily; hence knot-tying
 
        -- Is only consulted lazily; hence knot-tying
 
+instance Outputable ZonkEnv where 
+  ppr (ZonkEnv _ _ty_env var_env) = vcat (map ppr (varEnvElts var_env))
+
+
 emptyZonkEnv :: ZonkEnv
 emptyZonkEnv :: ZonkEnv
-emptyZonkEnv = ZonkEnv zonkTypeZapping emptyVarEnv
+emptyZonkEnv = ZonkEnv zonkTypeZapping emptyVarEnv emptyVarEnv
+
+extendIdZonkEnv :: ZonkEnv -> [Var] -> ZonkEnv
+extendIdZonkEnv (ZonkEnv zonk_ty ty_env id_env) ids 
+  = ZonkEnv zonk_ty ty_env (extendVarEnvList id_env [(id,id) | id <- ids])
 
 
-extendZonkEnv :: ZonkEnv -> [Id] -> ZonkEnv
-extendZonkEnv (ZonkEnv zonk_ty env) ids 
-  = ZonkEnv zonk_ty (extendVarEnvList env [(id,id) | id <- ids])
+extendIdZonkEnv1 :: ZonkEnv -> Var -> ZonkEnv
+extendIdZonkEnv1 (ZonkEnv zonk_ty ty_env id_env) id 
+  = ZonkEnv zonk_ty ty_env (extendVarEnv id_env id id)
 
 
-extendZonkEnv1 :: ZonkEnv -> Id -> ZonkEnv
-extendZonkEnv1 (ZonkEnv zonk_ty env) id 
-  = ZonkEnv zonk_ty (extendVarEnv env id id)
+extendTyZonkEnv1 :: ZonkEnv -> TyVar -> ZonkEnv
+extendTyZonkEnv1 (ZonkEnv zonk_ty ty_env id_env) ty
+  = ZonkEnv zonk_ty (extendVarEnv ty_env ty ty) id_env
 
 
-setZonkType :: ZonkEnv -> (TcType -> TcM Type) -> ZonkEnv
-setZonkType (ZonkEnv _ env) zonk_ty = ZonkEnv zonk_ty env
+setZonkType :: ZonkEnv -> UnboundTyVarZonker -> ZonkEnv
+setZonkType (ZonkEnv _ ty_env id_env) zonk_ty = ZonkEnv zonk_ty ty_env id_env
 
 zonkEnvIds :: ZonkEnv -> [Id]
 
 zonkEnvIds :: ZonkEnv -> [Id]
-zonkEnvIds (ZonkEnv _ env) = varEnvElts env
+zonkEnvIds (ZonkEnv _ _ id_env) = varEnvElts id_env
 
 zonkIdOcc :: ZonkEnv -> TcId -> Id
 -- Ids defined in this module should be in the envt; 
 
 zonkIdOcc :: ZonkEnv -> TcId -> Id
 -- Ids defined in this module should be in the envt; 
@@ -222,7 +247,7 @@ zonkIdOcc :: ZonkEnv -> TcId -> Id
 --
 -- Even without template splices, in module Main, the checking of
 -- 'main' is done as a separate chunk.
 --
 -- Even without template splices, in module Main, the checking of
 -- 'main' is done as a separate chunk.
-zonkIdOcc (ZonkEnv _zonk_ty env) id 
+zonkIdOcc (ZonkEnv _zonk_ty _ty_env env) id 
   | isLocalVar id = lookupVarEnv env id `orElse` id
   | otherwise    = id
 
   | isLocalVar id = lookupVarEnv env id `orElse` id
   | otherwise    = id
 
@@ -239,27 +264,43 @@ zonkIdBndr env id
 zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id]
 zonkIdBndrs env ids = mappM (zonkIdBndr env) ids
 
 zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id]
 zonkIdBndrs env ids = mappM (zonkIdBndr env) ids
 
-zonkDictBndrs :: ZonkEnv -> [Var] -> TcM [Var]
--- "Dictionary" binders can be coercion variables or dictionary variables
-zonkDictBndrs env ids = mappM (zonkDictBndr env) ids
-
-zonkDictBndr :: ZonkEnv -> Var -> TcM Var
-zonkDictBndr env var | isTyVar var = zonkTyVarBndr env var
-                    | otherwise   = zonkIdBndr env var
-
 zonkTopBndrs :: [TcId] -> TcM [Id]
 zonkTopBndrs ids = zonkIdBndrs emptyZonkEnv ids
 
 zonkTopBndrs :: [TcId] -> TcM [Id]
 zonkTopBndrs ids = zonkIdBndrs emptyZonkEnv ids
 
--- Zonk the kind of a non-TC tyvar in case it is a coercion variable (their
--- kind contains types).
---
-zonkTyVarBndr :: ZonkEnv -> TyVar -> TcM TyVar
-zonkTyVarBndr env tv
-  | isCoVar tv
-  = do { kind <- zonkTcTypeToType env (tyVarKind tv)
-       ; return $ setTyVarKind tv kind
-       }
-  | otherwise = return tv
+zonkEvBndrsX :: ZonkEnv -> [EvVar] -> TcM (ZonkEnv, [Var])
+zonkEvBndrsX = mapAccumLM zonkEvBndrX 
+
+zonkEvBndrX :: ZonkEnv -> EvVar -> TcM (ZonkEnv, EvVar)
+-- Works for dictionaries and coercions
+zonkEvBndrX env var
+  = do { var' <- zonkEvBndr env var
+       ; return (extendIdZonkEnv1 env var', var') }
+
+zonkEvBndr :: ZonkEnv -> EvVar -> TcM EvVar
+-- Works for dictionaries and coercions
+-- Does not extend the ZonkEnv
+zonkEvBndr env var 
+  = do { let var_ty = varType var
+       ; ty <- 
+           {-# SCC "zonkEvBndr_zonkTcTypeToType" #-}
+           zonkTcTypeToType env var_ty
+       ; return (setVarType var ty) }
+
+zonkEvVarOcc :: ZonkEnv -> EvVar -> EvVar
+zonkEvVarOcc env v = zonkIdOcc env v
+
+zonkTyBndrsX :: ZonkEnv -> [TyVar] -> TcM (ZonkEnv, [TyVar])
+zonkTyBndrsX = mapAccumLM zonkTyBndrX 
+
+zonkTyBndrX :: ZonkEnv -> TyVar -> TcM (ZonkEnv, TyVar)
+zonkTyBndrX env tv
+  = do { tv' <- zonkTyBndr env tv
+       ; return (extendTyZonkEnv1 env tv', tv') }
+
+zonkTyBndr :: ZonkEnv -> TyVar -> TcM TyVar
+zonkTyBndr env tv
+  = do { ki <- zonkTcTypeToType env (tyVarKind tv)
+       ; return (setVarType tv ki) }
 \end{code}
 
 
 \end{code}
 
 
@@ -270,33 +311,62 @@ zonkTopExpr e = zonkExpr emptyZonkEnv e
 zonkTopLExpr :: LHsExpr TcId -> TcM (LHsExpr Id)
 zonkTopLExpr e = zonkLExpr 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') }
+zonkTopDecls :: Bag EvBind 
+             -> LHsBinds TcId -> NameSet
+             -> [LRuleDecl TcId] -> [LVectDecl TcId] -> [LTcSpecPrag] -> [LForeignDecl TcId]
+             -> TcM ([Id], 
+                     Bag EvBind,
+                     Bag (LHsBind  Id),
+                     [LForeignDecl Id],
+                     [LTcSpecPrag],
+                     [LRuleDecl    Id],
+                     [LVectDecl    Id])
+zonkTopDecls ev_binds binds sig_ns rules vects imp_specs fords
+  = do  { (env1, ev_binds') <- zonkEvBinds emptyZonkEnv ev_binds
+
+        -- Warn about missing signatures
+        -- Do this only when we we have a type to offer
+        ; warn_missing_sigs <- woptM Opt_WarnMissingSigs
+        ; let sig_warn | warn_missing_sigs = topSigWarn sig_ns
+                       | otherwise         = noSigWarn
+
+        ; (env2, binds') <- zonkRecMonoBinds env1 sig_warn binds
+                        -- Top level is implicitly recursive
+        ; rules' <- zonkRules env2 rules
+        ; vects' <- zonkVects env2 vects
+        ; specs' <- zonkLTcSpecPrags env2 imp_specs
+        ; fords' <- zonkForeignExports env2 fords
+        ; return (zonkEnvIds env2, ev_binds', binds', fords', specs', rules', vects') }
 
 ---------------------------------------------
 zonkLocalBinds :: ZonkEnv -> HsLocalBinds TcId -> TcM (ZonkEnv, HsLocalBinds Id)
 zonkLocalBinds env EmptyLocalBinds
   = return (env, EmptyLocalBinds)
 
 
 ---------------------------------------------
 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 _ (HsValBinds (ValBindsIn {}))
+  = panic "zonkLocalBinds" -- Not in typechecker output
+
+zonkLocalBinds env (HsValBinds vb@(ValBindsOut binds sigs))
+  = do { warn_missing_sigs <- woptM Opt_WarnMissingLocalSigs
+        ; let sig_warn | not warn_missing_sigs = noSigWarn
+                       | otherwise             = localSigWarn sig_ns
+              sig_ns = getTypeSigNames vb
+       ; (env1, new_binds) <- go env sig_warn binds
+        ; return (env1, HsValBinds (ValBindsOut new_binds sigs)) }
+  where
+    go env _ []
+      = return (env, [])
+    go env sig_warn ((r,b):bs) 
+      = do { (env1, b')  <- zonkRecMonoBinds env sig_warn b
+          ; (env2, bs') <- go env1 sig_warn bs
+          ; return (env2, (r,b'):bs') }
 
 zonkLocalBinds env (HsIPBinds (IPBinds binds dict_binds))
   = mappM (wrapLocM zonk_ip_bind) binds        `thenM` \ new_binds ->
     let
 
 zonkLocalBinds env (HsIPBinds (IPBinds binds dict_binds))
   = mappM (wrapLocM zonk_ip_bind) binds        `thenM` \ new_binds ->
     let
-       env1 = extendZonkEnv env [ipNameName n | L _ (IPBind n _) <- new_binds]
+       env1 = extendIdZonkEnv env [ipNameName n | L _ (IPBind n _) <- new_binds]
     in
     in
-    zonkRecMonoBinds env1 dict_binds   `thenM` \ (env2, new_dict_binds) -> 
+    zonkTcEvBinds env1 dict_binds      `thenM` \ (env2, new_dict_binds) -> 
     returnM (env2, HsIPBinds (IPBinds new_binds new_dict_binds))
   where
     zonk_ip_bind (IPBind n e)
     returnM (env2, HsIPBinds (IPBinds new_binds new_dict_binds))
   where
     zonk_ip_bind (IPBind n e)
@@ -304,76 +374,123 @@ zonkLocalBinds env (HsIPBinds (IPBinds binds dict_binds))
          zonkLExpr env e                       `thenM` \ e' ->
          returnM (IPBind n' e')
 
          zonkLExpr env e                       `thenM` \ e' ->
          returnM (IPBind n' e')
 
+---------------------------------------------
+zonkRecMonoBinds :: ZonkEnv -> SigWarn -> LHsBinds TcId -> TcM (ZonkEnv, LHsBinds Id)
+zonkRecMonoBinds env sig_warn binds 
+ = fixM (\ ~(_, new_binds) -> do 
+       { let env1 = extendIdZonkEnv env (collectHsBindsBinders new_binds)
+        ; binds' <- zonkMonoBinds env1 sig_warn binds
+        ; return (env1, binds') })
 
 ---------------------------------------------
 
 ---------------------------------------------
-zonkValBinds :: ZonkEnv -> HsValBinds TcId -> TcM (ZonkEnv, HsValBinds Id)
-zonkValBinds _ (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) }
+type SigWarn = Bool -> [Id] -> TcM ()  
+     -- Missing-signature warning
+     -- The Bool is True for an AbsBinds, False otherwise
+
+noSigWarn :: SigWarn
+noSigWarn _ _ = return ()
+
+topSigWarn :: NameSet -> SigWarn
+topSigWarn sig_ns _ ids = mapM_ (topSigWarnId sig_ns) ids
+
+topSigWarnId :: NameSet -> Id -> TcM ()
+-- The NameSet is the Ids that *lack* a signature
+-- We have to do it this way round because there are
+-- lots of top-level bindings that are generated by GHC
+-- and that don't have signatures
+topSigWarnId sig_ns id
+  | idName id `elemNameSet` sig_ns = warnMissingSig msg id
+  | otherwise                      = return ()
   where
   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') }
+    msg = ptext (sLit "Top-level binding with no type signature:")
+
+localSigWarn :: NameSet -> SigWarn
+localSigWarn sig_ns is_abs_bind ids
+  | not is_abs_bind = return ()
+  | otherwise       = mapM_ (localSigWarnId sig_ns) ids
+
+localSigWarnId :: NameSet -> Id -> TcM ()
+-- NameSet are the Ids that *have* type signatures
+localSigWarnId sig_ns id
+  | not (isSigmaTy (idType id))    = return ()
+  | idName id `elemNameSet` sig_ns = return ()
+  | otherwise                      = warnMissingSig msg id
+  where
+    msg = ptext (sLit "Polymophic local binding with no type signature:")
 
 
----------------------------------------------
-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') })
+warnMissingSig :: SDoc -> Id -> TcM ()
+warnMissingSig msg id
+  = do  { env0 <- tcInitTidyEnv
+        ; let (env1, tidy_ty) = tidyOpenType env0 (idType id)
+        ; addWarnTcM (env1, mk_msg tidy_ty) }
+  where
+    mk_msg ty = sep [ msg, nest 2 $ pprPrefixName (idName id) <+> dcolon <+> ppr ty ]
 
 ---------------------------------------------
 
 ---------------------------------------------
-zonkMonoBinds :: ZonkEnv -> LHsBinds TcId -> TcM (LHsBinds Id)
-zonkMonoBinds env binds = mapBagM (wrapLocM (zonk_bind env)) binds
+zonkMonoBinds :: ZonkEnv -> SigWarn -> LHsBinds TcId -> TcM (LHsBinds Id)
+zonkMonoBinds env sig_warn binds = mapBagM (wrapLocM (zonk_bind env sig_warn)) binds
 
 
-zonk_bind :: ZonkEnv -> HsBind TcId -> TcM (HsBind Id)
-zonk_bind env bind@(PatBind { pat_lhs = pat, pat_rhs = grhss, pat_rhs_ty = ty})
+zonk_bind :: ZonkEnv -> SigWarn -> HsBind TcId -> TcM (HsBind Id)
+zonk_bind env sig_warn bind@(PatBind { pat_lhs = pat, pat_rhs = grhss, pat_rhs_ty = ty})
   = do { (_env, new_pat) <- zonkPat env pat            -- Env already extended
   = do { (_env, new_pat) <- zonkPat env pat            -- Env already extended
+        ; sig_warn False (collectPatBinders new_pat)
        ; 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 }) }
 
        ; 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 })
+zonk_bind env sig_warn (VarBind { var_id = var, var_rhs = expr, var_inline = inl })
+  = do { new_var  <- zonkIdBndr env var
+       ; sig_warn False [new_var]
+       ; new_expr <- zonkLExpr env expr
+       ; return (VarBind { var_id = new_var, var_rhs = new_expr, var_inline = inl }) }
+
+zonk_bind env sig_warn bind@(FunBind { fun_id = L loc var, fun_matches = ms
+                                     , fun_co_fn = co_fn })
+  = do { new_var <- zonkIdBndr env var
+       ; sig_warn False [new_var]
+       ; (env1, new_co_fn) <- zonkCoFn env co_fn
+       ; new_ms <- zonkMatchGroup env1 ms
+       ; return (bind { fun_id = L loc new_var, fun_matches = new_ms
+                      , fun_co_fn = new_co_fn }) }
+
+zonk_bind env sig_warn (AbsBinds { abs_tvs = tyvars, abs_ev_vars = evs
+                                 , abs_ev_binds = ev_binds
+                                , abs_exports = exports
+                                 , abs_binds = val_binds })
   = ASSERT( all isImmutableTyVar tyvars )
   = ASSERT( all isImmutableTyVar tyvars )
-    zonkDictBndrs env dicts                    `thenM` \ new_dicts ->
-    fixM (\ ~(new_val_binds, _) ->
-       let
-         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 })
+    do { (env0, new_tyvars) <- zonkTyBndrsX env tyvars
+       ; (env1, new_evs) <- zonkEvBndrsX env0 evs
+       ; (env2, new_ev_binds) <- zonkTcEvBinds env1 ev_binds
+       ; (new_val_bind, new_exports) <- fixM $ \ ~(new_val_binds, _) ->
+         do { let env3 = extendIdZonkEnv env2 (collectHsBindsBinders new_val_binds)
+           ; new_val_binds <- zonkMonoBinds env3 noSigWarn val_binds
+           ; new_exports   <- mapM (zonkExport env3) exports
+           ; return (new_val_binds, new_exports) } 
+       ; sig_warn True (map abe_poly new_exports)
+       ; return (AbsBinds { abs_tvs = new_tyvars, abs_ev_vars = new_evs
+                          , abs_ev_binds = new_ev_binds
+                         , abs_exports = new_exports, abs_binds = new_val_bind }) }
   where
   where
-    zonkExport env (tyvars, global, local, prags)
-       -- The tyvars are already zonked
-       = 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@(L _ (InlinePrag {}))  = return prag
-    zonk_prag (L loc (SpecPrag expr ty inl))
-       = do { expr' <- zonkExpr env expr 
-            ; ty'   <- zonkTcTypeToType env ty
-            ; return (L loc (SpecPrag expr' ty' inl)) }
+    zonkExport env (ABE{ abe_wrap = wrap, abe_poly = poly_id
+                       , abe_mono = mono_id, abe_prags = prags })
+       = zonkIdBndr env poly_id                `thenM` \ new_poly_id ->
+         zonkCoFn env wrap                     `thenM` \ (_, new_wrap) ->
+          zonkSpecPrags env prags              `thenM` \ new_prags -> 
+         returnM (ABE{ abe_wrap = new_wrap, abe_poly = new_poly_id
+                      , abe_mono = zonkIdOcc env mono_id, abe_prags = new_prags })
+
+zonkSpecPrags :: ZonkEnv -> TcSpecPrags -> TcM TcSpecPrags
+zonkSpecPrags _   IsDefaultMethod = return IsDefaultMethod
+zonkSpecPrags env (SpecPrags ps)  = do { ps' <- zonkLTcSpecPrags env ps
+                                       ; return (SpecPrags ps') }
+
+zonkLTcSpecPrags :: ZonkEnv -> [LTcSpecPrag] -> TcM [LTcSpecPrag]
+zonkLTcSpecPrags env ps
+  = mapM zonk_prag ps
+  where
+    zonk_prag (L loc (SpecPrag id co_fn inl))
+       = do { (_, co_fn') <- zonkCoFn env co_fn
+            ; return (L loc (SpecPrag (zonkIdOcc env id) co_fn' inl)) }
 \end{code}
 
 %************************************************************************
 \end{code}
 
 %************************************************************************
@@ -497,23 +614,22 @@ zonkExpr env (HsCase expr ms)
     zonkMatchGroup env ms      `thenM` \ new_ms ->
     returnM (HsCase new_expr new_ms)
 
     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 (HsIf e0 e1 e2 e3)
+  = do { new_e0 <- fmapMaybeM (zonkExpr env) e0
+       ; new_e1 <- zonkLExpr env e1
+       ; new_e2 <- zonkLExpr env e2
+       ; new_e3 <- zonkLExpr env e3
+       ; returnM (HsIf new_e0 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 (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 ->
+zonkExpr env (HsDo do_or_lc stmts ty)
+  = zonkStmts env stmts        `thenM` \ (_, new_stmts) ->
     zonkTcTypeToType env ty    `thenM` \ new_ty   ->
     zonkTcTypeToType env ty    `thenM` \ new_ty   ->
-    returnM (HsDo (zonkDo env do_or_lc) 
-                 new_stmts new_body new_ty)
+    returnM (HsDo do_or_lc new_stmts new_ty)
 
 zonkExpr env (ExplicitList ty exprs)
   = zonkTcTypeToType env ty    `thenM` \ new_ty ->
 
 zonkExpr env (ExplicitList ty exprs)
   = zonkTcTypeToType env ty    `thenM` \ new_ty ->
@@ -604,38 +720,23 @@ zonk_cmd_top env (HsCmdTop cmd stack_tys ty ids)
 -------------------------------------------------------------------------
 zonkCoFn :: ZonkEnv -> HsWrapper -> TcM (ZonkEnv, HsWrapper)
 zonkCoFn env WpHole   = return (env, WpHole)
 -------------------------------------------------------------------------
 zonkCoFn :: ZonkEnv -> HsWrapper -> TcM (ZonkEnv, HsWrapper)
 zonkCoFn env WpHole   = return (env, WpHole)
-zonkCoFn env WpInline = return (env, WpInline)
 zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
                                    ; (env2, c2') <- zonkCoFn env1 c2
                                    ; return (env2, WpCompose c1' c2') }
 zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
                                    ; (env2, c2') <- zonkCoFn env1 c2
                                    ; return (env2, WpCompose c1' c2') }
-zonkCoFn env (WpCast co)    = do { co' <- zonkTcTypeToType env co
-                                ; return (env, WpCast co') }
-zonkCoFn env (WpLam id)     = do { id' <- zonkDictBndr env id
-                                ; let env1 = extendZonkEnv1 env id'
-                                ; return (env1, WpLam id') }
+zonkCoFn env (WpCast co) = do { co' <- zonkTcLCoToLCo env co
+                             ; return (env, WpCast co') }
+zonkCoFn env (WpEvLam ev)   = do { (env', ev') <- zonkEvBndrX env ev
+                                ; return (env', WpEvLam ev') }
+zonkCoFn env (WpEvApp arg)  = do { arg' <- zonkEvTerm env arg 
+                                 ; return (env, WpEvApp arg') }
 zonkCoFn env (WpTyLam tv)   = ASSERT( isImmutableTyVar tv )
 zonkCoFn env (WpTyLam tv)   = ASSERT( isImmutableTyVar tv )
-                              do { tv' <- zonkTyVarBndr env tv
-                                ; return (env, WpTyLam tv') }
-zonkCoFn env (WpApp v)
-       | isTcTyVar v       = do { co <- zonkTcTyVar v
-                                ; return (env, WpTyApp co) }
-               -- Yuk!  A mutable coercion variable is a TcTyVar 
-               --       not a CoVar, so don't use isCoVar!
-               -- Yuk!  A WpApp can't hold the zonked type,
-               --       so we switch to WpTyApp
-       | otherwise         = return (env, WpApp (zonkIdOcc env v))
+                              do { (env', tv') <- zonkTyBndrX env tv
+                                ; return (env', WpTyLam tv') }
 zonkCoFn env (WpTyApp ty)   = do { ty' <- zonkTcTypeToType env ty
                                 ; return (env, WpTyApp ty') }
 zonkCoFn env (WpTyApp ty)   = do { ty' <- zonkTcTypeToType env ty
                                 ; return (env, WpTyApp ty') }
-zonkCoFn env (WpLet bs)     = do { (env1, bs') <- zonkRecMonoBinds env bs
+zonkCoFn env (WpLet bs)     = do { (env1, bs') <- zonkTcEvBinds env bs
                                 ; return (env1, WpLet bs') }
 
                                 ; return (env1, WpLet bs') }
 
-
--------------------------------------------------------------------------
-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 _   do_or_lc      = do_or_lc
-
 -------------------------------------------------------------------------
 zonkOverLit :: ZonkEnv -> HsOverLit TcId -> TcM (HsOverLit Id)
 zonkOverLit env lit@(OverLit { ol_witness = e, ol_type = ty })
 -------------------------------------------------------------------------
 zonkOverLit :: ZonkEnv -> HsOverLit TcId -> TcM (HsOverLit Id)
 zonkOverLit env lit@(OverLit { ol_witness = e, ol_type = ty })
@@ -675,65 +776,70 @@ zonkStmts env (s:ss) = do { (env1, s')  <- wrapLocSndM (zonkStmt env) s
                          ; return (env2, s' : ss') }
 
 zonkStmt :: ZonkEnv -> Stmt TcId -> TcM (ZonkEnv, Stmt Id)
                          ; return (env2, s' : ss') }
 
 zonkStmt :: ZonkEnv -> Stmt TcId -> TcM (ZonkEnv, Stmt Id)
-zonkStmt env (ParStmt stmts_w_bndrs)
+zonkStmt env (ParStmt stmts_w_bndrs mzip_op bind_op return_op)
   = mappM zonk_branch stmts_w_bndrs    `thenM` \ new_stmts_w_bndrs ->
     let 
        new_binders = concat (map snd new_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
+       env1 = extendIdZonkEnv env new_binders
     in
     in
-    return (env1, ParStmt new_stmts_w_bndrs)
+    zonkExpr env1 mzip_op   `thenM` \ new_mzip ->
+    zonkExpr env1 bind_op   `thenM` \ new_bind ->
+    zonkExpr env1 return_op `thenM` \ new_return ->
+    return (env1, ParStmt new_stmts_w_bndrs new_mzip new_bind new_return)
   where
     zonk_branch (stmts, bndrs) = zonkStmts env stmts   `thenM` \ (env1, new_stmts) ->
                                 returnM (new_stmts, zonkIdOccs env1 bndrs)
 
   where
     zonk_branch (stmts, bndrs) = zonkStmts env stmts   `thenM` \ (env1, new_stmts) ->
                                 returnM (new_stmts, zonkIdOccs env1 bndrs)
 
-zonkStmt env (RecStmt segStmts lvs rvs rets binds)
-  = zonkIdBndrs env rvs                `thenM` \ new_rvs ->
-    let
-       env1 = extendZonkEnv env new_rvs
-    in
-    zonkStmts env1 segStmts    `thenM` \ (env2, new_segStmts) ->
+zonkStmt env (RecStmt { recS_stmts = segStmts, recS_later_ids = lvs, recS_rec_ids = rvs
+                      , recS_ret_fn = ret_id, recS_mfix_fn = mfix_id, recS_bind_fn = bind_id
+                      , recS_later_rets = later_rets, recS_rec_rets = rec_rets
+                      , recS_ret_ty = ret_ty })
+  = do { new_rvs <- zonkIdBndrs env rvs
+       ; new_lvs <- zonkIdBndrs env lvs
+       ; new_ret_ty  <- zonkTcTypeToType env ret_ty
+       ; new_ret_id  <- zonkExpr env ret_id
+       ; new_mfix_id <- zonkExpr env mfix_id
+       ; new_bind_id <- zonkExpr env bind_id
+       ; let env1 = extendIdZonkEnv env new_rvs
+       ; (env2, new_segStmts) <- zonkStmts env1 segStmts
        -- Zonk the ret-expressions in an envt that 
        -- has the polymorphic bindings in the envt
        -- 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)
+       ; new_later_rets <- mapM (zonkExpr env2) later_rets
+       ; new_rec_rets <- mapM (zonkExpr env2) rec_rets
+       ; return (extendIdZonkEnv env new_lvs,     -- Only the lvs are needed
+                 RecStmt { recS_stmts = new_segStmts, recS_later_ids = new_lvs
+                         , recS_rec_ids = new_rvs, recS_ret_fn = new_ret_id
+                         , recS_mfix_fn = new_mfix_id, recS_bind_fn = new_bind_id
+                         , recS_later_rets = new_later_rets
+                         , recS_rec_rets = new_rec_rets, recS_ret_ty = new_ret_ty }) }
+
+zonkStmt env (ExprStmt expr then_op guard_op ty)
   = zonkLExpr env expr         `thenM` \ new_expr ->
     zonkExpr env then_op       `thenM` \ new_then ->
   = zonkLExpr env expr         `thenM` \ new_expr ->
     zonkExpr env then_op       `thenM` \ new_then ->
+    zonkExpr env guard_op      `thenM` \ new_guard ->
     zonkTcTypeToType env ty    `thenM` \ new_ty ->
     zonkTcTypeToType env ty    `thenM` \ new_ty ->
-    returnM (env, ExprStmt new_expr new_then new_ty)
+    returnM (env, ExprStmt new_expr new_then new_guard new_ty)
 
 
-zonkStmt env (TransformStmt (stmts, binders) usingExpr maybeByExpr)
-  = do { (env', stmts') <- zonkStmts env stmts 
-    ; let binders' = zonkIdOccs env' binders
-    ; usingExpr' <- zonkLExpr env' usingExpr
-    ; maybeByExpr' <- zonkMaybeLExpr env' maybeByExpr
-    ; return (env', TransformStmt (stmts', binders') usingExpr' maybeByExpr') }
-    
-zonkStmt env (GroupStmt (stmts, binderMap) groupByClause)
+zonkStmt env (LastStmt expr ret_op)
+  = zonkLExpr env expr         `thenM` \ new_expr ->
+    zonkExpr env ret_op                `thenM` \ new_ret ->
+    returnM (env, LastStmt new_expr new_ret)
+
+zonkStmt env (TransStmt { trS_stmts = stmts, trS_bndrs = binderMap
+                        , trS_by = by, trS_form = form, trS_using = using
+                        , trS_ret = return_op, trS_bind = bind_op, trS_fmap = liftM_op })
   = do { (env', stmts') <- zonkStmts env stmts 
     ; binderMap' <- mappM (zonkBinderMapEntry env') binderMap
   = do { (env', stmts') <- zonkStmts env stmts 
     ; binderMap' <- mappM (zonkBinderMapEntry env') binderMap
-    ; groupByClause' <- 
-        case groupByClause of
-            GroupByNothing usingExpr -> (zonkLExpr env' usingExpr) >>= (return . GroupByNothing)
-            GroupBySomething eitherUsingExpr byExpr -> do
-                eitherUsingExpr' <- mapEitherM (zonkLExpr env') (zonkExpr env') eitherUsingExpr
-                byExpr' <- zonkLExpr env' byExpr
-                return $ GroupBySomething eitherUsingExpr' byExpr'
-                
-    ; let env'' = extendZonkEnv env' (map snd binderMap')
-    ; return (env'', GroupStmt (stmts', binderMap') groupByClause') }
+    ; by'        <- fmapMaybeM (zonkLExpr env') by
+    ; using'     <- zonkLExpr env using
+    ; return_op' <- zonkExpr env' return_op
+    ; bind_op'   <- zonkExpr env' bind_op
+    ; liftM_op'  <- zonkExpr env' liftM_op
+    ; let env'' = extendIdZonkEnv env' (map snd binderMap')
+    ; return (env'', TransStmt { trS_stmts = stmts', trS_bndrs = binderMap'
+                               , trS_by = by', trS_form = form, trS_using = using'
+                               , trS_ret = return_op', trS_bind = bind_op', trS_fmap = liftM_op' }) }
   where
   where
-    mapEitherM f g x = do
-      case x of
-        Left a -> f a >>= (return . Left)
-        Right b -> g b >>= (return . Right)
-  
     zonkBinderMapEntry env (oldBinder, newBinder) = do 
         let oldBinder' = zonkIdOcc env oldBinder
         newBinder' <- zonkIdBndr env newBinder
     zonkBinderMapEntry env (oldBinder, newBinder) = do 
         let oldBinder' = zonkIdOcc env oldBinder
         newBinder' <- zonkIdBndr env newBinder
@@ -750,11 +856,6 @@ zonkStmt env (BindStmt pat expr bind_op fail_op)
        ; new_fail <- zonkExpr env fail_op
        ; return (env1, BindStmt new_pat new_expr new_bind new_fail) }
 
        ; new_fail <- zonkExpr env fail_op
        ; return (env1, BindStmt new_pat new_expr new_bind new_fail) }
 
-zonkMaybeLExpr :: ZonkEnv -> Maybe (LHsExpr TcId) -> TcM (Maybe (LHsExpr Id))
-zonkMaybeLExpr _   Nothing  = return Nothing
-zonkMaybeLExpr env (Just e) = (zonkLExpr env e) >>= (return . Just)
-
-
 -------------------------------------------------------------------------
 zonkRecFields :: ZonkEnv -> HsRecordBinds TcId -> TcM (HsRecordBinds TcId)
 zonkRecFields env (HsRecFields flds dd)
 -------------------------------------------------------------------------
 zonkRecFields :: ZonkEnv -> HsRecordBinds TcId -> TcM (HsRecordBinds TcId)
 zonkRecFields env (HsRecFields flds dd)
@@ -796,12 +897,7 @@ zonk_pat env (WildPat ty)
 
 zonk_pat env (VarPat v)
   = do { v' <- zonkIdBndr env v
 
 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') }
+       ; return (extendIdZonkEnv1 env v', VarPat v') }
 
 zonk_pat env (LazyPat pat)
   = do { (env', pat') <- zonkPat env pat
 
 zonk_pat env (LazyPat pat)
   = do { (env', pat') <- zonkPat env pat
@@ -813,7 +909,7 @@ zonk_pat env (BangPat pat)
 
 zonk_pat env (AsPat (L loc v) pat)
   = do { v' <- zonkIdBndr env v
 
 zonk_pat env (AsPat (L loc v) pat)
   = do { v' <- zonkIdBndr env v
-       ; (env', pat') <- zonkPat (extendZonkEnv1 env v') pat
+       ; (env', pat') <- zonkPat (extendIdZonkEnv1 env v') pat
        ; return (env', AsPat (L loc v') pat') }
 
 zonk_pat env (ViewPat expr pat ty)
        ; return (env', AsPat (L loc v') pat') }
 
 zonk_pat env (ViewPat expr pat ty)
@@ -837,15 +933,23 @@ zonk_pat env (TuplePat pats boxed ty)
        ; (env', pats') <- zonkPats env pats
        ; return (env', TuplePat pats' boxed ty') }
 
        ; (env', pats') <- zonkPats env pats
        ; return (env', TuplePat pats' boxed ty') }
 
-zonk_pat env p@(ConPatOut { pat_ty = ty, pat_dicts = dicts, pat_binds = binds, pat_args = args })
-  = ASSERT( all isImmutableTyVar (pat_tvs p) ) 
+zonk_pat env p@(ConPatOut { pat_ty = ty, pat_tvs = tyvars
+                          , pat_dicts = evs, pat_binds = binds
+                          , pat_args = args })
+  = ASSERT( all isImmutableTyVar tyvars ) 
     do { new_ty <- zonkTcTypeToType env ty
     do { new_ty <- zonkTcTypeToType env ty
-       ; new_dicts <- zonkDictBndrs env dicts
-       ; let env1 = extendZonkEnv env new_dicts
-       ; (env2, new_binds) <- zonkRecMonoBinds env1 binds
+        ; (env0, new_tyvars) <- zonkTyBndrsX env tyvars
+          -- Must zonk the existential variables, because their
+          -- /kind/ need potential zonking.
+          -- cf typecheck/should_compile/tc221.hs
+       ; (env1, new_evs) <- zonkEvBndrsX env0 evs
+       ; (env2, new_binds) <- zonkTcEvBinds env1 binds
        ; (env', new_args) <- zonkConStuff env2 args
        ; (env', new_args) <- zonkConStuff env2 args
-       ; returnM (env', p { pat_ty = new_ty, pat_dicts = new_dicts, 
-                            pat_binds = new_binds, pat_args = new_args }) }
+       ; returnM (env', p { pat_ty = new_ty, 
+                             pat_tvs = new_tyvars,
+                             pat_dicts = new_evs, 
+                            pat_binds = new_binds, 
+                             pat_args = new_args }) }
 
 zonk_pat env (LitPat lit) = return (env, LitPat lit)
 
 
 zonk_pat env (LitPat lit) = return (env, LitPat lit)
 
@@ -856,10 +960,7 @@ zonk_pat env (SigPatOut pat ty)
 
 zonk_pat env (NPat lit mb_neg eq_expr)
   = do { lit' <- zonkOverLit env lit
 
 zonk_pat env (NPat lit mb_neg eq_expr)
   = do { lit' <- zonkOverLit env lit
-       ; mb_neg' <- case mb_neg of
-                       Nothing  -> return Nothing
-                       Just neg -> do { neg' <- zonkExpr env neg
-                                      ; return (Just neg') }
+       ; mb_neg' <- fmapMaybeM (zonkExpr env) mb_neg
        ; eq_expr' <- zonkExpr env eq_expr
        ; return (env, NPat lit' mb_neg' eq_expr') }
 
        ; eq_expr' <- zonkExpr env eq_expr
        ; return (env, NPat lit' mb_neg' eq_expr') }
 
@@ -868,7 +969,7 @@ zonk_pat env (NPlusKPat (L loc n) lit e1 e2)
        ; lit' <- zonkOverLit env lit
        ; e1' <- zonkExpr env e1
        ; e2' <- zonkExpr env e2
        ; lit' <- zonkOverLit env lit
        ; e1' <- zonkExpr env e1
        ; e2' <- zonkExpr env e2
-       ; return (extendZonkEnv1 env n', NPlusKPat (L loc n') lit' e1' e2') }
+       ; return (extendIdZonkEnv1 env n', NPlusKPat (L loc n') lit' e1' e2') }
 
 zonk_pat env (CoPat co_fn pat ty) 
   = do { (env', co_fn') <- zonkCoFn env co_fn
 
 zonk_pat env (CoPat co_fn pat ty) 
   = do { (env', co_fn') <- zonkCoFn env co_fn
@@ -918,8 +1019,8 @@ zonkForeignExports :: ZonkEnv -> [LForeignDecl TcId] -> TcM [LForeignDecl Id]
 zonkForeignExports env ls = mappM (wrapLocM (zonkForeignExport env)) ls
 
 zonkForeignExport :: ZonkEnv -> ForeignDecl TcId -> TcM (ForeignDecl Id)
 zonkForeignExports env ls = mappM (wrapLocM (zonkForeignExport env)) ls
 
 zonkForeignExport :: ZonkEnv -> ForeignDecl TcId -> TcM (ForeignDecl Id)
-zonkForeignExport env (ForeignExport i _hs_ty spec) =
-   returnM (ForeignExport (fmap (zonkIdOcc env) i) undefined spec)
+zonkForeignExport env (ForeignExport i _hs_ty co spec) =
+   returnM (ForeignExport (fmap (zonkIdOcc env) i) undefined co spec)
 zonkForeignExport _ for_imp 
   = returnM for_imp    -- Foreign imports don't need zonking
 \end{code}
 zonkForeignExport _ for_imp 
   = returnM for_imp    -- Foreign imports don't need zonking
 \end{code}
@@ -930,158 +1031,307 @@ zonkRules env rs = mappM (wrapLocM (zonkRule env)) rs
 
 zonkRule :: ZonkEnv -> RuleDecl TcId -> TcM (RuleDecl Id)
 zonkRule env (HsRule name act (vars{-::[RuleBndr TcId]-}) lhs fv_lhs rhs fv_rhs)
 
 zonkRule :: ZonkEnv -> RuleDecl TcId -> TcM (RuleDecl Id)
 zonkRule env (HsRule name act (vars{-::[RuleBndr TcId]-}) lhs fv_lhs rhs fv_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 ->
+  = do { unbound_tkv_set <- newMutVar emptyVarSet
+       ; let env_rule = setZonkType env (zonkTvCollecting unbound_tkv_set)
+              -- See Note [Zonking the LHS of a RULE]
 
 
-    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 fv_lhs new_rhs fv_rhs)
-               -- I hate this map RuleBndr stuff
+       ; (env_inside, new_bndrs) <- mapAccumLM zonk_bndr env_rule vars
+
+       ; new_lhs <- zonkLExpr env_inside lhs
+       ; new_rhs <- zonkLExpr env_inside rhs
+
+       ; unbound_tkvs <- readMutVar unbound_tkv_set
+
+       ; let final_bndrs :: [RuleBndr Var]
+             final_bndrs = map (RuleBndr . noLoc)
+                             (varSetElemsKvsFirst unbound_tkvs)
+                           ++ new_bndrs
+
+       ; return $ 
+         HsRule name act final_bndrs new_lhs fv_lhs new_rhs fv_rhs }
   where
   where
-   zonk_bndr (RuleBndr v) 
-       | isId (unLoc v) = wrapLocM (zonkIdBndr env)   v
-       | otherwise      = ASSERT( isImmutableTyVar (unLoc v) )
-                          return v
-   zonk_bndr (RuleBndrSig {}) = panic "zonk_bndr RuleBndrSig"
+   zonk_bndr env (RuleBndr (L loc v)) 
+      = do { (env', v') <- zonk_it env v
+           ; return (env', RuleBndr (L loc v')) }
+   zonk_bndr _ (RuleBndrSig {}) = panic "zonk_bndr RuleBndrSig"
+
+   zonk_it env v
+     | isId v     = do { v' <- zonkIdBndr env v
+                       ; return (extendIdZonkEnv1 env v', v') }
+     | otherwise  = ASSERT( isImmutableTyVar v)
+                    zonkTyBndrX env v
+                    -- DV: used to be return (env,v) but that is plain 
+                    -- wrong because we may need to go inside the kind 
+                    -- of v and zonk there!
 \end{code}
 
 \end{code}
 
+\begin{code}
+zonkVects :: ZonkEnv -> [LVectDecl TcId] -> TcM [LVectDecl Id]
+zonkVects env = mappM (wrapLocM (zonkVect env))
+
+zonkVect :: ZonkEnv -> VectDecl TcId -> TcM (VectDecl Id)
+zonkVect env (HsVect v e)
+  = do { v' <- wrapLocM (zonkIdBndr env) v
+       ; e' <- fmapMaybeM (zonkLExpr env) e
+       ; return $ HsVect v' e'
+       }
+zonkVect env (HsNoVect v)
+  = do { v' <- wrapLocM (zonkIdBndr env) v
+       ; return $ HsNoVect v'
+       }
+zonkVect _env (HsVectTypeOut s t rt)
+  = return $ HsVectTypeOut s t rt
+zonkVect _ (HsVectTypeIn _ _ _) = panic "TcHsSyn.zonkVect: HsVectTypeIn"
+zonkVect _env (HsVectClassOut c)
+  = return $ HsVectClassOut c
+zonkVect _ (HsVectClassIn _) = panic "TcHsSyn.zonkVect: HsVectClassIn"
+zonkVect _env (HsVectInstOut i)
+  = return $ HsVectInstOut i
+zonkVect _ (HsVectInstIn _) = panic "TcHsSyn.zonkVect: HsVectInstIn"
+\end{code}
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
-\subsection[BackSubst-Foreign]{Foreign exports}
+              Constraints and evidence
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
+zonkEvTerm :: ZonkEnv -> EvTerm -> TcM EvTerm
+zonkEvTerm env (EvId v)           = ASSERT2( isId v, ppr v ) 
+                                    return (EvId (zonkIdOcc env v))
+zonkEvTerm env (EvCoercion co)    = do { co' <- zonkTcLCoToLCo env co
+                                       ; return (EvCoercion co') }
+zonkEvTerm env (EvCast v co)      = ASSERT( isId v) 
+                                    do { co' <- zonkTcLCoToLCo env co
+                                       ; return (mkEvCast (zonkIdOcc env v) co') }
+
+zonkEvTerm env (EvKindCast v co) = ASSERT( isId v) 
+                                    do { co' <- zonkTcLCoToLCo env co
+                                       ; return (mkEvKindCast (zonkIdOcc env v) co') }
+
+zonkEvTerm env (EvTupleSel v n)   = return (EvTupleSel (zonkIdOcc env v) n)
+zonkEvTerm env (EvTupleMk vs)     = return (EvTupleMk (map (zonkIdOcc env) vs))
+zonkEvTerm env (EvSuperClass d n) = return (EvSuperClass (zonkIdOcc env d) n)
+zonkEvTerm env (EvDFunApp df tys tms)
+  = do { tys' <- zonkTcTypeToTypes env tys
+       ; let tms' = map (zonkEvVarOcc env) tms
+       ; return (EvDFunApp (zonkIdOcc env df) tys' tms') }
+zonkEvTerm env (EvDelayedError ty msg)
+  = do { ty' <- zonkTcTypeToType env ty
+       ; return (EvDelayedError ty' msg) }
+
+zonkTcEvBinds :: ZonkEnv -> TcEvBinds -> TcM (ZonkEnv, TcEvBinds)
+zonkTcEvBinds env (TcEvBinds var) = do { (env', bs') <- zonkEvBindsVar env var
+                                      ; return (env', EvBinds bs') }
+zonkTcEvBinds env (EvBinds bs)    = do { (env', bs') <- zonkEvBinds env bs
+                                      ; return (env', EvBinds bs') }
+
+zonkEvBindsVar :: ZonkEnv -> EvBindsVar -> TcM (ZonkEnv, Bag EvBind)
+zonkEvBindsVar env (EvBindsVar ref _) = do { bs <- readMutVar ref
+                                           ; zonkEvBinds env (evBindMapBinds bs) }
+
+zonkEvBinds :: ZonkEnv -> Bag EvBind -> TcM (ZonkEnv, Bag EvBind)
+zonkEvBinds env binds
+  = {-# SCC "zonkEvBinds" #-}
+    fixM (\ ~( _, new_binds) -> do
+        { let env1 = extendIdZonkEnv env (collect_ev_bndrs new_binds)
+         ; binds' <- mapBagM (zonkEvBind env1) binds
+         ; return (env1, binds') })
+  where
+    collect_ev_bndrs :: Bag EvBind -> [EvVar]
+    collect_ev_bndrs = foldrBag add [] 
+    add (EvBind var _) vars = var : vars
+
+zonkEvBind :: ZonkEnv -> EvBind -> TcM EvBind
+zonkEvBind env (EvBind var term)
+  -- This function has some special cases for avoiding re-zonking the
+  -- same types many types. See Note [Optimized Evidence Binding Zonking]
+  = case term of 
+      -- Fast path for reflexivity coercions:
+      EvCoercion co 
+        | Just ty <- isTcReflCo_maybe co
+        ->
+          do { zty  <- zonkTcTypeToType env ty
+             ; let var' = setVarType var (mkEqPred (zty,zty))
+             ; return (EvBind var' (EvCoercion (mkTcReflCo zty))) }
+
+      -- Fast path for variable-variable bindings 
+      -- NB: could be optimized further! (e.g. SymCo cv)
+        | Just cv <- getTcCoVar_maybe co 
+        -> do { let cv' = zonkIdOcc env cv -- Just lazily look up
+                    term' = EvCoercion (TcCoVarCo cv')
+                    var'  = setVarType var (varType cv')
+              ; return (EvBind var' term') }
+      -- Ugly safe and slow path
+      _ -> do { var'  <- {-# SCC "zonkEvBndr" #-} zonkEvBndr env var
+              ; term' <- zonkEvTerm env term 
+              ; return (EvBind var' term')
+              }
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+                         Zonking types
+%*                                                                     *
+%************************************************************************
+
+Note [Zonking the LHS of a RULE]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+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 get zonkTvCollecting to gather 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)
+
+And that in turn is why ZonkEnv carries the function to use for
+type variables!
+
+Note [Zonking mutable unbound type or kind variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In zonkTypeZapping, we zonk mutable but unbound type or kind variables to an
+arbitrary type. We know if they are unbound even though we don't carry an
+environment, because at the binding site for a variable we bind the mutable
+var to a fresh immutable one.  So the mutable store plays the role of an
+environment.  If we come across a mutable variable that isn't so bound, it
+must be completely free. We zonk the expected kind to make sure we don't get
+some unbound meta variable as the kind.
+
+Note that since we have kind polymorphism, zonk_unbound_tyvar will handle both
+type and kind variables. Consider the following datatype:
+
+  data Phantom a = Phantom Int
+
+The type of Phantom is (forall (k : BOX). forall (a : k). Int). Both `a` and
+`k` are unbound variables. We want to zonk this to
+(forall (k : AnyK). forall (a : Any AnyK). Int). For that we have to check if
+we have a type or a kind variable; for kind variables we just return AnyK (and
+not the ill-kinded Any BOX).
+
+Note [Optimized Evidence Binding Zonking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+When optimising evidence binds we may come accross situations where 
+a coercion is just reflexivity: 
+      cv = ReflCo ty
+In such a case it is a waste of time to zonk both ty and the type 
+of the coercion, especially if the types involved are huge. For this
+reason this case is optimized to only zonk 'ty' and set the type of 
+the variable to be that zonked type.
+
+Another case that hurts a lot are simple coercion bindings of the form:
+      cv1 = cv2
+      cv3 = cv1
+      cv4 = cv2 
+etc. In all such cases it is very easy to just get the zonked type of 
+cv2 and use it to set the type of the LHS coercion variable without zonking
+twice. Though this case is funny, it can happen due the way that evidence 
+from spontaneously solved goals is now used.
+See Note [Optimizing Spontaneously Solved Goals] about this.
+
+NB: That these optimizations are independently useful, regardless of the 
+constraint solver strategy.
+
+DV, TODO: followup on this note mentioning new examples I will add to perf/
+
+
+\begin{code}
+mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
+             -> (TcTyVar -> Type)      -- What to do for an immutable var
+             -> TcTyVar -> TcM TcType
+mkZonkTcTyVar unbound_mvar_fn unbound_ivar_fn
+  = zonk_tv
+  where
+    zonk_tv tv 
+     = ASSERT( isTcTyVar tv )
+       case tcTyVarDetails tv of
+         SkolemTv {}    -> return (unbound_ivar_fn tv)
+         RuntimeUnk {}  -> return (unbound_ivar_fn tv)
+         FlatSkol ty    -> zonkType zonk_tv ty
+         MetaTv _ ref   -> do { cts <- readMutVar ref
+                             ; case cts of    
+                                  Flexi -> do { kind <- {-# SCC "zonkKind1" #-}
+                                                         zonkType zonk_tv (tyVarKind tv)
+                                               ; unbound_mvar_fn (setTyVarKind tv kind) }
+                                  Indirect ty -> do { zty <- zonkType zonk_tv ty 
+                                                     -- Small optimisation: shortern-out indirect steps
+                                                     -- so that the old type may be more easily collected.
+                                                     ; writeMutVar ref (Indirect zty)
+                                                     ; return zty } }
+
 zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
 zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
-zonkTcTypeToType (ZonkEnv zonk_ty _) ty = zonk_ty ty
+zonkTcTypeToType (ZonkEnv zonk_unbound_tyvar tv_env _id_env)
+  = zonkType (mkZonkTcTyVar zonk_unbound_tyvar zonk_bound_tyvar)
+  where
+    zonk_bound_tyvar tv = case lookupVarEnv tv_env tv of
+                            Nothing  -> mkTyVarTy tv
+                            Just tv' -> mkTyVarTy tv'
 
 zonkTcTypeToTypes :: ZonkEnv -> [TcType] -> TcM [Type]
 zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
 
 
 zonkTcTypeToTypes :: ZonkEnv -> [TcType] -> TcM [Type]
 zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
 
-zonkTypeCollecting :: TcRef TyVarSet -> TcType -> TcM Type
+zonkTvCollecting :: TcRef TyVarSet -> UnboundTyVarZonker
 -- This variant collects unbound type variables in a mutable variable
 -- 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
+-- Works on both types and kinds
+zonkTvCollecting unbound_tv_set tv
+  = do { poly_kinds <- xoptM Opt_PolyKinds
+       ; if isKiVar tv && not poly_kinds then defaultKindVarToStar tv
+         else do
+       { tv' <- zonkQuantifiedTyVar tv
+       ; tv_set <- readMutVar unbound_tv_set
+       ; writeMutVar unbound_tv_set (extendVarSet tv_set tv')
+       ; return (mkTyVarTy tv') } }
+
+zonkTypeZapping :: UnboundTyVarZonker
 -- This variant is used for everything except the LHS of rules
 -- It zaps unbound type variables to (), or some other arbitrary 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 { ty <- mkArbitraryType warn tv
-                              ; writeMetaTyVar tv ty
-                              ; return ty }
-       where
-           warn span msg = setSrcSpan span (addWarnTc msg)
-
-
-{-     Note [Strangely-kinded void TyCons]
-       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-       See Trac #959 for more examples
-
-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.
-
-Meanwhile I have now fixed GHC to emit a civilized warning.
- -}
-
-mkArbitraryType :: (SrcSpan -> SDoc -> TcRnIf g l a)   -- How to complain
-               -> TcTyVar
-               -> TcRnIf g l Type              -- Used by desugarer too
--- Make up an arbitrary type whose kind is the same as the tyvar.
--- We'll use this to instantiate the (unbound) tyvar.
---
--- Also used by the desugarer; hence the (tiresome) parameter
--- to use when generating a warning
-mkArbitraryType warn tv 
-  | liftedTypeKind `isSubKind` kind            -- The vastly common case
-  = return anyPrimTy
-  | eqKind kind (tyConKind anyPrimTyCon1)      -- @*->*@
-  = return (mkTyConApp anyPrimTyCon1 [])       --     No tuples this size
-  | all isLiftedTypeKind args                  -- @*-> ... ->*->*@
-  , isLiftedTypeKind res                       --    Horrible hack to make less use 
-  = return (mkTyConApp tup_tc [])              --    of mkAnyPrimTyCon
-  | otherwise
-  = do { _ <- warn (getSrcSpan tv) msg
-       ; return (mkTyConApp (mkAnyPrimTyCon (getUnique tv) kind) []) }
-               -- 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.
+-- Works on both types and kinds
+zonkTypeZapping tv
+  = do { let ty = if isKiVar tv
+                  -- ty is actually a kind, zonk to AnyK
+                  then anyKind
+                  else anyTypeOfKind (tyVarKind tv)
+       ; writeMetaTyVar tv ty
+       ; return ty }
+
+
+zonkTcLCoToLCo :: ZonkEnv -> TcCoercion -> TcM TcCoercion
+-- NB: zonking often reveals that the coercion is an identity
+--     in which case the Refl-ness can propagate up to the top
+--     which in turn gives more efficient desugaring.  So it's
+--     worth using the 'mk' smart constructors on the RHS
+zonkTcLCoToLCo env co
+  = go co
   where
   where
-    kind       = tyVarKind tv
-    (args,res) = splitKindFunTys kind
-    tup_tc     = tupleTyCon Boxed (length args)
-               
-    msg = vcat [ hang (ptext (sLit "Inventing strangely-kinded Any TyCon"))
-                   2 (ptext (sLit "of kind") <+> quotes (ppr kind))
-              , nest 2 (ptext (sLit "from an instantiation of type variable") <+> quotes (ppr tv))
-              , ptext (sLit "This warning can be suppressed by a type signature fixing") <+> quotes (ppr tv)
-              , nest 2 (ptext (sLit "but is harmless without -O (and usually harmless anyway)."))
-              , ptext (sLit "See http://hackage.haskell.org/trac/ghc/ticket/959 for details")  ]
+    go (TcLetCo bs co)        = do { (env', bs') <- zonkTcEvBinds env bs
+                                   ; co' <- zonkTcLCoToLCo env' co
+                                   ; return (TcLetCo bs' co') }
+    go (TcCoVarCo cv)         = return (mkTcCoVarCo (zonkEvVarOcc env cv))
+    go (TcRefl ty)            = do { ty' <- zonkTcTypeToType env ty
+                                   ; return (TcRefl ty') }
+    go (TcTyConAppCo tc cos)  = do { cos' <- mapM go cos; return (mkTcTyConAppCo tc cos') }
+    go (TcAxiomInstCo ax tys) = do { tys' <- zonkTcTypeToTypes env tys; return (TcAxiomInstCo ax tys') }
+    go (TcAppCo co1 co2)      = do { co1' <- go co1; co2' <- go co2
+                                   ; return (mkTcAppCo co1' co2') }
+    go (TcSymCo co)           = do { co' <- go co; return (mkTcSymCo co')  }
+    go (TcNthCo n co)         = do { co' <- go co; return (mkTcNthCo n co')  }
+    go (TcTransCo co1 co2)    = do { co1' <- go co1; co2' <- go co2
+                                   ; return (mkTcTransCo co1' co2')  }
+    go (TcForAllCo tv co)     = ASSERT( isImmutableTyVar tv )
+                                do { co' <- go co; return (mkTcForAllCo tv co') }
+    go (TcInstCo co ty)       = do { co' <- go co; ty' <- zonkTcTypeToType env ty; return (TcInstCo co' ty') }
 \end{code}
 \end{code}