diff --git a/ghc/compiler/typecheck/TcMatches.lhs b/ghc/compiler/typecheck/TcMatches.lhs
index edebb87d88ef178e2f3e11679ae5c399e3ae4e41..eddaca16759c37fcca5b051c38c2e0bbd73091e4 100644
--- a/ghc/compiler/typecheck/TcMatches.lhs
+++ b/ghc/compiler/typecheck/TcMatches.lhs
@@ -19,7 +19,7 @@ import RnHsSyn ( RenamedMatch, RenamedGRHSs, RenamedStmt )
import TcHsSyn ( TcMatch, TcGRHSs, TcStmt )
import TcMonad
-import TcMonoType ( kcHsSigType, kcTyVarScope, checkSigTyVars, tcHsTyVar, tcHsSigType, sigPatCtxt )
+import TcMonoType ( kcHsSigType, kcTyVarScope, newSigTyVars, checkSigTyVars, tcHsSigType, sigPatCtxt )
import Inst ( Inst, LIE, plusLIE, emptyLIE, plusLIEs )
import TcEnv ( tcExtendTyVarEnv, tcExtendLocalValEnv, tcExtendGlobalTyVars, tcGetGlobalTyVars )
import TcPat ( tcPat, tcPatBndr_NoSigs, polyPatSig )
@@ -141,10 +141,9 @@ tcMatch xve1 match@(Match sig_tvs pats maybe_rhs_sig grhss) expected_ty ctxt
newTyVarTy openTypeKind `thenNF_Tc` \ tyvar_ty ->
-- Extend the tyvar env and check the match itself
- kcTyVarScope sig_tvs (mapTc_ kcHsSigType sig_tys) `thenTc` \ sig_tyvars ->
- tcExtendTyVarEnv sig_tyvars (
- tc_match tyvar_ty
- ) `thenTc` \ (pat_ids, match_and_lie) ->
+ kcTyVarScope sig_tvs (mapTc_ kcHsSigType sig_tys) `thenTc` \ sig_tv_kinds ->
+ newSigTyVars sig_tv_kinds `thenNF_Tc` \ sig_tyvars ->
+ tcExtendTyVarEnv sig_tyvars (tc_match tyvar_ty) `thenTc` \ (pat_ids, match_and_lie) ->
-- Check that the scoped type variables from the patterns
-- have not been constrained
diff --git a/ghc/compiler/typecheck/TcModule.lhs b/ghc/compiler/typecheck/TcModule.lhs
index f4a3934faebe4d0d2e86cc0b527d226ea52f9468..86f20cace2d081b8735343b771de81eab0ad0391 100644
--- a/ghc/compiler/typecheck/TcModule.lhs
+++ b/ghc/compiler/typecheck/TcModule.lhs
@@ -147,7 +147,7 @@ tcModule rn_name_supply fixities
-- Type-check the type and class decls
tcTyAndClassDecls unf_env decls `thenTc` \ env ->
- -- Typecheck the instance decls, includes deriving
+ -- Typecheck the instance decls, includes deriving
tcSetEnv env $
tcInstDecls1 unf_env decls
diff --git a/ghc/compiler/typecheck/TcMonoType.lhs b/ghc/compiler/typecheck/TcMonoType.lhs
index ee3b281ac78703cf3ab05d5076cfaf7fb94806ec..17189bd9f4ee60357ff9ae6edd9ed6f3be0facd1 100644
--- a/ghc/compiler/typecheck/TcMonoType.lhs
+++ b/ghc/compiler/typecheck/TcMonoType.lhs
@@ -5,12 +5,12 @@
\begin{code}
module TcMonoType ( tcHsType, tcHsSigType, tcHsBoxedSigType,
- tcContext, tcClassContext, tcHsTyVar,
+ tcContext, tcClassContext,
-- Kind checking
kcHsTyVar, kcHsTyVars, mkTyClTyVars,
kcHsType, kcHsSigType, kcHsBoxedSigType, kcHsContext,
- kcTyVarScope,
+ kcTyVarScope, newSigTyVars, mkImmutTyVars,
TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
checkSigTyVars, sigCtxt, sigPatCtxt
@@ -69,12 +69,73 @@ import Outputable
%************************************************************************
%* *
-\subsection{Checking types}
+\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 kcTyVarScope 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 kcTyVarScope 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}
+kcTyVarScope :: [HsTyVarBndr Name]
+ -> TcM s a -- The kind checker
+ -> TcM s [(Name,Kind)]
+ -- Do a kind check to find out the kinds of the type variables
+ -- Then return a bunch of name-kind pairs, from which to
+ -- construct the type variables. We don't return the tyvars
+ -- themselves because sometimes we want mutable ones and
+ -- sometimes we want immutable ones.
+kcTyVarScope [] kind_check = returnTc []
+ -- A useful short cut for a common case!
+
+kcTyVarScope tv_names kind_check
+ = kcHsTyVars tv_names `thenNF_Tc` \ tv_names_w_kinds ->
+ tcExtendKindEnv tv_names_w_kinds kind_check `thenTc_`
+ zonkKindEnv tv_names_w_kinds
+\end{code}
+
+
+\begin{code}
kcHsTyVar :: HsTyVarBndr name -> NF_TcM s (name, TcKind)
kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM s [(name, TcKind)]
@@ -189,24 +250,6 @@ kcHsPred pred@(HsPClass cls tys)
unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)
\end{code}
-\begin{code}
-kcTyVarScope :: [HsTyVarBndr Name]
- -> TcM s a -- The kind checker
- -> TcM s [TyVar]
- -- Do a kind check to find out the kinds of the type variables
- -- Then return the type variables
-
-kcTyVarScope [] kind_check = returnTc []
- -- A useful short cut for a common case!
-
-kcTyVarScope tv_names kind_check
- = kcHsTyVars tv_names `thenNF_Tc` \ tv_names_w_kinds ->
- tcExtendKindEnv tv_names_w_kinds kind_check `thenTc_`
- zonkKindEnv tv_names_w_kinds `thenNF_Tc` \ zonked_pairs ->
- returnTc (map mk_tyvar zonked_pairs)
-\end{code}
-
-
%************************************************************************
%* *
\subsection{Checking types}
@@ -287,13 +330,14 @@ tcHsType (HsUsgForAllTy uv_name ty)
tcHsType ty `thenTc` \ tc_ty ->
returnTc (mkUsForAllTy uv tc_ty)
-tcHsType full_ty@(HsForAllTy (Just tv_names) context ty)
- = let
- kind_check = kcHsContext context `thenTc_` kcHsType ty
+tcHsType full_ty@(HsForAllTy (Just tv_names) ctxt ty)
+ = kcTyVarScope tv_names
+ (kcHsContext ctxt `thenTc_` kcHsType ty) `thenTc` \ tv_kinds ->
+ let
+ forall_tyvars = mkImmutTyVars tv_kinds
in
- kcTyVarScope tv_names kind_check `thenTc` \ forall_tyvars ->
tcExtendTyVarEnv forall_tyvars $
- tcContext context `thenTc` \ theta ->
+ tcContext ctxt `thenTc` \ theta ->
tcHsType ty `thenTc` \ tau ->
let
-- Check for ambiguity
@@ -387,7 +431,7 @@ tc_fun_type (HsTyVar name) arg_tys
-- data Tree a b = ...
-- type Foo a = Tree [a]
-- f :: Foo a b -> ...
- err_msg = arityErr "type synonym" name arity n_args
+ err_msg = arityErr "Type synonym" name arity n_args
n_args = length arg_tys
other -> failWithTc (wrongThingErr "type constructor" thing name)
@@ -438,24 +482,19 @@ tcClassAssertion ccall_ok assn@(HsPIParam name ty)
%************************************************************************
\begin{code}
-mk_tyvar (tv_bndr, kind) = mkTyVar tv_bndr kind
+mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
+newSigTyVars :: [(Name,Kind)] -> NF_TcM s [TcTyVar]
+
+mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
+newSigTyVars pairs = listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- pairs]
mkTyClTyVars :: Kind -- Kind of the tycon or class
-> [HsTyVarBndr Name]
-> [TyVar]
mkTyClTyVars kind tyvar_names
- = map mk_tyvar tyvars_w_kinds
+ = mkImmutTyVars tyvars_w_kinds
where
(tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
-
-tcHsTyVar :: HsTyVarBndr Name -> NF_TcM s TcTyVar
-tcHsTyVar (UserTyVar name) = newKindVar `thenNF_Tc` \ kind ->
- tcNewMutTyVar name kind
- -- NB: mutable kind => mutable tyvar, so that zonking can bind
- -- the tyvar to its immutable form
-
-tcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (mkTyVar name kind)
-
\end{code}
diff --git a/ghc/compiler/typecheck/TcRules.lhs b/ghc/compiler/typecheck/TcRules.lhs
index ec9176134b19f16f31a5ba00f34e8a250d86b212..808165d1eddcbcf50e51d6e328468627ab51c6ad 100644
--- a/ghc/compiler/typecheck/TcRules.lhs
+++ b/ghc/compiler/typecheck/TcRules.lhs
@@ -14,9 +14,9 @@ import RnHsSyn ( RenamedHsDecl )
import TcHsSyn ( TypecheckedRuleDecl, mkHsLet )
import TcMonad
import TcSimplify ( tcSimplifyToDicts, tcSimplifyAndCheck )
-import TcType ( zonkTcTypes, newTyVarTy )
+import TcType ( zonkTcTypes, zonkTcTyVarToTyVar, newTyVarTy )
import TcIfaceSig ( tcCoreExpr, tcCoreLamBndrs, tcVar )
-import TcMonoType ( tcHsSigType, tcHsTyVar, checkSigTyVars )
+import TcMonoType ( kcTyVarScope, kcHsSigType, tcHsSigType, newSigTyVars, checkSigTyVars )
import TcExpr ( tcExpr )
import TcEnv ( tcExtendLocalValEnv, newLocalId,
tcExtendTyVarEnv
@@ -55,11 +55,13 @@ tcRule (HsRule name sig_tvs vars lhs rhs src_loc)
-- Deal with the tyvars mentioned in signatures
-- Yuk to the UserTyVar
- mapNF_Tc (tcHsTyVar . UserTyVar) sig_tvs `thenNF_Tc` \ sig_tyvars ->
+ kcTyVarScope (map UserTyVar sig_tvs)
+ (mapTc_ kcHsSigType sig_tys) `thenTc` \ sig_tv_kinds ->
+ newSigTyVars sig_tv_kinds `thenNF_Tc` \ sig_tyvars ->
tcExtendTyVarEnv sig_tyvars (
-- Ditto forall'd variables
- mapNF_Tc new_id vars `thenNF_Tc` \ ids ->
+ mapNF_Tc new_id vars `thenNF_Tc` \ ids ->
tcExtendLocalValEnv [(idName id, id) | id <- ids] $
-- Now LHS and RHS
@@ -90,22 +92,23 @@ tcRule (HsRule name sig_tvs vars lhs rhs src_loc)
in
-- Gather type variables to quantify over
- zonkTcTypes (rule_ty : map idType tpl_ids) `thenNF_Tc` \ zonked_tys ->
- let
- tpl_tvs = tyVarsOfTypes zonked_tys
- in
+ -- and turn them into real TyVars (just as in TcBinds.tcBindWithSigs)
+ zonkTcTypes (rule_ty : map idType tpl_ids) `thenNF_Tc` \ zonked_tys ->
+ mapTc zonkTcTyVarToTyVar (varSetElems (tyVarsOfTypes zonked_tys)) `thenTc` \ tvs ->
-- RHS can be a bit more lenient. In particular,
-- we let constant dictionaries etc float outwards
- tcSimplifyAndCheck (text "tcRule") tpl_tvs
+ tcSimplifyAndCheck (text "tcRule") (mkVarSet tvs)
lhs_dicts rhs_lie `thenTc` \ (lie', rhs_binds) ->
- returnTc (lie', HsRule name (varSetElems tpl_tvs)
+ returnTc (lie', HsRule name tvs
(map RuleBndr tpl_ids) -- yuk
(mkHsLet lhs_binds lhs')
(mkHsLet rhs_binds rhs')
src_loc)
where
+ sig_tys = [t | RuleBndrSig _ t <- vars]
+
new_id (RuleBndr var) = newTyVarTy openTypeKind `thenNF_Tc` \ ty ->
returnNF_Tc (mkVanillaId var ty)
new_id (RuleBndrSig var rn_ty) = tcHsSigType rn_ty `thenTc` \ ty ->
diff --git a/ghc/compiler/typecheck/TcTyDecls.lhs b/ghc/compiler/typecheck/TcTyDecls.lhs
index 5efdb208f0bcb88bc08c70349cdca200efb86669..2340aef36a80610de61f614fa978fa05b7c8f2cc 100644
--- a/ghc/compiler/typecheck/TcTyDecls.lhs
+++ b/ghc/compiler/typecheck/TcTyDecls.lhs
@@ -21,7 +21,7 @@ import TcHsSyn ( TcMonoBinds, idsToMonoBinds )
import BasicTypes ( RecFlag(..), NewOrData(..) )
import TcMonoType ( tcHsSigType, tcHsBoxedSigType, kcTyVarScope, tcClassContext,
- kcHsContext, kcHsSigType
+ kcHsContext, kcHsSigType, mkImmutTyVars
)
import TcEnv ( tcExtendTyVarEnv, tcLookupTy, tcLookupValueByKey, TyThing(..), TyThingDetails(..) )
import TcMonad
@@ -141,7 +141,10 @@ tcConDecl :: TyCon -> [TyVar] -> ClassContext -> RenamedConDecl -> TcM s DataCon
tcConDecl tycon tyvars ctxt (ConDecl name wkr_name ex_tvs ex_ctxt details src_loc)
= tcAddSrcLoc src_loc $
- kcTyVarScope ex_tvs (kcConDetails ex_ctxt details) `thenTc` \ ex_tyvars ->
+ kcTyVarScope ex_tvs (kcConDetails ex_ctxt details) `thenTc` \ ex_tv_kinds ->
+ let
+ ex_tyvars = mkImmutTyVars ex_tv_kinds
+ in
tcExtendTyVarEnv ex_tyvars $
tcClassContext ex_ctxt `thenTc` \ ex_theta ->
case details of
diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs
index 7c92681dd5719e5ba095c93a1a8453c08d4d490b..a9aa01ef41b5048ccded3c3f8cb6bd76efc911c0 100644
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/ghc/compiler/typecheck/TcUnify.lhs
@@ -325,8 +325,10 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
checkTcM (not (isSigTyVar tv1))
(failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
- WARN( not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1), (ppr tv1 <+> ppr (tyVarKind tv1)) $$
- (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2)) )
+ warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
+ ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
+ (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2))) `thenNF_Tc_`
+
tcPutTyVar tv1 non_var_ty2 `thenNF_Tc_`
-- This used to say "ps_ty2" instead of "non_var_ty2"