[commit: ghc] master: Fix #10493. (ace8d4f)

[git at git.haskell.org]

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

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

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

commit ace8d4fcfd798b70c34e325c562878b0a8f5e2cb
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Mon Jun 8 16:46:46 2015 -0400

    Fix #10493.
    
    Now, a Coercible (T1 ...) (T2 ...) constraint is insoluble only
    when both T1 and T2 say "yes" to isDistinctTyCon. Several comments
    also updated in this patch.


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

ace8d4fcfd798b70c34e325c562878b0a8f5e2cb
 compiler/typecheck/TcCanonical.hs                  | 11 +++++++++--
 compiler/types/TyCon.hs                            |  2 +-
 compiler/types/Unify.hs                            | 11 +++++++++--
 testsuite/tests/typecheck/should_compile/T10493.hs |  9 +++++++++
 testsuite/tests/typecheck/should_compile/all.T     |  1 +
 5 files changed, 29 insertions(+), 5 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index ab9d2c2..e69f12d 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -665,7 +665,7 @@ canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
 
   -- Fail straight away for better error messages
   -- See Note [Use canEqFailure in canDecomposableTyConApp]
-  | isDataFamilyTyCon tc1 || isDataFamilyTyCon tc2
+  | eq_rel == ReprEq && not (isDistinctTyCon tc1 && isDistinctTyCon tc2)
   = canEqFailure ev eq_rel ty1 ty2
   | otherwise
   = canEqHardFailure ev eq_rel ty1 ty2
@@ -678,7 +678,7 @@ Note [Use canEqFailure in canDecomposableTyConApp]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We must use canEqFailure, not canEqHardFailure here, because there is
 the possibility of success if working with a representational equality.
-Here is the case:
+Here is one case:
 
   type family TF a where TF Char = Bool
   data family DF a
@@ -688,6 +688,13 @@ Suppose we are canonicalising (Int ~R DF (T a)), where we don't yet
 know `a`. This is *not* a hard failure, because we might soon learn
 that `a` is, in fact, Char, and then the equality succeeds.
 
+Here is another case:
+
+  [G] Coercible Age Int
+
+where Age's constructor is not in scope. We don't want to report
+an "inaccessible code" error in the context of this Given!
+
 Note [Decomposing newtypes]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 As explained in Note [NthCo and newtypes] in Coercion, we can't use
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 94fba28..71111c0 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -1211,7 +1211,7 @@ isDataTyCon (AlgTyCon {algTcRhs = rhs})
 isDataTyCon _ = False
 
 -- | 'isDistinctTyCon' is true of 'TyCon's that are equal only to
--- themselves, even via coercions (except for unsafeCoerce).
+-- themselves, even via representational coercions (except for unsafeCoerce).
 -- This excludes newtypes, type functions, type synonyms.
 -- It relates directly to the FC consistency story:
 --     If the axioms are consistent,
diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index 0bfcfab..218dc99 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -280,8 +280,8 @@ to 'Bool', in which case x::T Int, so
 Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom)
 value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
 gives a coercion
-        CoX :: X ~ Int
-So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
+        CoX :: X ~R Int
+So (T CoX)_R :: T X ~R T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
 of type (T X) constructed with T1.  Hence
         ANSWER = NO we can't prune the T1 branch (surprisingly)
 
@@ -317,6 +317,13 @@ drop more and more dead code.
 For now we implement a very simple test: type variables match
 anything, type functions (incl newtypes) match anything, and only
 distinct data types fail to match.  We can elaborate later.
+
+NB: typesCantMatch is subtly different than the apartness checks
+elsewhere in this module. It reasons over *representational* equality
+(saying that a newtype is not distinct from its representation) whereas
+the checks in, say, tcUnifyTysFG are about *nominal* equality. tcUnifyTysFG
+also assumes that its inputs are type-family-free, whereas no such assumption
+is in play here.
 -}
 
 typesCantMatch :: [(Type,Type)] -> Bool
diff --git a/testsuite/tests/typecheck/should_compile/T10493.hs b/testsuite/tests/typecheck/should_compile/T10493.hs
new file mode 100644
index 0000000..3e3caae
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T10493.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+module T10493 where
+
+import Data.Coerce
+import Data.Ord (Down)  -- no constructor
+
+foo :: Coercible (Down Int) Int => Down Int -> Int
+foo = coerce
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 1f5623d..e26d27a 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -460,3 +460,4 @@ test('T10423', normal, compile, [''])
 test('T10489', normal, compile, [''])
 test('T10348', normal, compile, [''])
 test('T10494', normal, compile, [''])
+test('T10493', normal, compile, [''])