Skolem escape errors are not always reported as such

This program is correctly rejected, but with an unhelpful error message:

{-# LANGUAGE ExistentialQuantification #-}
module SK where

data Bar = forall a. Bar a

foo :: a -> ()
foo _ = ()

get :: Bar -> ()
get x = foo (case x of Bar a -> a)

SK.hs:10:33: error:
    • Couldn't match expected type ‘a0’ with actual type ‘a’
      ‘a’ is a rigid type variable bound by
        a pattern with constructor: Bar :: forall a. a -> Bar,
        in a case alternative
        at SK.hs:10:24-28
    • In the expression: a
      In a case alternative: Bar a -> a
      In the first argument of ‘foo’, namely ‘(case x of { Bar a -> a })’
    • Relevant bindings include
        a :: a (bound at SK.hs:10:28)
   |
10 | get x = foo (case x of Bar a -> a)
   |                                 ^

The root cause of the problem is an escaped skolem, namely a, but the error message does not actually say that anywhere, making it quite confusing. The a0 variable is clearly a unification variable, so it is not obvious why it isn’t allowed to unify with a.

The root cause of this issue is twofold:

1. During typechecking, we end up with the unsolvable wanted equality a_ane[ssk:1] ~# a0_anb[tau:0]. The skolem will always be placed on the left, since swapOverTyVars prefers to put deeper tyvar on the left (as justified by Note [Deeper level on the left] and #15009 (closed)).

2. But mkTyVarEqErr' incorrectly assumes that if a skolem is on the left, a meta tyvar won’t ever be on the right. This assumption is outdated since 2bbdd00c, which first landed in GHC 8.6.

The culprit here appears to be mkTyVarEqErr', which should probably be modified to flip the equality around on its own if the left side is a skolem and the right side is a meta tyvar. Here’s a patch that does exactly that:

diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index ae08f78443..8729de501f 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -1485,10 +1485,14 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
        ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 }

 mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2
+  | isUserSkolem ctxt tv1             -- if tv1 is a skolem and ty2 is a meta-tyvar,
+  , Just tv2 <- tcGetTyVar_maybe ty2  --   flip the equality around so that we
+  , isMetaTyVar tv2                   --   report skolem escape errors (see #18114)
+  = mkTyVarEqErr' dflags ctxt report ct (flipSwap <$> oriented) tv2 ty1
+
   | not insoluble_occurs_check   -- See Note [Occurs check wins]
-  , isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
-                            -- be oriented the other way round;
-                            -- see GHC.Tc.Solver.Canonical.canEqTyVarTyVar
+  , isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else we would have
+                            -- flipped it around in the previous case
     || isTyVarTyVar tv1 && not (isTyVarTy ty2)
     || ctEqRel ct == ReprEq
      -- the cases below don't really apply to ReprEq (except occurs check)

This appears to fix the issue, yielding a much nicer error message on the above program:

SK.hs:10:33: error:
    • Couldn't match expected type ‘a0’ with actual type ‘a’
        because type variable ‘a’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a pattern with constructor: Bar :: forall a. a -> Bar,
        in a case alternative
        at SK.hs:10:24-28
    • In the expression: a
      In a case alternative: Bar a -> a
      In the first argument of ‘foo’, namely ‘(case x of { Bar a -> a })’
    • Relevant bindings include
        a :: a (bound at SK.hs:10:28)
   |
10 | get x = foo (case x of Bar a -> a)
   |                                 ^

It needs a test case, but unless anyone has any objections, I intend to open an MR with the above patch soon.