Confusing interaction of pattern synonyms and view patterns

Summary

I'm using the bug report template, but I'm not entirely convinced it's a bug. Anyway.

This code rather surprisingly fails to compile:

{-# LANGUAGE PatternSynonyms, GADTs, ViewPatterns #-}

import Data.Typeable

data Gadt x y where
  ExistentialInGadt :: Typeable a => a -> Gadt x x

pattern CastGadt :: Typeable a => x ~ y => a -> Gadt x y
pattern CastGadt a <- ExistentialInGadt (cast -> Just a)

test :: Gadt i o -> Bool
test gadt = case gadt of
  CastGadt a -> a
  _ -> False

The complete error message says:

test.hs:13:3: error:
    • No instance for (Typeable a0) arising from a pattern
    • In the pattern: CastGadt a
      In a case alternative: CastGadt a -> a
      In the expression:
        case gadt of
          CastGadt a -> a
          _ -> False
   |
13 |   CastGadt a -> a
   |   ^^^^^^^^^^

test.hs:13:17: error:
    • Couldn't match expected type ‘Bool’ with actual type ‘a0’
        ‘a0’ is untouchable
          inside the constraints: i ~ o
          bound by a pattern with pattern synonym:
                     CastGadt :: forall a x y. Typeable a => (x ~ y) => a -> Gadt x y,
                   in a case alternative
          at test.hs:13:3-12
    • In the expression: a
      In a case alternative: CastGadt a -> a
      In the expression:
        case gadt of
          CastGadt a -> a
          _ -> False
    • Relevant bindings include a :: a0 (bound at test.hs:13:12)
   |
13 |   CastGadt a -> a
   |                 ^

Note that Typeable isn't particularly relevant here, and neither are GADTs, those are used for illustrative purposes -- the crux of the issue is given constraints on a pattern synonym using a view pattern that needs the required constraints.

It's not obvious why GHC insists a0 is untouchable. What's even more confusing, a pattern synonym without given constraints works as expected (i.e. it doesn't provide the constraint x ~ y, but it does compile):

-- this compiles fine
pattern CastGadtNoGivens :: Typeable a => a -> Gadt x y
pattern CastGadtNoGivens a <- ExistentialInGadt (cast -> Just a)

test :: Gadt i o -> Bool
test gadt = case gadt of
  CastGadtNoGivens a -> a
  _ -> False

-- as expected, this would fail:
-- testGivens :: Gadt i o -> (i ~ o => Bool -> r) -> r
-- testGivens gadt f = case gadt of
--   CastGadtNoGivens x -> f x

Furthermore, the code substituting the pattern synonym definition compiles just fine, but that's not really a surprise:

-- This is totally fine
{-# LANGUAGE GADTs, ViewPatterns, TypeOperators #-}

import Data.Typeable
import Data.Type.Equality

data Gadt x y where
  ExistentialInGadt :: Typeable a => a -> Gadt x x

test :: Gadt i o -> (Bool, i :~: o)
test gadt = case gadt of
  ExistentialInGadt (cast -> Just a) -> (a, Refl)
  _ -> undefined

Now, thanks to @int-index being very generous with his time, we more or less figured out why this happens. Specifically, in GHC.Tc.Gen.Pat.tcPatSynPat we have:

        ; (ev_binds, (arg_pats', res))
             <- checkConstraints skol_info ex_tvs' prov_dicts' $
                tcConArgs (PatSynCon pat_syn) arg_tys_scaled tenv penv arg_pats thing_inside

All seems reasonable enough, however with the pattern synonym above, we run into a bit of an issue: checkConstraints wants to know if a is Typeable to construct an implication, however it didn't actually typecheck the constructor arguments yet, as tcConArgs is to be run later. Hence, it can't know yet what a is and whether it's Typeable.

The pattern synonym without givens apparently works because checkConstraints goes into the "fast path" and actually skips building the implications.

I didn't really investigate the code without pattern synonyms, but my hunch is cast is applied before givens are brought into scope (semantically this makes sense at least).

#19847 (closed) and #21501 (closed) seem to be symptoms of this very same issue (to be clear: I didn't run traces, but the setup is the same), but those also use pattern type applications, and that complicates things a bit.

Steps to reproduce

Copy the code above and try to compile it (or load it in GHCi)

Expected behavior

The code compiles, or at least a less arcane error message is produced.

Environment

• GHC version used: 9.0, 9.2, 9.4