+
+%************************************************************************
+%* *
+\subsection{Kind checking}
+%* *
+%************************************************************************
+
+Kind checking
+~~~~~~~~~~~~~
+When we come across the binding site for some type variables, we
+proceed in two stages
+
+1. Figure out what kind each tyvar has
+
+2. Create suitably-kinded tyvars,
+ extend the envt,
+ and typecheck the body
+
+To do step 1, we proceed thus:
+
+1a. Bind each type variable to a kind variable
+1b. Apply the kind checker
+1c. Zonk the resulting kinds
+
+The kind checker is passed to tcHsTyVars as an argument.
+
+For example, when we find
+ (forall a m. m a -> m a)
+we bind a,m to kind varibles and kind-check (m a -> m a). This
+makes a get kind *, and m get kind *->*. Now we typecheck (m a -> m a)
+in an environment that binds a and m suitably.
+
+The kind checker passed to tcHsTyVars needs to look at enough to
+establish the kind of the tyvar:
+ * For a group of type and class decls, it's just the group, not
+ the rest of the program
+ * For a tyvar bound in a pattern type signature, its the types
+ mentioned in the other type signatures in that bunch of patterns
+ * For a tyvar bound in a RULE, it's the type signatures on other
+ universally quantified variables in the rule
+
+Note that this may occasionally give surprising results. For example:
+
+ data T a b = MkT (a b)
+
+Here we deduce a::*->*, b::*.
+But equally valid would be
+ a::(*->*)-> *, b::*->*
+
+\begin{code}
+-- tcHsTyVars is used for type variables in type signatures
+-- e.g. forall a. a->a
+-- They are immutable, because they scope only over the signature
+-- They may or may not be explicitly-kinded
+tcHsTyVars :: [HsTyVarBndr Name]
+ -> TcM a -- The kind checker
+ -> ([TyVar] -> TcM b)
+ -> TcM b
+
+tcHsTyVars [] kind_check thing_inside = thing_inside []
+ -- A useful short cut for a common case!
+
+tcHsTyVars tv_names kind_check thing_inside
+ = kcHsTyVars tv_names `thenNF_Tc` \ tv_names_w_kinds ->
+ tcExtendKindEnv tv_names_w_kinds kind_check `thenTc_`
+ zonkKindEnv tv_names_w_kinds `thenNF_Tc` \ tvs_w_kinds ->
+ let
+ tyvars = mkImmutTyVars tvs_w_kinds
+ in
+ tcExtendTyVarEnv tyvars (thing_inside tyvars)
+
+
+
+tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
+-- tcAddScopedTyVars is used for scoped type variables
+-- added by pattern type signatures
+-- e.g. \ (x::a) (y::a) -> x+y
+-- They never have explicit kinds (because this is source-code only)
+-- They are mutable (because they can get bound to a more specific type)
+
+-- Find the not-already-in-scope signature type variables,
+-- kind-check them, and bring them into scope
+--
+-- We no longer specify that these type variables must be univerally
+-- quantified (lots of email on the subject). If you want to put that
+-- back in, you need to
+-- a) Do a checkSigTyVars after thing_inside
+-- b) More insidiously, don't pass in expected_ty, else
+-- we unify with it too early and checkSigTyVars barfs
+-- Instead you have to pass in a fresh ty var, and unify
+-- it with expected_ty afterwards
+tcAddScopedTyVars [] thing_inside
+ = thing_inside -- Quick get-out for the empty case
+
+tcAddScopedTyVars sig_tys thing_inside
+ = tcGetEnv `thenNF_Tc` \ env ->
+ let
+ all_sig_tvs = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
+ sig_tvs = filter not_in_scope (nameSetToList all_sig_tvs)
+ not_in_scope tv = not (tcInLocalScope env tv)
+ in
+ mapNF_Tc newNamedKindVar sig_tvs `thenTc` \ kind_env ->
+ tcExtendKindEnv kind_env (kcHsSigTypes sig_tys) `thenTc_`
+ zonkKindEnv kind_env `thenNF_Tc` \ tvs_w_kinds ->
+ listTc [ tcNewMutTyVar name kind PatSigTv
+ | (name, kind) <- tvs_w_kinds] `thenNF_Tc` \ tyvars ->
+ tcExtendTyVarEnv tyvars thing_inside
+\end{code}
+