Opened 4 years ago

Closed 3 weeks ago

Last modified 3 weeks ago

#9793 closed feature request (fixed)

Some as-patterns could be accepted in pattern synonyms

Reported by: cactus Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 7.8.3
Keywords: PatternSynonyms GHCProposal Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: patsyn/should_fail/as-pattern
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D1666
Wiki Page:

Description

Currently all as-patterns are rejected in pattern synonym definitions, to avoid situations like

pattern P x y <- x@(y:_)

since there's no valid reason to be able to then write something like

f [True] False = ...

this would just lead to confusion.

However, I think we could accept as-patterns where the body of the as-pattern doesn't contain any variable bindings that are accessible via the pattern synonym. In other words, this should be OK:

pattern P x <- x@(y:_)

since it's exactly equivalent to

pattern P x <- x@(_:_)

which I don't think is as confusing as the other example.

I haven't really made up my mind yet if these should be bidirectional; but they certainly could be, by just ignoring the body of the as-pattern in the wrapper; so the following two would be equivalent:

pattern P1 x = [x@(y:_)]
pattern P2 x <- [x@(y:_)]
  where
    P2 x = [x]

Change History (16)

comment:1 Changed 4 years ago by cactus

Keywords: PatternSynonyms added; pattern synonyms removed

comment:2 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:3 Changed 3 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:4 Changed 3 years ago by mpickering

Differential Rev(s): Phab:D1666
Status: newpatch

comment:5 Changed 2 years ago by simonpj

Hang on. What is the design here? Specifically, what is the semantics of matching?

To put it another way, suppose I have

pattern P x <- x@(Right _)

What does it mean to match against that?

Well, to a first approximation, in a pattern, P pat means the same as <rhs of P> with pat instead of x. So

f (P (Left y)) = e

means

f ((Left y)@(Right _)) = e

And what does that mean?

Perhaps we could expand the semantics of as-patterns to be p1 @ p2, meaning match against both p1 and p1. An "and-pattern" if you like. Now everything would be well-specified. And I suppose you could say things like

f ((\xs -> length xs < 10) -> True)@(y:_) = ...

which would match against a list of length shorter than 10, and then bind 'y' to the head of that list.

But this is a bigger change, and not directly related to pattern synonyms.

So far I'm unconvinced.

Simon

comment:6 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In 48e0634/ghc:

Revert "Allow as-patterns in pattern synonym declarations."

I'm reverting this until we agree a design.
See comment:5 in Trac #9793.

Incidentally the reference to Trac #9739 in the reverted
patch is bogus; it shold have said #9793.

This reverts commit 44640af7afa1a01ff2e2357f7c1436b4804866fc.

comment:7 Changed 2 years ago by simonpj

Milestone: 8.0.18.2.1

comment:8 Changed 2 years ago by mpickering

Owner: cactus deleted

comment:9 Changed 2 years ago by mpickering

Keywords: newcomer added

comment:10 Changed 19 months ago by bgamari

Status: patchnew

comment:11 Changed 16 months ago by rwbarton

Keywords: newcomer removed
Milestone: 8.2.18.4.1

comment:12 Changed 5 months ago by bgamari

Milestone: 8.4.18.6.1

This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.

comment:13 Changed 4 months ago by typedrat

I'm running up against this right now, and while the idea of contributing to GHC (especially with what may be an extremely non-trivial first submitted change) is daunting, I'd be happy to at least try and do it if a design is decided on.

Generally, my use case is trying to fake impredicative types in the specific application of GADT phantom types, and being able to just erase the existential wrapper from view and make it look like perfectly normal pattern matching when it's actually being taken apart would make it "feel" a lot nicer, in my opinion.

Last edited 4 months ago by typedrat (previous) (diff)

comment:14 Changed 4 months ago by simonpj

See https://github.com/ghc-proposals/ghc-proposals/pull/94, where I propose loosening the rules for as-patterns.

Perhaps your use-case would strengthen the case. Can you explain it with code? (You could do so here, and then add a comment to the proposal thread pointing to it._

comment:15 Changed 3 weeks ago by RyanGlScott

Resolution: fixed
Status: newclosed
Test Case: patsyn/should_fail/as-pattern

This was implemented in commit 411a97e2c0083529b4259d0cad8f453bae110dee.

comment:16 Changed 3 weeks ago by RyanGlScott

Keywords: GHCProposal added
Note: See TracTickets for help on using tickets.