[GHC] #14253: Pattern match checker mistakenly concludes pattern match on pattern synonym is unreachable

[GHC]

#14253: Pattern match checker mistakenly concludes pattern match on pattern synonym
is unreachable
-------------------------------------+-------------------------------------
           Reporter:  bgamari        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.4.1
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider this program,
 {{{#!hs
 {-# 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14253>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler