PatternSynonyms: Problems with quantified constraints / foralls
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)
| ^^^