[GHC] #15020: PatternSynonyms: Problems with quantified constraints / foralls

[GHC]

#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