Note [The equality types story] in TysPrim
authorRichard Eisenberg <eir@cis.upenn.edu>
Wed, 16 Dec 2015 18:04:09 +0000 (13:04 -0500)
committerRichard Eisenberg <eir@cis.upenn.edu>
Wed, 16 Dec 2015 18:04:09 +0000 (13:04 -0500)
This supercedes the Note recently written in TysWiredIn.

compiler/prelude/PrelNames.hs
compiler/prelude/TysPrim.hs
compiler/prelude/TysWiredIn.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcUnify.hs
compiler/types/Class.hs
libraries/base/Data/Type/Equality.hs
libraries/ghc-prim/GHC/Types.hs

index a963a07..a9f37aa 100644 (file)
@@ -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
 
index 9d3d829..3fabb3f 100644 (file)
@@ -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) $
index da1fa70..ab23716 100644 (file)
@@ -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
index 3f50eb9..78bf845 100644 (file)
@@ -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' ]
index a6a6fa1..47d554d 100644 (file)
@@ -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
index c854eac..1257dbf 100644 (file)
@@ -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
index bb7cdaf..c56fa25 100644 (file)
@@ -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 ||
index f6cd487..28a66f2 100644 (file)
@@ -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
index d8b2ff5..b30db97 100644 (file)
@@ -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
 
 {- *********************************************************************
 *                                                                      *