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

Wibbles in the new kind-checking stuff

diff --git a/ghc/compiler/typecheck/TcMatches.lhs b/ghc/compiler/typecheck/TcMatches.lhs
index edebb87..eddaca1 100644 (file)
--- 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 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 )
 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
        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
 
        -- 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 f4a3934..86f20ca 100644 (file)
--- 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 ->
     
                 -- 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 
        tcSetEnv env $
 
        tcInstDecls1 unf_env decls 

diff --git a/ghc/compiler/typecheck/TcMonoType.lhs b/ghc/compiler/typecheck/TcMonoType.lhs
index ee3b281..17189bd 100644 (file)
--- a/ghc/compiler/typecheck/TcMonoType.lhs
+++ b/ghc/compiler/typecheck/TcMonoType.lhs
@@ -5,12 +5,12 @@
 
 \begin{code}
 module TcMonoType ( tcHsType, tcHsSigType, tcHsBoxedSigType, 
 
 \begin{code}
 module TcMonoType ( tcHsType, tcHsSigType, tcHsBoxedSigType, 

-                   tcContext, tcClassContext, tcHsTyVar, 
+                   tcContext, tcClassContext,

 
                        -- Kind checking
                    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
                    kcHsType, kcHsSigType, kcHsBoxedSigType, kcHsContext,
 
                        -- Kind checking
                    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
                    kcHsType, kcHsSigType, kcHsBoxedSigType, kcHsContext,

-                   kcTyVarScope, 
+                   kcTyVarScope, newSigTyVars, mkImmutTyVars,

 
                    TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
                    checkSigTyVars, sigCtxt, sigPatCtxt
 
                    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}
 \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)]
 
 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}
 
     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}
 %************************************************************************
 %*                                                                     *
 \subsection{Checking types}

@@ -287,13 +330,14 @@ tcHsType (HsUsgForAllTy uv_name ty)
     tcHsType ty                     `thenTc` \ tc_ty ->
     returnTc (mkUsForAllTy uv tc_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
     in

-    kcTyVarScope tv_names kind_check   `thenTc` \ forall_tyvars ->

     tcExtendTyVarEnv forall_tyvars     $
     tcExtendTyVarEnv forall_tyvars     $

-    tcContext context                  `thenTc` \ theta ->
+    tcContext ctxt                     `thenTc` \ theta ->

     tcHsType ty                                `thenTc` \ tau ->
     let
        -- Check for ambiguity
     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 -> ...
                        --      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)
                    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}
 %************************************************************************
 
 \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
 
 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
   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}
 
 
 \end{code}
 
 

diff --git a/ghc/compiler/typecheck/TcRules.lhs b/ghc/compiler/typecheck/TcRules.lhs
index ec91761..808165d 100644 (file)
--- 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 TcHsSyn         ( TypecheckedRuleDecl, mkHsLet )
 import TcMonad
 import TcSimplify      ( tcSimplifyToDicts, tcSimplifyAndCheck )

-import TcType          ( zonkTcTypes, newTyVarTy )
+import TcType          ( zonkTcTypes, zonkTcTyVarToTyVar, newTyVarTy )

 import TcIfaceSig      ( tcCoreExpr, tcCoreLamBndrs, tcVar )
 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
 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
 
        -- 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
     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
        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
     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
 
        -- 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) ->
 
                       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
                                (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 ->
     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 5efdb20..2340aef 100644 (file)
--- 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,
 import BasicTypes      ( RecFlag(..), NewOrData(..) )
 
 import TcMonoType      ( tcHsSigType, tcHsBoxedSigType, kcTyVarScope, tcClassContext,

-                         kcHsContext, kcHsSigType
+                         kcHsContext, kcHsSigType, mkImmutTyVars

                        )
 import TcEnv           ( tcExtendTyVarEnv, tcLookupTy, tcLookupValueByKey, TyThing(..), TyThingDetails(..) )
 import TcMonad
                        )
 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                                        $
 
 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
     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 7c92681..a9aa01e 100644 (file)
--- 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_`
 
     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"
 
     tcPutTyVar tv1 non_var_ty2                         `thenNF_Tc_`
        -- This used to say "ps_ty2" instead of "non_var_ty2"