Warn about unused type variables in type families
[ghc.git] / compiler / rename / RnTypes.hs
index 346d764..ebcab85 100644 (file)
@@ -4,27 +4,31 @@
 \section[RnSource]{Main pass of renamer}
 -}
 
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE CPP #-}
 
 module RnTypes (
         -- Type related stuff
         rnHsType, rnLHsType, rnLHsTypes, rnContext,
         rnHsKind, rnLHsKind, rnLHsMaybeKind,
-        rnHsSigType, rnLHsInstType, rnConDeclFields,
-        newTyVarNameRn, rnLHsTypeWithWildCards,
-        rnHsSigTypeWithWildCards, collectWildCards,
+        rnHsSigType, rnHsWcType,
+        rnHsSigWcType, rnHsSigWcTypeScoped,
+        rnLHsInstType,
+        newTyVarNameRn, collectAnonWildCards,
+        rnConDeclFields,
+        rnLTyVar,
 
         -- Precence related stuff
         mkOpAppRn, mkNegAppRn, mkOpFormRn, mkConOpPatRn,
         checkPrecMatch, checkSectionPrec,
 
         -- Binding related stuff
-        warnContextQuantification, warnUnusedForAlls,
-        bindSigTyVarsFV, bindHsTyVars, rnHsBndrSig,
+        warnUnusedForAlls, bindLHsTyVarBndr,
+        bindSigTyVarsFV, bindHsQTyVars, bindLRdrNames,
         extractHsTyRdrTyVars, extractHsTysRdrTyVars,
+        extractHsTysRdrTyVarsDups, rmDupsInRdrTyVars,
         extractRdrKindSigVars, extractDataDefnKindVars,
-        filterInScope
+        freeKiTyVarsAllVars, freeKiTyVarsKindVars, freeKiTyVarsTypeVars
   ) where
 
 import {-# SOURCE #-} RnSplice( rnSpliceType )
@@ -37,9 +41,11 @@ import TcRnMonad
 import RdrName
 import PrelNames
 import TysPrim          ( funTyConName )
+import TysWiredIn       ( starKindTyConName, unicodeStarKindTyConName )
 import Name
 import SrcLoc
 import NameSet
+import FieldLabel
 
 import Util
 import BasicTypes       ( compareFixity, funTyFixity, negateFixity,
@@ -47,7 +53,9 @@ import BasicTypes       ( compareFixity, funTyFixity, negateFixity,
 import Outputable
 import FastString
 import Maybes
-import Data.List        ( nub, nubBy, deleteFirstsBy )
+import qualified GHC.LanguageExtensions as LangExt
+
+import Data.List        ( (\\), nubBy, partition )
 import Control.Monad    ( unless, when )
 
 #if __GLASGOW_HASKELL__ < 709
@@ -61,32 +69,235 @@ These type renamers are in a separate module, rather than in (say) RnSource,
 to break several loop.
 
 *********************************************************
-*                                                      *
-\subsection{Renaming types}
-*                                                      *
+*                                                       *
+           HsSigWcType (i.e with wildcards)
+*                                                       *
 *********************************************************
 -}
 
-rnHsSigType :: SDoc -> LHsType RdrName -> RnM (LHsType Name, FreeVars)
-        -- rnHsSigType is used for source-language type signatures,
-        -- which use *implicit* universal quantification.
-rnHsSigType doc_str ty = rnLHsType (TypeSigCtx doc_str) ty
+rnHsSigWcType :: HsDocContext -> LHsSigWcType RdrName
+            -> RnM (LHsSigWcType Name, FreeVars)
+rnHsSigWcType doc sig_ty
+  = rn_hs_sig_wc_type True doc sig_ty $ \sig_ty' ->
+    return (sig_ty', emptyFVs)
+
+rnHsSigWcTypeScoped :: HsDocContext -> LHsSigWcType RdrName
+                    -> (LHsSigWcType Name -> RnM (a, FreeVars))
+                    -> RnM (a, FreeVars)
+-- Used for
+--   - Signatures on binders in a RULE
+--   - Pattern type signatures
+-- Wildcards are allowed
+rnHsSigWcTypeScoped ctx sig_ty thing_inside
+  = rn_hs_sig_wc_type False ctx sig_ty thing_inside
+    -- False: for pattern type sigs and rules we /do/ want
+    --        to bring those type varibles into scope
+    -- e.g  \ (x :: forall a. a-> b) -> e
+    -- Here we do bring 'b' into scope
+
+rn_hs_sig_wc_type :: Bool   -- see rnImplicitBndrs
+                  -> HsDocContext
+                  -> LHsSigWcType RdrName
+                  -> (LHsSigWcType Name -> RnM (a, FreeVars))
+                  -> RnM (a, FreeVars)
+-- rn_hs_sig_wc_type is used for source-language type signatures
+rn_hs_sig_wc_type no_implicit_if_forall ctxt
+                  (HsIB { hsib_body = wc_ty }) thing_inside
+  = do { let hs_ty = hswc_body wc_ty
+       ; free_vars <- extract_filtered_rdr_ty_vars hs_ty
+       ; (free_vars', nwc_rdrs) <- partition_nwcs free_vars
+       ; rnImplicitBndrs no_implicit_if_forall free_vars' hs_ty $ \ vars ->
+    do { rn_hs_wc_type ctxt wc_ty nwc_rdrs $ \ wc_ty' ->
+         thing_inside (HsIB { hsib_vars = vars
+                            , hsib_body = wc_ty' }) } }
+
+rnHsWcType :: HsDocContext -> LHsWcType RdrName -> RnM (LHsWcType Name, FreeVars)
+rnHsWcType ctxt wc_ty@(HsWC { hswc_body = hs_ty })
+  = do { free_vars <- extract_filtered_rdr_ty_vars hs_ty
+       ; (_, nwc_rdrs) <- partition_nwcs free_vars
+       ; rn_hs_wc_type ctxt wc_ty nwc_rdrs $ \ wc_ty' ->
+         return (wc_ty', emptyFVs) }
+
+-- | Finds free type and kind variables in a type, without duplicates and
+-- variables that are already in LocalRdrEnv.
+extract_filtered_rdr_ty_vars :: LHsType RdrName -> RnM FreeKiTyVars
+extract_filtered_rdr_ty_vars hs_ty
+  = do { rdr_env <- getLocalRdrEnv
+       ; filterInScope rdr_env <$> extractHsTyRdrTyVars hs_ty }
+
+-- | When the NamedWildCards extension is enabled, removes type variables
+-- that start with an underscore from the FreeKiTyVars in the argument
+-- and returns them in a separate list.
+-- When the extension is disabled, the function returns the argument and
+-- empty list.
+-- See Note [Renaming named wild cards]
+partition_nwcs :: FreeKiTyVars -> RnM (FreeKiTyVars, [Located RdrName])
+partition_nwcs free_vars@(FKTV { fktv_tys = tys, fktv_all = all })
+  = do { wildcards_enabled <- fmap (xopt LangExt.NamedWildCards) getDynFlags
+       ; let (nwcs, no_nwcs) =
+                if wildcards_enabled
+                then partition (startsWithUnderscore . rdrNameOcc . unLoc) tys
+                else ([], tys)
+             free_vars' = free_vars { fktv_tys = no_nwcs
+                                    , fktv_all = all \\ nwcs }
+       ; return (free_vars', nwcs) }
+
+-- | Renames a type with wild card binders.
+-- Expects a list of names of type variables that should be replaced with
+-- named wild cards. (See Note [Renaming named wild cards])
+-- Although the parser does not create named wild cards, it is possible to find
+-- them in declaration splices, so the function tries to collect them.
+rn_hs_wc_type :: HsDocContext -> LHsWcType RdrName -> [Located RdrName]
+              -> (LHsWcType Name -> RnM (a, FreeVars))
+              -> RnM (a, FreeVars)
+rn_hs_wc_type ctxt (HsWC { hswc_body = hs_ty }) nwc_rdrs thing_inside
+  = do { let nwc_collected = collectNamedWildCards hs_ty
+       -- the parser doesn't generate named wcs, but they may be in splices
+       ; rdr_env <- getLocalRdrEnv
+       ; nwcs <- sequence [ newLocalBndrRn lrdr
+                          | lrdr@(L _ rdr) <- nwc_collected ++ nwc_rdrs
+                          , not (inScope rdr_env rdr) ]
+       ; setLocalRdrEnv (extendLocalRdrEnvNwcs rdr_env nwcs) $
+         bindLocalNamesFV nwcs $
+    do { (wc_ty, fvs1) <- rnWcSigTy ctxt hs_ty
+       ; let wc_ty' :: HsWildCardBndrs Name (LHsType Name)
+             wc_ty' = wc_ty { hswc_wcs = nwcs ++ hswc_wcs wc_ty }
+       ; (res, fvs2) <- thing_inside wc_ty'
+       ; return (res, fvs1 `plusFV` fvs2) } }
 
-rnLHsInstType :: SDoc -> LHsType RdrName -> RnM (LHsType Name, FreeVars)
--- Rename the type in an instance or standalone deriving decl
-rnLHsInstType doc_str ty
-  = do { (ty', fvs) <- rnLHsType (GenericCtx doc_str) ty
-       ; unless good_inst_ty (addErrAt (getLoc ty) (badInstTy ty))
-       ; return (ty', fvs) }
+rnWcSigTy :: HsDocContext -> LHsType RdrName
+          -> RnM (LHsWcType Name, FreeVars)
+-- ^ Renames just the top level of a type signature
+-- It's exactly like rnHsTyKi, except that it uses rnWcSigContext
+-- on a qualified type, and return info on any extra-constraints
+-- wildcard.  Some code duplication, but no big deal.
+rnWcSigTy ctxt (L loc hs_ty@(HsForAllTy { hst_bndrs = tvs, hst_body = hs_tau }))
+  = bindLHsTyVarBndrs ctxt Nothing [] tvs $ \ _ tvs' ->
+    do { lcl_env <- getLocalRdrEnv
+       ; let explicitly_bound = fmap hsLTyVarName tvs'
+       ; setLocalRdrEnv (delLocalRdrEnvNwcs lcl_env explicitly_bound) $
+           -- See Note [Renaming named wild cards]
+    do { (hs_tau', fvs) <- rnWcSigTy ctxt hs_tau
+       ; warnUnusedForAlls (inTypeDoc hs_ty) tvs' fvs
+       ; let hs_ty' = HsForAllTy { hst_bndrs = tvs', hst_body = hswc_body hs_tau' }
+       ; return ( hs_tau' { hswc_body = L loc hs_ty' }, fvs) } }
+
+rnWcSigTy ctxt (L loc (HsQualTy { hst_ctxt = hs_ctxt, hst_body = tau }))
+  = do { (hs_ctxt', fvs1) <- rnWcSigContext ctxt hs_ctxt
+       ; (tau',     fvs2) <- rnLHsType ctxt tau
+       ; let awcs_tau = collectAnonWildCards tau'
+             hs_ty'   = HsQualTy { hst_ctxt = hswc_body hs_ctxt'
+                                 , hst_body = tau' }
+       ; return ( HsWC { hswc_wcs = hswc_wcs hs_ctxt' ++ awcs_tau
+                       , hswc_ctx = hswc_ctx hs_ctxt'
+                       , hswc_body = L loc hs_ty' }
+                , fvs1 `plusFV` fvs2) }
+
+rnWcSigTy ctxt hs_ty
+  = do { (hs_ty', fvs) <- rnLHsType ctxt hs_ty
+       ; return (HsWC { hswc_wcs = collectAnonWildCards hs_ty'
+                      , hswc_ctx = Nothing
+                      , hswc_body = hs_ty' }
+                , fvs) }
+
+rnWcSigContext :: HsDocContext -> LHsContext RdrName
+               -> RnM (HsWildCardBndrs Name (LHsContext Name), FreeVars)
+rnWcSigContext ctxt (L loc hs_ctxt)
+  = getLocalRdrEnv >>= rn_wc_sig_context
   where
-    good_inst_ty
-      | Just (_, _, L _ cls, _) <-
-                        splitLHsInstDeclTy_maybe (flattenTopLevelLHsForAllTy ty)
-      , isTcOcc (rdrNameOcc cls) = True
-      | otherwise                = False
-
-badInstTy :: LHsType RdrName -> SDoc
-badInstTy ty = ptext (sLit "Malformed instance:") <+> ppr ty
+    rn_wc_sig_context :: LocalRdrEnv
+                      -> RnM (HsWildCardBndrs Name (LHsContext Name), FreeVars)
+    rn_wc_sig_context lcl_env
+      | Just (hs_ctxt1, hs_ctxt_last) <- snocView hs_ctxt
+      , L lx (HsWildCardTy wc) <- (to_nwc lcl_env . ignoreParens) hs_ctxt_last
+      = do { (hs_ctxt1', fvs) <- mapFvRn rn_top_constraint hs_ctxt1
+           ; wc'              <- setSrcSpan lx $
+                                 rnExtraConstraintWildCard ctxt wc
+           ; let hs_ctxt' = hs_ctxt1' ++ [L lx (HsWildCardTy wc')]
+                 awcs     = concatMap collectAnonWildCards hs_ctxt1'
+                 -- NB: *not* including the extra-constraint wildcard
+           ; return ( HsWC { hswc_wcs = awcs
+                           , hswc_ctx = Just lx
+                           , hswc_body = L loc hs_ctxt' }
+                    , fvs ) }
+      | otherwise
+      = do { (hs_ctxt', fvs) <- mapFvRn rn_top_constraint hs_ctxt
+           ; return (HsWC { hswc_wcs = concatMap collectAnonWildCards hs_ctxt'
+                          , hswc_ctx = Nothing
+                          , hswc_body = L loc hs_ctxt' }, fvs) }
+
+    to_nwc :: LocalRdrEnv -> LHsType RdrName -> LHsType RdrName
+    to_nwc _  lnwc@(L _ (HsWildCardTy {})) = lnwc
+    to_nwc lcl_env (L loc (HsTyVar lname@(L _ rdr_name)))
+      | rdr_name `inLocalRdrEnvNwcsRdrName` lcl_env
+      = L loc (HsWildCardTy (NamedWildCard lname))
+    to_nwc _ lt = lt
+
+    rn_top_constraint = rnLHsTyKi RnTopConstraint ctxt
+
+
+{- ******************************************************
+*                                                       *
+           HsSigtype (i.e. no wildcards)
+*                                                       *
+****************************************************** -}
+
+rnHsSigType :: HsDocContext -> LHsSigType RdrName
+            -> RnM (LHsSigType Name, FreeVars)
+-- Used for source-language type signatures
+-- that cannot have wildcards
+rnHsSigType ctx (HsIB { hsib_body = hs_ty })
+  = do { vars <- extract_filtered_rdr_ty_vars hs_ty
+       ; rnImplicitBndrs True vars hs_ty $ \ vars ->
+    do { (body', fvs) <- rnLHsType ctx hs_ty
+       ; return (HsIB { hsib_vars = vars
+                      , hsib_body = body' }, fvs) } }
+
+rnImplicitBndrs :: Bool    -- True <=> no implicit quantification
+                           --          if type is headed by a forall
+                           -- E.g.  f :: forall a. a->b
+                           -- Do not quantify over 'b' too.
+                -> FreeKiTyVars
+                -> LHsType RdrName
+                -> ([Name] -> RnM (a, FreeVars))
+                -> RnM (a, FreeVars)
+rnImplicitBndrs no_implicit_if_forall free_vars hs_ty@(L loc _) thing_inside
+  = do { let real_tv_rdrs  -- Implicit quantification only if
+                           -- there is no explicit forall
+               | no_implicit_if_forall
+               , L _ (HsForAllTy {}) <- hs_ty = []
+               | otherwise                    = freeKiTyVarsTypeVars free_vars
+             real_rdrs = freeKiTyVarsKindVars free_vars ++ real_tv_rdrs
+       ; traceRn (text "rnSigType" <+> (ppr hs_ty $$ ppr free_vars $$
+                                        ppr real_rdrs))
+       ; vars <- mapM (newLocalBndrRn . L loc . unLoc) real_rdrs
+       ; bindLocalNamesFV vars $
+         thing_inside vars }
+
+rnLHsInstType :: SDoc -> LHsSigType RdrName -> RnM (LHsSigType Name, FreeVars)
+-- Rename the type in an instance or standalone deriving decl
+-- The 'doc_str' is "an instance declaration" or "a VECTORISE pragma"
+rnLHsInstType doc_str inst_ty
+  | Just cls <- getLHsInstDeclClass_maybe inst_ty
+  , isTcOcc (rdrNameOcc (unLoc cls))
+         -- The guards check that the instance type looks like
+         --   blah => C ty1 .. tyn
+  = do { let full_doc = doc_str <+> ptext (sLit "for") <+> quotes (ppr cls)
+       ; rnHsSigType (GenericCtx full_doc) inst_ty }
+
+  | otherwise  -- The instance is malformed, but we'd still like
+               -- to make progress rather than failing outright, so
+               -- we report more errors.  So we rename it anyway.
+  = do { addErrAt (getLoc (hsSigType inst_ty)) $
+         ptext (sLit "Malformed instance:") <+> ppr inst_ty
+       ; rnHsSigType (GenericCtx doc_str) inst_ty }
+
+
+{- ******************************************************
+*                                                       *
+           LHsType and HsType
+*                                                       *
+****************************************************** -}
 
 {-
 rnHsType is here because we call it from loadInstDecl, and I didn't
@@ -108,22 +319,78 @@ f :: forall a. a -> b         is an error
 f :: forall a. () => a -> b   is an error
 f :: forall a. a -> (() => b) binds "a" and "b"
 
-The -fwarn-context-quantification flag warns about
-this situation. See rnHsTyKi for case HsForAllTy Qualified.
+This situation is now considered to be an error. See rnHsTyKi for case
+HsForAllTy Qualified.
+
+Note [Dealing with *]
+~~~~~~~~~~~~~~~~~~~~~
+As a legacy from the days when types and kinds were different, we use
+the type * to mean what we now call GHC.Types.Type. The problem is that
+* should associate just like an identifier, *not* a symbol.
+Running example: the user has written
+
+  T (Int, Bool) b + c * d
+
+At this point, we have a bunch of stretches of types
+
+  [[T, (Int, Bool), b], [c], [d]]
+
+these are the [[LHsType Name]] and a bunch of operators
+
+  [GHC.TypeLits.+, GHC.Types.*]
+
+Note that the * is GHC.Types.*. So, we want to rearrange to have
+
+  [[T, (Int, Bool), b], [c, *, d]]
+
+and
+
+  [GHC.TypeLits.+]
+
+as our lists. We can then do normal fixity resolution on these. The fixities
+must come along for the ride just so that the list stays in sync with the
+operators.
+
+Note [Renaming named wild cards]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Identifiers starting with an underscore are always parsed as type variables.
+(Parser.y) When the NamedWildCards extension is enabled, the renamer replaces
+those variables with named wild cards.
+
+The NameSet lre_nwcs in LocalRdrEnv is used to keep the names of the type
+variables that should be replaced with named wild cards. The set is filled only
+in functions that return a LHsWcType and thus expect to find wild cards.
+In other functions, the set remains empty and the wild cards are not created.
+Because of this, the replacement does not occur in contexts where the wild
+cards are not expected, like data type declarations or type synonyms.
+(See the comments in Trac #10982)
+
+While renaming HsForAllTy (rnWcSigTy, rnHsTyKi), the explicitly bound names are
+removed from the lre_nwcs NameSet. As a result, they are not replaced in the
+quantifier body even if they start with an underscore. (Trac #11098) Eg
+
+    qux :: _a -> (forall _a . _a -> _a) -> _a
+
+The _a bound by forall is a tyvar, the _a outside the parens are wild cards.
 -}
 
-rnLHsTyKi  :: Bool --  True <=> renaming a type, False <=> a kind
+rnLHsTyKi  :: RnTyKiWhat
            -> HsDocContext -> LHsType RdrName -> RnM (LHsType Name, FreeVars)
-rnLHsTyKi isType doc (L loc ty)
+rnLHsTyKi what doc (L loc ty)
   = setSrcSpan loc $
-    do { (ty', fvs) <- rnHsTyKi isType doc ty
+    do { (ty', fvs) <- rnHsTyKi what doc ty
        ; return (L loc ty', fvs) }
 
 rnLHsType  :: HsDocContext -> LHsType RdrName -> RnM (LHsType Name, FreeVars)
-rnLHsType = rnLHsTyKi True
+rnLHsType cxt ty = -- pprTrace "rnHsType" (pprHsDocContext cxt $$ ppr ty) $
+                   rnLHsTyKi (RnTypeBody TypeLevel) cxt ty
+
+rnLHsPred  :: RnTyKiWhat -> HsDocContext -> LHsType RdrName -> RnM (LHsType Name, FreeVars)
+rnLHsPred (RnTypeBody level) = rnLHsTyKi (RnConstraint level)
+rnLHsPred what               = rnLHsTyKi what
 
 rnLHsKind  :: HsDocContext -> LHsKind RdrName -> RnM (LHsKind Name, FreeVars)
-rnLHsKind = rnLHsTyKi False
+rnLHsKind = rnLHsTyKi (RnTypeBody KindLevel)
 
 rnLHsMaybeKind  :: HsDocContext -> Maybe (LHsKind RdrName)
                 -> RnM (Maybe (LHsKind Name), FreeVars)
@@ -134,270 +401,401 @@ rnLHsMaybeKind doc (Just kind)
        ; return (Just kind', fvs) }
 
 rnHsType  :: HsDocContext -> HsType RdrName -> RnM (HsType Name, FreeVars)
-rnHsType = rnHsTyKi True
+rnHsType cxt ty = rnHsTyKi (RnTypeBody TypeLevel) cxt ty
+
 rnHsKind  :: HsDocContext -> HsKind RdrName -> RnM (HsKind Name, FreeVars)
-rnHsKind = rnHsTyKi False
-
-rnHsTyKi :: Bool -> HsDocContext -> HsType RdrName -> RnM (HsType Name, FreeVars)
-
-rnHsTyKi isType doc ty@HsForAllTy{}
-  = rnHsTyKiForAll isType doc (flattenTopLevelHsForAllTy ty)
-
-rnHsTyKi isType _ (HsTyVar rdr_name)
-  = do { name <- rnTyVar isType rdr_name
-       ; return (HsTyVar name, unitFV name) }
-
--- If we see (forall a . ty), without foralls on, the forall will give
--- a sensible error message, but we don't want to complain about the dot too
--- Hence the jiggery pokery with ty1
-rnHsTyKi isType doc ty@(HsOpTy ty1 (wrapper, L loc op) ty2)
-  = ASSERT( isType ) setSrcSpan loc $
-    do  { ops_ok <- xoptM Opt_TypeOperators
-        ; op' <- if ops_ok
-                 then rnTyVar isType op
-                 else do { addErr (opTyErr op ty)
-                         ; return (mkUnboundName op) }  -- Avoid double complaint
-        ; let l_op' = L loc op'
-        ; fix <- lookupTyFixityRn l_op'
-        ; (ty1', fvs1) <- rnLHsType doc ty1
-        ; (ty2', fvs2) <- rnLHsType doc ty2
-        ; res_ty <- mkHsOpTyRn (\t1 t2 -> HsOpTy t1 (wrapper, l_op') t2)
-                               op' fix ty1' ty2'
-        ; return (res_ty, (fvs1 `plusFV` fvs2) `addOneFV` op') }
-
-rnHsTyKi isType doc (HsParTy ty)
-  = do { (ty', fvs) <- rnLHsTyKi isType doc ty
+rnHsKind = rnHsTyKi (RnTypeBody KindLevel)
+
+data RnTyKiWhat = RnTypeBody TypeOrKind
+                | RnTopConstraint           -- Top-level context of HsSigWcTypes
+                | RnConstraint TypeOrKind   -- All other constraints
+
+instance Outputable RnTyKiWhat where
+  ppr (RnTypeBody lev)   = text "RnTypeBody" <+> ppr lev
+  ppr RnTopConstraint    = text "RnTopConstraint"
+  ppr (RnConstraint lev) = text "RnConstraint" <+> ppr lev
+
+isRnKindLevel :: RnTyKiWhat -> Bool
+isRnKindLevel (RnTypeBody KindLevel)   = True
+isRnKindLevel (RnConstraint KindLevel) = True
+isRnKindLevel _                        = False
+
+rnHsTyKi :: RnTyKiWhat -> HsDocContext -> HsType RdrName -> RnM (HsType Name, FreeVars)
+
+rnHsTyKi what doc ty@(HsForAllTy { hst_bndrs = tyvars, hst_body  = tau })
+  = do { checkTypeInType what ty
+       ; bindLHsTyVarBndrs doc Nothing [] tyvars $ \ _ tyvars' ->
+    do { lcl_env <- getLocalRdrEnv
+       ; let explicitly_bound = fmap hsLTyVarName tyvars'
+       ; setLocalRdrEnv (delLocalRdrEnvNwcs lcl_env explicitly_bound) $
+           -- See Note [Renaming named wild cards]
+    do { (tau',  fvs) <- rnLHsTyKi what doc tau
+       ; warnUnusedForAlls (inTypeDoc ty) tyvars' fvs
+       ; return ( HsForAllTy { hst_bndrs = tyvars', hst_body =  tau' }
+                , fvs) } } }
+
+rnHsTyKi what doc ty@(HsQualTy { hst_ctxt = lctxt
+                               , hst_body = tau })
+  = do { checkTypeInType what ty
+       ; (ctxt', fvs1) <- rnTyKiContext what doc lctxt
+       ; (tau',  fvs2) <- rnLHsTyKi what doc tau
+       ; return (HsQualTy { hst_ctxt = ctxt', hst_body =  tau' }
+                , fvs1 `plusFV` fvs2) }
+
+rnHsTyKi what doc (HsTyVar lname@(L loc rdr_name))
+  = do { lcl_env <- getLocalRdrEnv
+           -- See Note [Renaming named wild cards]
+       ; if rdr_name `inLocalRdrEnvNwcsRdrName` lcl_env
+         then rnHsTyKi what doc (HsWildCardTy (NamedWildCard lname))
+         else do { name <- rnTyVar what rdr_name
+                 ; return (HsTyVar (L loc name), unitFV name) } }
+
+rnHsTyKi what doc ty@(HsOpTy ty1 l_op ty2)
+  = setSrcSpan (getLoc l_op) $
+    do  { (l_op', fvs1) <- rnHsTyOp what ty l_op
+        ; fix   <- lookupTyFixityRn l_op'
+        ; (ty1', fvs2) <- rnLHsTyKi what doc ty1
+        ; (ty2', fvs3) <- rnLHsTyKi what doc ty2
+        ; res_ty <- mkHsOpTyRn (\t1 t2 -> HsOpTy t1 l_op' t2)
+                               (unLoc l_op') fix ty1' ty2'
+        ; return (res_ty, plusFVs [fvs1, fvs2, fvs3]) }
+
+rnHsTyKi what doc (HsParTy ty)
+  = do { (ty', fvs) <- rnLHsTyKi what doc ty
        ; return (HsParTy ty', fvs) }
 
-rnHsTyKi isType doc (HsBangTy b ty)
-  = ASSERT( isType )
-    do { (ty', fvs) <- rnLHsType doc ty
+rnHsTyKi _ doc (HsBangTy b ty)
+  = do { (ty', fvs) <- rnLHsType doc ty
        ; return (HsBangTy b ty', fvs) }
 
+rnHsTyKi _ doc@(ConDeclCtx names) (HsRecTy flds)
+  = do {
+       -- AZ:reviewers: is there a monadic version of concatMap?
+         flss <- mapM (lookupConstructorFields . unLoc) names
+       ; let fls = concat flss
+       ; (flds', fvs) <- rnConDeclFields fls doc flds
+       ; return (HsRecTy flds', fvs) }
+
 rnHsTyKi _ doc ty@(HsRecTy flds)
   = do { addErr (hang (ptext (sLit "Record syntax is illegal here:"))
                     2 (ppr ty))
-       ; (flds', fvs) <- rnConDeclFields doc flds
+       ; (flds', fvs) <- rnConDeclFields [] doc flds
        ; return (HsRecTy flds', fvs) }
 
-rnHsTyKi isType doc (HsFunTy ty1 ty2)
-  = do { (ty1', fvs1) <- rnLHsTyKi isType doc ty1
+rnHsTyKi what doc (HsFunTy ty1 ty2)
+  = do { (ty1', fvs1) <- rnLHsTyKi what doc ty1
         -- Might find a for-all as the arg of a function type
-       ; (ty2', fvs2) <- rnLHsTyKi isType doc ty2
+       ; (ty2', fvs2) <- rnLHsTyKi what doc ty2
         -- Or as the result.  This happens when reading Prelude.hi
         -- when we find return :: forall m. Monad m -> forall a. a -> m a
 
         -- Check for fixity rearrangements
-       ; res_ty <- if isType
-                   then mkHsOpTyRn HsFunTy funTyConName funTyFixity ty1' ty2'
-                   else return (HsFunTy ty1' ty2')
+       ; res_ty <- mkHsOpTyRn HsFunTy funTyConName funTyFixity ty1' ty2'
        ; return (res_ty, fvs1 `plusFV` fvs2) }
 
-rnHsTyKi isType doc listTy@(HsListTy ty)
-  = do { data_kinds <- xoptM Opt_DataKinds
-       ; unless (data_kinds || isType) (addErr (dataKindsErr isType listTy))
-       ; (ty', fvs) <- rnLHsTyKi isType doc ty
+rnHsTyKi what doc listTy@(HsListTy ty)
+  = do { data_kinds <- xoptM LangExt.DataKinds
+       ; when (not data_kinds && isRnKindLevel what)
+              (addErr (dataKindsErr what listTy))
+       ; (ty', fvs) <- rnLHsTyKi what doc ty
        ; return (HsListTy ty', fvs) }
 
-rnHsTyKi isType doc (HsKindSig ty k)
-  = ASSERT( isType )
-    do { kind_sigs_ok <- xoptM Opt_KindSignatures
-       ; unless kind_sigs_ok (badSigErr False doc ty)
-       ; (ty', fvs1) <- rnLHsType doc ty
+rnHsTyKi what doc t@(HsKindSig ty k)
+  = do { checkTypeInType what t
+       ; kind_sigs_ok <- xoptM LangExt.KindSignatures
+       ; unless kind_sigs_ok (badKindSigErr doc ty)
+       ; (ty', fvs1) <- rnLHsTyKi what doc ty
        ; (k', fvs2) <- rnLHsKind doc k
        ; return (HsKindSig ty' k', fvs1 `plusFV` fvs2) }
 
-rnHsTyKi isType doc (HsPArrTy ty)
-  = ASSERT( isType )
-    do { (ty', fvs) <- rnLHsType doc ty
+rnHsTyKi what doc t@(HsPArrTy ty)
+  = do { notInKinds what t
+       ; (ty', fvs) <- rnLHsType doc ty
        ; return (HsPArrTy ty', fvs) }
 
 -- Unboxed tuples are allowed to have poly-typed arguments.  These
 -- sometimes crop up as a result of CPR worker-wrappering dictionaries.
-rnHsTyKi isType doc tupleTy@(HsTupleTy tup_con tys)
-  = do { data_kinds <- xoptM Opt_DataKinds
-       ; unless (data_kinds || isType) (addErr (dataKindsErr isType tupleTy))
-       ; (tys', fvs) <- mapFvRn (rnLHsTyKi isType doc) tys
+rnHsTyKi what doc tupleTy@(HsTupleTy tup_con tys)
+  = do { data_kinds <- xoptM LangExt.DataKinds
+       ; when (not data_kinds && isRnKindLevel what)
+              (addErr (dataKindsErr what tupleTy))
+       ; (tys', fvs) <- mapFvRn (rnLHsTyKi what doc) tys
        ; return (HsTupleTy tup_con tys', fvs) }
 
 -- Ensure that a type-level integer is nonnegative (#8306, #8412)
-rnHsTyKi isType _ tyLit@(HsTyLit t)
-  = do { data_kinds <- xoptM Opt_DataKinds
-       ; unless data_kinds (addErr (dataKindsErr isType tyLit))
+rnHsTyKi what _ tyLit@(HsTyLit t)
+  = do { data_kinds <- xoptM LangExt.DataKinds
+       ; unless data_kinds (addErr (dataKindsErr what tyLit))
        ; when (negLit t) (addErr negLitErr)
+       ; checkTypeInType what tyLit
        ; return (HsTyLit t, emptyFVs) }
   where
     negLit (HsStrTy _ _) = False
     negLit (HsNumTy _ i) = i < 0
     negLitErr = ptext (sLit "Illegal literal in type (type literals must not be negative):") <+> ppr tyLit
 
-rnHsTyKi isType doc (HsAppTy ty1 ty2)
-  = do { (ty1', fvs1) <- rnLHsTyKi isType doc ty1
-       ; (ty2', fvs2) <- rnLHsTyKi isType doc ty2
+rnHsTyKi isType doc overall_ty@(HsAppsTy tys)
+  = do { -- Step 1: Break up the HsAppsTy into symbols and non-symbol regions
+         let (non_syms, syms) = splitHsAppsTy tys
+
+             -- Step 2: rename the pieces
+       ; (syms1, fvs1)      <- mapFvRn (rnHsTyOp isType overall_ty) syms
+       ; (non_syms1, fvs2)  <- (mapFvRn . mapFvRn) (rnLHsTyKi isType doc) non_syms
+
+             -- Step 3: deal with *. See Note [Dealing with *]
+       ; let (non_syms2, syms2) = deal_with_star [] [] non_syms1 syms1
+
+             -- Step 4: collapse the non-symbol regions with HsAppTy
+       ; non_syms3 <- mapM deal_with_non_syms non_syms2
+
+             -- Step 5: assemble the pieces, using mkHsOpTyRn
+       ; L _ res_ty <- build_res_ty non_syms3 syms2
+
+        -- all done. Phew.
+       ; return (res_ty, fvs1 `plusFV` fvs2) }
+  where
+    -- See Note [Dealing with *]
+    deal_with_star :: [[LHsType Name]] -> [Located Name]
+                   -> [[LHsType Name]] -> [Located Name]
+                   -> ([[LHsType Name]], [Located Name])
+    deal_with_star acc1 acc2
+                   (non_syms1 : non_syms2 : non_syms) (L loc star : ops)
+      | star `hasKey` starKindTyConKey || star `hasKey` unicodeStarKindTyConKey
+      = deal_with_star acc1 acc2
+                       ((non_syms1 ++ L loc (HsTyVar (L loc star)) : non_syms2) : non_syms)
+                       ops
+    deal_with_star acc1 acc2 (non_syms1 : non_syms) (op1 : ops)
+      = deal_with_star (non_syms1 : acc1) (op1 : acc2) non_syms ops
+    deal_with_star acc1 acc2 [non_syms] []
+      = (reverse (non_syms : acc1), reverse acc2)
+    deal_with_star _ _ _ _
+      = pprPanic "deal_with_star" (ppr overall_ty)
+
+    -- collapse [LHsType Name] to LHsType Name by making applications
+    -- monadic only for failure
+    deal_with_non_syms :: [LHsType Name] -> RnM (LHsType Name)
+    deal_with_non_syms (non_sym : non_syms) = return $ mkHsAppTys non_sym non_syms
+    deal_with_non_syms []                   = failWith (emptyNonSymsErr overall_ty)
+
+    -- assemble a right-biased OpTy for use in mkHsOpTyRn
+    build_res_ty :: [LHsType Name] -> [Located Name] -> RnM (LHsType Name)
+    build_res_ty (arg1 : args) (op1 : ops)
+      = do { rhs <- build_res_ty args ops
+           ; fix <- lookupTyFixityRn op1
+           ; res <-
+               mkHsOpTyRn (\t1 t2 -> HsOpTy t1 op1 t2) (unLoc op1) fix arg1 rhs
+           ; let loc = combineSrcSpans (getLoc arg1) (getLoc rhs)
+           ; return (L loc res)
+           }
+    build_res_ty [arg] [] = return arg
+    build_res_ty _ _ = pprPanic "build_op_ty" (ppr overall_ty)
+
+rnHsTyKi what doc (HsAppTy ty1 ty2)
+  = do { (ty1', fvs1) <- rnLHsTyKi what doc ty1
+       ; (ty2', fvs2) <- rnLHsTyKi what doc ty2
        ; return (HsAppTy ty1' ty2', fvs1 `plusFV` fvs2) }
 
-rnHsTyKi isType doc (HsIParamTy n ty)
-  = ASSERT( isType )
-    do { (ty', fvs) <- rnLHsType doc ty
+rnHsTyKi what doc t@(HsIParamTy n ty)
+  = do { notInKinds what t
+       ; (ty', fvs) <- rnLHsType doc ty
        ; return (HsIParamTy n ty', fvs) }
 
-rnHsTyKi isType doc (HsEqTy ty1 ty2)
-  = ASSERT( isType )
-    do { (ty1', fvs1) <- rnLHsType doc ty1
-       ; (ty2', fvs2) <- rnLHsType doc ty2
+rnHsTyKi what doc t@(HsEqTy ty1 ty2)
+  = do { checkTypeInType what t
+       ; (ty1', fvs1) <- rnLHsTyKi what doc ty1
+       ; (ty2', fvs2) <- rnLHsTyKi what doc ty2
        ; return (HsEqTy ty1' ty2', fvs1 `plusFV` fvs2) }
 
-rnHsTyKi isType _ (HsSpliceTy sp k)
-  = ASSERT( isType )
-    rnSpliceType sp k
+rnHsTyKi _ _ (HsSpliceTy sp k)
+  = rnSpliceType sp k
 
-rnHsTyKi isType doc (HsDocTy ty haddock_doc)
-  = ASSERT( isType )
-    do { (ty', fvs) <- rnLHsType doc ty
+rnHsTyKi _ doc (HsDocTy ty haddock_doc)
+  = do { (ty', fvs) <- rnLHsType doc ty
        ; haddock_doc' <- rnLHsDoc haddock_doc
        ; return (HsDocTy ty' haddock_doc', fvs) }
 
-rnHsTyKi isType _ (HsCoreTy ty)
-  = ASSERT( isType )
-    return (HsCoreTy ty, emptyFVs)
+rnHsTyKi _ _ (HsCoreTy ty)
+  = return (HsCoreTy ty, emptyFVs)
     -- The emptyFVs probably isn't quite right
     -- but I don't think it matters
 
-rnHsTyKi _ _ (HsWrapTy {})
-  = panic "rnHsTyKi"
-
-rnHsTyKi isType doc ty@(HsExplicitListTy k tys)
-  = ASSERT( isType )
-    do { data_kinds <- xoptM Opt_DataKinds
-       ; unless data_kinds (addErr (dataKindsErr isType ty))
-       ; (tys', fvs) <- rnLHsTypes doc tys
+rnHsTyKi what doc ty@(HsExplicitListTy k tys)
+  = do { checkTypeInType what ty
+       ; data_kinds <- xoptM LangExt.DataKinds
+       ; unless data_kinds (addErr (dataKindsErr what ty))
+       ; (tys', fvs) <- mapFvRn (rnLHsTyKi what doc) tys
        ; return (HsExplicitListTy k tys', fvs) }
 
-rnHsTyKi isType doc ty@(HsExplicitTupleTy kis tys)
-  = ASSERT( isType )
-    do { data_kinds <- xoptM Opt_DataKinds
-       ; unless data_kinds (addErr (dataKindsErr isType ty))
-       ; (tys', fvs) <- rnLHsTypes doc tys
+rnHsTyKi what doc ty@(HsExplicitTupleTy kis tys)
+  = do { checkTypeInType what ty
+       ; data_kinds <- xoptM LangExt.DataKinds
+       ; unless data_kinds (addErr (dataKindsErr what ty))
+       ; (tys', fvs) <- mapFvRn (rnLHsTyKi what doc) tys
        ; return (HsExplicitTupleTy kis tys', fvs) }
 
-rnHsTyKi isType _doc (HsWildCardTy (AnonWildCard PlaceHolder))
-  = ASSERT( isType )
-    do { loc <- getSrcSpanM
-       ; uniq <- newUnique
-       ; let name = mkInternalName uniq (mkTyVarOcc "_") loc
-       ; return (HsWildCardTy (AnonWildCard name), emptyFVs) }
-         -- emptyFVs: this occurrence does not refer to a
-         --           binding, so don't treat it as a free variable
-
-rnHsTyKi isType doc (HsWildCardTy (NamedWildCard rdr_name))
-  = ASSERT( isType )
-    do { not_in_scope <- isNothing `fmap` lookupOccRn_maybe rdr_name
-       ; when not_in_scope $
-         -- When the named wild card is not in scope, it means it shouldn't be
-         -- there in the first place, i.e. rnHsSigTypeWithWildCards wasn't
-         -- used, so fail.
-         failWith $ text "Unexpected wild card:" <+> quotes (ppr rdr_name) $$
-                    docOfHsDocContext doc
-       ; name <- rnTyVar isType rdr_name
-       ; return (HsWildCardTy (NamedWildCard name), emptyFVs) }
+rnHsTyKi what ctxt (HsWildCardTy wc)
+  = do { wc' <- case mb_bad of
+           Just msg -> do { addErr (wildCardMsg ctxt msg)
+                          ; discardErrs (rnWildCard ctxt wc) }
+                          -- discardErrs: avoid reporting
+                          -- a second error
+           Nothing  -> rnWildCard ctxt wc
+
+       ; traceRn (text "rnHsTyKi wild" <+> ppr wc <+> ppr (isJust mb_bad))
+       ; return (HsWildCardTy wc', emptyFVs) }
          -- emptyFVs: this occurrence does not refer to a
-         --           binding, so don't treat it as a free variable
+         --           user-written binding site, so don't treat
+         --           it as a free variable
+  where
+    mb_bad :: Maybe SDoc
+    mb_bad | not (wildCardsAllowed ctxt)
+           = Just (notAllowed wc)
+           | otherwise
+           = case what of
+               RnTypeBody _    -> Nothing
+               RnConstraint _  -> Just constraint_msg
+               RnTopConstraint -> case wc of
+                     AnonWildCard {}  -> Just constraint_msg
+                     NamedWildCard {} -> Nothing
+
+    constraint_msg = hang (notAllowed wc <+> ptext (sLit "in a constraint"))
+                        2 hint_msg
+
+    hint_msg = case wc of
+       NamedWildCard {} -> empty
+       AnonWildCard {}  -> vcat [ ptext (sLit "except as the last top-level constraint of a type signature")
+                                , nest 2 (ptext (sLit "e.g  f :: (Eq a, _) => blah")) ]
+
+notAllowed :: HsWildCardInfo RdrName -> SDoc
+notAllowed wc =  ptext (sLit "Wildcard") <+> quotes (ppr wc)
+                 <+> ptext (sLit "not allowed")
+
+wildCardMsg :: HsDocContext -> SDoc -> SDoc
+wildCardMsg ctxt doc
+  = vcat [doc, nest 2 (ptext (sLit "in") <+> pprHsDocContext ctxt)]
 
 --------------
-rnHsTyKiForAll :: Bool -> HsDocContext -> HsType RdrName
-               -> RnM (HsType Name, FreeVars)
-rnHsTyKiForAll isType doc (HsForAllTy Implicit extra _ lctxt@(L _ ctxt) ty)
-  = ASSERT( isType ) do
-        -- Implicit quantifiction in source code (no kinds on tyvars)
-        -- Given the signature  C => T  we universally quantify
-        -- over FV(T) \ {in-scope-tyvars}
-    rdr_env <- getLocalRdrEnv
-    loc <- getSrcSpanM
-    let
-        (forall_kvs, forall_tvs) = filterInScope rdr_env $
-                                   extractHsTysRdrTyVars (ty:ctxt)
-           -- In for-all types we don't bring in scope
-           -- kind variables mentioned in kind signatures
-           -- (Well, not yet anyway....)
-           --    f :: Int -> T (a::k)    -- Not allowed
-
-           -- The filterInScope is to ensure that we don't quantify over
-           -- type variables that are in scope; when GlasgowExts is off,
-           -- there usually won't be any, except for class signatures:
-           --   class C a where { op :: a -> a }
-        tyvar_bndrs = userHsTyVarBndrs loc forall_tvs
-
-    rnForAll doc Implicit extra forall_kvs (mkHsQTvs tyvar_bndrs) lctxt ty
-
-rnHsTyKiForAll isType doc
-               fulltype@(HsForAllTy Qualified extra _ lctxt@(L _ ctxt) ty)
-  = ASSERT( isType ) do
-    rdr_env <- getLocalRdrEnv
-    loc <- getSrcSpanM
-    let
-        (forall_kvs, forall_tvs) = filterInScope rdr_env $
-                                   extractHsTysRdrTyVars (ty:ctxt)
-        tyvar_bndrs = userHsTyVarBndrs loc forall_tvs
-        in_type_doc = ptext (sLit "In the type") <+> quotes (ppr fulltype)
-
-    -- See Note [Context quantification]
-    warnContextQuantification (in_type_doc $$ docOfHsDocContext doc) tyvar_bndrs
-    rnForAll doc Implicit extra forall_kvs (mkHsQTvs tyvar_bndrs) lctxt ty
-
-rnHsTyKiForAll isType doc
-               ty@(HsForAllTy Explicit extra forall_tyvars lctxt@(L _ ctxt) tau)
-  = ASSERT( isType ) do {      -- Explicit quantification.
-         -- Check that the forall'd tyvars are actually
-         -- mentioned in the type, and produce a warning if not
-         let (kvs, mentioned) = extractHsTysRdrTyVars (tau:ctxt)
-             in_type_doc = ptext (sLit "In the type") <+> quotes (ppr ty)
-       ; warnUnusedForAlls (in_type_doc $$ docOfHsDocContext doc)
-                           forall_tyvars mentioned
-       ; traceRn (text "rnHsTyKiForAll:Exlicit" <+> vcat
-            [ppr forall_tyvars, ppr lctxt,ppr tau ])
-       ; rnForAll doc Explicit extra kvs forall_tyvars lctxt tau }
-
--- The following should never happen but keeps the completeness checker happy
-rnHsTyKiForAll isType doc ty = rnHsTyKi isType doc ty
---------------
-rnTyVar :: Bool -> RdrName -> RnM Name
-rnTyVar is_type rdr_name
-  | is_type   = lookupTypeOccRn rdr_name
-  | otherwise = lookupKindOccRn rdr_name
+rnTyVar :: RnTyKiWhat -> RdrName -> RnM Name
+rnTyVar what rdr_name
+  | isRnKindLevel what = lookupKindOccRn rdr_name
+  | otherwise          = lookupTypeOccRn rdr_name
+
+rnLTyVar :: Located RdrName -> RnM (Located Name)
+rnLTyVar (L loc rdr_name)
+  = do { tyvar <- lookupTypeOccRn rdr_name
+       ; return (L loc tyvar) }
 
+--------------
+rnHsTyOp :: Outputable a
+         => RnTyKiWhat -> a -> Located RdrName -> RnM (Located Name, FreeVars)
+rnHsTyOp what overall_ty (L loc op)
+  = do { ops_ok <- xoptM LangExt.TypeOperators
+       ; op' <- rnTyVar what op
+       ; unless (ops_ok
+                 || op' == starKindTyConName
+                 || op' == unicodeStarKindTyConName
+                 || op' `hasKey` eqTyConKey) $
+           addErr (opTyErr op overall_ty)
+       ; let l_op' = L loc op'
+       ; return (l_op', unitFV op') }
 
 --------------
 rnLHsTypes :: HsDocContext -> [LHsType RdrName]
            -> RnM ([LHsType Name], FreeVars)
 rnLHsTypes doc tys = mapFvRn (rnLHsType doc) tys
 
-rnForAll :: HsDocContext -> HsExplicitFlag
-         -> Maybe SrcSpan           -- Location of an extra-constraints wildcard
-         -> [RdrName]               -- Kind variables
-         -> LHsTyVarBndrs RdrName   -- Type variables
-         -> LHsContext RdrName -> LHsType RdrName
-         -> RnM (HsType Name, FreeVars)
-
-rnForAll doc exp extra kvs forall_tyvars ctxt ty
-  | null kvs, null (hsQTvBndrs forall_tyvars), null (unLoc ctxt), isNothing extra
-  = rnHsType doc (unLoc ty)
-        -- One reason for this case is that a type like Int#
-        -- starts off as (HsForAllTy Implicit Nothing [] Int), in case
-        -- there is some quantification.  Now that we have quantified
-        -- and discovered there are no type variables, it's nicer to turn
-        -- it into plain Int.  If it were Int# instead of Int, we'd actually
-        -- get an error, because the body of a genuine for-all is
-        -- of kind *.
+--------------
+extraConstraintWildCardsAllowed :: HsDocContext -> Bool
+extraConstraintWildCardsAllowed ctxt
+  = case ctxt of
+      TypeSigCtx {}       -> True
+      _                   -> False
+
+wildCardsAllowed :: HsDocContext -> Bool
+-- ^ In what contexts are wildcards permitted
+wildCardsAllowed ctxt
+   = case ctxt of
+       TypeSigCtx {}       -> True
+       TypBrCtx {}         -> True   -- Template Haskell quoted type
+       SpliceTypeCtx {}    -> True   -- Result of a Template Haskell splice
+       ExprWithTySigCtx {} -> True
+       PatCtx {}           -> True
+       RuleCtx {}          -> True
+       FamPatCtx {}        -> True   -- Not named wildcards though
+       GHCiCtx {}          -> True
+       _                   -> False
+
+rnExtraConstraintWildCard :: HsDocContext -> HsWildCardInfo RdrName
+                          -> RnM (HsWildCardInfo Name)
+-- Rename the extra-constraint spot in a type signature
+--    (blah, _) => type
+-- Check that extra-constraints are allowed at all, and
+-- if so that it's an anonymous wildcard
+rnExtraConstraintWildCard ctxt wc
+  = case mb_bad of
+      Nothing  -> rnWildCard ctxt wc
+      Just msg -> do { addErr (wildCardMsg ctxt msg)
+                     ; discardErrs (rnWildCard ctxt wc) }
+  where
+    mb_bad | not (extraConstraintWildCardsAllowed ctxt)
+           = Just (ptext (sLit "Extra-contraint wildcard") <+> quotes (ppr wc)
+                   <+> ptext (sLit "not allowed"))
+           | isNamedWildCard wc
+           = Just (hang (ptext (sLit "Named wildcard") <+> quotes (ppr wc)
+                         <+> ptext (sLit "not allowed as an extra-contraint"))
+                      2 (ptext (sLit "Use an anonymous wildcard instead")))
+           | otherwise
+           = Nothing
+
+rnWildCard :: HsDocContext -> HsWildCardInfo RdrName -> RnM (HsWildCardInfo Name)
+rnWildCard _ (AnonWildCard _)
+  = do { loc <- getSrcSpanM
+       ; uniq <- newUnique
+       ; let name = mkInternalName uniq (mkTyVarOcc "_") loc
+       ; return (AnonWildCard (L loc name)) }
+
+rnWildCard ctxt wc@(NamedWildCard (L loc rdr_name))
+  -- NB: The parser only generates NamedWildCard if -XNamedWildCards
+  --     is on, so we don't need to check for that here
+  = do { mb_name <- lookupOccRn_maybe rdr_name
+       ; traceRn (text "rnWildCard named" <+> (ppr rdr_name $$ ppr mb_name))
+       ; case mb_name of
+           Just n  -> return (NamedWildCard (L loc n))
+           Nothing -> do { addErr msg  -- I'm not sure how this can happen
+                         ; return (NamedWildCard (L loc (mkUnboundNameRdr rdr_name))) } }
+  where
+    msg = wildCardMsg ctxt (notAllowed wc)
 
-  | otherwise
-  = bindHsTyVars doc Nothing kvs forall_tyvars $ \ new_tyvars ->
-    do { (new_ctxt, fvs1) <- rnContext doc ctxt
-       ; (new_ty, fvs2) <- rnLHsType doc ty
-       ; return (HsForAllTy exp extra new_tyvars new_ctxt new_ty, fvs1 `plusFV` fvs2) }
-        -- Retain the same implicit/explicit flag as before
-        -- so that we can later print it correctly
 
 ---------------
+-- | Ensures either that we're in a type or that -XTypeInType is set
+checkTypeInType :: Outputable ty
+                => RnTyKiWhat
+                -> ty      -- ^ type
+                -> RnM ()
+checkTypeInType what ty
+  | isRnKindLevel what
+  = do { type_in_type <- xoptM LangExt.TypeInType
+       ; unless type_in_type $
+         addErr (text "Illegal kind:" <+> ppr ty $$
+                 text "Did you mean to enable TypeInType?") }
+checkTypeInType _ _ = return ()
+
+notInKinds :: Outputable ty
+           => RnTyKiWhat
+           -> ty
+           -> RnM ()
+notInKinds what ty
+  | isRnKindLevel what
+  = addErr (text "Illegal kind (even with TypeInType enabled):" <+> ppr ty)
+notInKinds _ _ = return ()
+
+{- *****************************************************
+*                                                      *
+          Binding type variables
+*                                                      *
+***************************************************** -}
+
 bindSigTyVarsFV :: [Name]
                 -> RnM (a, FreeVars)
                 -> RnM (a, FreeVars)
@@ -405,187 +803,203 @@ bindSigTyVarsFV :: [Name]
 -- with a separate type signature, to bring its tyvars into scope
 -- With no -XScopedTypeVariables, this is a no-op
 bindSigTyVarsFV tvs thing_inside
-  = do  { scoped_tyvars <- xoptM Opt_ScopedTypeVariables
+  = do  { scoped_tyvars <- xoptM LangExt.ScopedTypeVariables
         ; if not scoped_tyvars then
                 thing_inside
           else
                 bindLocalNamesFV tvs thing_inside }
 
+-- | Simply bring a bunch of RdrNames into scope. No checking for
+-- validity, at all. The binding location is taken from the location
+-- on each name.
+bindLRdrNames :: [Located RdrName]
+              -> ([Name] -> RnM (a, FreeVars))
+              -> RnM (a, FreeVars)
+bindLRdrNames rdrs thing_inside
+  = do { var_names <- mapM (newTyVarNameRn Nothing) rdrs
+       ; bindLocalNamesFV var_names $
+         thing_inside var_names }
+
 ---------------
-bindHsTyVars :: HsDocContext
-             -> Maybe a                 -- Just _  => an associated type decl
-             -> [RdrName]               -- Kind variables from scope
-             -> LHsTyVarBndrs RdrName   -- Type variables
-             -> (LHsTyVarBndrs Name -> RnM (b, FreeVars))
-             -> RnM (b, FreeVars)
+bindHsQTyVars :: forall a b.
+                 HsDocContext
+              -> Maybe a                 -- Just _  => an associated type decl
+              -> [Located RdrName]       -- Kind variables from scope, in l-to-r
+                                         -- order, but not from ...
+              -> (LHsQTyVars RdrName)     -- ... these user-written tyvars
+              -> (LHsQTyVars Name -> RnM (b, FreeVars))
+              -> RnM (b, FreeVars)
 -- (a) Bring kind variables into scope
 --     both (i)  passed in (kv_bndrs)
 --     and  (ii) mentioned in the kinds of tv_bndrs
 -- (b) Bring type variables into scope
-bindHsTyVars doc mb_assoc kv_bndrs tv_bndrs thing_inside
+bindHsQTyVars doc mb_assoc kv_bndrs tv_bndrs thing_inside
+  = do { bindLHsTyVarBndrs doc mb_assoc kv_bndrs (hsQTvExplicit tv_bndrs) $
+         \ rn_kvs rn_bndrs ->
+         thing_inside (HsQTvs { hsq_implicit = rn_kvs
+                              , hsq_explicit = rn_bndrs }) }
+
+bindLHsTyVarBndrs :: forall a b.
+                     HsDocContext
+                  -> Maybe a            -- Just _  => an associated type decl
+                  -> [Located RdrName]  -- Unbound kind variables from scope,
+                                        -- in l-to-r order, but not from ...
+                  -> [LHsTyVarBndr RdrName]  -- ... these user-written tyvars
+                  -> (   [Name]  -- all kv names
+                      -> [LHsTyVarBndr Name]
+                      -> RnM (b, FreeVars))
+                  -> RnM (b, FreeVars)
+bindLHsTyVarBndrs doc mb_assoc kv_bndrs tv_bndrs thing_inside
+  = do { when (isNothing mb_assoc) (checkShadowedRdrNames tv_names_w_loc)
+       ; go [] [] emptyNameSet emptyNameSet tv_bndrs }
+  where
+    tv_names_w_loc = map hsLTyVarLocName tv_bndrs
+
+    go :: [Name]                 -- kind-vars found (in reverse order)
+       -> [LHsTyVarBndr Name]    -- already renamed (in reverse order)
+       -> NameSet                -- kind vars already in scope (for dup checking)
+       -> NameSet                -- type vars already in scope (for dup checking)
+       -> [LHsTyVarBndr RdrName] -- still to be renamed, scoped
+       -> RnM (b, FreeVars)
+    go rn_kvs rn_tvs kv_names tv_names (tv_bndr : tv_bndrs)
+      = bindLHsTyVarBndr doc mb_assoc kv_names tv_names tv_bndr $
+        \ kv_nms tv_bndr' -> go (reverse kv_nms ++ rn_kvs)
+                                (tv_bndr' : rn_tvs)
+                                (kv_names `extendNameSetList` kv_nms)
+                                (tv_names `extendNameSet` hsLTyVarName tv_bndr')
+                                tv_bndrs
+
+    go rn_kvs rn_tvs _kv_names tv_names []
+      = -- still need to deal with the kv_bndrs passed in originally
+        bindImplicitKvs doc mb_assoc kv_bndrs tv_names $ \ kv_nms ->
+        do { let all_rn_kvs = reverse (reverse kv_nms ++ rn_kvs)
+                 all_rn_tvs = reverse rn_tvs
+           ; env <- getLocalRdrEnv
+           ; traceRn (text "bindHsTyVars" <+> (ppr env $$
+                                               ppr all_rn_kvs $$
+                                               ppr all_rn_tvs))
+           ; thing_inside all_rn_kvs all_rn_tvs }
+
+bindLHsTyVarBndr :: HsDocContext
+                 -> Maybe a   -- associated class
+                 -> NameSet   -- kind vars already in scope
+                 -> NameSet   -- type vars already in scope
+                 -> LHsTyVarBndr RdrName
+                 -> ([Name] -> LHsTyVarBndr Name -> RnM (b, FreeVars))
+                   -- passed the newly-bound implicitly-declared kind vars,
+                   -- and the renamed LHsTyVarBndr
+                 -> RnM (b, FreeVars)
+bindLHsTyVarBndr doc mb_assoc kv_names tv_names hs_tv_bndr thing_inside
+  = case hs_tv_bndr of
+      L loc (UserTyVar lrdr@(L lv rdr)) ->
+        do { check_dup loc rdr
+           ; nm <- newTyVarNameRn mb_assoc lrdr
+           ; bindLocalNamesFV [nm] $
+             thing_inside [] (L loc (UserTyVar (L lv nm))) }
+      L loc (KindedTyVar lrdr@(L lv rdr) kind) ->
+        do { check_dup lv rdr
+
+             -- check for -XKindSignatures
+           ; sig_ok <- xoptM LangExt.KindSignatures
+           ; unless sig_ok (badKindSigErr doc kind)
+
+             -- deal with kind vars in the user-written kind
+           ; free_kvs <- freeKiTyVarsAllVars <$> extractHsTyRdrTyVars kind
+           ; bindImplicitKvs doc mb_assoc free_kvs tv_names $ \ kv_nms ->
+             do { (kind', fvs1) <- rnLHsKind doc kind
+                ; tv_nm  <- newTyVarNameRn mb_assoc lrdr
+                ; (b, fvs2) <- bindLocalNamesFV [tv_nm] $
+                               thing_inside kv_nms
+                                 (L loc (KindedTyVar (L lv tv_nm) kind'))
+                ; return (b, fvs1 `plusFV` fvs2) }}
+  where
+      -- make sure that the RdrName isn't in the sets of
+      -- names. We can't just check that it's not in scope at all
+      -- because we might be inside an associated class.
+    check_dup :: SrcSpan -> RdrName -> RnM ()
+    check_dup loc rdr
+      = do { m_name <- lookupLocalOccRn_maybe rdr
+           ; whenIsJust m_name $ \name ->
+        do { when (name `elemNameSet` kv_names) $
+             addErrAt loc (vcat [ ki_ty_err_msg name
+                                , pprHsDocContext doc ])
+           ; when (name `elemNameSet` tv_names) $
+             dupNamesErr getLoc [L loc name, L (nameSrcSpan name) name] }}
+
+    ki_ty_err_msg n = text "Variable" <+> quotes (ppr n) <+>
+                      text "used as a kind variable before being bound" $$
+                      text "as a type variable. Perhaps reorder your variables?"
+
+
+bindImplicitKvs :: HsDocContext
+                -> Maybe a
+                -> [Located RdrName]  -- ^ kind var *occurrences*, from which
+                                      -- intent to bind is inferred
+                -> NameSet            -- ^ *type* variables, for type/kind
+                                      -- misuse check for -XNoTypeInType
+                -> ([Name] -> RnM (b, FreeVars)) -- ^ passed new kv_names
+                -> RnM (b, FreeVars)
+bindImplicitKvs _   _        []       _        thing_inside = thing_inside []
+bindImplicitKvs doc mb_assoc free_kvs tv_names thing_inside
   = do { rdr_env <- getLocalRdrEnv
-       ; let tvs = hsQTvBndrs tv_bndrs
-             kvs_from_tv_bndrs = [ kv | L _ (KindedTyVar _ kind) <- tvs
-                                 , let (_, kvs) = extractHsTyRdrTyVars kind
-                                 , kv <- kvs ]
-             all_kvs' = nub (kv_bndrs ++ kvs_from_tv_bndrs)
-             all_kvs  = filterOut (`elemLocalRdrEnv` rdr_env) all_kvs'
-
-             overlap_kvs = [ kv | kv <- all_kvs, any ((==) kv . hsLTyVarName) tvs ]
-                -- These variables appear both as kind and type variables
-                -- in the same declaration; eg  type family  T (x :: *) (y :: x)
-                -- We disallow this: too confusing!
-
-       ; poly_kind <- xoptM Opt_PolyKinds
-       ; unless (poly_kind || null all_kvs)
-                (addErr (badKindBndrs doc all_kvs))
-       ; unless (null overlap_kvs)
-                (addErr (overlappingKindVars doc overlap_kvs))
-
-       ; loc <- getSrcSpanM
-       ; kv_names <- mapM (newLocalBndrRn . L loc) all_kvs
-       ; bindLocalNamesFV kv_names $
-    do { let tv_names_w_loc = hsLTyVarLocNames tv_bndrs
-
-             rn_tv_bndr :: LHsTyVarBndr RdrName -> RnM (LHsTyVarBndr Name, FreeVars)
-             rn_tv_bndr (L loc (UserTyVar rdr))
-               = do { nm <- newTyVarNameRn mb_assoc rdr_env loc rdr
-                    ; return (L loc (UserTyVar nm), emptyFVs) }
-             rn_tv_bndr (L loc (KindedTyVar (L lv rdr) kind))
-               = do { sig_ok <- xoptM Opt_KindSignatures
-                    ; unless sig_ok (badSigErr False doc kind)
-                    ; nm <- newTyVarNameRn mb_assoc rdr_env loc rdr
-                    ; (kind', fvs) <- rnLHsKind doc kind
-                    ; return (L loc (KindedTyVar (L lv nm) kind'), fvs) }
-
-       -- Check for duplicate or shadowed tyvar bindrs
-       ; checkDupRdrNames tv_names_w_loc
-       ; when (isNothing mb_assoc) (checkShadowedRdrNames tv_names_w_loc)
-
-       ; (tv_bndrs', fvs1) <- mapFvRn rn_tv_bndr tvs
-       ; (res, fvs2) <- bindLocalNamesFV (map hsLTyVarName tv_bndrs') $
-                        do { inner_rdr_env <- getLocalRdrEnv
-                           ; traceRn (text "bhtv" <+> vcat
-                                 [ ppr tvs, ppr kv_bndrs, ppr kvs_from_tv_bndrs
-                                 , ppr $ map (`elemLocalRdrEnv` rdr_env) all_kvs'
-                                 , ppr $ map (getUnique . rdrNameOcc) all_kvs'
-                                 , ppr all_kvs, ppr rdr_env, ppr inner_rdr_env ])
-                           ; thing_inside (HsQTvs { hsq_tvs = tv_bndrs', hsq_kvs = kv_names }) }
-       ; return (res, fvs1 `plusFV` fvs2) } }
+       ; let part_kvs lrdr@(L loc kv_rdr)
+               = case lookupLocalRdrEnv rdr_env kv_rdr of
+                   Just kv_name -> Left (L loc kv_name)
+                   _            -> Right lrdr
+             (bound_kvs, new_kvs) = partitionWith part_kvs free_kvs
+
+          -- check whether we're mixing types & kinds illegally
+       ; type_in_type <- xoptM LangExt.TypeInType
+       ; unless type_in_type $
+         mapM_ (check_tv_used_in_kind tv_names) bound_kvs
+
+       ; poly_kinds <- xoptM LangExt.PolyKinds
+       ; unless poly_kinds $
+         addErr (badKindBndrs doc new_kvs)
+
+          -- bind the vars and move on
+       ; kv_nms <- mapM (newTyVarNameRn mb_assoc) new_kvs
+       ; bindLocalNamesFV kv_nms $
+         thing_inside kv_nms }
+  where
+      -- check to see if the variables free in a kind are bound as type
+      -- variables. Assume -XNoTypeInType.
+    check_tv_used_in_kind :: NameSet       -- ^ *type* variables
+                          -> Located Name  -- ^ renamed var used in kind
+                          -> RnM ()
+    check_tv_used_in_kind tv_names (L loc kv_name)
+      = when (kv_name `elemNameSet` tv_names) $
+        addErrAt loc (vcat [ text "Type variable" <+> quotes (ppr kv_name) <+>
+                             text "used in a kind." $$
+                             text "Did you mean to use TypeInType?"
+                           , pprHsDocContext doc ])
+
+
+newTyVarNameRn :: Maybe a -> Located RdrName -> RnM Name
+newTyVarNameRn mb_assoc (L loc rdr)
+  = do { rdr_env <- getLocalRdrEnv
+       ; case (mb_assoc, lookupLocalRdrEnv rdr_env rdr) of
+           (Just _, Just n) -> return n
+              -- Use the same Name as the parent class decl
 
-newTyVarNameRn :: Maybe a -> LocalRdrEnv -> SrcSpan -> RdrName -> RnM Name
-newTyVarNameRn mb_assoc rdr_env loc rdr
-  | Just _ <- mb_assoc    -- Use the same Name as the parent class decl
-  , Just n <- lookupLocalRdrEnv rdr_env rdr
-  = return n
-  | otherwise
-  = newLocalBndrRn (L loc rdr)
-
---------------------------------
-rnHsBndrSig :: HsDocContext
-            -> HsWithBndrs RdrName (LHsType RdrName)
-            -> (HsWithBndrs Name (LHsType Name) -> RnM (a, FreeVars))
-            -> RnM (a, FreeVars)
-rnHsBndrSig doc (HsWB { hswb_cts = ty@(L loc _) }) thing_inside
-  = do { sig_ok <- xoptM Opt_ScopedTypeVariables
-       ; unless sig_ok (badSigErr True doc ty)
-       ; let (kv_bndrs, tv_bndrs) = extractHsTyRdrTyVars ty
-       ; name_env <- getLocalRdrEnv
-       ; tv_names <- newLocalBndrsRn [L loc tv | tv <- tv_bndrs
-                                               , not (tv `elemLocalRdrEnv` name_env) ]
-       ; kv_names <- newLocalBndrsRn [L loc kv | kv <- kv_bndrs
-                                               , not (kv `elemLocalRdrEnv` name_env) ]
-       ; bindLocalNamesFV kv_names $
-         bindLocalNamesFV tv_names $
-    do { (ty', fvs1, wcs) <- rnLHsTypeWithWildCards doc ty
-       ; (res, fvs2) <- thing_inside (HsWB { hswb_cts = ty', hswb_kvs = kv_names,
-                                             hswb_tvs = tv_names, hswb_wcs = wcs })
-       ; return (res, fvs1 `plusFV` fvs2) } }
+           _                -> newLocalBndrRn (L loc rdr) }
 
-overlappingKindVars :: HsDocContext -> [RdrName] -> SDoc
-overlappingKindVars doc kvs
-  = vcat [ ptext (sLit "Kind variable") <> plural kvs <+>
-           ptext (sLit "also used as type variable") <> plural kvs
-           <> colon <+> pprQuotedList kvs
-         , docOfHsDocContext doc ]
+---------------------
+collectNamedWildCards :: LHsType RdrName -> [Located RdrName]
+collectNamedWildCards hs_ty
+  = nubBy eqLocated $
+    [n | L _ (NamedWildCard n) <- collectWildCards hs_ty ]
 
-badKindBndrs :: HsDocContext -> [RdrName] -> SDoc
-badKindBndrs doc kvs
-  = vcat [ hang (ptext (sLit "Unexpected kind variable") <> plural kvs
-                 <+> pprQuotedList kvs)
-              2 (ptext (sLit "Perhaps you intended to use PolyKinds"))
-         , docOfHsDocContext doc ]
+collectAnonWildCards :: LHsType Name -> [Name]
+collectAnonWildCards hs_ty
+  = [n | L _ (AnonWildCard (L _ n)) <- collectWildCards hs_ty ]
 
-badSigErr :: Bool -> HsDocContext -> LHsType RdrName -> TcM ()
-badSigErr is_type doc (L loc ty)
-  = setSrcSpan loc $ addErr $
-    vcat [ hang (ptext (sLit "Illegal") <+> what
-                 <+> ptext (sLit "signature:") <+> quotes (ppr ty))
-              2 (ptext (sLit "Perhaps you intended to use") <+> flag)
-         , docOfHsDocContext doc ]
+collectWildCards :: LHsType name -> [Located (HsWildCardInfo name)]
+-- | Extract all wild cards from a type.
+collectWildCards lty = go lty
   where
-    what | is_type   = ptext (sLit "type")
-         | otherwise = ptext (sLit "kind")
-    flag | is_type   = ptext (sLit "ScopedTypeVariables")
-         | otherwise = ptext (sLit "KindSignatures")
-
-dataKindsErr :: Bool -> HsType RdrName -> SDoc
-dataKindsErr is_type thing
-  = hang (ptext (sLit "Illegal") <+> what <> colon <+> quotes (ppr thing))
-       2 (ptext (sLit "Perhaps you intended to use DataKinds"))
-  where
-    what | is_type   = ptext (sLit "type")
-         | otherwise = ptext (sLit "kind")
-
---------------------------------
--- | Variant of @rnHsSigType@ that supports wild cards. Also returns the wild
--- cards to bind.
-rnHsSigTypeWithWildCards :: SDoc -> LHsType RdrName
-                         -> RnM (LHsType Name, FreeVars, [Name])
-rnHsSigTypeWithWildCards doc_str ty
-  = rnLHsTypeWithWildCards (TypeSigCtx doc_str) ty'
-  where
-    ty' = extractExtraCtsWc `fmap` flattenTopLevelLHsForAllTy ty
-    -- When there is a wild card at the end of the context, remove it and add
-    -- its location as the extra-constraints wild card in the HsForAllTy.
-    extractExtraCtsWc (HsForAllTy flag _ bndrs (L l ctxt) ty)
-      | Just (ctxt', ct) <- snocView ctxt
-      , L lx (HsWildCardTy (AnonWildCard _)) <- ignoreParens ct
-      = HsForAllTy flag (Just lx) bndrs (L l ctxt') ty
-    extractExtraCtsWc ty = ty
-
--- | Variant of @rnLHsType@ that supports wild cards. The third element of the
--- tuple consists of the freshly generated names of the anonymous wild cards
--- occurring in the type, as well as the names of the named wild cards in the
--- type that are not yet in scope.
-rnLHsTypeWithWildCards  :: HsDocContext -> LHsType RdrName
-                        -> RnM (LHsType Name, FreeVars, [Name])
-rnLHsTypeWithWildCards doc ty
-  = do { checkValidPartialType doc ty
-       ; rdr_env <- getLocalRdrEnv
-       -- Filter out named wildcards that are already in scope
-       ; let (_, wcs) = collectWildCards ty
-             nwcs = [L loc n | L loc (NamedWildCard n) <- wcs
-                             , not (elemLocalRdrEnv n rdr_env) ]
-       ; bindLocatedLocalsRn nwcs $ \nwcs' -> do {
-         (ty', fvs) <- rnLHsType doc ty
-       -- Add the anonymous wildcards that have been given names during
-       -- renaming
-       ; let (_, wcs') = collectWildCards ty'
-             awcs      = filter (isAnonWildCard . unLoc) wcs'
-       ; return (ty', fvs, nwcs' ++ map (HsSyn.wildCardName . unLoc) awcs) } }
-
--- | Extract all wild cards from a type. The named and anonymous
--- extra-constraints wild cards are returned separately to be able to give
--- more accurate error messages.
-collectWildCards
-  :: Eq name => LHsType name
-  -> ([Located (HsWildCardInfo name)],  -- extra-constraints wild cards
-      [Located (HsWildCardInfo name)])  -- wild cards
-collectWildCards lty = (extra, nubBy sameNamedWildCard wcs)
-  where
-    (extra, wcs) = go lty
     go (L loc ty) = case ty of
+      HsAppsTy tys            -> gos (mapMaybe prefix_types_only tys)
       HsAppTy ty1 ty2         -> go ty1 `mappend` go ty2
       HsFunTy ty1 ty2         -> go ty1 `mappend` go ty2
       HsListTy ty             -> go ty
@@ -601,127 +1015,73 @@ collectWildCards lty = (extra, nubBy sameNamedWildCard wcs)
       HsRecTy flds            -> gos $ map (cd_fld_type . unLoc) flds
       HsExplicitListTy _ tys  -> gos tys
       HsExplicitTupleTy _ tys -> gos tys
-      HsWrapTy _ ty           -> go (L loc ty)
       -- Interesting cases
-      HsWildCardTy wc         -> ([], [L loc wc])
-      HsForAllTy _ _ _ (L _ ctxt) ty -> ctxtWcs `mappend` go ty
-        where
-          ctxt' = map ignoreParens ctxt
-          extraWcs  = [L l wc | L l (HsWildCardTy wc) <- ctxt']
-          (_, wcs) = gos ctxt'
-          -- Remove extra-constraints wild cards from wcs
-          ctxtWcs = (extraWcs, deleteFirstsBy sameWildCard
-                               (nubBy sameWildCard wcs) extraWcs)
+      HsWildCardTy wc         -> [L loc wc]
+      HsForAllTy { hst_body = ty } -> go ty
+      HsQualTy { hst_ctxt = L _ ctxt
+               , hst_body = ty }  -> gos ctxt `mappend` go ty
       -- HsQuasiQuoteTy, HsSpliceTy, HsCoreTy, HsTyLit
       _ -> mempty
-    gos = mconcat . map go
-
--- | Check the validity of a partial type signature. The following things are
--- checked:
---
--- * Named extra-constraints wild cards aren't allowed,
--- e.g. invalid: @(Show a, _x) => a -> String@.
---
--- * There is only one extra-constraints wild card in the context and it must
--- come last, e.g. invalid: @(_, Show a) => a -> String@
--- or @(_, Show a, _) => a -> String@.
---
--- * There should be no unnamed wild cards in the context.
---
--- * An extra-constraints wild card can only occur in the top-level context.
--- This would be invalid: @(Eq a, _) => a -> (Num a, _) => a -> Bool@.
---
--- * Named wild cards occurring in the context must also occur in the monotype.
---
--- When an invalid wild card is found, we fail with an error.
-checkValidPartialType :: HsDocContext -> LHsType RdrName -> RnM ()
-checkValidPartialType doc lty
-  = do { whenNonEmpty isNamedWildCard inExtra $ \(L loc _) ->
-           failAt loc $ typeDoc $$
-           text "An extra-constraints wild card cannot be named" $$
-           docOfHsDocContext doc
-
-       ; whenNonEmpty isAnonWildCard extraTopLevel $ \(L loc _) ->
-           failAt loc $ typeDoc $$
-           -- If there was a valid extra-constraints wild card, it should have
-           -- already been removed and its location should be stored in the
-           -- HsForAllTy
-           (case extra of
-             Just _ ->
-               -- We're in a top-level context with an extracted
-               -- extra-constraints wild card.
-               text "Only a single extra-constraints wild card is allowed"
-             _ | TypeSigCtx _ <- doc ->
-               -- We're in a top-level context, but the extra-constraints wild
-               -- card didn't occur at the end.
-               fcat [ text "An extra-constraints wild card must occur"
-                    , text "at the end of the constraints" ]
-             _ ->
-               -- We're not in a top-level context, so no extra-constraints
-               -- wild cards are supported.
-               fcat [ text "An extra-constraints wild card is only allowed"
-                    , text "in the top-level context" ]) $$
-           docOfHsDocContext doc
-
-       ; whenNonEmpty isAnonWildCard inCtxt $ \(L loc _) ->
-           failAt loc $ typeDoc $$
-           text "Anonymous wild cards are not allowed in constraints" $$
-           docOfHsDocContext doc
-
-       ; whenNonEmpty isAnonWildCard nestedExtra $ \(L loc _) ->
-           failAt loc $ typeDoc $$
-           fcat [ text "An extra-constraints wild card is only allowed"
-                , text "in the top-level context" ] $$
-           docOfHsDocContext doc
-
-       ; whenNonEmpty isNamedWildCard inCtxtNotInTau $ \(L loc name) ->
-           failAt loc $ typeDoc $$
-           fcat [ text "The named wild card" <+> quotes (ppr name) <> space
-                , text "is only allowed in the constraints"
-                , text "when it also occurs in the rest of the type" ] $$
-           docOfHsDocContext doc }
-  where
-    typeDoc               = hang (text "Invalid partial type:") 2 (ppr lty)
-    (extra, ctxt, tau)    = splitPartialType lty
-    (inExtra,     _)      = collectWildCards lty
-    (nestedExtra, inTau)  = collectWildCards tau
-    (_,           inCtxt) = mconcat $ map collectWildCards ctxt
-    inCtxtNotInTau        = deleteFirstsBy sameWildCard inCtxt inTau
-    extraTopLevel         = deleteFirstsBy sameWildCard inExtra nestedExtra
 
-    splitPartialType (L _ (HsForAllTy _ extra _ (L _ ctxt) ty))
-      = (extra, map ignoreParens ctxt, ty)
-    splitPartialType ty = (Nothing, [], ty)
+    gos = mconcat . map go
 
-    whenNonEmpty test wcs f
-      = whenIsJust (listToMaybe $ filter (test . unLoc) wcs) f
+    prefix_types_only (HsAppPrefix ty) = Just ty
+    prefix_types_only (HsAppInfix _)   = Nothing
 
 
 {-
 *********************************************************
-*                                                      *
-\subsection{Contexts and predicates}
-*                                                      *
+*                                                       *
+        ConDeclField
+*                                                       *
 *********************************************************
+
+When renaming a ConDeclField, we have to find the FieldLabel
+associated with each field.  But we already have all the FieldLabels
+available (since they were brought into scope by
+RnNames.getLocalNonValBinders), so we just take the list as an
+argument, build a map and look them up.
 -}
 
-rnConDeclFields :: HsDocContext -> [LConDeclField RdrName]
+rnConDeclFields :: [FieldLabel] -> HsDocContext -> [LConDeclField RdrName]
                 -> RnM ([LConDeclField Name], FreeVars)
-rnConDeclFields doc fields = mapFvRn (rnField doc) fields
+rnConDeclFields fls doc fields = mapFvRn (rnField fl_env doc) fields
+  where
+    fl_env = mkFsEnv [ (flLabel fl, fl) | fl <- fls ]
 
-rnField :: HsDocContext -> LConDeclField RdrName
+rnField :: FastStringEnv FieldLabel -> HsDocContext -> LConDeclField RdrName
         -> RnM (LConDeclField Name, FreeVars)
-rnField doc (L l (ConDeclField names ty haddock_doc))
-  = do { new_names <- mapM lookupLocatedTopBndrRn names
+rnField fl_env doc (L l (ConDeclField names ty haddock_doc))
+  = do { let new_names = map (fmap lookupField) names
        ; (new_ty, fvs) <- rnLHsType doc ty
        ; new_haddock_doc <- rnMbLHsDoc haddock_doc
        ; return (L l (ConDeclField new_names new_ty new_haddock_doc), fvs) }
+  where
+    lookupField :: FieldOcc RdrName -> FieldOcc Name
+    lookupField (FieldOcc (L lr rdr) _) = FieldOcc (L lr rdr) (flSelector fl)
+      where
+        lbl = occNameFS $ rdrNameOcc rdr
+        fl  = expectJust "rnField" $ lookupFsEnv fl_env lbl
 
-rnContext :: HsDocContext -> LHsContext RdrName -> RnM (LHsContext Name, FreeVars)
-rnContext doc (L loc cxt)
-  = do { (cxt', fvs) <- rnLHsTypes doc cxt
+
+{-
+*********************************************************
+*                                                       *
+        Contexts
+*                                                       *
+*********************************************************
+-}
+
+rnTyKiContext :: RnTyKiWhat
+              -> HsDocContext -> LHsContext RdrName -> RnM (LHsContext Name, FreeVars)
+rnTyKiContext what doc (L loc cxt)
+  = do { traceRn (text "rncontext" <+> ppr cxt)
+       ; (cxt', fvs) <- mapFvRn (rnLHsPred what doc) cxt
        ; return (L loc cxt', fvs) }
 
+rnContext :: HsDocContext -> LHsContext RdrName -> RnM (LHsContext Name, FreeVars)
+rnContext = rnTyKiContext (RnConstraint TypeLevel)
+
 {-
 ************************************************************************
 *                                                                      *
@@ -754,10 +1114,10 @@ mkHsOpTyRn :: (LHsType Name -> LHsType Name -> HsType Name)
            -> Name -> Fixity -> LHsType Name -> LHsType Name
            -> RnM (HsType Name)
 
-mkHsOpTyRn mk1 pp_op1 fix1 ty1 (L loc2 (HsOpTy ty21 (w2, op2) ty22))
+mkHsOpTyRn mk1 pp_op1 fix1 ty1 (L loc2 (HsOpTy ty21 op2 ty22))
   = do  { fix2 <- lookupTyFixityRn op2
         ; mk_hs_op_ty mk1 pp_op1 fix1 ty1
-                      (\t1 t2 -> HsOpTy t1 (w2, op2) t2)
+                      (\t1 t2 -> HsOpTy t1 op2 t2)
                       (unLoc op2) fix2 ty21 ty22 loc2 }
 
 mkHsOpTyRn mk1 pp_op1 fix1 ty1 (L loc2 (HsFunTy ty21 ty22))
@@ -838,10 +1198,10 @@ mkOpAppRn e1 op fix e2                  -- Default case, no rearrangment
 
 ----------------------------
 get_op :: LHsExpr Name -> Name
--- An unbound name could be either HsVar or HsUnboundVra
+-- An unbound name could be either HsVar or HsUnboundVar
 -- See RnExpr.rnUnboundVar
-get_op (L _ (HsVar n))          = n
-get_op (L _ (HsUnboundVar occ)) = mkUnboundName (mkRdrUnqual occ)
+get_op (L _ (HsVar (L _ n)))    = n
+get_op (L _ (HsUnboundVar occ)) = mkUnboundName occ
 get_op other                    = pprPanic "get_op" (ppr other)
 
 -- Parser left-associates everything, but
@@ -924,7 +1284,7 @@ checkPrecMatch :: Name -> MatchGroup Name body -> RnM ()
   --   eg  a `op` b `C` c = ...
   -- See comments with rnExpr (OpApp ...) about "deriving"
 
-checkPrecMatch op (MG { mg_alts = ms })
+checkPrecMatch op (MG { mg_alts = L _ ms })
   = mapM_ check ms
   where
     check (L _ (Match _ (L l1 p1 : L l2 p2 :_) _ _))
@@ -1007,60 +1367,67 @@ ppr_opfix (op, fixity) = pp_op <+> brackets (ppr fixity)
      pp_op | op == negateName = ptext (sLit "prefix `-'")
            | otherwise        = quotes (ppr op)
 
-{-
-*********************************************************
+{- *****************************************************
 *                                                      *
-\subsection{Errors}
+                 Errors
 *                                                      *
-*********************************************************
--}
+***************************************************** -}
 
-warnUnusedForAlls :: SDoc -> LHsTyVarBndrs RdrName -> [RdrName] -> TcM ()
-warnUnusedForAlls in_doc bound mentioned_rdrs
-  = whenWOptM Opt_WarnUnusedMatches $
-    mapM_ add_warn bound_but_not_used
+badKindBndrs :: HsDocContext -> [Located RdrName] -> SDoc
+badKindBndrs doc kvs
+  = withHsDocContext doc $
+    hang (ptext (sLit "Unexpected kind variable") <> plural kvs
+                 <+> pprQuotedList kvs)
+       2 (ptext (sLit "Perhaps you intended to use PolyKinds"))
+
+badKindSigErr :: HsDocContext -> LHsType RdrName -> TcM ()
+badKindSigErr doc (L loc ty)
+  = setSrcSpan loc $ addErr $
+    withHsDocContext doc $
+    hang (ptext (sLit "Illegal kind signature:") <+> quotes (ppr ty))
+       2 (ptext (sLit "Perhaps you intended to use KindSignatures"))
+
+dataKindsErr :: RnTyKiWhat -> HsType RdrName -> SDoc
+dataKindsErr what thing
+  = hang (ptext (sLit "Illegal") <+> pp_what <> colon <+> quotes (ppr thing))
+       2 (ptext (sLit "Perhaps you intended to use DataKinds"))
   where
-    bound_names        = hsLTyVarLocNames bound
-    bound_but_not_used = filterOut ((`elem` mentioned_rdrs) . unLoc) bound_names
+    pp_what | isRnKindLevel what = ptext (sLit "kind")
+            | otherwise          = ptext (sLit "type")
 
-    add_warn (L loc tv)
-      = addWarnAt loc $
-        vcat [ ptext (sLit "Unused quantified type variable") <+> quotes (ppr tv)
-             , in_doc ]
+inTypeDoc :: HsType RdrName -> SDoc
+inTypeDoc ty = ptext (sLit "In the type") <+> quotes (ppr ty)
 
-warnContextQuantification :: SDoc -> [LHsTyVarBndr RdrName] -> TcM ()
-warnContextQuantification in_doc tvs
-  = whenWOptM Opt_WarnContextQuantification $
-    mapM_ add_warn tvs
+warnUnusedForAlls :: SDoc -> [LHsTyVarBndr Name] -> FreeVars -> TcM ()
+warnUnusedForAlls in_doc bound_names used_names
+  = whenWOptM Opt_WarnUnusedMatches $
+    mapM_ add_warn bound_names
   where
     add_warn (L loc tv)
-      = addWarnAt loc $
-        vcat [ ptext (sLit "Variable") <+> quotes (ppr tv) <+>
-               ptext (sLit "is implicitly quantified due to a context") $$
-               ptext (sLit "Use explicit forall syntax instead.") $$
-               ptext (sLit "This will become an error in GHC 7.12.")
+      = unless (hsTyVarName tv `elemNameSet` used_names) $
+        addWarnAt loc $
+        vcat [ ptext (sLit "Unused quantified type variable") <+> quotes (ppr tv)
              , in_doc ]
 
-opTyErr :: RdrName -> HsType RdrName -> SDoc
-opTyErr op ty@(HsOpTy ty1 _ _)
-  = hang (ptext (sLit "Illegal operator") <+> quotes (ppr op) <+> ptext (sLit "in type") <+> quotes (ppr ty))
+opTyErr :: Outputable a => RdrName -> a -> SDoc
+opTyErr op overall_ty
+  = hang (ptext (sLit "Illegal operator") <+> quotes (ppr op) <+> ptext (sLit "in type") <+> quotes (ppr overall_ty))
          2 extra
   where
-    extra | op == dot_tv_RDR && forall_head ty1
+    extra | op == dot_tv_RDR
           = perhapsForallMsg
           | otherwise
           = ptext (sLit "Use TypeOperators to allow operators in types")
 
-    forall_head (L _ (HsTyVar tv))   = tv == forall_tv_RDR
-    forall_head (L _ (HsAppTy ty _)) = forall_head ty
-    forall_head _other               = False
-opTyErr _ ty = pprPanic "opTyErr: Not an op" (ppr ty)
+emptyNonSymsErr :: HsType RdrName -> SDoc
+emptyNonSymsErr overall_ty
+  = text "Operator applied to too few arguments:" <+> ppr overall_ty
 
 {-
 ************************************************************************
 *                                                                      *
       Finding the free type variables of a (HsType RdrName)
-*                                                                    *
+*                                                                      *
 ************************************************************************
 
 
@@ -1093,113 +1460,228 @@ Hence we returns a pair (kind-vars, type vars)
 See also Note [HsBSig binder lists] in HsTypes
 -}
 
-type FreeKiTyVars = ([RdrName], [RdrName])
+data FreeKiTyVars = FKTV { fktv_kis    :: [Located RdrName]
+                         , _fktv_k_set :: OccSet  -- for efficiency,
+                                                  -- only used internally
+                         , fktv_tys    :: [Located RdrName]
+                         , _fktv_t_set :: OccSet
+                         , fktv_all    :: [Located RdrName] }
+
+instance Outputable FreeKiTyVars where
+  ppr (FKTV kis _ tys _ _) = ppr (kis, tys)
+
+emptyFKTV :: FreeKiTyVars
+emptyFKTV = FKTV [] emptyOccSet [] emptyOccSet []
+
+freeKiTyVarsAllVars :: FreeKiTyVars -> [Located RdrName]
+freeKiTyVarsAllVars = fktv_all
+
+freeKiTyVarsKindVars :: FreeKiTyVars -> [Located RdrName]
+freeKiTyVarsKindVars = fktv_kis
+
+freeKiTyVarsTypeVars :: FreeKiTyVars -> [Located RdrName]
+freeKiTyVarsTypeVars = fktv_tys
 
 filterInScope :: LocalRdrEnv -> FreeKiTyVars -> FreeKiTyVars
-filterInScope rdr_env (kvs, tvs)
-  = (filterOut in_scope kvs, filterOut in_scope tvs)
+filterInScope rdr_env (FKTV kis k_set tys t_set all)
+  = FKTV (filterOut in_scope kis)
+         (filterOccSet (not . in_scope_occ) k_set)
+         (filterOut in_scope tys)
+         (filterOccSet (not . in_scope_occ) t_set)
+         (filterOut in_scope all)
   where
-    in_scope tv = tv `elemLocalRdrEnv` rdr_env
+    in_scope         = inScope rdr_env . unLoc
+    in_scope_occ occ = isJust $ lookupLocalRdrOcc rdr_env occ
 
-extractHsTyRdrTyVars :: LHsType RdrName -> FreeKiTyVars
+inScope :: LocalRdrEnv -> RdrName -> Bool
+inScope rdr_env rdr = rdr `elemLocalRdrEnv` rdr_env
+
+extractHsTyRdrTyVars :: LHsType RdrName -> RnM FreeKiTyVars
 -- extractHsTyRdrNames finds the free (kind, type) variables of a HsType
 --                        or the free (sort, kind) variables of a HsKind
 -- It's used when making the for-alls explicit.
+-- Does not return any wildcards
+-- When the same name occurs multiple times in the types, only the first
+-- occurence is returned.
 -- See Note [Kind and type-variable binders]
 extractHsTyRdrTyVars ty
-  = case extract_lty ty ([],[]) of
-     (kvs, tvs) -> (nub kvs, nub tvs)
-
-extractHsTysRdrTyVars :: [LHsType RdrName] -> FreeKiTyVars
+  = do { FKTV kis k_set tys t_set all <- extract_lty TypeLevel ty emptyFKTV
+       ; return (FKTV (nubL kis) k_set
+                      (nubL tys) t_set
+                      (nubL all)) }
+
+-- | Extracts free type and kind variables from types in a list.
+-- When the same name occurs multiple times in the types, only the first
+-- occurence is returned and the rest is filtered out.
 -- See Note [Kind and type-variable binders]
-extractHsTysRdrTyVars ty
-  = case extract_ltys ty ([],[]) of
-     (kvs, tvs) -> (nub kvs, nub tvs)
-
-extractRdrKindSigVars :: Maybe (LHsKind RdrName) -> [RdrName]
-extractRdrKindSigVars Nothing = []
-extractRdrKindSigVars (Just k) = nub (fst (extract_lkind k ([],[])))
-
-extractDataDefnKindVars :: HsDataDefn RdrName -> [RdrName]
+extractHsTysRdrTyVars :: [LHsType RdrName] -> RnM FreeKiTyVars
+extractHsTysRdrTyVars tys
+  = rmDupsInRdrTyVars <$> extractHsTysRdrTyVarsDups tys
+
+-- | Extracts free type and kind variables from types in a list.
+-- When the same name occurs multiple times in the types, all occurences
+-- are returned.
+extractHsTysRdrTyVarsDups :: [LHsType RdrName] -> RnM FreeKiTyVars
+extractHsTysRdrTyVarsDups tys
+  = extract_ltys TypeLevel tys emptyFKTV
+
+-- | Removes multiple occurences of the same name from FreeKiTyVars.
+rmDupsInRdrTyVars :: FreeKiTyVars -> FreeKiTyVars
+rmDupsInRdrTyVars (FKTV kis k_set tys t_set all)
+  = FKTV (nubL kis) k_set (nubL tys) t_set (nubL all)
+
+extractRdrKindSigVars :: LFamilyResultSig RdrName -> RnM [Located RdrName]
+extractRdrKindSigVars (L _ resultSig)
+    | KindSig k                        <- resultSig = kindRdrNameFromSig k
+    | TyVarSig (L _ (KindedTyVar _ k)) <- resultSig = kindRdrNameFromSig k
+    | otherwise = return []
+    where kindRdrNameFromSig k = freeKiTyVarsAllVars <$> extractHsTyRdrTyVars k
+
+extractDataDefnKindVars :: HsDataDefn RdrName -> RnM [Located RdrName]
 -- Get the scoped kind variables mentioned free in the constructor decls
 -- Eg    data T a = T1 (S (a :: k) | forall (b::k). T2 (S b)
 -- Here k should scope over the whole definition
 extractDataDefnKindVars (HsDataDefn { dd_ctxt = ctxt, dd_kindSig = ksig
                                     , dd_cons = cons, dd_derivs = derivs })
-  = fst $ extract_lctxt ctxt $
-          extract_mb extract_lkind ksig $
-          extract_mb (extract_ltys . unLoc) derivs $
-          foldr (extract_con . unLoc) ([],[]) cons
+  = (nubL . freeKiTyVarsKindVars) <$>
+    (extract_lctxt TypeLevel ctxt =<<
+     extract_mb extract_lkind ksig =<<
+     extract_mb (extract_sig_tys . unLoc) derivs =<<
+     foldrM (extract_con . unLoc) emptyFKTV cons)
   where
-    extract_con (ConDecl { con_res = ResTyGADT {} }) acc = acc
-    extract_con (ConDecl { con_res = ResTyH98, con_qvars = qvs
-                         , con_cxt = ctxt, con_details = details }) acc
-      = extract_hs_tv_bndrs qvs acc $
-        extract_lctxt ctxt $
-        extract_ltys (hsConDeclArgTys details) ([],[])
-
-
-extract_lctxt :: LHsContext RdrName -> FreeKiTyVars -> FreeKiTyVars
-extract_lctxt ctxt = extract_ltys (unLoc ctxt)
-
-extract_ltys :: [LHsType RdrName] -> FreeKiTyVars -> FreeKiTyVars
-extract_ltys tys acc = foldr extract_lty acc tys
-
-extract_mb :: (a -> FreeKiTyVars -> FreeKiTyVars) -> Maybe a -> FreeKiTyVars -> FreeKiTyVars
-extract_mb _ Nothing  acc = acc
+    extract_con (ConDeclGADT { }) acc = return acc
+    extract_con (ConDeclH98 { con_qvars = qvs
+                            , con_cxt = ctxt, con_details = details }) acc
+      = extract_hs_tv_bndrs (maybe [] hsQTvExplicit qvs) acc =<<
+        extract_mlctxt ctxt =<<
+        extract_ltys TypeLevel (hsConDeclArgTys details) emptyFKTV
+
+extract_mlctxt :: Maybe (LHsContext RdrName) -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_mlctxt Nothing     acc = return acc
+extract_mlctxt (Just ctxt) acc = extract_lctxt TypeLevel ctxt acc
+
+extract_lctxt :: TypeOrKind
+              -> LHsContext RdrName -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_lctxt t_or_k ctxt = extract_ltys t_or_k (unLoc ctxt)
+
+extract_sig_tys :: [LHsSigType RdrName] -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_sig_tys sig_tys acc
+  = foldrM (\sig_ty acc -> extract_lty TypeLevel (hsSigType sig_ty) acc)
+           acc sig_tys
+
+extract_ltys :: TypeOrKind
+             -> [LHsType RdrName] -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_ltys t_or_k tys acc = foldrM (extract_lty t_or_k) acc tys
+
+extract_mb :: (a -> FreeKiTyVars -> RnM FreeKiTyVars)
+           -> Maybe a -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_mb _ Nothing  acc = return acc
 extract_mb f (Just x) acc = f x acc
 
-extract_lkind :: LHsType RdrName -> FreeKiTyVars -> FreeKiTyVars
-extract_lkind kind (acc_kvs, acc_tvs) = case extract_lty kind ([], acc_kvs) of
-                                          (_, res_kvs) -> (res_kvs, acc_tvs)
-                                        -- Kinds shouldn't have sort signatures!
+extract_lkind :: LHsType RdrName -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_lkind = extract_lty KindLevel
 
-extract_lty :: LHsType RdrName -> FreeKiTyVars -> FreeKiTyVars
-extract_lty (L _ ty) acc
+extract_lty :: TypeOrKind -> LHsType RdrName -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_lty t_or_k (L _ ty) acc
   = case ty of
-      HsTyVar tv                -> extract_tv tv acc
-      HsBangTy _ ty             -> extract_lty ty acc
-      HsRecTy flds              -> foldr (extract_lty . cd_fld_type . unLoc) acc
+      HsTyVar ltv               -> extract_tv t_or_k ltv acc
+      HsBangTy _ ty             -> extract_lty t_or_k ty acc
+      HsRecTy flds              -> foldrM (extract_lty t_or_k
+                                           . cd_fld_type . unLoc) acc
                                          flds
-      HsAppTy ty1 ty2           -> extract_lty ty1 (extract_lty ty2 acc)
-      HsListTy ty               -> extract_lty ty acc
-      HsPArrTy ty               -> extract_lty ty acc
-      HsTupleTy _ tys           -> extract_ltys tys acc
-      HsFunTy ty1 ty2           -> extract_lty ty1 (extract_lty ty2 acc)
-      HsIParamTy _ ty           -> extract_lty ty acc
-      HsEqTy ty1 ty2            -> extract_lty ty1 (extract_lty ty2 acc)
-      HsOpTy ty1 (_, (L _ tv)) ty2 -> extract_tv tv (extract_lty ty1 (extract_lty ty2 acc))
-      HsParTy ty                -> extract_lty ty acc
-      HsCoreTy {}               -> acc  -- The type is closed
-      HsSpliceTy {}             -> acc  -- Type splices mention no type variables
-      HsDocTy ty _              -> extract_lty ty acc
-      HsExplicitListTy _ tys    -> extract_ltys tys acc
-      HsExplicitTupleTy _ tys   -> extract_ltys tys acc
-      HsTyLit _                 -> acc
-      HsWrapTy _ _              -> panic "extract_lty"
-      HsKindSig ty ki           -> extract_lty ty (extract_lkind ki acc)
-      HsForAllTy _ _ tvs cx ty  -> extract_hs_tv_bndrs tvs acc $
-                                   extract_lctxt cx   $
-                                   extract_lty ty ([],[])
+      HsAppsTy tys              -> extract_apps t_or_k tys acc
+      HsAppTy ty1 ty2           -> extract_lty t_or_k ty1 =<<
+                                   extract_lty t_or_k ty2 acc
+      HsListTy ty               -> extract_lty t_or_k ty acc
+      HsPArrTy ty               -> extract_lty t_or_k ty acc
+      HsTupleTy _ tys           -> extract_ltys t_or_k tys acc
+      HsFunTy ty1 ty2           -> extract_lty t_or_k ty1 =<<
+                                   extract_lty t_or_k ty2 acc
+      HsIParamTy _ ty           -> extract_lty t_or_k ty acc
+      HsEqTy ty1 ty2            -> extract_lty t_or_k ty1 =<<
+                                   extract_lty t_or_k ty2 acc
+      HsOpTy ty1 tv ty2         -> extract_tv t_or_k tv =<<
+                                   extract_lty t_or_k ty1 =<<
+                                   extract_lty t_or_k ty2 acc
+      HsParTy ty                -> extract_lty t_or_k ty acc
+      HsCoreTy {}               -> return acc  -- The type is closed
+      HsSpliceTy {}             -> return acc  -- Type splices mention no tvs
+      HsDocTy ty _              -> extract_lty t_or_k ty acc
+      HsExplicitListTy _ tys    -> extract_ltys t_or_k tys acc
+      HsExplicitTupleTy _ tys   -> extract_ltys t_or_k tys acc
+      HsTyLit _                 -> return acc
+      HsKindSig ty ki           -> extract_lty t_or_k ty =<<
+                                   extract_lkind ki acc
+      HsForAllTy { hst_bndrs = tvs, hst_body = ty }
+                                -> extract_hs_tv_bndrs tvs acc =<<
+                                   extract_lty t_or_k ty emptyFKTV
+      HsQualTy { hst_ctxt = ctxt, hst_body = ty }
+                                -> extract_lctxt t_or_k ctxt   =<<
+                                   extract_lty t_or_k ty acc
       -- We deal with these separately in rnLHsTypeWithWildCards
-      HsWildCardTy _            -> acc
-
-extract_hs_tv_bndrs :: LHsTyVarBndrs RdrName -> FreeKiTyVars
-                    -> FreeKiTyVars -> FreeKiTyVars
-extract_hs_tv_bndrs (HsQTvs { hsq_tvs = tvs })
-                    (acc_kvs, acc_tvs)   -- Note accumulator comes first
-                    (body_kvs, body_tvs)
+      HsWildCardTy {}           -> return acc
+
+extract_apps :: TypeOrKind
+             -> [HsAppType RdrName] -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_apps t_or_k tys acc = foldrM (extract_app t_or_k) acc tys
+
+extract_app :: TypeOrKind -> HsAppType RdrName -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_app t_or_k (HsAppInfix tv)  acc = extract_tv t_or_k tv acc
+extract_app t_or_k (HsAppPrefix ty) acc = extract_lty t_or_k ty acc
+
+extract_hs_tv_bndrs :: [LHsTyVarBndr RdrName] -> FreeKiTyVars
+                    -> FreeKiTyVars -> RnM FreeKiTyVars
+-- In (forall (a :: Maybe e). a -> b) we have
+--     'a' is bound by the forall
+--     'b' is a free type variable
+--     'e' is a free kind variable
+extract_hs_tv_bndrs tvs
+                    (FKTV acc_kvs acc_k_set acc_tvs acc_t_set acc_all)
+                           -- Note accumulator comes first
+                    (FKTV body_kvs body_k_set body_tvs body_t_set body_all)
   | null tvs
-  = (body_kvs ++ acc_kvs, body_tvs ++ acc_tvs)
+  = return $
+    FKTV (body_kvs ++ acc_kvs) (body_k_set `unionOccSets` acc_k_set)
+         (body_tvs ++ acc_tvs) (body_t_set `unionOccSets` acc_t_set)
+         (body_all ++ acc_all)
   | otherwise
-  = (acc_kvs ++ filterOut (`elem` local_kvs) body_kvs,
-     acc_tvs ++ filterOut (`elem` local_tvs) body_tvs)
+  = do { FKTV bndr_kvs bndr_k_set _ _ _
+           <- foldrM extract_lkind emptyFKTV [k | L _ (KindedTyVar _ k) <- tvs]
+
+       ; let locals = mkOccSet $ map (rdrNameOcc . hsLTyVarName) tvs
+       ; return $
+         FKTV (filterOut ((`elemOccSet` locals) . rdrNameOcc . unLoc) (bndr_kvs ++ body_kvs) ++ acc_kvs)
+              ((body_k_set `minusOccSet` locals) `unionOccSets` acc_k_set `unionOccSets` bndr_k_set)
+              (filterOut ((`elemOccSet` locals) . rdrNameOcc . unLoc) body_tvs ++ acc_tvs)
+              ((body_t_set `minusOccSet` locals) `unionOccSets` acc_t_set)
+              (filterOut ((`elemOccSet` locals) . rdrNameOcc . unLoc) (bndr_kvs ++ body_all) ++ acc_all) }
+
+extract_tv :: TypeOrKind -> Located RdrName -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_tv t_or_k ltv@(L _ tv) acc
+  | isRdrTyVar tv = case acc of
+      FKTV kvs k_set tvs t_set all
+        |  isTypeLevel t_or_k
+        -> do { when (occ `elemOccSet` k_set) $
+                mixedVarsErr ltv
+              ; return (FKTV kvs k_set (ltv : tvs) (t_set `extendOccSet` occ)
+                             (ltv : all)) }
+        |  otherwise
+        -> do { when (occ `elemOccSet` t_set) $
+                mixedVarsErr ltv
+              ; return (FKTV (ltv : kvs) (k_set `extendOccSet` occ) tvs t_set
+                             (ltv : all)) }
+  | otherwise     = return acc
   where
-    local_tvs = map hsLTyVarName tvs
-    (_, local_kvs) = foldr extract_lty ([], []) [k | L _ (KindedTyVar _ k) <- tvs]
-       -- These kind variables are bound here if not bound further out
-
-extract_tv :: RdrName -> FreeKiTyVars -> FreeKiTyVars
-extract_tv tv acc
-  | isRdrTyVar tv = case acc of (kvs,tvs) -> (kvs, tv : tvs)
-  | otherwise     = acc
+    occ = rdrNameOcc tv
+
+mixedVarsErr :: Located RdrName -> RnM ()
+mixedVarsErr (L loc tv)
+  = do { typeintype <- xoptM LangExt.TypeInType
+       ; unless typeintype $
+         addErrAt loc $ text "Variable" <+> quotes (ppr tv) <+>
+                        text "used as both a kind and a type" $$
+                        text "Did you intend to use TypeInType?" }
+
+-- just used in this module; seemed convenient here
+nubL :: Eq a => [Located a] -> [Located a]
+nubL = nubBy eqLocated