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

4 files changed, 41 insertions, 3 deletions

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 45435a145e..e2244a99e6 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 c71a01aa6c..7f85d6b055 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 0000000000..c6f0856184
--- /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 6074a3597e..9f0d9b4a8d 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, [''])