[commit: ghc] master: Tweak comments around UnivCos. (d3ce417)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/d3ce41729890db851ea1d2c9a03efd979c2526c2/ghc

>---------------------------------------------------------------

commit d3ce41729890db851ea1d2c9a03efd979c2526c2
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Tue Dec 22 15:08:04 2015 -0500

    Tweak comments around UnivCos.


>---------------------------------------------------------------

d3ce41729890db851ea1d2c9a03efd979c2526c2
 compiler/types/TyCoRep.hs | 34 ++++++++++++++++++----------------
 1 file changed, 18 insertions(+), 16 deletions(-)

diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index c53a012..01946ba 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -880,18 +880,19 @@ role and kind, which is done in the UnivCo constructor.
 
 -- | For simplicity, we have just one UnivCo that represents a coercion from
 -- some type to some other type, with (in general) no restrictions on the
--- type. To make better sense of these, we tag a UnivCo with a
--- UnivCoProvenance. This provenance is rarely consulted and is more
--- for debugging info than anything else.
--- An important exception to this rule is that we also use a UnivCo
--- for coercion holes. See Note [Coercion holes].
+-- type. The UnivCoProvenance specifies more exactly what the coercion really
+-- is and why a program should (or shouldn't!) trust the coercion.
+-- It is reasonable to consider each constructor of 'UnivCoProvenance'
+-- as a totally independent coercion form; their only commonality is
+-- that they don't tell you what types they coercion between. (That info
+-- is in the 'UnivCo' constructor of 'Coercion'.
 data UnivCoProvenance
   = UnsafeCoerceProv   -- ^ From @unsafeCoerce#@. These are unsound.
 
-  | PhantomProv Coercion -- ^ See Note [Phantom coercions]
+  | PhantomProv CoercionN -- ^ See Note [Phantom coercions]
 
-  | ProofIrrelProv Coercion  -- ^ From the fact that any two coercions are
-                             --   considered equivalent. See Note [ProofIrrelProv]
+  | ProofIrrelProv CoercionN  -- ^ From the fact that any two coercions are
+                              --   considered equivalent. See Note [ProofIrrelProv]
 
   | PluginProv String  -- ^ From a plugin, which asserts that this coercion
                        --   is sound. The string is for the use of the plugin.
@@ -929,10 +930,11 @@ Consider
      data T a = T1 | T2
 Then we have
      T s ~R T t
-for any old s,t. The witness for this is a phantom coercion built with
-PhantomProv.  The role ofthe UnivCo is always representational.  The
-Coercion stored is the (nominal) kind coercion between the types
-   kind(T s) ~ kind (T t)
+for any old s,t. The witness for this is (TyConAppCo T Rep co),
+where (co :: s ~P t) is a phantom coercion built with PhantomProv.
+The role of the UnivCo is always Phantom.  The Coercion stored is the
+(nominal) kind coercion between the types
+   kind(s) ~N kind (t)
 
 Note [Coercion holes]
 ~~~~~~~~~~~~~~~~~~~~~~~~
@@ -947,14 +949,14 @@ During typechecking, constraint solving for type classes works by
 For equality constraints we use a different strategy.  See Note [The
 equality types story] in TysPrim for background on equality constraints.
   - For boxed equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just
-    liek type classes above
-  - But for /unxboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2)
+    like type classes above. (Indeed, boxed equality constraints *are* classes.)
+  - But for /unboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2)
     we use a different plan
 
 For unboxed equalities:
   - Generate a CoercionHole, a mutable variable just like a unification
     variable
-  - Wrap the CoercionHole in a Wanted constraint; see TcRnType.TcEvDest
+  - Wrap the CoercionHole in a Wanted constraint; see TcRnTypes.TcEvDest
   - Use the CoercionHole in a Coercion, via HoleProv
   - Solve the constraint later
   - When solved, fill in the CoercionHole by side effect, instead of
@@ -992,7 +994,7 @@ Other notes about HoleCo:
 
 Note [ProofIrrelProv]
 ~~~~~~~~~~~~~~~~~~~~~
-A ProofIreelProv is a coercion between coercions. For example:
+A ProofIrrelProv is a coercion between coercions. For example:
 
   data G a where
     MkG :: G Bool