[commit: ghc] master: Clarify some comments around injectivity. (daf1eee)

[git at git.haskell.org]

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

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

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

commit daf1eee4cdfeba6af77dafe3561fe178b9f30f11
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Tue Jun 16 08:45:04 2015 -0400

    Clarify some comments around injectivity.


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

daf1eee4cdfeba6af77dafe3561fe178b9f30f11
 compiler/typecheck/TcCanonical.hs | 21 +++++++++++++++++++--
 compiler/typecheck/TcRnDriver.hs  |  2 +-
 compiler/types/TyCon.hs           | 22 +++++++++++++---------
 3 files changed, 33 insertions(+), 12 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 7512e42..ee5b6dd 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -720,7 +720,9 @@ NthCo on representational coercions over newtypes. NthCo comes into play
 only when decomposing givens. So we avoid decomposing representational given
 equalities over newtypes.
 
-But is it ever sensible to decompose *Wanted* constraints over newtypes? Yes, as
+But is it ever sensible to decompose *Wanted* constraints over newtypes? Yes --
+it's the only way we could ever prove (IO Int ~R IO Age), recalling that IO
+is a newtype. However, we must decompose wanteds only as
 long as there are no Givens that might (later) influence Coercible solving.
 (See Note [Instance and Given overlap] in TcInteract.) By the time we reach
 canDecomposableTyConApp, we know that any newtypes that can be unwrapped have
@@ -743,6 +745,20 @@ evidence that (Nt Int ~R Nt Char), even if we can't form that evidence in this
 module (because Mk is not in scope). Creating this scenario in source Haskell
 is challenging; there is no test case.
 
+Example of how decomposing a wanted newtype is wrong, if it's not the only
+possibility:
+
+  newtype Nt a = MkNt (Id a)
+  type family Id a where Id a = a
+
+  [W] Nt Int ~R Nt Age
+
+Because of its use of a type family, Nt's parameter will get inferred to have
+a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
+is unsatisfiable. Unwrapping, though, leads to a solution.
+
+In summary, decomposing a wanted is always sound, but it might not be complete.
+So we do it when it's the only possible way forward.
 
 Note [Decomposing equality]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -814,7 +830,8 @@ implementation is indeed merged.)
 {2}: See Note [Decomposing newtypes]
 
 {3}: Because of the possibility of newtype instances, we must treat data families
-like newtypes. See also Note [Decomposing newtypes].
+like newtypes. See also Note [Decomposing newtypes]. See #10534 and test case
+typecheck/should_fail/T10534.
 
 {4}: Because type variables can stand in for newtypes, we conservatively do not
 decompose AppTys over representational equality.
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index b260418..0e3ee2d 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -996,7 +996,7 @@ checkBootTyCon tc1 tc2
                  quotes (text "representational") <+> text "in boot files.")
 
     eqAlgRhs tc (AbstractTyCon dis1) rhs2
-      | dis1      = check (isDistinctAlgRhs rhs2)   --Check compatibility
+      | dis1      = check (isGenInjAlgRhs rhs2)   --Check compatibility
                           (text "The natures of the declarations for" <+>
                            quotes (ppr tc) <+> text "are different")
       | otherwise = checkSuccess
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 11f0c42..0a7ba63 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -49,7 +49,7 @@ module TyCon(
         isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
         isBuiltInSynFamTyCon_maybe,
         isUnLiftedTyCon,
-        isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isDistinctAlgRhs,
+        isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs,
         isTyConAssoc, tyConAssoc_maybe,
         isRecursiveTyCon,
         isImplicitTyCon,
@@ -1165,7 +1165,7 @@ isAbstractTyCon _ = False
 -- algebraic
 makeTyConAbstract :: TyCon -> TyCon
 makeTyConAbstract tc@(AlgTyCon { algTcRhs = rhs })
-  = tc { algTcRhs = AbstractTyCon (isDistinctAlgRhs rhs) }
+  = tc { algTcRhs = AbstractTyCon (isGenInjAlgRhs rhs) }
 makeTyConAbstract tc = pprPanic "makeTyConAbstract" (ppr tc)
 
 -- | Does this 'TyCon' represent something that cannot be defined in Haskell?
@@ -1214,12 +1214,13 @@ isDataTyCon _ = False
 -- (where X is the role passed in):
 --   If (T a1 b1 c1) ~X (T a2 b2 c2), then (a1 ~X1 a2), (b1 ~X2 b2), and (c1 ~X3 c2)
 -- (where X1, X2, and X3, are the roles given by tyConRolesX tc X)
+-- See also Note [Decomposing equalities] in TcCanonical
 isInjectiveTyCon :: TyCon -> Role -> Bool
 isInjectiveTyCon _                             Phantom          = False
 isInjectiveTyCon (FunTyCon {})                 _                = True
 isInjectiveTyCon (AlgTyCon {})                 Nominal          = True
 isInjectiveTyCon (AlgTyCon {algTcRhs = rhs})   Representational
-  = isDistinctAlgRhs rhs
+  = isGenInjAlgRhs rhs
 isInjectiveTyCon (SynonymTyCon {})             _                = False
 isInjectiveTyCon (FamilyTyCon {})              _                = False
 isInjectiveTyCon (PrimTyCon {})                _                = True
@@ -1230,6 +1231,7 @@ isInjectiveTyCon (PromotedTyCon {ty_con = tc}) r
 -- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
 -- (where X is the role passed in):
 --   If (T tys ~X t), then (t's head ~X T).
+-- See also Note [Decomposing equalities] in TcCanonical
 isGenerativeTyCon :: TyCon -> Role -> Bool
 isGenerativeTyCon = isInjectiveTyCon
   -- as it happens, generativity and injectivity coincide, but there's
@@ -1237,12 +1239,12 @@ isGenerativeTyCon = isInjectiveTyCon
 
 -- | Is this an 'AlgTyConRhs' of a 'TyCon' that is generative and injective
 -- with respect to representational equality?
-isDistinctAlgRhs :: AlgTyConRhs -> Bool
-isDistinctAlgRhs (TupleTyCon {})          = True
-isDistinctAlgRhs (DataTyCon {})           = True
-isDistinctAlgRhs (DataFamilyTyCon {})     = False
-isDistinctAlgRhs (AbstractTyCon distinct) = distinct
-isDistinctAlgRhs (NewTyCon {})            = False
+isGenInjAlgRhs :: AlgTyConRhs -> Bool
+isGenInjAlgRhs (TupleTyCon {})          = True
+isGenInjAlgRhs (DataTyCon {})           = True
+isGenInjAlgRhs (DataFamilyTyCon {})     = False
+isGenInjAlgRhs (AbstractTyCon distinct) = distinct
+isGenInjAlgRhs (NewTyCon {})            = False
 
 -- | Is this 'TyCon' that for a @newtype@
 isNewTyCon :: TyCon -> Bool
@@ -1332,6 +1334,8 @@ isTypeSynonymTyCon _                 = False
 mightBeUnsaturatedTyCon :: TyCon -> Bool
 -- True iff we can decompose (T a b c) into ((T a b) c)
 --   I.e. is it injective and generative w.r.t nominal equality?
+--   That is, if (T a b) ~N d e f, is it always the case that
+--            (T ~N d), (a ~N e) and (b ~N f)?
 -- Specifically NOT true of synonyms (open and otherwise)
 --
 -- It'd be unusual to call mightBeUnsaturatedTyCon on a regular H98