Opened 4 years ago

Last modified 3 years ago

#11646 new feature request

Make pattern synonym export type mismatch a warning

Reported by: dfeuer Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1-rc2
Keywords: PatternSynonyms Cc: mpickering, rdragon
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page: PatternSynonyms/AssociatingSynonyms


As I understand it, attempting to associate a pattern synonym with a type constructor that it "obviously" doesn't match is an error. This is strange for two reasons:

  1. An "erroneous" association cannot compromise type safety.
  1. The test is incomplete.

Therefore, I believe such mismatches should lead to warnings instead of errors.

Change History (6)

comment:1 Changed 4 years ago by thomie

Cc: mpickering rdragon added
Keywords: PatternSynonyms added
Wiki Page: PatternSynonyms/AssociatingSynonyms

dfeuer: do you have an example, so the PatternSynonyms experts have something to work with. Thanks.

comment:2 Changed 4 years ago by mpickering

You understand correctly. The check would be better but it is difficult to specify when a pattern synonym should and should not be allowed to bundled.

Do you have an example where the check prevents you from writing the program you want to write?

comment:3 Changed 3 years ago by thomie

Resolution: wontfix
Status: newclosed

No response from submitter. Unclear which problem this feature would solve. Please reopen if you disagree.

comment:4 in reply to:  3 Changed 3 years ago by dfeuer

Replying to thomie:

No response from submitter. Unclear which problem this feature would solve. Please reopen if you disagree.

I disagree on philosophical grounds somewhat more than practical grounds. Pattern synonyms are fundamentally a syntactic feature. The essential idea is that we're writing introduction and elimination functions and tying them to construction and pattern matching syntax. In the associated pattern syntax, we tie a type constructor name to pattern synonym bindings. The type checker has essentially nothing useful to contribute at the export stage. I think it should really stay completely out of the way. Others disagree, for their own reasons, but I'd like to at least be able to say that I don't care and I'd like it to leave me alone.

I'll be opening another ticket shortly relating to a more practical problem with the way pattern synonyms are typed, to which the most obvious solution is essentially "Just let me do what I want, because it can't hurt type safety." Same philosophy here.

comment:5 Changed 3 years ago by dfeuer

Resolution: wontfix
Status: closednew

comment:6 Changed 3 years ago by simonpj

So to be concrete, you want to allow this:

module M( Maybe( Nothing, Just, P ) ) where

pattern P x = [x, True]

So now an importing module can import Maybe(..) and will get two data constructors for Maybe and one for lists.

I agree that there is nothing unsound about this, just a bit unexpected. I'd be perfectly OK with issuing a warning rather than an error.

But doing anything at all requires some work from someone. And it may well be that someone then pops up to say "it really really should be an error". So a compelling use-case or two, and evidence of interest from other users would help. Does anyone else have an opinion.

Note: See TracTickets for help on using tickets.