[GHC] #16281: PatternSynonyms doesn't accept non-prenex quantified functions, doesn't float foralls

3 Feb 2019

      #16281: PatternSynonyms doesn't accept non-prenex quantified functions, doesn't
float foralls
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.7
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternSynonyms                    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This works under GHC HEAD (8.7.20190115)

 {{{#!hs
 {-# Language RankNTypes      #-}
 {-# Language ViewPatterns    #-}
 {-# Language PatternSynonyms #-}

 newtype Logic a = Logic (forall xx. (a -> (xx -> xx)) -> (xx -> xx))

 runLogic :: Logic a -> forall xx. (a -> xx -> xx) -> (xx -> xx)
 runLogic (Logic logic) = logic

 pattern L :: (forall xx. (a -> xx -> xx) -> xx -> xx) -> Logic a
 pattern L f <- (runLogic -> f)
 }}}

 I was under the impression that these would be equivalent
 {{{#!hs
 runLogic :: Logic a -> forall xx. (a -> xx -> xx) -> (xx -> xx)
 runLogic :: Logic a ->            (a -> xx -> xx) -> (xx -> xx)
 }}}
 apart from the order of visible type application and such, but it fails:

 {{{#!hs
 {-# Language RankNTypes      #-}
 {-# Language ViewPatterns    #-}
 {-# Language PatternSynonyms #-}

 newtype Logic a = Logic (forall xx. (a -> (xx -> xx)) -> (xx -> xx))

 runLogic :: Logic a -> (a -> xx -> xx) -> (xx -> xx)
 runLogic (Logic logic) = logic

 pattern L :: (forall xx. (a -> xx -> xx) -> xx -> xx) -> Logic a
 pattern L f <- (runLogic -> f)
 }}}

 {{{
 $ ... -ignore-dot-ghci 1022_bug.hs
 GHCi, version 8.7.20190115: https://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( 1022_bug.hs, interpreted )

 1022_bug.hs:11:29: error:
     • Couldn't match expected type ‘forall xx.
                                     (a -> xx -> xx) -> xx -> xx’
                   with actual type ‘(a -> xx0 -> xx0) -> xx0 -> xx0’
     • In the declaration for pattern synonym ‘L’
     • Relevant bindings include
         f :: (a -> xx0 -> xx0) -> xx0 -> xx0 (bound at 1022_bug.hs:11:29)
    |
 11 | pattern L f <- (runLogic -> f)
    |                             ^
 Failed, no modules loaded.
 Prelude>
 }}}

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