X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FTypeRep.lhs;h=7705650e36182e38443c8e36b34e4ff9d9d08037;hb=0cb269be72ffe42498c74d5be845eb27d8818423;hp=5625f8ec32d97842488e15b87935f1f7d3594df2;hpb=c76c69c5b62f1ca4fa52d75b0dfbd37b7eddbb09;p=ghc-hetmet.git

diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs
index 5625f8e..7705650 100644
--- a/compiler/types/TypeRep.lhs
+++ b/compiler/types/TypeRep.lhs
@@ -192,8 +192,11 @@ data Type
 	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
@@ -216,7 +219,7 @@ data TyNote = FTVNote TyVarSet	-- The free type variables of the noted expressio
 \end{code}
 
 -------------------------------------
- 		Source types
+ 		Note [PredTy]
 
 A type of the form
 	PredTy p
@@ -256,6 +259,24 @@ 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).
 
+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.
+
 
 %************************************************************************
 %*									*
@@ -313,7 +334,7 @@ funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] lif
 
 
 tySuperKindTyCon     = mkSuperKindTyCon tySuperKindTyConName
-coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
+coSuperKindTyCon     = mkSuperKindTyCon coSuperKindTyConName
 
 liftedTypeKindTyCon   = mkKindTyCon liftedTypeKindTyConName
 openTypeKindTyCon     = mkKindTyCon openTypeKindTyConName
@@ -324,13 +345,13 @@ 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
@@ -372,9 +393,11 @@ tySuperKind, coSuperKind :: SuperKind
 tySuperKind = kindTyConType tySuperKindTyCon 
 coSuperKind = kindTyConType coSuperKindTyCon 
 
+isTySuperKind (NoteTy _ ty)    = isTySuperKind ty
 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
 isTySuperKind other            = False
 
+isCoSuperKind (NoteTy _ ty)    = isCoSuperKind ty
 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
 isCoSuperKind other            = False