%
+% (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,
-- Kinds
liftedTypeKind, unliftedTypeKind, openTypeKind,
argTypeKind, ubxTupleKind,
isLiftedTypeKindCon, isLiftedTypeKind,
- mkArrowKind, mkArrowKinds,
+ mkArrowKind, mkArrowKinds, isCoercionKind,
-- Kind constructors...
liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
isTySuperKind, isCoSuperKind,
tySuperKindTyCon, coSuperKindTyCon,
- isCoercionKindTyCon,
-
pprKind, pprParendKind
) where
#include "HsVersions.h"
import {-# SOURCE #-} DataCon( DataCon, dataConName )
-import Monad ( guard )
--- friends:
-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, mkVoidPrimTyCon, mkSuperKindTyCon, isSuperKindTyCon, mkCoercionTyCon )
-import Class ( Class )
+-- friends:
+import Var
+import VarSet
+import Name
+import OccName
+import BasicTypes
+import TyCon
+import Class
-- others
-import PrelNames ( gHC_PRIM, funTyConKey, tySuperKindTyConKey,
- coSuperKindTyConKey, liftedTypeKindTyConKey,
- openTypeKindTyConKey, unliftedTypeKindTyConKey,
- ubxTupleKindTyConKey, argTypeKindTyConKey, listTyConKey,
- parrTyConKey, hasKey, eqCoercionKindTyConKey )
+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 SuperKind = Type -- Invariant: a super kind is always
-- TyConApp SuperKindTyCon ...
-type Coercion = Type
-
-type CoercionKind = Kind
-
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
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.
+
%************************************************************************
%* *
tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
-coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
+coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName
openTypeKindTyCon = mkKindTyCon openTypeKindTyConName
unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName
argTypeKindTyCon = mkKindTyCon argTypeKindTyConName
-eqCoercionKindTyCon =
- mkCoercionTyCon eqCoercionKindTyConName 2 (\ _ -> coSuperKind)
mkKindTyCon :: Name -> TyCon
-mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0 []
+mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
--------------------------
-- ... and now their names
-tySuperKindTyConName = mkPrimTyConName FSLIT("BOX") tySuperKindTyConKey tySuperKindTyCon
-coSuperKindTyConName = mkPrimTyConName FSLIT("COERCION") coSuperKindTyConKey coSuperKindTyCon
+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
+ubxTupleKindTyConName = mkPrimTyConName FSLIT("(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
argTypeKindTyConName = mkPrimTyConName FSLIT("??") argTypeKindTyConKey argTypeKindTyCon
funTyConName = mkPrimTyConName FSLIT("(->)") funTyConKey funTyCon
-eqCoercionKindTyConName = mkWiredInName gHC_PRIM (mkOccNameFS tcName (FSLIT(":=:")))
- eqCoercionKindTyConKey Nothing (ATyCon eqCoercionKindTyCon)
- BuiltInSyntax
-
mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
key
- Nothing -- No parent object
(ATyCon tycon)
BuiltInSyntax
-- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
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
-isCoercionKindTyCon kc = kc `hasKey` eqCoercionKindTyConKey
-
-
-------------------
--- lastly we need a few functions on Kinds
+-- 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}
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
projects / ghc-hetmet.git / blobdiff