[project @ 2000-07-14 13:37:53 by simonpj]

Wibbles in the new kind-checking stuff

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

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 

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}
 
 

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 ->

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

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"