PatternSynonyms doesn't accept non-prenex quantified functions, doesn't float foralls

This works under GHC HEAD (8.7.20190115)

{-# 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

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:

{-# 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>

Trac metadata

Trac field	Value
Version	8.7
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

The problem is that the thing after the :: in pattern Blah :: is not a type. It's a type-like thing, with requireds, universals, provideds, existentials, arguments, and a result, all arranged using familiar notation. Perhaps someday, we'll generalize this, allowing type variables to appear in arbitrary positions within the type (maybe someone wants an existential before a universal, for example), but this is a largish design problem.

I'm inclined to "wontfix" for this one, leaving it for a ghc-proposal to flesh out all the details of the new design.

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedWon'tFix

added PatternSynonyms label

added Pnormal label