[commit: ghc] master: Stop marking soluble ~R# constraints as insoluble (f0d27f5)

[git at git.haskell.org]

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

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

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

commit f0d27f515ffbc476144d1d1dd1a71bf9fa93c94b
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon Jul 23 15:33:13 2018 +0100

    Stop marking soluble ~R# constraints as insoluble
    
    We had a constraint (a b ~R# Int), and were marking it as 'insoluble'.
    That's bad; it isn't.  And it caused Trac #15431. Soultion is simple.
    
    I did a tiny refactor on can_eq_app, so that it is used only for
    nominal equalities.


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

f0d27f515ffbc476144d1d1dd1a71bf9fa93c94b
 compiler/typecheck/TcCanonical.hs                  | 39 +++++++++++++---------
 testsuite/tests/typecheck/should_compile/T15431.hs | 15 +++++++++
 .../tests/typecheck/should_compile/T15431a.hs      | 12 +++++++
 testsuite/tests/typecheck/should_compile/all.T     |  2 ++
 4 files changed, 53 insertions(+), 15 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 42f28c7..c45afd2 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -894,11 +894,13 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel
 
 -- See Note [Canonicalising type applications] about why we require flat types
 can_eq_nc' True _rdr_env _envs ev eq_rel (AppTy t1 s1) _ ty2 _
-  | Just (t2, s2) <- tcSplitAppTy_maybe ty2
-  = can_eq_app ev eq_rel t1 s1 t2 s2
+  | NomEq <- eq_rel
+  , Just (t2, s2) <- tcSplitAppTy_maybe ty2
+  = can_eq_app ev t1 s1 t2 s2
 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 _ (AppTy t2 s2) _
-  | Just (t1, s1) <- tcSplitAppTy_maybe ty1
-  = can_eq_app ev eq_rel t1 s1 t2 s2
+  | NomEq <- eq_rel
+  , Just (t1, s1) <- tcSplitAppTy_maybe ty1
+  = can_eq_app ev t1 s1 t2 s2
 
 -- No similarity in type structure detected. Flatten and try again.
 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
@@ -908,9 +910,22 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
        ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
 
 -- We've flattened and the types don't match. Give up.
-can_eq_nc' True _rdr_env _envs ev _eq_rel _ ps_ty1 _ ps_ty2
+can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
   = do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
-       ; canEqHardFailure ev ps_ty1 ps_ty2 }
+       ; case eq_rel of -- See Note [Unsolved equalities]
+            ReprEq -> continueWith (mkIrredCt ev)
+            NomEq  -> continueWith (mkInsolubleCt ev) }
+          -- No need to call canEqFailure/canEqHardFailure because they
+          -- flatten, and the types involved here are already flat
+
+{- Note [Unsolved equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we have an unsolved equality like
+  (a b ~R# Int)
+that is not necessarily insoluble!  Maybe 'a' will turn out to be a newtype.
+So we want to make it a potentially-soluble Irred not an insoluble one.
+Missing this point is what caused Trac #15431
+-}
 
 ---------------------------------
 can_eq_nc_forall :: CtEvidence -> EqRel
@@ -1220,8 +1235,8 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
 ---------
 -- ^ Decompose a type application.
 -- All input types must be flat. See Note [Canonicalising type applications]
-can_eq_app :: CtEvidence       -- :: s1 t1 ~r s2 t2
-           -> EqRel            -- r
+-- Nominal equality only!
+can_eq_app :: CtEvidence       -- :: s1 t1 ~N s2 t2
            -> Xi -> Xi         -- s1 t1
            -> Xi -> Xi         -- s2 t2
            -> TcS (StopOrContinue Ct)
@@ -1229,13 +1244,7 @@ can_eq_app :: CtEvidence       -- :: s1 t1 ~r s2 t2
 -- AppTys only decompose for nominal equality, so this case just leads
 -- to an irreducible constraint; see typecheck/should_compile/T10494
 -- See Note [Decomposing equality], note {4}
-can_eq_app ev ReprEq _ _ _ _
-  = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
-       ; continueWith (mkIrredCt ev) }
-          -- no need to call canEqFailure, because that flattens, and the
-          -- types involved here are already flat
-
-can_eq_app ev NomEq s1 t1 s2 t2
+can_eq_app ev s1 t1 s2 t2
   | CtDerived { ctev_loc = loc } <- ev
   = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
        ; stopWith ev "Decomposed [D] AppTy" }
diff --git a/testsuite/tests/typecheck/should_compile/T15431.hs b/testsuite/tests/typecheck/should_compile/T15431.hs
new file mode 100644
index 0000000..21fa4c4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15431.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE GADTs, FlexibleContexts #-}
+
+module T15431 where
+
+import Data.Coerce
+
+data T t where
+  A :: Show (t a) => t a -> T t
+  B :: Coercible Int (t a) => t a -> T t
+
+f :: T t -> String
+f (A t) = show t
+
+g :: T t -> Int
+g (B t) = coerce t
diff --git a/testsuite/tests/typecheck/should_compile/T15431a.hs b/testsuite/tests/typecheck/should_compile/T15431a.hs
new file mode 100644
index 0000000..cf5a831
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15431a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+module T15431a where
+
+import Data.Coerce
+import Data.Functor.Identity
+
+g1 :: Coercible (t a) Int => t a -> Int
+g1 = coerce
+
+g2 :: Coercible Int (t a) => t a -> Int
+g2 = coerce
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 10295f5..6babe4e 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -640,3 +640,5 @@ def onlyHsParLocs(x):
                         and not "<no location info>" in loc)
     return '\n'.join(filteredLines)
 test('T15242', normalise_errmsg_fun(onlyHsParLocs), compile, [''])
+test('T15431', normal, compile, [''])
+test('T15431a', normal, compile, [''])