\begin{code}
module TypeRep (
- Type(..), TyNote(..), UsageAnn(..), -- Representation visible to friends
- Kind, TyVarSubst,
-
- superKind, superBoxity, -- :: SuperKind
-
- boxedKind, -- :: Kind :: BX
- anyBoxKind, -- :: Kind :: BX
- typeCon, -- :: KindCon :: BX -> KX
- anyBoxCon, -- :: KindCon :: BX
-
- boxedTypeKind, unboxedTypeKind, openTypeKind, -- Kind :: superKind
-
- mkArrowKind, mkArrowKinds,
+ Type(..), TyNote(..), PredType(..), UsageAnn(..), -- Representation visible to friends
+
+ Kind, ThetaType, RhoType, TauType, SigmaType, -- Synonyms
+ TyVarSubst,
+
+ superKind, superBoxity, -- KX and BX respectively
+ boxedBoxity, unboxedBoxity, -- :: BX
+ openKindCon, -- :: KX
+ typeCon, -- :: BX -> KX
+ boxedTypeKind, unboxedTypeKind, openTypeKind, -- :: KX
+ mkArrowKind, mkArrowKinds, -- :: KX -> KX -> KX
funTyCon
) where
import VarEnv
import VarSet
-import Name ( Provenance(..), ExportFlag(..),
- mkWiredInTyConName, mkGlobalName, mkKindOccFS, tcName,
- )
+import Name ( Name, mkGlobalName, mkKindOccFS, tcName )
+import OccName ( tcName )
import TyCon ( TyCon, KindCon,
mkFunTyCon, mkKindCon, mkSuperKindCon,
)
+import Class ( Class )
-- others
-import SrcLoc ( mkBuiltinSrcLoc )
-import PrelMods ( pREL_GHC )
-import Unique -- quite a few *Keys
-import Util ( thenCmp )
+import SrcLoc ( builtinSrcLoc )
+import PrelNames ( pREL_GHC, kindConKey, boxityConKey, boxedConKey,
+ unboxedConKey, typeConKey, anyBoxConKey, funTyConName
+ )
\end{code}
%************************************************************************
Type -- Function is *not* a TyConApp
Type
- | TyConApp -- Application of a TyCon
- TyCon -- *Invariant* saturated appliations of FunTyCon and
- -- synonyms have their own constructors, below.
+ | TyConApp -- Application of a TyCon
+ TyCon -- *Invariant* saturated appliations of FunTyCon and
+ -- synonyms have their own constructors, below.
[Type] -- Might not be saturated.
- | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
+ | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
Type
Type
- | NoteTy -- Saturated application of a type synonym
+ | ForAllTy -- A polymorphic type
+ TyVar
+ Type
+
+ | PredTy -- A Haskell predicate
+ PredType
+
+ | NoteTy -- A type with a note attached
TyNote
Type -- The expanded version
- | ForAllTy
- TyVar
- Type -- TypeKind
-
data TyNote
= SynNote Type -- The unexpanded version of the type synonym; always a TyConApp
| FTVNote TyVarSet -- The free type variables of the noted expression
= UsOnce -- Used at most once
| UsMany -- Used possibly many times (no info; this annotation can be omitted)
| UsVar UVar -- Annotation is variable (unbound OK only inside analysis)
+
+
+type ThetaType = [PredType]
+type RhoType = Type
+type TauType = Type
+type SigmaType = Type
+\end{code}
+
+
+-------------------------------------
+ Predicates
+
+Consider these examples:
+ f :: (Eq a) => a -> Int
+ g :: (?x :: Int -> Int) => a -> Int
+ h :: (r\l) => {r} => {l::Int | r}
+
+Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
+Predicates are represented inside GHC by PredType:
+
+\begin{code}
+data PredType = Class Class [Type]
+ | IParam Name Type
\end{code}
+(We don't support TREX records yet, but the setup is designed
+to expand to allow them.)
+
+A Haskell qualified type, such as that for f,g,h above, is
+represented using
+ * a FunTy for the double arrow
+ * with a PredTy as the function argument
+
+The predicate really does turn into a real extra argument to the
+function. If the argument has type (PredTy p) then the predicate p is
+represented by evidence (a dictionary, for example, of type (predRepTy p).
+
%************************************************************************
%* *
Kinds
~~~~~
-k::K = Type bx
- | k -> k
- | kv
+kind :: KX = kind -> kind
+ | Type boxity -- (Type *) is printed as just *
+ -- (Type #) is printed as just #
+
+ | OpenKind -- Can be boxed or unboxed
+ -- Printed '?'
+
+ | kv -- A kind variable; *only* happens during kind checking
+
+boxity :: BX = * -- Boxed
+ | # -- Unboxed
+ | bv -- A boxity variable; *only* happens during kind checking
+
+There's a little subtyping at the kind level:
+ forall b. Type b <: OpenKind
-kv :: KX is a kind variable
+That is, a type of kind (Type b) is OK in a context requiring an OpenKind
-Type :: BX -> KX
+OpenKind, written '?', is used as the kind for certain type variables,
+in two situations:
-bx::BX = Boxed
- | Unboxed
- | AnyBox -- Used *only* for special built-in things
- -- like error :: forall (a::*?). String -> a
- -- Here, the 'a' can be instantiated to a boxed or
- -- unboxed type.
- | bv
+1. The universally quantified type variable(s) for special built-in
+ things like error :: forall (a::?). String -> a.
+ Here, the 'a' can be instantiated to a boxed or unboxed type.
-bxv :: BX is a boxity variable
+2. Kind '?' is also used when the typechecker needs to create a fresh
+ type variable, one that may very well later be unified with a type.
+ For example, suppose f::a, and we see an application (f x). Then a
+ must be a function type, so we unify a with (b->c). But what kind
+ are b and c? They can be boxed or unboxed types, so we give them kind '?'.
+
+ When the type checker generalises over a bunch of type variables, it
+ makes any that still have kind '?' into kind '*'. So kind '?' is never
+ present in an inferred type.
-sk = KX -- A kind
- | BX -- A boxity
- | sk -> sk -- In ptic (BX -> KX)
\begin{code}
-mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str)
- (LocalDef mkBuiltinSrcLoc NotExported)
+mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str) builtinSrcLoc
-- mk_kind_name is a bit of a hack
-- The LocalDef means that we print the name without
-- a qualifier, which is what we want for these kinds.
-- It's used for both Kinds and Boxities
\end{code}
-Define KX, BX.
+------------------------------------------
+Define KX, the type of a kind
+ BX, the type of a boxity
\begin{code}
superKind :: SuperKind -- KX, the type of all kinds
superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
\end{code}
-Define Boxed, Unboxed, AnyBox
+------------------------------------------
+Define boxities: @*@ and @#@
\begin{code}
-boxedKind, unboxedKind, anyBoxKind :: Kind -- Of superkind superBoxity
+boxedBoxity, unboxedBoxity :: Kind -- :: BX
boxedConName = mk_kind_name boxedConKey SLIT("*")
-boxedKind = TyConApp (mkKindCon boxedConName superBoxity) []
+boxedBoxity = TyConApp (mkKindCon boxedConName superBoxity) []
unboxedConName = mk_kind_name unboxedConKey SLIT("#")
-unboxedKind = TyConApp (mkKindCon unboxedConName superBoxity) []
-
-anyBoxConName = mk_kind_name anyBoxConKey SLIT("?")
-anyBoxCon = mkKindCon anyBoxConName superBoxity -- A kind of wild card
-anyBoxKind = TyConApp anyBoxCon []
+unboxedBoxity = TyConApp (mkKindCon unboxedConName superBoxity) []
\end{code}
-Define Type
+------------------------------------------
+Define kinds: Type, Type *, Type #, and OpenKind
\begin{code}
-typeCon :: KindCon
+typeCon :: KindCon -- :: BX -> KX
typeConName = mk_kind_name typeConKey SLIT("Type")
typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
+
+boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind -- Of superkind superKind
+
+boxedTypeKind = TyConApp typeCon [boxedBoxity]
+unboxedTypeKind = TyConApp typeCon [unboxedBoxity]
+
+openKindConName = mk_kind_name anyBoxConKey SLIT("?")
+openKindCon = mkKindCon openKindConName superKind
+openTypeKind = TyConApp openKindCon []
\end{code}
-Define (Type Boxed), (Type Unboxed), (Type AnyBox)
+------------------------------------------
+Define arrow kinds
\begin{code}
-boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind
-boxedTypeKind = TyConApp typeCon [boxedKind]
-unboxedTypeKind = TyConApp typeCon [unboxedKind]
-openTypeKind = TyConApp typeCon [anyBoxKind]
-
mkArrowKind :: Kind -> Kind -> Kind
mkArrowKind k1 k2 = k1 `FunTy` k2
We define a few wired-in type constructors here to avoid module knots
\begin{code}
-funTyConName = mkWiredInTyConName funTyConKey pREL_GHC SLIT("(->)") funTyCon
funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
\end{code}
-%************************************************************************
-%* *
-\subsection{Equality on types}
-%* *
-%************************************************************************
-
-For the moment at least, type comparisons don't work if
-there are embedded for-alls.
-
-\begin{code}
-instance Eq Type where
- ty1 == ty2 = case ty1 `cmpTy` ty2 of { EQ -> True; other -> False }
-
-instance Ord Type where
- compare ty1 ty2 = cmpTy ty1 ty2
-
-cmpTy :: Type -> Type -> Ordering
-cmpTy ty1 ty2
- = cmp emptyVarEnv ty1 ty2
- where
- -- The "env" maps type variables in ty1 to type variables in ty2
- -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
- -- we in effect substitute tv2 for tv1 in t1 before continuing
- lookup env tv1 = case lookupVarEnv env tv1 of
- Just tv2 -> tv2
- Nothing -> tv1
-
- -- Get rid of NoteTy
- cmp env (NoteTy _ ty1) ty2 = cmp env ty1 ty2
- cmp env ty1 (NoteTy _ ty2) = cmp env ty1 ty2
-
- -- Deal with equal constructors
- cmp env (TyVarTy tv1) (TyVarTy tv2) = lookup env tv1 `compare` tv2
- cmp env (AppTy f1 a1) (AppTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
- cmp env (FunTy f1 a1) (FunTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
- cmp env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmps env tys1 tys2)
- cmp env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmp (extendVarEnv env tv1 tv2) t1 t2
-
- -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy
- cmp env (AppTy _ _) (TyVarTy _) = GT
-
- cmp env (FunTy _ _) (TyVarTy _) = GT
- cmp env (FunTy _ _) (AppTy _ _) = GT
-
- cmp env (TyConApp _ _) (TyVarTy _) = GT
- cmp env (TyConApp _ _) (AppTy _ _) = GT
- cmp env (TyConApp _ _) (FunTy _ _) = GT
-
- cmp env (ForAllTy _ _) other = GT
-
- cmp env _ _ = LT
-
- cmps env [] [] = EQ
- cmps env (t:ts) [] = GT
- cmps env [] (t:ts) = LT
- cmps env (t1:t1s) (t2:t2s) = cmp env t1 t2 `thenCmp` cmps env t1s t2s
-\end{code}
-
projects / ghc-hetmet.git / blobdiff