[commit: ghc] master: Do not unify representational equalities (ae292c6)

[git at git.haskell.org]

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

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

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

commit ae292c6d1362f34117be75a2553049cec7022244
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri May 18 13:58:25 2018 +0100

    Do not unify representational equalities
    
    This patch is an easy fix to Trac #15144, which was caused
    by accidentally unifying a representational equality in the
    unflattener.  (The main code in TcInteract was always careful
    not to do so, but I'd missed the test in the unflattener.)
    
    See Note [Do not unify representational equalities]
    in TcInteract


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

ae292c6d1362f34117be75a2553049cec7022244
 compiler/typecheck/TcFlatten.hs                      |  5 ++++-
 compiler/typecheck/TcInteract.hs                     | 20 ++++++++++++++++++--
 .../tests/indexed-types/should_compile/T15144.hs     | 18 ++++++++++++++++++
 testsuite/tests/indexed-types/should_compile/all.T   |  1 +
 4 files changed, 41 insertions(+), 3 deletions(-)

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 45435a1..e2244a9 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -2015,7 +2015,10 @@ unflattenWanteds tv_eqs funeqs
     unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts
     unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv
                                     , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
-      | isFmvTyVar tv   -- Previously these fmvs were untouchable,
+
+      | NomEq <- eq_rel -- See Note [Do not unify representational equalities]
+                        --     in TcInteract
+      , isFmvTyVar tv   -- Previously these fmvs were untouchable,
                         -- but now they are touchable
                         -- NB: unlike unflattenFmv, filling a fmv here /does/
                         --     bump the unification count; it is "improvement"
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index c71a01a..7f85d6b 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1600,8 +1600,8 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
 
        ; stopWith ev "Solved from inert" }
 
-  | ReprEq <- eq_rel   -- We never solve representational
-  = unsolved_inert     -- equalities by unification
+  | ReprEq <- eq_rel   -- See Note [Do not unify representational equalities]
+  = unsolved_inert
 
   | isGiven ev         -- See Note [Touchables and givens]
   = unsolved_inert
@@ -1672,6 +1672,22 @@ See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
 double unifications is the main reason we disallow touchable
 unification variables as RHS of type family equations: F xis ~ alpha.
 
+Note [Do not unify representational equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider   [W] alpha ~R# b
+where alpha is touchable. Should we unify alpha := b?
+
+Certainly not!  Unifying forces alpha and be to be the same; but they
+only need to be representationally equal types.
+
+For example, we might have another constraint [W] alpha ~# N b
+where
+  newtype N b = MkN b
+and we want to get alpha := N b.
+
+See also Trac #15144, which was caused by unifying a representational
+equality (in the unflattener).
+
 
 ************************************************************************
 *                                                                      *
diff --git a/testsuite/tests/indexed-types/should_compile/T15144.hs b/testsuite/tests/indexed-types/should_compile/T15144.hs
new file mode 100644
index 0000000..c6f0856
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T15144.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+module T15144 where
+
+import Data.Coerce
+import Data.Proxy
+
+type family F x
+
+f :: Coercible (F a) b => Proxy a -> F a -> b
+f _ = coerce
+
+-- In #15144, we inferred the less-general type
+-- g :: Proxy a -> F a -> F a
+g p x = f p x
+
+h :: Coercible (F a) b => Proxy a -> F a -> b
+h p x = g p x
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 6074a35..9f0d9b4 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -280,3 +280,4 @@ test('T14237', normal, compile, [''])
 test('T14554', normal, compile, [''])
 test('T14680', normal, compile, [''])
 test('T15057', normal, compile, [''])
+test('T15144', normal, compile, [''])