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
\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
--------------------------
-- ... 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
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