Float representational equaliieswip/T18213

This draft patch (tests and better commit msg to come) improves
the solver by floating all equality constraints out of an
implication that does not allow term-level bindings.

Fixes #18213

3 files changed, 20 insertions, 10 deletions

diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 134b230c06..d4a739a7ae 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -2421,14 +2421,24 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
     -- Identify which equalities are candidates for floating
     -- Float out alpha ~ ty, or ty ~ alpha which might be unified outside
     -- See Note [Which equalities to float]
-    is_float_eq_candidate ct
-      | pred <- ctPred ct
-      , EqPred NomEq ty1 ty2 <- classifyPredType pred
+    is_float_eq_candidate ct = float_help (classifyPredType (ctPred ct))
+
+    term_ev_allowed = termEvidenceAllowed ev_binds_var
+
+    float_help (EqPred {}) | not term_ev_allowed = True
+       -- If term evidence is not allowed, try floating any
+       -- equality (both NomEq and ReprEq) in the hope that it
+       -- may be soluble higher up, where term evidence is allowed
+       -- See #18213
+
+    float_help (EqPred NomEq ty1 ty2)
+      -- NomEq only; ReprEq doesn't cause unification
       = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
           (Just tv1, _) -> float_tv_eq_candidate tv1 ty2
           (_, Just tv2) -> float_tv_eq_candidate tv2 ty1
           _             -> False
-      | otherwise = False
+
+    float_help _ = False
 
     float_tv_eq_candidate tv1 ty2  -- See Note [Which equalities to float]
       =  isMetaTyVar tv1
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index d95c13cd54..799a6197dc 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -1079,7 +1079,7 @@ shortCutSolver dflags ev_w ev_i
  && gopt Opt_SolveConstantDicts dflags
  -- Enabled by the -fsolve-constant-dicts flag
   = do { ev_binds_var <- getTcEvBindsVar
-       ; ev_binds <- ASSERT2( not (isCoEvBindsVar ev_binds_var ), ppr ev_w )
+       ; ev_binds <- ASSERT2( termEvidenceAllowed ev_binds_var, ppr ev_w )
                      getTcEvBindsMap ev_binds_var
        ; solved_dicts <- getSolvedDicts
 
@@ -2386,7 +2386,7 @@ chooseInstance work_item
       -- Precondition: evidence term matches the predicate workItem
      finish_wanted loc theta mk_ev
         = do { evb <- getTcEvBindsVar
-             ; if isCoEvBindsVar evb
+             ; if not (termEvidenceAllowed evb)
                then -- See Note [Instances in no-evidence implications]
                     continueWith work_item
                else
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs
index 8649871670..397d53154b 100644
--- a/compiler/GHC/Tc/Types/Evidence.hs
+++ b/compiler/GHC/Tc/Types/Evidence.hs
@@ -22,7 +22,7 @@ module GHC.Tc.Types.Evidence (
   evBindMapToVarSet,
   varSetMinusEvBindMap,
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
-  evBindVar, isCoEvBindsVar,
+  evBindVar, termEvidenceAllowed,
 
   -- * EvTerm (already a CoreExpr)
   EvTerm(..), EvExpr,
@@ -453,9 +453,9 @@ evidence bindings are allowed.  Notebly ():
   - When unifying forall-types
 -}
 
-isCoEvBindsVar :: EvBindsVar -> Bool
-isCoEvBindsVar (CoEvBindsVar {}) = True
-isCoEvBindsVar (EvBindsVar {})   = False
+termEvidenceAllowed :: EvBindsVar -> Bool
+termEvidenceAllowed (CoEvBindsVar {}) = False
+termEvidenceAllowed (EvBindsVar {})   = True
 
 -----------------
 newtype EvBindMap