Comments on equality types and classes

This is really just doucumenting one aspect of the kind-equality patch.

See especially Note [Equality types and classes] in TysWiredIn.
Other places should just point to this Note.

Richard please check for veracity.

2 files changed, 78 insertions, 29 deletions

diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs
index 1b5adf6bee..9d3d8297f5 100644
--- a/compiler/prelude/TysPrim.hs
+++ b/compiler/prelude/TysPrim.hs
@@ -476,6 +476,23 @@ mkStatePrimTy ty = TyConApp statePrimTyCon [ty]
 statePrimTyCon :: TyCon   -- See Note [The State# TyCon]
 statePrimTyCon   = pcPrimTyCon statePrimTyConName [Nominal] VoidRep
 
+{-
+RealWorld is deeply magical.  It is *primitive*, but it is not
+*unlifted* (hence ptrArg).  We never manipulate values of type
+RealWorld; it's only used in the type system, to parameterise State#.
+-}
+
+realWorldTyCon :: TyCon
+realWorldTyCon = mkLiftedPrimTyCon realWorldTyConName liftedTypeKind [] PtrRep
+realWorldTy :: Type
+realWorldTy          = mkTyConTy realWorldTyCon
+realWorldStatePrimTy :: Type
+realWorldStatePrimTy = mkStatePrimTy realWorldTy        -- State# RealWorld
+
+-- Note: the ``state-pairing'' types are not truly primitive,
+-- so they are defined in \tr{TysWiredIn.hs}, not here.
+
+
 voidPrimTy :: Type
 voidPrimTy = TyConApp voidPrimTyCon []
 
@@ -492,6 +509,14 @@ proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName kind [Nominal,Nominal] VoidRep
         kv   = kKiVar
         k    = mkTyVarTy kv
 
+
+{- *********************************************************************
+*                                                                      *
+                Primitive equality constraints
+    See Note [Equality types and classes] in TysWiredIn
+*                                                                      *
+********************************************************************* -}
+
 eqPrimTyCon :: TyCon  -- The representation type for equality predicates
                       -- See Note [The ~# TyCon]
 eqPrimTyCon  = mkPrimTyCon eqPrimTyConName kind roles VoidRep
@@ -531,29 +556,12 @@ eqPhantPrimTyCon = mkPrimTyCon eqPhantPrimTyConName kind
         k1            = mkTyVarTy kv1
         k2            = mkTyVarTy kv2
 
-{-
-RealWorld is deeply magical.  It is *primitive*, but it is not
-*unlifted* (hence ptrArg).  We never manipulate values of type
-RealWorld; it's only used in the type system, to parameterise State#.
--}
-
-realWorldTyCon :: TyCon
-realWorldTyCon = mkLiftedPrimTyCon realWorldTyConName liftedTypeKind [] PtrRep
-realWorldTy :: Type
-realWorldTy          = mkTyConTy realWorldTyCon
-realWorldStatePrimTy :: Type
-realWorldStatePrimTy = mkStatePrimTy realWorldTy        -- State# RealWorld
 
-{-
-Note: the ``state-pairing'' types are not truly primitive, so they are
-defined in \tr{TysWiredIn.hs}, not here.
-
-************************************************************************
+{- *********************************************************************
 *                                                                      *
-\subsection[TysPrim-arrays]{The primitive array types}
+             The primitive array types
 *                                                                      *
-************************************************************************
--}
+********************************************************************* -}
 
 arrayPrimTyCon, mutableArrayPrimTyCon, mutableByteArrayPrimTyCon,
     byteArrayPrimTyCon, arrayArrayPrimTyCon, mutableArrayArrayPrimTyCon,
@@ -584,13 +592,12 @@ mkMutableArrayArrayPrimTy s = TyConApp mutableArrayArrayPrimTyCon [s]
 mkSmallMutableArrayPrimTy :: Type -> Type -> Type
 mkSmallMutableArrayPrimTy s elt = TyConApp smallMutableArrayPrimTyCon [s, elt]
 
-{-
-************************************************************************
+
+{- *********************************************************************
 *                                                                      *
-\subsection[TysPrim-mut-var]{The mutable variable type}
+                The mutable variable type
 *                                                                      *
-************************************************************************
--}
+********************************************************************* -}
 
 mutVarPrimTyCon :: TyCon
 mutVarPrimTyCon = pcPrimTyCon mutVarPrimTyConName [Nominal, Representational] PtrRep
diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index d92c4cda3f..8a4ca4d570 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -608,12 +608,41 @@ unboxedUnitTyCon = tupleTyCon Unboxed 0
 unboxedUnitDataCon :: DataCon
 unboxedUnitDataCon = tupleDataCon   Unboxed 0
 
-{-
-************************************************************************
+
+{- *********************************************************************
 *                                                                      *
-     The ``boxed primitive'' types (@Char@, @Int@, etc)
+              Equality types and classes
 *                                                                      *
-************************************************************************
+********************************************************************* -}
+
+{- Note [Equality types and classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have the following gallery of equality types and classes
+
+* (a ~ b) :: Constraint     is defined in base:Data.Type.Equality,
+  It is an ordinary type class; it is kind-homogenous, lifted,
+  and has (a ~~ b) as a superclass
+
+* (a ~~ b) :: Constraint    is defined in ghc-prim:GHC.Types
+  It is a wired-in class (heqTyCon, heqClass).
+  It is kind-inhomogeous, lifted,
+  and has (a ~# b) as a superclass
+
+* (a ~# b) :: Constraint    is a primitive equality constraint
+                            for Nominal equality
+  Is is primitive (eqPrimTyCon), and kind-inhomogeneous
+
+* (a :~: b) :: *            is defined in base:Data.Type.Equality
+  It is an ordinary GADT, which provides evidence for type equality
+
+* (Coercible a b) :: Constraint    is defined in ghc-prim:GHC.Types
+  It is a wired-in class (coercibleTyCon, coercibleClass).
+  It is kind-homogeous, lifted,
+  and has (a ~R# b) as a superclass
+
+* (a ~R# b) :: Constraint   is a primitive equality constraint
+                            for Representational equality
+  Is is primitive (eqReprPrimTyCon), and kind-inhomogeneous
 -}
 
 heqTyCon, coercibleTyCon :: TyCon
@@ -661,6 +690,13 @@ heqSCSelId, coercibleSCSelId :: Id
     sc_pred   = mkTyConApp eqReprPrimTyCon [k, k, mkTyVarTy av, mkTyVarTy bv]
     sc_sel_id = mkDictSelId coercibleSCSelIdName klass
 
+
+{- *********************************************************************
+*                                                                      *
+                Kinds and levity
+*                                                                      *
+********************************************************************* -}
+
 -- For information about the usage of the following type, see Note [TYPE]
 -- in module TysPrim
 levityTy :: Type
@@ -700,6 +736,12 @@ unicodeStarKindTyCon  = mkSynonymTyCon unicodeStarKindTyConName
                                        [] []
                                        (tYPE liftedDataConTy)
 
+{- *********************************************************************
+*                                                                      *
+     The boxed primitive types: Char, Int, etc
+*                                                                      *
+********************************************************************* -}
+
 charTy :: Type
 charTy = mkTyConTy charTyCon