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 )
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
\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
%************************************************************************
%* *
-\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)]
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}
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
-- 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)
%************************************************************************
\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}
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
-- 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
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 ->
projects / ghc-hetmet.git / commitdiff