Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,249
    • Issues 4,249
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 391
    • Merge Requests 391
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #15020

Closed
Open
Opened Apr 10, 2018 by Icelandjack@IcelandjackReporter

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)
   |                                  ^^^
Edited Mar 10, 2019 by Icelandjack
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#15020