Narrow the dont-decompose-newtype testwip/T22924

Following #22924 this patch narrows the test that stops
us decomposing newtypes.  The key change is the use of
noGivenNewtypeReprEqs in GHC.Tc.Solver.Canonical.canTyConApp.

We went to and fro on the solution, as you can see in #22924.
The result is carefully documented in
  Note [Decomoposing newtype equalities]

On the way I had revert most of
  commit 3e827c3f74ef76d90d79ab6c4e71aa954a1a6b90
  Author: Richard Eisenberg <rae@cs.brynmawr.edu>
  Date:   Mon Dec 5 10:14:02 2022 -0500

    Do newtype unwrapping in the canonicaliser and rewriter

    See Note [Unwrap newtypes first], which has the details.

It turns out that

(a) 3e827c3f makes GHC behave worse on some recursive newtypes
    (see one of the tests on this commit)
(b) the finer-grained test (namely noGivenNewtypeReprEqs) renders
    3e827c3f unnecessary

1 files changed, 13 insertions, 57 deletions

diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index b4e4b25a29..16ab2471b3 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -42,7 +42,6 @@ import GHC.Builtin.Types (tYPETyCon)
 import Data.List ( find )
 import GHC.Data.List.Infinite (Infinite)
 import qualified GHC.Data.List.Infinite as Inf
-import GHC.Tc.Instance.Family (tcTopNormaliseNewTypeTF_maybe)
 
 {-
 ************************************************************************
@@ -225,10 +224,10 @@ rewrite ev ty
        ; return result }
 
 -- | See Note [Rewriting]
--- This variant of 'rewrite' rewrites w.r.t. nominal equality only,
--- as this is better than full rewriting for error messages. Specifically,
--- we want to avoid unwrapping newtypes, as doing so can end up causing
--- an otherwise-unnecessary stack overflow.
+-- `rewriteForErrors` is a variant of 'rewrite' that rewrites
+-- w.r.t. nominal equality only, as this is better than full rewriting
+-- for error messages. (This was important when we flirted with rewriting
+-- newtypes but perhaps less so now.)
 rewriteForErrors :: CtEvidence -> TcType
                  -> TcS (Reduction, RewriterSet)
 rewriteForErrors ev ty
@@ -499,27 +498,14 @@ rewrite_one (TyVarTy tv)
 rewrite_one (AppTy ty1 ty2)
   = rewrite_app_tys ty1 [ty2]
 
-rewrite_one ty@(TyConApp tc tys)
+rewrite_one (TyConApp tc tys)
   -- If it's a type family application, try to reduce it
   | isTypeFamilyTyCon tc
   = rewrite_fam_app tc tys
 
-  | otherwise
-  = do { eq_rel <- getEqRel
-       ; if eq_rel == ReprEq
-
-         then -- Rewriting w.r.t. representational equality requires
-              --   unwrapping newtypes; see GHC.Tc.Solver.Canonical.
-              --   Note [Unwrap newtypes first]
-              -- NB: try rewrite_newtype_app even when tc isn't a newtype;
-              -- the allows the possibility of having a newtype buried under
-              -- a synonym. Needed for e.g. T12067.
-              rewrite_newtype_app ty
-
-         else -- For * a normal data type application
-              --     * data family application
-              -- we just recursively rewrite the arguments.
-              rewrite_ty_con_app tc tys }
+  | otherwise -- We just recursively rewrite the arguments.
+              -- See Note [Do not rewrite newtypes]
+  = rewrite_ty_con_app tc tys
 
 rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
   = do { arg_redn <- rewrite_one ty1
@@ -678,42 +664,12 @@ rewrite_vector ki roles tys
     fvs                                = tyCoVarsOfType ki
 {-# INLINE rewrite_vector #-}
 
--- Rewrite a (potential) newtype application
--- Precondition: the ambient EqRel is ReprEq
--- Precondition: the type is a TyConApp
--- See Note [Newtypes can blow the stack]
-rewrite_newtype_app :: TcType -> RewriteM Reduction
-rewrite_newtype_app ty@(TyConApp tc tys)
-  = do { rdr_env <- liftTcS getGlobalRdrEnvTcS
-       ; tf_envs <- liftTcS getFamInstEnvs
-       ; case (tcTopNormaliseNewTypeTF_maybe tf_envs rdr_env ty) of
-           Nothing -> -- Non-newtype or abstract newtype
-                      rewrite_ty_con_app tc tys
-
-           Just ((used_ctors, co), ty')   -- co :: ty ~ ty'
-             -> do { liftTcS $ recordUsedGREs used_ctors
-                   ; checkStackDepth ty
-                   ; rewrite_reduction (Reduction co ty') } }
-
-rewrite_newtype_app other_ty = pprPanic "rewrite_newtype_app" (ppr other_ty)
-
-{- Note [Newtypes can blow the stack]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have
-
-  newtype X = MkX (Int -> X)
-  newtype Y = MkY (Int -> Y)
-
-and now wish to prove
-
-  [W] X ~R Y
 
-This Wanted will loop, expanding out the newtypes ever deeper looking
-for a solid match or a solid discrepancy. Indeed, there is something
-appropriate to this looping, because X and Y *do* have the same representation,
-in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
-coercion will ever witness it. This loop won't actually cause GHC to hang,
-though, because we check our depth when unwrapping newtypes.
+{- Note [Do not rewrite newtypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We flirted with unwrapping newtypes in the rewriter -- see GHC.Tc.Solver.Canonical
+Note [Unwrap newtypes first]. But that turned out to be a bad idea because
+of recursive newtypes, as that Note says.  So be careful if you re-add it!
 
 Note [Rewriting synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~