Pattern match checker mistakenly concludes pattern match on pattern synonym is unreachable

Consider this program,

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}

module Test where

import GHC.Exts
import Data.Kind

data TypeRep (a :: k) where
    Con :: TypeRep (a :: k)
    TrFun   :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                      (a :: TYPE r1) (b :: TYPE r2).
               TypeRep a
            -> TypeRep b
            -> TypeRep (a -> b)

pattern Fun :: forall k (fun :: k). ()
            => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                      (arg :: TYPE r1) (res :: TYPE r2).
               (k ~ Type, fun ~~ (arg -> res))
            => TypeRep arg
            -> TypeRep res
            -> TypeRep fun
pattern Fun arg res <- TrFun arg res
  where Fun arg res = undefined

data Dynamic where
    Dynamic :: forall a. TypeRep a -> a -> Dynamic

-- Removing this allows compilation to proceed
{-# COMPLETE Con #-}

dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
-- Changing Fun to TrFun allows compilation to proceed
dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined
dynApply _ _ = Nothing

As written the program fails with,

test.hs:34:1: warning: [-Woverlapping-patterns]
    Pattern match has inaccessible right hand side
    In an equation for ‘dynApply’:
        dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = ...
   |
34 | dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This can be worked around by doing one of the following,

1. Removing the COMPLETE pragma
2. Changing the use of the Fun pattern synonym into a use of the TrFun constructor.

Something is quite wrong here.

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	George
Operating system
Architecture