Commit 7f79d0c7 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Refactoring around super-kinds

And in particular we now have BOX :: BOX
See Note [SuperKind (BOX)] in TysPrim
parent 95d2e12c
......@@ -53,6 +53,7 @@ module DataCon (
import Type
import TypeRep( Type(..) ) -- Used in promoteType
import PrelNames( liftedTypeKindTyConKey )
import Kind
import Unify
import Coercion
......@@ -983,7 +984,7 @@ These two 'buildPromoted..' functions are here because
\begin{code}
buildPromotedTyCon :: TyCon -> TyCon
buildPromotedTyCon tc
= mkPromotedTyCon tc tySuperKind
= mkPromotedTyCon tc (promoteKind (tyConKind tc))
buildPromotedDataCon :: DataCon -> TyCon
buildPromotedDataCon dc
......@@ -1040,7 +1041,7 @@ promoteType ty
= mkForAllTys kvs (go rho)
where
(tvs, rho) = splitForAllTys ty
kvs = [ mkKindVar (tyVarName tv) tySuperKind | tv <- tvs ]
kvs = [ mkKindVar (tyVarName tv) superKind | tv <- tvs ]
env = zipVarEnv tvs kvs
go (TyConApp tc tys) = mkTyConApp (buildPromotedTyCon tc) (map go tys)
......@@ -1048,4 +1049,12 @@ promoteType ty
go (TyVarTy tv) | Just kv <- lookupVarEnv env tv
= TyVarTy kv
go _ = panic "promoteType" -- Argument did not satisfy isPromotableType
promoteKind :: Kind -> SuperKind
-- Promote the kind of a type constructor
-- from (* -> * -> *) to (BOX -> BOX -> BOX)
promoteKind (TyConApp tc [])
| tc `hasKey` liftedTypeKindTyConKey = superKind
promoteKind (FunTy arg res) = FunTy (promoteKind arg) (promoteKind res)
promoteKind k = pprPanic "promoteKind" (ppr k)
\end{code}
......@@ -329,7 +329,7 @@ setTcTyVarDetails tv details = tv { tc_tv_details = details }
mkKindVar :: Name -> SuperKind -> KindVar
-- mkKindVar take a SuperKind as argument because we don't have access
-- to tySuperKind here.
-- to superKind here.
mkKindVar name kind = TyVar
{ varName = name
, realUnique = getKeyFastInt (nameUnique name)
......
......@@ -416,7 +416,7 @@ varTypeTcTyVars :: Var -> TyVarSet
-- Find the type variables free in the type of the variable
-- Remember, coercion variables can mention type variables...
varTypeTcTyVars var
| isLocalId var = tcTyVarsOfType (idType var)
| isLocalId var = tyVarsOfType (idType var)
| otherwise = emptyVarSet -- Global Ids and non-coercion TyVars
idFreeVars :: Id -> VarSet
......
......@@ -732,7 +732,7 @@ dsEvTerm (EvDelayedError ty msg) = Var errorId `mkTyApps` [ty] `mkApps` [litMsg]
---------------------------------------
dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> CoreExpr
-- This is the crucial function that moves
-- from LCoercions to Coercions; see Note [TcCoercions] in Coercion
-- from TcCoercions to Coercions; see Note [TcCoercions] in Coercion
-- e.g. dsTcCoercion (trans g1 g2) k
-- = case g1 of EqBox g1# ->
-- case g2 of EqBox g2# ->
......
......@@ -123,7 +123,7 @@ ifaceTyConName IfaceUnliftedTypeKindTc = unliftedTypeKindTyConName
ifaceTyConName IfaceUbxTupleKindTc = ubxTupleKindTyConName
ifaceTyConName IfaceArgTypeKindTc = argTypeKindTyConName
ifaceTyConName IfaceConstraintKindTc = constraintKindTyConName
ifaceTyConName IfaceSuperKindTc = tySuperKindTyConName
ifaceTyConName IfaceSuperKindTc = superKindTyConName
ifaceTyConName (IfaceTc ext) = ext
ifaceTyConName (IfaceIPTc n) = pprPanic "ifaceTyConName:IPTc" (ppr n)
-- Note [The Name of an IfaceAnyTc]
......@@ -399,7 +399,7 @@ toIfaceWiredInTyCon tc nm
| nm == argTypeKindTyConName = IfaceArgTypeKindTc
| nm == constraintKindTyConName = IfaceConstraintKindTc
| nm == ubxTupleKindTyConName = IfaceUbxTupleKindTc
| nm == tySuperKindTyConName = IfaceSuperKindTc
| nm == superKindTyConName = IfaceSuperKindTc
| otherwise = IfaceTc nm
----------------
......
......@@ -41,7 +41,7 @@ import TyCon
import DataCon
import PrelNames
import TysWiredIn
import TysPrim ( tySuperKindTyCon )
import TysPrim ( superKindTyCon )
import BasicTypes ( Arity, strongLoopBreaker )
import Literal
import qualified Var
......@@ -1302,7 +1302,7 @@ tcIfaceTyCon IfaceUnliftedTypeKindTc = return unliftedTypeKindTyCon
tcIfaceTyCon IfaceArgTypeKindTc = return argTypeKindTyCon
tcIfaceTyCon IfaceUbxTupleKindTc = return ubxTupleKindTyCon
tcIfaceTyCon IfaceConstraintKindTc = return constraintKindTyCon
tcIfaceTyCon IfaceSuperKindTc = return tySuperKindTyCon
tcIfaceTyCon IfaceSuperKindTc = return superKindTyCon
-- Even though we are in an interface file, we want to make
-- sure the instances and RULES of this tycon are loaded
......
......@@ -1255,8 +1255,8 @@ eitherTyConKey :: Unique
eitherTyConKey = mkPreludeTyConUnique 84
-- Super Kinds constructors
tySuperKindTyConKey :: Unique
tySuperKindTyConKey = mkPreludeTyConUnique 85
superKindTyConKey :: Unique
superKindTyConKey = mkPreludeTyConUnique 85
-- Kind constructors
liftedTypeKindTyConKey, anyKindTyConKey, openTypeKindTyConKey,
......
......@@ -25,11 +25,11 @@ module TysPrim(
kKiVar,
-- Kind constructors...
tySuperKindTyCon, tySuperKind, anyKindTyCon,
superKindTyCon, superKind, anyKindTyCon,
liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
argTypeKindTyCon, ubxTupleKindTyCon, constraintKindTyCon,
tySuperKindTyConName, anyKindTyConName, liftedTypeKindTyConName,
superKindTyConName, anyKindTyConName, liftedTypeKindTyConName,
openTypeKindTyConName, unliftedTypeKindTyConName,
ubxTupleKindTyConName, argTypeKindTyConName,
constraintKindTyConName,
......@@ -232,7 +232,7 @@ argAlphaTy = mkTyVarTy argAlphaTyVar
argBetaTy = mkTyVarTy argBetaTyVar
kKiVar :: KindVar
kKiVar = (tyVarList tySuperKind) !! 10
kKiVar = (tyVarList superKind) !! 10
\end{code}
......@@ -281,33 +281,53 @@ funTyCon = mkFunTyCon funTyConName $
%* *
%************************************************************************
Note [SuperKind (BOX)]
~~~~~~~~~~~~~~~~~~~~~~
Kinds are classified by "super-kinds". There is only one super-kind, namely BOX.
Perhaps surprisingly we give BOX the kind BOX, thus BOX :: BOX
Reason: we want to have kind equalities, thus (without the kind applications)
keq :: * ~ * = Eq# <refl *>
Remember that
(~) :: forall (k:BOX). k -> k -> Constraint
(~#) :: forall (k:BOX). k -> k -> #
Eq# :: forall (k:BOX). forall (a:k) (b:k). (~#) k a b -> (~) k a b
So the full defn of keq is
keq :: (~) BOX * * = Eq# BOX * * <refl *>
So you can see it's convenient to have BOX:BOX
\begin{code}
-- | See "Type#kind_subtyping" for details of the distinction between the 'Kind' 'TyCon's
tySuperKindTyCon, anyKindTyCon, liftedTypeKindTyCon,
superKindTyCon, anyKindTyCon, liftedTypeKindTyCon,
openTypeKindTyCon, unliftedTypeKindTyCon,
ubxTupleKindTyCon, argTypeKindTyCon,
constraintKindTyCon
:: TyCon
tySuperKindTyConName, anyKindTyConName, liftedTypeKindTyConName,
superKindTyConName, anyKindTyConName, liftedTypeKindTyConName,
openTypeKindTyConName, unliftedTypeKindTyConName,
ubxTupleKindTyConName, argTypeKindTyConName,
constraintKindTyConName
:: Name
tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
anyKindTyCon = mkKindTyCon anyKindTyConName tySuperKind
liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName tySuperKind
openTypeKindTyCon = mkKindTyCon openTypeKindTyConName tySuperKind
unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName tySuperKind
ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName tySuperKind
argTypeKindTyCon = mkKindTyCon argTypeKindTyConName tySuperKind
constraintKindTyCon = mkKindTyCon constraintKindTyConName tySuperKind
superKindTyCon = mkKindTyCon superKindTyConName superKind
-- See Note [SuperKind (BOX)]
anyKindTyCon = mkKindTyCon anyKindTyConName superKind
liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName superKind
openTypeKindTyCon = mkKindTyCon openTypeKindTyConName superKind
unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName superKind
ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName superKind
argTypeKindTyCon = mkKindTyCon argTypeKindTyConName superKind
constraintKindTyCon = mkKindTyCon constraintKindTyConName superKind
--------------------------
-- ... and now their names
tySuperKindTyConName = mkPrimTyConName (fsLit "BOX") tySuperKindTyConKey tySuperKindTyCon
anyKindTyConName = mkPrimTyConName (fsLit "AnyK") anyKindTyConKey anyKindTyCon
superKindTyConName = mkPrimTyConName (fsLit "BOX") superKindTyConKey superKindTyCon
anyKindTyConName = mkPrimTyConName (fsLit "AnyK") anyKindTyConKey anyKindTyCon
liftedTypeKindTyConName = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon
openTypeKindTyConName = mkPrimTyConName (fsLit "OpenKind") openTypeKindTyConKey openTypeKindTyCon
unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
......@@ -330,10 +350,12 @@ kindTyConType :: TyCon -> Type
kindTyConType kind = TyConApp kind []
-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind, constraintKind :: Kind
anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind,
argTypeKind, ubxTupleKind, constraintKind,
superKind :: Kind
-- See Note [Any kinds]
anyKind = kindTyConType anyKindTyCon
superKind = kindTyConType superKindTyCon
anyKind = kindTyConType anyKindTyCon -- See Note [Any kinds]
liftedTypeKind = kindTyConType liftedTypeKindTyCon
unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
openTypeKind = kindTyConType openTypeKindTyCon
......@@ -348,9 +370,6 @@ mkArrowKind k1 k2 = FunTy k1 k2
-- | Iterated application of 'mkArrowKind'
mkArrowKinds :: [Kind] -> Kind -> Kind
mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
tySuperKind :: SuperKind
tySuperKind = kindTyConType tySuperKindTyCon
\end{code}
%************************************************************************
......
......@@ -389,7 +389,7 @@ mkKindName unique = mkSystemName unique kind_var_occ
mkMetaKindVar :: Unique -> IORef MetaDetails -> MetaKindVar
mkMetaKindVar u r
= mkTcTyVar (mkKindName u)
tySuperKind -- not sure this is right,
superKind -- not sure this is right,
-- do we need kind vars for
-- coercions?
(MetaTv TauTv r)
......
......@@ -12,7 +12,7 @@
module Kind (
-- * Main data type
Kind, typeKind,
SuperKind, Kind, typeKind,
-- Kinds
anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind,
......@@ -25,7 +25,7 @@ module Kind (
constraintKindTyCon,
-- Super Kinds
tySuperKind, tySuperKindTyCon,
superKind, superKindTyCon,
pprKind, pprParendKind,
......@@ -37,7 +37,7 @@ module Kind (
isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
isUbxTupleKind, isArgTypeKind, isConstraintKind,
isConstraintOrLiftedKind, isKind,
isSuperKind, noHashInKind,
isSuperKind, isSuperKindTyCon, noHashInKind,
isLiftedTypeKindCon, isConstraintKindCon,
isAnyKind, isAnyKindCon,
......@@ -223,8 +223,11 @@ tcIsSubArgTypeKind _ = False
-- | Is this a super-kind (i.e. a type-of-kinds)?
isSuperKind :: Type -> Bool
isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
isSuperKind _ = False
isSuperKind (TyConApp skc []) = isSuperKindTyCon skc
isSuperKind _ = False
isSuperKindTyCon :: TyCon -> Bool
isSuperKindTyCon tc = tc `hasKey` superKindTyConKey
-- | Is this a kind (i.e. a type-of-types)?
isKind :: Kind -> Bool
......
......@@ -36,7 +36,6 @@ module TyCon(
mkLiftedPrimTyCon,
mkTupleTyCon,
mkSynTyCon,
mkSuperKindTyCon,
mkForeignTyCon,
mkPromotedDataTyCon,
mkPromotedTyCon,
......@@ -48,8 +47,8 @@ module TyCon(
isPrimTyCon,
isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
isSynTyCon, isClosedSynTyCon,
isSuperKindTyCon, isDecomposableTyCon,
isForeignTyCon, tyConHasKind,
isDecomposableTyCon,
isForeignTyCon,
isPromotedDataTyCon, isPromotedTypeTyCon,
isInjectiveTyCon,
......@@ -84,6 +83,7 @@ module TyCon(
tcExpandTyCon_maybe, coreExpandTyCon_maybe,
makeTyConAbstract,
newTyConCo, newTyConCo_maybe,
pprPromotionQuote,
-- * Primitive representations of Types
PrimRep(..),
......@@ -394,18 +394,6 @@ data TyCon
-- holds the name of the imported thing
}
-- | Super-kinds. These are "kinds-of-kinds" and are never seen in
-- Haskell source programs. There are only two super-kinds: TY (aka
-- "box"), which is the super-kind of kinds that construct types
-- eventually, and CO (aka "diamond"), which is the super-kind of
-- kinds that just represent coercions.
--
-- Super-kinds have no kind themselves, and have arity zero
| SuperKindTyCon {
tyConUnique :: Unique,
tyConName :: Name
}
-- | Represents promoted data constructor.
| PromotedDataTyCon { -- See Note [Promoted data constructors]
tyConUnique :: Unique, -- ^ Same Unique as the data constructor
......@@ -420,7 +408,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
tc_kind :: Kind, -- ^ Always TysPrim.superKind
ty_con :: TyCon -- ^ Corresponding type constructor
}
......@@ -954,14 +942,6 @@ mkSynTyCon name kind tyvars rhs parent
synTcParent = parent
}
-- | Create a super-kind 'TyCon'
mkSuperKindTyCon :: Name -> TyCon -- Super kinds always have arity zero
mkSuperKindTyCon name
= SuperKindTyCon {
tyConName = name,
tyConUnique = nameUnique name
}
-- | Create a promoted data constructor 'TyCon'
-- Somewhat dodgily, we give it the same Name
-- as the data constructor itself
......@@ -1215,11 +1195,6 @@ isForeignTyCon :: TyCon -> Bool
isForeignTyCon (PrimTyCon {tyConExtName = Just _}) = True
isForeignTyCon _ = False
-- | Is this a super-kind 'TyCon'?
isSuperKindTyCon :: TyCon -> Bool
isSuperKindTyCon (SuperKindTyCon {}) = True
isSuperKindTyCon _ = False
-- | Is this a PromotedDataTyCon?
isPromotedDataTyCon :: TyCon -> Bool
isPromotedDataTyCon (PromotedDataTyCon {}) = True
......@@ -1248,7 +1223,7 @@ isImplicitTyCon tycon
| isAlgTyCon tycon = isTupleTyCon tycon
| otherwise = True
-- 'otherwise' catches: FunTyCon, PrimTyCon,
-- PromotedDataCon, PomotedTypeTyCon, SuperKindTyCon
-- PromotedDataCon, PomotedTypeTyCon
\end{code}
......@@ -1296,12 +1271,7 @@ expand tvs rhs tys
\begin{code}
tyConKind :: TyCon -> Kind
tyConKind (SuperKindTyCon {}) = pprPanic "tyConKind" empty
tyConKind tc = tc_kind tc
tyConHasKind :: TyCon -> Bool
tyConHasKind (SuperKindTyCon {}) = False
tyConHasKind _ = True
tyConKind = tc_kind
-- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no constructors
-- could be found
......@@ -1500,7 +1470,14 @@ instance Uniquable TyCon where
getUnique tc = tyConUnique tc
instance Outputable TyCon where
ppr tc = ppr (tyConName tc)
-- At the moment a promoted TyCon has the same Name as its
-- corresponding TyCon, so we add the quote to distinguish it here
ppr tc = pprPromotionQuote tc <> ppr (tyConName tc)
pprPromotionQuote :: TyCon -> SDoc
pprPromotionQuote (PromotedTypeTyCon {}) = char '\''
pprPromotionQuote (PromotedDataTyCon {}) = char '\''
pprPromotionQuote _ = empty
instance NamedThing TyCon where
getName = tyConName
......
......@@ -79,7 +79,7 @@ module Type (
-- ** Common Kinds and SuperKinds
anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind,
argTypeKind, ubxTupleKind, constraintKind,
tySuperKind,
superKind,
-- ** Common Kind type constructors
liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
......@@ -1544,7 +1544,7 @@ type SimpleKind = Kind
typeKind :: Type -> Kind
typeKind (TyConApp tc tys)
| isPromotedTypeTyCon tc
= ASSERT( tyConArity tc == length tys ) tySuperKind
= ASSERT( tyConArity tc == length tys ) superKind
| otherwise
= kindAppResult (tyConKind tc) tys
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment