#15020: PatternSynonyms: Problems with quantified constraints / foralls -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | PatternSynonyms 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 changed by Iceland_jack: Old description:

I couldn't find a way to implement `PLam2` as a simply bidirectional pattern synonym, I expected it to work but I recall a similar ticket. I couldn't find it though.

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

newtype Lam1 = Lam1 (forall xx mm. Monad mm => mm xx)

pattern PLam1 :: (forall xx mm. Monad mm => mm xx) -> Lam1 pattern PLam1 a = Lam1 a

--

newtype Lam2 a = Lam2 (forall mm. Monad mm => mm a)

newtype Forall f = Forall (forall xx. f xx)

-- · FAILS · -- pattern PLam2 :: (forall xx mm. Monad mm => mm xx) -> Forall Lam2 -- pattern PLam2 lam = Forall (Lam2 lam)

--

get :: Forall Lam2 -> forall xx mm. Monad mm => mm xx get (Forall (Lam2 lam)) = lam

pattern PLam3 :: (forall xx mm. Monad mm => mm xx) -> Forall Lam2 pattern PLam3 lam <- (get -> lam) where PLam3 lam = Forall (Lam2 lam) }}}

The complaint is and I wonder if this is a limitation of PatternSynonyms

{{{ • Couldn't match type ‘xx0’ with ‘xx’ because type variable ‘xx’ would escape its scope This (rigid, skolem) type variable is bound by a type expected by the context: forall xx (mm :: * -> *). Monad mm => mm xx at Test.hs:16:34-36 Expected type: mm xx Actual type: mm xx0 • In the declaration for pattern synonym ‘PLam2’ • Relevant bindings include lam :: forall (mm :: * -> *). Monad mm => mm xx0 (bound at Test.hs:16:34) | 16 | pattern PLam2 lam = Forall (Lam2 lam) | ^^^ }}}

New description: I couldn't find a way to implement `PLam2` as a simply bidirectional pattern synonym, I expected it to work but I recall a similar ticket. I couldn't find it though. {{{#!hs {-# Language RankNTypes, PatternSynonyms, ViewPatterns #-} newtype Lam1 = Lam1 (forall xx mm. Monad mm => mm xx) pattern PLam1 :: (forall xx mm. Monad mm => mm xx) -> Lam1 pattern PLam1 a = Lam1 a -- newtype Lam2 a = Lam2 (forall mm. Monad mm => mm a) newtype Forall f = Forall (forall xx. f xx) -- · FAILS · -- pattern PLam2 :: (forall xx mm. Monad mm => mm xx) -> Forall Lam2 -- pattern PLam2 lam = Forall (Lam2 lam) -- get :: Forall Lam2 -> forall xx mm. Monad mm => mm xx get (Forall (Lam2 lam)) = lam pattern PLam3 :: (forall xx mm. Monad mm => mm xx) -> Forall Lam2 pattern PLam3 lam <- (get -> lam) where PLam3 lam = Forall (Lam2 lam) }}} The complaint is `V`, I wonder if this is a limitation of PatternSynonyms {{{ • Couldn't match type ‘xx0’ with ‘xx’ because type variable ‘xx’ would escape its scope This (rigid, skolem) type variable is bound by a type expected by the context: forall xx (mm :: * -> *). Monad mm => mm xx at Test.hs:16:34-36 Expected type: mm xx Actual type: mm xx0 • In the declaration for pattern synonym ‘PLam2’ • Relevant bindings include lam :: forall (mm :: * -> *). Monad mm => mm xx0 (bound at Test.hs:16:34) | 16 | pattern PLam2 lam = Forall (Lam2 lam) | ^^^ }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15020#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler