Get rid of TcTyVars more assiduously
[ghc.git] / compiler / typecheck / TcHsSyn.hs
index 80dd175..2589576 100644 (file)
@@ -9,23 +9,32 @@ This module is an extension of @HsSyn@ syntax, for use in the type
 checker.
 -}
 
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, TupleSections #-}
 
 module TcHsSyn (
-        mkHsConApp, mkHsDictLet, mkHsApp,
+        mkHsDictLet, mkHsApp,
         hsLitType, hsLPatType, hsPatType,
-        mkHsAppTy, mkSimpleHsAlt,
+        mkHsAppTy, mkHsCaseAlt,
         nlHsIntLit,
         shortCutLit, hsOverLitName,
         conLikeResTy,
 
-        -- re-exported from TcMonad
+        -- re-exported from TcMonad
         TcId, TcIdSet,
 
+        -- * Zonking
+        -- | For a description of "zonking", see Note [What is zonking?]
+        -- in TcMType
         zonkTopDecls, zonkTopExpr, zonkTopLExpr,
         zonkTopBndrs, zonkTyBndrsX,
-        emptyZonkEnv, mkEmptyZonkEnv, mkTyVarZonkEnv,
+        zonkTyConBinders,
+        emptyZonkEnv, mkEmptyZonkEnv,
         zonkTcTypeToType, zonkTcTypeToTypes, zonkTyVarOcc,
+        zonkCoToCo, zonkSigType,
+        zonkEvBinds,
+
+        -- * Validity checking
+        checkForRepresentationPolymorphism
   ) where
 
 #include "HsVersions.h"
@@ -34,20 +43,19 @@ import HsSyn
 import Id
 import TcRnMonad
 import PrelNames
-import TypeRep     -- We can see the representation of types
 import TcType
-import RdrName ( RdrName, rdrNameOcc )
-import TcMType ( defaultKindVarToStar, zonkQuantifiedTyVar, writeMetaTyVar )
+import TcMType
 import TcEvidence
-import Coercion
 import TysPrim
 import TysWiredIn
 import Type
+import TyCon
+import Coercion
 import ConLike
 import DataCon
-import PatSyn( patSynInstResTy )
+import HscTypes
 import Name
-import NameSet
+import NameEnv
 import Var
 import VarSet
 import VarEnv
@@ -57,12 +65,13 @@ import BasicTypes
 import Maybes
 import SrcLoc
 import Bag
-import FastString
 import Outputable
 import Util
-#if __GLASGOW_HASKELL__ < 709
-import Data.Traversable ( traverse )
-#endif
+import UniqFM
+
+import Control.Monad
+import Data.List  ( partition )
+import Control.Arrow ( second )
 
 {-
 ************************************************************************
@@ -81,7 +90,7 @@ hsLPatType (L _ pat) = hsPatType pat
 hsPatType :: Pat Id -> Type
 hsPatType (ParPat pat)                = hsLPatType pat
 hsPatType (WildPat ty)                = ty
-hsPatType (VarPat var)                = idType var
+hsPatType (VarPat (L _ var))          = idType var
 hsPatType (BangPat pat)               = hsLPatType pat
 hsPatType (LazyPat pat)               = hsLPatType pat
 hsPatType (LitPat lit)                = hsLitType lit
@@ -90,18 +99,16 @@ hsPatType (ViewPat _ _ ty)            = ty
 hsPatType (ListPat _ ty Nothing)      = mkListTy ty
 hsPatType (ListPat _ _ (Just (ty,_))) = ty
 hsPatType (PArrPat _ ty)              = mkPArrTy ty
-hsPatType (TuplePat _ bx tys)         = mkTupleTy (boxityNormalTupleSort bx) tys
+hsPatType (TuplePat _ bx tys)         = mkTupleTy bx tys
+hsPatType (SumPat _ _ _ tys)          = mkSumTy tys
 hsPatType (ConPatOut { pat_con = L _ con, pat_arg_tys = tys })
                                       = conLikeResTy con tys
 hsPatType (SigPatOut _ ty)            = ty
-hsPatType (NPat (L _ lit) _ _)        = overLitType lit
-hsPatType (NPlusKPat id _ _ _)        = idType (unLoc id)
+hsPatType (NPat _ _ _ ty)             = ty
+hsPatType (NPlusKPat _ _ _ _ _ ty)    = ty
 hsPatType (CoPat _ _ ty)              = ty
 hsPatType p                           = pprPanic "hsPatType" (ppr p)
 
-conLikeResTy :: ConLike -> [Type] -> Type
-conLikeResTy (RealDataCon con) tys = mkTyConApp (dataConTyCon con) tys
-conLikeResTy (PatSynCon ps)    tys = patSynInstResTy ps tys
 
 hsLitType :: HsLit -> TcType
 hsLitType (HsChar _ _)       = charTy
@@ -177,15 +184,35 @@ It's all pretty boring stuff, because HsSyn is such a large type, and
 the environment manipulation is tiresome.
 -}
 
-type UnboundTyVarZonker = TcTyVar-> TcM Type
+-- Confused by zonking? See Note [What is zonking?] in TcMType.
+type UnboundTyVarZonker = TcTyVar -> TcM Type
         -- How to zonk an unbound type variable
+        -- The TcTyVar is (a) a MetaTv (b) Flexi and
+        --     (c) its kind is alrady zonked
         -- Note [Zonking the LHS of a RULE]
 
+-- | A ZonkEnv carries around several bits.
+-- The UnboundTyVarZonker just zaps unbouned meta-tyvars to Any (as
+-- defined in zonkTypeZapping), except on the LHS of rules. See
+-- Note [Zonking the LHS of a RULE].
+--
+-- The (TyCoVarEnv TyVar) and is just an optimisation: when binding a
+-- tyvar or covar, we zonk the kind right away and add a mapping to
+-- the env. This prevents re-zonking the kind at every occurrence. But
+-- this is *just* an optimisation.
+--
+-- The final (IdEnv Var) optimises zonking for Ids. It is
+-- knot-tied. We must be careful never to put coercion variables
+-- (which are Ids, after all) in the knot-tied env, because coercions
+-- can appear in types, and we sometimes inspect a zonked type in this
+-- module.
+--
+-- Confused by zonking? See Note [What is zonking?] in TcMType.
 data ZonkEnv
   = ZonkEnv
       UnboundTyVarZonker
