Give promoted DataCons a tyConArity and promoted TyCons a tyConKind
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 6 Feb 2012 08:40:44 +0000 (08:40 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 6 Feb 2012 08:40:44 +0000 (08:40 +0000)
..and fix up Core Lint.  (I was getting a bogus Core Lint failure.)

compiler/basicTypes/DataCon.lhs
compiler/coreSyn/CoreLint.lhs
compiler/iface/BuildTyCl.lhs
compiler/prelude/TysWiredIn.lhs
compiler/typecheck/TcHsType.lhs
compiler/types/Kind.lhs
compiler/types/TyCon.lhs

index c2cf0bf..e08bc67 100644 (file)
@@ -42,12 +42,18 @@ module DataCon (
 
         -- * Splitting product types
        splitProductType_maybe, splitProductType, deepSplitProductType,
-        deepSplitProductType_maybe
+        deepSplitProductType_maybe,
+
+        -- ** Promotion related functions
+        promoteType, isPromotableType, isPromotableTyCon,
+        buildPromotedTyCon, buildPromotedDataCon,
     ) where
 
 #include "HsVersions.h"
 
 import Type
+import TypeRep( Type(..) )  -- Used in promoteType
+import Kind
 import Unify
 import Coercion
 import TyCon
@@ -61,6 +67,7 @@ import Util
 import BasicTypes
 import FastString
 import Module
+import VarEnv
 
 import qualified Data.Data as Data
 import qualified Data.Typeable
@@ -959,4 +966,86 @@ computeRep stricts tys
                       where
                         (_tycon, _tycon_args, arg_dc, arg_tys) 
                            = deepSplitProductType "unbox_strict_arg_ty" ty
-\end{code}
\ No newline at end of file
+\end{code}
+
+
+%************************************************************************
+%*                                                                      *
+        Promoting of data types to the kind level
+%*                                                                      *
+%************************************************************************
+
+These two 'buildPromoted..' functions are here because
+ * They belong together
+ * 'buildPromotedTyCon' is used by promoteType
+ * 'buildPromotedTyCon' depends on DataCon stuff
+
+\begin{code}
+buildPromotedTyCon :: TyCon -> TyCon
+buildPromotedTyCon tc
+  = mkPromotedTyCon tc tySuperKind
+
+buildPromotedDataCon :: DataCon -> TyCon
+buildPromotedDataCon dc 
+  = ASSERT ( isPromotableType ty )
+    mkPromotedDataTyCon dc (getName dc) (getUnique dc) kind arity
+  where 
+    ty    = dataConUserType dc
+    kind  = promoteType ty
+    arity = dataConSourceArity dc
+\end{code}
+
+Note [Promoting a Type to a Kind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppsoe we have a data constructor D
+     D :: forall (a:*). Maybe a -> T a
+We promote this to be a type constructor 'D:
+     'D :: forall (k:BOX). 'Maybe k -> 'T k
+
+The transformation from type to kind is done by promoteType
+
+  * Convert forall (a:*) to forall (k:BOX), and substitute
+
+  * Ensure all foralls are at the top (no higher rank stuff)
+
+  * Ensure that all type constructors mentioned (Maybe and T
+    in the example) are promotable; that is, they have kind 
+          * -> ... -> * -> *
+
+\begin{code}
+isPromotableType :: Type -> Bool
+isPromotableType ty
+  = all (isLiftedTypeKind . tyVarKind) tvs
+    && go rho
+  where
+    (tvs, rho) = splitForAllTys ty
+    go (TyConApp tc tys) | Just n <- isPromotableTyCon tc
+                         = tys `lengthIs` n && all go tys
+    go (FunTy arg res)   = go arg && go res
+    go (TyVarTy tvar)    = tvar `elem` tvs
+    go _                 = False
+
+-- If tc's kind is [ *^n -> * ] returns [ Just n ], else returns [ Nothing ]
+isPromotableTyCon :: TyCon -> Maybe Int
+isPromotableTyCon tc
+  | all isLiftedTypeKind (res:args) = Just $ length args
+  | otherwise                       = Nothing
+  where
+    (args, res) = splitKindFunTys (tyConKind tc)
+
+-- | Promotes a type to a kind. 
+-- Assumes the argument satisfies 'isPromotableType'
+promoteType :: Type -> Kind
+promoteType ty
+  = mkForAllTys kvs (go rho)
+  where
+    (tvs, rho) = splitForAllTys ty
+    kvs = [ mkKindVar (tyVarName tv) tySuperKind | tv <- tvs ]
+    env = zipVarEnv tvs kvs
+
+    go (TyConApp tc tys) = mkTyConApp (buildPromotedTyCon tc) (map go tys)
+    go (FunTy arg res)   = mkArrowKind (go arg) (go res)
+    go (TyVarTy tv)      | Just kv <- lookupVarEnv env tv 
+                         = TyVarTy kv
+    go _ = panic "promoteType"  -- Argument did not satisfy isPromotableType
+\end{code}
index 1f2c34c..d40ef52 100644 (file)
@@ -664,31 +664,33 @@ lintInTy ty
        ; lintKind k
        ; return ty' }
 
-lintInCo :: InCoercion -> LintM OutCoercion
--- Check the coercion, and apply the substitution to it
--- See Note [Linting type lets]
-lintInCo co
-  = addLoc (InCo co) $
-    do  { co' <- applySubstCo co
-        ; _   <- lintCoercion co'
-        ; return co' }
-
 -------------------
 lintKind :: OutKind -> LintM ()
 -- Check well-formedness of kinds: *, *->*, Either * (* -> *), etc
+lintKind (TyVarTy kv) 
+ = do { checkTyCoVarInScope kv
+      ; unless (isSuperKind (varType kv))
+               (addErrL (hang (ptext (sLit "Badly kinded kind variable"))
+                            2 (ppr kv <+> dcolon <+> ppr (varType kv)))) }
+
 lintKind (FunTy k1 k2)
-  = lintKind k1 >> lintKind k2
+  = do { lintKind k1; lintKind k2 }
 
 lintKind kind@(TyConApp tc kis)
-  = do { unless (isSuperKindTyCon tc || tyConArity tc == length kis)
-           (addErrL malformed_kind)
-       ; mapM_ lintKind kis }
-  where
-    malformed_kind = hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind))
+  | not (isSuperKind (tyConKind tc))
+  = addErrL (hang (ptext (sLit "Type constructor") <+> quotes (ppr tc))
+                2 (ptext (sLit "cannot be used in a kind")))
+  
+  | not (tyConArity tc == length kis)
+  = addErrL (hang (ptext (sLit "Unsaturated ype constructor in kind"))
+                2 (quotes (ppr kind)))
+
+  | otherwise
+  = mapM_ lintKind kis
 
-lintKind (TyVarTy kv) = checkTyCoVarInScope kv
 lintKind kind
-  = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
+  = addErrL (hang (ptext (sLit "Malformed kind:")) 
+          2 (quotes (ppr kind)))
 
 -------------------
 lintTyBndrKind :: OutTyVar -> LintM ()
@@ -699,16 +701,118 @@ lintTyBndrKind tv =
   then return ()    -- kind forall
   else lintKind ki  -- type forall
 
+----------
+checkTcApp :: OutCoercion -> Int -> Type -> LintM OutType
+checkTcApp co n ty
+  | Just tys <- tyConAppArgs_maybe ty
+  , n < length tys
+  = return (tys !! n)
+  | otherwise
+  = failWithL (hang (ptext (sLit "Bad getNth:") <+> ppr co)
+                  2 (ptext (sLit "Offending type:") <+> ppr ty))
+
 -------------------
+lintType :: OutType -> LintM Kind
+-- The returned Kind has itself been linted
+lintType (TyVarTy tv)
+  = do { checkTyCoVarInScope tv
+       ; let kind = tyVarKind tv
+       ; lintKind kind
+       ; WARN( isSuperKind kind, msg )
+         return kind }
+  where msg = hang (ptext (sLit "Expecting a type, but got a kind"))
+                 2 (ptext (sLit "Offending kind:") <+> ppr tv)
+
+lintType ty@(AppTy t1 t2) 
+  = do { k1 <- lintType t1
+       ; lint_ty_app ty k1 [t2] }
+
+lintType ty@(FunTy t1 t2)
+  = lint_ty_app ty (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind) [t1,t2]
+
+lintType ty@(TyConApp tc tys)
+  | tyConHasKind tc   -- Guards for SuperKindOon
+  , not (isUnLiftedTyCon tc) || tys `lengthIs` tyConArity tc
+       -- Check that primitive types are saturated
+       -- See Note [The kind invariant] in TypeRep
+  = lint_ty_app ty (tyConKind tc) tys
+  | otherwise
+  = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
+
+lintType (ForAllTy tv ty)
+  = do { lintTyBndrKind tv
+       ; addInScopeVar tv (lintType ty) }
+
+----------------
+lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
+lint_ty_app ty k tys 
+  = lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
+
+----------------
+lint_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
+lint_co_app ty k tys 
+  = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys
+       ; return () }
+
+----------------
+lint_kind_app :: SDoc -> Kind -> [OutType] -> LintM Kind
+-- (lint_kind_app d fun_kind arg_tys)
+--    We have an application (f arg_ty1 .. arg_tyn),
+--    where f :: fun_kind
+-- Takes care of linting the OutTypes
+lint_kind_app doc kfn tys = go kfn tys
+  where
+    fail_msg = vcat [ hang (ptext (sLit "Kind application error in")) 2 doc
+                    , nest 2 (ptext (sLit "Function kind =") <+> ppr kfn)
+                    , nest 2 (ptext (sLit "Arg types =") <+> ppr tys) ]
+
+    go kfn [] = return kfn
+    go kfn (ty:tys) =
+      case splitKindFunTy_maybe kfn of
+      { Nothing ->
+          case splitForAllTy_maybe kfn of
+          { Nothing -> failWithL fail_msg
+          ; Just (kv, body) -> do
+              -- Something of kind (forall kv. body) gets instantiated
+              -- with ty. 'kv' is a kind variable and 'ty' is a kind.
+            { unless (isSuperKind (tyVarKind kv)) (addErrL fail_msg)
+            ; lintKind ty
+            ; go (substKiWith [kv] [ty] body) tys } }
+      ; Just (kfa, kfb) -> do
+          -- Something of kind (kfa -> kfb) is applied to ty. 'ty' is
+          -- a type accepting kind 'kfa'.
+        { k <- lintType ty
+        ; lintKind kfa
+        ; unless (k `isSubKind` kfa) (addErrL fail_msg)
+        ; go kfb tys } }
+
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+         Linting coercions
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+lintInCo :: InCoercion -> LintM OutCoercion
+-- Check the coercion, and apply the substitution to it
+-- See Note [Linting type lets]
+lintInCo co
+  = addLoc (InCo co) $
+    do  { co' <- applySubstCo co
+        ; _   <- lintCoercion co'
+        ; return co' }
+
 lintKindCoercion :: OutCoercion -> LintM OutKind
 -- Kind coercions are only reflexivity because they mean kind
 -- instantiation.  See Note [Kind coercions] in Coercion
+lintKindCoercion (Refl k)
+  = do { lintKind k
+       ; return k }
 lintKindCoercion co
-  = do { (k1,k2) <- lintCoercion co
-       ; checkL (k1 `eqKind` k2) 
-                (hang (ptext (sLit "Non-refl kind coercion")) 
-                    2 (ppr co))
-       ; return k1 }
+  = failWithL (hang (ptext (sLit "Non-refl kind coercion")) 
+                  2 (ppr co))
 
 lintCoercion :: OutCoercion -> LintM (OutType, OutType)
 -- Check the kind of a coercion term, returning the kind
@@ -732,14 +836,14 @@ lintCoercion co@(TyConAppCo tc cos)
          -- kis are the kind instantiations of tc
        ; kis <- mapM lintKindCoercion cokis
        ; (ss,ts) <- mapAndUnzipM lintCoercion cotys
-       ; check_co_app co ki (kis ++ ss)
+       ; lint_co_app co ki (kis ++ ss)
        ; return (mkTyConApp tc (kis ++ ss), mkTyConApp tc (kis ++ ts)) }
 
 
 lintCoercion co@(AppCo co1 co2)
   = do { (s1,t1) <- lintCoercion co1
        ; (s2,t2) <- lintCoercion co2
-       ; check_co_app co (typeKind s1) [s2]
+       ; lint_co_app co (typeKind s1) [s2]
        ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
 
 lintCoercion (ForAllCo v co)
@@ -808,85 +912,6 @@ lintCoercion (InstCo co arg_ty)
             | otherwise
             -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
          Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
-
-----------
-checkTcApp :: OutCoercion -> Int -> Type -> LintM OutType
-checkTcApp co n ty
-  | Just tys <- tyConAppArgs_maybe ty
-  , n < length tys
-  = return (tys !! n)
-  | otherwise
-  = failWithL (hang (ptext (sLit "Bad getNth:") <+> ppr co)
-                  2 (ptext (sLit "Offending type:") <+> ppr ty))
-
--------------------
-lintType :: OutType -> LintM Kind
-lintType (TyVarTy tv)
-  = do { checkTyCoVarInScope tv
-       ; let kind = tyVarKind tv
-       ; lintKind kind
-       ; WARN( isSuperKind kind, msg )
-         return kind }
-  where msg = hang (ptext (sLit "Expecting a type, but got a kind"))
-                 2 (ptext (sLit "Offending kind:") <+> ppr tv)
-
-lintType ty@(AppTy t1 t2) 
-  = do { k1 <- lintType t1
-       ; lint_ty_app ty k1 [t2] }
-
-lintType ty@(FunTy t1 t2)
-  = lint_ty_app ty (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind) [t1,t2]
-
-lintType ty@(TyConApp tc tys)
-  | tyConHasKind tc   -- Guards for SuperKindOon
-  , not (isUnLiftedTyCon tc) || tys `lengthIs` tyConArity tc
-       -- Check that primitive types are saturated
-       -- See Note [The kind invariant] in TypeRep
-  = lint_ty_app ty (tyConKind tc) tys
-  | otherwise
-  = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
-
-lintType (ForAllTy tv ty)
-  = do { lintTyBndrKind tv
-       ; addInScopeVar tv (lintType ty) }
-
-----------------
-lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
-lint_ty_app ty k tys = lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
-
-----------------
-check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
-check_co_app ty k tys = lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys >> return ()
-
-----------------
-lint_kind_app :: SDoc -> Kind -> [OutType] -> LintM Kind
--- Takes care of linting the OutTypes
-lint_kind_app doc kfn tys = go kfn tys
-  where
-    fail_msg = vcat [ hang (ptext (sLit "Kind application error in")) 2 doc
-                    , nest 2 (ptext (sLit "Function kind =") <+> ppr kfn)
-                    , nest 2 (ptext (sLit "Arg types =") <+> ppr tys) ]
-
-    go kfn [] = return kfn
-    go kfn (ty:tys) =
-      case splitKindFunTy_maybe kfn of
-      { Nothing ->
-          case splitForAllTy_maybe kfn of
-          { Nothing -> failWithL fail_msg
-          ; Just (kv, body) -> do
-              -- Something of kind (forall kv. body) gets instantiated
-              -- with ty. 'kv' is a kind variable and 'ty' is a kind.
-            { unless (isSuperKind (tyVarKind kv)) (addErrL fail_msg)
-            ; lintKind ty
-            ; go (substKiWith [kv] [ty] body) tys } }
-      ; Just (kfa, kfb) -> do
-          -- Something of kind (kfa -> kfb) is applied to ty. 'ty' is
-          -- a type accepting kind 'kfa'.
-        { k <- lintType ty
-        ; lintKind kfa
-        ; unless (k `isSubKind` kfa) (addErrL fail_msg)
-        ; go kfb tys } }
-
 \end{code}
 
 %************************************************************************
index 1ffabb4..75b8d91 100644 (file)
@@ -15,7 +15,6 @@ module BuildTyCl (
         buildSynTyCon,
         buildAlgTyCon, 
         buildDataCon,
-        buildPromotedDataTyCon,
         TcMethInfo, buildClass,
         distinctAbstractTyConRhs, totallyAbstractTyConRhs,
         mkNewTyConRhs, mkDataTyConRhs, 
@@ -35,13 +34,11 @@ import MkId
 import Class
 import TyCon
 import Type
-import Kind             ( promoteType, isPromotableType )
 import Coercion
 
 import TcRnMonad
 import Util            ( isSingleton )
 import Outputable
-import Unique           ( getUnique )
 \end{code}
        
 
@@ -184,11 +181,6 @@ mkDataConStupidTheta tycon arg_tys univ_tvs
     arg_tyvars      = tyVarsOfTypes arg_tys
     in_arg_tys pred = not $ isEmptyVarSet $ 
                      tyVarsOfType pred `intersectVarSet` arg_tyvars
-
-buildPromotedDataTyCon :: DataCon -> TyCon
-buildPromotedDataTyCon dc = ASSERT ( isPromotableType ty )
-  mkPromotedDataTyCon dc (getName dc) (getUnique dc) (promoteType ty)
-  where ty = dataConUserType dc
 \end{code}
 
 
index cd5ca66..162a702 100644 (file)
@@ -88,13 +88,14 @@ import TysPrim
 import Coercion
 import Constants       ( mAX_TUPLE_SIZE )
 import Module          ( Module )
-import DataCon          ( DataCon, mkDataCon, dataConWorkId, dataConSourceArity )
+import DataCon
 import Var
 import TyCon
 import TypeRep
 import RdrName
 import Name
-import BasicTypes       ( TupleSort(..), tupleSortBoxity, IPName(..), Arity, RecFlag(..), Boxity(..), HsBang(..) )
+import BasicTypes       ( TupleSort(..), tupleSortBoxity, IPName(..), 
+                          Arity, RecFlag(..), Boxity(..), HsBang(..) )
 import Unique           ( incrUnique, mkTupleTyConUnique,
                          mkTupleDataConUnique, mkPArrDataConUnique )
 import Data.Array
@@ -221,7 +222,6 @@ parrTyCon_RDR       = nameRdrName parrTyConName
 eqTyCon_RDR     = nameRdrName eqTyConName
 \end{code}
 
-
 %************************************************************************
 %*                                                                      *
 \subsection{mkWiredInTyCon}
@@ -324,7 +324,7 @@ tupleTyCon UnboxedTuple i = fst (unboxedTupleArr ! i)
 tupleTyCon ConstraintTuple    i = fst (factTupleArr    ! i)
 
 promotedTupleTyCon :: TupleSort -> Arity -> TyCon
-promotedTupleTyCon sort i = mkPromotedTyCon (tupleTyCon sort i)
+promotedTupleTyCon sort i = buildPromotedTyCon (tupleTyCon sort i)
 
 tupleCon :: TupleSort -> Arity -> DataCon
 tupleCon sort i | i > mAX_TUPLE_SIZE = snd (mk_tuple sort i)   -- Build one specially
@@ -633,7 +633,7 @@ mkPromotedListTy :: Type -> Type
 mkPromotedListTy ty = mkTyConApp promotedListTyCon [ty]
 
 promotedListTyCon :: TyCon
-promotedListTyCon = mkPromotedTyCon listTyCon
+promotedListTyCon = buildPromotedTyCon listTyCon
 
 nilDataCon :: DataCon
 nilDataCon  = pcDataCon nilDataConName alpha_tyvar [] listTyCon
index 9d3534b..66b7438 100644 (file)
@@ -59,7 +59,7 @@ import Kind
 import Var
 import VarSet
 import TyCon
-import DataCon ( DataCon, dataConUserType )
+import DataCon
 import TysPrim ( liftedTypeKindTyConName, constraintKindTyConName )
 import Class
 import RdrName ( rdrNameSpace, nameRdrName )
@@ -72,7 +72,6 @@ import DynFlags ( ExtensionFlag( Opt_DataKinds ) )
 import Util
 import UniqSupply
 import Outputable
-import BuildTyCl ( buildPromotedDataTyCon )
 import FastString
 import Control.Monad ( unless )
 \end{code}
@@ -747,14 +746,14 @@ ds_type (HsExplicitListTy kind tys) = do
   kind' <- zonkTcKindToKind kind
   ds_tys <- mapM dsHsType tys
   return $
-   foldr (\a b -> mkTyConApp (buildPromotedDataTyCon consDataCon) [kind', a, b])
-         (mkTyConApp (buildPromotedDataTyCon nilDataCon) [kind']) ds_tys
+   foldr (\a b -> mkTyConApp (buildPromotedDataCon consDataCon) [kind', a, b])
+         (mkTyConApp (buildPromotedDataCon nilDataCon) [kind']) ds_tys
 
 ds_type (HsExplicitTupleTy kis tys) = do
   MASSERT( length kis == length tys )
   kis' <- mapM zonkTcKindToKind kis
   tys' <- mapM dsHsType tys
-  return $ mkTyConApp (buildPromotedDataTyCon (tupleCon BoxedTuple (length kis'))) (kis' ++ tys')
+  return $ mkTyConApp (buildPromotedDataCon (tupleCon BoxedTuple (length kis'))) (kis' ++ tys')
 
 ds_type (HsWrapTy (WpKiApps kappas) ty) = do
   tau <- ds_type ty
@@ -809,7 +808,7 @@ ds_var_app name arg_tys
   = do { thing <- tcLookupGlobal name
        ; case thing of
            ATyCon tc   -> return (mkTyConApp tc arg_tys)
-           ADataCon dc -> return (mkTyConApp (buildPromotedDataTyCon dc) arg_tys) 
+           ADataCon dc -> return (mkTyConApp (buildPromotedDataCon dc) arg_tys) 
           _           -> wrongThingErr "type" (AGlobal thing) name }
 
 addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
@@ -1348,12 +1347,11 @@ sc_ds_var_app name arg_kis = do
       | isAlgTyCon tc || isTupleTyCon tc -> do
       data_kinds <- xoptM Opt_DataKinds
       unless data_kinds $ addErr (dataKindsErr name)
-      let tc_kind = tyConKind tc
-      case isPromotableKind tc_kind of
+      case isPromotableTyCon tc of
         Just n | n == length arg_kis ->
-          return (mkTyConApp (mkPromotedTyCon tc) arg_kis)
-        Just _  -> err tc_kind "is not fully applied"
-        Nothing -> err tc_kind "is not promotable"
+          return (mkTyConApp (buildPromotedTyCon tc) arg_kis)
+        Just _  -> err tc "is not fully applied"
+        Nothing -> err tc "is not promotable"
 
     -- It is in scope, but not what we expected
     Just thing -> wrongThingErr "promoted type" thing name
@@ -1363,9 +1361,9 @@ sc_ds_var_app name arg_kis = do
                   failWithTc (ptext (sLit "Promoted kind") <+> 
                               quotes (ppr name) <+>
                               ptext (sLit "used in a mutually recursive group"))
-
-  where err k m = failWithTc (    quotes (ppr name) <+> ptext (sLit "of kind")
-                              <+> quotes (ppr k)    <+> ptext (sLit m))
+  where 
+   err tc msg = failWithTc (quotes (ppr tc) <+> ptext (sLit "of kind")
+                        <+> quotes (ppr (tyConKind tc)) <+> ptext (sLit msg))
 
 \end{code}
 
index 90223d4..e919297 100644 (file)
@@ -48,10 +48,7 @@ module Kind (
 
         -- ** Functions on variables
         isKiVar, splitKiTyVars, partitionKiTyVars,
-        kiVarsOfKind, kiVarsOfKinds,
-
-        -- ** Promotion related functions
-        promoteType, isPromotableType, isPromotableKind,
+        kiVarsOfKind, kiVarsOfKinds
 
        ) where
 
@@ -251,8 +248,10 @@ isSubKind' duringTc k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
 
   | isSuperKindTyCon kc1 || isSuperKindTyCon kc2
     -- handles BOX
-    = ASSERT2( isSuperKindTyCon kc2 && null k1s && null k2s, ppr kc1 <+> ppr kc2 )
-      True
+    = WARN( not (isSuperKindTyCon kc2 && isSuperKindTyCon kc2 
+                  && null k1s && null k2s), 
+             ppr kc1 <+> ppr kc2 )
+      kc1 == kc2
 
   | otherwise = -- handles usual kinds (*, #, (#), etc.)
                 ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
@@ -313,54 +312,4 @@ kiVarsOfKind = tyVarsOfType
 
 kiVarsOfKinds :: [Kind] -> VarSet
 kiVarsOfKinds = tyVarsOfTypes
-
--- Datatype promotion
-isPromotableType :: Type -> Bool
-isPromotableType = go emptyVarSet
-  where
-    go vars (TyConApp tc tys) = ASSERT( not (isPromotedDataTyCon tc) ) all (go vars) tys
-    go vars (FunTy arg res) = all (go vars) [arg,res]
-    go vars (TyVarTy tvar) = tvar `elemVarSet` vars
-    go vars (ForAllTy tvar ty) = isPromotableTyVar tvar && go (vars `extendVarSet` tvar) ty
-    go _ _ = panic "isPromotableType"  -- argument was not kind-shaped
-
-isPromotableTyVar :: TyVar -> Bool
-isPromotableTyVar = isLiftedTypeKind . varType
-
--- | Promotes a type to a kind. Assumes the argument is promotable.
-promoteType :: Type -> Kind
-promoteType (TyConApp tc tys) = mkTyConApp (mkPromotedTyCon tc) 
-                                           (map promoteType tys)
-  -- T t1 .. tn  ~~>  'T k1 .. kn  where  ti ~~> ki
-promoteType (FunTy arg res) = mkArrowKind (promoteType arg) (promoteType res)
-  -- t1 -> t2  ~~>  k1 -> k2  where  ti ~~> ki
-promoteType (TyVarTy tvar) = mkTyVarTy (promoteTyVar tvar)
-  -- a :: *  ~~>  a :: BOX
-promoteType (ForAllTy tvar ty) = ForAllTy (promoteTyVar tvar) (promoteType ty)
-  -- forall (a :: *). t  ~~> forall (a :: BOX). k  where  t ~~> k
-promoteType _ = panic "promoteType"  -- argument was not kind-shaped
-
-promoteTyVar :: TyVar -> KindVar
-promoteTyVar tvar = mkKindVar (tyVarName tvar) tySuperKind
-
--- If kind is [ *^n -> * ] returns [ Just n ], else returns [ Nothing ]
-isPromotableKind :: Kind -> Maybe Int
-isPromotableKind kind =
-  let (args, res) = splitKindFunTys kind in
-  if all isLiftedTypeKind (res:args)
-  then Just $ length args
-  else Nothing
-
-{- Note [Promoting a Type to a Kind]
-   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We only promote the followings.
-- Type variables: a
-- Fully applied arrow types: tau -> sigma
-- Fully applied type constructors of kind:
-     n >= 0
-  /-----------\
-  * -> ... -> * -> *
-- Polymorphic types over type variables of kind star:
-  forall (a::*). tau
--}
 \end{code}
index 4317e40..e2c192f 100644 (file)
@@ -94,7 +94,7 @@ module TyCon(
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TypeRep ( Kind, Type, PredType )
-import {-# SOURCE #-} DataCon ( DataCon, isVanillaDataCon, dataConName )
+import {-# SOURCE #-} DataCon ( DataCon, isVanillaDataCon )
 import {-# SOURCE #-} IParam  ( ipTyConName )
 
 import Var
@@ -410,6 +410,7 @@ data TyCon
   | PromotedDataTyCon {                -- See Note [Promoted data constructors]
        tyConUnique :: Unique, -- ^ Same Unique as the data constructor
        tyConName   :: Name,   -- ^ Same Name as the data constructor
+       tyConArity  :: Arity, 
        tc_kind     :: Kind,   -- ^ Translated type of the data constructor
         dataCon     :: DataCon -- ^ Corresponding data constructor
     }
@@ -419,6 +420,7 @@ data TyCon
        tyConUnique :: Unique, -- ^ Same Unique as the type constructor
        tyConName   :: Name,   -- ^ Same Name as the type constructor
        tyConArity  :: Arity,  -- ^ n if ty_con :: * -> ... -> *  n times
+        tc_kind     :: Kind,   -- ^ Always tySuperKind
         ty_con      :: TyCon   -- ^ Corresponding type constructor
     }
 
@@ -961,25 +963,30 @@ mkSuperKindTyCon name
   }
 
 -- | Create a promoted data constructor 'TyCon'
-mkPromotedDataTyCon :: DataCon -> Name -> Unique -> Kind -> TyCon
-mkPromotedDataTyCon con name unique kind
+-- Somewhat dodgily, we give it the same Name 
+-- as the data constructor itself
+mkPromotedDataTyCon :: DataCon -> Name -> Unique -> Kind -> Arity -> TyCon
+mkPromotedDataTyCon con name unique kind arity
   = PromotedDataTyCon {
-        tyConName = name,
+        tyConName   = name,
         tyConUnique = unique,
-        tc_kind = kind,
-        dataCon = con
+        tyConArity  = arity,
+        tc_kind     = kind,
+        dataCon     = con
   }
 
 -- | Create a promoted type constructor 'TyCon'
-mkPromotedTyCon :: TyCon -> TyCon
-mkPromotedTyCon con
+-- Somewhat dodgily, we give it the same Name 
+-- as the type constructor itself
+mkPromotedTyCon :: TyCon -> Kind -> TyCon
+mkPromotedTyCon tc kind
   = PromotedTypeTyCon {
-        tyConName = getName con,
-        tyConUnique = getUnique con,
-        tyConArity = tyConArity con,
-        ty_con = con
+        tyConName   = getName tc,
+        tyConUnique = getUnique tc,
+        tyConArity  = tyConArity tc,
+        tc_kind     = kind,
+        ty_con      = tc
   }
-
 \end{code}
 
 \begin{code}
@@ -1288,15 +1295,9 @@ expand tvs rhs tys
 \end{code}
 
 \begin{code}
-
 tyConKind :: TyCon -> Kind
-tyConKind (FunTyCon          { tc_kind = k }) = k
-tyConKind (AlgTyCon          { tc_kind = k }) = k
-tyConKind (TupleTyCon        { tc_kind = k }) = k
-tyConKind (SynTyCon          { tc_kind = k }) = k
-tyConKind (PrimTyCon         { tc_kind = k }) = k
-tyConKind (PromotedDataTyCon { tc_kind = k }) = k
-tyConKind tc = pprPanic "tyConKind" (ppr tc)   -- SuperKindTyCon and CoTyCon
+tyConKind (SuperKindTyCon {}) = pprPanic "tyConKind" empty
+tyConKind tc                  = tc_kind tc
 
 tyConHasKind :: TyCon -> Bool
 tyConHasKind (SuperKindTyCon {}) = False
@@ -1499,8 +1500,7 @@ instance Uniquable TyCon where
     getUnique tc = tyConUnique tc
 
 instance Outputable TyCon where
-    ppr (PromotedDataTyCon {dataCon = dc}) = quote (ppr (dataConName dc))
-    ppr tc = ppr (getName tc)
+    ppr tc = ppr (tyConName tc)
 
 instance NamedThing TyCon where
     getName = tyConName