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

2 files changed, 22 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).
+
 
 ************************************************************************
 *                                                                      *