-      (TyVarEnv TyVar)          --
-      (IdEnv    Var)            -- What variables are in scope
+      (TyCoVarEnv 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
@@ -193,35 +220,52 @@ data ZonkEnv
         -- Is only consulted lazily; hence knot-tying
 
 instance Outputable ZonkEnv where
-  ppr (ZonkEnv _ _ty_env var_env) = vcat (map ppr (varEnvElts var_env))
+  ppr (ZonkEnv _ _ty_env var_env) = pprUFM var_env (vcat . map ppr)
 
 
+-- The EvBinds have to already be zonked, but that's usually the case.
 emptyZonkEnv :: ZonkEnv
 emptyZonkEnv = mkEmptyZonkEnv zonkTypeZapping
 
 mkEmptyZonkEnv :: UnboundTyVarZonker -> ZonkEnv
 mkEmptyZonkEnv zonker = ZonkEnv zonker emptyVarEnv emptyVarEnv
 
-extendIdZonkEnv :: ZonkEnv -> [Var] -> ZonkEnv
-extendIdZonkEnv (ZonkEnv zonk_ty ty_env id_env) ids
+-- | Extend the knot-tied environment.
+extendIdZonkEnvRec :: ZonkEnv -> [Var] -> ZonkEnv
+extendIdZonkEnvRec (ZonkEnv zonk_ty ty_env id_env) ids
+    -- NB: Don't look at the var to decide which env't to put it in. That
+    -- would end up knot-tying all the env'ts.
   = ZonkEnv zonk_ty ty_env (extendVarEnvList id_env [(id,id) | id <- ids])
+  -- Given coercion variables will actually end up here. That's OK though:
+  -- coercion variables are never looked up in the knot-tied env't, so zonking
+  -- them simply doesn't get optimised. No one gets hurt. An improvement (?)
+  -- would be to do SCC analysis in zonkEvBinds and then only knot-tie the
+  -- recursive groups. But perhaps the time it takes to do the analysis is
+  -- more than the savings.
+
+extendZonkEnv :: ZonkEnv -> [Var] -> ZonkEnv
+extendZonkEnv (ZonkEnv zonk_ty tyco_env id_env) vars
+  = ZonkEnv zonk_ty (extendVarEnvList tyco_env [(tv,tv) | tv <- tycovars])
+                    (extendVarEnvList id_env   [(id,id) | id <- ids])
+  where (tycovars, ids) = partition isTyCoVar vars
 
 extendIdZonkEnv1 :: ZonkEnv -> Var -> ZonkEnv
 extendIdZonkEnv1 (ZonkEnv zonk_ty ty_env id_env) id
   = ZonkEnv zonk_ty ty_env (extendVarEnv id_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
-
-mkTyVarZonkEnv :: [TyVar] -> ZonkEnv
-mkTyVarZonkEnv tvs = ZonkEnv zonkTypeZapping (mkVarEnv [(tv,tv) | tv <- tvs]) emptyVarEnv
+extendTyZonkEnv1 (ZonkEnv zonk_ty ty_env id_env) tv
+  = ZonkEnv zonk_ty (extendVarEnv ty_env tv tv) id_env
 
 setZonkType :: ZonkEnv -> UnboundTyVarZonker -> ZonkEnv
-setZonkType (ZonkEnv _ ty_env id_env) zonk_ty = ZonkEnv zonk_ty ty_env id_env
+setZonkType (ZonkEnv _ ty_env id_env) zonk_ty
+  = ZonkEnv zonk_ty ty_env id_env
 
-zonkEnvIds :: ZonkEnv -> [Id]
-zonkEnvIds (ZonkEnv _ _ id_env) = varEnvElts id_env
+zonkEnvIds :: ZonkEnv -> TypeEnv
+zonkEnvIds (ZonkEnv _ _ id_env) =
+  mkNameEnv [(getName id, AnId id) | id <- nonDetEltsUFM id_env]
+  -- It's OK to use nonDetEltsUFM here because we forget the ordering
+  -- immediately by creating a TypeEnv
 
 zonkIdOcc :: ZonkEnv -> TcId -> Id
 -- Ids defined in this module should be in the envt;
@@ -239,8 +283,9 @@ zonkIdOcc :: ZonkEnv -> TcId -> Id
 --
 -- Even without template splices, in module Main, the checking of
 -- 'main' is done as a separate chunk.
-zonkIdOcc (ZonkEnv _zonk_ty _ty_env env) id
-  | isLocalVar id = lookupVarEnv env id `orElse` id
+zonkIdOcc (ZonkEnv _zonk_ty _ty_env id_env) id
+  | isLocalVar id = lookupVarEnv id_env id `orElse`
+                    id
   | otherwise     = id
 
 zonkIdOccs :: ZonkEnv -> [TcId] -> [Id]
@@ -251,7 +296,9 @@ zonkIdOccs env ids = map (zonkIdOcc env) ids
 zonkIdBndr :: ZonkEnv -> TcId -> TcM Id
 zonkIdBndr env id
   = do ty' <- zonkTcTypeToType env (idType id)
-       return (Id.setIdType id ty')
+       ensureNotRepresentationPolymorphic ty'
+         (text "In the type of binder" <+> quotes (ppr id))
+       return (setIdType id ty')
 
 zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id]
 zonkIdBndrs env ids = mapM (zonkIdBndr env) ids
@@ -259,6 +306,9 @@ zonkIdBndrs env ids = mapM (zonkIdBndr env) ids
 zonkTopBndrs :: [TcId] -> TcM [Id]
 zonkTopBndrs ids = zonkIdBndrs emptyZonkEnv ids
 
+zonkFieldOcc :: ZonkEnv -> FieldOcc TcId -> TcM (FieldOcc Id)
+zonkFieldOcc env (FieldOcc lbl sel) = fmap (FieldOcc lbl) $ zonkIdBndr env sel
+
 zonkEvBndrsX :: ZonkEnv -> [EvVar] -> TcM (ZonkEnv, [Var])
 zonkEvBndrsX = mapAccumLM zonkEvBndrX
 
@@ -266,7 +316,7 @@ zonkEvBndrX :: ZonkEnv -> EvVar -> TcM (ZonkEnv, EvVar)
 -- Works for dictionaries and coercions
 zonkEvBndrX env var
   = do { var' <- zonkEvBndr env var
-       ; return (extendIdZonkEnv1 env var', var') }
+       ; return (extendZonkEnv env [var'], var') }
 
 zonkEvBndr :: ZonkEnv -> EvVar -> TcM EvVar
 -- Works for dictionaries and coercions
@@ -278,8 +328,12 @@ zonkEvBndr env var
            zonkTcTypeToType env var_ty
        ; return (setVarType var ty) }
 
-zonkEvVarOcc :: ZonkEnv -> EvVar -> EvVar
-zonkEvVarOcc env v = zonkIdOcc env v
+zonkEvVarOcc :: ZonkEnv -> EvVar -> TcM EvTerm
+zonkEvVarOcc env v
+  | isCoVar v
+  = EvCoercion <$> zonkCoVarOcc env v
+  | otherwise
+  = return (EvId $ zonkIdOcc env v)
 
 zonkTyBndrsX :: ZonkEnv -> [TyVar] -> TcM (ZonkEnv, [TyVar])
 zonkTyBndrsX = mapAccumLM zonkTyBndrX
@@ -288,10 +342,20 @@ zonkTyBndrX :: ZonkEnv -> TyVar -> TcM (ZonkEnv, TyVar)
 -- This guarantees to return a TyVar (not a TcTyVar)
 -- then we add it to the envt, so all occurrences are replaced
 zonkTyBndrX env tv
-  = do { ki <- zonkTcTypeToType env (tyVarKind tv)
+  = ASSERT( isImmutableTyVar tv )
+    do { ki <- zonkTcTypeToType env (tyVarKind tv)
+               -- Internal names tidy up better, for iface files.
        ; let tv' = mkTyVar (tyVarName tv) ki
        ; return (extendTyZonkEnv1 env tv', tv') }
 
+zonkTyConBinders :: ZonkEnv -> [TyConBinder] -> TcM (ZonkEnv, [TyConBinder])
+zonkTyConBinders = mapAccumLM zonkTyConBinderX
+
+zonkTyConBinderX :: ZonkEnv -> TyConBinder -> TcM (ZonkEnv, TyConBinder)
+zonkTyConBinderX env (TvBndr tv vis)
+  = do { (env', tv') <- zonkTyBndrX env tv
+       ; return (env', TvBndr tv' vis) }
+
 zonkTopExpr :: HsExpr TcId -> TcM (HsExpr Id)
 zonkTopExpr e = zonkExpr emptyZonkEnv e
 
@@ -299,33 +363,18 @@ zonkTopLExpr :: LHsExpr TcId -> TcM (LHsExpr Id)
 zonkTopLExpr e = zonkLExpr emptyZonkEnv e
 
 zonkTopDecls :: Bag EvBind
-             -> LHsBinds TcId 
-             -> Maybe (Located [LIE RdrName]) 
-             -> NameSet
+             -> LHsBinds TcId
              -> [LRuleDecl TcId] -> [LVectDecl TcId] -> [LTcSpecPrag] -> [LForeignDecl TcId]
-             -> TcM ([Id],
+             -> TcM (TypeEnv,
                      Bag EvBind,
                      LHsBinds Id,
                      [LForeignDecl Id],
                      [LTcSpecPrag],
                      [LRuleDecl    Id],
                      [LVectDecl    Id])
-zonkTopDecls ev_binds binds export_ies sig_ns rules vects imp_specs fords
+zonkTopDecls ev_binds binds 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
-        ; warn_only_exported <- woptM Opt_WarnMissingExportedSigs
-        ; let export_occs  = maybe emptyBag
-                                   (listToBag . map (rdrNameOcc . ieName . unLoc) . unLoc)
-                                   export_ies
-              sig_warn
-                | warn_only_exported = topSigWarnIfExported export_occs sig_ns
-                | warn_missing_sigs  = topSigWarn sig_ns
-                | otherwise          = noSigWarn
-
-        ; (env2, binds') <- zonkRecMonoBinds env1 sig_warn binds
+        ; (env2, binds') <- zonkRecMonoBinds env1 binds
                         -- Top level is implicitly recursive
         ; rules' <- zonkRules env2 rules
         ; vects' <- zonkVects env2 vects
@@ -341,25 +390,21 @@ zonkLocalBinds env EmptyLocalBinds
 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
+zonkLocalBinds env (HsValBinds (ValBindsOut binds sigs))
+  = do  { (env1, new_binds) <- go env binds
         ; return (env1, HsValBinds (ValBindsOut new_binds sigs)) }
   where
-    go env []
+    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
+    go env ((r,b):bs)
+      = do { (env1, b')  <- zonkRecMonoBinds env b
+           ; (env2, bs') <- go env1 bs
            ; return (env2, (r,b'):bs') }
 
 zonkLocalBinds env (HsIPBinds (IPBinds binds dict_binds)) = do
     new_binds <- mapM (wrapLocM zonk_ip_bind) binds
     let
-        env1 = extendIdZonkEnv env [ n | L _ (IPBind (Right n) _) <- new_binds]
+        env1 = extendIdZonkEnvRec env [ n | L _ (IPBind (Right n) _) <- new_binds]
     (env2, new_dict_binds) <- zonkTcEvBinds env1 dict_binds
     return (env2, HsIPBinds (IPBinds new_binds new_dict_binds))
   where
@@ -369,132 +414,114 @@ zonkLocalBinds env (HsIPBinds (IPBinds binds dict_binds)) = do
              return (IPBind n' e')
 
 ---------------------------------------------
-zonkRecMonoBinds :: ZonkEnv -> SigWarn -> LHsBinds TcId -> TcM (ZonkEnv, LHsBinds Id)
-zonkRecMonoBinds env sig_warn binds
+zonkRecMonoBinds :: ZonkEnv -> LHsBinds TcId -> TcM (ZonkEnv, LHsBinds Id)
+zonkRecMonoBinds env binds
  = fixM (\ ~(_, new_binds) -> do
-        { let env1 = extendIdZonkEnv env (collectHsBindsBinders new_binds)
-        ; binds' <- zonkMonoBinds env1 sig_warn binds
+        { let env1 = extendIdZonkEnvRec env (collectHsBindsBinders new_binds)
+        ; binds' <- zonkMonoBinds env1 binds
         ; return (env1, binds') })
 
 ---------------------------------------------
-type SigWarn = Bool -> [Id] -> TcM ()
-     -- Missing-signature warning
-     -- The Bool is True for an AbsBinds, False otherwise
-
-noSigWarn :: SigWarn
-noSigWarn _ _ = return ()
+zonkMonoBinds :: ZonkEnv -> LHsBinds TcId -> TcM (LHsBinds Id)
+zonkMonoBinds env binds = mapBagM (zonk_lbind env) binds
 
-topSigWarnIfExported :: Bag OccName -> NameSet -> SigWarn
-topSigWarnIfExported exported sig_ns _ ids
-  = mapM_ (topSigWarnIdIfExported exported sig_ns) ids
+zonk_lbind :: ZonkEnv -> LHsBind TcId -> TcM (LHsBind Id)
+zonk_lbind env = wrapLocM (zonk_bind env)
 
-topSigWarnIdIfExported :: Bag OccName -> NameSet -> Id -> TcM ()
-topSigWarnIdIfExported exported sig_ns id
-  | getOccName id `elemBag` exported
-  = topSigWarnId sig_ns id
-  | otherwise
-  = 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
-    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 "Polymorphic local binding with no type signature:")
-
-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 -> SigWarn -> LHsBinds TcId -> TcM (LHsBinds Id)
-zonkMonoBinds env sig_warn binds = mapBagM (zonk_lbind env sig_warn) binds
-
-zonk_lbind :: ZonkEnv -> SigWarn -> LHsBind TcId -> TcM (LHsBind Id)
-zonk_lbind env sig_warn = wrapLocM (zonk_bind env sig_warn)
-
-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})
+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
-        ; sig_warn False (collectPatBinders new_pat)
         ; new_grhss <- zonkGRHSs env zonkLExpr grhss
         ; new_ty    <- zonkTcTypeToType env ty
         ; return (bind { pat_lhs = new_pat, pat_rhs = new_grhss, pat_rhs_ty = new_ty }) }
 
-zonk_bind env sig_warn (VarBind { var_id = var, var_rhs = expr, var_inline = inl })
+zonk_bind env (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 })
+zonk_bind env 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 zonkLExpr 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 })
+zonk_bind env (AbsBinds { abs_tvs = tyvars, abs_ev_vars = evs
+                        , abs_ev_binds = ev_binds
+                        , abs_exports = exports
+                        , abs_binds = val_binds })
   = ASSERT( all isImmutableTyVar tyvars )
     do { (env0, new_tyvars) <- zonkTyBndrsX env tyvars
        ; (env1, new_evs) <- zonkEvBndrsX env0 evs
        ; (env2, new_ev_binds) <- zonkTcEvBinds_s 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
+         do { let env3 = extendIdZonkEnvRec env2
+                           (collectHsBindsBinders new_val_binds)
+            ; new_val_binds <- zonkMonoBinds env3 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
-    zonkExport env (ABE{ abe_wrap = wrap, abe_poly = poly_id
+    zonkExport env (ABE{ abe_wrap = wrap
+                       , abe_poly = poly_id
                        , abe_mono = mono_id, abe_prags = prags })
         = do new_poly_id <- zonkIdBndr env poly_id
              (_, new_wrap) <- zonkCoFn env wrap
              new_prags <- zonkSpecPrags env prags
-             return (ABE{ abe_wrap = new_wrap, abe_poly = new_poly_id
+             return (ABE{ abe_wrap = new_wrap
+                        , abe_poly = new_poly_id
                         , abe_mono = zonkIdOcc env mono_id
                         , abe_prags = new_prags })
 
-zonk_bind env _sig_warn (PatSynBind bind@(PSB { psb_id = L loc id
-                                              , psb_args = details
-                                              , psb_def = lpat
-                                              , psb_dir = dir }))
+zonk_bind env outer_bind@(AbsBindsSig { abs_tvs         = tyvars
+                                      , abs_ev_vars     = evs
+                                      , abs_sig_export  = poly
+                                      , abs_sig_prags   = prags
+                                      , abs_sig_ev_bind = ev_bind
+                                      , abs_sig_bind    = lbind })
+  | L bind_loc bind@(FunBind { fun_id      = L loc local
+                             , fun_matches = ms
+                             , fun_co_fn   = co_fn }) <- lbind
+  = ASSERT( all isImmutableTyVar tyvars )
+    do { (env0, new_tyvars)  <- zonkTyBndrsX env  tyvars
+       ; (env1, new_evs)     <- zonkEvBndrsX env0 evs
+       ; (env2, new_ev_bind) <- zonkTcEvBinds env1 ev_bind
+           -- Inline zonk_bind (FunBind ...) because we wish to skip
+           -- the check for representation-polymorphic binders. The
+           -- local binder in the FunBind in an AbsBindsSig is never actually
+           -- bound in Core -- indeed, that's the whole point of AbsBindsSig.
+           -- just calling zonk_bind causes #11405.
+       ; new_local           <- updateVarTypeM (zonkTcTypeToType env2) local
+       ; (env3, new_co_fn)   <- zonkCoFn env2 co_fn
+       ; new_ms              <- zonkMatchGroup env3 zonkLExpr ms
+           -- If there is a representation polymorphism problem, it will
+           -- be caught here:
+       ; new_poly_id         <- zonkIdBndr env2 poly
+       ; new_prags           <- zonkSpecPrags env2 prags
+       ; let new_val_bind = L bind_loc (bind { fun_id      = L loc new_local
+                                             , fun_matches = new_ms
+                                             , fun_co_fn   = new_co_fn })
+       ; return (AbsBindsSig { abs_tvs         = new_tyvars
+                             , abs_ev_vars     = new_evs
+                             , abs_sig_export  = new_poly_id
+                             , abs_sig_prags   = new_prags
+                             , abs_sig_ev_bind = new_ev_bind
+                             , abs_sig_bind    = new_val_bind  }) }
+
+  | otherwise
+  = pprPanic "zonk_bind" (ppr outer_bind)
+
+zonk_bind env (PatSynBind bind@(PSB { psb_id = L loc id
+                                    , psb_args = details
+                                    , psb_def = lpat
+                                    , psb_dir = dir }))
   = do { id' <- zonkIdBndr env id
        ; details' <- zonkPatSynDetails env details
-       ;(env1, lpat') <- zonkPat env lpat
+       ; (env1, lpat') <- zonkPat env lpat
        ; (_env2, dir') <- zonkPatSynDir env1 dir
        ; return $ PatSynBind $
                   bind { psb_id = L loc id'
@@ -538,11 +565,13 @@ zonkLTcSpecPrags env ps
 zonkMatchGroup :: ZonkEnv
                -> (ZonkEnv -> Located (body TcId) -> TcM (Located (body Id)))
                -> MatchGroup TcId (Located (body TcId)) -> TcM (MatchGroup Id (Located (body Id)))
-zonkMatchGroup env zBody (MG { mg_alts = ms, mg_arg_tys = arg_tys, mg_res_ty = res_ty, mg_origin = origin })
+zonkMatchGroup env zBody (MG { mg_alts = L l ms, mg_arg_tys = arg_tys
+                             , mg_res_ty = res_ty, mg_origin = origin })
   = do  { ms' <- mapM (zonkMatch env zBody) ms
         ; arg_tys' <- zonkTcTypeToTypes env arg_tys
         ; res_ty'  <- zonkTcTypeToType env res_ty
-        ; return (MG { mg_alts = ms', mg_arg_tys = arg_tys', mg_res_ty = res_ty', mg_origin = origin }) }
+        ; return (MG { mg_alts = L l ms', mg_arg_tys = arg_tys'
+                     , mg_res_ty = res_ty', mg_origin = origin }) }
 
 zonkMatch :: ZonkEnv
           -> (ZonkEnv -> Located (body TcId) -> TcM (Located (body Id)))
@@ -557,7 +586,7 @@ zonkGRHSs :: ZonkEnv
           -> (ZonkEnv -> Located (body TcId) -> TcM (Located (body Id)))
           -> GRHSs TcId (Located (body TcId)) -> TcM (GRHSs Id (Located (body Id)))
 
-zonkGRHSs env zBody (GRHSs grhss binds) = do
+zonkGRHSs env zBody (GRHSs grhss (L l binds)) = do
     (new_env, new_binds) <- zonkLocalBinds env binds
     let
         zonk_grhs (GRHS guarded rhs)
@@ -565,7 +594,7 @@ zonkGRHSs env zBody (GRHSs grhss binds) = do
                new_rhs <- zBody env2 rhs
                return (GRHS new_guarded new_rhs)
     new_grhss <- mapM (wrapLocM zonk_grhs) grhss
-    return (GRHSs new_grhss new_binds)
+    return (GRHSs new_grhss (L l new_binds))
 
 {-
 ************************************************************************
@@ -582,12 +611,15 @@ zonkExpr   :: ZonkEnv -> HsExpr TcId    -> TcM (HsExpr Id)
 zonkLExprs env exprs = mapM (zonkLExpr env) exprs
 zonkLExpr  env expr  = wrapLocM (zonkExpr env) expr
 
-zonkExpr env (HsVar id)
-  = return (HsVar (zonkIdOcc env id))
+zonkExpr env (HsVar (L l id))
+  = return (HsVar (L l (zonkIdOcc env id)))
 
 zonkExpr _ (HsIPVar id)
   = return (HsIPVar id)
 
+zonkExpr _ (HsOverLabel l)
+  = return (HsOverLabel l)
+
 zonkExpr env (HsLit (HsRat f ty))
   = do new_ty <- zonkTcTypeToType env ty
        return (HsLit (HsRat f new_ty))
@@ -603,16 +635,20 @@ zonkExpr env (HsLam matches)
   = do new_matches <- zonkMatchGroup env zonkLExpr matches
        return (HsLam new_matches)
 
-zonkExpr env (HsLamCase arg matches)
-  = do new_arg <- zonkTcTypeToType env arg
-       new_matches <- zonkMatchGroup env zonkLExpr matches
-       return (HsLamCase new_arg new_matches)
+zonkExpr env (HsLamCase matches)
+  = do new_matches <- zonkMatchGroup env zonkLExpr matches
+       return (HsLamCase new_matches)
 
 zonkExpr env (HsApp e1 e2)
   = do new_e1 <- zonkLExpr env e1
        new_e2 <- zonkLExpr env e2
        return (HsApp new_e1 new_e2)
 
+zonkExpr env (HsAppTypeOut e t)
+  = do new_e <- zonkLExpr env e
+       return (HsAppTypeOut new_e t)
+       -- NB: the type is an HsType; can't zonk that!
+
 zonkExpr _ e@(HsRnBracketOut _ _)
   = pprPanic "zonkExpr: HsRnBracketOut" (ppr e)
 
@@ -633,8 +669,8 @@ zonkExpr env (OpApp e1 op fixity e2)
        return (OpApp new_e1 new_op fixity new_e2)
 
 zonkExpr env (NegApp expr op)
-  = do new_expr <- zonkLExpr env expr
-       new_op <- zonkExpr env op
+  = do (env', new_op) <- zonkSyntaxExpr env op
+       new_expr <- zonkLExpr env' expr
        return (NegApp new_expr new_op)
 
 zonkExpr env (HsPar e)
@@ -660,17 +696,28 @@ zonkExpr env (ExplicitTuple tup_args boxed)
     zonk_tup_arg (L l (Missing t)) = do { t' <- zonkTcTypeToType env t
                                         ; return (L l (Missing t')) }
 
+zonkExpr env (ExplicitSum alt arity expr args)
+  = do new_args <- mapM (zonkTcTypeToType env) args
+       new_expr <- zonkLExpr env expr
+       return (ExplicitSum alt arity new_expr new_args)
+
 zonkExpr env (HsCase expr ms)
   = do new_expr <- zonkLExpr env expr
        new_ms <- zonkMatchGroup env zonkLExpr ms
        return (HsCase new_expr new_ms)
 
-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
-       ; return (HsIf new_e0 new_e1 new_e2 new_e3) }
+zonkExpr env (HsIf Nothing e1 e2 e3)
+  = do new_e1 <- zonkLExpr env e1
+       new_e2 <- zonkLExpr env e2
+       new_e3 <- zonkLExpr env e3
+       return (HsIf Nothing new_e1 new_e2 new_e3)
+
+zonkExpr env (HsIf (Just fun) e1 e2 e3)
+  = do (env1, new_fun) <- zonkSyntaxExpr env fun
+       new_e1 <- zonkLExpr env1 e1
+       new_e2 <- zonkLExpr env1 e2
+       new_e3 <- zonkLExpr env1 e3
+       return (HsIf (Just new_fun) new_e1 new_e2 new_e3)
 
 zonkExpr env (HsMultiIf ty alts)
   = do { alts' <- mapM (wrapLocM zonk_alt) alts
@@ -681,56 +728,58 @@ zonkExpr env (HsMultiIf ty alts)
                ; expr'          <- zonkLExpr env' expr
                ; return $ GRHS guard' expr' }
 
-zonkExpr env (HsLet binds expr)
+zonkExpr env (HsLet (L l binds) expr)
   = do (new_env, new_binds) <- zonkLocalBinds env binds
        new_expr <- zonkLExpr new_env expr
-       return (HsLet new_binds new_expr)
+       return (HsLet (L l new_binds) new_expr)
 
-zonkExpr env (HsDo do_or_lc stmts ty)
+zonkExpr env (HsDo do_or_lc (L l stmts) ty)
   = do (_, new_stmts) <- zonkStmts env zonkLExpr stmts
        new_ty <- zonkTcTypeToType env ty
-       return (HsDo do_or_lc new_stmts new_ty)
+       return (HsDo do_or_lc (L l new_stmts) new_ty)
 
 zonkExpr env (ExplicitList ty wit exprs)
-  = do new_ty <- zonkTcTypeToType env ty
-       new_wit <- zonkWit env wit
-       new_exprs <- zonkLExprs env exprs
+  = do (env1, new_wit) <- zonkWit env wit
+       new_ty <- zonkTcTypeToType env1 ty
+       new_exprs <- zonkLExprs env1 exprs
        return (ExplicitList new_ty new_wit new_exprs)
-   where zonkWit _ Nothing = return Nothing
-         zonkWit env (Just fln) = do new_fln <- zonkExpr env fln
-                                     return (Just new_fln)
+   where zonkWit env Nothing    = return (env, Nothing)
+         zonkWit env (Just fln) = second Just <$> zonkSyntaxExpr env fln
 
 zonkExpr env (ExplicitPArr ty exprs)
   = do new_ty <- zonkTcTypeToType env ty
        new_exprs <- zonkLExprs env exprs
        return (ExplicitPArr new_ty new_exprs)
 
-zonkExpr env (RecordCon data_con con_expr rbinds)
+zonkExpr env expr@(RecordCon { rcon_con_expr = con_expr, rcon_flds = rbinds })
   = do  { new_con_expr <- zonkExpr env con_expr
         ; new_rbinds   <- zonkRecFields env rbinds
-        ; return (RecordCon data_con new_con_expr new_rbinds) }
+        ; return (expr { rcon_con_expr = new_con_expr
+                       , rcon_flds = new_rbinds }) }
 
-zonkExpr env (RecordUpd expr rbinds cons in_tys out_tys)
+zonkExpr env (RecordUpd { rupd_expr = expr, rupd_flds = rbinds
+                        , rupd_cons = cons, rupd_in_tys = in_tys
+                        , rupd_out_tys = out_tys, rupd_wrap = req_wrap })
   = do  { new_expr    <- zonkLExpr env expr
         ; new_in_tys  <- mapM (zonkTcTypeToType env) in_tys
         ; new_out_tys <- mapM (zonkTcTypeToType env) out_tys
-        ; new_rbinds  <- zonkRecFields env rbinds
-        ; return (RecordUpd new_expr new_rbinds cons new_in_tys new_out_tys) }
+        ; new_rbinds  <- zonkRecUpdFields env rbinds
+        ; (_, new_recwrap) <- zonkCoFn env req_wrap
+        ; return (RecordUpd { rupd_expr = new_expr, rupd_flds =  new_rbinds
+                            , rupd_cons = cons, rupd_in_tys = new_in_tys
+                            , rupd_out_tys = new_out_tys, rupd_wrap = new_recwrap }) }
 
 zonkExpr env (ExprWithTySigOut e ty)
   = do { e' <- zonkLExpr env e
        ; return (ExprWithTySigOut e' ty) }
 
-zonkExpr _ (ExprWithTySig _ _ _) = panic "zonkExpr env:ExprWithTySig"
-
 zonkExpr env (ArithSeq expr wit info)
-  = do new_expr <- zonkExpr env expr
-       new_wit <- zonkWit env wit
-       new_info <- zonkArithSeq env info
+  = do (env1, new_wit) <- zonkWit env wit
+       new_expr <- zonkExpr env expr
+       new_info <- zonkArithSeq env1 info
        return (ArithSeq new_expr new_wit new_info)
-   where zonkWit _ Nothing = return Nothing
-         zonkWit env (Just fln) = do new_fln <- zonkExpr env fln
-                                     return (Just new_fln)
+   where zonkWit env Nothing    = return (env, Nothing)
+         zonkWit env (Just fln) = second Just <$> zonkSyntaxExpr env fln
 
 zonkExpr env (PArrSeq expr info)
   = do new_expr <- zonkExpr env expr
@@ -741,9 +790,9 @@ zonkExpr env (HsSCC src lbl expr)
   = do new_expr <- zonkLExpr env expr
        return (HsSCC src lbl new_expr)
 
-zonkExpr env (HsTickPragma src info expr)
+zonkExpr env (HsTickPragma src info srcInfo expr)
   = do new_expr <- zonkLExpr env expr
-       return (HsTickPragma src info new_expr)
+       return (HsTickPragma src info srcInfo new_expr)
 
 -- hdaume: core annotations
 zonkExpr env (HsCoreAnn src lbl expr)
@@ -757,30 +806,63 @@ zonkExpr env (HsProc pat body)
         ; return (HsProc new_pat new_body) }
 
 -- StaticPointers extension
-zonkExpr env (HsStatic expr)
-  = HsStatic <$> zonkLExpr env expr
+zonkExpr env (HsStatic fvs expr)
+  = HsStatic fvs <$> zonkLExpr env expr
 
 zonkExpr env (HsWrap co_fn expr)
   = do (env1, new_co_fn) <- zonkCoFn env co_fn
        new_expr <- zonkExpr env1 expr
        return (HsWrap new_co_fn new_expr)
 
-zonkExpr _ (HsUnboundVar v)
-  = return (HsUnboundVar v)
+zonkExpr _ e@(HsUnboundVar {}) = return e
 
 zonkExpr _ expr = pprPanic "zonkExpr" (ppr expr)
 
 -------------------------------------------------------------------------
+{-
+Note [Skolems in zonkSyntaxExpr]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider rebindable syntax with something like
+
+  (>>=) :: (forall x. blah) -> (forall y. blah') -> blah''
+
+The x and y become skolems that are in scope when type-checking the
+arguments to the bind. This means that we must extend the ZonkEnv with
+these skolems when zonking the arguments to the bind. But the skolems
+are different between the two arguments, and so we should theoretically
+carry around different environments to use for the different arguments.
+
+However, this becomes a logistical nightmare, especially in dealing with
+the more exotic Stmt forms. So, we simplify by making the critical
+assumption that the uniques of the skolems are different. (This assumption
+is justified by the use of newUnique in TcMType.instSkolTyCoVarX.)
+Now, we can safely just extend one environment.
+-}
+
+-- See Note [Skolems in zonkSyntaxExpr]
+zonkSyntaxExpr :: ZonkEnv -> SyntaxExpr TcId
+               -> TcM (ZonkEnv, SyntaxExpr Id)
+zonkSyntaxExpr env (SyntaxExpr { syn_expr      = expr
+                               , syn_arg_wraps = arg_wraps
+                               , syn_res_wrap  = res_wrap })
+  = do { (env0, res_wrap')  <- zonkCoFn env res_wrap
+       ; expr'              <- zonkExpr env0 expr
+       ; (env1, arg_wraps') <- mapAccumLM zonkCoFn env0 arg_wraps
+       ; return (env1, SyntaxExpr { syn_expr      = expr'
+                                  , syn_arg_wraps = arg_wraps'
+                                  , syn_res_wrap  = res_wrap' }) }
+
+-------------------------------------------------------------------------
 
 zonkLCmd  :: ZonkEnv -> LHsCmd TcId   -> TcM (LHsCmd Id)
 zonkCmd   :: ZonkEnv -> HsCmd TcId    -> TcM (HsCmd Id)
 
 zonkLCmd  env cmd  = wrapLocM (zonkCmd env) cmd
 
-zonkCmd env (HsCmdCast co cmd)
-  = do { co' <- zonkTcCoToCo env co
-       ; cmd' <- zonkCmd env cmd
-       ; return (HsCmdCast co' cmd') }
+zonkCmd env (HsCmdWrap w cmd)
+  = do { (env1, w') <- zonkCoFn env w
+       ; cmd' <- zonkCmd env1 cmd
+       ; return (HsCmdWrap w' cmd') }
 zonkCmd env (HsCmdArrApp e1 e2 ty ho rl)
   = do new_e1 <- zonkLExpr env e1
        new_e2 <- zonkLExpr env e2
@@ -811,21 +893,24 @@ zonkCmd env (HsCmdCase expr ms)
        return (HsCmdCase new_expr new_ms)
 
 zonkCmd env (HsCmdIf eCond ePred cThen cElse)
-  = do { new_eCond <- fmapMaybeM (zonkExpr env) eCond
-       ; new_ePred <- zonkLExpr env ePred
-       ; new_cThen <- zonkLCmd env cThen
-       ; new_cElse <- zonkLCmd env cElse
+  = do { (env1, new_eCond) <- zonkWit env eCond
+       ; new_ePred <- zonkLExpr env1 ePred
+       ; new_cThen <- zonkLCmd env1 cThen
+       ; new_cElse <- zonkLCmd env1 cElse
        ; return (HsCmdIf new_eCond new_ePred new_cThen new_cElse) }
+  where
+    zonkWit env Nothing  = return (env, Nothing)
+    zonkWit env (Just w) = second Just <$> zonkSyntaxExpr env w
 
-zonkCmd env (HsCmdLet binds cmd)
+zonkCmd env (HsCmdLet (L l binds) cmd)
   = do (new_env, new_binds) <- zonkLocalBinds env binds
        new_cmd <- zonkLCmd new_env cmd
-       return (HsCmdLet new_binds new_cmd)
+       return (HsCmdLet (L l new_binds) new_cmd)
 
-zonkCmd env (HsCmdDo stmts ty)
+zonkCmd env (HsCmdDo (L l stmts) ty)
   = do (_, new_stmts) <- zonkStmts env zonkLCmd stmts
        new_ty <- zonkTcTypeToType env ty
-       return (HsCmdDo new_stmts new_ty)
+       return (HsCmdDo (L l new_stmts) new_ty)
 
 
 
@@ -848,12 +933,11 @@ zonkCoFn env WpHole   = return (env, WpHole)
 zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
                                     ; (env2, c2') <- zonkCoFn env1 c2
                                     ; return (env2, WpCompose c1' c2') }
-zonkCoFn env (WpFun c1 c2 t1 t2) = do { (env1, c1') <- zonkCoFn env c1
-                                      ; (env2, c2') <- zonkCoFn env1 c2
-                                      ; t1'         <- zonkTcTypeToType env2 t1
-                                      ; t2'         <- zonkTcTypeToType env2 t2
-                                      ; return (env2, WpFun c1' c2' t1' t2') }
-zonkCoFn env (WpCast co) = do { co' <- zonkTcCoToCo env co
+zonkCoFn env (WpFun c1 c2 t1) = do { (env1, c1') <- zonkCoFn env c1
+                                   ; (env2, c2') <- zonkCoFn env1 c2
+                                   ; t1'         <- zonkTcTypeToType env2 t1
+                                   ; return (env2, WpFun c1' c2' t1') }
+zonkCoFn env (WpCast co) = do { co' <- zonkCoToCo env co
                               ; return (env, WpCast co') }
 zonkCoFn env (WpEvLam ev)   = do { (env', ev') <- zonkEvBndrX env ev
                                  ; return (env', WpEvLam ev') }
@@ -910,84 +994,138 @@ zonkStmts env zBody (s:ss) = do { (env1, s')  <- wrapLocSndM (zonkStmt env zBody
 zonkStmt :: ZonkEnv
          -> (ZonkEnv -> Located (body TcId) -> TcM (Located (body Id)))
          -> Stmt TcId (Located (body TcId)) -> TcM (ZonkEnv, Stmt Id (Located (body Id)))
-zonkStmt env _ (ParStmt stmts_w_bndrs mzip_op bind_op)
-  = do { new_stmts_w_bndrs <- mapM zonk_branch stmts_w_bndrs
+zonkStmt env _ (ParStmt stmts_w_bndrs mzip_op bind_op bind_ty)
+  = do { (env1, new_bind_op) <- zonkSyntaxExpr env bind_op
+       ; new_bind_ty <- zonkTcTypeToType env1 bind_ty
+       ; new_stmts_w_bndrs <- mapM (zonk_branch env1) stmts_w_bndrs
        ; let new_binders = [b | ParStmtBlock _ bs _ <- new_stmts_w_bndrs, b <- bs]
-             env1 = extendIdZonkEnv env new_binders
-       ; new_mzip <- zonkExpr env1 mzip_op
-       ; new_bind <- zonkExpr env1 bind_op
-       ; return (env1, ParStmt new_stmts_w_bndrs new_mzip new_bind) }
+             env2 = extendIdZonkEnvRec env1 new_binders
+       ; new_mzip <- zonkExpr env2 mzip_op
+       ; return (env2, ParStmt new_stmts_w_bndrs new_mzip new_bind_op new_bind_ty) }
   where
-    zonk_branch (ParStmtBlock stmts bndrs return_op)
-       = do { (env1, new_stmts) <- zonkStmts env zonkLExpr stmts
-            ; new_return <- zonkExpr env1 return_op
-            ; return (ParStmtBlock new_stmts (zonkIdOccs env1 bndrs) new_return) }
+    zonk_branch env1 (ParStmtBlock stmts bndrs return_op)
+       = do { (env2, new_stmts)  <- zonkStmts env1 zonkLExpr stmts
+            ; (env3, new_return) <- zonkSyntaxExpr env2 return_op
+            ; return (ParStmtBlock new_stmts (zonkIdOccs env3 bndrs) new_return) }
 
 zonkStmt env zBody (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_ret_fn = ret_id, recS_mfix_fn = mfix_id
+                            , recS_bind_fn = bind_id, recS_bind_ty = bind_ty
                             , 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 zBody segStmts
+  = do { (env1, new_bind_id) <- zonkSyntaxExpr env bind_id
+       ; (env2, new_mfix_id) <- zonkSyntaxExpr env1 mfix_id
+       ; (env3, new_ret_id)  <- zonkSyntaxExpr env2 ret_id
+       ; new_bind_ty <- zonkTcTypeToType env3 bind_ty
+       ; new_rvs <- zonkIdBndrs env3 rvs
+       ; new_lvs <- zonkIdBndrs env3 lvs
+       ; new_ret_ty  <- zonkTcTypeToType env3 ret_ty
+       ; let env4 = extendIdZonkEnvRec env3 new_rvs
+       ; (env5, new_segStmts) <- zonkStmts env4 zBody segStmts
         -- Zonk the ret-expressions in an envt that
         -- has the polymorphic bindings in the envt
-       ; 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
+       ; new_later_rets <- mapM (zonkExpr env5) later_rets
+       ; new_rec_rets <- mapM (zonkExpr env5) rec_rets
+       ; return (extendIdZonkEnvRec env3 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_bind_ty = new_bind_ty
                          , recS_later_rets = new_later_rets
                          , recS_rec_rets = new_rec_rets, recS_ret_ty = new_ret_ty }) }
 
 zonkStmt env zBody (BodyStmt body then_op guard_op ty)
-  = do new_body <- zBody env body
-       new_then <- zonkExpr env then_op
-       new_guard <- zonkExpr env guard_op
-       new_ty <- zonkTcTypeToType env ty
-       return (env, BodyStmt new_body new_then new_guard new_ty)
+  = do (env1, new_then_op)  <- zonkSyntaxExpr env then_op
+       (env2, new_guard_op) <- zonkSyntaxExpr env1 guard_op
+       new_body <- zBody env2 body
+       new_ty   <- zonkTcTypeToType env2 ty
+       return (env2, BodyStmt new_body new_then_op new_guard_op new_ty)
 
-zonkStmt env zBody (LastStmt body ret_op)
-  = do new_body <- zBody env body
-       new_ret <- zonkExpr env ret_op
-       return (env, LastStmt new_body new_ret)
+zonkStmt env zBody (LastStmt body noret ret_op)
+  = do (env1, new_ret) <- zonkSyntaxExpr env ret_op
+       new_body <- zBody env1 body
+       return (env, LastStmt new_body noret 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 zonkLExpr stmts
-    ; binderMap' <- mapM (zonkBinderMapEntry env') binderMap
-    ; 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_bind_arg_ty = bind_arg_ty
+                          , trS_fmap = liftM_op })
+  = do {
+    ; (env1, bind_op') <- zonkSyntaxExpr env bind_op
+    ; bind_arg_ty' <- zonkTcTypeToType env1 bind_arg_ty
+    ; (env2, stmts') <- zonkStmts env1 zonkLExpr stmts
+    ; by'        <- fmapMaybeM (zonkLExpr env2) by
+    ; using'     <- zonkLExpr env2 using
+
+    ; (env3, return_op') <- zonkSyntaxExpr env2 return_op
+    ; binderMap' <- mapM (zonkBinderMapEntry env3) binderMap
+    ; liftM_op'  <- zonkExpr env3 liftM_op
+    ; let env3' = extendIdZonkEnvRec env3 (map snd binderMap')
+    ; return (env3', 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' }) }
+                               , trS_ret = return_op', trS_bind = bind_op'
+                               , trS_bind_arg_ty = bind_arg_ty'
+                               , trS_fmap = liftM_op' }) }
   where
-    zonkBinderMapEntry env (oldBinder, newBinder) = do
+    zonkBinderMapEntry env  (oldBinder, newBinder) = do
         let oldBinder' = zonkIdOcc env oldBinder
         newBinder' <- zonkIdBndr env newBinder
         return (oldBinder', newBinder')
 
-zonkStmt env _ (LetStmt binds)
+zonkStmt env _ (LetStmt (L l binds))
   = do (env1, new_binds) <- zonkLocalBinds env binds
-       return (env1, LetStmt new_binds)
-
-zonkStmt env zBody (BindStmt pat body bind_op fail_op)
-  = do  { new_body <- zBody env body
-        ; (env1, new_pat) <- zonkPat env pat
-        ; new_bind <- zonkExpr env bind_op
-        ; new_fail <- zonkExpr env fail_op
-        ; return (env1, BindStmt new_pat new_body new_bind new_fail) }
+       return (env1, LetStmt (L l new_binds))
+
+zonkStmt env zBody (BindStmt pat body bind_op fail_op bind_ty)
+  = do  { (env1, new_bind) <- zonkSyntaxExpr env bind_op
+        ; new_bind_ty <- zonkTcTypeToType env1 bind_ty
+        ; new_body <- zBody env1 body
+        ; (env2, new_pat) <- zonkPat env1 pat
+        ; (_, new_fail) <- zonkSyntaxExpr env1 fail_op
+        ; return (env2, BindStmt new_pat new_body new_bind new_fail new_bind_ty) }
+
+-- Scopes: join > ops (in reverse order) > pats (in forward order)
+--              > rest of stmts
+zonkStmt env _zBody (ApplicativeStmt args mb_join body_ty)
+  = do  { (env1, new_mb_join)   <- zonk_join env mb_join
+        ; (env2, new_args)      <- zonk_args env1 args
+        ; new_body_ty           <- zonkTcTypeToType env2 body_ty
+        ; return (env2, ApplicativeStmt new_args new_mb_join new_body_ty) }
+  where
+    zonk_join env Nothing  = return (env, Nothing)
+    zonk_join env (Just j) = second Just <$> zonkSyntaxExpr env j
+
+    get_pat (_, ApplicativeArgOne pat _)    = pat
+    get_pat (_, ApplicativeArgMany _ _ pat) = pat
+
+    replace_pat pat (op, ApplicativeArgOne _ a)
+      = (op, ApplicativeArgOne pat a)
+    replace_pat pat (op, ApplicativeArgMany a b _)
+      = (op, ApplicativeArgMany a b pat)
+
+    zonk_args env args
+      = do { (env1, new_args_rev) <- zonk_args_rev env (reverse args)
+           ; (env2, new_pats)     <- zonkPats env1 (map get_pat args)
+           ; return (env2, zipWith replace_pat new_pats (reverse new_args_rev)) }
+
+     -- these need to go backward, because if any operators are higher-rank,
+     -- later operators may introduce skolems that are in scope for earlier
+     -- arguments
+    zonk_args_rev env ((op, arg) : args)
+      = do { (env1, new_op)         <- zonkSyntaxExpr env op
+           ; new_arg                <- zonk_arg env1 arg
+           ; (env2, new_args)       <- zonk_args_rev env1 args
+           ; return (env2, (new_op, new_arg) : new_args) }
+    zonk_args_rev env [] = return (env, [])
+
+    zonk_arg env (ApplicativeArgOne pat expr)
+      = do { new_expr <- zonkLExpr env expr
+           ; return (ApplicativeArgOne pat new_expr) }
+    zonk_arg env (ApplicativeArgMany stmts ret pat)
+      = do { (env1, new_stmts) <- zonkStmts env zonkLExpr stmts
+           ; new_ret           <- zonkExpr env1 ret
+           ; return (ApplicativeArgMany new_stmts new_ret pat) }
 
 -------------------------------------------------------------------------
 zonkRecFields :: ZonkEnv -> HsRecordBinds TcId -> TcM (HsRecordBinds TcId)
@@ -996,9 +1134,18 @@ zonkRecFields env (HsRecFields flds dd)
         ; return (HsRecFields flds' dd) }
   where
     zonk_rbind (L l fld)
-      = do { new_id   <- wrapLocM (zonkIdBndr env) (hsRecFieldId fld)
+      = do { new_id   <- wrapLocM (zonkFieldOcc env) (hsRecFieldLbl fld)
            ; new_expr <- zonkLExpr env (hsRecFieldArg fld)
-           ; return (L l (fld { hsRecFieldId = new_id
+           ; return (L l (fld { hsRecFieldLbl = new_id
+                              , hsRecFieldArg = new_expr })) }
+
+zonkRecUpdFields :: ZonkEnv -> [LHsRecUpdField TcId] -> TcM [LHsRecUpdField TcId]
+zonkRecUpdFields env = mapM zonk_rbind
+  where
+    zonk_rbind (L l fld)
+      = do { new_id   <- wrapLocM (zonkFieldOcc env) (hsRecUpdFieldOcc fld)
+           ; new_expr <- zonkLExpr env (hsRecFieldArg fld)
+           ; return (L l (fld { hsRecFieldLbl = fmap ambiguousFieldOcc new_id
                               , hsRecFieldArg = new_expr })) }
 
 -------------------------------------------------------------------------
@@ -1029,11 +1176,13 @@ zonk_pat env (ParPat p)
 
 zonk_pat env (WildPat ty)
   = do  { ty' <- zonkTcTypeToType env ty
+        ; ensureNotRepresentationPolymorphic ty'
+            (text "In a wildcard pattern")
         ; return (env, WildPat ty') }
 
-zonk_pat env (VarPat v)
+zonk_pat env (VarPat (L l v))
   = do  { v' <- zonkIdBndr env v
-        ; return (extendIdZonkEnv1 env v', VarPat v') }
+        ; return (extendIdZonkEnv1 env v', VarPat (L l v')) }
 
 zonk_pat env (LazyPat pat)
   = do  { (env', pat') <- zonkPat env pat
@@ -1060,11 +1209,11 @@ zonk_pat env (ListPat pats ty Nothing)
         ; return (env', ListPat pats' ty' Nothing) }
 
 zonk_pat env (ListPat pats ty (Just (ty2,wit)))
-  = do  { wit' <- zonkExpr env wit
-        ; ty2' <- zonkTcTypeToType env ty2
-        ; ty' <- zonkTcTypeToType env ty
-        ; (env', pats') <- zonkPats env pats
-        ; return (env', ListPat pats' ty' (Just (ty2',wit'))) }
+  = do  { (env', wit') <- zonkSyntaxExpr env wit
+        ; ty2' <- zonkTcTypeToType env' ty2
+        ; ty' <- zonkTcTypeToType env' ty
+        ; (env'', pats') <- zonkPats env' pats
+        ; return (env'', ListPat pats' ty' (Just (ty2',wit'))) }
 
 zonk_pat env (PArrPat pats ty)
   = do  { ty' <- zonkTcTypeToType env ty
@@ -1076,6 +1225,11 @@ zonk_pat env (TuplePat pats boxed tys)
         ; (env', pats') <- zonkPats env pats
         ; return (env', TuplePat pats' boxed tys') }
 
+zonk_pat env (SumPat pat alt arity tys)
+  = do  { tys' <- mapM (zonkTcTypeToType env) tys
+        ; (env', pat') <- zonkPat env pat
+        ; return (env', SumPat pat' alt arity tys') }
+
 zonk_pat env p@(ConPatOut { pat_arg_tys = tys, pat_tvs = tyvars
                           , pat_dicts = evs, pat_binds = binds
                           , pat_args = args, pat_wrap = wrapper })
@@ -1103,19 +1257,25 @@ zonk_pat env (SigPatOut pat ty)
         ; (env', pat') <- zonkPat env pat
         ; return (env', SigPatOut pat' ty') }
 
-zonk_pat env (NPat (L l lit) mb_neg eq_expr)
-  = do  { lit' <- zonkOverLit env lit
-        ; mb_neg' <- fmapMaybeM (zonkExpr env) mb_neg
-        ; eq_expr' <- zonkExpr env eq_expr
-        ; return (env, NPat (L l lit') mb_neg' eq_expr') }
-
-zonk_pat env (NPlusKPat (L loc n) (L l lit) e1 e2)
-  = do  { n' <- zonkIdBndr env n
-        ; lit' <- zonkOverLit env lit
-        ; e1' <- zonkExpr env e1
-        ; e2' <- zonkExpr env e2
-        ; return (extendIdZonkEnv1 env n',
-                  NPlusKPat (L loc n') (L l lit') e1' e2') }
+zonk_pat env (NPat (L l lit) mb_neg eq_expr ty)
+  = do  { (env1, eq_expr') <- zonkSyntaxExpr env eq_expr
+        ; (env2, mb_neg') <- case mb_neg of
+            Nothing -> return (env1, Nothing)
+            Just n  -> second Just <$> zonkSyntaxExpr env1 n
+
+        ; lit' <- zonkOverLit env2 lit
+        ; ty' <- zonkTcTypeToType env2 ty
+        ; return (env2, NPat (L l lit') mb_neg' eq_expr' ty') }
+
+zonk_pat env (NPlusKPat (L loc n) (L l lit1) lit2 e1 e2 ty)
+  = do  { (env1, e1') <- zonkSyntaxExpr env  e1
+        ; (env2, e2') <- zonkSyntaxExpr env1 e2
+        ; n' <- zonkIdBndr env2 n
+        ; lit1' <- zonkOverLit env2 lit1
+        ; lit2' <- zonkOverLit env2 lit2
+        ; ty' <- zonkTcTypeToType env2 ty
+        ; return (extendIdZonkEnv1 env2 n',
+                  NPlusKPat (L loc n') (L l lit1') lit2' e1' e2' ty') }
 
 zonk_pat env (CoPat co_fn pat ty)
   = do { (env', co_fn') <- zonkCoFn env co_fn
@@ -1165,8 +1325,10 @@ zonkForeignExports :: ZonkEnv -> [LForeignDecl TcId] -> TcM [LForeignDecl Id]
 zonkForeignExports env ls = mapM (wrapLocM (zonkForeignExport env)) ls
 
 zonkForeignExport :: ZonkEnv -> ForeignDecl TcId -> TcM (ForeignDecl Id)
-zonkForeignExport env (ForeignExport i _hs_ty co spec) =
-   return (ForeignExport (fmap (zonkIdOcc env) i) undefined co spec)
+zonkForeignExport env (ForeignExport { fd_name = i, fd_co = co, fd_fe = spec })
+  = return (ForeignExport { fd_name = fmap (zonkIdOcc env) i
+                          , fd_sig_ty = undefined, fd_co = co
+                          , fd_fe = spec })
 zonkForeignExport _ for_imp
   = return for_imp     -- Foreign imports don't need zonking
 
@@ -1175,24 +1337,15 @@ zonkRules env rs = mapM (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)
-  = do { unbound_tkv_set <- newMutVar emptyVarSet
-       ; let env_rule = setZonkType env (zonkTvCollecting unbound_tkv_set)
-              -- See Note [Zonking the LHS of a RULE]
+  = do { (env_inside, new_bndrs) <- mapAccumLM zonk_bndr env vars
 
-       ; (env_inside, new_bndrs) <- mapAccumLM zonk_bndr env_rule vars
+       ; let env_lhs = setZonkType env_inside zonkTvSkolemising
+              -- See Note [Zonking the LHS of a RULE]
 
-       ; new_lhs <- zonkLExpr env_inside lhs
+       ; new_lhs <- zonkLExpr env_lhs    lhs
        ; new_rhs <- zonkLExpr env_inside rhs
 
-       ; unbound_tkvs <- readMutVar unbound_tkv_set
-
-       ; let final_bndrs :: [LRuleBndr Var]
-             final_bndrs = map (noLoc . RuleBndr . noLoc)
-                               (varSetElemsKvsFirst unbound_tkvs)
-                           ++ new_bndrs
-
-       ; return $
-         HsRule name act final_bndrs new_lhs fv_lhs new_rhs fv_rhs }
+       ; return (HsRule name act new_bndrs new_lhs fv_lhs new_rhs fv_rhs) }
   where
    zonk_bndr env (L l (RuleBndr (L loc v)))
       = do { (env', v') <- zonk_it env v
@@ -1201,7 +1354,7 @@ zonkRule env (HsRule name act (vars{-::[RuleBndr TcId]-}) lhs fv_lhs rhs fv_rhs)
 
    zonk_it env v
      | isId v     = do { v' <- zonkIdBndr env v
-                       ; return (extendIdZonkEnv1 env v', v') }
+                       ; return (extendIdZonkEnvRec env [v'], v') }
      | otherwise  = ASSERT( isImmutableTyVar v)
                     zonkTyBndrX env v
                     -- DV: used to be return (env,v) but that is plain
@@ -1241,47 +1394,46 @@ zonkVect _ (HsVectInstIn _) = panic "TcHsSyn.zonkVect: HsVectInstIn"
 
 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' <- zonkTcCoToCo env co
+                                    zonkEvVarOcc env v
+zonkEvTerm env (EvCoercion co)    = do { co' <- zonkCoToCo env co
                                        ; return (EvCoercion co') }
 zonkEvTerm env (EvCast tm co)     = do { tm' <- zonkEvTerm env tm
-                                       ; co' <- zonkTcCoToCo env co
+                                       ; co' <- zonkCoToCo env co
                                        ; return (mkEvCast tm' co') }
-zonkEvTerm env (EvTupleMk tms)    = return (EvTupleMk (zonkIdOccs env tms))
 zonkEvTerm _   (EvLit l)          = return (EvLit l)
 
-zonkEvTerm env (EvTypeable ev) =
-  fmap EvTypeable $
-  case ev of
-    EvTypeableTyCon tc ks    -> return (EvTypeableTyCon tc ks)
-    EvTypeableTyApp t1 t2    -> do e1 <- zonk t1
-                                   e2 <- zonk t2
-                                   return (EvTypeableTyApp e1 e2)
-    EvTypeableTyLit t        -> EvTypeableTyLit `fmap` zonkTcTypeToType env t
-  where
-  zonk (ev,t) = do ev' <- zonkEvTerm env ev
-                   t'  <- zonkTcTypeToType env t
-                   return (ev',t')
-
+zonkEvTerm env (EvTypeable ty ev) =
+  do { ev' <- zonkEvTypeable env ev
+     ; ty' <- zonkTcTypeToType env ty
+     ; return (EvTypeable ty' ev') }
 zonkEvTerm env (EvCallStack cs)
   = case cs of
       EvCsEmpty -> return (EvCallStack cs)
-      EvCsTop n l tm -> do { tm' <- zonkEvTerm env tm
-                           ; return (EvCallStack (EvCsTop n l tm')) }
       EvCsPushCall n l tm -> do { tm' <- zonkEvTerm env tm
                                 ; return (EvCallStack (EvCsPushCall n l tm')) }
 
-zonkEvTerm env (EvTupleSel tm n)  = do { tm' <- zonkEvTerm env tm
-                                       ; return (EvTupleSel tm' n) }
 zonkEvTerm env (EvSuperClass d n) = do { d' <- zonkEvTerm env d
                                        ; return (EvSuperClass d' n) }
 zonkEvTerm env (EvDFunApp df tys tms)
   = do { tys' <- zonkTcTypeToTypes env tys
-       ; return (EvDFunApp (zonkIdOcc env df) tys' (zonkIdOccs env tms)) }
+       ; tms' <- mapM (zonkEvTerm env) tms
+       ; return (EvDFunApp (zonkIdOcc env df) tys' tms') }
 zonkEvTerm env (EvDelayedError ty msg)
   = do { ty' <- zonkTcTypeToType env ty
        ; return (EvDelayedError ty' msg) }
 
+zonkEvTypeable :: ZonkEnv -> EvTypeable -> TcM EvTypeable
+zonkEvTypeable env (EvTypeableTyCon ts)
+  = do { ts' <- mapM (zonkEvTerm env) ts
+       ; return $ EvTypeableTyCon ts' }
+zonkEvTypeable env (EvTypeableTyApp t1 t2)
+  = do { t1' <- zonkEvTerm env t1
+       ; t2' <- zonkEvTerm env t2
+       ; return (EvTypeableTyApp t1' t2') }
+zonkEvTypeable env (EvTypeableTyLit t1)
+  = do { t1' <- zonkEvTerm env t1
+       ; return (EvTypeableTyLit t1') }
+
 zonkTcEvBinds_s :: ZonkEnv -> [TcEvBinds] -> TcM (ZonkEnv, [TcEvBinds])
 zonkTcEvBinds_s env bs = do { (env, bs') <- mapAccumLM zonk_tc_ev_binds env bs
                             ; return (env, [EvBinds (unionManyBags bs')]) }
@@ -1295,14 +1447,15 @@ zonk_tc_ev_binds env (TcEvBinds var) = zonkEvBindsVar env var
 zonk_tc_ev_binds env (EvBinds bs)    = zonkEvBinds env bs
 
 zonkEvBindsVar :: ZonkEnv -> EvBindsVar -> TcM (ZonkEnv, Bag EvBind)
-zonkEvBindsVar env (EvBindsVar ref _) = do { bs <- readMutVar ref
-                                           ; zonkEvBinds env (evBindMapBinds bs) }
+zonkEvBindsVar env (EvBindsVar { ebv_binds = 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)
+         { let env1 = extendIdZonkEnvRec env (collect_ev_bndrs new_binds)
          ; binds' <- mapBagM (zonkEvBind env1) binds
          ; return (env1, binds') })
   where
@@ -1311,18 +1464,19 @@ zonkEvBinds env binds
     add (EvBind { eb_lhs = var }) vars = var : vars
 
 zonkEvBind :: ZonkEnv -> EvBind -> TcM EvBind
-zonkEvBind env (EvBind { eb_lhs = var, eb_rhs = term, eb_is_given = is_given })
+zonkEvBind env bind@(EvBind { eb_lhs = var, eb_rhs = term })
   = do { var'  <- {-# SCC "zonkEvBndr" #-} zonkEvBndr env var
 
          -- Optimise the common case of Refl coercions
          -- See Note [Optimise coercion zonking]
          -- This has a very big effect on some programs (eg Trac #5030)
+
        ; term' <- case getEqPredTys_maybe (idType var') of
            Just (r, ty1, ty2) | ty1 `eqType` ty2
                   -> return (EvCoercion (mkTcReflCo r ty1))
            _other -> zonkEvTerm env term
 
-      ; return (EvBind { eb_lhs = var', eb_rhs = term', eb_is_given = is_given }) }
+       ; return (bind { eb_lhs = var', eb_rhs = term' }) }
 
 {-
 ************************************************************************
@@ -1331,31 +1485,6 @@ zonkEvBind env (EvBind { eb_lhs = var, eb_rhs = term, eb_is_given = is_given })
 *                                                                      *
 ************************************************************************
 
-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
@@ -1371,13 +1500,11 @@ 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
+The type of Phantom is (forall (k : *). 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).
+(forall (k : Any *). forall (a : Any (Any *)). Int).
 
-Note [Optimise coercion zonkind]
+Note [Optimise coercion zonking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When optimising evidence binds we may come across situations where
 a coercion looks like
@@ -1391,6 +1518,7 @@ use Refl on the right, ignoring the actual coercion on the RHS.
 
 This can have a very big effect, because the constraint solver sometimes does go
 to a lot of effort to prove Refl!  (Eg when solving  10+3 = 10+3; cf Trac #5030)
+
 -}
 
 zonkTyVarOcc :: ZonkEnv -> TyVar -> TcM TcType
@@ -1416,129 +1544,233 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
   where
     lookup_in_env    -- Look up in the env just as we do for Ids
       = case lookupVarEnv tv_env tv of
-          Nothing  -> return (mkTyVarTy tv)
+          Nothing  -> mkTyVarTy <$> updateTyVarKindM (zonkTcTypeToType env) tv
           Just tv' -> return (mkTyVarTy tv')
 
+zonkCoVarOcc :: ZonkEnv -> CoVar -> TcM Coercion
+zonkCoVarOcc env@(ZonkEnv _ tyco_env _) cv
+  | Just cv' <- lookupVarEnv tyco_env cv  -- don't look in the knot-tied env
+  = return $ mkCoVarCo cv'
+  | otherwise
+  = mkCoVarCo <$> updateVarTypeM (zonkTcTypeToType env) cv
+
+zonkCoHole :: ZonkEnv -> CoercionHole
+           -> Role -> Type -> Type  -- these are all redundant with
+                                    -- the details in the hole,
+                                    -- unzonked
+           -> TcM Coercion
+zonkCoHole env h r t1 t2
+  = do { contents <- unpackCoercionHole_maybe h
+       ; case contents of
+           Just co -> do { co <- zonkCoToCo env co
+                         ; checkCoercionHole co h r t1 t2 }
+
+              -- This next case should happen only in the presence of
+              -- (undeferred) type errors. Originally, I put in a panic
+              -- here, but that caused too many uses of `failIfErrsM`.
+           Nothing -> do { traceTc "Zonking unfilled coercion hole" (ppr h)
+                         ; when debugIsOn $
+                           whenNoErrs $
+                           MASSERT2( False
+                                   , text "Type-correct unfilled coercion hole"
+                                     <+> ppr h )
+                         ; t1 <- zonkTcTypeToType env t1
+                         ; t2 <- zonkTcTypeToType env t2
+                         ; return $ mkHoleCo h r t1 t2 } }
+
+zonk_tycomapper :: TyCoMapper ZonkEnv TcM
+zonk_tycomapper = TyCoMapper
+  { tcm_smart = True   -- Establish type invariants
+                       -- See Note [Type-checking inside the knot] in TcHsType
+  , tcm_tyvar = zonkTyVarOcc
+  , tcm_covar = zonkCoVarOcc
+  , tcm_hole  = zonkCoHole
+  , tcm_tybinder = \env tv _vis -> zonkTyBndrX env tv }
+
+-- Confused by zonking? See Note [What is zonking?] in TcMType.
 zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
-zonkTcTypeToType env ty
-  = go ty
-  where
-    go (TyConApp tc tys) = do tys' <- mapM go tys
-                              return (mkTyConApp tc tys')
-                -- Establish Type invariants
-                -- See Note [Zonking inside the knot] in TcHsType
-
-    go (LitTy n)         = return (LitTy n)
-
-    go (FunTy arg res)   = do arg' <- go arg
-                              res' <- go res
-                              return (FunTy arg' res')
-
-    go (AppTy fun arg)   = do fun' <- go fun
-                              arg' <- go arg
-                              return (mkAppTy fun' arg')
-                -- NB the mkAppTy; we might have instantiated a
-                -- type variable to a type constructor, so we need
-                -- to pull the TyConApp to the top.
-
-        -- The two interesting cases!
-    go (TyVarTy tv) = zonkTyVarOcc env tv
-
-    go (ForAllTy tv ty) = ASSERT( isImmutableTyVar tv )
-                          do { (env', tv') <- zonkTyBndrX env tv
-                             ; ty' <- zonkTcTypeToType env' ty
-                             ; return (ForAllTy tv' ty') }
+zonkTcTypeToType = mapType zonk_tycomapper
 
 zonkTcTypeToTypes :: ZonkEnv -> [TcType] -> TcM [Type]
 zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
 
 zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion
-zonkCoToCo env co
-  = go co
+zonkCoToCo = mapCoercion zonk_tycomapper
+
+zonkSigType :: TcType -> TcM Type
+-- Zonk the type obtained from a user type signature
+-- We want to turn any quantified (forall'd) variables into TyVars
+-- but we may find some free TcTyVars, and we want to leave them
+-- completely alone.  They may even have unification variables inside
+-- e.g.  f (x::a) = ...(e :: a -> a)....
+-- The type sig for 'e' mentions a free 'a' which will be a
+-- unification SigTv variable.
+zonkSigType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_tv)
   where
-    go (Refl r ty)               = mkReflCo r <$> zonkTcTypeToType env ty
-    go (TyConAppCo r tc args)    = mkTyConAppCo r tc <$> mapM go args
-    go (AppCo co arg)            = mkAppCo <$> go co <*> go arg
-    go (AxiomInstCo ax ind args) = AxiomInstCo ax ind <$> mapM go args
-    go (UnivCo s r ty1 ty2)      = mkUnivCo s r <$> zonkTcTypeToType env ty1
-                                                <*> zonkTcTypeToType env ty2
-    go (SymCo co)                = mkSymCo <$> go co
-    go (TransCo co1 co2)         = mkTransCo <$> go co1 <*> go co2
-    go (NthCo n co)              = mkNthCo n <$> go co
-    go (LRCo lr co)              = mkLRCo lr <$> go co
-    go (InstCo co arg)           = mkInstCo <$> go co <*> zonkTcTypeToType env arg
-    go (SubCo co)                = mkSubCo <$> go co
-    go (AxiomRuleCo ax ts cs)    = AxiomRuleCo ax <$> mapM (zonkTcTypeToType env) ts
-                                                  <*> mapM go cs
-
-    -- The two interesting cases!
-    go (CoVarCo cv)              = return (mkCoVarCo $ zonkIdOcc env cv)
-    go (ForAllCo tv co)          = ASSERT( isImmutableTyVar tv )
-                                   do { (env', tv') <- zonkTyBndrX env tv
-                                      ; co' <- zonkCoToCo env' co
-                                      ; return (mkForAllCo tv' co') }
-                                   
-zonkTvCollecting :: TcRef TyVarSet -> UnboundTyVarZonker
--- This variant collects unbound type variables in a mutable variable
--- Works on both types and kinds
-zonkTvCollecting unbound_tv_set tv
-  = do { poly_kinds <- xoptM Opt_PolyKinds
-       ; if isKindVar 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') } }
+    zonk_unbound_tv :: UnboundTyVarZonker
+    zonk_unbound_tv tv = return (mkTyVarTy tv)
+
+zonkTvSkolemising :: UnboundTyVarZonker
+-- This variant is used for the LHS of rules
+-- See Note [Zonking the LHS of a RULE].
+zonkTvSkolemising tv
+  = do { tv' <- skolemiseUnboundMetaTyVar 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
+-- It zaps unbound type variables to Any, except for RuntimeRep
+-- vars which it zonks to PtrRepLIfted
 -- Works on both types and kinds
 zonkTypeZapping tv
-  = do { let ty = if isKindVar tv
-                  -- ty is actually a kind, zonk to AnyK
-                  then anyKind
-                  else anyTypeOfKind (defaultKind (tyVarKind tv))
+  = do { let ty | isRuntimeRepVar tv = ptrRepLiftedTy
+                | otherwise          = anyTypeOfKind (tyVarKind tv)
        ; writeMetaTyVar tv ty
        ; return ty }
 
+---------------------------------------
+{- Note [Zonking the LHS of a RULE]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also DsBinds Note [Free tyvars on rule LHS]
+
+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 alpha (C alpha)) and we do
+not want to zap the unbound meta-tyvar 'alpha' to Any, because that
+limits the applicability of the rule.  Instead, we want to quantify
+over it!
+
+We do this in two stages.
+
+* During zonking, we skolemise 'alpha' to 'a'.  We do this by using
+  zonkTvSkolemising as the UnboundTyVarZonker in the ZonkEnv.
+  (This is the whole reason that the ZonkEnv has a UnboundTyVarZonker.)
+
+* In DsBinds, we quantify over it.  See DsBinds
+  Note [Free tyvars on rule LHS]
+
+Quantifying here is awkward 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)
+
+Note [Unboxed tuples in representation polymorphism check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Recall that all types that have values (that is, lifted and unlifted
+types) have kinds that look like (TYPE rep), where (rep :: RuntimeRep)
+tells how the values are represented at runtime. Lifted types have
+kind (TYPE PtrRepLifted) (for which * is just a synonym) and, say,
+Int# has kind (TYPE IntRep).
+
+It would be terrible if the code generator came upon a binder of a type
+whose kind is something like TYPE r, where r is a skolem type variable.
+The code generator wouldn't know what to do. So we eliminate that case
+here.
+
+Although representation polymorphism and the RuntimeRep type catch
+most ways of abusing unlifted types, it still isn't quite satisfactory
+around unboxed tuples. That's because all unboxed tuple types have kind
+TYPE UnboxedTupleRep, which is clearly a lie: it doesn't actually tell
+you what the representation is.
+
+Naively, when checking for representation polymorphism, you might think we can
+just look for free variables in a type's RuntimeRep. But this misses the
+UnboxedTupleRep case.
+
+So, instead, we handle unboxed tuples specially. Only after unboxed tuples
+are handled do we look for free tyvars in a RuntimeRep.
+
+We must still be careful in the UnboxedTupleRep case. A binder whose type
+has kind UnboxedTupleRep is OK -- only as long as the type is really an
+unboxed tuple, which the code generator treats specially. So we do this:
+ 1. Check if the type is an unboxed tuple. If so, recur.
+ 2. Check if the kind is TYPE UnboxedTupleRep. If so, error.
+ 3. Check if the kind has any free variables. If so, error.
 
-zonkTcCoToCo :: 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
-zonkTcCoToCo env co
-  = go co
+In case 1, we have a type that looks like
+
+  (# , #) PtrRepLifted IntRep Bool Int#
+
+recalling that
+
+  (# , #) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep).
+             TYPE r1 -> TYPE r2 -> TYPE UnboxedTupleRep
+
+It's tempting just to look at the RuntimeRep arguments to make sure
+that they are devoid of free variables and not UnboxedTupleRep. This
+naive check, though, fails on nested unboxed tuples, like
+(# Int#, (# Bool, Void# #) #). Thus, instead of looking at the RuntimeRep
+args to the unboxed tuple constructor, we look at the types themselves.
+
+Here are a few examples:
+
+   type family F r :: TYPE r
+
+   x :: (F r :: TYPE r)   -- REJECTED: simple representation polymorphism
+     where r is an in-scope type variable of kind RuntimeRep
+
+   x :: (F PtrRepLifted :: TYPE PtrRepLifted)   -- OK
+   x :: (F IntRep       :: TYPE IntRep)         -- OK
+
+   x :: (F UnboxedTupleRep :: TYPE UnboxedTupleRep)  -- REJECTED
+
+   x :: ((# Int, Bool #) :: TYPE UnboxedTupleRep)    -- OK
+-}
+
+-- | According to the rules around representation polymorphism
+-- (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder
+-- can have a representation-polymorphic type. This check ensures
+-- that we respect this rule. It is a bit regrettable that this error
+-- occurs in zonking, after which we should have reported all errors.
+-- But it's hard to see where else to do it, because this can be discovered
+-- only after all solving is done. And, perhaps most importantly, this
+-- isn't really a compositional property of a type system, so it's
+-- not a terrible surprise that the check has to go in an awkward spot.
+ensureNotRepresentationPolymorphic
+  :: Type  -- its zonked type
+  -> SDoc  -- where this happened
+  -> TcM ()
+ensureNotRepresentationPolymorphic ty doc
+  = whenNoErrs $   -- sometimes we end up zonking bogus definitions of type
+                   -- forall a. a. See, for example, test ghci/scripts/T9140
+    checkForRepresentationPolymorphism doc ty
+
+   -- See Note [Unboxed tuples in representation polymorphism check]
+checkForRepresentationPolymorphism :: SDoc -> Type -> TcM ()
+checkForRepresentationPolymorphism extra ty
+  | Just (tc, tys) <- splitTyConApp_maybe ty
+  , isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc
+  = mapM_ (checkForRepresentationPolymorphism extra) (dropRuntimeRepArgs tys)
+
+  | tuple_rep || sum_rep
+  = addErr (vcat [ text "The type" <+> quotes (ppr tidy_ty) <+>
+                     (text "is not an unboxed" <+> tuple_or_sum <> comma)
+                 , text "and yet its kind suggests that it has the representation"
+                 , text "of an unboxed" <+> tuple_or_sum <> text ". This is not allowed." ] $$
+            extra)
+
+  | not (isEmptyVarSet (tyCoVarsOfType runtime_rep))
+  = addErr $
+    hang (text "A representation-polymorphic type is not allowed here:")
+       2 (vcat [ text "Type:" <+> ppr tidy_ty
+               , text "Kind:" <+> ppr tidy_ki ]) $$
+    extra
+
+  | otherwise
+  = return ()
   where
-    go (TcLetCo bs co)        = do { (env', bs') <- zonkTcEvBinds env bs
-                                   ; co' <- zonkTcCoToCo env' co
-                                   ; return (TcLetCo bs' co') }
-    go (TcCoVarCo cv)         = return (mkTcCoVarCo (zonkEvVarOcc env cv))
-    go (TcRefl r ty)          = do { ty' <- zonkTcTypeToType env ty
-                                   ; return (TcRefl r ty') }
-    go (TcTyConAppCo r tc cos)
-                              = do { cos' <- mapM go cos; return (mkTcTyConAppCo r tc cos') }
-    go (TcAxiomInstCo ax ind cos)
-                              = do { cos' <- mapM go cos; return (TcAxiomInstCo ax ind cos') }
-    go (TcAppCo co1 co2)      = do { co1' <- go co1; co2' <- go co2
-                                   ; return (mkTcAppCo co1' co2') }
-    go (TcCastCo co1 co2)     = do { co1' <- go co1; co2' <- go co2
-                                   ; return (TcCastCo co1' co2') }
-    go (TcPhantomCo ty1 ty2)  = do { ty1' <- zonkTcTypeToType env ty1
-                                   ; ty2' <- zonkTcTypeToType env ty2
-                                   ; return (TcPhantomCo ty1' ty2') }
-    go (TcSymCo co)           = do { co' <- go co; return (mkTcSymCo co') }
-    go (TcNthCo n co)         = do { co' <- go co; return (mkTcNthCo n co') }
-    go (TcLRCo lr co)         = do { co' <- go co; return (mkTcLRCo lr 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 (TcSubCo co)           = do { co' <- go co; return (mkTcSubCo co') }
-    go (TcAxiomRuleCo co ts cs) = do { ts' <- zonkTcTypeToTypes env ts
-                                     ; cs' <- mapM go cs
-                                     ; return (TcAxiomRuleCo co ts' cs')
-                                     }
-    go (TcCoercion co)        = do { co' <- zonkCoToCo env co
-                                   ; return (TcCoercion co') }
+    tuple_rep    = runtime_rep `eqType` unboxedTupleRepDataConTy
+    sum_rep      = runtime_rep `eqType` unboxedSumRepDataConTy
+    tuple_or_sum = text (if tuple_rep then "tuple" else "sum")
+
+    ki          = typeKind ty
+    runtime_rep = getRuntimeRepFromKind "check_type" ki
+
+    (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
+    tidy_ki             = tidyType tidy_env (typeKind ty)