[commit: ghc] master: Omit Typeable from the "naturally coherent" list (c41ccbf)
git at git.haskell.org
git at git.haskell.org
Tue Sep 26 14:06:30 UTC 2017
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/c41ccbfa8aaeb99dd9a36cb3d99993f0fa039cdc/ghc
>---------------------------------------------------------------
commit c41ccbfa8aaeb99dd9a36cb3d99993f0fa039cdc
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Tue Sep 26 15:02:09 2017 +0100
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.)
>---------------------------------------------------------------
c41ccbfa8aaeb99dd9a36cb3d99993f0fa039cdc
compiler/prelude/TysPrim.hs | 31 +++++++++---------
compiler/typecheck/TcInteract.hs | 70 +++++++++++++++++++++++++++++++---------
2 files changed, 70 insertions(+), 31 deletions(-)
diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs
index b4a5b6b..5c099e8 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 1298932..260bb4a 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.
-}
More information about the ghc-commits
mailing list