Commit 046b47ab authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Note [The equality types story] in TysPrim

This supercedes the Note recently written in TysWiredIn.
parent efaa51de
......@@ -1372,7 +1372,7 @@ fingerprintDataConName :: Name
fingerprintDataConName =
dcQual gHC_FINGERPRINT_TYPE (fsLit "Fingerprint") fingerprintDataConKey
-- homogeneous equality
-- homogeneous equality. See Note [The equality types story] in TysPrim
eqTyConName :: Name
eqTyConName = tcQual dATA_TYPE_EQUALITY (fsLit "~") eqTyConKey
......
......@@ -443,16 +443,144 @@ doublePrimTyCon = pcPrimTyCon0 doublePrimTyConName DoubleRep
* *
************************************************************************
Note [The ~# TyCon]
~~~~~~~~~~~~~~~~~~~~
There is a perfectly ordinary type constructor ~# that represents the type
of coercions (which, remember, are values). For example
Refl Int :: ~# * * Int Int
Note [The equality types story]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
GHC sports a veritable menagerie of equality types:
Hetero? Levity Result Role Defining module
------------------------------------------------------------
~# hetero unlifted # nominal GHC.Prim
~~ hetero lifted Constraint nominal GHC.Types
~ homo lifted Constraint nominal Data.Type.Equality
:~: homo lifted * nominal Data.Type.Equality
~R# hetero unlifted # repr. GHC.Prim
Coercible homo lifted Constraint repr. GHC.Types
Coercion homo lifted * repr. Data.Type.Coercion
~P# hetero unlifted phantom GHC.Prim
Recall that "hetero" means the equality can related types of different
kinds. Knowing that (t1 ~# t2) or (t1 ~R# t2) or even that (t1 ~P# t2)
also means that (k1 ~# k2), where (t1 :: k1) and (t2 :: k2).
To produce less confusion for end users, when not dumping and without
-fprint-equality-relations, each of these groups is printed as the bottommost
listed equality. That is, (~#) and (~~) are both rendered as (~) in
error messages, and (~R#) is rendered as Coercible.
Let's take these one at a time:
(~#) :: forall k1 k2. k1 -> k2 -> #
This is The Type Of Equality in GHC. It classifies nominal coercions.
This type is used in the solver for recording equality constraints.
It responds "yes" to Type.isEqPred and classifies as an EqPred in
Type.classifyPredType.
All wanted constraints of this type are built with coercion holes.
(See Note [Coercion holes] in TyCoRep.) But see also
Note [Deferred errors for coercion holes] in TcErrors to see how
equality constraints are deferred.
Within GHC, ~# is called eqPrimTyCon, and it is defined in TysPrim.
(~~) :: forall k1 k2. k1 -> k2 -> Constraint
This is (almost) an ordinary class, defined as if by
class a ~# b => a ~~ b
instance a ~# b => a ~~ b
Here's what's unusual about it:
* We can't actually declare it that way because we don't have syntax for ~#.
And ~# isn't a constraint, so even if we could write it, it wouldn't kind
check.
* Users cannot write instances of it.
* It is "naturally coherent". This means that the solver won't hesitate to
solve a goal of type (a ~~ b) even if there is, say (Int ~~ c) in the
context. (Normally, it waits to learn more, just in case the given
influences what happens next.) This is quite like having
IncoherentInstances enabled.
* It always terminates. That is, in the UndecidableInstances checks, we
don't worry if a (~~) constraint is too big, as we know that solving
equality terminates.
On the other hand, this behaves just like any class w.r.t. eager superclass
unpacking in the solver. So a lifted equality given quickly becomes an unlifted
equality given. This is good, because the solver knows all about unlifted
equalities. There is some special-casing in TcInteract.matchClassInst to
pretend that there is an instance of this class, as we can't write the instance
in Haskell.
Within GHC, ~~ is called heqTyCon, and it is defined in TysWiredIn.
(~) :: forall k. k -> k -> Constraint
This is defined in Data.Type.Equality:
class a ~~ b => (a :: k) ~ (b :: k)
instance a ~~ b => a ~ b
This is even more so an ordinary class than (~~), with the following exceptions:
* Users cannot write instances of it.
* It is "naturally coherent". (See (~~).)
* (~) is magical syntax, as ~ is a reserved symbol. It cannot be exported
or imported.
* It always terminates.
Within GHC, ~ is called eqTyCon, and it is defined in PrelNames. Note that
it is *not* wired in.
(:~:) :: forall k. k -> k -> *
This is a perfectly ordinary GADT, wrapping (~). It is not defined within
GHC at all.
(~R#) :: forall k1 k2. k1 -> k2 -> #
The is the representational analogue of ~#. This is the type of representational
equalities that the solver works on. All wanted constraints of this type are
built with coercion holes.
Within GHC, ~R# is called eqReprPrimTyCon, and it is defined in TysPrim.
Coercible :: forall k. k -> k -> Constraint
This is quite like (~~) in the way it's defined and treated within GHC, but
it's homogeneous. Homogeneity helps with type inference (as GHC can solve one
kind from the other) and, in my (Richard's) estimation, will be more intuitive
for users.
An alternative design included HCoercible (like (~~)) and Coercible (like (~)).
One annoyance was that we want `coerce :: Coercible a b => a -> b`, and
we need the type of coerce to be fully wired-in. So the HCoercible/Coercible
split required that both types be fully wired-in. Instead of doing this,
I just got rid of HCoercible, as I'm not sure who would use it, anyway.
Within GHC, Coercible is called coercibleTyCon, and it is defined in
TysWiredIn.
Coercion :: forall k. k -> k -> *
This is a perfectly ordinary GADT, wrapping Coercible. It is not defined
within GHC at all.
(~P#) :: forall k1 k2. k1 -> k2 -> #
This is the phantom analogue of ~# and it is barely used at all.
(The solver has no idea about this one.) Here is the motivation:
data Phant a = MkPhant
type role Phant phantom
Phant <Int, Bool>_P :: Phant Int ~P# Phant Bool
We just need to have something to put on that last line. You probably
don't need to worry about it.
It is a kind-polymorphic type constructor like Any:
Refl Maybe :: ~# (* -> *) (* -> *) Maybe Maybe
(~) only appears saturated. So we check that in CoreLint.
Note [The State# TyCon]
~~~~~~~~~~~~~~~~~~~~~~~
......@@ -513,12 +641,12 @@ proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName kind [Nominal,Nominal] VoidRep
{- *********************************************************************
* *
Primitive equality constraints
See Note [Equality types and classes] in TysWiredIn
See Note [The equality types story]
* *
********************************************************************* -}
eqPrimTyCon :: TyCon -- The representation type for equality predicates
-- See Note [The ~# TyCon]
-- See Note [The equality types story]
eqPrimTyCon = mkPrimTyCon eqPrimTyConName kind roles VoidRep
where kind = ForAllTy (Named kv1 Invisible) $
ForAllTy (Named kv2 Invisible) $
......@@ -531,7 +659,7 @@ eqPrimTyCon = mkPrimTyCon eqPrimTyConName kind roles VoidRep
-- like eqPrimTyCon, but the type for *Representational* coercions
-- this should only ever appear as the type of a covar. Its role is
-- interpreted in coercionRole
eqReprPrimTyCon :: TyCon
eqReprPrimTyCon :: TyCon -- See Note [The equality types story]
eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName kind
roles VoidRep
where kind = ForAllTy (Named kv1 Invisible) $
......
......@@ -616,36 +616,7 @@ unboxedUnitDataCon = tupleDataCon Unboxed 0
* *
********************************************************************* -}
{- 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
-}
-- See Note [The equality types story] in TysPrim
heqTyCon, coercibleTyCon :: TyCon
heqClass, coercibleClass :: Class
heqDataCon, coercibleDataCon :: DataCon
......
......@@ -2098,12 +2098,14 @@ solveCallStack ev ev_cs = do
* *
***********************************************************************-}
-- See also Note [The equality types story] in TysPrim
matchLiftedEquality :: [Type] -> TcS LookupInstResult
matchLiftedEquality args
= return (GenInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
, lir_mk_ev = EvDFunApp (dataConWrapId heqDataCon) args
, lir_safe_over = True })
-- See also Note [The equality types story] in TysPrim
matchLiftedCoercible :: [Type] -> TcS LookupInstResult
matchLiftedCoercible args@[k, t1, t2]
= return (GenInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
......
......@@ -2091,6 +2091,8 @@ So a Given has EvVar inside it rather that (as previously) an EvTerm.
-}
-- | A place for type-checking evidence to go after it is generated.
-- Wanted equalities are always HoleDest; other wanteds are always
-- EvVarDest.
data TcEvDest
= EvVarDest EvVar -- ^ bind this var to the evidence
| HoleDest CoercionHole -- ^ fill in this hole with the evidence
......
......@@ -617,7 +617,8 @@ buildImplication skol_info skol_tvs given thing_inside
-- But with the solver producing unlifted equalities, we need
-- to have an EvBindsVar for them when they might be deferred to
-- runtime. Otherwise, they end up as top-level unlifted bindings,
-- which are verboten.
-- which are verboten. See also Note [Deferred errors for coercion holes]
-- in TcErrors.
else
do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
......
......@@ -261,6 +261,7 @@ classExtraBigSig (Class {classTyVars = tyvars, classFunDeps = fundeps,
-- | If a class is "naturally coherent", then we needn't worry at all, in any
-- way, about overlapping/incoherent instances. Just solve the thing!
naturallyCoherentClass :: Class -> Bool
-- See also Note [The equality class story] in TysPrim.
naturallyCoherentClass cls
= cls `hasKey` heqTyConKey ||
cls `hasKey` eqTyConKey ||
......
......@@ -54,17 +54,16 @@ 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
-- See Note [Equality types and clases in TysWiredIn]
class a ~~ b => (a :: k) ~ (b :: k) | a -> b, b -> a
-- See Note [The equality types story] in TysPrim
-- 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.
-- NB: Not exported, as (~) is magical syntax. That's also why there's
-- no fixity.
instance {-# INCOHERENT #-} a ~~ b => a ~ b
-- See Note [Equality types and clases in TysWiredIn]
-- See Note [The equality types story] in TysPrim
-- If we have a Wanted (t1 ~ t2), we want to immediately
-- simplify it to (t1 ~~ t2) and solve that instead
--
......@@ -79,7 +78,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 -- See Note [Equality types and clases in TysWiredIn]
data a :~: b where -- See Note [The equality types story] in TysPrim
Refl :: a :~: a
-- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van
......
......@@ -189,7 +189,8 @@ 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 -- See Note [Equality types and clases in TysWiredIn]
class a ~~ b
-- See also Note [The equality types story] in TysPrim
-- | @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
......@@ -238,7 +239,8 @@ class a ~~ b -- See Note [Equality types and clases in TysWiredIn]
-- by Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones and Stephanie Weirich.
--
-- @since 4.7.0.0
class Coercible a b -- See Note [Equality types and clases in TysWiredIn]
class Coercible a b
-- See also Note [The equality types story] in TysPrim
{- *********************************************************************
* *
......
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