Opened 8 months ago

Closed 8 months ago

#16281 closed bug (wontfix)

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

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.7
Keywords: PatternSynonyms Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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>

Change History (2)

comment:1 Changed 8 months ago by goldfire

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.

comment:2 Changed 8 months ago by goldfire

Resolution: wontfix
Status: newclosed
Note: See TracTickets for help on using tickets.