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

10 Apr 2018

      #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
           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:
-------------------------------------+-------------------------------------
 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)
    |                                  ^^^
 }}}

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