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.

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