Commit b8ca6459 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 98cdaee7
......@@ -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
......
......@@ -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
......
......@@ -54,11 +54,21 @@ import Data.Type.Bool
-- | Lifted, homogeneous equality. By lifted, we mean that it can be
-- bogus (deferred type error). By homogeneous, the two types @a@
-- and @b@ must have the same kind.
class a ~~ b => (a :: k) ~ (b :: k) | a -> b, b -> a
-- NB: Not exported, as (~) is magical syntax. That's also why there's
-- no fixity.
class a ~~ b
=> (a :: k) ~ (b :: k) | a -> b, b -> a
-- See Note [Equality types and clases in TysWiredIn]
-- NB: All this class does is to wrap its superclass, which is
-- the "real", inhomogeneous equality; this is needed when
-- we have a Given (a~b), and we want to prove things from it
-- NB: Not exported, as (~) is magical syntax.
-- That's also why there's no fixity.
instance {-# INCOHERENT #-} a ~~ b => a ~ b
-- incoherent because we want to use this instance eagerly, even when
-- See Note [Equality types and clases in TysWiredIn]
-- If we have a Wanted (t1 ~ t2), we want to immediately
-- simplify it to (t1 ~~ t2) and solve that instead
--
-- INCOHERENT because we want to use this instance eagerly, even when
-- the tyvars are partially unknown.
infix 4 :~:
......@@ -69,7 +79,7 @@ infix 4 :~:
-- in the body of the pattern-match, the compiler knows that @a ~ b@.
--
-- @since 4.7.0.0
data a :~: b where
data a :~: b where -- See Note [Equality types and clases in TysWiredIn]
Refl :: a :~: a
-- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van
......
......@@ -189,9 +189,9 @@ inside GHC, to change the kind and type.
-- | Lifted, heterogeneous equality. By lifted, we mean that it
-- can be bogus (deferred type error). By heterogeneous, the two
-- types @a@ and @b@ might have different kinds.
class a ~~ b
class a ~~ b -- See Note [Equality types and clases in TysWiredIn]
-- | This two-parameter class has instances for types @a@ and @b@ if
-- | @Coercible@ is a two-parameter class that has instances for types @a@ and @b@ if
-- the compiler can infer that they have the same representation. This class
-- does not have regular instances; instead they are created on-the-fly during
-- type-checking. Trying to manually declare an instance of @Coercible@
......@@ -238,7 +238,7 @@ class a ~~ b
-- by Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones and Stephanie Weirich.
--
-- @since 4.7.0.0
class Coercible a b
class Coercible a b -- See Note [Equality types and clases in TysWiredIn]
{- *********************************************************************
* *
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment