Omit Typeable from the "naturally coherent" list

In doing something else (Trac #14218) I tripped over the
definition of "naturally coherent" classes.  This patch

- Cocuments properly what that means

- Removes Typeable from the list, because now we know what
  it meams, Typeable clearly doesn't belong.

No regressions.

(Actually the term "naturally coherent" seems a bit off.
More like "invertible" or something.  But I left it.)

2 files changed, 70 insertions, 31 deletions

diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs
index b4a5b6b541..5c099e845e 100644
--- a/compiler/prelude/TysPrim.hs
+++ b/compiler/prelude/TysPrim.hs
@@ -582,18 +582,17 @@ 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
+           Built-in tc      Hetero?   Levity      Result       Role      Defining module
+-----------------------------------------------------------------------------------------
+~#         eqPrimTyCon      hetero    unlifted    #            nominal   GHC.Prim
+~~         hEqTyCon         hetero    lifted      Constraint   nominal   GHC.Types
+~          eqTyCon          homo      lifted      Constraint   nominal   Data.Type.Equality
+:~:        -                homo      lifted      *            nominal   Data.Type.Equality
+
+~R#        eqReprPrimTy     hetero    unlifted    #            repr      GHC.Prim
+Coercible  coercibleTyCon   homo      lifted      Constraint   repr      GHC.Types
+Coercion   -                homo      lifted      *            repr      Data.Type.Coercion
+~P#        eqPhantPrimTyCon 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)
@@ -638,8 +637,8 @@ Here's what's unusual about 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.
+   influences what happens next.) See Note [Naturally coherent classes]
+   in TcInteract.
 
  * It always terminates. That is, in the UndecidableInstances checks, we
    don't worry if a (~~) constraint is too big, as we know that solving
@@ -666,8 +665,8 @@ This is even more so an ordinary class than (~~), with the following exceptions:
 
  * It is "naturally coherent". (See (~~).)
 
- * (~) is magical syntax, as ~ is a reserved symbol. It cannot be exported
-   or imported.
+ * (~) is magical syntax, as ~ is a reserved symbol.
+   It cannot be exported or imported.
 
  * It always terminates.
 
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 1298932b27..260bb4aae3 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -2185,14 +2185,20 @@ match_class_inst dflags clas tys loc
 
 -- | 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 Note [Naturally coherent classes]
 -- See also Note [The equality class story] in TysPrim.
+naturallyCoherentClass :: Class -> Bool
 naturallyCoherentClass cls
-  = isCTupleClass cls ||   -- See "Tuple classes" in Note [Instance and Given overlap]
-    cls `hasKey` heqTyConKey ||
-    cls `hasKey` eqTyConKey ||
-    cls `hasKey` coercibleTyConKey ||
-    cls `hasKey` typeableClassKey
+  = isCTupleClass cls
+    || cls `hasKey` heqTyConKey
+    || cls `hasKey` eqTyConKey
+    || cls `hasKey` coercibleTyConKey
+{-
+    || cls `hasKey` typeableClassKey
+    -- I have no idea why Typeable is in this list, and it looks utterly
+    -- wrong, according the reasoning in Note [Naturally coherent classes].
+    -- So I've commented it out, and sure enough everything seems fine.
+-}
 
 {- Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2249,15 +2255,6 @@ Other notes:
 
 * Another "live" example is Trac #10195; another is #10177.
 
-* Tuple classes.  For reasons described in TcSMonad
-  Note [Tuples hiding implicit parameters], we may have a constraint
-     [W] (?x::Int, C a)
-  with an exactly-matching Given constraint.  We must decompose this
-  tuple and solve the components separately, otherwise we won't solve
-  it at all!  It is perfectly safe to decompose it, because the "instance"
-  for class tuples is bidirectional: the Given can also be decomposed
-  to provide the pieces.
-
 * We ignore the overlap problem if -XIncoherentInstances is in force:
   see Trac #6002 for a worked-out example where this makes a
   difference.
@@ -2286,6 +2283,49 @@ Other notes:
 All of this is disgustingly delicate, so to discourage people from writing
 simplifiable class givens, we warn about signatures that contain them;
 see TcValidity Note [Simplifiable given constraints].
+
+Note [Naturally coherent classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A few built-in classes are "naturally coherent".  This term means that
+the "instance" for the class is bidirectional with its superclass(es).
+For example, consider (~~), which behaves as if it was defined like
+this:
+  class a ~# b => a ~~ b
+  instance a ~# b => a ~~ b
+(See Note [The equality types story] in TysPrim.)
+
+Faced with [W] t1 ~~ t2, it's always OK to reduce it to [W] t1 ~# t2,
+without worrying about Note [Instance and Given overlap].  Why?  Because
+if we had [G] s1 ~~ s2, then we'd get the superclass [G] s1 ~# s2, and
+so the reduction of the [W] contraint does not risk losing any solutions.
+
+On the other hand, it can be fatal to /fail/ to reduce such
+equalities, on the grounds of Note [Instance and Given overlap],
+because many good things flow from [W] t1 ~# t2.
+
+The same reasoning applies to
+
+* (~~)        heqTyCOn
+* (~)         eqTyCon
+* Coercible   coercibleTyCon
+
+And less obviously to:
+
+* Tuple classes.  For reasons described in TcSMonad
+  Note [Tuples hiding implicit parameters], we may have a constraint
+     [W] (?x::Int, C a)
+  with an exactly-matching Given constraint.  We must decompose this
+  tuple and solve the components separately, otherwise we won't solve
+  it at all!  It is perfectly safe to decompose it, because again the
+  superclasses invert the instance;  e.g.
+      class (c1, c2) => (% c1, c2 %)
+      instance (c1, c2) => (% c1, c2 %)
+  Example in Trac #14218
+
+Exammples: T5853, T10432, T5315, T9222, T2627b, T3028b
+
+PS: the term "naturally coherent" doesn't really seem helpful.
+Perhaps "invertible" or something?  I left it for now though.
 -}