[GHC] #10928: Refine pattern synonym signatures
GHC
ghc-devs at haskell.org
Wed Oct 7 13:33:28 UTC 2015
#10928: Refine pattern synonym signatures
-------------------------------------+-------------------------------------
Reporter: mpickering | Owner:
Type: bug | Status: new
Priority: normal | Milestone: 8.0.1
Component: Compiler | Version: 7.10.2
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: Other | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
-------------------------------------+-------------------------------------
Comment (by goldfire):
Concur with comment:14. Keep current syntax, but with reversed ordering.
Specifying only one constraint would now indicate a '''required'''
constraint.
On a separate note, the parallelism with GADT syntax discussed in
comment:12 is already broken. Consider
{{{#!hs
data G a where
MkG :: G Int
pattern P :: G Int
pattern P = MkG
}}}
The pattern and the data constructor have '''different''' static
semantics. Specifically,
{{{#!hs
-- this works:
ctor :: G a -> a
ctor MkG = 5
-- this doesn't:
pat :: G a -> a
pat P = 5
}}}
This is because a non-uniformity in the return type of a pattern is taken
as a required equality constraint, not a provided equality constraint. The
top set of definitions is equivalent to
{{{#!hs
data G a where
MkG :: a ~ Int => G a
pattern P :: {- required -} a ~ Int => {- provided -} () => G a
pattern P = MkG
}}}
This was a design decision made in pattern synonym typing. I don't love
this decision, but I can't quite argue against it either. It's one more
way in which we must be honest that the things appearing after `MkG ::`
and `P ::` are '''not''' types, but type-like specifications with a very
specific interpretation.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10928#comment:16>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list