[commit: ghc] ghc-kinds: handling kinds in check_mono/arg-type (1316f57)

[Julien Cretin]

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : ghc-kinds

http://hackage.haskell.org/trac/ghc/changeset/1316f57194d4e34319ed54447f23023cfb21ba1a

>---------------------------------------------------------------

commit 1316f57194d4e34319ed54447f23023cfb21ba1a
Author: Julien Cretin <ghc at ia0.eu>
Date:   Mon Sep 19 15:41:40 2011 +0200

    handling kinds in check_mono/arg-type

>---------------------------------------------------------------

 compiler/iface/BuildTyCl.lhs   |    3 +--
 compiler/typecheck/TcMType.lhs |   14 ++++++++------
 compiler/typecheck/TcUnify.lhs |    4 +---
 compiler/types/Type.lhs        |   11 +++++------
 4 files changed, 15 insertions(+), 17 deletions(-)

diff --git a/compiler/iface/BuildTyCl.lhs b/compiler/iface/BuildTyCl.lhs
index 8a5f3d0..ea50ff3 100644
--- a/compiler/iface/BuildTyCl.lhs
+++ b/compiler/iface/BuildTyCl.lhs
@@ -210,8 +210,7 @@ mkDataConStupidTheta tycon arg_tys univ_tvs
   | null stupid_theta = []	-- The common case
   | otherwise 	      = filter in_arg_tys stupid_theta
   where
-    tc_subst	 = zipTopTvSubst (tyConKiVars tycon ++ tyConTyVars tycon)  -- IA0: is this correct?
-                                 (mkTyVarTys univ_tvs)
+    tc_subst	 = zipTopTvSubst (tyConTyVars tycon) (mkTyVarTys univ_tvs)
     stupid_theta = substTheta tc_subst (tyConStupidTheta tycon)
 	-- Start by instantiating the master copy of the 
 	-- stupid theta, taken from the TyCon
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 2a9ceba..b72d9a5 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -919,9 +919,11 @@ data UbxTupFlag = UT_Ok	| UT_NotOk
 	-- The "Ok" version means "ok if UnboxedTuples is on"
 
 ----------------------------------------
-check_mono_type :: Rank -> Type -> TcM ()	-- No foralls anywhere
+check_mono_type :: Rank -> KindOrType -> TcM ()	-- No foralls anywhere
 				      		-- No unlifted types of any kind
 check_mono_type rank ty
+  | isKind ty = return ()  -- IA0: Do we need to check kinds?
+  | otherwise
    = do { check_type rank UT_NotOk ty
 	; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
 
@@ -953,7 +955,7 @@ check_type rank _ (AppTy ty1 ty2)
   = do	{ check_arg_type rank ty1
 	; check_arg_type rank ty2 }
 
-check_type rank ubx_tup ty@(TyConApp tc tys')
+check_type rank ubx_tup ty@(TyConApp tc tys)
   | isSynTyCon tc
   = do	{ 	-- Check that the synonym has enough args
 		-- This applies equally to open and closed synonyms
@@ -990,8 +992,6 @@ check_type rank ubx_tup ty@(TyConApp tc tys')
   = mapM_ (check_arg_type rank) tys
 
   where
-    (kvs, _) = splitForAllTys (tyConKind tc)  -- tys contain kind instantiation arguments
-    tys = drop (length kvs) tys'  -- IA0: Are there any checks to do on the kind arguments?
     ubx_tup_ok ub_tuples_allowed = case ubx_tup of
                                    UT_Ok -> ub_tuples_allowed
                                    _     -> False
@@ -1005,7 +1005,7 @@ check_type rank ubx_tup ty@(TyConApp tc tys')
 check_type _ _ ty = pprPanic "check_type" (ppr ty)
 
 ----------------------------------------
-check_arg_type :: Rank -> Type -> TcM ()
+check_arg_type :: Rank -> KindOrType -> TcM ()
 -- The sort of type that can instantiate a type variable,
 -- or be the argument of a type constructor.
 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
@@ -1025,6 +1025,8 @@ check_arg_type :: Rank -> Type -> TcM ()
 -- Anyway, they are dealt with by a special case in check_tau_type
 
 check_arg_type rank ty 
+  | isKind ty = return ()  -- IA0: Do we need to check a kind?
+  | otherwise
   = do	{ impred <- xoptM Opt_ImpredicativeTypes
 	; let rank' = case rank of 	    -- Predictive => must be monotype
 	      	        MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
@@ -1414,7 +1416,7 @@ checkValidInstHead clas tys
                   all tcInstHeadTyAppAllTyVars tys)
                  (instTypeErr pp_pred head_type_args_tyvars_msg)
        ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
-                  isSingleton (dropWhile (isSuperKind.typeKind) tys))  -- only count type arguments
+                  isSingleton (dropWhile isKind tys))  -- only count type arguments
                  (instTypeErr pp_pred head_one_type_msg)
          -- May not contain type family applications
        ; mapM_ checkTyFamFreeness tys
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 2466497..469e1a2 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -221,10 +221,8 @@ matchExpectedTyConApp tc orig_ty
 
     go n_req ty@(TyConApp tycon args) tys
       | tc == tycon
-      = ASSERT( n_req == n_args)   -- ty::*
+      = ASSERT( n_req == length args)   -- ty::*
         return (mkReflCo ty, args ++ tys)
-        where n_args = length (drop (length kvs) args)  -- remove the kind arguments
-              (kvs, _) = splitForAllTys (tyConKind tycon)
 
     go n_req (AppTy fun arg) tys
       | n_req > 0
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index 7bbe30c..e7cac4b 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -33,7 +33,7 @@ module Type (
 	splitFunTys, splitFunTysN,
 	funResultTy, funArgTy, zipFunTys, 
 
-	mkTyConApp, mkTyConTy, tyConKiVars,
+	mkTyConApp, mkTyConTy,
 	tyConAppTyCon_maybe, tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs, 
 	splitTyConApp_maybe, splitTyConApp, 
 
@@ -62,7 +62,7 @@ module Type (
         funTyCon,
 
         -- ** Predicates on types
-        isTyVarTy, isFunTy, isDictTy, isPredTy,
+        isTyVarTy, isFunTy, isDictTy, isPredTy, isKindTy,
 
 	-- (Lifting and boxity)
 	isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
@@ -482,10 +482,6 @@ funArgTy ty                = pprPanic "funArgTy" (ppr ty)
 -- mean a distinct type, but all other type-constructor applications
 -- including functions are returned as Just ..
 
-tyConKiVars :: TyCon -> [KindVar]
--- returns the quantified kind variables of a TyCon
-tyConKiVars tc = fst (splitForAllTys (tyConKind tc))
-
 -- | The same as @fst . splitTyConApp@
 tyConAppTyCon_maybe :: Type -> Maybe TyCon
 tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
@@ -792,6 +788,9 @@ isPredTy ty
   | isSuperKind ty = False
   | otherwise = typeKind ty `eqKind` constraintKind
 
+isKindTy :: Type -> Bool
+isKindTy = isSuperKind . typeKind
+
 isClassPred, isEqPred, isIPPred :: PredType -> Bool
 isClassPred ty = case tyConAppTyCon_maybe ty of
     Just tyCon | isClassTyCon tyCon -> True