[GHC] #9954: Required constraints are not inferred for pattern synonyms involving GADTs

[GHC]

#9954: Required constraints are not inferred for pattern synonyms involving GADTs
-------------------------------------+-------------------------------------
              Reporter:  cactus      |             Owner:  cactus
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:
  (Type checker)                     |  Operating System:  Unknown/Multiple
              Keywords:              |   Type of failure:  GHC rejects
  PatternSynonyms                    |  valid program
          Architecture:              |        Blocked By:
  Unknown/Multiple                   |   Related Tickets:  #9953
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Let's say we have the following setup:

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

 data T a where
   MkT1 :: a -> T a
   MkT2 :: a -> T (Maybe a)

 f :: (Eq a) => a -> a
 f = id
 }}}

 Then the following definition works as expected:

 {{{#!hs
 pattern P1 x <- MkT1 (f -> x)
 }}}

 with the following inferred type:

 {{{
 λ» :i P1
 pattern P1 :: () => Eq t => t -> T t
 }}}

 However, trying to do the same with {{MkT2}} doesn't work:

 {{{#!hs
 pattern P2 x <- MkT2 (f -> x)
 }}}

 this results in

 {{{
 Could not deduce (Eq a1) arising from a use of ‘f’
 from the context (t ~ Maybe a1)
   bound by a pattern with constructor
              MkT2 :: forall a. a -> T (Maybe a),
            in a pattern synonym declaration
 }}}

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