Permit data types in signatures to be implemented with equivalent pattern synonyms (and vice versa)

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?)

Trac metadata

Trac field	Value
Version	8.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	lowest
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture