[GHC] #12820: Regression around pattern synonyms and higher-rank types

[GHC]

#12820: Regression around pattern synonyms and higher-rank types
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             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:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 What makes you say it's correct?

 Consier
 {{{
 f :: String -> Int
 f ( (\_ -> id) -> (x :: forall a. a->a) ) = 3
 }}}
 This too is rejected with
 {{{
 T12820.hs:10:20: error:
     * Couldn't match expected type `a0 -> a0'
                   with actual type `forall a. a -> a'
     * When checking that the pattern signature: forall a. a -> a
         fits the type of its context: a0 -> a0
       In the pattern: x :: forall a. a -> a
       In the pattern: (\ _ -> id) -> (x :: forall a. a -> a)
 }}}
 Suppose we are inferring the type of `f -> p`.  W could either

 * Infer the type of `f`, and use that to check the type of pattern `p`, or
 * Infer the type of `p`, and use that to check the type of `f` (actually
 it only fixes teh result type of `f` but still.

 We use the first alternative, but perhpas the second makes more sense.

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