#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by simonpj):
I could just pretend that `P` is another constructor of `T`: {{{ data T a b where MkT :: a -> T a Bool MkX :: T a b P :: T Bool Bool }}} Alas, no. If the definition of T really did have that constructor P, then GADT-style type refinement would take place when you match on P. So for example, this would typecheck: {{{ f :: T a b -> a -> Bool f P v = v && True }}} But obviously the expansion does not: {{{ f :: T a b -> a -> Bool f (MkT x) v = v && True }}} Moreover, these are terribly simple examples. In general a pattern synonym might mention dozens of constructor from dozens of types. Which of those types would you like to pretend the pattern synonym constructor is from?
This is what I mean by modularity: no matter how complicated the right hand side of the pattern synonym, I want the client (of the library defining the pattern synonym) to be able to use it by knowing only its type -- just like he can for a function exported by a library. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler