Opened 18 months ago

Last modified 9 months ago

#15020 new bug

PatternSynonyms: Problems with quantified constraints / foralls

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.5
Keywords: PatternSynonyms Cc:
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 (last modified by Iceland_jack)

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

Change History (4)

comment:1 Changed 18 months ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 17 months ago by simonpj

Interesting. Would you expect the following to work?

data Lam2 a = Lam2 (forall mm. Monad mm => mm a)
            | Other
newtype Forall f = Forall (forall xx. f xx)

mLam2 :: Forall Lam2 -> r -> ((forall xx mm. Monad mm => mm xx) -> r) -> r
mLam2 (Forall (Lam2 lam)) d k = k lam
mLam2 (Forall Other)      d k = d

Here mLam2 is the sort of matching function that GHC builds for PLam2. And indeed mLam2 is rejected because lam is not polymorphic enough.

Is that so unreasonable?

(I checked why mkLam3 works; it's because teh pattern matching is pushed into the argument of the continuation, something like this

mLam3 :: Forall Lam2 -> r -> ((forall xx mm. Monad mm => mm xx) -> r) -> r
mLam3 x d k = k (case x of { Forall (Lam2 lam) -> lam })

But this won't work when we want to bind multiple arguments, or when the match can fail.)

I don't see an easy way to improve this.

comment:3 Changed 15 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be addressed by GHC 8.6.

comment:4 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.