[commit: ghc] master: Update Notes for Coercible (23efdd6)

[git at git.haskell.org]

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

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

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

commit 23efdd6f739eca3f910030a7a85948257747d9bc
Author: Joachim Breitner <mail at joachim-breitner.de>
Date:   Fri Nov 29 09:28:53 2013 +0000

    Update Notes for Coercible


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

23efdd6f739eca3f910030a7a85948257747d9bc
 compiler/prelude/primops.txt.pp    |    2 +-
 compiler/typecheck/TcCanonical.lhs |    1 +
 compiler/typecheck/TcInteract.lhs  |   33 +++++++++++++++++++++++++--------
 compiler/typecheck/TcValidity.lhs  |    2 +-
 4 files changed, 28 insertions(+), 10 deletions(-)

diff --git a/compiler/prelude/primops.txt.pp b/compiler/prelude/primops.txt.pp
index 37591af..41a6785 100644
--- a/compiler/prelude/primops.txt.pp
+++ b/compiler/prelude/primops.txt.pp
@@ -2372,7 +2372,7 @@ primclass Coercible a b
 
      In SafeHaskell code, this instance is only usable if the constructors of
      every type constructor used in the definition of {\tt D} (including
-     those of {\tt D} itself) is in scope.
+     those of {\tt D} itself) are in scope.
 
      The third kind of instance exists for every {\tt newtype NT = MkNT T} and
      comes in two variants, namely
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 8f60bc5..392f12d 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -235,6 +235,7 @@ canClassNC ev cls tys
 
 -- This case implements Coercible (forall a. body) (forall b. body)
 canClass ev cls tys
+  -- See Note [Coercible instances]
   | cls == coercibleClass
   , [_k, ty1, ty2] <- tys
   , tcIsForAllTy ty1
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 0ede57c..805afb6 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -2030,9 +2030,9 @@ requestCoercible loc ty1 ty2 =
 Note [Coercible Instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 The class Coercible is special: There are no regular instances, and the user
-cannot even define them. Instead, the type checker will create instances and
-their evidence out of thin air, in getCoercibleInst. The following “instances”
-are present:
+cannot even define them (it is listed as an `abstractClass` in TcValidity).
+Instead, the type checker will create instances and their evidence out of thin
+air, in getCoercibleInst. The following “instances” are present:
 
  1. instance Coercible a a
     for any type a at any kind k.
@@ -2050,13 +2050,15 @@ are present:
 
     Furthermore in Safe Haskell code, we check that
      * the data constructors of C are in scope and
-     * the data constructors of all type constructors used in the definition of C are in scope.
+     * the data constructors of all type constructors used in the definition of
+     * C are in scope.
        This is required as otherwise the previous check can be circumvented by
        just adding a local data type around C.
 
  3. instance Coercible r b => Coercible (NT t1 t2 ...) b
     instance Coercible a r => Coercible a (NT t1 t2 ...)
-    for a newtype constructor NT where
+    for a newtype constructor NT (nor data family instance that resolves to a
+    newtype) where
      * r is the concrete type of NT, instantiated with the arguments t1 t2 ...
      * the data constructors of NT are in scope.
 
@@ -2068,9 +2070,24 @@ are present:
       newtype NT3 a b = NT3 (b -> a)
       Coercible (NT2 Int) (NT3 Int) -- cannot be derived
 
-These three shapes of instances correspond to the three constructors of
-EvCoercible (defined in EvEvidence). They are assembled here and turned to Core
-by dsEvTerm in DsBinds.
+  4. instance (forall a. Coercible t1 t2) => Coercible (forall a. t1) (forall a. t2)
+     (which would be illegal to write like that in the source code, but we have
+     it nevertheless).
+
+The type checker generates evidence in the form of EvCoercion, but the
+TcCoercion therein has role Representational,  which are turned into Core
+coercions by dsEvTerm in DsBinds.
+
+The evidence for the first three instance is generated here by
+getCoercibleInst, the forth instance is implemented in the canonicalization
+stage using deferTcSForAllEq.
+
+When the constraint cannot be solved, it is treated as any other unsolved
+constraint, i.e. it can turn up in an inferred type signature, or reported to
+the user as a regular "Cannot derive instance ..." error. In the latter case,
+coercible_msg in TcErrors gives additional explanations of why GHC could not
+find a Coercible instance, so it duplicates some of the logic from
+getCoercibleInst (in negated form).
 
 
 Note [Instance and Given overlap]
diff --git a/compiler/typecheck/TcValidity.lhs b/compiler/typecheck/TcValidity.lhs
index f32369e..90a9be9 100644
--- a/compiler/typecheck/TcValidity.lhs
+++ b/compiler/typecheck/TcValidity.lhs
@@ -803,7 +803,7 @@ checkValidInstHead ctxt clas cls_args
                 text "The class is abstract, manual instances are not permitted."
 
 abstractClasses :: [ Class ]
-abstractClasses = [ coercibleClass ]
+abstractClasses = [ coercibleClass ] -- See Note [Coercible Instances]
 
 instTypeErr :: Class -> [Type] -> SDoc -> SDoc
 instTypeErr cls tys msg