[GHC] #11524: Something is amiss with quantification in pattern synonym type signatures

[GHC]

#11524: Something is amiss with quantification in pattern synonym type signatures
-------------------------------------+-------------------------------------
           Reporter:  bgamari        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.0.1
          Component:  Compiler       |           Version:  8.0.1-rc1
  (Type checker)                     |
           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 PolyKinds #-}
 {-# LANGUAGE ExplicitForAll #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeInType #-}

 module Test where

 data AType (a :: k) where
     AMaybe :: AType Maybe
     AInt :: AType Int
     AApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). AType a -> AType b ->
 AType (a b)

 pattern PApp :: () => (fun ~ a b) => AType a -> AType b -> AType fun
 --pattern PApp :: forall k (fun :: k) k1 (a :: k1 -> k) (b :: k1).
 --            () => (fun ~ a b) => AType a -> AType b -> AType fun
 pattern PApp fun arg <- AApp fun arg
 }}}

 I would have thought that the two type signatures would be equivalent.
 However, when I use the quantified signature GHC complains with,
 {{{
 hi.hs:14:34: error:
     • Expected kind ‘AType a’, but ‘fun’ has kind ‘AType a1’
     • In the declaration for pattern synonym ‘PApp’
     • Relevant bindings include
         arg :: AType b1 (bound at hi.hs:14:34)
         fun :: AType a1 (bound at hi.hs:14:30)
 }}}

 Moreover, if I use the un-quantified signature and ask GHCi for the full
 type signature, it gives me the precisely the quantified type that it
 rejected previously,

 {{{
 λ> :info PApp
 pattern PApp :: forall k (fun :: k) k1 (a :: k1
                                              -> k) (b :: k1). () => fun ~
 a b => AType a
 -> AType b
 -> AType fun
         -- Defined at hi.hs:14:1
 }}}

 Very odd.

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