diff options
| -rw-r--r-- | compiler/prelude/PrelNames.hs | 2 | ||||
| -rw-r--r-- | compiler/prelude/TysPrim.hs | 150 | ||||
| -rw-r--r-- | compiler/prelude/TysWiredIn.hs | 31 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcUnify.hs | 3 | ||||
| -rw-r--r-- | compiler/types/Class.hs | 1 | ||||
| -rw-r--r-- | libraries/base/Data/Type/Equality.hs | 13 | ||||
| -rw-r--r-- | libraries/ghc-prim/GHC/Types.hs | 6 |
9 files changed, 158 insertions, 52 deletions
diff --git a/compiler/prelude/PrelNames.hs b/compiler/prelude/PrelNames.hs index a963a07f30..a9f37aa49a 100644 --- a/compiler/prelude/PrelNames.hs +++ b/compiler/prelude/PrelNames.hs @@ -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 diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs index 9d3d8297f5..3fabb3ffda 100644 --- a/compiler/prelude/TysPrim.hs +++ b/compiler/prelude/TysPrim.hs @@ -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) $ diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs index da1fa70f68..ab2371616c 100644 --- a/compiler/prelude/TysWiredIn.hs +++ b/compiler/prelude/TysWiredIn.hs @@ -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 diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 3f50eb94cc..78bf845133 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -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' ] diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index a6a6fa1a1a..47d554d50a 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -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 diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index c854eac851..1257dbf077 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -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 diff --git a/compiler/types/Class.hs b/compiler/types/Class.hs index bb7cdaf124..c56fa251e5 100644 --- a/compiler/types/Class.hs +++ b/compiler/types/Class.hs @@ -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 || diff --git a/libraries/base/Data/Type/Equality.hs b/libraries/base/Data/Type/Equality.hs index f6cd487c46..28a66f2c9d 100644 --- a/libraries/base/Data/Type/Equality.hs +++ b/libraries/base/Data/Type/Equality.hs @@ -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 diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs index d8b2ff5b4c..b30db97400 100644 --- a/libraries/ghc-prim/GHC/Types.hs +++ b/libraries/ghc-prim/GHC/Types.hs @@ -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 {- ********************************************************************* * * |