Remove -dtrace-level
[ghc.git] / compiler / rename / RnTypes.hs
index 090ed64..56a0331 100644 (file)
@@ -4,27 +4,32 @@
 \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, rnLTyVar, collectWildCards,
+        rnHsKind, rnLHsKind,
+        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, rnLHsTyVarBndr,
-        extractHsTyRdrTyVars, extractHsTysRdrTyVars, extractTyVarBndrNames,
+        bindLHsTyVarBndr,
+        bindSigTyVarsFV, bindHsQTyVars, bindLRdrNames,
+        extractFilteredRdrTyVars,
+        extractHsTyRdrTyVars, extractHsTysRdrTyVars,
+        extractHsTysRdrTyVarsDups, rmDupsInRdrTyVars,
         extractRdrKindSigVars, extractDataDefnKindVars,
-        filterInScope
+        freeKiTyVarsAllVars, freeKiTyVarsKindVars, freeKiTyVarsTypeVars
   ) where
 
 import {-# SOURCE #-} RnSplice( rnSpliceType )
@@ -37,9 +42,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,13 +54,10 @@ import BasicTypes       ( compareFixity, funTyFixity, negateFixity,
 import Outputable
 import FastString
 import Maybes
-import Data.List        ( nub, nubBy, deleteFirstsBy )
-import qualified Data.Set as Set
-import Control.Monad    ( unless, when )
+import qualified GHC.LanguageExtensions as LangExt
 
-#if __GLASGOW_HASKELL__ < 709
-import Data.Monoid      ( mappend, mempty, mconcat )
-#endif
+import Data.List        ( (\\), nubBy, partition )
+import Control.Monad    ( unless, when )
 
 #include "HsVersions.h"
 
@@ -62,32 +66,238 @@ 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
+-- type signatures on binders only allowed with ScopedTypeVariables
+rnHsSigWcTypeScoped ctx sig_ty thing_inside
+  = do { ty_sig_okay <- xoptM LangExt.ScopedTypeVariables
+       ; checkErr ty_sig_okay (unexpectedTypeSigErr sig_ty)
+       ; 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 variables 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
+                  (HsWC { hswc_body = HsIB { hsib_body = hs_ty }})
+                  thing_inside
+  = do { free_vars <- extractFilteredRdrTyVars hs_ty
+       ; (tv_rdrs, nwc_rdrs) <- partition_nwcs free_vars
+       ; rnImplicitBndrs no_implicit_if_forall tv_rdrs hs_ty $ \ vars ->
+    do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
+       ; let sig_ty' = HsWC { hswc_wcs = wcs, hswc_body = ib_ty' }
+             ib_ty'  = HsIB { hsib_vars = vars, hsib_body = hs_ty' }
+       ; (res, fvs2) <- thing_inside sig_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) }
+rnHsWcType :: HsDocContext -> LHsWcType RdrName -> RnM (LHsWcType Name, FreeVars)
+rnHsWcType ctxt (HsWC { hswc_body = hs_ty })
+  = do { free_vars <- extractFilteredRdrTyVars hs_ty
+       ; (_, nwc_rdrs) <- partition_nwcs free_vars
+       ; (wcs, hs_ty', fvs) <- rnWcBody ctxt nwc_rdrs hs_ty
+       ; let sig_ty' = HsWC { hswc_wcs = wcs, hswc_body = hs_ty' }
+       ; return (sig_ty', fvs) }
+
+rnWcBody :: HsDocContext -> [Located RdrName] -> LHsType RdrName
+         -> RnM ([Name], LHsType Name, FreeVars)
+rnWcBody ctxt nwc_rdrs hs_ty
+  = do { nwcs <- mapM newLocalBndrRn nwc_rdrs
+       ; let env = RTKE { rtke_level = TypeLevel
+                        , rtke_what  = RnTypeBody
+                        , rtke_nwcs  = mkNameSet nwcs
+                        , rtke_ctxt  = ctxt }
+       ; (hs_ty', fvs) <- bindLocalNamesFV nwcs $
+                          rn_lty env hs_ty
+       ; let awcs = collectAnonWildCards hs_ty'
+       ; return (nwcs ++ awcs, hs_ty', fvs) }
+  where
+    rn_lty env (L loc hs_ty)
+      = setSrcSpan loc $
+        do { (hs_ty', fvs) <- rn_ty env hs_ty
+           ; return (L loc hs_ty', fvs) }
+
+    rn_ty :: RnTyKiEnv -> HsType RdrName -> RnM (HsType Name, FreeVars)
+    -- A lot of faff just to allow the extra-constraints wildcard to appear
+    rn_ty env hs_ty@(HsForAllTy { hst_bndrs = tvs, hst_body = hs_body })
+      = bindLHsTyVarBndrs (rtke_ctxt env) (Just $ inTypeDoc hs_ty)
+                           Nothing [] tvs $ \ _ tvs' _ _ ->
+        do { (hs_body', fvs) <- rn_lty env hs_body
+           ; return (HsForAllTy { hst_bndrs = tvs', hst_body = hs_body' }, fvs) }
+
+    rn_ty env (HsQualTy { hst_ctxt = L cx hs_ctxt, hst_body = hs_ty })
+      | Just (hs_ctxt1, hs_ctxt_last) <- snocView hs_ctxt
+      , L lx (HsWildCardTy wc) <- ignoreParens hs_ctxt_last
+      = do { (hs_ctxt1', fvs1) <- mapFvRn (rn_top_constraint env) hs_ctxt1
+           ; wc' <- setSrcSpan lx $
+                    do { checkExtraConstraintWildCard env wc
+                       ; rnAnonWildCard wc }
+           ; let hs_ctxt' = hs_ctxt1' ++ [L lx (HsWildCardTy wc')]
+           ; (hs_ty', fvs2) <- rnLHsTyKi env hs_ty
+           ; return (HsQualTy { hst_ctxt = L cx hs_ctxt', hst_body = hs_ty' }
+                    , fvs1 `plusFV` fvs2) }
+
+      | otherwise
+      = do { (hs_ctxt', fvs1) <- mapFvRn (rn_top_constraint env) hs_ctxt
+           ; (hs_ty', fvs2)   <- rnLHsTyKi env hs_ty
+           ; return (HsQualTy { hst_ctxt = L cx hs_ctxt', hst_body = hs_ty' }
+                    , fvs1 `plusFV` fvs2) }
+
+    rn_ty env hs_ty = rnHsTyKi env hs_ty
+
+    rn_top_constraint env = rnLHsTyKi (env { rtke_what = RnTopConstraint })
+
+
+checkExtraConstraintWildCard :: RnTyKiEnv -> HsWildCardInfo RdrName
+                             -> RnM ()
+-- 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
+checkExtraConstraintWildCard env wc
+  = checkWildCard env mb_bad
   where
-    good_inst_ty
-      | Just (_, _, L _ cls, _) <-
-                        splitLHsInstDeclTy_maybe (flattenTopLevelLHsForAllTy ty)
-      , isTcOcc (rdrNameOcc cls) = True
-      | otherwise                = False
+    mb_bad | not (extraConstraintWildCardsAllowed env)
+           = Just (text "Extra-constraint wildcard" <+> quotes (ppr wc)
+                   <+> text "not allowed")
+           | otherwise
+           = Nothing
+
+extraConstraintWildCardsAllowed :: RnTyKiEnv -> Bool
+extraConstraintWildCardsAllowed env
+  = case rtke_ctxt env of
+      TypeSigCtx {}       -> True
+      ExprWithTySigCtx {} -> True
+      _                   -> False
+
+-- | Finds free type and kind variables in a type,
+--     without duplicates, and
+--     without variables that are already in scope in LocalRdrEnv
+--   NB: this includes named wildcards, which look like perfectly
+--       ordinary type variables at this point
+extractFilteredRdrTyVars :: LHsType RdrName -> RnM FreeKiTyVars
+extractFilteredRdrTyVars hs_ty
+  = do { rdr_env <- getLocalRdrEnv
+       ; filterInScope rdr_env <$> extractHsTyRdrTyVars hs_ty }
+
+-- | When the NamedWildCards extension is enabled, partition_nwcs
+-- 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) | wildcards_enabled = partition is_wildcard tys
+                             | otherwise         = ([], tys)
+             free_vars' = free_vars { fktv_tys = no_nwcs
+                                    , fktv_all = all \\ nwcs }
+       ; return (free_vars', nwcs) }
+  where
+     is_wildcard :: Located RdrName -> Bool
+     is_wildcard rdr = startsWithUnderscore (rdrNameOcc (unLoc rdr))
+
+{- Note [Renaming named wild cards]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Identifiers starting with an underscore are always parsed as type variables.
+It is only here in the renamer that we give the special treatment.
+See Note [The wildcard story for types] in HsTypes.
+
+It's easy!  When we collect the implicitly bound type variables, ready
+to bring them into scope, and NamedWildCards is on, we partition the
+variables into the ones that start with an underscore (the named
+wildcards) and the rest. Then we just add them to the hswc_wcs field
+of the HsWildCardBndrs structure, and we are done.
 
-badInstTy :: LHsType RdrName -> SDoc
-badInstTy ty = ptext (sLit "Malformed instance:") <+> ppr ty
+
+*********************************************************
+*                                                       *
+           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 <- extractFilteredRdrTyVars 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 "rnSigType" (ppr hs_ty $$ ppr free_vars $$
+                                        ppr real_rdrs)
+
+       ; traceRn "" (text "rnSigType2" <+> 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 <+> text "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)) $
+         text "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
@@ -109,300 +319,478 @@ 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 [QualTy in kinds]
+~~~~~~~~~~~~~~~~~~~~~~
+I was wondering whether QualTy could occur only at TypeLevel.  But no,
+we can have a qualified type in a kind too. Here is an example:
+
+  type family F a where
+    F Bool = Nat
+    F Nat  = Type
+
+  type family G a where
+    G Type = Type -> Type
+    G ()   = Nat
+
+  data X :: forall k1 k2. (F k1 ~ G k2) => k1 -> k2 -> Type where
+    MkX :: X 'True '()
+
+See that k1 becomes Bool and k2 becomes (), so the equality is
+satisfied. If I write MkX :: X 'True 'False, compilation fails with a
+suitable message:
+
+  MkX :: X 'True '()
+    • Couldn't match kind ‘G Bool’ with ‘Nat’
+      Expected kind: G Bool
+        Actual kind: F Bool
+
+However: in a kind, the constraints in the QualTy must all be
+equalities; or at least, any kinds with a class constraint are
+uninhabited.
 -}
 
-rnLHsTyKi  :: Bool --  True <=> renaming a type, False <=> a kind
-           -> HsDocContext -> LHsType RdrName -> RnM (LHsType Name, FreeVars)
-rnLHsTyKi isType doc (L loc ty)
-  = setSrcSpan loc $
-    do { (ty', fvs) <- rnHsTyKi isType doc ty
-       ; return (L loc ty', fvs) }
+data RnTyKiEnv
+  = RTKE { rtke_ctxt  :: HsDocContext
+         , rtke_level :: TypeOrKind  -- Am I renaming a type or a kind?
+         , rtke_what  :: RnTyKiWhat  -- And within that what am I renaming?
+         , rtke_nwcs  :: NameSet     -- These are the in-scope named wildcards
+    }
+
+data RnTyKiWhat = RnTypeBody
+                | RnTopConstraint   -- Top-level context of HsSigWcTypes
+                | RnConstraint      -- All other constraints
+
+instance Outputable RnTyKiEnv where
+  ppr (RTKE { rtke_level = lev, rtke_what = what
+            , rtke_nwcs = wcs, rtke_ctxt = ctxt })
+    = text "RTKE"
+      <+> braces (sep [ ppr lev, ppr what, ppr wcs
+                      , pprHsDocContext ctxt ])
+
+instance Outputable RnTyKiWhat where
+  ppr RnTypeBody      = text "RnTypeBody"
+  ppr RnTopConstraint = text "RnTopConstraint"
+  ppr RnConstraint    = text "RnConstraint"
+
+mkTyKiEnv :: HsDocContext -> TypeOrKind -> RnTyKiWhat -> RnTyKiEnv
+mkTyKiEnv cxt level what
+ = RTKE { rtke_level = level, rtke_nwcs = emptyNameSet
+        , rtke_what = what, rtke_ctxt = cxt }
+
+isRnKindLevel :: RnTyKiEnv -> Bool
+isRnKindLevel (RTKE { rtke_level = KindLevel }) = True
+isRnKindLevel _                                 = False
 
+--------------
 rnLHsType  :: HsDocContext -> LHsType RdrName -> RnM (LHsType Name, FreeVars)
-rnLHsType = rnLHsTyKi True
+rnLHsType ctxt ty = rnLHsTyKi (mkTyKiEnv ctxt TypeLevel RnTypeBody) ty
 
-rnLHsKind  :: HsDocContext -> LHsKind RdrName -> RnM (LHsKind Name, FreeVars)
-rnLHsKind = rnLHsTyKi False
-
-rnLHsMaybeKind  :: HsDocContext -> Maybe (LHsKind RdrName)
-                -> RnM (Maybe (LHsKind Name), FreeVars)
-rnLHsMaybeKind _ Nothing
-  = return (Nothing, emptyFVs)
-rnLHsMaybeKind doc (Just kind)
-  = do { (kind', fvs) <- rnLHsKind doc kind
-       ; return (Just kind', fvs) }
+rnLHsTypes :: HsDocContext -> [LHsType RdrName] -> RnM ([LHsType Name], FreeVars)
+rnLHsTypes doc tys = mapFvRn (rnLHsType doc) tys
 
 rnHsType  :: HsDocContext -> HsType RdrName -> RnM (HsType Name, FreeVars)
-rnHsType = rnHsTyKi True
+rnHsType ctxt ty = rnHsTyKi (mkTyKiEnv ctxt TypeLevel RnTypeBody) ty
+
+rnLHsKind  :: HsDocContext -> LHsKind RdrName -> RnM (LHsKind Name, FreeVars)
+rnLHsKind ctxt kind = rnLHsTyKi (mkTyKiEnv ctxt KindLevel RnTypeBody) kind
+
 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 ctxt kind = rnHsTyKi  (mkTyKiEnv ctxt KindLevel RnTypeBody) kind
+
+--------------
+rnTyKiContext :: RnTyKiEnv -> LHsContext RdrName -> RnM (LHsContext Name, FreeVars)
+rnTyKiContext env (L loc cxt)
+  = do { traceRn "rncontext" (ppr cxt)
+       ; let env' = env { rtke_what = RnConstraint }
+       ; (cxt', fvs) <- mapFvRn (rnLHsTyKi env') cxt
+       ; return (L loc cxt', fvs) }
+
+rnContext :: HsDocContext -> LHsContext RdrName -> RnM (LHsContext Name, FreeVars)
+rnContext doc theta = rnTyKiContext (mkTyKiEnv doc TypeLevel RnConstraint) theta
+
+--------------
+rnLHsTyKi  :: RnTyKiEnv -> LHsType RdrName -> RnM (LHsType Name, FreeVars)
+rnLHsTyKi env (L loc ty)
+  = setSrcSpan loc $
+    do { (ty', fvs) <- rnHsTyKi env ty
+       ; return (L loc ty', fvs) }
+
+rnHsTyKi :: RnTyKiEnv -> HsType RdrName -> RnM (HsType Name, FreeVars)
+
+rnHsTyKi env ty@(HsForAllTy { hst_bndrs = tyvars, hst_body  = tau })
+  = do { checkTypeInType env ty
+       ; bindLHsTyVarBndrs (rtke_ctxt env) (Just $ inTypeDoc ty)
+                           Nothing [] tyvars $ \ _ tyvars' _ _ ->
+    do { (tau',  fvs) <- rnLHsTyKi env tau
+       ; return ( HsForAllTy { hst_bndrs = tyvars', hst_body =  tau' }
+                , fvs) } }
+
+rnHsTyKi env ty@(HsQualTy { hst_ctxt = lctxt, hst_body = tau })
+  = do { checkTypeInType env ty  -- See Note [QualTy in kinds]
+       ; (ctxt', fvs1) <- rnTyKiContext env lctxt
+       ; (tau',  fvs2) <- rnLHsTyKi env tau
+       ; return (HsQualTy { hst_ctxt = ctxt', hst_body =  tau' }
+                , fvs1 `plusFV` fvs2) }
+
+rnHsTyKi env (HsTyVar (L loc rdr_name))
+  = do { name <- rnTyVar env rdr_name
+       ; return (HsTyVar (L loc name), unitFV name) }
+
+rnHsTyKi env ty@(HsOpTy ty1 l_op ty2)
+  = setSrcSpan (getLoc l_op) $
+    do  { (l_op', fvs1) <- rnHsTyOp env ty l_op
+        ; fix   <- lookupTyFixityRn l_op'
+        ; (ty1', fvs2) <- rnLHsTyKi env ty1
+        ; (ty2', fvs3) <- rnLHsTyKi env 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 env (HsParTy ty)
+  = do { (ty', fvs) <- rnLHsTyKi env ty
        ; return (HsParTy ty', fvs) }
 
-rnHsTyKi isType doc (HsBangTy b ty)
-  = ASSERT( isType )
-    do { (ty', fvs) <- rnLHsType doc ty
+rnHsTyKi env (HsBangTy b ty)
+  = do { (ty', fvs) <- rnLHsTyKi env ty
        ; return (HsBangTy b ty', fvs) }
 
-rnHsTyKi _ doc ty@(HsRecTy flds)
-  = do { addErr (hang (ptext (sLit "Record syntax is illegal here:"))
-                    2 (ppr ty))
-       ; (flds', fvs) <- rnConDeclFields doc flds
+rnHsTyKi env ty@(HsRecTy flds)
+  = do { let ctxt = rtke_ctxt env
+       ; fls          <- get_fields ctxt
+       ; (flds', fvs) <- rnConDeclFields ctxt fls flds
        ; return (HsRecTy flds', fvs) }
-
-rnHsTyKi isType doc (HsFunTy ty1 ty2)
-  = do { (ty1', fvs1) <- rnLHsTyKi isType doc ty1
+  where
+    get_fields (ConDeclCtx names)
+      = concatMapM (lookupConstructorFields . unLoc) names
+    get_fields _
+      = do { addErr (hang (text "Record syntax is illegal here:")
+                                   2 (ppr ty))
+           ; return [] }
+
+rnHsTyKi env (HsFunTy ty1 ty2)
+  = do { (ty1', fvs1) <- rnLHsTyKi env ty1
         -- Might find a for-all as the arg of a function type
-       ; (ty2', fvs2) <- rnLHsTyKi isType doc ty2
+       ; (ty2', fvs2) <- rnLHsTyKi env 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 env listTy@(HsListTy ty)
+  = do { data_kinds <- xoptM LangExt.DataKinds
+       ; when (not data_kinds && isRnKindLevel env)
+              (addErr (dataKindsErr env listTy))
+       ; (ty', fvs) <- rnLHsTyKi env 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
-       ; (k', fvs2) <- rnLHsKind doc k
+rnHsTyKi env t@(HsKindSig ty k)
+  = do { checkTypeInType env t
+       ; kind_sigs_ok <- xoptM LangExt.KindSignatures
+       ; unless kind_sigs_ok (badKindSigErr (rtke_ctxt env) ty)
+       ; (ty', fvs1) <- rnLHsTyKi env ty
+       ; (k', fvs2)  <- rnLHsTyKi (env { rtke_level = KindLevel }) k
        ; return (HsKindSig ty' k', fvs1 `plusFV` fvs2) }
 
-rnHsTyKi isType doc (HsPArrTy ty)
-  = ASSERT( isType )
-    do { (ty', fvs) <- rnLHsType doc ty
+rnHsTyKi env t@(HsPArrTy ty)
+  = do { notInKinds env t
+       ; (ty', fvs) <- rnLHsTyKi env 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 env tupleTy@(HsTupleTy tup_con tys)
+  = do { data_kinds <- xoptM LangExt.DataKinds
+       ; when (not data_kinds && isRnKindLevel env)
+              (addErr (dataKindsErr env tupleTy))
+       ; (tys', fvs) <- mapFvRn (rnLHsTyKi env) tys
        ; return (HsTupleTy tup_con tys', fvs) }
 
+rnHsTyKi env sumTy@(HsSumTy tys)
+  = do { data_kinds <- xoptM LangExt.DataKinds
+       ; when (not data_kinds && isRnKindLevel env)
+              (addErr (dataKindsErr env sumTy))
+       ; (tys', fvs) <- mapFvRn (rnLHsTyKi env) tys
+       ; return (HsSumTy 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 env tyLit@(HsTyLit t)
+  = do { data_kinds <- xoptM LangExt.DataKinds
+       ; unless data_kinds (addErr (dataKindsErr env tyLit))
        ; when (negLit t) (addErr negLitErr)
+       ; checkTypeInType env 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
+    negLitErr = text "Illegal literal in type (type literals must not be negative):" <+> ppr tyLit
+
+rnHsTyKi env 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 env overall_ty) syms
+       ; (non_syms1, fvs2)  <- (mapFvRn . mapFvRn) (rnLHsTyKi env) non_syms
+
+             -- Step 3: deal with *. See Note [Dealing with *]
+       ; let (non_syms2, syms2) = deal_with_star [] [] non_syms1 syms1
 
-rnHsTyKi isType doc (HsAppTy ty1 ty2)
-  = do { (ty1', fvs1) <- rnLHsTyKi isType doc ty1
-       ; (ty2', fvs2) <- rnLHsTyKi isType doc ty2
+             -- 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 env (HsAppTy ty1 ty2)
+  = do { (ty1', fvs1) <- rnLHsTyKi env ty1
+       ; (ty2', fvs2) <- rnLHsTyKi env ty2
        ; return (HsAppTy ty1' ty2', fvs1 `plusFV` fvs2) }
 
-rnHsTyKi isType doc (HsIParamTy n ty)
-  = ASSERT( isType )
-    do { (ty', fvs) <- rnLHsType doc ty
+rnHsTyKi env t@(HsIParamTy n ty)
+  = do { notInKinds env t
+       ; (ty', fvs) <- rnLHsTyKi env 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 env t@(HsEqTy ty1 ty2)
+  = do { checkTypeInType env t
+       ; (ty1', fvs1) <- rnLHsTyKi env ty1
+       ; (ty2', fvs2) <- rnLHsTyKi env 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 env (HsDocTy ty haddock_doc)
+  = do { (ty', fvs) <- rnLHsTyKi env 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 env ty@(HsExplicitListTy k tys)
+  = do { checkTypeInType env ty
+       ; data_kinds <- xoptM LangExt.DataKinds
+       ; unless data_kinds (addErr (dataKindsErr env ty))
+       ; (tys', fvs) <- mapFvRn (rnLHsTyKi env) 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 env ty@(HsExplicitTupleTy kis tys)
+  = do { checkTypeInType env ty
+       ; data_kinds <- xoptM LangExt.DataKinds
+       ; unless data_kinds (addErr (dataKindsErr env ty))
+       ; (tys', fvs) <- mapFvRn (rnLHsTyKi env) 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 env (HsWildCardTy wc)
+  = do { checkAnonWildCard env wc
+       ; wc' <- rnAnonWildCard wc
+       ; 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
 
 --------------
-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
-
-rnLTyVar :: Bool -> Located RdrName -> RnM (Located Name)
-rnLTyVar is_type (L loc rdr_name) = do
-  tyvar' <- rnTyVar is_type rdr_name
-  return (L loc tyvar')
+rnTyVar :: RnTyKiEnv -> RdrName -> RnM Name
+rnTyVar env rdr_name
+  = do { name <- if   isRnKindLevel env
+                 then lookupKindOccRn rdr_name
+                 else lookupTypeOccRn rdr_name
+       ; checkNamedWildCard env name
+       ; return name }
+
+rnLTyVar :: Located RdrName -> RnM (Located Name)
+-- Called externally; does not deal with wildards
+rnLTyVar (L loc rdr_name)
+  = do { tyvar <- lookupTypeOccRn rdr_name
+       ; return (L loc tyvar) }
 
 --------------
-rnLHsTypes :: HsDocContext -> [LHsType RdrName]
-           -> RnM ([LHsType Name], FreeVars)
-rnLHsTypes doc tys = mapFvRn (rnLHsType doc) tys
+rnHsTyOp :: Outputable a
+         => RnTyKiEnv -> a -> Located RdrName -> RnM (Located Name, FreeVars)
+rnHsTyOp env overall_ty (L loc op)
+  = do { ops_ok <- xoptM LangExt.TypeOperators
+       ; op' <- rnTyVar env 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') }
 
-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 *.
+--------------
+notAllowed :: SDoc -> SDoc
+notAllowed doc
+  = text "Wildcard" <+> quotes doc <+> ptext (sLit "not allowed")
+
+checkWildCard :: RnTyKiEnv -> Maybe SDoc -> RnM ()
+checkWildCard env (Just doc)
+  = addErr $ vcat [doc, nest 2 (text "in" <+> pprHsDocContext (rtke_ctxt env))]
+checkWildCard _ Nothing
+  = return ()
 
-  | 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
+checkAnonWildCard :: RnTyKiEnv -> HsWildCardInfo RdrName -> RnM ()
+-- Report an error if an anonymoous wildcard is illegal here
+checkAnonWildCard env wc
+  = checkWildCard env mb_bad
+  where
+    mb_bad :: Maybe SDoc
+    mb_bad | not (wildCardsAllowed env)
+           = Just (notAllowed (ppr wc))
+           | otherwise
+           = case rtke_what env of
+               RnTypeBody      -> Nothing
+               RnConstraint    -> Just constraint_msg
+               RnTopConstraint -> Just constraint_msg
+
+    constraint_msg = hang (notAllowed (ppr wc) <+> text "in a constraint")
+                        2 hint_msg
+    hint_msg = vcat [ text "except as the last top-level constraint of a type signature"
+                    , nest 2 (text "e.g  f :: (Eq a, _) => blah") ]
+
+checkNamedWildCard :: RnTyKiEnv -> Name -> RnM ()
+-- Report an error if a named wildcard is illegal here
+checkNamedWildCard env name
+  = checkWildCard env mb_bad
+  where
+    mb_bad | not (name `elemNameSet` rtke_nwcs env)
+           = Nothing  -- Not a wildcard
+           | not (wildCardsAllowed env)
+           = Just (notAllowed (ppr name))
+           | otherwise
+           = case rtke_what env of
+               RnTypeBody      -> Nothing   -- Allowed
+               RnTopConstraint -> Nothing   -- Allowed
+               RnConstraint    -> Just constraint_msg
+    constraint_msg = notAllowed (ppr name) <+> text "in a constraint"
+
+wildCardsAllowed :: RnTyKiEnv -> Bool
+-- ^ In what contexts are wildcards permitted
+wildCardsAllowed env
+   = case rtke_ctxt env 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
+       HsTypeCtx {}        -> True
+       _                   -> False
+
+rnAnonWildCard :: HsWildCardInfo RdrName -> RnM (HsWildCardInfo Name)
+rnAnonWildCard (AnonWildCard _)
+  = do { loc <- getSrcSpanM
+       ; uniq <- newUnique
+       ; let name = mkInternalName uniq (mkTyVarOcc "_") loc
+       ; return (AnonWildCard (L loc name)) }
 
 ---------------
+-- | Ensures either that we're in a type or that -XTypeInType is set
+checkTypeInType :: Outputable ty
+                => RnTyKiEnv
+                -> ty      -- ^ type
+                -> RnM ()
+checkTypeInType env ty
+  | isRnKindLevel env
+  = 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
+           => RnTyKiEnv
+           -> ty
+           -> RnM ()
+notInKinds env ty
+  | isRnKindLevel env
+  = addErr (text "Illegal kind (even with TypeInType enabled):" <+> ppr ty)
+notInKinds _ _ = return ()
+
+{- *****************************************************
+*                                                      *
+          Binding type variables
+*                                                      *
+***************************************************** -}
+
 bindSigTyVarsFV :: [Name]
                 -> RnM (a, FreeVars)
                 -> RnM (a, FreeVars)
@@ -410,324 +798,300 @@ 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 SDoc         -- if we are to check for unused tvs,
+                                    -- a phrase like "in the type ..."
+              -> 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 -> NameSet -> RnM (b, FreeVars))
+                  -- also returns all names used in kind signatures, for the
+                  -- TypeInType clause of Note [Complete user-supplied kind
+                  -- signatures] in HsDecls
+              -> 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
-  = 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
-
-       -- 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 (rnLHsTyVarBndr doc mb_assoc rdr_env) 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) } }
-
-rnLHsTyVarBndr :: HsDocContext -> Maybe a -> LocalRdrEnv
-               -> LHsTyVarBndr RdrName -> RnM (LHsTyVarBndr Name, FreeVars)
-rnLHsTyVarBndr _ mb_assoc rdr_env (L loc (UserTyVar rdr))
-  = do { nm <- newTyVarNameRn mb_assoc rdr_env loc rdr
-       ; return (L loc (UserTyVar nm), emptyFVs) }
-rnLHsTyVarBndr doc mb_assoc rdr_env (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) }
-
-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)
-       ; rdr_env <- getLocalRdrEnv
-       ; let (kv_bndrs, tv_bndrs) = filterInScope rdr_env $
-                                    extractHsTyRdrTyVars ty
-       ; kv_names <- newLocalBndrsRn (map (L loc) kv_bndrs)
-       ; tv_names <- newLocalBndrsRn (map (L loc) tv_bndrs)
-       ; 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) } }
-
-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 ]
-
-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 ]
-
-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 ]
+bindHsQTyVars doc mb_in_doc mb_assoc kv_bndrs tv_bndrs thing_inside
+  = do { bindLHsTyVarBndrs doc mb_in_doc
+                           mb_assoc kv_bndrs (hsQTvExplicit tv_bndrs) $
+         \ rn_kvs rn_bndrs dep_var_set all_dep_vars ->
+         thing_inside (HsQTvs { hsq_implicit = rn_kvs
+                              , hsq_explicit = rn_bndrs
+                              , hsq_dependent = dep_var_set }) all_dep_vars }
+
+bindLHsTyVarBndrs :: forall a b.
+                     HsDocContext
+                  -> Maybe SDoc         -- if we are to check for unused tvs,
+                                        -- a phrase like "in the type ..."
+                  -> 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]
+                      -> NameSet -- which names, from the preceding list,
+                                 -- are used dependently within that list
+                                 -- See Note [Dependent LHsQTyVars] in TcHsType
+                      -> NameSet -- all names used in kind signatures
+                      -> RnM (b, FreeVars))
+                  -> RnM (b, FreeVars)
+bindLHsTyVarBndrs doc mb_in_doc mb_assoc kv_bndrs tv_bndrs thing_inside
+  = do { when (isNothing mb_assoc) (checkShadowedRdrNames tv_names_w_loc)
+       ; go [] [] emptyNameSet emptyNameSet emptyNameSet tv_bndrs }
   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"))
+    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)
+       -> NameSet                -- (all) variables used dependently
+       -> [LHsTyVarBndr RdrName] -- still to be renamed, scoped
+       -> RnM (b, FreeVars)
+    go rn_kvs rn_tvs kv_names tv_names dep_vars (tv_bndr : tv_bndrs)
+      = bindLHsTyVarBndr doc mb_assoc kv_names tv_names tv_bndr $
+        \ kv_nms used_dependently tv_bndr' ->
+        do { (b, fvs) <- go (reverse kv_nms ++ rn_kvs)
+                            (tv_bndr' : rn_tvs)
+                            (kv_names `extendNameSetList` kv_nms)
+                            (tv_names `extendNameSet` hsLTyVarName tv_bndr')
+                            (dep_vars `unionNameSet` used_dependently)
+                            tv_bndrs
+           ; warn_unused tv_bndr' fvs
+           ; return (b, fvs) }
+
+    go rn_kvs rn_tvs _kv_names tv_names dep_vars []
+      = -- still need to deal with the kv_bndrs passed in originally
+        bindImplicitKvs doc mb_assoc kv_bndrs tv_names $ \ kv_nms others ->
+        do { let all_rn_kvs = reverse (reverse kv_nms ++ rn_kvs)
+                 all_rn_tvs = reverse rn_tvs
+           ; env <- getLocalRdrEnv
+           ; let all_dep_vars = dep_vars `unionNameSet` others
+                 exp_dep_vars -- variables in all_rn_tvs that are in dep_vars
+                   = mkNameSet [ name
+                               | v <- all_rn_tvs
+                               , let name = hsLTyVarName v
+                               , name `elemNameSet` all_dep_vars ]
+           ; traceRn "bindHsTyVars" (ppr env $$
+                                     ppr all_rn_kvs $$
+                                     ppr all_rn_tvs $$
+                                     ppr exp_dep_vars)
+           ; thing_inside all_rn_kvs all_rn_tvs exp_dep_vars all_dep_vars }
+
+    warn_unused tv_bndr fvs = case mb_in_doc of
+      Just in_doc -> warnUnusedForAll in_doc tv_bndr fvs
+      Nothing     -> return ()
+
+bindLHsTyVarBndr :: HsDocContext
+                 -> Maybe a   -- associated class
+                 -> NameSet   -- kind vars already in scope
+                 -> NameSet   -- type vars already in scope
+                 -> LHsTyVarBndr RdrName
+                 -> ([Name] -> NameSet -> LHsTyVarBndr Name -> RnM (b, FreeVars))
+                   -- passed the newly-bound implicitly-declared kind vars,
+                   -- any other names used in a kind
+                   -- 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 [] emptyNameSet (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 $
+             \ new_kv_nms other_kv_nms ->
+             do { (kind', fvs1) <- rnLHsKind doc kind
+                ; tv_nm  <- newTyVarNameRn mb_assoc lrdr
+                ; (b, fvs2) <- bindLocalNamesFV [tv_nm] $
+                               thing_inside new_kv_nms other_kv_nms
+                                 (L loc (KindedTyVar (L lv tv_nm) kind'))
+                ; return (b, fvs1 `plusFV` fvs2) }}
   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'
+      -- 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] -> NameSet -> RnM (b, FreeVars))
+                   -- ^ passed new kv_names, and any other names used in a kind
+                -> RnM (b, FreeVars)
+bindImplicitKvs _   _        []       _        thing_inside
+  = thing_inside [] emptyNameSet
+bindImplicitKvs doc mb_assoc free_kvs tv_names thing_inside
+  = do { rdr_env <- getLocalRdrEnv
+       ; 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 (mkNameSet (map unLoc bound_kvs)) }
   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)
+      -- 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
+
+           _                -> newLocalBndrRn (L loc rdr) }
+
+---------------------
+collectAnonWildCards :: LHsType Name -> [Name]
+-- | Extract all wild cards from a type.
+collectAnonWildCards lty = go lty
   where
-    (extra, wcs) = go lty
-    go (L loc ty) = case ty of
-      HsAppTy ty1 ty2         -> go ty1 `mappend` go ty2
-      HsFunTy ty1 ty2         -> go ty1 `mappend` go ty2
-      HsListTy ty             -> go ty
-      HsPArrTy ty             -> go ty
-      HsTupleTy _ tys         -> gos tys
-      HsOpTy ty1 _ ty2        -> go ty1 `mappend` go ty2
-      HsParTy ty              -> go ty
-      HsIParamTy _ ty         -> go ty
-      HsEqTy ty1 ty2          -> go ty1 `mappend` go ty2
-      HsKindSig ty kind       -> go ty `mappend` go kind
-      HsDocTy ty _            -> go ty
-      HsBangTy _ ty           -> go ty
-      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)
+    go (L _ ty) = case ty of
+      HsWildCardTy (AnonWildCard (L _ wc)) -> [wc]
+      HsAppsTy tys                 -> gos (mapMaybe (prefix_types_only . unLoc) tys)
+      HsAppTy ty1 ty2              -> go ty1 `mappend` go ty2
+      HsFunTy ty1 ty2              -> go ty1 `mappend` go ty2
+      HsListTy ty                  -> go ty
+      HsPArrTy ty                  -> go ty
+      HsTupleTy _ tys              -> gos tys
+      HsOpTy ty1 _ ty2             -> go ty1 `mappend` go ty2
+      HsParTy ty                   -> go ty
+      HsIParamTy _ ty              -> go ty
+      HsEqTy ty1 ty2               -> go ty1 `mappend` go ty2
+      HsKindSig ty kind            -> go ty `mappend` go kind
+      HsDocTy ty _                 -> go ty
+      HsBangTy _ ty                -> go ty
+      HsRecTy flds                 -> gos $ map (cd_fld_type . unLoc) flds
+      HsExplicitListTy _ tys       -> gos tys
+      HsExplicitTupleTy _ tys      -> gos tys
+      HsForAllTy { hst_bndrs = bndrs
+                 , hst_body = ty } -> collectAnonWildCardsBndrs bndrs
+                                      `mappend` go ty
+      HsQualTy { hst_ctxt = L _ ctxt
+               , hst_body = ty }  -> gos ctxt `mappend` go ty
+      HsSpliceTy (HsSpliced _ (HsSplicedTy ty)) _ -> go $ L noSrcSpan 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
 
+collectAnonWildCardsBndrs :: [LHsTyVarBndr Name] -> [Name]
+collectAnonWildCardsBndrs ltvs = concatMap (go . unLoc) ltvs
+  where
+    go (UserTyVar _)      = []
+    go (KindedTyVar _ ki) = collectAnonWildCards ki
 
 {-
 *********************************************************
-*                                                      *
-\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 :: HsDocContext -> [FieldLabel] -> [LConDeclField RdrName]
                 -> RnM ([LConDeclField Name], FreeVars)
-rnConDeclFields doc fields = mapFvRn (rnField doc) fields
+-- Also called from RnSource
+-- No wildcards can appear in record fields
+rnConDeclFields ctxt fls fields
+   = mapFvRn (rnField fl_env env) fields
+  where
+    env    = mkTyKiEnv ctxt TypeLevel RnTypeBody
+    fl_env = mkFsEnv [ (flLabel fl, fl) | fl <- fls ]
 
-rnField :: HsDocContext -> LConDeclField RdrName
+rnField :: FastStringEnv FieldLabel -> RnTyKiEnv -> LConDeclField RdrName
         -> RnM (LConDeclField Name, FreeVars)
-rnField doc (L l (ConDeclField names ty haddock_doc))
-  = do { new_names <- mapM lookupLocatedTopBndrRn names
-       ; (new_ty, fvs) <- rnLHsType doc ty
+rnField fl_env env (L l (ConDeclField names ty haddock_doc))
+  = do { let new_names = map (fmap lookupField) names
+       ; (new_ty, fvs) <- rnLHsTyKi env ty
        ; new_haddock_doc <- rnMbLHsDoc haddock_doc
        ; return (L l (ConDeclField new_names new_ty new_haddock_doc), fvs) }
-
-rnContext :: HsDocContext -> LHsContext RdrName -> RnM (LHsContext Name, FreeVars)
-rnContext doc (L loc cxt)
-  = do { (cxt', fvs) <- rnLHsTypes doc cxt
-       ; return (L loc cxt', 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
 
 {-
 ************************************************************************
@@ -761,10 +1125,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))
@@ -845,11 +1209,11 @@ 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 other                    = pprPanic "get_op" (ppr other)
+get_op (L _ (HsVar (L _ n)))   = n
+get_op (L _ (HsUnboundVar uv)) = mkUnboundName (unboundVarOcc uv)
+get_op other                   = pprPanic "get_op" (ppr other)
 
 -- Parser left-associates everything, but
 -- derived instances may have correctly-associated things to
@@ -931,7 +1295,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 :_) _ _))
@@ -950,8 +1314,8 @@ checkPrecMatch op (MG { mg_alts = ms })
 
 checkPrec :: Name -> Pat Name -> Bool -> IOEnv (Env TcGblEnv TcLclEnv) ()
 checkPrec op (ConPatIn op1 (InfixCon _ _)) right = do
-    op_fix@(Fixity op_prec  op_dir) <- lookupFixityRn op
-    op1_fix@(Fixity op1_prec op1_dir) <- lookupFixityRn (unLoc op1)
+    op_fix@(Fixity op_prec  op_dir) <- lookupFixityRn op
+    op1_fix@(Fixity op1_prec op1_dir) <- lookupFixityRn (unLoc op1)
     let
         inf_ok = op1_prec > op_prec ||
                  (op1_prec == op_prec &&
@@ -979,8 +1343,8 @@ checkSectionPrec direction section op arg
         _                -> return ()
   where
     op_name = get_op op
-    go_for_it arg_op arg_fix@(Fixity arg_prec assoc) = do
-          op_fix@(Fixity op_prec _) <- lookupFixityRn op_name
+    go_for_it arg_op arg_fix@(Fixity arg_prec assoc) = do
+          op_fix@(Fixity op_prec _) <- lookupFixityRn op_name
           unless (op_prec < arg_prec
                   || (op_prec == arg_prec && direction == assoc))
                  (sectionPrecErr (op_name, op_fix)
@@ -993,81 +1357,90 @@ precParseErr op1@(n1,_) op2@(n2,_)
   | isUnboundName n1 || isUnboundName n2
   = return ()     -- Avoid error cascade
   | otherwise
-  = addErr $ hang (ptext (sLit "Precedence parsing error"))
-      4 (hsep [ptext (sLit "cannot mix"), ppr_opfix op1, ptext (sLit "and"),
+  = addErr $ hang (text "Precedence parsing error")
+      4 (hsep [text "cannot mix", ppr_opfix op1, ptext (sLit "and"),
                ppr_opfix op2,
-               ptext (sLit "in the same infix expression")])
+               text "in the same infix expression"])
 
 sectionPrecErr :: (Name, Fixity) -> (Name, Fixity) -> HsExpr RdrName -> RnM ()
 sectionPrecErr op@(n1,_) arg_op@(n2,_) section
   | isUnboundName n1 || isUnboundName n2
   = return ()     -- Avoid error cascade
   | otherwise
-  = addErr $ vcat [ptext (sLit "The operator") <+> ppr_opfix op <+> ptext (sLit "of a section"),
-         nest 4 (sep [ptext (sLit "must have lower precedence than that of the operand,"),
-                      nest 2 (ptext (sLit "namely") <+> ppr_opfix arg_op)]),
-         nest 4 (ptext (sLit "in the section:") <+> quotes (ppr section))]
+  = addErr $ vcat [text "The operator" <+> ppr_opfix op <+> ptext (sLit "of a section"),
+         nest 4 (sep [text "must have lower precedence than that of the operand,",
+                      nest 2 (text "namely" <+> ppr_opfix arg_op)]),
+         nest 4 (text "in the section:" <+> quotes (ppr section))]
 
 ppr_opfix :: (Name, Fixity) -> SDoc
 ppr_opfix (op, fixity) = pp_op <+> brackets (ppr fixity)
    where
-     pp_op | op == negateName = ptext (sLit "prefix `-'")
+     pp_op | op == negateName = text "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
-  where
-    bound_names        = hsLTyVarLocNames bound
-    bound_but_not_used = filterOut ((`elem` mentioned_rdrs) . unLoc) bound_names
-
-    add_warn (L loc tv)
-      = addWarnAt loc $
-        vcat [ ptext (sLit "Unused quantified type variable") <+> quotes (ppr tv)
-             , in_doc ]
-
-warnContextQuantification :: SDoc -> [LHsTyVarBndr RdrName] -> TcM ()
-warnContextQuantification in_doc tvs
-  = whenWOptM Opt_WarnContextQuantification $
-    mapM_ add_warn tvs
+unexpectedTypeSigErr :: LHsSigWcType RdrName -> SDoc
+unexpectedTypeSigErr ty
+  = hang (text "Illegal type signature:" <+> quotes (ppr ty))
+       2 (text "Type signatures are only allowed in patterns with ScopedTypeVariables")
+
+badKindBndrs :: HsDocContext -> [Located RdrName] -> SDoc
+badKindBndrs doc kvs
+  = withHsDocContext doc $
+    hang (text "Unexpected kind variable" <> plural kvs
+                 <+> pprQuotedList kvs)
+       2 (text "Perhaps you intended to use PolyKinds")
+
+badKindSigErr :: HsDocContext -> LHsType RdrName -> TcM ()
+badKindSigErr doc (L loc ty)
+  = setSrcSpan loc $ addErr $
+    withHsDocContext doc $
+    hang (text "Illegal kind signature:" <+> quotes (ppr ty))
+       2 (text "Perhaps you intended to use KindSignatures")
+
+dataKindsErr :: RnTyKiEnv -> HsType RdrName -> SDoc
+dataKindsErr env thing
+  = hang (text "Illegal" <+> pp_what <> colon <+> quotes (ppr thing))
+       2 (text "Perhaps you intended to use DataKinds")
   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.")
-             , 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))
+    pp_what | isRnKindLevel env = text "kind"
+            | otherwise          = text "type"
+
+inTypeDoc :: HsType RdrName -> SDoc
+inTypeDoc ty = text "In the type" <+> quotes (ppr ty)
+
+warnUnusedForAll :: SDoc -> LHsTyVarBndr Name -> FreeVars -> TcM ()
+warnUnusedForAll in_doc (L loc tv) used_names
+  = whenWOptM Opt_WarnUnusedForalls $
+    unless (hsTyVarName tv `elemNameSet` used_names) $
+    addWarnAt (Reason Opt_WarnUnusedForalls) loc $
+    vcat [ text "Unused quantified type variable" <+> quotes (ppr tv)
+         , in_doc ]
+
+opTyErr :: Outputable a => RdrName -> a -> SDoc
+opTyErr op overall_ty
+  = hang (text "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")
+          = text "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)
-*                                                                    *
+*                                                                      *
 ************************************************************************
 
 
@@ -1100,129 +1473,230 @@ 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
+
+inScope :: LocalRdrEnv -> RdrName -> Bool
+inScope rdr_env rdr = rdr `elemLocalRdrEnv` rdr_env
 
-extractHsTyRdrTyVars :: LHsType RdrName -> FreeKiTyVars
+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)
-
--- Extracts variable names used in a type variable binder. Note that HsType
--- represents data and type constructors as type variables and so this function
--- will also return data and type constructors.
-extractTyVarBndrNames :: LHsTyVarBndr RdrName -> Set.Set RdrName
-extractTyVarBndrNames (L _ (UserTyVar name))
-  = Set.singleton name
-extractTyVarBndrNames (L _ (KindedTyVar (L _ name) k))
-  = Set.singleton name `Set.union` (Set.fromList tvs)
-                       `Set.union` (Set.fromList kvs)
-    where (kvs, tvs) = extractHsTyRdrTyVars k
-
-extractRdrKindSigVars :: LFamilyResultSig 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
-    | TyVarSig (L _ (UserTyVar _))     <- resultSig = []
-    | otherwise = [] -- this can only be NoSig but pattern exhasutiveness
-                     -- checker complains about "NoSig <- resultSig"
-    where kindRdrNameFromSig k = nub (fst (extract_lkind k ([],[])))
+    | otherwise = return []
+    where kindRdrNameFromSig k = freeKiTyVarsAllVars <$> extractHsTyRdrTyVars k
 
-extractDataDefnKindVars :: HsDataDefn RdrName -> [RdrName]
+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
+                                    , dd_cons = cons, dd_derivs = L _ derivs })
+  = (nubL . freeKiTyVarsKindVars) <$>
+    (extract_lctxt TypeLevel ctxt =<<
+     extract_mb extract_lkind ksig =<<
+     extract_sig_tys (concatMap (unLoc . deriv_clause_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
+      HsSumTy 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
+             -> [LHsAppType RdrName] -> FreeKiTyVars -> RnM FreeKiTyVars
+extract_apps t_or_k tys acc = foldrM (extract_app t_or_k) acc tys
+
+extract_app :: TypeOrKind -> LHsAppType RdrName -> FreeKiTyVars
+            -> RnM FreeKiTyVars
+extract_app t_or_k (L _ (HsAppInfix tv))  acc = extract_tv t_or_k tv acc
+extract_app t_or_k (L _ (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