[GHC] #12717: Permit data types in signatures to be implemented with equivalent pattern synonyms (and vice versa)

[GHC]

#12717: Permit data types in signatures to be implemented with equivalent pattern
synonyms (and vice versa)
-------------------------------------+-------------------------------------
           Reporter:  ezyang         |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  lowest         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:  backpack       |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Suppose I write in a signature:

 {{{
 data Type = TArrow t1 t2 | TApp String [Type]
 }}}

 But it turns out that the real data type only has TApp (and uses "->" as
 the TyCon for TArrow). It would be nice if a pattern synonym could be used
 to implement this "concrete abstract data type" instead. Signature
 matching would have to typecheck the pattern synonyms against each other,
 and also check for totality. Note that in this example, App would need a
 guard against the Arrow case; otherwise the patterns overlap, whereas in
 the data type above it shouldn't matter what order the patterns go in.

 The converse might be useful too:

 {{{
 data Type
 pattern TArrow :: Type -> Type -> Type
 pattern TInt :: Type
 }}}

 These patterns would be available for matching, with the assumption that
 they weren't total. If they were implemented directly using constructors,
 that should not be a problem. (In fact, do we even support abstract
 pattern synonyms?)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12717>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler