From 2b55cb5f33666a71eaac7968c59e483860112e5c Mon Sep 17 00:00:00 2001
From: sheaf <sam.derbyshire@gmail.com>
Date: Mon, 3 Jul 2023 18:23:47 +0200
Subject: [PATCH] Reinstate untouchable variable error messages

This extra bit of information was accidentally being discarded after
a refactoring of the way we reported problems when unifying a type
variable with another type. This patch rectifies that.
---
 compiler/GHC/Tc/Errors/Ppr.hs                 | 21 +++++++++++--------
 compiler/GHC/Tc/Errors/Types.hs               |  8 -------
 compiler/GHC/Types/Error/Codes.hs             |  2 +-
 testsuite/tests/ado/T16135.stderr             |  5 +++++
 .../should_compile/Simple14.stderr            | 13 ++++++++----
 .../tests/typecheck/should_fail/T21338.stderr | 16 ++++++++++----
 6 files changed, 39 insertions(+), 26 deletions(-)

diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 6c875434a695..91278ad6807b 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -21,6 +21,7 @@ module GHC.Tc.Errors.Ppr
   , inHsDocContext
   , TcRnMessageOpts(..)
   , pprTyThingUsedWrong
+  , pprUntouchableVariable
 
   -- | Useful when overriding message printing.
   , messageWithInfoDiagnosticMessage
@@ -3726,13 +3727,6 @@ pprTcSolverReportMsg _ (FixedRuntimeRepError frr_origs) =
           = quotes (text "Levity")
           | otherwise
           = text "type"
-pprTcSolverReportMsg _ (UntouchableVariable tv implic)
-  | Implic { ic_given = given, ic_info = skol_info } <- implic
-  = sep [ quotes (ppr tv) <+> text "is untouchable"
-        , nest 2 $ text "inside the constraints:" <+> pprEvVarTheta given
-        , nest 2 $ text "bound by" <+> ppr skol_info
-        , nest 2 $ text "at" <+>
-          ppr (getCtLocEnvLoc (ic_env implic)) ]
 pprTcSolverReportMsg _ (BlockedEquality item) =
   vcat [ hang (text "Cannot use equality for substitution:")
            2 (ppr (errorItemPred item))
@@ -4004,6 +3998,13 @@ pprCannotUnifyVariableReason ctxt (RepresentationalEq tv_info mb_coercible_msg)
   = pprTyVarInfo ctxt tv_info
   $$ maybe empty pprCoercibleMsg mb_coercible_msg
 
+pprUntouchableVariable :: TcTyVar -> Implication -> SDoc
+pprUntouchableVariable tv (Implic { ic_given = given, ic_info = skol_info, ic_env = env })
+  = sep [ quotes (ppr tv) <+> text "is untouchable"
+        , nest 2 $ text "inside the constraints:" <+> pprEvVarTheta given
+        , nest 2 $ text "bound by" <+> ppr skol_info
+        , nest 2 $ text "at" <+> ppr (getCtLocEnvLoc env) ]
+
 pprMismatchMsg :: SolverReportErrCtxt -> MismatchMsg -> SDoc
 pprMismatchMsg ctxt
   (BasicMismatch { mismatch_ea   = ea
@@ -4486,8 +4487,10 @@ pprWhenMatching ctxt (WhenMatching cty1 cty2 sub_o mb_sub_t_or_k) =
         Right msg  -> pprMismatchMsg ctxt msg
 
 pprTyVarInfo :: SolverReportErrCtxt -> TyVarInfo -> SDoc
-pprTyVarInfo ctxt (TyVarInfo { thisTyVar = tv1, otherTy = mb_tv2 }) =
-  mk_msg tv1 $$ case mb_tv2 of { Nothing -> empty; Just tv2 -> mk_msg tv2 }
+pprTyVarInfo ctxt (TyVarInfo { thisTyVar = tv1, otherTy = mb_tv2, thisTyVarIsUntouchable = mb_implic })
+  = vcat [ mk_msg tv1
+         , maybe empty (pprUntouchableVariable tv1) mb_implic
+         , case mb_tv2 of { Nothing -> empty; Just tv2 -> mk_msg tv2 } ]
   where
     mk_msg tv = case tcTyVarDetails tv of
       SkolemTv sk_info _ _ -> pprSkols ctxt [(getSkolemInfo sk_info, [tv])]
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index fc41719d8304..cd5afbf9e66c 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -4987,14 +4987,6 @@ data TcSolverReportMsg
   -- See 'HoleError'.
   | ReportHoleError Hole HoleError
 
-  -- | Trying to unify an untouchable variable, e.g. a variable from an outer scope.
-  --
-  -- Test case: Simple14
-  | UntouchableVariable
-    { untouchableTyVar :: TyVar
-    , untouchableTyVarImplication :: Implication
-    }
-
   -- | Cannot unify a variable, because of a type mismatch.
   | CannotUnifyVariable
     { mismatchMsg         :: MismatchMsg
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index edc4211c3b16..b1aadbfb58a8 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -306,7 +306,6 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "UserTypeError"                                 = 64725
   GhcDiagnosticCode "UnsatisfiableError"                            = 22250
   GhcDiagnosticCode "ReportHoleError"                               = 88464
-  GhcDiagnosticCode "UntouchableVariable"                           = 34699
   GhcDiagnosticCode "FixedRuntimeRepError"                          = 55287
   GhcDiagnosticCode "BlockedEquality"                               = 06200
   GhcDiagnosticCode "ExpectingMoreArguments"                        = 81325
@@ -851,6 +850,7 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnUnexpectedTypeSplice"                      = 39180
   GhcDiagnosticCode "PsErrUnexpectedTypeAppInDecl"                  = 45054
   GhcDiagnosticCode "TcRnUnpromotableThing"                         = 88634
+  GhcDiagnosticCode "UntouchableVariable"                           = 34699
 
 {- *********************************************************************
 *                                                                      *
diff --git a/testsuite/tests/ado/T16135.stderr b/testsuite/tests/ado/T16135.stderr
index e6a77cdfe606..7b27716fb489 100644
--- a/testsuite/tests/ado/T16135.stderr
+++ b/testsuite/tests/ado/T16135.stderr
@@ -2,6 +2,11 @@ T16135.hs:11:18: error: [GHC-83865]
     • Couldn't match type ‘a0’ with ‘a’
       Expected: f a0
         Actual: f a
+      ‘a0’ is untouchable
+        inside the constraints: Functor f
+        bound by the type signature for:
+                   runf :: forall (f :: * -> *). Functor f => IO (T f)
+        at T16135.hs:7:1-39
       ‘a’ is a rigid type variable bound by
         a pattern with constructor:
           MkT :: forall {k} (f :: k -> *) (a :: k). f a -> T f,
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.stderr b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
index 50a708440fec..e008318859c6 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.stderr
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
@@ -3,10 +3,15 @@ Simple14.hs:22:27: error: [GHC-83865]
     • Couldn't match type ‘z0’ with ‘n’
       Expected: EQ_ z0 z0
         Actual: EQ_ m n
-        ‘n’ is a rigid type variable bound by
-          the type signature for:
-            foo :: forall m n. EQ_ (Maybe m) (Maybe n)
-          at Simple14.hs:21:1-42
+      ‘z0’ is untouchable
+        inside the constraints: Maybe m ~ Maybe n
+        bound by a type expected by the context:
+                   (Maybe m ~ Maybe n) => EQ_ z0 z0
+        at Simple14.hs:22:26-41
+      ‘n’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall m n. EQ_ (Maybe m) (Maybe n)
+        at Simple14.hs:21:1-42
     • In the second argument of ‘eqE’, namely ‘(eqI :: EQ_ m n)’
       In the expression: x `eqE` (eqI :: EQ_ m n)
       In the first argument of ‘ntI’, namely
diff --git a/testsuite/tests/typecheck/should_fail/T21338.stderr b/testsuite/tests/typecheck/should_fail/T21338.stderr
index 4fed65d7af0e..1e6802002a2e 100644
--- a/testsuite/tests/typecheck/should_fail/T21338.stderr
+++ b/testsuite/tests/typecheck/should_fail/T21338.stderr
@@ -3,10 +3,18 @@ T21338.hs:38:24: error: [GHC-83865]
     • Couldn't match type ‘flds0’ with ‘flds’
       Expected: NP (K String) flds
         Actual: NP (K String) flds0
-        ‘flds’ is a rigid type variable bound by
-          the type signature for:
-            fieldNames :: forall a (flds :: [*]). NP (K String) flds
-          at T21338.hs:36:1-57
+      ‘flds0’ is untouchable
+        inside the constraints: All flds0
+        bound by a pattern with constructor:
+                   Record :: forall (xs :: [*]).
+                             All xs =>
+                             NP (K String) xs -> ConstructorInfo xs,
+                 in a case alternative
+        at T21338.hs:38:3-11
+      ‘flds’ is a rigid type variable bound by
+        the type signature for:
+          fieldNames :: forall a (flds :: [*]). NP (K String) flds
+        at T21338.hs:36:1-57
     • In the second argument of ‘hmap’, namely ‘np’
       In the expression: hmap id np
       In a case alternative: Record np -> hmap id np
-- 
GitLab