
#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 kosmikus): I agree completely with the function example. I'm just sure about whether the pattern synonym situation is really analogous. The reason is that in {{{ data T a b where MkT :: a -> T a Bool MkX :: T a b pattern P = MkT True }}} 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 }}} Then both `f` and `g` as shown above using `P` would type-check. So if for `P` as a constructor, the information that the "expression type" is `T Bool Bool` and the "target type" is `T a b` is sufficient, then why can't we do the same for `P` as a pattern synonym. That's still modular, IMHO. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler