%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1998
%
\section[TypeRep]{Type - friends' interface}
funTyCon,
-- Pretty-printing
- pprType, pprParendType, pprTyThingCategory,
- pprPred, pprTheta, pprThetaArrow, pprClassPred,
+ pprType, pprParendType, pprTyThingCategory,
+ pprPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
- -- Re-export fromKind
+ -- Kinds
liftedTypeKind, unliftedTypeKind, openTypeKind,
- isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
- mkArrowKind, mkArrowKinds,
+ argTypeKind, ubxTupleKind,
+ isLiftedTypeKindCon, isLiftedTypeKind,
+ mkArrowKind, mkArrowKinds, isCoercionKind,
+
+ -- Kind constructors...
+ liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
+ argTypeKindTyCon, ubxTupleKindTyCon,
+
+ -- And their names
+ unliftedTypeKindTyConName, openTypeKindTyConName,
+ ubxTupleKindTyConName, argTypeKindTyConName,
+ liftedTypeKindTyConName,
+
+ -- Super Kinds
+ tySuperKind, coSuperKind,
+ isTySuperKind, isCoSuperKind,
+ tySuperKindTyCon, coSuperKindTyCon,
+
pprKind, pprParendKind
) where
import {-# SOURCE #-} DataCon( DataCon, dataConName )
-- friends:
-import Kind
-import Var ( Var, Id, TyVar, tyVarKind )
-import VarSet ( TyVarSet )
-import Name ( Name, NamedThing(..), BuiltInSyntax(..), mkWiredInName )
-import OccName ( mkOccNameFS, tcName, parenSymOcc )
-import BasicTypes ( IPName, tupleParens )
-import TyCon ( TyCon, mkFunTyCon, tyConArity, tupleTyConBoxity, isTupleTyCon, isRecursiveTyCon, isNewTyCon )
-import Class ( Class )
+import Var
+import VarSet
+import Name
+import OccName
+import BasicTypes
+import TyCon
+import Class
-- others
-import PrelNames ( gHC_PRIM, funTyConKey, listTyConKey, parrTyConKey, hasKey )
+import PrelNames
import Outputable
\end{code}
TyVar
Type
- | PredTy -- A high level source type
- PredType -- ...can be expanded to a representation type...
+ | PredTy -- The type of evidence for a type predictate
+ PredType -- See Note [PredTy], and Note [Equality predicates]
+ -- NB: A PredTy (EqPred _ _) can appear only as the kind
+ -- of a coercion variable; never as the argument or result
+ -- of a FunTy (unlike ClassP, IParam)
| NoteTy -- A type with a note attached
TyNote
Type -- The expanded version
+type Kind = Type -- Invariant: a kind is always
+ -- FunTy k1 k2
+ -- or TyConApp PrimTyCon [...]
+ -- or TyVar kv (during inference only)
+ -- or ForAll ... (for top-level coercions)
+
+type SuperKind = Type -- Invariant: a super kind is always
+ -- TyConApp SuperKindTyCon ...
+
data TyNote = FTVNote TyVarSet -- The free type variables of the noted expression
\end{code}
-------------------------------------
- Source types
+ Note [PredTy]
A type of the form
PredTy p
data PredType
= ClassP Class [Type] -- Class predicate
| IParam (IPName Name) Type -- Implicit parameter
+ | EqPred Type Type -- Equality predicate (ty1 :=: ty2)
type ThetaType = [PredType]
\end{code}
function. If the argument has type (PredTy p) then the predicate p is
represented by evidence (a dictionary, for example, of type (predRepTy p).
+Note [Equality predicates]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+ forall a b. (a :=: S b) => a -> b
+could be represented by
+ ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
+OR
+ ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
+
+The latter is what we do. (Unlike for class and implicit parameter
+constraints, which do use FunTy.)
+
+Reason:
+ * FunTy is always a *value* function
+ * ForAllTy is discarded at runtime
+
+We often need to make a "wildcard" (c::PredTy..). We always use the same
+name (wildCoVarName), since it's not mentioned.
+
%************************************************************************
%* *
%************************************************************************
%* *
-\subsection{Wired-in type constructors
+ Wired-in type constructors
%* *
%************************************************************************
We define a few wired-in type constructors here to avoid module knots
\begin{code}
+--------------------------
+-- First the TyCons...
+
funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
-- You might think that (->) should have type (?? -> ? -> *), and you'd be right
-- But if we do that we get kind errors when saying
-- the kind sub-typing does. Sigh. It really only matters if you use (->) in
-- a prefix way, thus: (->) Int# Int#. And this is unusual.
-funTyConName = mkWiredInName gHC_PRIM
- (mkOccNameFS tcName FSLIT("(->)"))
- funTyConKey
- Nothing -- No parent object
- (ATyCon funTyCon) -- Relevant TyCon
- BuiltInSyntax
+
+tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
+coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
+
+liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName
+openTypeKindTyCon = mkKindTyCon openTypeKindTyConName
+unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
+ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName
+argTypeKindTyCon = mkKindTyCon argTypeKindTyConName
+
+mkKindTyCon :: Name -> TyCon
+mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
+
+--------------------------
+-- ... and now their names
+
+tySuperKindTyConName = mkPrimTyConName FSLIT("BOX") tySuperKindTyConKey tySuperKindTyCon
+coSuperKindTyConName = mkPrimTyConName FSLIT("COERCION") coSuperKindTyConKey coSuperKindTyCon
+liftedTypeKindTyConName = mkPrimTyConName FSLIT("*") liftedTypeKindTyConKey liftedTypeKindTyCon
+openTypeKindTyConName = mkPrimTyConName FSLIT("?") openTypeKindTyConKey openTypeKindTyCon
+unliftedTypeKindTyConName = mkPrimTyConName FSLIT("#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
+ubxTupleKindTyConName = mkPrimTyConName FSLIT("(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
+argTypeKindTyConName = mkPrimTyConName FSLIT("??") argTypeKindTyConKey argTypeKindTyCon
+funTyConName = mkPrimTyConName FSLIT("(->)") funTyConKey funTyCon
+
+mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
+ key
+ (ATyCon tycon)
+ BuiltInSyntax
+ -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
+ -- because they are never in scope in the source
+
+------------------
+-- We also need Kinds and SuperKinds, locally and in TyCon
+
+kindTyConType :: TyCon -> Type
+kindTyConType kind = TyConApp kind []
+
+liftedTypeKind = kindTyConType liftedTypeKindTyCon
+unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
+openTypeKind = kindTyConType openTypeKindTyCon
+argTypeKind = kindTyConType argTypeKindTyCon
+ubxTupleKind = kindTyConType ubxTupleKindTyCon
+
+mkArrowKind :: Kind -> Kind -> Kind
+mkArrowKind k1 k2 = FunTy k1 k2
+
+mkArrowKinds :: [Kind] -> Kind -> Kind
+mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
+
+tySuperKind, coSuperKind :: SuperKind
+tySuperKind = kindTyConType tySuperKindTyCon
+coSuperKind = kindTyConType coSuperKindTyCon
+
+isTySuperKind (NoteTy _ ty) = isTySuperKind ty
+isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
+isTySuperKind other = False
+
+isCoSuperKind :: SuperKind -> Bool
+isCoSuperKind (NoteTy _ ty) = isCoSuperKind ty
+isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
+isCoSuperKind other = False
+
+-------------------
+-- Lastly we need a few functions on Kinds
+
+isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
+
+isLiftedTypeKind :: Kind -> Bool
+isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
+isLiftedTypeKind other = False
+
+isCoercionKind :: Kind -> Bool
+-- All coercions are of form (ty1 :=: ty2)
+-- This function is here rather than in Coercion,
+-- because it's used in a knot-tied way to enforce invariants in Var
+isCoercionKind (NoteTy _ k) = isCoercionKind k
+isCoercionKind (PredTy (EqPred {})) = True
+isCoercionKind other = False
\end{code}
+
%************************************************************************
%* *
\subsection{The external interface}
pprPred :: PredType -> SDoc
pprPred (ClassP cls tys) = pprClassPred cls tys
pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
+pprPred (EqPred ty1 ty2) = sep [ppr ty1, nest 2 (ptext SLIT(":=:")), ppr ty2]
pprClassPred :: Class -> [Type] -> SDoc
pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas)
------------------
-- OK, here's the main printer
+pprKind = pprType
+pprParendKind = pprParendType
+
ppr_type :: Prec -> Type -> SDoc
ppr_type p (TyVarTy tv) = ppr tv
-ppr_type p (PredTy pred) = braces (ppr pred)
+ppr_type p (PredTy pred) = ifPprDebug (ptext SLIT("<pred>")) <> (ppr pred)
ppr_type p (NoteTy other ty2) = ppr_type p ty2
ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
ppr_tc_app p tc [ty]
| tc `hasKey` listTyConKey = brackets (pprType ty)
| tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
+ | tc `hasKey` liftedTypeKindTyConKey = ptext SLIT("*")
+ | tc `hasKey` unliftedTypeKindTyConKey = ptext SLIT("#")
+ | tc `hasKey` openTypeKindTyConKey = ptext SLIT("(?)")
+ | tc `hasKey` ubxTupleKindTyConKey = ptext SLIT("(#)")
+ | tc `hasKey` argTypeKindTyConKey = ptext SLIT("??")
+
ppr_tc_app p tc tys
| isTupleTyCon tc && tyConArity tc == length tys
= tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))